Structure prim_recTheory

signature prim_recTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val LESS_DEF : thm
    val PRE_DEF : thm
    val PRIM_REC : thm
    val PRIM_REC_FUN : thm
    val SIMP_REC : thm
    val SIMP_REC_REL : thm
    val measure_def : thm
    val wellfounded_def : thm
  
  (*  Theorems  *)
    val DC : thm
    val EQ_LESS : thm
    val INV_SUC_EQ : thm
    val LESS_0 : thm
    val LESS_0_0 : thm
    val LESS_LEMMA1 : thm
    val LESS_LEMMA2 : thm
    val LESS_MONO : thm
    val LESS_NOT_EQ : thm
    val LESS_REFL : thm
    val LESS_SUC : thm
    val LESS_SUC_IMP : thm
    val LESS_SUC_REFL : thm
    val LESS_SUC_SUC : thm
    val LESS_THM : thm
    val NOT_LESS_0 : thm
    val NOT_LESS_EQ : thm
    val PRE : thm
    val PRIM_REC_EQN : thm
    val PRIM_REC_THM : thm
    val SIMP_REC_EXISTS : thm
    val SIMP_REC_REL_UNIQUE : thm
    val SIMP_REC_REL_UNIQUE_RESULT : thm
    val SIMP_REC_THM : thm
    val SUC_ID : thm
    val SUC_LESS : thm
    val WF_IFF_WELLFOUNDED : thm
    val WF_LESS : thm
    val WF_PRED : thm
    val WF_measure : thm
    val measure_thm : thm
    val num_Axiom : thm
    val num_Axiom_old : thm
  
  val prim_rec_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [num] Parent theory of "prim_rec"
   
   [relation] Parent theory of "prim_rec"
   
   [LESS_DEF]  Definition
      
      |- !m n. m < n = ?P. (!n. P (SUC n) ==> P n) /\ P m /\ ~P n
   
   [PRE_DEF]  Definition
      
      |- !m. PRE m = (if m = 0 then 0 else @n. m = SUC n)
   
   [PRIM_REC]  Definition
      
      |- !x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)
   
   [PRIM_REC_FUN]  Definition
      
      |- !x f. PRIM_REC_FUN x f = SIMP_REC (\n. x) (\fun n. f (fun (PRE n)) n)
   
   [SIMP_REC]  Definition
      
      |- !x f' n. ?g. SIMP_REC_REL g x f' (SUC n) /\ (SIMP_REC x f' n = g n)
   
   [SIMP_REC_REL]  Definition
      
      |- !fun x f n.
           SIMP_REC_REL fun x f n =
           (fun 0 = x) /\ !m. m < n ==> (fun (SUC m) = f (fun m))
   
   [measure_def]  Definition
      
      |- measure = inv_image $<
   
   [wellfounded_def]  Definition
      
      |- !R. wellfounded R = ~ ?f. !n. R (f (SUC n)) (f n)
   
   [DC]  Theorem
      
      |- !P R a.
           P a /\ (!x. P x ==> ?y. P y /\ R x y) ==>
           ?f. (f 0 = a) /\ !n. P (f n) /\ R (f n) (f (SUC n))
   
   [EQ_LESS]  Theorem
      
      |- !n. (SUC m = n) ==> m < n
   
   [INV_SUC_EQ]  Theorem
      
      |- !m n. (SUC m = SUC n) = (m = n)
   
   [LESS_0]  Theorem
      
      |- !n. 0 < SUC n
   
   [LESS_0_0]  Theorem
      
      |- 0 < SUC 0
   
   [LESS_LEMMA1]  Theorem
      
      |- !m n. m < SUC n ==> (m = n) \/ m < n
   
   [LESS_LEMMA2]  Theorem
      
      |- !m n. (m = n) \/ m < n ==> m < SUC n
   
   [LESS_MONO]  Theorem
      
      |- !m n. m < n ==> SUC m < SUC n
   
   [LESS_NOT_EQ]  Theorem
      
      |- !m n. m < n ==> ~(m = n)
   
   [LESS_REFL]  Theorem
      
      |- !n. ~(n < n)
   
   [LESS_SUC]  Theorem
      
      |- !m n. m < n ==> m < SUC n
   
   [LESS_SUC_IMP]  Theorem
      
      |- !m n. m < SUC n ==> ~(m = n) ==> m < n
   
   [LESS_SUC_REFL]  Theorem
      
      |- !n. n < SUC n
   
   [LESS_SUC_SUC]  Theorem
      
      |- !m. m < SUC m /\ m < SUC (SUC m)
   
   [LESS_THM]  Theorem
      
      |- !m n. m < SUC n = (m = n) \/ m < n
   
   [NOT_LESS_0]  Theorem
      
      |- !n. ~(n < 0)
   
   [NOT_LESS_EQ]  Theorem
      
      |- !m n. (m = n) ==> ~(m < n)
   
   [PRE]  Theorem
      
      |- (PRE 0 = 0) /\ !m. PRE (SUC m) = m
   
   [PRIM_REC_EQN]  Theorem
      
      |- !x f.
           (!n. PRIM_REC_FUN x f 0 n = x) /\
           !m n. PRIM_REC_FUN x f (SUC m) n = f (PRIM_REC_FUN x f m (PRE n)) n
   
   [PRIM_REC_THM]  Theorem
      
      |- !x f.
           (PRIM_REC x f 0 = x) /\ !m. PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m
   
   [SIMP_REC_EXISTS]  Theorem
      
      |- !x f n. ?fun. SIMP_REC_REL fun x f n
   
   [SIMP_REC_REL_UNIQUE]  Theorem
      
      |- !x f g1 g2 m1 m2.
           SIMP_REC_REL g1 x f m1 /\ SIMP_REC_REL g2 x f m2 ==>
           !n. n < m1 /\ n < m2 ==> (g1 n = g2 n)
   
   [SIMP_REC_REL_UNIQUE_RESULT]  Theorem
      
      |- !x f n. ?!y. ?g. SIMP_REC_REL g x f (SUC n) /\ (y = g n)
   
   [SIMP_REC_THM]  Theorem
      
      |- !x f. (SIMP_REC x f 0 = x) /\ !m. SIMP_REC x f (SUC m) = f (SIMP_REC x f m)
   
   [SUC_ID]  Theorem
      
      |- !n. ~(SUC n = n)
   
   [SUC_LESS]  Theorem
      
      |- !m n. SUC m < n ==> m < n
   
   [WF_IFF_WELLFOUNDED]  Theorem
      
      |- !R. WF R = wellfounded R
   
   [WF_LESS]  Theorem
      
      |- WF $<
   
   [WF_PRED]  Theorem
      
      |- WF (\x y. y = SUC x)
   
   [WF_measure]  Theorem
      
      |- !m. WF (measure m)
   
   [measure_thm]  Theorem
      
      |- !f x y. measure f x y = f x < f y
   
   [num_Axiom]  Theorem
      
      |- !e f. ?fn. (fn 0 = e) /\ !n. fn (SUC n) = f n (fn n)
   
   [num_Axiom_old]  Theorem
      
      |- !e f. ?!fn1. (fn1 0 = e) /\ !n. fn1 (SUC n) = f (fn1 n) n
   
   
*)
end