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