Theory: prim_rec

Parents

• relation
• num

Types

Constants

• <  :num -> num -> bool
• PRIM_REC_FUN  :'a -> ('a -> num -> 'a) -> num -> num -> 'a
• measure  :('a -> num) -> 'a -> 'a -> bool
• SIMP_REC  :'a -> ('a -> 'a) -> num -> 'a
• SIMP_REC_REL  :(num -> 'a) -> 'a -> ('a -> 'a) -> num -> bool
• wellfounded  :('a -> 'a -> bool) -> bool
• PRIM_REC  :'a -> ('a -> num -> 'a) -> num -> 'a
• PRE  :num -> num

Definitions

LESS_DEF

|- !m n. m < n = ?P. (!n. P (SUC n) ==> P n) /\ P m /\ ~P n

measure_def

|- measure = inv_image $<

PRE_DEF

|- !m. PRE m = (if m = 0 then 0 else @n. m = SUC n)

PRIM_REC

|- !x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)

PRIM_REC_FUN

|- !x f. PRIM_REC_FUN x f = SIMP_REC (\n. x) (\fun n. f (fun (PRE n)) n)

SIMP_REC

|- !x f' n. ?g. SIMP_REC_REL g x f' (SUC n) /\ (SIMP_REC x f' n = g 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))

wellfounded_def

|- !R. wellfounded R = ~?f. !n. R (f (SUC n)) (f n)

Theorems

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))

EQ_LESS

|- !n. (SUC m = n) ==> m < n

INV_SUC_EQ

|- !m n. (SUC m = SUC n) = (m = n)

LESS_0

|- !n. 0 < SUC n

LESS_0_0

|- 0 < SUC 0

LESS_LEMMA1

|- !m n. m < SUC n ==> (m = n) \/ m < n

LESS_LEMMA2

|- !m n. (m = n) \/ m < n ==> m < SUC n

LESS_MONO

|- !m n. m < n ==> SUC m < SUC n

LESS_NOT_EQ

|- !m n. m < n ==> ~(m = n)

LESS_REFL

|- !n. ~(n < n)

LESS_SUC

|- !m n. m < n ==> m < SUC n

LESS_SUC_IMP

|- !m n. m < SUC n ==> ~(m = n) ==> m < n

LESS_SUC_REFL

|- !n. n < SUC n

LESS_SUC_SUC

|- !m. m < SUC m /\ m < SUC (SUC m)

LESS_THM

|- !m n. m < SUC n = (m = n) \/ m < n

NOT_LESS_0

|- !n. ~(n < 0)

NOT_LESS_EQ

|- !m n. (m = n) ==> ~(m < n)

num_Axiom

|- !e f. ?fn. (fn 0 = e) /\ !n. fn (SUC n) = f n (fn n)

num_Axiom_old

|- !e f. ?!fn1. (fn1 0 = e) /\ !n. fn1 (SUC n) = f (fn1 n) n

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

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)

SIMP_REC_THM

|- !x f. (SIMP_REC x f 0 = x) /\ !m. SIMP_REC x f (SUC m) = f (SIMP_REC x f m)

SUC_ID

|- !n. ~(SUC n = n)

SUC_LESS

|- !m n. SUC m < n ==> m < n

WF_IFF_WELLFOUNDED

|- !R. WF R = wellfounded R

WF_LESS

|- WF $<

WF_measure

|- !m. WF (measure m)

WF_PRED

|- WF (\x y. y = SUC x)