Structure realaxTheory

signature realaxTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val hreal_of_real : 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_abs : thm
    val real_add : thm
    val real_bijections : thm
    val real_div : thm
    val real_ge : thm
    val real_gt : thm
    val real_inv : thm
    val real_lte : thm
    val real_max : thm
    val real_min : thm
    val real_mul : thm
    val real_neg : thm
    val real_of_hreal : thm
    val real_of_num : thm
    val real_pow : thm
    val real_sub : thm
  
  (*  Theorems  *)
    val REAL : thm
    val REAL_0 : thm
    val REAL_1 : thm
    val REAL_10 : thm
    val REAL_10' : thm
    val REAL_ABS_NEG : thm
    val REAL_ABS_NUM : thm
    val REAL_ADD : thm
    val REAL_ADD_AC : thm
    val REAL_ADD_ASSOC : thm
    val REAL_ADD_LDISTRIB : thm
    val REAL_ADD_LID : thm
    val REAL_ADD_LID' : thm
    val REAL_ADD_LINV : thm
    val REAL_ADD_LINV' : thm
    val REAL_ADD_RDISTRIB : thm
    val REAL_ADD_RID : thm
    val REAL_ADD_RINV : thm
    val REAL_ADD_SYM : thm
    val REAL_BIJ : thm
    val REAL_ENTIRE : thm
    val REAL_EQ_ADD_LCANCEL : thm
    val REAL_EQ_ADD_RCANCEL : thm
    val REAL_INJ : thm
    val REAL_INV_0 : thm
    val REAL_INV_0' : thm
    val REAL_ISO : thm
    val REAL_ISO_EQ : thm
    val REAL_LDISTRIB : thm
    val REAL_LE : thm
    val REAL_LET_ADD : thm
    val REAL_LET_TOTAL : thm
    val REAL_LET_TRANS : thm
    val REAL_LE_01 : thm
    val REAL_LE_ADD : thm
    val REAL_LE_ADDR : thm
    val REAL_LE_ANTISYM : thm
    val REAL_LE_LADD : thm
    val REAL_LE_LADD_IMP : thm
    val REAL_LE_LNEG : thm
    val REAL_LE_LT : thm
    val REAL_LE_MUL : thm
    val REAL_LE_NEG2 : thm
    val REAL_LE_NEGTOTAL : thm
    val REAL_LE_RADD : thm
    val REAL_LE_REFL : thm
    val REAL_LE_RNEG : thm
    val REAL_LE_SQUARE : thm
    val REAL_LE_TOTAL : thm
    val REAL_LE_TRANS : thm
    val REAL_LNEG_UNIQ : thm
    val REAL_LTE_ADD : thm
    val REAL_LTE_ANTISYM : thm
    val REAL_LTE_TOTAL : thm
    val REAL_LTE_TRANS : thm
    val REAL_LT_01 : thm
    val REAL_LT_ADD : thm
    val REAL_LT_ADDR : thm
    val REAL_LT_ANTISYM : thm
    val REAL_LT_GT : thm
    val REAL_LT_IADD : thm
    val REAL_LT_IMP_LE : thm
    val REAL_LT_LADD : thm
    val REAL_LT_LADD_IMP : thm
    val REAL_LT_LE : thm
    val REAL_LT_MUL : thm
    val REAL_LT_MUL' : thm
    val REAL_LT_NEGTOTAL : thm
    val REAL_LT_NZ : thm
    val REAL_LT_RADD : thm
    val REAL_LT_REFL : thm
    val REAL_LT_TOTAL : thm
    val REAL_LT_TRANS : thm
    val REAL_MUL : thm
    val REAL_MUL_AC : thm
    val REAL_MUL_ASSOC : thm
    val REAL_MUL_LID : thm
    val REAL_MUL_LID' : thm
    val REAL_MUL_LINV : thm
    val REAL_MUL_LINV' : thm
    val REAL_MUL_LNEG : thm
    val REAL_MUL_LZERO : thm
    val REAL_MUL_RID : thm
    val REAL_MUL_RNEG : thm
    val REAL_MUL_RZERO : thm
    val REAL_MUL_SYM : thm
    val REAL_NEG_0 : thm
    val REAL_NEG_ADD : thm
    val REAL_NEG_LMUL : thm
    val REAL_NEG_LT0 : thm
    val REAL_NEG_NEG : thm
    val REAL_NEG_RMUL : thm
    val REAL_NEG_SUB : thm
    val REAL_NOT_LE : thm
    val REAL_NOT_LT : thm
    val REAL_OF_NUM_ADD : thm
    val REAL_OF_NUM_EQ : thm
    val REAL_OF_NUM_LE : thm
    val REAL_OF_NUM_MUL : thm
    val REAL_OF_NUM_POW : thm
    val REAL_OF_NUM_SUB : thm
    val REAL_POLY_CLAUSES : thm
    val REAL_POLY_NEG_CLAUSES : thm
    val REAL_POS : thm
    val REAL_POS_LT : thm
    val REAL_POW_2 : thm
    val REAL_POW_NEG : thm
    val REAL_RDISTRIB : thm
    val REAL_RNEG_UNIQ : thm
    val REAL_SUB_0 : thm
    val REAL_SUB_LE : thm
    val REAL_SUB_LT : thm
    val REAL_SUP_ALLPOS : thm
    val REAL_SUP_ALLPOS' : thm
    val real_ABS_REP_CLASS : thm
    val real_QUOTIENT : thm
    val real_lt : 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)
   
   [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. treal_eq r r ∧ (c = treal_eq r)) rep
   
   [real_abs]  Definition
      
      ⊢ ∀x. abs x = if 0 ≤ x then x else -x
   
   [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. treal_eq r r ∧ (c = treal_eq r)) r ⇔
            (real_REP_CLASS (real_ABS_CLASS r) = r)
   
   [real_div]  Definition
      
      ⊢ ∀x y. x / y = x * y⁻¹
   
   [real_ge]  Definition
      
      ⊢ ∀x y. x ≥ y ⇔ y ≤ x
   
   [real_gt]  Definition
      
      ⊢ ∀x y. x > y ⇔ y < x
   
   [real_inv]  Definition
      
      ⊢ ∀T1. T1⁻¹ = real_ABS (treal_inv (real_REP T1))
   
   [real_lte]  Definition
      
      ⊢ ∀x y. x ≤ y ⇔ ¬(y < x)
   
   [real_max]  Definition
      
      ⊢ ∀x y. max x y = if x ≤ y then y else x
   
   [real_min]  Definition
      
      ⊢ ∀x y. min x y = if x ≤ y then x else y
   
   [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)
   
   [real_of_num]  Definition
      
      ⊢ (0 = real_0) ∧ ∀n. &SUC n = &n + real_1
   
   [real_pow]  Definition
      
      ⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n
   
   [real_sub]  Definition
      
      ⊢ ∀x y. x − y = x + -y
   
   [REAL]  Theorem
      
      ⊢ ∀n. &SUC n = &n + 1
   
   [REAL_0]  Theorem
      
      ⊢ real_0 = 0
   
   [REAL_1]  Theorem
      
      ⊢ real_1 = 1
   
   [REAL_10]  Theorem
      
      ⊢ real_1 ≠ real_0
   
   [REAL_10']  Theorem
      
      ⊢ 1 ≠ 0
   
   [REAL_ABS_NEG]  Theorem
      
      ⊢ ∀x. abs (-x) = abs x
   
   [REAL_ABS_NUM]  Theorem
      
      ⊢ ∀n. abs (&n) = &n
   
   [REAL_ADD]  Theorem
      
      ⊢ ∀m n. &m + &n = &(m + n)
   
   [REAL_ADD_AC]  Theorem
      
      ⊢ (m + n = n + m) ∧ (m + n + p = m + (n + p)) ∧
        (m + (n + p) = n + (m + p))
   
   [REAL_ADD_ASSOC]  Theorem
      
      ⊢ ∀x y z. x + (y + z) = x + y + z
   
   [REAL_ADD_LDISTRIB]  Theorem
      
      ⊢ ∀x y z. x * (y + z) = x * y + x * z
   
   [REAL_ADD_LID]  Theorem
      
      ⊢ ∀x. real_0 + x = x
   
   [REAL_ADD_LID']  Theorem
      
      ⊢ ∀x. 0 + x = x
   
   [REAL_ADD_LINV]  Theorem
      
      ⊢ ∀x. -x + x = real_0
   
   [REAL_ADD_LINV']  Theorem
      
      ⊢ ∀x. -x + x = 0
   
   [REAL_ADD_RDISTRIB]  Theorem
      
      ⊢ ∀x y z. (x + y) * z = x * z + y * z
   
   [REAL_ADD_RID]  Theorem
      
      ⊢ ∀x. x + 0 = x
   
   [REAL_ADD_RINV]  Theorem
      
      ⊢ ∀x. x + -x = 0
   
   [REAL_ADD_SYM]  Theorem
      
      ⊢ ∀x y. x + y = y + x
   
   [REAL_BIJ]  Theorem
      
      ⊢ (∀h. hreal_of_real (real_of_hreal h) = h) ∧
        ∀r. real_0 < r ⇔ (real_of_hreal (hreal_of_real r) = r)
   
   [REAL_ENTIRE]  Theorem
      
      ⊢ ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)
   
   [REAL_EQ_ADD_LCANCEL]  Theorem
      
      ⊢ ∀x y z. (x + y = x + z) ⇔ (y = z)
   
   [REAL_EQ_ADD_RCANCEL]  Theorem
      
      ⊢ ∀x y z. (x + z = y + z) ⇔ (x = y)
   
   [REAL_INJ]  Theorem
      
      ⊢ ∀m n. (&m = &n) ⇔ (m = n)
   
   [REAL_INV_0]  Theorem
      
      ⊢ real_0⁻¹ = real_0
   
   [REAL_INV_0']  Theorem
      
      ⊢ 0⁻¹ = 0
   
   [REAL_ISO]  Theorem
      
      ⊢ ∀h i. h hreal_lt i ⇒ real_of_hreal h < real_of_hreal i
   
   [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_LE]  Theorem
      
      ⊢ ∀m n. &m ≤ &n ⇔ m ≤ n
   
   [REAL_LET_ADD]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
   
   [REAL_LET_TOTAL]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y < x
   
   [REAL_LET_TRANS]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
   
   [REAL_LE_01]  Theorem
      
      ⊢ 0 ≤ 1
   
   [REAL_LE_ADD]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
   
   [REAL_LE_ADDR]  Theorem
      
      ⊢ ∀x y. x ≤ x + y ⇔ 0 ≤ y
   
   [REAL_LE_ANTISYM]  Theorem
      
      ⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ (x = y)
   
   [REAL_LE_LADD]  Theorem
      
      ⊢ ∀x y z. x + y ≤ x + z ⇔ y ≤ z
   
   [REAL_LE_LADD_IMP]  Theorem
      
      ⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
   
   [REAL_LE_LNEG]  Theorem
      
      ⊢ ∀x y. -x ≤ y ⇔ 0 ≤ x + y
   
   [REAL_LE_LT]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇔ x < y ∨ (x = y)
   
   [REAL_LE_MUL]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
   
   [REAL_LE_NEG2]  Theorem
      
      ⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
   
   [REAL_LE_NEGTOTAL]  Theorem
      
      ⊢ ∀x. 0 ≤ x ∨ 0 ≤ -x
   
   [REAL_LE_RADD]  Theorem
      
      ⊢ ∀x y z. x + z ≤ y + z ⇔ x ≤ y
   
   [REAL_LE_REFL]  Theorem
      
      ⊢ ∀x. x ≤ x
   
   [REAL_LE_RNEG]  Theorem
      
      ⊢ ∀x y. x ≤ -y ⇔ x + y ≤ 0
   
   [REAL_LE_SQUARE]  Theorem
      
      ⊢ ∀x. 0 ≤ x * x
   
   [REAL_LE_TOTAL]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y ≤ x
   
   [REAL_LE_TRANS]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
   
   [REAL_LNEG_UNIQ]  Theorem
      
      ⊢ ∀x y. (x + y = 0) ⇔ (x = -y)
   
   [REAL_LTE_ADD]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
   
   [REAL_LTE_ANTISYM]  Theorem
      
      ⊢ ∀x y. ¬(x ≤ y ∧ y < x)
   
   [REAL_LTE_TOTAL]  Theorem
      
      ⊢ ∀x y. x < y ∨ y ≤ x
   
   [REAL_LTE_TRANS]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
   
   [REAL_LT_01]  Theorem
      
      ⊢ 0 < 1
   
   [REAL_LT_ADD]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
   
   [REAL_LT_ADDR]  Theorem
      
      ⊢ ∀x y. x < x + y ⇔ 0 < y
   
   [REAL_LT_ANTISYM]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y < x)
   
   [REAL_LT_GT]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ¬(y < x)
   
   [REAL_LT_IADD]  Theorem
      
      ⊢ ∀x y z. y < z ⇒ x + y < x + z
   
   [REAL_LT_IMP_LE]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x ≤ y
   
   [REAL_LT_LADD]  Theorem
      
      ⊢ ∀x y z. x + y < x + z ⇔ y < z
   
   [REAL_LT_LADD_IMP]  Theorem
      
      ⊢ ∀x y z. y < z ⇒ x + y < x + z
   
   [REAL_LT_LE]  Theorem
      
      ⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
   
   [REAL_LT_MUL]  Theorem
      
      ⊢ ∀x y. real_0 < x ∧ real_0 < y ⇒ real_0 < x * y
   
   [REAL_LT_MUL']  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
   
   [REAL_LT_NEGTOTAL]  Theorem
      
      ⊢ ∀x. (x = 0) ∨ 0 < x ∨ 0 < -x
   
   [REAL_LT_NZ]  Theorem
      
      ⊢ ∀n. &n ≠ 0 ⇔ 0 < &n
   
   [REAL_LT_RADD]  Theorem
      
      ⊢ ∀x y z. x + z < y + z ⇔ 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]  Theorem
      
      ⊢ ∀m n. &m * &n = &(m * n)
   
   [REAL_MUL_AC]  Theorem
      
      ⊢ (m * n = n * m) ∧ (m * n * p = m * (n * p)) ∧
        (m * (n * p) = n * (m * p))
   
   [REAL_MUL_ASSOC]  Theorem
      
      ⊢ ∀x y z. x * (y * z) = x * y * z
   
   [REAL_MUL_LID]  Theorem
      
      ⊢ ∀x. real_1 * x = x
   
   [REAL_MUL_LID']  Theorem
      
      ⊢ ∀x. 1 * x = x
   
   [REAL_MUL_LINV]  Theorem
      
      ⊢ ∀x. x ≠ real_0 ⇒ (x⁻¹ * x = real_1)
   
   [REAL_MUL_LINV']  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ (x⁻¹ * x = 1)
   
   [REAL_MUL_LNEG]  Theorem
      
      ⊢ ∀x y. -x * y = -(x * y)
   
   [REAL_MUL_LZERO]  Theorem
      
      ⊢ ∀x. 0 * x = 0
   
   [REAL_MUL_RID]  Theorem
      
      ⊢ ∀x. x * 1 = x
   
   [REAL_MUL_RNEG]  Theorem
      
      ⊢ ∀x y. x * -y = -(x * y)
   
   [REAL_MUL_RZERO]  Theorem
      
      ⊢ ∀x. x * 0 = 0
   
   [REAL_MUL_SYM]  Theorem
      
      ⊢ ∀x y. x * y = y * x
   
   [REAL_NEG_0]  Theorem
      
      ⊢ -0 = 0
   
   [REAL_NEG_ADD]  Theorem
      
      ⊢ ∀x y. -(x + y) = -x + -y
   
   [REAL_NEG_LMUL]  Theorem
      
      ⊢ ∀x y. -(x * y) = -x * y
   
   [REAL_NEG_LT0]  Theorem
      
      ⊢ ∀x. -x < 0 ⇔ 0 < x
   
   [REAL_NEG_NEG]  Theorem
      
      ⊢ ∀x. --x = x
   
   [REAL_NEG_RMUL]  Theorem
      
      ⊢ ∀x y. -(x * y) = x * -y
   
   [REAL_NEG_SUB]  Theorem
      
      ⊢ ∀x y. -(x − y) = y − x
   
   [REAL_NOT_LE]  Theorem
      
      ⊢ ∀x y. ¬(x ≤ y) ⇔ y < x
   
   [REAL_NOT_LT]  Theorem
      
      ⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
   
   [REAL_OF_NUM_ADD]  Theorem
      
      ⊢ ∀m n. &m + &n = &(m + n)
   
   [REAL_OF_NUM_EQ]  Theorem
      
      ⊢ ∀m n. (&m = &n) ⇔ (m = n)
   
   [REAL_OF_NUM_LE]  Theorem
      
      ⊢ ∀m n. &m ≤ &n ⇔ m ≤ n
   
   [REAL_OF_NUM_MUL]  Theorem
      
      ⊢ ∀m n. &m * &n = &(m * n)
   
   [REAL_OF_NUM_POW]  Theorem
      
      ⊢ ∀x n. &x pow n = &(x ** n)
   
   [REAL_OF_NUM_SUB]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ (&(n − m) = &n − &m)
   
   [REAL_POLY_CLAUSES]  Theorem
      
      ⊢ (∀x y z. x + (y + z) = x + y + z) ∧ (∀x y. x + y = y + x) ∧
        (∀x. 0 + x = x) ∧ (∀x y z. x * (y * z) = x * y * z) ∧
        (∀x y. x * y = y * x) ∧ (∀x. 1 * x = x) ∧ (∀x. 0 * x = 0) ∧
        (∀x y z. x * (y + z) = x * y + x * z) ∧ (∀x. x pow 0 = 1) ∧
        ∀x n. x pow SUC n = x * x pow n
   
   [REAL_POLY_NEG_CLAUSES]  Theorem
      
      ⊢ (∀x. -x = -1 * x) ∧ ∀x y. x − y = x + -1 * y
   
   [REAL_POS]  Theorem
      
      ⊢ ∀n. 0 ≤ &n
   
   [REAL_POS_LT]  Theorem
      
      ⊢ ∀n. 0 < &SUC n
   
   [REAL_POW_2]  Theorem
      
      ⊢ ∀x. x pow 2 = x * x
   
   [REAL_POW_NEG]  Theorem
      
      ⊢ ∀x n. -x pow n = if EVEN n then x pow n else -(x pow n)
   
   [REAL_RDISTRIB]  Theorem
      
      ⊢ ∀x y z. (x + y) * z = x * z + y * z
   
   [REAL_RNEG_UNIQ]  Theorem
      
      ⊢ ∀x y. (x + y = 0) ⇔ (y = -x)
   
   [REAL_SUB_0]  Theorem
      
      ⊢ ∀x y. (x − y = 0) ⇔ (x = y)
   
   [REAL_SUB_LE]  Theorem
      
      ⊢ ∀x y. 0 ≤ x − y ⇔ y ≤ x
   
   [REAL_SUB_LT]  Theorem
      
      ⊢ ∀x y. 0 < x − y ⇔ y < 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
   
   [REAL_SUP_ALLPOS']  Theorem
      
      ⊢ ∀P. (∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
            ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
   
   [real_ABS_REP_CLASS]  Theorem
      
      ⊢ (∀a. real_ABS_CLASS (real_REP_CLASS a) = a) ∧
        ∀c. (∃r. treal_eq r r ∧ (c = treal_eq r)) ⇔
            (real_REP_CLASS (real_ABS_CLASS c) = c)
   
   [real_QUOTIENT]  Theorem
      
      ⊢ QUOTIENT treal_eq real_ABS real_REP
   
   [real_lt]  Theorem
      
      ⊢ ∀y x. x < y ⇔ ¬(y ≤ x)
   
   
*)
end

HOL 4, Trindemossen-1