Theory "prim_rec"

Signature

Definitions

LESS_DEF

|- ∀m n. m < n ⇔ ∃P. (∀n. P (SUC n) ⇒ P n) ∧ P m ∧ ¬P n

PRE_DEF

|- ∀m. PRE m = if m = 0 then 0 else @n. m = SUC 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)

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)

PRE

|- (PRE 0 = 0) ∧ ∀m. PRE (SUC m) = m

LESS_REFL

|- ∀n. ¬(n < n)

SUC_LESS

|- ∀m n. SUC m < n ⇒ m < n

NOT_LESS_0

|- ∀n. ¬(n < 0)

LESS_0

|- ∀n. 0 < SUC n

LESS_0_0

|- 0 < SUC 0

LESS_MONO

|- ∀m n. m < n ⇒ SUC m < SUC n

LESS_MONO_REV

|- ∀m n. SUC m < SUC n ⇒ m < n

LESS_MONO_EQ

|- ∀m n. SUC m < SUC n ⇔ m < n

TC_IM_RTC_SUC

|- ∀m n. (λx y. y = SUC x)⁺ m (SUC n) ⇔ (λx y. y = SUC x)^* m n

RTC_IM_TC

|- ∀m n. (λx y. y = f x)^* (f m) n ⇔ (λx y. y = f x)⁺ m n

LESS_ALT

|- $< = (λx y. y = SUC x)⁺

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

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)

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