Theory: hreal

Parents

• hrat

Types

• hreal(Arity = 0)

Constants

• hreal  :(hrat -> bool) -> hreal
• cut  :hreal -> hrat -> bool
• hreal_add  :hreal -> hreal -> hreal
• cut_of_hrat  :hrat -> hrat -> bool
• hreal_inv  :hreal -> hreal
• hreal_mul  :hreal -> hreal -> hreal
• hreal_1  :hreal
• hreal_lt  :hreal -> hreal -> bool
• hreal_sub  :hreal -> hreal -> hreal
• hreal_sup  :(hreal -> bool) -> hreal
• hrat_lt  :hrat -> hrat -> bool
• isacut  :(hrat -> bool) -> bool

Definitions

cut_of_hrat

|- !x. cut_of_hrat x = (\y. y hrat_lt x)

hrat_lt

|- !x y. x hrat_lt y = ?d. y = x hrat_add d

hreal_1

|- hreal_1 = hreal (cut_of_hrat hrat_1)

hreal_add

|- !X Y.
     X hreal_add Y =
     hreal (\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y)

hreal_inv

|- !X.
     hreal_inv X =
     hreal
       (\w. ?d. d hrat_lt hrat_1 /\ !x. cut X x ==> w hrat_mul x hrat_lt d)

hreal_mul

|- !X Y.
     X hreal_mul Y =
     hreal (\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y)

hreal_sub

|- !Y X. Y hreal_sub X = hreal (\w. ?x. ~cut X x /\ cut Y (x hrat_add w))

hreal_TY_DEF

|- ?rep. TYPE_DEFINITION isacut rep

hreal_tybij

|- (!a. hreal (cut a) = a) /\ !r. isacut r = (cut (hreal r) = r)

isacut

|- !C'.
     isacut C' =
     (?x. C' x) /\ (?x. ~C' x) /\ (!x y. C' x /\ y hrat_lt x ==> C' y) /\
     !x. C' x ==> ?y. C' y /\ x hrat_lt y

Theorems

CUT_BOUNDED

|- !X. ?x. ~cut X x

CUT_DOWN

|- !X x y. cut X x /\ y hrat_lt x ==> cut X y

CUT_ISACUT

|- !X. isacut (cut X)

CUT_NEARTOP_ADD

|- !X e. ?x. cut X x /\ ~cut X (x hrat_add e)

CUT_NEARTOP_MUL

|- !X u. hrat_1 hrat_lt u ==> ?x. cut X x /\ ~cut X (u hrat_mul x)

CUT_NONEMPTY

|- !X. ?x. cut X x

CUT_STRADDLE

|- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y

CUT_UBOUND

|- !X x y. ~cut X x /\ x hrat_lt y ==> ~cut X y

CUT_UP

|- !X x. cut X x ==> ?y. cut X y /\ x hrat_lt y

EQUAL_CUTS

|- !X Y. (cut X = cut Y) ==> (X = Y)

HRAT_DOWN

|- !x. ?y. y hrat_lt x

HRAT_DOWN2

|- !x y. ?z. z hrat_lt x /\ z hrat_lt y

HRAT_EQ_LADD

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

HRAT_EQ_LMUL

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

HRAT_GT_L1

|- !x y. hrat_1 hrat_lt hrat_inv x hrat_mul y = x hrat_lt y

HRAT_GT_LMUL1

|- !x y. y hrat_lt x hrat_mul y = hrat_1 hrat_lt x

HRAT_INV_MUL

|- !x y. hrat_inv (x hrat_mul y) = hrat_inv x hrat_mul hrat_inv y

HRAT_LT_ADD2

|- !u v x y. u hrat_lt x /\ v hrat_lt y ==> u hrat_add v hrat_lt x hrat_add y

HRAT_LT_ADDL

|- !x y. x hrat_lt x hrat_add y

HRAT_LT_ADDR

|- !x y. y hrat_lt x hrat_add y

HRAT_LT_ANTISYM

|- !x y. ~(x hrat_lt y /\ y hrat_lt x)

HRAT_LT_GT

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

HRAT_LT_L1

|- !x y. hrat_inv x hrat_mul y hrat_lt hrat_1 = y hrat_lt x

