Theory: intreal

Theorems

INT_CEILING

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

INT_CEILING'

⊢ ∀r i. ⌈r⌉ = i ⇔ r ≤ real_of_int i ∧ real_of_int i < r + 1

INT_CEILING_ADD_NUM

⊢ ⌈x + &n⌉ = ⌈x⌉ + &n ∧ ⌈&n + x⌉ = ⌈x⌉ + &n

INT_CEILING_BOUNDS

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

INT_CEILING_BOUNDS'

⊢ ∀r. r ≤ real_of_int ⌈r⌉ ∧ real_of_int ⌈r⌉ < r + 1

INT_CEILING_COMPUTE

⊢ ⌈0⌉ = 0 ∧
  ⌈&m⌉ = (let i = ⌊&m⌋ in if real_of_int i = &m then i else i + 1) ∧
  ⌈-&m⌉ = (let i = ⌊-&m⌋ in if real_of_int i = -&m then i else i + 1) ∧
  (⌈&NUMERAL (BIT1 m) / &NUMERAL (BIT1 n)⌉ =
   (let
      i = ⌊&NUMERAL (BIT1 m) / &NUMERAL (BIT1 n)⌋
    in
      if real_of_int i = &NUMERAL (BIT1 m) / &NUMERAL (BIT1 n) then i
      else i + 1) ∧
   ⌈&NUMERAL (BIT2 m) / &NUMERAL (BIT1 n)⌉ =
   (let
      i = ⌊&NUMERAL (BIT2 m) / &NUMERAL (BIT1 n)⌋
    in
      if real_of_int i = &NUMERAL (BIT2 m) / &NUMERAL (BIT1 n) then i
      else i + 1) ∧
   ⌈&NUMERAL (BIT1 m) / &NUMERAL (BIT2 n)⌉ =
   (let
      i = ⌊&NUMERAL (BIT1 m) / &NUMERAL (BIT2 n)⌋
    in
      if real_of_int i = &NUMERAL (BIT1 m) / &NUMERAL (BIT2 n) then i
      else i + 1) ∧
   ⌈&NUMERAL (BIT2 m) / &NUMERAL (BIT2 n)⌉ =
   (let
      i = ⌊&NUMERAL (BIT2 m) / &NUMERAL (BIT2 n)⌋
    in
      if real_of_int i = &NUMERAL (BIT2 m) / &NUMERAL (BIT2 n) then i
      else i + 1)) ∧
  ⌈-&NUMERAL (BIT1 m) / &NUMERAL (BIT1 n)⌉ =
  (let
     i = ⌊-&NUMERAL (BIT1 m) / &NUMERAL (BIT1 n)⌋
   in
     if real_of_int i = -&NUMERAL (BIT1 m) / &NUMERAL (BIT1 n) then i
     else i + 1) ∧
  ⌈-&NUMERAL (BIT2 m) / &NUMERAL (BIT1 n)⌉ =
  (let
     i = ⌊-&NUMERAL (BIT2 m) / &NUMERAL (BIT1 n)⌋
   in
     if real_of_int i = -&NUMERAL (BIT2 m) / &NUMERAL (BIT1 n) then i
     else i + 1) ∧
  ⌈-&NUMERAL (BIT1 m) / &NUMERAL (BIT2 n)⌉ =
  (let
     i = ⌊-&NUMERAL (BIT1 m) / &NUMERAL (BIT2 n)⌋
   in
     if real_of_int i = -&NUMERAL (BIT1 m) / &NUMERAL (BIT2 n) then i
     else i + 1) ∧
  ⌈-&NUMERAL (BIT2 m) / &NUMERAL (BIT2 n)⌉ =
  (let
     i = ⌊-&NUMERAL (BIT2 m) / &NUMERAL (BIT2 n)⌋
   in
     if real_of_int i = -&NUMERAL (BIT2 m) / &NUMERAL (BIT2 n) then i
     else i + 1)

