Structure intrealTheory

signature intrealTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val INT_CEILING_def : thm
    val INT_FLOOR_def : thm
    val frac_def : thm
    val is_int_def : thm
    val real_of_int : thm
  
  (*  Theorems  *)
    val INT_CEILING : thm
    val INT_CEILING' : thm
    val INT_CEILING_ADD_NUM : thm
    val INT_CEILING_BOUNDS : thm
    val INT_CEILING_BOUNDS' : thm
    val INT_CEILING_COMPUTE : thm
    val INT_CEILING_INT_FLOOR : thm
    val INT_CEILING_NEG : thm
    val INT_CEILING_SUB_NUM : thm
    val INT_FLOOR : thm
    val INT_FLOOR' : thm
    val INT_FLOOR_ADD_NUM : thm
    val INT_FLOOR_BOUNDS : thm
    val INT_FLOOR_BOUNDS' : thm
    val INT_FLOOR_EQNS : thm
    val INT_FLOOR_MONO : thm
    val INT_FLOOR_NEG : thm
    val INT_FLOOR_SUB1 : thm
    val INT_FLOOR_SUB_NUM : thm
    val INT_FLOOR_SUC : thm
    val INT_FLOOR_SUM : thm
    val INT_FLOOR_SUM_NUM : thm
    val INT_FLOOR_compute : thm
    val INT_NUM_CEILING : thm
    val INT_NUM_FLOOR : thm
    val int_floor_1 : thm
    val ints_exist_in_gaps : thm
    val is_int_alt : thm
    val is_int_eq_frac_0 : thm
    val is_int_thm : thm
    val real_of_int_11 : thm
    val real_of_int_add : thm
    val real_of_int_def : thm
    val real_of_int_le : thm
    val real_of_int_lt : thm
    val real_of_int_monotonic : thm
    val real_of_int_mul : thm
    val real_of_int_neg : thm
    val real_of_int_num : thm
    val real_of_int_sub : thm
