Theory "intreal"

Parents real Omega int_arith

Signature

Constant	Type
INT_CEILING	:real -> int
INT_FLOOR	:real -> int
is_int	:real -> bool
real_of_int	:int -> real

Definitions

real_of_int

⊢ ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i

is_int_def

⊢ ∀x. is_int x ⇔ (x = real_of_int (flr x))

INT_FLOOR_def

⊢ ∀x. flr x = LEAST_INT i. x < real_of_int (i + 1)

INT_CEILING_def

⊢ ∀x. clg x = LEAST_INT i. x ≤ real_of_int i

Theorems

real_of_int_sub

⊢ real_of_int (m − n) = real_of_int m − real_of_int n

real_of_int_num

⊢ real_of_int (&n) = &n

real_of_int_neg

⊢ real_of_int (-m) = -real_of_int m

real_of_int_mul

⊢ real_of_int (m * n) = real_of_int m * real_of_int n

real_of_int_monotonic

⊢ ∀i j. i < j ⇒ real_of_int i < real_of_int j

real_of_int_lt

⊢ real_of_int m < real_of_int n ⇔ m < n

real_of_int_le

⊢ real_of_int m ≤ real_of_int n ⇔ m ≤ n

real_of_int_def

⊢ ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i

real_of_int_add

⊢ real_of_int (m + n) = real_of_int m + real_of_int n

real_of_int_11

⊢ (real_of_int m = real_of_int n) ⇔ (m = n)

INT_FLOOR_EQNS

⊢ (∀n. flr (&n) = &n) ∧ (∀n. flr (-&n) = -&n) ∧
  (∀n m. 0 < m ⇒ (flr (&n / &m) = &n / &m)) ∧
  ∀n m. 0 < m ⇒ (flr (-&n / &m) = -&n / &m)

INT_FLOOR_compute

⊢ (flr (&n) = &n) ∧ (flr (-&n) = -&n) ∧
  (flr (&n / &NUMERAL (BIT1 m)) = &n / &NUMERAL (BIT1 m)) ∧
  (flr (&n / &NUMERAL (BIT2 m)) = &n / &NUMERAL (BIT2 m)) ∧
  (flr (-&n / &NUMERAL (BIT1 m)) = -&n / &NUMERAL (BIT1 m)) ∧
  (flr (-&n / &NUMERAL (BIT2 m)) = -&n / &NUMERAL (BIT2 m))

INT_FLOOR_BOUNDS

⊢ ∀r. real_of_int (flr r) ≤ r ∧ r < real_of_int (flr r + 1)

INT_FLOOR

⊢ ∀r i. (flr r = i) ⇔ real_of_int i ≤ r ∧ r < real_of_int (i + 1)

INT_CEILING_INT_FLOOR

⊢ ∀r. clg r = (let i = flr r in if real_of_int i = r then i else i + 1)

INT_CEILING_BOUNDS

⊢ ∀r. real_of_int (clg r − 1) < r ∧ r ≤ real_of_int (clg r)

INT_CEILING

⊢ ∀r i. (clg r = i) ⇔ real_of_int (i − 1) < r ∧ r ≤ real_of_int i