INT_CEILING_INT_FLOOR

⊢ ∀r. ⌈r⌉ = (let i = ⌊r⌋ in if real_of_int i = r then i else i + 1)

INT_CEILING_NEG

⊢ ∀x. ⌈-x⌉ = -⌊x⌋

INT_CEILING_SUB_NUM

⊢ ⌈x − &n⌉ = ⌈x⌉ − &n ∧ ⌈&n − x⌉ = ⌈-x⌉ + &n

INT_FLOOR

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

INT_FLOOR'

⊢ ∀r i. ⌊r⌋ = i ⇔ r − 1 < real_of_int i ∧ real_of_int i ≤ r

INT_FLOOR_ADD_NUM

⊢ ⌊x + &n⌋ = ⌊x⌋ + &n ∧ ⌊&n + x⌋ = ⌊x⌋ + &n

INT_FLOOR_BOUNDS

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

INT_FLOOR_BOUNDS'

⊢ ∀r. r − 1 < real_of_int ⌊r⌋ ∧ real_of_int ⌊r⌋ ≤ r

INT_FLOOR_EQNS

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

INT_FLOOR_MONO

⊢ x < y ⇒ ⌊x⌋ ≤ ⌊y⌋

INT_FLOOR_NEG

⊢ ∀x. ⌊-x⌋ = -⌈x⌉

INT_FLOOR_SUB1

⊢ ⌊x − 1⌋ = ⌊x⌋ − 1

INT_FLOOR_SUB_NUM

⊢ ⌊x − &n⌋ = ⌊x⌋ − &n ∧ ⌊&n − x⌋ = ⌊-x⌋ + &n

INT_FLOOR_SUC

⊢ ⌊x + 1⌋ = ⌊x⌋ + 1

INT_FLOOR_SUM

⊢ ⌊x + real_of_int y⌋ = ⌊x⌋ + y ∧ ⌊real_of_int y + x⌋ = ⌊x⌋ + y

INT_FLOOR_SUM_NUM

⊢ ⌊x + &n⌋ = ⌊x⌋ + &n ∧ ⌊&n + x⌋ = ⌊x⌋ + &n

INT_FLOOR_compute

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

INT_NUM_CEILING

⊢ ∀r. 0 ≤ r ⇒ &clg r = ⌈r⌉

INT_NUM_FLOOR

⊢ ∀r. 0 ≤ r ⇒ &flr r = ⌊r⌋

int_floor_1

⊢ ⌊&n⌋ = &n ∧ ⌊-&n⌋ = -&n

ints_exist_in_gaps

⊢ ∀a b. a + 1 < b ⇒ ∃i. a < real_of_int i ∧ real_of_int i < b

is_int_alt

⊢ ∀x. is_int x ⇔ x = real_of_int ⌈x⌉

is_int_eq_frac_0

⊢ ∀x. is_int x ⇔ frac x = 0

is_int_thm

⊢ ∀x. is_int x ⇔ ⌊x⌋ = ⌈x⌉

real_of_int_11

⊢ real_of_int m = real_of_int n ⇔ m = n

real_of_int_EQN

⊢ (real_of_int i = &n ⇔ i = &n) ∧ (&n = real_of_int i ⇔ i = &n) ∧
  (real_of_int i = -&n ⇔ i = -&n) ∧ (-&n = real_of_int i ⇔ i = -&n)

real_of_int_add

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

real_of_int_def

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

real_of_int_le

⊢ real_of_int m ≤ real_of_int n ⇔ m ≤ n

real_of_int_lt

⊢ real_of_int m < real_of_int n ⇔ m < n

real_of_int_monotonic

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

real_of_int_mul

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

real_of_int_neg

⊢ real_of_int (-m) = -real_of_int m

real_of_int_num

⊢ real_of_int (&n) = &n

real_of_int_sub

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

Theory intreal

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems