Structure hratTheory

signature hratTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val hrat_1 : thm
    val hrat_ABS_def : thm
    val hrat_REP_def : thm
    val hrat_TY_DEF : thm
    val hrat_add : thm
    val hrat_bijections : thm
    val hrat_inv : thm
    val hrat_mul : thm
    val hrat_sucint : thm
    val trat_1 : thm
    val trat_add : thm
    val trat_eq : thm
    val trat_inv : thm
    val trat_mul : thm
    val trat_sucint : thm

  (*  Theorems  *)
    val HRAT_ADD_ASSOC : thm
    val HRAT_ADD_SYM : thm
    val HRAT_ADD_TOTAL : thm
    val HRAT_ARCH : thm
    val HRAT_LDISTRIB : thm
    val HRAT_MUL_ASSOC : thm
    val HRAT_MUL_LID : thm
    val HRAT_MUL_LINV : thm
    val HRAT_MUL_SYM : thm
    val HRAT_NOZERO : thm
    val HRAT_SUCINT : thm
    val TRAT_ADD_ASSOC : thm
    val TRAT_ADD_SYM : thm
    val TRAT_ADD_SYM_EQ : thm
    val TRAT_ADD_TOTAL : thm
    val TRAT_ADD_WELLDEFINED : thm
    val TRAT_ADD_WELLDEFINED2 : thm
    val TRAT_ARCH : thm
    val TRAT_EQ_AP : thm
    val TRAT_EQ_EQUIV : thm
    val TRAT_EQ_REFL : thm
    val TRAT_EQ_SYM : thm
    val TRAT_EQ_TRANS : thm
    val TRAT_INV_WELLDEFINED : thm
    val TRAT_LDISTRIB : thm
    val TRAT_MUL_ASSOC : thm
    val TRAT_MUL_LID : thm
    val TRAT_MUL_LINV : thm
    val TRAT_MUL_SYM : thm
    val TRAT_MUL_SYM_EQ : thm
    val TRAT_MUL_WELLDEFINED : thm
    val TRAT_MUL_WELLDEFINED2 : thm
    val TRAT_NOZERO : thm
    val TRAT_SUCINT : thm
    val TRAT_SUCINT_0 : thm
    val hrat_ABS_REP_CLASS : thm
    val hrat_QUOTIENT : thm

  val hrat_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [quotient_list] Parent theory of "hrat"

   [quotient_option] Parent theory of "hrat"

   [quotient_pair] Parent theory of "hrat"

   [quotient_sum] Parent theory of "hrat"

   [hrat_1]  Definition

      |- hrat_1 = hrat_ABS trat_1

   [hrat_ABS_def]  Definition

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

   [hrat_REP_def]  Definition

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

   [hrat_TY_DEF]  Definition

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

   [hrat_add]  Definition

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

   [hrat_bijections]  Definition

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

   [hrat_inv]  Definition

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

   [hrat_mul]  Definition

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

   [hrat_sucint]  Definition

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

   [trat_1]  Definition

      |- trat_1 = (0,0)

   [trat_add]  Definition

      |- ∀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]  Definition

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

   [trat_inv]  Definition

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

   [trat_mul]  Definition

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

   [trat_sucint]  Definition

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

   [HRAT_ADD_ASSOC]  Theorem

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

   [HRAT_ADD_SYM]  Theorem

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

   [HRAT_ADD_TOTAL]  Theorem

      |- ∀h i. (h = i) ∨ (∃d. h = i hrat_add d) ∨ ∃d. i = h hrat_add d

   [HRAT_ARCH]  Theorem

      |- ∀h. ∃n d. hrat_sucint n = h hrat_add d

   [HRAT_LDISTRIB]  Theorem

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

   [HRAT_MUL_ASSOC]  Theorem

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

   [HRAT_MUL_LID]  Theorem

      |- ∀h. hrat_1 hrat_mul h = h

   [HRAT_MUL_LINV]  Theorem

      |- ∀h. hrat_inv h hrat_mul h = hrat_1

   [HRAT_MUL_SYM]  Theorem

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

   [HRAT_NOZERO]  Theorem

      |- ∀h i. h hrat_add i ≠ h

   [HRAT_SUCINT]  Theorem

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

   [TRAT_ADD_ASSOC]  Theorem

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

   [TRAT_ADD_SYM]  Theorem

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

   [TRAT_ADD_SYM_EQ]  Theorem

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

   [TRAT_ADD_TOTAL]  Theorem

      |- ∀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]  Theorem

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

   [TRAT_ADD_WELLDEFINED2]  Theorem

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

   [TRAT_ARCH]  Theorem

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

   [TRAT_EQ_AP]  Theorem

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

   [TRAT_EQ_EQUIV]  Theorem

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

   [TRAT_EQ_REFL]  Theorem

      |- ∀p. p trat_eq p

   [TRAT_EQ_SYM]  Theorem

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

   [TRAT_EQ_TRANS]  Theorem

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

   [TRAT_INV_WELLDEFINED]  Theorem

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

   [TRAT_LDISTRIB]  Theorem

      |- ∀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]  Theorem

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

   [TRAT_MUL_LID]  Theorem

      |- ∀h. trat_1 trat_mul h trat_eq h

   [TRAT_MUL_LINV]  Theorem

      |- ∀h. trat_inv h trat_mul h trat_eq trat_1

   [TRAT_MUL_SYM]  Theorem

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

   [TRAT_MUL_SYM_EQ]  Theorem

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

   [TRAT_MUL_WELLDEFINED]  Theorem

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

   [TRAT_MUL_WELLDEFINED2]  Theorem

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

   [TRAT_NOZERO]  Theorem

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

   [TRAT_SUCINT]  Theorem

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

   [TRAT_SUCINT_0]  Theorem

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

   [hrat_ABS_REP_CLASS]  Theorem

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

   [hrat_QUOTIENT]  Theorem

      |- QUOTIENT $trat_eq hrat_ABS hrat_REP


*)
end

HOL 4, Kananaskis-10