Theory: realax

Parents

• hreal

Types

• real(Arity = 0)

Constants

• real_neg  :real -> real
• treal_mul  :hreal # hreal -> hreal # hreal -> hreal # hreal
• mk_real  :(hreal # hreal -> bool) -> real
• real_mul  :real -> real -> real
• inv  :real -> real
• dest_real  :real -> hreal # hreal -> bool
• treal_0  :hreal # hreal
• treal_1  :hreal # hreal
• real_of_hreal  :hreal -> real
• real_lt  :real -> real -> bool
• hreal_of_treal  :hreal # hreal -> hreal
• hreal_of_real  :real -> hreal
• treal_of_hreal  :hreal -> hreal # hreal
• real_0  :real
• real_1  :real
• treal_add  :hreal # hreal -> hreal # hreal -> hreal # hreal
• real_add  :real -> real -> real
• treal_eq  :hreal # hreal -> hreal # hreal -> bool
• treal_inv  :hreal # hreal -> hreal # hreal
• treal_lt  :hreal # hreal -> hreal # hreal -> bool
• treal_neg  :hreal # hreal -> hreal # hreal

Definitions

hreal_of_real

|- !T1. hreal_of_real T1 = hreal_of_treal ($@ (dest_real T1))

hreal_of_treal

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

real_0

|- real_0 = mk_real ($treal_eq treal_0)

real_1

|- real_1 = mk_real ($treal_eq treal_1)

real_add

|- !T1 T2.
     T1 + T2 =
     mk_real ($treal_eq ($@ (dest_real T1) treal_add $@ (dest_real T2)))

real_inv

|- !T1. inv T1 = mk_real ($treal_eq (treal_inv ($@ (dest_real T1))))

real_lt

|- !T1 T2. T1 < T2 = $@ (dest_real T1) treal_lt $@ (dest_real T2)

real_mul

|- !T1 T2.
     T1 * T2 =
     mk_real ($treal_eq ($@ (dest_real T1) treal_mul $@ (dest_real T2)))

real_neg

|- !T1. ~T1 = mk_real ($treal_eq (treal_neg ($@ (dest_real T1))))

real_of_hreal

|- !T1. real_of_hreal T1 = mk_real ($treal_eq (treal_of_hreal T1))

real_TY_DEF

|- ?rep. TYPE_DEFINITION (\c. ?x. c = $treal_eq x) rep

real_tybij

|- (!a. mk_real (dest_real a) = a) /\
   !r. (\c. ?x. c = $treal_eq x) r = (dest_real (mk_real r) = r)

treal_0

|- treal_0 = (hreal_1,hreal_1)

treal_1

|- treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)

treal_add

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

treal_eq

|- !x1 y1 x2 y2.
     (x1,y1) treal_eq (x2,y2) = (x1 hreal_add y2 = 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_lt

|- !x1 y1 x2 y2.
     (x1,y1) treal_lt (x2,y2) = x1 hreal_add y2 hreal_lt x2 hreal_add y1

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_neg

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

treal_of_hreal

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

Theorems

HREAL_EQ_ADDL

|- !x y. ~(x = x hreal_add y)

HREAL_EQ_ADDR

|- !x y. ~(x hreal_add y = x)

HREAL_EQ_LADD

|- !x y z. (x hreal_add y = x hreal_add z) = (y = z)

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_ADDL

|- !x y. x hreal_lt x hreal_add 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_LADD

|- !x y z. x hreal_add y hreal_lt x hreal_add z = y hreal_lt z

HREAL_LT_NE

|- !x y. x hreal_lt y ==> ~(x = y)

HREAL_LT_REFL

|- !x. ~(x hreal_lt x)

HREAL_RDISTRIB

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

REAL_10

|- ~(real_1 = real_0)

REAL_ADD_ASSOC

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

REAL_ADD_LID

|- !x. real_0 + x = x

REAL_ADD_LINV

|- !x. ~x + x = real_0

REAL_ADD_SYM

|- !x y. x + y = y + x

REAL_INV_0

|- inv real_0 = real_0

REAL_ISO_EQ

|- !h i. h hreal_lt i = real_of_hreal h < real_of_hreal i

REAL_LDISTRIB

|- !x y z. x * (y + z) = x * y + 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_LT_REFL

|- !x. ~(x < x)

REAL_LT_TOTAL

|- !x y. (x = y) \/ x < y \/ y < x

REAL_LT_TRANS

|- !x y z. x < y /\ y < z ==> x < z

REAL_MUL_ASSOC

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

REAL_MUL_LID

|- !x. real_1 * x = x

REAL_MUL_LINV

|- !x. ~(x = real_0) ==> (inv x * x = real_1)

REAL_MUL_SYM

|- !x y. x * y = y * x

REAL_POS

|- !X. real_0 < 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

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

TREAL_10

|- ~(treal_1 treal_eq treal_0)

TREAL_ADD_ASSOC

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

TREAL_ADD_LID

|- !x. treal_0 treal_add x treal_eq x

TREAL_ADD_LINV

|- !x. treal_neg x treal_add x treal_eq treal_0

TREAL_ADD_SYM

|- !x y. x treal_add y = y treal_add x

TREAL_ADD_WELLDEF

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

|- !x1 x2 y. x1 treal_eq x2 ==> x1 treal_add y treal_eq x2 treal_add y

TREAL_BIJ

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

|- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i)

TREAL_EQ_AP

|- !p q. (p = q) ==> p treal_eq q

TREAL_EQ_EQUIV

|- !p q. p treal_eq q = ($treal_eq p = $treal_eq q)

TREAL_EQ_REFL

|- !x. x treal_eq x

TREAL_EQ_SYM

|- !x y. x treal_eq y = y treal_eq x

TREAL_EQ_TRANS

|- !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z

TREAL_INV_0

|- treal_inv treal_0 treal_eq treal_0

TREAL_INV_WELLDEF

|- !x1 x2. x1 treal_eq x2 ==> treal_inv x1 treal_eq treal_inv x2

TREAL_ISO

|- !h i. h hreal_lt i ==> treal_of_hreal h treal_lt treal_of_hreal i

TREAL_LDISTRIB

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

TREAL_LT_ADD

|- !x y z. y treal_lt z ==> x treal_add y treal_lt x treal_add z

TREAL_LT_MUL

|- !x y.
     treal_0 treal_lt x /\ treal_0 treal_lt y ==>
     treal_0 treal_lt x treal_mul y

TREAL_LT_REFL

|- !x. ~(x treal_lt x)

TREAL_LT_TOTAL

|- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x

TREAL_LT_TRANS

|- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z

TREAL_LT_WELLDEF

|- !x1 x2 y1 y2.
     x1 treal_eq x2 /\ y1 treal_eq y2 ==> (x1 treal_lt y1 = x2 treal_lt y2)

TREAL_LT_WELLDEFL

|- !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2)

TREAL_LT_WELLDEFR

|- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_lt y = x2 treal_lt y)

TREAL_MUL_ASSOC

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

TREAL_MUL_LID

|- !x. treal_1 treal_mul x treal_eq x

TREAL_MUL_LINV

|- !x. ~(x treal_eq treal_0) ==> treal_inv x treal_mul x treal_eq treal_1

TREAL_MUL_SYM

|- !x y. x treal_mul y = y treal_mul x

TREAL_MUL_WELLDEF

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

|- !x1 x2 y. x1 treal_eq x2 ==> x1 treal_mul y treal_eq x2 treal_mul y

TREAL_NEG_WELLDEF

|- !x1 x2. x1 treal_eq x2 ==> treal_neg x1 treal_eq treal_neg x2