Theory "hrat"

Parents quotient_sum quotient_pair quotient_option quotient_list

Signature

Type	Arity
hrat	0
Constant	Type
hrat_1	:hrat
hrat_ABS	:num # num -> hrat
hrat_ABS_CLASS	:num reln -> hrat
hrat_REP	:hrat -> num # num
hrat_REP_CLASS	:hrat -> num reln
hrat_add	:hrat -> hrat -> hrat
hrat_inv	:hrat -> hrat
hrat_mul	:hrat -> hrat -> hrat
hrat_sucint	:num -> hrat
trat_1	:num # num
trat_add	:num # num -> num # num -> num # num
trat_eq	:(num # num) reln
trat_inv	:num # num -> num # num
trat_mul	:num # num -> num # num -> num # num
trat_sucint	:num -> num # num

Definitions

trat_1

|- trat_1 = (0,0)

trat_inv

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

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_mul

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

trat_sucint

|- (trat_sucint 0 = trat_1) ∧
   ∀n. trat_sucint (SUC n) = trat_sucint n trat_add trat_1

trat_eq

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

hrat_TY_DEF

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

hrat_bijections

|- (∀a. hrat_ABS_CLASS (hrat_REP_CLASS a) = a) ∧
   ∀r.
     (λc. ∃r. trat_eq r r ∧ (c = trat_eq r)) r ⇔
     (hrat_REP_CLASS (hrat_ABS_CLASS r) = r)

hrat_REP_def

|- ∀a. hrat_REP a = $@ (hrat_REP_CLASS a)

hrat_ABS_def

|- ∀r. hrat_ABS r = hrat_ABS_CLASS (trat_eq r)

hrat_1

|- hrat_1 = hrat_ABS trat_1

hrat_inv

|- ∀T1. hrat_inv T1 = hrat_ABS (trat_inv (hrat_REP T1))

hrat_add

|- ∀T1 T2. T1 hrat_add T2 = hrat_ABS (hrat_REP T1 trat_add hrat_REP T2)

hrat_mul

|- ∀T1 T2. T1 hrat_mul T2 = hrat_ABS (hrat_REP T1 trat_mul hrat_REP T2)

hrat_sucint

|- ∀T1. hrat_sucint T1 = hrat_ABS (trat_sucint T1)

Theorems

TRAT_EQ_REFL

|- ∀p. trat_eq p p

TRAT_EQ_SYM

|- ∀p q. trat_eq p q ⇔ trat_eq q p

TRAT_EQ_TRANS

|- ∀p q r. trat_eq p q ∧ trat_eq q r ⇒ trat_eq p r

TRAT_EQ_AP

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

TRAT_ADD_SYM_EQ

|- ∀h i. h trat_add i = i trat_add h

TRAT_MUL_SYM_EQ

|- ∀h i. h trat_mul i = i trat_mul h

TRAT_INV_WELLDEFINED

|- ∀p q. trat_eq p q ⇒ trat_eq (trat_inv p) (trat_inv q)

TRAT_ADD_WELLDEFINED

|- ∀p q r. trat_eq p q ⇒ trat_eq (p trat_add r) (q trat_add r)

TRAT_ADD_WELLDEFINED2

|- ∀p1 p2 q1 q2.
     trat_eq p1 p2 ∧ trat_eq q1 q2 ⇒ trat_eq (p1 trat_add q1) (p2 trat_add q2)

TRAT_MUL_WELLDEFINED

|- ∀p q r. trat_eq p q ⇒ trat_eq (p trat_mul r) (q trat_mul r)

TRAT_MUL_WELLDEFINED2

|- ∀p1 p2 q1 q2.
     trat_eq p1 p2 ∧ trat_eq q1 q2 ⇒ trat_eq (p1 trat_mul q1) (p2 trat_mul q2)

TRAT_ADD_SYM

|- ∀h i. trat_eq (h trat_add i) (i trat_add h)

TRAT_ADD_ASSOC

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

TRAT_MUL_SYM

|- ∀h i. trat_eq (h trat_mul i) (i trat_mul h)

TRAT_MUL_ASSOC

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

TRAT_LDISTRIB

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

TRAT_MUL_LID

|- ∀h. trat_eq (trat_1 trat_mul h) h

TRAT_MUL_LINV

|- ∀h. trat_eq (trat_inv h trat_mul h) trat_1

TRAT_NOZERO

|- ∀h i. ¬trat_eq (h trat_add i) h

TRAT_ADD_TOTAL

|- ∀h i.
     trat_eq h i ∨ (∃d. trat_eq h (i trat_add d)) ∨
     ∃d. trat_eq i (h trat_add d)

TRAT_SUCINT_0

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

TRAT_ARCH

|- ∀h. ∃n d. trat_eq (trat_sucint n) (h trat_add d)

TRAT_SUCINT

|- trat_eq (trat_sucint 0) trat_1 ∧
   ∀n. trat_eq (trat_sucint (SUC n)) (trat_sucint n trat_add trat_1)

TRAT_EQ_EQUIV

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

hrat_ABS_REP_CLASS

|- (∀a. hrat_ABS_CLASS (hrat_REP_CLASS a) = a) ∧
   ∀c.
     (∃r. trat_eq r r ∧ (c = trat_eq r)) ⇔
     (hrat_REP_CLASS (hrat_ABS_CLASS c) = c)

hrat_QUOTIENT

|- QUOTIENT trat_eq hrat_ABS hrat_REP

HRAT_ADD_SYM

|- ∀h i. h hrat_add i = i hrat_add h

HRAT_ADD_ASSOC

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

HRAT_MUL_SYM

|- ∀h i. h hrat_mul i = i hrat_mul h

HRAT_MUL_ASSOC

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

HRAT_LDISTRIB

|- ∀h i j. h hrat_mul (i hrat_add j) = h hrat_mul i hrat_add h 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_NOZERO

|- ∀h i. h hrat_add i ≠ 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_SUCINT

|- (hrat_sucint 0 = hrat_1) ∧
   ∀n. hrat_sucint (SUC n) = hrat_sucint n hrat_add hrat_1