Theory "realax"

Signature

Definitions

treal_of_hreal

⊢ ∀x. treal_of_hreal x = (x hreal_add hreal_1,hreal_1)

treal_neg

⊢ ∀x y. treal_neg (x,y) = (y,x)

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_add

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

treal_1

⊢ treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)

treal_0

⊢ treal_0 = (hreal_1,hreal_1)

real_TY_DEF

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

real_REP_def

⊢ ∀a. real_REP a = $@ (real_REP_CLASS a)

real_of_hreal

⊢ ∀T1. real_of_hreal T1 = real_ABS (treal_of_hreal T1)

real_neg

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

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_inv

⊢ ∀T1. T1⁻¹ = real_ABS (treal_inv (real_REP T1))

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_add

⊢ ∀T1 T2. T1 + T2 = real_ABS (real_REP T1 treal_add real_REP T2)

real_ABS_def

⊢ ∀r. real_ABS r = real_ABS_CLASS (treal_eq r)

real_1

⊢ real_1 = real_ABS treal_1

real_0

⊢ real_0 = real_ABS treal_0

hreal_of_treal

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

hreal_of_real

⊢ ∀T1. hreal_of_real T1 = hreal_of_treal (real_REP T1)

Theorems

TREAL_NEG_WELLDEF

⊢ ∀x1 x2. treal_eq x1 x2 ⇒ treal_eq (treal_neg x1) (treal_neg x2)

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_MUL_SYM

⊢ ∀x y. x treal_mul y = y treal_mul x

TREAL_MUL_LINV

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

TREAL_MUL_LID

⊢ ∀x. treal_eq (treal_1 treal_mul x) x

TREAL_MUL_ASSOC

⊢ ∀x y z. x treal_mul (y treal_mul z) = x treal_mul y treal_mul z

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_LT_TRANS

⊢ ∀x y z. treal_lt x y ∧ treal_lt y z ⇒ treal_lt x z

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_MUL

⊢ ∀x y.
      treal_lt treal_0 x ∧ treal_lt treal_0 y ⇒
      treal_lt treal_0 (x treal_mul y)

TREAL_LT_ADD

⊢ ∀x y z. treal_lt y z ⇒ treal_lt (x treal_add y) (x treal_add z)

TREAL_LDISTRIB

⊢ ∀x y z. x treal_mul (y treal_add z) = x treal_mul y treal_add x treal_mul z

TREAL_ISO

⊢ ∀h i. h hreal_lt i ⇒ treal_lt (treal_of_hreal h) (treal_of_hreal i)

TREAL_INV_WELLDEF

⊢ ∀x1 x2. treal_eq x1 x2 ⇒ treal_eq (treal_inv x1) (treal_inv x2)

TREAL_INV_0

⊢ treal_eq (treal_inv treal_0) treal_0

TREAL_EQ_TRANS

⊢ ∀x y z. treal_eq x y ∧ treal_eq y z ⇒ treal_eq x z

TREAL_EQ_SYM

⊢ ∀x y. treal_eq x y ⇔ treal_eq y x

TREAL_EQ_REFL

⊢ ∀x. treal_eq x x

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_BIJ_WELLDEF

⊢ ∀h i. treal_eq h i ⇒ (hreal_of_treal h = hreal_of_treal i)

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_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_ADD_SYM

⊢ ∀x y. x treal_add y = y treal_add x

TREAL_ADD_LINV

⊢ ∀x. treal_eq (treal_neg x treal_add x) treal_0

TREAL_ADD_LID

⊢ ∀x. treal_eq (treal_0 treal_add x) x

TREAL_ADD_ASSOC

⊢ ∀x y z. x treal_add (y treal_add z) = x treal_add y treal_add z

TREAL_10

⊢ ¬treal_eq treal_1 treal_0

SUP_ALLPOS_LEMMA4

⊢ ∀y. ¬(real_0 < y) ⇒ ∀x. y < real_of_hreal 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_LEMMA2

⊢ ∀P X. P (real_of_hreal X) ⇔ (λh. P (real_of_hreal h)) 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)

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_QUOTIENT

⊢ QUOTIENT treal_eq real_ABS real_REP

REAL_POS

⊢ ∀X. real_0 < real_of_hreal X

REAL_MUL_SYM

⊢ ∀x y. x * y = y * x

REAL_MUL_LINV

⊢ ∀x. x ≠ real_0 ⇒ (x⁻¹ * x = real_1)

REAL_MUL_LID

⊢ ∀x. real_1 * x = x

REAL_MUL_ASSOC

⊢ ∀x y z. x * (y * z) = x * y * z

REAL_LT_TRANS

⊢ ∀x y z. x < y ∧ y < z ⇒ x < z

REAL_LT_TOTAL

⊢ ∀x y. (x = y) ∨ x < y ∨ y < x

REAL_LT_REFL

⊢ ∀x. ¬(x < x)

REAL_LT_MUL

⊢ ∀x y. real_0 < x ∧ real_0 < y ⇒ real_0 < x * y

REAL_LT_IADD

⊢ ∀x y z. y < z ⇒ x + y < x + z

REAL_LDISTRIB

⊢ ∀x y z. x * (y + z) = x * y + x * z

REAL_ISO_EQ

⊢ ∀h i. h hreal_lt i ⇔ real_of_hreal h < real_of_hreal i

REAL_INV_0

⊢ real_0⁻¹ = real_0

REAL_ADD_SYM

⊢ ∀x y. x + y = y + x

REAL_ADD_LINV

⊢ ∀x. -x + x = real_0

REAL_ADD_LID

⊢ ∀x. real_0 + x = x

REAL_ADD_ASSOC

⊢ ∀x y z. x + (y + z) = x + y + z

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_10

⊢ real_1 ≠ real_0

HREAL_RDISTRIB

⊢ ∀x y z. (x hreal_add y) hreal_mul z = x hreal_mul z hreal_add y hreal_mul z

HREAL_LT_REFL

⊢ ∀x. ¬(x hreal_lt x)

HREAL_LT_NE

⊢ ∀x y. x hreal_lt y ⇒ x ≠ y

HREAL_LT_LADD

⊢ ∀x y z. x hreal_add y hreal_lt x hreal_add z ⇔ y hreal_lt z

HREAL_LT_GT

⊢ ∀x y. x hreal_lt y ⇒ ¬(y hreal_lt x)

HREAL_LT_ADDR

⊢ ∀x y. ¬(x hreal_add y hreal_lt x)

HREAL_LT_ADDL

⊢ ∀x y. x hreal_lt x hreal_add y

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_EQ_LADD

⊢ ∀x y z. (x hreal_add y = x hreal_add z) ⇔ (y = z)

HREAL_EQ_ADDR

⊢ ∀x y. x hreal_add y ≠ x

HREAL_EQ_ADDL

⊢ ∀x y. x ≠ x hreal_add y