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. inv 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
|- inv 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) ==> (inv 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-3