Structure hrealTheory

signature hrealTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val cut_of_hrat : thm
    val hrat_lt : thm
    val hreal_1 : thm
    val hreal_TY_DEF : thm
    val hreal_add : thm
    val hreal_inv : thm
    val hreal_lt : thm
    val hreal_mul : thm
    val hreal_of_treal : thm
    val hreal_sub : thm
    val hreal_sup : thm
    val hreal_tybij : thm
    val isacut : 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 CUT_BOUNDED : thm
    val CUT_DOWN : thm
    val CUT_ISACUT : thm
    val CUT_NEARTOP_ADD : thm
    val CUT_NEARTOP_MUL : thm
    val CUT_NONEMPTY : thm
    val CUT_STRADDLE : thm
    val CUT_UBOUND : thm
    val CUT_UP : thm
    val EQUAL_CUTS : thm
    val HRAT_DOWN : thm
    val HRAT_DOWN2 : thm
    val HRAT_EQ_LADD : thm
    val HRAT_EQ_LMUL : thm
    val HRAT_GT_L1 : thm
    val HRAT_GT_LMUL1 : thm
    val HRAT_INV_MUL : thm
    val HRAT_LT_ADD2 : thm
    val HRAT_LT_ADDL : thm
    val HRAT_LT_ADDR : thm
    val HRAT_LT_ANTISYM : thm
    val HRAT_LT_GT : thm
    val HRAT_LT_L1 : thm
    val HRAT_LT_LADD : thm
    val HRAT_LT_LMUL : thm
    val HRAT_LT_LMUL1 : thm
    val HRAT_LT_MUL2 : thm
    val HRAT_LT_NE : thm
    val HRAT_LT_R1 : thm
    val HRAT_LT_RADD : thm
    val HRAT_LT_REFL : thm
    val HRAT_LT_RMUL : thm
    val HRAT_LT_RMUL1 : thm
    val HRAT_LT_TOTAL : thm
    val HRAT_LT_TRANS : thm
    val HRAT_MEAN : thm
    val HRAT_MUL_RID : thm
    val HRAT_MUL_RINV : thm
    val HRAT_RDISTRIB : thm
    val HRAT_UP : thm
    val HREAL_ADD_ASSOC : thm
    val HREAL_ADD_ISACUT : thm
    val HREAL_ADD_SYM : thm
    val HREAL_ADD_TOTAL : thm
    val HREAL_EQ_ADDL : thm
    val HREAL_EQ_ADDR : thm
    val HREAL_EQ_LADD : thm
    val HREAL_INV_ISACUT : thm
    val HREAL_LDISTRIB : thm
    val HREAL_LT : 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_LEMMA : thm
    val HREAL_LT_NE : thm
    val HREAL_LT_REFL : thm
    val HREAL_LT_TOTAL : thm
    val HREAL_MUL_ASSOC : thm
    val HREAL_MUL_ISACUT : thm
    val HREAL_MUL_LID : thm
    val HREAL_MUL_LINV : thm
    val HREAL_MUL_SYM : thm
    val HREAL_NOZERO : thm
    val HREAL_RDISTRIB : thm
    val HREAL_SUB_ADD : thm
    val HREAL_SUB_ISACUT : thm
    val HREAL_SUP : thm
    val HREAL_SUP_ISACUT : thm
    val ISACUT_HRAT : 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 hreal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [hrat] Parent theory of "hreal"
   
   [cut_of_hrat]  Definition
      
      ⊢ ∀x. cut_of_hrat x = (λy. y hrat_lt x)
   
   [hrat_lt]  Definition
      
      ⊢ ∀x y. x hrat_lt y ⇔ ∃d. y = x hrat_add d
   
   [hreal_1]  Definition
      
      ⊢ hreal_1 = hreal (cut_of_hrat hrat_1)
   
   [hreal_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION isacut rep
   
   [hreal_add]  Definition
      
      ⊢ ∀X Y.
          X hreal_add Y =
          hreal (λw. ∃x y. (w = x hrat_add y) ∧ cut X x ∧ cut Y y)
   
   [hreal_inv]  Definition
      
      ⊢ ∀X. hreal_inv X =
            hreal
              (λw.
                   ∃d. d hrat_lt hrat_1 ∧
                       ∀x. cut X x ⇒ w hrat_mul x hrat_lt d)
   
   [hreal_lt]  Definition
      
      ⊢ ∀X Y. X hreal_lt Y ⇔ X ≠ Y ∧ ∀x. cut X x ⇒ cut Y x
   
   [hreal_mul]  Definition
      
      ⊢ ∀X Y.
          X hreal_mul Y =
          hreal (λw. ∃x y. (w = x hrat_mul y) ∧ cut X x ∧ cut Y y)
   
   [hreal_of_treal]  Definition
      
      ⊢ ∀x y. hreal_of_treal (x,y) = @d. x = y hreal_add d
   
   [hreal_sub]  Definition
      
      ⊢ ∀Y X.
          Y hreal_sub X = hreal (λw. ∃x. ¬cut X x ∧ cut Y (x hrat_add w))
   
   [hreal_sup]  Definition
      
      ⊢ ∀P. hreal_sup P = hreal (λw. ∃X. P X ∧ cut X w)
   
   [hreal_tybij]  Definition
      
      ⊢ (∀a. hreal (cut a) = a) ∧ ∀r. isacut r ⇔ (cut (hreal r) = r)
   
   [isacut]  Definition
      
      ⊢ ∀C. isacut C ⇔
            (∃x. C x) ∧ (∃x. ¬C x) ∧ (∀x y. C x ∧ y hrat_lt x ⇒ C y) ∧
            ∀x. C x ⇒ ∃y. C y ∧ x hrat_lt y
   
   [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)
   
   [CUT_BOUNDED]  Theorem
      
      ⊢ ∀X. ∃x. ¬cut X x
   
   [CUT_DOWN]  Theorem
      
      ⊢ ∀X x y. cut X x ∧ y hrat_lt x ⇒ cut X y
   
   [CUT_ISACUT]  Theorem
      
      ⊢ ∀X. isacut (cut X)
   
   [CUT_NEARTOP_ADD]  Theorem
      
      ⊢ ∀X e. ∃x. cut X x ∧ ¬cut X (x hrat_add e)
   
   [CUT_NEARTOP_MUL]  Theorem
      
      ⊢ ∀X u. hrat_1 hrat_lt u ⇒ ∃x. cut X x ∧ ¬cut X (u hrat_mul x)
   
   [CUT_NONEMPTY]  Theorem
      
      ⊢ ∀X. ∃x. cut X x
   
   [CUT_STRADDLE]  Theorem
      
      ⊢ ∀X x y. cut X x ∧ ¬cut X y ⇒ x hrat_lt y
   
   [CUT_UBOUND]  Theorem
      
      ⊢ ∀X x y. ¬cut X x ∧ x hrat_lt y ⇒ ¬cut X y
   
   [CUT_UP]  Theorem
      
      ⊢ ∀X x. cut X x ⇒ ∃y. cut X y ∧ x hrat_lt y
   
   [EQUAL_CUTS]  Theorem
      
      ⊢ ∀X Y. (cut X = cut Y) ⇒ (X = Y)
   
   [HRAT_DOWN]  Theorem
      
      ⊢ ∀x. ∃y. y hrat_lt x
   
   [HRAT_DOWN2]  Theorem
      
      ⊢ ∀x y. ∃z. z hrat_lt x ∧ z hrat_lt y
   
   [HRAT_EQ_LADD]  Theorem
      
      ⊢ ∀x y z. (x hrat_add y = x hrat_add z) ⇔ (y = z)
   
   [HRAT_EQ_LMUL]  Theorem
      
      ⊢ ∀x y z. (x hrat_mul y = x hrat_mul z) ⇔ (y = z)
   
   [HRAT_GT_L1]  Theorem
      
      ⊢ ∀x y. hrat_1 hrat_lt hrat_inv x hrat_mul y ⇔ x hrat_lt y
   
   [HRAT_GT_LMUL1]  Theorem
      
      ⊢ ∀x y. y hrat_lt x hrat_mul y ⇔ hrat_1 hrat_lt x
   
   [HRAT_INV_MUL]  Theorem
      
      ⊢ ∀x y. hrat_inv (x hrat_mul y) = hrat_inv x hrat_mul hrat_inv y
   
   [HRAT_LT_ADD2]  Theorem
      
      ⊢ ∀u v x y.
          u hrat_lt x ∧ v hrat_lt y ⇒ u hrat_add v hrat_lt x hrat_add y
   
   [HRAT_LT_ADDL]  Theorem
      
      ⊢ ∀x y. x hrat_lt x hrat_add y
   
   [HRAT_LT_ADDR]  Theorem
      
      ⊢ ∀x y. y hrat_lt x hrat_add y
   
   [HRAT_LT_ANTISYM]  Theorem
      
      ⊢ ∀x y. ¬(x hrat_lt y ∧ y hrat_lt x)
   
   [HRAT_LT_GT]  Theorem
      
      ⊢ ∀x y. x hrat_lt y ⇒ ¬(y hrat_lt x)
   
   [HRAT_LT_L1]  Theorem
      
      ⊢ ∀x y. hrat_inv x hrat_mul y hrat_lt hrat_1 ⇔ y hrat_lt x
   
   [HRAT_LT_LADD]  Theorem
      
      ⊢ ∀x y z. z hrat_add x hrat_lt z hrat_add y ⇔ x hrat_lt y
   
   [HRAT_LT_LMUL]  Theorem
      
      ⊢ ∀x y z. z hrat_mul x hrat_lt z hrat_mul y ⇔ x hrat_lt y
   
   [HRAT_LT_LMUL1]  Theorem
      
      ⊢ ∀x y. x hrat_mul y hrat_lt y ⇔ x hrat_lt hrat_1
   
   [HRAT_LT_MUL2]  Theorem
      
      ⊢ ∀u v x y.
          u hrat_lt x ∧ v hrat_lt y ⇒ u hrat_mul v hrat_lt x hrat_mul y
   
   [HRAT_LT_NE]  Theorem
      
      ⊢ ∀x y. x hrat_lt y ⇒ x ≠ y
   
   [HRAT_LT_R1]  Theorem
      
      ⊢ ∀x y. x hrat_mul hrat_inv y hrat_lt hrat_1 ⇔ x hrat_lt y
   
   [HRAT_LT_RADD]  Theorem
      
      ⊢ ∀x y z. x hrat_add z hrat_lt y hrat_add z ⇔ x hrat_lt y
   
   [HRAT_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x hrat_lt x)
   
   [HRAT_LT_RMUL]  Theorem
      
      ⊢ ∀x y z. x hrat_mul z hrat_lt y hrat_mul z ⇔ x hrat_lt y
   
   [HRAT_LT_RMUL1]  Theorem
      
      ⊢ ∀x y. x hrat_mul y hrat_lt x ⇔ y hrat_lt hrat_1
   
   [HRAT_LT_TOTAL]  Theorem
      
      ⊢ ∀x y. (x = y) ∨ x hrat_lt y ∨ y hrat_lt x
   
   [HRAT_LT_TRANS]  Theorem
      
      ⊢ ∀x y z. x hrat_lt y ∧ y hrat_lt z ⇒ x hrat_lt z
   
   [HRAT_MEAN]  Theorem
      
      ⊢ ∀x y. x hrat_lt y ⇒ ∃z. x hrat_lt z ∧ z hrat_lt y
   
   [HRAT_MUL_RID]  Theorem
      
      ⊢ ∀x. x hrat_mul hrat_1 = x
   
   [HRAT_MUL_RINV]  Theorem
      
      ⊢ ∀x. x hrat_mul hrat_inv x = hrat_1
   
   [HRAT_RDISTRIB]  Theorem
      
      ⊢ ∀x y z.
          (x hrat_add y) hrat_mul z = x hrat_mul z hrat_add y hrat_mul z
   
   [HRAT_UP]  Theorem
      
      ⊢ ∀x. ∃y. x hrat_lt y
   
   [HREAL_ADD_ASSOC]  Theorem
      
      ⊢ ∀X Y Z. X hreal_add (Y hreal_add Z) = X hreal_add Y hreal_add Z
   
   [HREAL_ADD_ISACUT]  Theorem
      
      ⊢ ∀X Y. isacut (λw. ∃x y. (w = x hrat_add y) ∧ cut X x ∧ cut Y y)
   
   [HREAL_ADD_SYM]  Theorem
      
      ⊢ ∀X Y. X hreal_add Y = Y hreal_add X
   
   [HREAL_ADD_TOTAL]  Theorem
      
      ⊢ ∀X Y. (X = Y) ∨ (∃D. Y = X hreal_add D) ∨ ∃D. X = Y hreal_add D
   
   [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_INV_ISACUT]  Theorem
      
      ⊢ ∀X. isacut
              (λw.
                   ∃d. d hrat_lt hrat_1 ∧
                       ∀x. cut X x ⇒ w hrat_mul x hrat_lt d)
   
   [HREAL_LDISTRIB]  Theorem
      
      ⊢ ∀X Y Z.
          X hreal_mul (Y hreal_add Z) =
          X hreal_mul Y hreal_add X hreal_mul Z
   
   [HREAL_LT]  Theorem
      
      ⊢ ∀X Y. X hreal_lt Y ⇔ ∃D. Y = X hreal_add D
   
   [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_LEMMA]  Theorem
      
      ⊢ ∀X Y. X hreal_lt Y ⇒ ∃x. ¬cut X x ∧ cut Y x
   
   [HREAL_LT_NE]  Theorem
      
      ⊢ ∀x y. x hreal_lt y ⇒ x ≠ y
   
   [HREAL_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x hreal_lt x)
   
   [HREAL_LT_TOTAL]  Theorem
      
      ⊢ ∀X Y. (X = Y) ∨ X hreal_lt Y ∨ Y hreal_lt X
   
   [HREAL_MUL_ASSOC]  Theorem
      
      ⊢ ∀X Y Z. X hreal_mul (Y hreal_mul Z) = X hreal_mul Y hreal_mul Z
   
   [HREAL_MUL_ISACUT]  Theorem
      
      ⊢ ∀X Y. isacut (λw. ∃x y. (w = x hrat_mul y) ∧ cut X x ∧ cut Y y)
   
   [HREAL_MUL_LID]  Theorem
      
      ⊢ ∀X. hreal_1 hreal_mul X = X
   
   [HREAL_MUL_LINV]  Theorem
      
      ⊢ ∀X. hreal_inv X hreal_mul X = hreal_1
   
   [HREAL_MUL_SYM]  Theorem
      
      ⊢ ∀X Y. X hreal_mul Y = Y hreal_mul X
   
   [HREAL_NOZERO]  Theorem
      
      ⊢ ∀X Y. X hreal_add Y ≠ X
   
   [HREAL_RDISTRIB]  Theorem
      
      ⊢ ∀x y z.
          (x hreal_add y) hreal_mul z =
          x hreal_mul z hreal_add y hreal_mul z
   
   [HREAL_SUB_ADD]  Theorem
      
      ⊢ ∀X Y. X hreal_lt Y ⇒ (Y hreal_sub X hreal_add X = Y)
   
   [HREAL_SUB_ISACUT]  Theorem
      
      ⊢ ∀X Y.
          X hreal_lt Y ⇒ isacut (λw. ∃x. ¬cut X x ∧ cut Y (x hrat_add w))
   
   [HREAL_SUP]  Theorem
      
      ⊢ ∀P. (∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒
            ∀Y. (∃X. P X ∧ Y hreal_lt X) ⇔ Y hreal_lt hreal_sup P
   
   [HREAL_SUP_ISACUT]  Theorem
      
      ⊢ ∀P. (∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒
            isacut (λw. ∃X. P X ∧ cut X w)
   
   [ISACUT_HRAT]  Theorem
      
      ⊢ ∀h. isacut (cut_of_hrat h)
   
   [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
   
   
*)
end

HOL 4, Trindemossen-1