section \<open>Peano's axioms for Natural Numbers\<close>
theory Peano_Axioms
imports Main
begin
locale peano = \<comment> \<open>or: \<^theory_text>\<open>class\<close>\<close>
fixes zero :: 'a
fixes succ :: "'a \ 'a"
assumes succ_neq_zero [simp]: "succ m \ zero"
assumes succ_inject [simp]: "succ m = succ n \ m = n"
assumes induct [case_names zero succ, induct type: 'a]:
"P zero \ (\n. P n \ P (succ n)) \ P n"
begin
lemma zero_neq_succ [simp]: "zero \ succ m"
by (rule succ_neq_zero [symmetric])
text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
inductive Rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b \ bool"
for e :: 'b and r :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
where
Rec_zero: "Rec e r zero e"
| Rec_succ: "Rec e r m n \ Rec e r (succ m) (r m n)"
lemma Rec_functional: "\!y::'b. Rec e r x y" for x :: 'a
proof -
let ?R = "Rec e r"
show ?thesis
proof (induct x)
case zero
show "\!y. ?R zero y"
proof
show "?R zero e" ..
show "y = e" if "?R zero y" for y
using that by cases simp_all
qed
next
case (succ m)
from \<open>\<exists>!y. ?R m y\<close>
obtain y where y: "?R m y" and yy': "\y'. ?R m y' \ y = y'"
by blast
show "\!z. ?R (succ m) z"
proof
from y show "?R (succ m) (r m y)" ..
next
fix z
assume "?R (succ m) z"
then obtain u where "z = r m u" and "?R m u"
by cases simp_all
with yy' show "z = r m y"
by (simp only:)
qed
qed
qed
text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
definition rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b"
where "rec e r x = (THE y. Rec e r x y)"
lemma rec_eval:
assumes Rec: "Rec e r x y"
shows "rec e r x = y"
unfolding rec_def
using Rec_functional and Rec by (rule the1_equality)
lemma rec_zero [simp]: "rec e r zero = e"
proof (rule rec_eval)
show "Rec e r zero e" ..
qed
lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
proof (rule rec_eval)
let ?R = "Rec e r"
have "?R m (rec e r m)"
unfolding rec_def using Rec_functional by (rule theI')
then show "?R (succ m) (r m (rec e r m))" ..
qed
text \<open>\<^medskip> Example: addition (monomorphic)\<close>
definition add :: "'a \ 'a \ 'a"
where "add m n = rec n (\_ k. succ k) m"
lemma add_zero [simp]: "add zero n = n"
and add_succ [simp]: "add (succ m) n = succ (add m n)"
unfolding add_def by simp_all
lemma add_assoc: "add (add k m) n = add k (add m n)"
by (induct k) simp_all
lemma add_zero_right: "add m zero = m"
by (induct m) simp_all
lemma add_succ_right: "add m (succ n) = succ (add m n)"
by (induct m) simp_all
lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
succ (succ (succ (succ (succ zero))))"
by simp
text \<open>\<^medskip> Example: replication (polymorphic)\<close>
definition repl :: "'a \ 'b \ 'b list"
where "repl n x = rec [] (\_ xs. x # xs) n"
lemma repl_zero [simp]: "repl zero x = []"
and repl_succ [simp]: "repl (succ n) x = x # repl n x"
unfolding repl_def by simp_all
lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
by simp
end
text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
interpretation peano 0 Suc
proof
fix m n
show "Suc m \ 0" by simp
show "Suc m = Suc n \ m = n" by simp
show "P n"
if zero: "P 0"
and succ: "\n. P n \ P (Suc n)"
for P
proof (induct n)
case 0
show ?case by (rule zero)
next
case Suc
then show ?case by (rule succ)
qed
qed
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
