Structure numTheory

signature numTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val IS_NUM_REP : thm
    val SUC_DEF : thm
    val SUC_REP_DEF : thm
    val ZERO_DEF : thm
    val ZERO_REP_DEF : thm
    val num_ISO_DEF : thm
    val num_TY_DEF : thm

  (*  Theorems  *)
    val INDUCTION : thm
    val INV_SUC : thm
    val NOT_SUC : thm

  val num_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [marker] Parent theory of "num"

   [IS_NUM_REP]  Definition

      |- ∀m.
           IS_NUM_REP m ⇔ ∀P. P ZERO_REP ∧ (∀n. P n ⇒ P (SUC_REP n)) ⇒ P m

   [SUC_DEF]  Definition

      |- ∀m. SUC m = ABS_num (SUC_REP (REP_num m))

   [SUC_REP_DEF]  Definition

      |- ONE_ONE SUC_REP ∧ ¬ONTO SUC_REP

   [ZERO_DEF]  Definition

      |- 0 = ABS_num ZERO_REP

   [ZERO_REP_DEF]  Definition

      |- ∀y. ZERO_REP ≠ SUC_REP y

   [num_ISO_DEF]  Definition

      |- (∀a. ABS_num (REP_num a) = a) ∧
         ∀r. IS_NUM_REP r ⇔ (REP_num (ABS_num r) = r)

   [num_TY_DEF]  Definition

      |- ∃rep. TYPE_DEFINITION IS_NUM_REP rep

   [INDUCTION]  Theorem

      |- ∀P. P 0 ∧ (∀n. P n ⇒ P (SUC n)) ⇒ ∀n. P n

   [INV_SUC]  Theorem

      |- ∀m n. (SUC m = SUC n) ⇒ (m = n)

   [NOT_SUC]  Theorem

      |- ∀n. SUC n ≠ 0


*)
end

HOL 4, Kananaskis-11