Theory: prim_rec

Parents

<:num -> num -> bool {fixity = Infix 450}
SIMP_REC_REL:(num -> 'a) -> 'a -> ('a -> 'a) -> num -> bool {fixity = Prefix}
SIMP_REC_FUN:'a -> ('a -> 'a) -> num -> num -> 'a {fixity = Prefix}
SIMP_REC:'a -> ('a -> 'a) -> num -> 'a {fixity = Prefix}
PRE:num -> num {fixity = Prefix}
PRIM_REC_FUN:'a -> ('a -> num -> 'a) -> num -> num -> 'a {fixity = Prefix}
PRIM_REC:'a -> ('a -> num -> 'a) -> num -> 'a {fixity = Prefix}

LESS

|- !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_FUN

|- !x f n. SIMP_REC_FUN x f n = (@fun. SIMP_REC_REL fun x f n)

SIMP_REC

|- !x f n. SIMP_REC x f n = SIMP_REC_FUN x f (SUC n) n

PRE_DEF

|- !m. PRE m = ((m = 0) => 0 | (@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)

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_FUN_LEMMA

|- (?fun. SIMP_REC_REL fun x f n) =
   (SIMP_REC_FUN x f n 0 = x) /\
   (!m. m < n ==> (SIMP_REC_FUN x f n (SUC m) = f (SIMP_REC_FUN x f n m)))

SIMP_REC_EXISTS

|- !x f n. ?fun. SIMP_REC_REL fun x f 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)

num_Axiom

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