Theory "prim_rec"

Parents num relation

Signature

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

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

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

measure_def

⊢ measure = inv_image $<

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_ALT

⊢ $< = (λx y. y = SUC x)⁺

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_MONO_EQ

⊢ ∀m n. SUC m < SUC n ⇔ m < n

LESS_MONO_REV

⊢ ∀m n. SUC m < SUC n ⇒ m < 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)

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

RTC_IM_TC

⊢ ∀m n. (λx y. y = f x)꙳ (f m) n ⇔ (λx y. y = f x)⁺ 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)

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

TC_IM_RTC_SUC

⊢ ∀m n. (λx y. y = SUC x)⁺ m (SUC n) ⇔ (λx y. y = SUC x)꙳ m n

WF_IFF_WELLFOUNDED

⊢ ∀R. WF R ⇔ Wellfounded R

WF_LESS

⊢ WF $<

WF_PRED

⊢ WF (λx y. y = SUC x)

WF_measure

⊢ ∀m. WF (measure m)

measure_thm

⊢ ∀f x y. measure f x y ⇔ f x < f y

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