HRAT_LT_LADD

|- !x y z. z hrat_add x hrat_lt z hrat_add y = x hrat_lt y

HRAT_LT_LMUL

|- !x y z. z hrat_mul x hrat_lt z hrat_mul y = x hrat_lt y

HRAT_LT_LMUL1

|- !x y. x hrat_mul y hrat_lt y = x hrat_lt hrat_1

HRAT_LT_MUL2

|- !u v x y. u hrat_lt x /\ v hrat_lt y ==> u hrat_mul v hrat_lt x hrat_mul y

HRAT_LT_NE

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

HRAT_LT_R1

|- !x y. x hrat_mul hrat_inv y hrat_lt hrat_1 = x hrat_lt y

HRAT_LT_RADD

|- !x y z. x hrat_add z hrat_lt y hrat_add z = x hrat_lt y

HRAT_LT_REFL

|- !x. ~(x hrat_lt x)

HRAT_LT_RMUL

|- !x y z. x hrat_mul z hrat_lt y hrat_mul z = x hrat_lt y

HRAT_LT_RMUL1

|- !x y. x hrat_mul y hrat_lt x = y hrat_lt hrat_1

HRAT_LT_TOTAL

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

HRAT_LT_TRANS

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

HRAT_MEAN

|- !x y. x hrat_lt y ==> ?z. x hrat_lt z /\ z hrat_lt y

HRAT_MUL_RID

|- !x. x hrat_mul hrat_1 = x

HRAT_MUL_RINV

|- !x. x hrat_mul hrat_inv x = hrat_1

HRAT_RDISTRIB

|- !x y z. (x hrat_add y) hrat_mul z = x hrat_mul z hrat_add y hrat_mul z

HRAT_UP

|- !x. ?y. x hrat_lt y

HREAL_ADD_ASSOC

|- !X Y Z. X hreal_add (Y hreal_add Z) = X hreal_add Y hreal_add Z

HREAL_ADD_ISACUT

|- !X Y. isacut (\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y)

HREAL_ADD_SYM

|- !X Y. X hreal_add Y = Y hreal_add X

HREAL_ADD_TOTAL

|- !X Y. (X = Y) \/ (?D. Y = X hreal_add D) \/ ?D. X = Y hreal_add D

HREAL_INV_ISACUT

|- !X.
     isacut
       (\w. ?d. d hrat_lt hrat_1 /\ !x. cut X x ==> w hrat_mul x hrat_lt d)

HREAL_LDISTRIB

|- !X Y Z. X hreal_mul (Y hreal_add Z) = X hreal_mul Y hreal_add X hreal_mul Z

HREAL_LT

|- !X Y. X hreal_lt Y = ?D. Y = X hreal_add D

HREAL_LT_LEMMA

|- !X Y. X hreal_lt Y ==> ?x. ~cut X x /\ cut Y x

HREAL_LT_TOTAL

|- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X

HREAL_MUL_ASSOC

|- !X Y Z. X hreal_mul (Y hreal_mul Z) = X hreal_mul Y hreal_mul Z

HREAL_MUL_ISACUT

|- !X Y. isacut (\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y)

HREAL_MUL_LID

|- !X. hreal_1 hreal_mul X = X

HREAL_MUL_LINV

|- !X. hreal_inv X hreal_mul X = hreal_1

HREAL_MUL_SYM

|- !X Y. X hreal_mul Y = Y hreal_mul X

HREAL_NOZERO

|- !X Y. ~(X hreal_add Y = X)

HREAL_SUB_ADD

|- !X Y. X hreal_lt Y ==> (Y hreal_sub X hreal_add X = Y)

HREAL_SUB_ISACUT

|- !X Y. X hreal_lt Y ==> isacut (\w. ?x. ~cut X x /\ cut Y (x hrat_add w))

HREAL_SUP

|- !P.
     (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==>
     !Y. (?X. P X /\ Y hreal_lt X) = Y hreal_lt hreal_sup P

HREAL_SUP_ISACUT

|- !P.
     (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==>
     isacut (\w. ?X. P X /\ cut X w)

ISACUT_HRAT

|- !h. isacut (cut_of_hrat h)