Theory: hrat

Parents

• numeral
• pair

Types

• hrat(Arity = 0)

Constants

• trat_inv  :num # num -> num # num
• trat_mul  :num # num -> num # num -> num # num
• hrat_1  :hrat
• trat_sucint  :num -> num # num
• trat_eq  :num # num -> num # num -> bool
• trat_1  :num # num
• hrat_sucint  :num -> hrat
• hrat_add  :hrat -> hrat -> hrat
• hrat_inv  :hrat -> hrat
• hrat_mul  :hrat -> hrat -> hrat
• mk_hrat  :(num # num -> bool) -> hrat
• trat_add  :num # num -> num # num -> num # num
• dest_hrat  :hrat -> num # num -> bool

Definitions

hrat_1

|- hrat_1 = mk_hrat ($trat_eq trat_1)

hrat_add

|- !T1 T2.
     T1 hrat_add T2 =
     mk_hrat ($trat_eq ($@ (dest_hrat T1) trat_add $@ (dest_hrat T2)))

hrat_inv

|- !T1. hrat_inv T1 = mk_hrat ($trat_eq (trat_inv ($@ (dest_hrat T1))))

hrat_mul

|- !T1 T2.
     T1 hrat_mul T2 =
     mk_hrat ($trat_eq ($@ (dest_hrat T1) trat_mul $@ (dest_hrat T2)))

hrat_TY_DEF

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

hrat_tybij

|- (!a. mk_hrat (dest_hrat a) = a) /\
   !r. (\c. ?x. c = $trat_eq x) r = (dest_hrat (mk_hrat r) = r)

trat_1

|- trat_1 = (0,0)

trat_add

|- !x y x' y'.
     (x,y) trat_add (x',y') =
     (PRE (SUC x * SUC y' + SUC x' * SUC y),PRE (SUC y * SUC y'))

trat_eq

|- !x y x' y'. (x,y) trat_eq (x',y') = (SUC x * SUC y' = SUC x' * SUC y)

trat_inv

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

trat_mul

|- !x y x' y'.
     (x,y) trat_mul (x',y') = (PRE (SUC x * SUC x'),PRE (SUC y * SUC y'))

Theorems

HRAT_ADD_ASSOC

|- !h i j. h hrat_add (i hrat_add j) = h hrat_add i hrat_add j

HRAT_ADD_SYM

|- !h i. h hrat_add i = i hrat_add h

HRAT_ADD_TOTAL

|- !h i. (h = i) \/ (?d. h = i hrat_add d) \/ ?d. i = h hrat_add d

HRAT_ARCH

|- !h. ?n d. hrat_sucint n = h hrat_add d

HRAT_LDISTRIB

|- !h i j. h hrat_mul (i hrat_add j) = h hrat_mul i hrat_add h hrat_mul j

HRAT_MUL_ASSOC

|- !h i j. h hrat_mul (i hrat_mul j) = h hrat_mul i hrat_mul j

HRAT_MUL_LID

|- !h. hrat_1 hrat_mul h = h

HRAT_MUL_LINV

|- !h. hrat_inv h hrat_mul h = hrat_1

HRAT_MUL_SYM

|- !h i. h hrat_mul i = i hrat_mul h

HRAT_NOZERO

|- !h i. ~(h hrat_add i = h)

HRAT_SUCINT

|- (hrat_sucint 0 = hrat_1) /\
   !n. hrat_sucint (SUC n) = hrat_sucint n hrat_add hrat_1

TRAT_ADD_ASSOC

|- !h i j. h trat_add (i trat_add j) trat_eq h trat_add i trat_add j

TRAT_ADD_SYM

|- !h i. h trat_add i trat_eq i trat_add h

TRAT_ADD_SYM_EQ

|- !h i. h trat_add i = i trat_add h

TRAT_ADD_TOTAL

|- !h i.
     h trat_eq i \/ (?d. h trat_eq i trat_add d) \/ ?d. i trat_eq h trat_add d

TRAT_ADD_WELLDEFINED

|- !p q r. p trat_eq q ==> p trat_add r trat_eq q trat_add r

TRAT_ADD_WELLDEFINED2

|- !p1 p2 q1 q2.
     p1 trat_eq p2 /\ q1 trat_eq q2 ==> p1 trat_add q1 trat_eq p2 trat_add q2

TRAT_ARCH

|- !h. ?n d. trat_sucint n trat_eq h trat_add d

TRAT_EQ_AP

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

TRAT_EQ_EQUIV

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

TRAT_EQ_REFL

|- !p. p trat_eq p

TRAT_EQ_SYM

|- !p q. p trat_eq q = q trat_eq p

TRAT_EQ_TRANS

|- !p q r. p trat_eq q /\ q trat_eq r ==> p trat_eq r

TRAT_INV_WELLDEFINED

|- !p q. p trat_eq q ==> trat_inv p trat_eq trat_inv q

TRAT_LDISTRIB

|- !h i j.
     h trat_mul (i trat_add j) trat_eq h trat_mul i trat_add h trat_mul j

TRAT_MUL_ASSOC

|- !h i j. h trat_mul (i trat_mul j) trat_eq h trat_mul i trat_mul j

TRAT_MUL_LID

|- !h. trat_1 trat_mul h trat_eq h

TRAT_MUL_LINV

|- !h. trat_inv h trat_mul h trat_eq trat_1

TRAT_MUL_SYM

|- !h i. h trat_mul i trat_eq i trat_mul h

TRAT_MUL_SYM_EQ

|- !h i. h trat_mul i = i trat_mul h

TRAT_MUL_WELLDEFINED

|- !p q r. p trat_eq q ==> p trat_mul r trat_eq q trat_mul r

TRAT_MUL_WELLDEFINED2

|- !p1 p2 q1 q2.
     p1 trat_eq p2 /\ q1 trat_eq q2 ==> p1 trat_mul q1 trat_eq p2 trat_mul q2

TRAT_NOZERO

|- !h i. ~(h trat_add i trat_eq h)

TRAT_SUCINT

|- trat_sucint 0 trat_eq trat_1 /\
   !n. trat_sucint (SUC n) trat_eq trat_sucint n trat_add trat_1

TRAT_SUCINT_0

|- !n. trat_sucint n trat_eq (n,0)