|
1 section \<open>Peano's axioms for Natural Numbers\<close> |
|
2 |
|
3 theory Peano_Axioms |
|
4 imports Main |
|
5 begin |
|
6 |
|
7 locale peano = |
|
8 fixes zero :: 'n |
|
9 fixes succ :: "'n \<Rightarrow> 'n" |
|
10 assumes succ_neq_zero [simp]: "succ m \<noteq> zero" |
|
11 assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n" |
|
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" |
|
14 begin |
|
15 |
|
16 lemma zero_neq_succ [simp]: "zero \<noteq> succ m" |
|
17 by (rule succ_neq_zero [symmetric]) |
|
18 |
|
19 |
|
20 text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close> |
|
21 |
|
22 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool" |
|
23 for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a" |
|
24 where |
|
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)" |
|
27 |
|
28 lemma Rec_functional: "\<exists>!y::'a. Rec e r x y" for x :: 'n |
|
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 |
|
36 show "?R zero e" .. |
|
37 show "y = e" if "?R zero y" for y |
|
38 using that by cases simp_all |
|
39 qed |
|
40 next |
|
41 case (succ m) |
|
42 from \<open>\<exists>!y. ?R m y\<close> |
|
43 obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" |
|
44 by blast |
|
45 show "\<exists>!z. ?R (succ m) z" |
|
46 proof |
|
47 from y show "?R (succ m) (r m y)" .. |
|
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:) |
|
55 qed |
|
56 qed |
|
57 qed |
|
58 |
|
59 |
|
60 text \<open>\<^medskip> The recursion operator -- polymorphic!\<close> |
|
61 |
|
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)" |
|
64 |
|
65 lemma rec_eval: |
|
66 assumes Rec: "Rec e r x y" |
|
67 shows "rec e r x = y" |
|
68 unfolding rec_def |
|
69 using Rec_functional and Rec by (rule the1_equality) |
|
70 |
|
71 lemma rec_zero [simp]: "rec e r zero = e" |
|
72 proof (rule rec_eval) |
|
73 show "Rec e r zero e" .. |
|
74 qed |
|
75 |
|
76 lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)" |
|
77 proof (rule rec_eval) |
|
78 let ?R = "Rec e r" |
|
79 have "?R m (rec e r m)" |
|
80 unfolding rec_def using Rec_functional by (rule theI') |
|
81 then show "?R (succ m) (r m (rec e r m))" .. |
|
82 qed |
|
83 |
|
84 |
|
85 text \<open>\<^medskip> Example: addition (monomorphic)\<close> |
|
86 |
|
87 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" |
|
88 where "add m n = rec n (\<lambda>_ k. succ k) m" |
|
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 |
|
103 lemma "add (succ (succ (succ zero))) (succ (succ zero)) = |
|
104 succ (succ (succ (succ (succ zero))))" |
|
105 by simp |
|
106 |
|
107 |
|
108 text \<open>\<^medskip> Example: replication (polymorphic)\<close> |
|
109 |
|
110 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
111 where "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
|
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 |
|
123 text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close> |
|
124 |
|
125 interpretation peano 0 Suc |
|
126 proof |
|
127 fix m n |
|
128 show "Suc m \<noteq> 0" by simp |
|
129 show "Suc m = Suc n \<longleftrightarrow> m = n" by simp |
|
130 show "P n" |
|
131 if zero: "P 0" |
|
132 and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)" |
|
133 for P |
|
134 proof (induct n) |
|
135 case 0 |
|
136 show ?case by (rule zero) |
|
137 next |
|
138 case Suc |
|
139 then show ?case by (rule succ) |
|
140 qed |
|
141 qed |
|
142 |
|
143 end |