64920
|
1 |
section \<open>Peano's axioms for Natural Numbers\<close>
|
19087
|
2 |
|
64920
|
3 |
theory Peano_Axioms
|
|
4 |
imports Main
|
19087
|
5 |
begin
|
|
6 |
|
64920
|
7 |
locale peano =
|
19087
|
8 |
fixes zero :: 'n
|
64920
|
9 |
fixes succ :: "'n \<Rightarrow> 'n"
|
|
10 |
assumes succ_neq_zero [simp]: "succ m \<noteq> zero"
|
59031
|
11 |
assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
|
64920
|
12 |
assumes induct [case_names zero succ, induct type: 'n]:
|
|
13 |
"P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
|
21368
|
14 |
begin
|
19087
|
15 |
|
21368
|
16 |
lemma zero_neq_succ [simp]: "zero \<noteq> succ m"
|
19087
|
17 |
by (rule succ_neq_zero [symmetric])
|
|
18 |
|
|
19 |
|
63054
|
20 |
text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
|
19087
|
21 |
|
44603
|
22 |
inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
|
21368
|
23 |
for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
24 |
where
|
63054
|
25 |
Rec_zero: "Rec e r zero e"
|
|
26 |
| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
|
19087
|
27 |
|
64920
|
28 |
lemma Rec_functional: "\<exists>!y::'a. Rec e r x y" for x :: 'n
|
21368
|
29 |
proof -
|
|
30 |
let ?R = "Rec e r"
|
|
31 |
show ?thesis
|
|
32 |
proof (induct x)
|
|
33 |
case zero
|
|
34 |
show "\<exists>!y. ?R zero y"
|
|
35 |
proof
|
21392
|
36 |
show "?R zero e" ..
|
63054
|
37 |
show "y = e" if "?R zero y" for y
|
|
38 |
using that by cases simp_all
|
21368
|
39 |
qed
|
|
40 |
next
|
|
41 |
case (succ m)
|
59031
|
42 |
from \<open>\<exists>!y. ?R m y\<close>
|
63054
|
43 |
obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
|
|
44 |
by blast
|
21368
|
45 |
show "\<exists>!z. ?R (succ m) z"
|
|
46 |
proof
|
21392
|
47 |
from y show "?R (succ m) (r m y)" ..
|
63054
|
48 |
next
|
|
49 |
fix z
|
|
50 |
assume "?R (succ m) z"
|
|
51 |
then obtain u where "z = r m u" and "?R m u"
|
|
52 |
by cases simp_all
|
|
53 |
with yy' show "z = r m y"
|
|
54 |
by (simp only:)
|
21368
|
55 |
qed
|
19087
|
56 |
qed
|
|
57 |
qed
|
|
58 |
|
|
59 |
|
63054
|
60 |
text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
|
19087
|
61 |
|
44603
|
62 |
definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
|
|
63 |
where "rec e r x = (THE y. Rec e r x y)"
|
19087
|
64 |
|
21368
|
65 |
lemma rec_eval:
|
|
66 |
assumes Rec: "Rec e r x y"
|
19087
|
67 |
shows "rec e r x = y"
|
|
68 |
unfolding rec_def
|
|
69 |
using Rec_functional and Rec by (rule the1_equality)
|
|
70 |
|
21368
|
71 |
lemma rec_zero [simp]: "rec e r zero = e"
|
19087
|
72 |
proof (rule rec_eval)
|
21392
|
73 |
show "Rec e r zero e" ..
|
19087
|
74 |
qed
|
|
75 |
|
21368
|
76 |
lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
|
19087
|
77 |
proof (rule rec_eval)
|
21368
|
78 |
let ?R = "Rec e r"
|
|
79 |
have "?R m (rec e r m)"
|
|
80 |
unfolding rec_def using Rec_functional by (rule theI')
|
21392
|
81 |
then show "?R (succ m) (r m (rec e r m))" ..
|
19087
|
82 |
qed
|
|
83 |
|
|
84 |
|
63054
|
85 |
text \<open>\<^medskip> Example: addition (monomorphic)\<close>
|
21368
|
86 |
|
44603
|
87 |
definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
|
|
88 |
where "add m n = rec n (\<lambda>_ k. succ k) m"
|
21368
|
89 |
|
|
90 |
lemma add_zero [simp]: "add zero n = n"
|
|
91 |
and add_succ [simp]: "add (succ m) n = succ (add m n)"
|
|
92 |
unfolding add_def by simp_all
|
|
93 |
|
|
94 |
lemma add_assoc: "add (add k m) n = add k (add m n)"
|
|
95 |
by (induct k) simp_all
|
|
96 |
|
|
97 |
lemma add_zero_right: "add m zero = m"
|
|
98 |
by (induct m) simp_all
|
|
99 |
|
|
100 |
lemma add_succ_right: "add m (succ n) = succ (add m n)"
|
|
101 |
by (induct m) simp_all
|
|
102 |
|
21392
|
103 |
lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
|
|
104 |
succ (succ (succ (succ (succ zero))))"
|
|
105 |
by simp
|
|
106 |
|
21368
|
107 |
|
63054
|
108 |
text \<open>\<^medskip> Example: replication (polymorphic)\<close>
|
21368
|
109 |
|
44603
|
110 |
definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
|
|
111 |
where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
|
21368
|
112 |
|
|
113 |
lemma repl_zero [simp]: "repl zero x = []"
|
|
114 |
and repl_succ [simp]: "repl (succ n) x = x # repl n x"
|
|
115 |
unfolding repl_def by simp_all
|
|
116 |
|
|
117 |
lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
|
|
118 |
by simp
|
|
119 |
|
|
120 |
end
|
|
121 |
|
|
122 |
|
63054
|
123 |
text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
|
19087
|
124 |
|
64920
|
125 |
interpretation peano 0 Suc
|
|
126 |
proof
|
19087
|
127 |
fix m n
|
64920
|
128 |
show "Suc m \<noteq> 0" by simp
|
59031
|
129 |
show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
|
63054
|
130 |
show "P n"
|
|
131 |
if zero: "P 0"
|
19087
|
132 |
and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
|
63054
|
133 |
for P
|
19087
|
134 |
proof (induct n)
|
44603
|
135 |
case 0
|
|
136 |
show ?case by (rule zero)
|
19087
|
137 |
next
|
44603
|
138 |
case Suc
|
|
139 |
then show ?case by (rule succ)
|
19087
|
140 |
qed
|
|
141 |
qed
|
|
142 |
|
|
143 |
end
|