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