Theory "prim_rec"

Parents num relation

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

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