Theory "realax"

Signature

Definitions

treal_0

|- treal_0 = (hreal_1,hreal_1)

treal_1

|- treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)

treal_neg

|- ∀x y. treal_neg (x,y) = (y,x)

treal_add

|- ∀x1 y1 x2 y2. (x1,y1) treal_add (x2,y2) = (x1 hreal_add x2,y1 hreal_add y2)

treal_mul

|- ∀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_lt

|- ∀x1 y1 x2 y2.
     treal_lt (x1,y1) (x2,y2) ⇔ x1 hreal_add y2 hreal_lt x2 hreal_add y1

treal_inv

|- ∀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_eq

|- ∀x1 y1 x2 y2.
     treal_eq (x1,y1) (x2,y2) ⇔ (x1 hreal_add y2 = x2 hreal_add y1)

treal_of_hreal

|- ∀x. treal_of_hreal x = (x hreal_add hreal_1,hreal_1)

hreal_of_treal

|- ∀x y. hreal_of_treal (x,y) = @d. x = y hreal_add d

real_TY_DEF

|- ∃rep. TYPE_DEFINITION (λc. ∃r. treal_eq r r ∧ (c = treal_eq r)) rep

real_bijections

|- (∀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_REP_def

|- ∀a. real_REP a = $@ (real_REP_CLASS a)

real_ABS_def

|- ∀r. real_ABS r = real_ABS_CLASS (treal_eq r)

real_0

|- real_0 = real_ABS treal_0

real_1

|- real_1 = real_ABS treal_1

real_neg

|- ∀T1. -T1 = real_ABS (treal_neg (real_REP T1))

real_inv

|- ∀T1. inv T1 = real_ABS (treal_inv (real_REP T1))

real_add

|- ∀T1 T2. T1 + T2 = real_ABS (real_REP T1 treal_add real_REP T2)

real_mul

|- ∀T1 T2. T1 * T2 = real_ABS (real_REP T1 treal_mul real_REP T2)

real_lt

|- ∀T1 T2. T1 < T2 ⇔ treal_lt (real_REP T1) (real_REP T2)

real_of_hreal

|- ∀T1. real_of_hreal T1 = real_ABS (treal_of_hreal T1)

hreal_of_real

|- ∀T1. hreal_of_real T1 = hreal_of_treal (real_REP T1)

Theorems

HREAL_RDISTRIB

|- ∀x y z. (x hreal_add y) hreal_mul z = x hreal_mul z hreal_add y hreal_mul z

HREAL_EQ_ADDR

|- ∀x y. x hreal_add y ≠ x

HREAL_EQ_ADDL

|- ∀x y. x ≠ x hreal_add y

HREAL_EQ_LADD

|- ∀x y z. (x hreal_add y = x hreal_add z) ⇔ (y = z)

HREAL_LT_REFL

|- ∀x. ¬(x hreal_lt x)

HREAL_LT_ADDL

|- ∀x y. x hreal_lt x hreal_add y

HREAL_LT_NE

|- ∀x y. x hreal_lt y ⇒ x ≠ y

HREAL_LT_ADDR

|- ∀x y. ¬(x hreal_add y hreal_lt x)

HREAL_LT_GT

|- ∀x y. x hreal_lt y ⇒ ¬(y hreal_lt x)

HREAL_LT_ADD2

|- ∀x1 x2 y1 y2.
     x1 hreal_lt y1 ∧ x2 hreal_lt y2 ⇒
     x1 hreal_add x2 hreal_lt y1 hreal_add y2

HREAL_LT_LADD

|- ∀x y z. x hreal_add y hreal_lt x hreal_add z ⇔ y hreal_lt z

TREAL_EQ_REFL

|- ∀x. treal_eq x x

TREAL_EQ_SYM

|- ∀x y. treal_eq x y ⇔ treal_eq y x

TREAL_EQ_TRANS

|- ∀x y z. treal_eq x y ∧ treal_eq y z ⇒ treal_eq x z

TREAL_EQ_EQUIV

|- ∀p q. treal_eq p q ⇔ (treal_eq p = treal_eq q)

TREAL_EQ_AP

|- ∀p q. (p = q) ⇒ treal_eq p q

TREAL_10

|- ¬treal_eq treal_1 treal_0

TREAL_ADD_SYM

|- ∀x y. x treal_add y = y treal_add x

TREAL_MUL_SYM

|- ∀x y. x treal_mul y = y treal_mul x

TREAL_ADD_ASSOC

|- ∀x y z. x treal_add (y treal_add z) = x treal_add y treal_add z

TREAL_MUL_ASSOC

|- ∀x y z. x treal_mul (y treal_mul z) = x treal_mul y treal_mul z

TREAL_LDISTRIB

|- ∀x y z. x treal_mul (y treal_add z) = x treal_mul y treal_add x treal_mul z

TREAL_ADD_LID

|- ∀x. treal_eq (treal_0 treal_add x) x

TREAL_MUL_LID

|- ∀x. treal_eq (treal_1 treal_mul x) x

TREAL_ADD_LINV

|- ∀x. treal_eq (treal_neg x treal_add x) treal_0

TREAL_INV_0

|- treal_eq (treal_inv treal_0) treal_0

TREAL_MUL_LINV

|- ∀x. ¬treal_eq x treal_0 ⇒ treal_eq (treal_inv x treal_mul x) treal_1

TREAL_LT_TOTAL

|- ∀x y. treal_eq x y ∨ treal_lt x y ∨ treal_lt y x

TREAL_LT_REFL

|- ∀x. ¬treal_lt x x

TREAL_LT_TRANS

|- ∀x y z. treal_lt x y ∧ treal_lt y z ⇒ treal_lt x z

TREAL_LT_ADD

|- ∀x y z. treal_lt y z ⇒ treal_lt (x treal_add y) (x treal_add z)

TREAL_LT_MUL

|- ∀x y.
     treal_lt treal_0 x ∧ treal_lt treal_0 y ⇒
     treal_lt treal_0 (x treal_mul y)

TREAL_BIJ

|- (∀h. hreal_of_treal (treal_of_hreal h) = h) ∧
   ∀r. treal_lt treal_0 r ⇔ treal_eq (treal_of_hreal (hreal_of_treal r)) r

TREAL_ISO

|- ∀h i. h hreal_lt i ⇒ treal_lt (treal_of_hreal h) (treal_of_hreal i)

TREAL_BIJ_WELLDEF

|- ∀h i. treal_eq h i ⇒ (hreal_of_treal h = hreal_of_treal i)

TREAL_NEG_WELLDEF

|- ∀x1 x2. treal_eq x1 x2 ⇒ treal_eq (treal_neg x1) (treal_neg x2)

TREAL_ADD_WELLDEFR

|- ∀x1 x2 y. treal_eq x1 x2 ⇒ treal_eq (x1 treal_add y) (x2 treal_add y)

TREAL_ADD_WELLDEF

|- ∀x1 x2 y1 y2.
     treal_eq x1 x2 ∧ treal_eq y1 y2 ⇒
     treal_eq (x1 treal_add y1) (x2 treal_add y2)

TREAL_MUL_WELLDEFR

|- ∀x1 x2 y. treal_eq x1 x2 ⇒ treal_eq (x1 treal_mul y) (x2 treal_mul y)

TREAL_MUL_WELLDEF

|- ∀x1 x2 y1 y2.
     treal_eq x1 x2 ∧ treal_eq y1 y2 ⇒
     treal_eq (x1 treal_mul y1) (x2 treal_mul y2)

TREAL_LT_WELLDEFR

|- ∀x1 x2 y. treal_eq x1 x2 ⇒ (treal_lt x1 y ⇔ treal_lt x2 y)

TREAL_LT_WELLDEFL

|- ∀x y1 y2. treal_eq y1 y2 ⇒ (treal_lt x y1 ⇔ treal_lt x y2)

TREAL_LT_WELLDEF

|- ∀x1 x2 y1 y2.
     treal_eq x1 x2 ∧ treal_eq y1 y2 ⇒ (treal_lt x1 y1 ⇔ treal_lt x2 y2)

TREAL_INV_WELLDEF

|- ∀x1 x2. treal_eq x1 x2 ⇒ treal_eq (treal_inv x1) (treal_inv x2)

real_ABS_REP_CLASS

|- (∀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

|- QUOTIENT treal_eq real_ABS real_REP

REAL_ISO_EQ

|- ∀h i. h hreal_lt i ⇔ real_of_hreal h < real_of_hreal i

REAL_POS

|- ∀X. real_0 < real_of_hreal X

SUP_ALLPOS_LEMMA1

|- ∀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

|- ∀P X. P (real_of_hreal X) ⇔ (λh. P (real_of_hreal h)) X

SUP_ALLPOS_LEMMA3

|- ∀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

|- ∀y. ¬(real_0 < y) ⇒ ∀x. y < real_of_hreal x

REAL_SUP_ALLPOS

|- ∀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_10

|- real_1 ≠ real_0

REAL_ADD_SYM

|- ∀x y. x + y = y + x

REAL_MUL_SYM

|- ∀x y. x * y = y * x

REAL_ADD_ASSOC

|- ∀x y z. x + (y + z) = x + y + z

REAL_MUL_ASSOC

|- ∀x y z. x * (y * z) = x * y * z

REAL_LDISTRIB

|- ∀x y z. x * (y + z) = x * y + x * z

REAL_ADD_LID

|- ∀x. real_0 + x = x

REAL_MUL_LID

|- ∀x. real_1 * x = x

REAL_ADD_LINV

|- ∀x. -x + x = real_0

REAL_MUL_LINV

|- ∀x. x ≠ real_0 ⇒ (inv x * x = real_1)

REAL_LT_TOTAL

|- ∀x y. (x = y) ∨ x < y ∨ y < x

REAL_LT_REFL

|- ∀x. ¬(x < x)

REAL_LT_TRANS

|- ∀x y z. x < y ∧ y < z ⇒ x < z

REAL_LT_IADD

|- ∀x y z. y < z ⇒ x + y < x + z

REAL_LT_MUL

|- ∀x y. real_0 < x ∧ real_0 < y ⇒ real_0 < x * y

REAL_INV_0

|- inv real_0 = real_0