Structure intrealTheory

signature intrealTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val INT_CEILING_def : thm
    val INT_FLOOR_def : thm
    val is_int_def : thm
    val real_of_int : thm
  
  (*  Theorems  *)
    val INT_CEILING : thm
    val INT_CEILING_BOUNDS : thm
    val INT_CEILING_INT_FLOOR : thm
    val INT_FLOOR : thm
    val INT_FLOOR_BOUNDS : thm
    val INT_FLOOR_EQNS : thm
    val INT_FLOOR_compute : 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
  
  val intreal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [Omega] Parent theory of "intreal"
   
   [int_arith] Parent theory of "intreal"
   
   [real] Parent theory of "intreal"
   
   [INT_CEILING_def]  Definition
      
      ⊢ ∀x. clg x = LEAST_INT i. x ≤ real_of_int i
   
   [INT_FLOOR_def]  Definition
      
      ⊢ ∀x. flr x = LEAST_INT i. x < real_of_int (i + 1)
   
   [is_int_def]  Definition
      
      ⊢ ∀x. is_int x ⇔ (x = real_of_int (flr x))
   
   [real_of_int]  Definition
      
      ⊢ ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i
   
   [INT_CEILING]  Theorem
      
      ⊢ ∀r i. (clg r = i) ⇔ real_of_int (i − 1) < r ∧ r ≤ real_of_int i
   
   [INT_CEILING_BOUNDS]  Theorem
      
      ⊢ ∀r. real_of_int (clg r − 1) < r ∧ r ≤ real_of_int (clg r)
   
   [INT_CEILING_INT_FLOOR]  Theorem
      
      ⊢ ∀r.
            clg r =
            (let i = flr r in if real_of_int i = r then i else i + 1)
   
   [INT_FLOOR]  Theorem
      
      ⊢ ∀r i. (flr r = i) ⇔ real_of_int i ≤ r ∧ r < real_of_int (i + 1)
   
   [INT_FLOOR_BOUNDS]  Theorem
      
      ⊢ ∀r. real_of_int (flr r) ≤ r ∧ r < real_of_int (flr r + 1)
   
   [INT_FLOOR_EQNS]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (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))
   
   [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, Kananaskis-11