Theory "prim_rec"

Parents     relation   num

Signature

Constant Type
< :num reln
PRE :num -> num
PRIM_REC :α -> (α -> num -> α) -> num -> α
PRIM_REC_FUN :α -> (α -> num -> α) -> num -> num -> α
SIMP_REC :α -> (α -> α) -> num -> α
SIMP_REC_REL :(num -> α) -> α -> (α -> α) -> num -> bool
measure :(α -> num) -> α reln
wellfounded :α reln -> bool

Definitions

LESS_DEF 
|- ∀m n. m < n ⇔ ∃P. (∀n. P (SUC n) ⇒ P n) ∧ P m ∧ ¬P n
SIMP_REC_REL 
|- ∀fun x f n.
     SIMP_REC_REL fun x f n ⇔
     (fun 0 = x) ∧ ∀m. m < n ⇒ (fun (SUC m) = f (fun m))
SIMP_REC 
|- ∀x f' n. ∃g. SIMP_REC_REL g x f' (SUC n) ∧ (SIMP_REC x f' n = g n)
PRE_DEF 
|- ∀m. PRE m = if m = 0 then 0 else @n. m = SUC n
PRIM_REC_FUN 
|- ∀x f. PRIM_REC_FUN x f = SIMP_REC (λn. x) (λfun n. f (fun (PRE n)) n)
PRIM_REC 
|- ∀x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)
wellfounded_def 
|- ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)
measure_def 
|- measure = inv_image $<

Theorems

INV_SUC_EQ 
|- ∀m n. (SUC m = SUC n) ⇔ (m = n)
LESS_REFL 
|- ∀n. ¬(n < n)
SUC_LESS 
|- ∀m n. SUC m < n ⇒ m < n
NOT_LESS_0 
|- ∀n. ¬(n < 0)
LESS_0_0 
|- 0 < SUC 0
LESS_MONO 
|- ∀m n. m < n ⇒ SUC m < SUC n
LESS_SUC_REFL 
|- ∀n. n < SUC n
LESS_SUC 
|- ∀m n. m < n ⇒ m < SUC n
LESS_LEMMA1 
|- ∀m n. m < SUC n ⇒ (m = n) ∨ m < n
LESS_LEMMA2 
|- ∀m n. (m = n) ∨ m < n ⇒ m < SUC n
LESS_THM 
|- ∀m n. m < SUC n ⇔ (m = n) ∨ m < n
LESS_SUC_IMP 
|- ∀m n. m < SUC n ⇒ m ≠ n ⇒ m < n
LESS_0 
|- ∀n. 0 < SUC n
EQ_LESS 
|- ∀n. (SUC m = n) ⇒ m < n
SUC_ID 
|- ∀n. SUC n ≠ n
NOT_LESS_EQ 
|- ∀m n. (m = n) ⇒ ¬(m < n)
LESS_NOT_EQ 
|- ∀m n. m < n ⇒ m ≠ n
SIMP_REC_EXISTS 
|- ∀x f n. ∃fun. SIMP_REC_REL fun x f n
SIMP_REC_REL_UNIQUE 
|- ∀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 
|- ∀x f n. ∃!y. ∃g. SIMP_REC_REL g x f (SUC n) ∧ (y = g n)
LESS_SUC_SUC 
|- ∀m. m < SUC m ∧ m < SUC (SUC m)
SIMP_REC_THM 
|- ∀x f. (SIMP_REC x f 0 = x) ∧ ∀m. SIMP_REC x f (SUC m) = f (SIMP_REC x f m)
PRE 
|- (PRE 0 = 0) ∧ ∀m. PRE (SUC m) = m
PRIM_REC_EQN 
|- ∀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 
|- ∀x f.
     (PRIM_REC x f 0 = x) ∧ ∀m. PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m
DC 
|- ∀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))
num_Axiom_old 
|- ∀e f. ∃!fn1. (fn1 0 = e) ∧ ∀n. fn1 (SUC n) = f (fn1 n) n
num_Axiom 
|- ∀e f. ∃fn. (fn 0 = e) ∧ ∀n. fn (SUC n) = f n (fn n)
WF_IFF_WELLFOUNDED 
|- ∀R. WF R ⇔ wellfounded R
WF_PRED 
|- WF (λx y. y = SUC x)
WF_LESS 
|- WF $<
WF_measure 
|- ∀m. WF (measure m)
measure_thm 
|- ∀f x y. measure f x y ⇔ f x < f y