(*
   [Omega] Parent theory of "intreal"
   
   [real] Parent theory of "intreal"
   
   [INT_CEILING_def]  Definition
      
      ⊢ ∀x. ⌈x⌉ = LEAST_INT i. x ≤ real_of_int i
   
   [INT_FLOOR_def]  Definition
      
      ⊢ ∀x. ⌊x⌋ = LEAST_INT i. x < real_of_int (i + 1)
   
   [frac_def]  Definition
      
      ⊢ ∀x. frac x = x − real_of_int ⌊x⌋
   
   [is_int_def]  Definition
      
      ⊢ ∀x. is_int x ⇔ x = real_of_int ⌊x⌋
   
   [real_of_int]  Definition
      
      ⊢ ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i
   
   [INT_CEILING]  Theorem
      
      ⊢ ∀r i. ⌈r⌉ = i ⇔ real_of_int (i − 1) < r ∧ r ≤ real_of_int i
   
   [INT_CEILING']  Theorem
      
      ⊢ ∀r i. ⌈r⌉ = i ⇔ r ≤ real_of_int i ∧ real_of_int i < r + 1
   
   [INT_CEILING_ADD_NUM]  Theorem
      
      ⊢ ⌈x + &n⌉ = ⌈x⌉ + &n ∧ ⌈&n + x⌉ = ⌈x⌉ + &n
   
   [INT_CEILING_BOUNDS]  Theorem
      
      ⊢ ∀r. real_of_int (⌈r⌉ − 1) < r ∧ r ≤ real_of_int ⌈r⌉
   
   [INT_CEILING_BOUNDS']  Theorem
      
      ⊢ ∀r. r ≤ real_of_int ⌈r⌉ ∧ real_of_int ⌈r⌉ < r + 1
   
   [INT_CEILING_COMPUTE]  Theorem
      
      ⊢ ⌈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]  Theorem
      
      ⊢ ∀r. ⌈r⌉ = (let i = ⌊r⌋ in if real_of_int i = r then i else i + 1)
   
   [INT_CEILING_NEG]  Theorem
      
      ⊢ ∀x. ⌈-x⌉ = -⌊x⌋
   
   [INT_CEILING_SUB_NUM]  Theorem
      
      ⊢ ⌈x − &n⌉ = ⌈x⌉ − &n ∧ ⌈&n − x⌉ = ⌈-x⌉ + &n
   
   [INT_FLOOR]  Theorem
      
      ⊢ ∀r i. ⌊r⌋ = i ⇔ real_of_int i ≤ r ∧ r < real_of_int (i + 1)
   
   [INT_FLOOR']  Theorem
      
      ⊢ ∀r i. ⌊r⌋ = i ⇔ r − 1 < real_of_int i ∧ real_of_int i ≤ r
   
   [INT_FLOOR_ADD_NUM]  Theorem
      
      ⊢ ⌊x + &n⌋ = ⌊x⌋ + &n ∧ ⌊&n + x⌋ = ⌊x⌋ + &n
   
   [INT_FLOOR_BOUNDS]  Theorem
      
      ⊢ ∀r. real_of_int ⌊r⌋ ≤ r ∧ r < real_of_int (⌊r⌋ + 1)
   
   [INT_FLOOR_BOUNDS']  Theorem
      
      ⊢ ∀r. r − 1 < real_of_int ⌊r⌋ ∧ real_of_int ⌊r⌋ ≤ r
   
   [INT_FLOOR_EQNS]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ x < y ⇒ ⌊x⌋ ≤ ⌊y⌋
   
   [INT_FLOOR_NEG]  Theorem
      
      ⊢ ∀x. ⌊-x⌋ = -⌈x⌉
   
   [INT_FLOOR_SUB1]  Theorem
      
      ⊢ ⌊x − 1⌋ = ⌊x⌋ − 1
   
   [INT_FLOOR_SUB_NUM]  Theorem
      
      ⊢ ⌊x − &n⌋ = ⌊x⌋ − &n ∧ ⌊&n − x⌋ = ⌊-x⌋ + &n
   
   [INT_FLOOR_SUC]  Theorem
      
      ⊢ ⌊x + 1⌋ = ⌊x⌋ + 1
   
   [INT_FLOOR_SUM]  Theorem
      
      ⊢ ⌊x + real_of_int y⌋ = ⌊x⌋ + y ∧ ⌊real_of_int y + x⌋ = ⌊x⌋ + y
   
   [INT_FLOOR_SUM_NUM]  Theorem
      
      ⊢ ⌊x + &n⌋ = ⌊x⌋ + &n ∧ ⌊&n + x⌋ = ⌊x⌋ + &n
   
   [INT_FLOOR_compute]  Theorem
      
      ⊢ ⌊&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]  Theorem
      
      ⊢ ∀r. 0 ≤ r ⇒ &clg r = ⌈r⌉
   
   [INT_NUM_FLOOR]  Theorem
      
      ⊢ ∀r. 0 ≤ r ⇒ &flr r = ⌊r⌋
   
   [int_floor_1]  Theorem
      
      ⊢ ⌊&n⌋ = &n ∧ ⌊-&n⌋ = -&n
   
   [ints_exist_in_gaps]  Theorem
      
      ⊢ ∀a b. a + 1 < b ⇒ ∃i. a < real_of_int i ∧ real_of_int i < b
   
   [is_int_alt]  Theorem
      
      ⊢ ∀x. is_int x ⇔ x = real_of_int ⌈x⌉
   
   [is_int_eq_frac_0]  Theorem
      
      ⊢ ∀x. is_int x ⇔ frac x = 0
   
   [is_int_thm]  Theorem
      
      ⊢ ∀x. is_int x ⇔ ⌊x⌋ = ⌈x⌉
   
   [real_of_int_11]  Theorem
      
      ⊢ real_of_int m = real_of_int n ⇔ m = n
   
   [real_of_int_add]  Theorem
      
      ⊢ real_of_int (m + n) = real_of_int m + real_of_int n
   
   [real_of_int_def]  Theorem
      
      ⊢ ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i
   
   [real_of_int_le]  Theorem
      
      ⊢ real_of_int m ≤ real_of_int n ⇔ m ≤ n
   
   [real_of_int_lt]  Theorem
      
      ⊢ real_of_int m < real_of_int n ⇔ m < n
   
   [real_of_int_monotonic]  Theorem
      
      ⊢ ∀i j. i < j ⇒ real_of_int i < real_of_int j
   
   [real_of_int_mul]  Theorem
      
      ⊢ real_of_int (m * n) = real_of_int m * real_of_int n
   
   [real_of_int_neg]  Theorem
      
      ⊢ real_of_int (-m) = -real_of_int m
   
   [real_of_int_num]  Theorem
      
      ⊢ real_of_int (&n) = &n
   
   [real_of_int_sub]  Theorem
      
      ⊢ real_of_int (m − n) = real_of_int m − real_of_int n
   
   
*)
end

HOL 4, Trindemossen-2