Theory Natural_Numbers
section ‹Natural numbers›
theory Natural_Numbers
imports FOL
begin
text ‹
Theory of the natural numbers: Peano's axioms, primitive recursion.
(Modernized version of Larry Paulson's theory "Nat".) \medskip
›
typedecl nat
instance nat :: ‹term› ..
axiomatization
Zero :: ‹nat› (‹0›) and
Suc :: ‹nat => nat› and
rec :: ‹[nat, 'a, [nat, 'a] => 'a] => 'a›
where
induct [case_names 0 Suc, induct type: nat]:
‹P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)› and
Suc_inject: ‹Suc(m) = Suc(n) ==> m = n› and
Suc_neq_0: ‹Suc(m) = 0 ==> R› and
rec_0: ‹rec(0, a, f) = a› and
rec_Suc: ‹rec(Suc(m), a, f) = f(m, rec(m, a, f))›
lemma Suc_n_not_n: ‹Suc(k) ≠ k›
proof (induct ‹k›)
show ‹Suc(0) ≠ 0›
proof
assume ‹Suc(0) = 0›
then show ‹False› by (rule Suc_neq_0)
qed
next
fix n assume hyp: ‹Suc(n) ≠ n›
show ‹Suc(Suc(n)) ≠ Suc(n)›
proof
assume ‹Suc(Suc(n)) = Suc(n)›
then have ‹Suc(n) = n› by (rule Suc_inject)
with hyp show ‹False› by contradiction
qed
qed
definition add :: ‹nat => nat => nat› (infixl ‹+› 60)
where ‹m + n = rec(m, n, λx y. Suc(y))›
lemma add_0 [simp]: ‹0 + n = n›
unfolding add_def by (rule rec_0)
lemma add_Suc [simp]: ‹Suc(m) + n = Suc(m + n)›
unfolding add_def by (rule rec_Suc)
lemma add_assoc: ‹(k + m) + n = k + (m + n)›
by (induct ‹k›) simp_all
lemma add_0_right: ‹m + 0 = m›
by (induct ‹m›) simp_all
lemma add_Suc_right: ‹m + Suc(n) = Suc(m + n)›
by (induct ‹m›) simp_all
lemma
assumes ‹!!n. f(Suc(n)) = Suc(f(n))›
shows ‹f(i + j) = i + f(j)›
using assms by (induct ‹i›) simp_all
end