Structure realaxTheory

signature realaxTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val hreal_of_real : thm
    val hreal_of_treal : thm
    val real_0 : thm
    val real_1 : thm
    val real_ABS_def : thm
    val real_REP_def : thm
    val real_TY_DEF : thm
    val real_add : thm
    val real_bijections : thm
    val real_inv : thm
    val real_lt : thm
    val real_mul : thm
    val real_neg : thm
    val real_of_hreal : thm
    val treal_0 : thm
    val treal_1 : thm
    val treal_add : thm
    val treal_eq : thm
    val treal_inv : thm
    val treal_lt : thm
    val treal_mul : thm
    val treal_neg : thm
    val treal_of_hreal : thm
  
  (*  Theorems  *)
    val HREAL_EQ_ADDL : thm
    val HREAL_EQ_ADDR : thm
    val HREAL_EQ_LADD : thm
    val HREAL_LT_ADD2 : thm
    val HREAL_LT_ADDL : thm
    val HREAL_LT_ADDR : thm
    val HREAL_LT_GT : thm
    val HREAL_LT_LADD : thm
    val HREAL_LT_NE : thm
    val HREAL_LT_REFL : thm
    val HREAL_RDISTRIB : thm
    val REAL_10 : thm
    val REAL_ADD_ASSOC : thm
    val REAL_ADD_LID : thm
    val REAL_ADD_LINV : thm
    val REAL_ADD_SYM : thm
    val REAL_INV_0 : thm
    val REAL_ISO_EQ : thm
    val REAL_LDISTRIB : thm
    val REAL_LT_IADD : thm
    val REAL_LT_MUL : thm
    val REAL_LT_REFL : thm
    val REAL_LT_TOTAL : thm
    val REAL_LT_TRANS : thm
    val REAL_MUL_ASSOC : thm
    val REAL_MUL_LID : thm
    val REAL_MUL_LINV : thm
    val REAL_MUL_SYM : thm
    val REAL_POS : thm
    val REAL_SUP_ALLPOS : thm
    val SUP_ALLPOS_LEMMA1 : thm
    val SUP_ALLPOS_LEMMA2 : thm
    val SUP_ALLPOS_LEMMA3 : thm
    val SUP_ALLPOS_LEMMA4 : thm
    val TREAL_10 : thm
    val TREAL_ADD_ASSOC : thm
    val TREAL_ADD_LID : thm
    val TREAL_ADD_LINV : thm
    val TREAL_ADD_SYM : thm
    val TREAL_ADD_WELLDEF : thm
    val TREAL_ADD_WELLDEFR : thm
    val TREAL_BIJ : thm
    val TREAL_BIJ_WELLDEF : thm
    val TREAL_EQ_AP : thm
    val TREAL_EQ_EQUIV : thm
    val TREAL_EQ_REFL : thm
    val TREAL_EQ_SYM : thm
    val TREAL_EQ_TRANS : thm
    val TREAL_INV_0 : thm
    val TREAL_INV_WELLDEF : thm
    val TREAL_ISO : thm
    val TREAL_LDISTRIB : thm
    val TREAL_LT_ADD : thm
    val TREAL_LT_MUL : thm
    val TREAL_LT_REFL : thm
    val TREAL_LT_TOTAL : thm
    val TREAL_LT_TRANS : thm
    val TREAL_LT_WELLDEF : thm
    val TREAL_LT_WELLDEFL : thm
    val TREAL_LT_WELLDEFR : thm
    val TREAL_MUL_ASSOC : thm
    val TREAL_MUL_LID : thm
    val TREAL_MUL_LINV : thm
    val TREAL_MUL_SYM : thm
    val TREAL_MUL_WELLDEF : thm
    val TREAL_MUL_WELLDEFR : thm
    val TREAL_NEG_WELLDEF : thm
    val real_ABS_REP_CLASS : thm
    val real_QUOTIENT : thm
  
  val realax_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [hreal] Parent theory of "realax"
   
   [hreal_of_real]  Definition
      
      ⊢ ∀T1. hreal_of_real T1 = hreal_of_treal (real_REP T1)
   
   [hreal_of_treal]  Definition
      
      ⊢ ∀x y. hreal_of_treal (x,y) = @d. x = y hreal_add d
   
   [real_0]  Definition
      
      ⊢ real_0 = real_ABS treal_0
   
   [real_1]  Definition
      
      ⊢ real_1 = real_ABS treal_1
   
   [real_ABS_def]  Definition
      
      ⊢ ∀r. real_ABS r = real_ABS_CLASS ($treal_eq r)
   
   [real_REP_def]  Definition
      
      ⊢ ∀a. real_REP a = $@ (real_REP_CLASS a)
   
   [real_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION (λc. ∃r. r treal_eq r ∧ (c = $treal_eq r)) rep
   
   [real_add]  Definition
      
      ⊢ ∀T1 T2. T1 + T2 = real_ABS (real_REP T1 treal_add real_REP T2)
   
   [real_bijections]  Definition
      
      ⊢ (∀a. real_ABS_CLASS (real_REP_CLASS a) = a) ∧
        ∀r. (λc. ∃r. r treal_eq r ∧ (c = $treal_eq r)) r ⇔
            (real_REP_CLASS (real_ABS_CLASS r) = r)
   
   [real_inv]  Definition
      
      ⊢ ∀T1. T1⁻¹ = real_ABS (treal_inv (real_REP T1))
   
   [real_lt]  Definition
      
      ⊢ ∀T1 T2. T1 < T2 ⇔ real_REP T1 treal_lt real_REP T2
   
   [real_mul]  Definition
      
      ⊢ ∀T1 T2. T1 * T2 = real_ABS (real_REP T1 treal_mul real_REP T2)
   
   [real_neg]  Definition
      
      ⊢ ∀T1. -T1 = real_ABS (treal_neg (real_REP T1))
   
   [real_of_hreal]  Definition
      
      ⊢ ∀T1. real_of_hreal T1 = real_ABS (treal_of_hreal T1)
   
   [treal_0]  Definition
      
      ⊢ treal_0 = (hreal_1,hreal_1)
   
   [treal_1]  Definition
      
      ⊢ treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)
   
   [treal_add]  Definition
      
      ⊢ ∀x1 y1 x2 y2.
          (x1,y1) treal_add (x2,y2) = (x1 hreal_add x2,y1 hreal_add y2)
   
   [treal_eq]  Definition
      
      ⊢ ∀x1 y1 x2 y2.
          (x1,y1) treal_eq (x2,y2) ⇔ (x1 hreal_add y2 = x2 hreal_add y1)
   
   [treal_inv]  Definition
      
      ⊢ ∀x y.
          treal_inv (x,y) =
          if x = y then treal_0
          else if y hreal_lt x then
            (hreal_inv (x hreal_sub y) hreal_add hreal_1,hreal_1)
          else (hreal_1,hreal_inv (y hreal_sub x) hreal_add hreal_1)
   
   [treal_lt]  Definition
      
      ⊢ ∀x1 y1 x2 y2.
          (x1,y1) treal_lt (x2,y2) ⇔
          x1 hreal_add y2 hreal_lt x2 hreal_add y1
   
   [treal_mul]  Definition
      
      ⊢ ∀x1 y1 x2 y2.
          (x1,y1) treal_mul (x2,y2) =
          (x1 hreal_mul x2 hreal_add y1 hreal_mul y2,
           x1 hreal_mul y2 hreal_add y1 hreal_mul x2)
   
   [treal_neg]  Definition
      
      ⊢ ∀x y. treal_neg (x,y) = (y,x)
   
   [treal_of_hreal]  Definition
      
      ⊢ ∀x. treal_of_hreal x = (x hreal_add hreal_1,hreal_1)
   
   [HREAL_EQ_ADDL]  Theorem
      
      ⊢ ∀x y. x ≠ x hreal_add y
   
   [HREAL_EQ_ADDR]  Theorem
      
      ⊢ ∀x y. x hreal_add y ≠ x
   
   [HREAL_EQ_LADD]  Theorem
      
      ⊢ ∀x y z. (x hreal_add y = x hreal_add z) ⇔ (y = z)
   
   [HREAL_LT_ADD2]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 hreal_lt y1 ∧ x2 hreal_lt y2 ⇒
          x1 hreal_add x2 hreal_lt y1 hreal_add y2
   
   [HREAL_LT_ADDL]  Theorem
      
      ⊢ ∀x y. x hreal_lt x hreal_add y
   
   [HREAL_LT_ADDR]  Theorem
      
      ⊢ ∀x y. ¬(x hreal_add y hreal_lt x)
   
   [HREAL_LT_GT]  Theorem
      
      ⊢ ∀x y. x hreal_lt y ⇒ ¬(y hreal_lt x)
   
   [HREAL_LT_LADD]  Theorem
      
      ⊢ ∀x y z. x hreal_add y hreal_lt x hreal_add z ⇔ y hreal_lt z
   
   [HREAL_LT_NE]  Theorem
      
      ⊢ ∀x y. x hreal_lt y ⇒ x ≠ y
   
   [HREAL_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x hreal_lt x)
   
   [HREAL_RDISTRIB]  Theorem
      
      ⊢ ∀x y z.
          (x hreal_add y) hreal_mul z =
          x hreal_mul z hreal_add y hreal_mul z
   
   [REAL_10]  Theorem
      
      ⊢ real_1 ≠ real_0
   
   [REAL_ADD_ASSOC]  Theorem
      
      ⊢ ∀x y z. x + (y + z) = x + y + z
   
   [REAL_ADD_LID]  Theorem
      
      ⊢ ∀x. real_0 + x = x
   
   [REAL_ADD_LINV]  Theorem
      
      ⊢ ∀x. -x + x = real_0
   
   [REAL_ADD_SYM]  Theorem
      
      ⊢ ∀x y. x + y = y + x
   
   [REAL_INV_0]  Theorem
      
      ⊢ real_0⁻¹ = real_0
   
   [REAL_ISO_EQ]  Theorem
      
      ⊢ ∀h i. h hreal_lt i ⇔ real_of_hreal h < real_of_hreal i
   
   [REAL_LDISTRIB]  Theorem
      
      ⊢ ∀x y z. x * (y + z) = x * y + x * z
   
   [REAL_LT_IADD]  Theorem
      
      ⊢ ∀x y z. y < z ⇒ x + y < x + z
   
   [REAL_LT_MUL]  Theorem
      
      ⊢ ∀x y. real_0 < x ∧ real_0 < y ⇒ real_0 < x * y
   
   [REAL_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x < x)
   
   [REAL_LT_TOTAL]  Theorem
      
      ⊢ ∀x y. (x = y) ∨ x < y ∨ y < x
   
   [REAL_LT_TRANS]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y < z ⇒ x < z
   
   [REAL_MUL_ASSOC]  Theorem
      
      ⊢ ∀x y z. x * (y * z) = x * y * z
   
   [REAL_MUL_LID]  Theorem
      
      ⊢ ∀x. real_1 * x = x
   
   [REAL_MUL_LINV]  Theorem
      
      ⊢ ∀x. x ≠ real_0 ⇒ (x⁻¹ * x = real_1)
   
   [REAL_MUL_SYM]  Theorem
      
      ⊢ ∀x y. x * y = y * x
   
   [REAL_POS]  Theorem
      
      ⊢ ∀X. real_0 < real_of_hreal X
   
   [REAL_SUP_ALLPOS]  Theorem
      
      ⊢ ∀P. (∀x. P x ⇒ real_0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
            ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
   
   [SUP_ALLPOS_LEMMA1]  Theorem
      
      ⊢ ∀P y.
          (∀x. P x ⇒ real_0 < x) ⇒
          ((∃x. P x ∧ y < x) ⇔
           ∃X. P (real_of_hreal X) ∧ y < real_of_hreal X)
   
   [SUP_ALLPOS_LEMMA2]  Theorem
      
      ⊢ ∀P X. P (real_of_hreal X) ⇔ (λh. P (real_of_hreal h)) X
   
   [SUP_ALLPOS_LEMMA3]  Theorem
      
      ⊢ ∀P. (∀x. P x ⇒ real_0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
            (∃X. (λh. P (real_of_hreal h)) X) ∧
            ∃Y. ∀X. (λh. P (real_of_hreal h)) X ⇒ X hreal_lt Y
   
   [SUP_ALLPOS_LEMMA4]  Theorem
      
      ⊢ ∀y. ¬(real_0 < y) ⇒ ∀x. y < real_of_hreal x
   
   [TREAL_10]  Theorem
      
      ⊢ ¬(treal_1 treal_eq treal_0)
   
   [TREAL_ADD_ASSOC]  Theorem
      
      ⊢ ∀x y z. x treal_add (y treal_add z) = x treal_add y treal_add z
   
   [TREAL_ADD_LID]  Theorem
      
      ⊢ ∀x. treal_0 treal_add x treal_eq x
   
   [TREAL_ADD_LINV]  Theorem
      
      ⊢ ∀x. treal_neg x treal_add x treal_eq treal_0
   
   [TREAL_ADD_SYM]  Theorem
      
      ⊢ ∀x y. x treal_add y = y treal_add x
   
   [TREAL_ADD_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒
          x1 treal_add y1 treal_eq x2 treal_add y2
   
   [TREAL_ADD_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ x1 treal_add y treal_eq x2 treal_add y
   
   [TREAL_BIJ]  Theorem
      
      ⊢ (∀h. hreal_of_treal (treal_of_hreal h) = h) ∧
        ∀r. treal_0 treal_lt r ⇔
            treal_of_hreal (hreal_of_treal r) treal_eq r
   
   [TREAL_BIJ_WELLDEF]  Theorem
      
      ⊢ ∀h i. h treal_eq i ⇒ (hreal_of_treal h = hreal_of_treal i)
   
   [TREAL_EQ_AP]  Theorem
      
      ⊢ ∀p q. (p = q) ⇒ p treal_eq q
   
   [TREAL_EQ_EQUIV]  Theorem
      
      ⊢ ∀p q. p treal_eq q ⇔ ($treal_eq p = $treal_eq q)
   
   [TREAL_EQ_REFL]  Theorem
      
      ⊢ ∀x. x treal_eq x
   
   [TREAL_EQ_SYM]  Theorem
      
      ⊢ ∀x y. x treal_eq y ⇔ y treal_eq x
   
   [TREAL_EQ_TRANS]  Theorem
      
      ⊢ ∀x y z. x treal_eq y ∧ y treal_eq z ⇒ x treal_eq z
   
   [TREAL_INV_0]  Theorem
      
      ⊢ treal_inv treal_0 treal_eq treal_0
   
   [TREAL_INV_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2. x1 treal_eq x2 ⇒ treal_inv x1 treal_eq treal_inv x2
   
   [TREAL_ISO]  Theorem
      
      ⊢ ∀h i. h hreal_lt i ⇒ treal_of_hreal h treal_lt treal_of_hreal i
   
   [TREAL_LDISTRIB]  Theorem
      
      ⊢ ∀x y z.
          x treal_mul (y treal_add z) =
          x treal_mul y treal_add x treal_mul z
   
   [TREAL_LT_ADD]  Theorem
      
      ⊢ ∀x y z. y treal_lt z ⇒ x treal_add y treal_lt x treal_add z
   
   [TREAL_LT_MUL]  Theorem
      
      ⊢ ∀x y.
          treal_0 treal_lt x ∧ treal_0 treal_lt y ⇒
          treal_0 treal_lt x treal_mul y
   
   [TREAL_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x treal_lt x)
   
   [TREAL_LT_TOTAL]  Theorem
      
      ⊢ ∀x y. x treal_eq y ∨ x treal_lt y ∨ y treal_lt x
   
   [TREAL_LT_TRANS]  Theorem
      
      ⊢ ∀x y z. x treal_lt y ∧ y treal_lt z ⇒ x treal_lt z
   
   [TREAL_LT_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒
          (x1 treal_lt y1 ⇔ x2 treal_lt y2)
   
   [TREAL_LT_WELLDEFL]  Theorem
      
      ⊢ ∀x y1 y2. y1 treal_eq y2 ⇒ (x treal_lt y1 ⇔ x treal_lt y2)
   
   [TREAL_LT_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ (x1 treal_lt y ⇔ x2 treal_lt y)
   
   [TREAL_MUL_ASSOC]  Theorem
      
      ⊢ ∀x y z. x treal_mul (y treal_mul z) = x treal_mul y treal_mul z
   
   [TREAL_MUL_LID]  Theorem
      
      ⊢ ∀x. treal_1 treal_mul x treal_eq x
   
   [TREAL_MUL_LINV]  Theorem
      
      ⊢ ∀x. ¬(x treal_eq treal_0) ⇒
            treal_inv x treal_mul x treal_eq treal_1
   
   [TREAL_MUL_SYM]  Theorem
      
      ⊢ ∀x y. x treal_mul y = y treal_mul x
   
   [TREAL_MUL_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒
          x1 treal_mul y1 treal_eq x2 treal_mul y2
   
   [TREAL_MUL_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ x1 treal_mul y treal_eq x2 treal_mul y
   
   [TREAL_NEG_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2. x1 treal_eq x2 ⇒ treal_neg x1 treal_eq treal_neg x2
   
   [real_ABS_REP_CLASS]  Theorem
      
      ⊢ (∀a. real_ABS_CLASS (real_REP_CLASS a) = a) ∧
        ∀c. (∃r. r treal_eq r ∧ (c = $treal_eq r)) ⇔
            (real_REP_CLASS (real_ABS_CLASS c) = c)
   
   [real_QUOTIENT]  Theorem
      
      ⊢ QUOTIENT $treal_eq real_ABS real_REP
   
   
*)
end

HOL 4, Kananaskis-14