Theory "hrat"

Signature

Definitions

trat_sucint

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

trat_mul

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

trat_inv

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

trat_eq

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

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_1

⊢ trat_1 = (0,0)

hrat_TY_DEF

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

hrat_sucint

⊢ ∀T1. hrat_sucint T1 = hrat_ABS (trat_sucint T1)

hrat_REP_def

⊢ ∀a. hrat_REP a = $@ (hrat_REP_CLASS a)

hrat_mul

⊢ ∀T1 T2. T1 hrat_mul T2 = hrat_ABS (hrat_REP T1 trat_mul hrat_REP T2)

hrat_inv

⊢ ∀T1. hrat_inv T1 = hrat_ABS (trat_inv (hrat_REP T1))

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_add

⊢ ∀T1 T2. T1 hrat_add T2 = hrat_ABS (hrat_REP T1 trat_add hrat_REP T2)

hrat_ABS_def

⊢ ∀r. hrat_ABS r = hrat_ABS_CLASS (trat_eq r)

hrat_1

⊢ hrat_1 = hrat_ABS trat_1

Theorems

TRAT_SUCINT_0

⊢ ∀n. trat_eq (trat_sucint n) (n,0)

TRAT_SUCINT

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

TRAT_NOZERO

⊢ ∀h i. ¬trat_eq (h trat_add i) h

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_MUL_WELLDEFINED

⊢ ∀p q r. trat_eq p q ⇒ trat_eq (p trat_mul r) (q trat_mul r)

TRAT_MUL_SYM_EQ

⊢ ∀h i. h trat_mul i = i trat_mul h

TRAT_MUL_SYM

⊢ ∀h i. trat_eq (h trat_mul i) (i trat_mul h)

TRAT_MUL_LINV

⊢ ∀h. trat_eq (trat_inv h trat_mul h) trat_1

TRAT_MUL_LID

⊢ ∀h. trat_eq (trat_1 trat_mul h) 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_INV_WELLDEFINED

⊢ ∀p q. trat_eq p q ⇒ trat_eq (trat_inv p) (trat_inv q)

TRAT_EQ_TRANS

⊢ ∀p q r. trat_eq p q ∧ trat_eq q r ⇒ trat_eq p r

TRAT_EQ_SYM

⊢ ∀p q. trat_eq p q ⇔ trat_eq q p

TRAT_EQ_REFL

⊢ ∀p. trat_eq p p

TRAT_EQ_EQUIV

⊢ ∀p q. trat_eq p q ⇔ (trat_eq p = trat_eq q)

TRAT_EQ_AP

⊢ ∀p q. (p = q) ⇒ trat_eq p q

TRAT_ARCH

⊢ ∀h. ∃n d. trat_eq (trat_sucint n) (h trat_add d)

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_ADD_WELLDEFINED

⊢ ∀p q r. trat_eq p q ⇒ trat_eq (p trat_add r) (q trat_add r)

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_ADD_SYM_EQ

⊢ ∀h i. h trat_add i = i trat_add h

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)

HRAT_SUCINT

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

hrat_QUOTIENT

⊢ QUOTIENT trat_eq hrat_ABS hrat_REP

HRAT_NOZERO

⊢ ∀h i. h hrat_add i ≠ h

HRAT_MUL_SYM

⊢ ∀h i. h hrat_mul i = i hrat_mul h

HRAT_MUL_LINV

⊢ ∀h. hrat_inv h hrat_mul h = hrat_1

HRAT_MUL_LID

⊢ ∀h. hrat_1 hrat_mul h = 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_ARCH

⊢ ∀h. ∃n d. hrat_sucint n = h hrat_add d

HRAT_ADD_TOTAL

⊢ ∀h i. (h = i) ∨ (∃d. h = i hrat_add d) ∨ ∃d. i = h hrat_add d

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