author | wenzelm |
Thu, 30 May 2013 20:38:50 +0200 | |
changeset 52252 | 81fcc11d8c65 |
parent 46546 | 42298c5d33b1 |
child 55415 | 05f5fdb8d093 |
permissions | -rw-r--r-- |
11024 | 1 |
(* Title: HOL/ex/Primrec.thy |
3335 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1997 University of Cambridge |
|
4 |
||
27626 | 5 |
Ackermann's Function and the |
6 |
Primitive Recursive Functions. |
|
3335 | 7 |
*) |
8 |
||
11024 | 9 |
header {* Primitive Recursive Functions *} |
10 |
||
16417 | 11 |
theory Primrec imports Main begin |
11024 | 12 |
|
13 |
text {* |
|
14 |
Proof adopted from |
|
15 |
||
16 |
Nora Szasz, A Machine Checked Proof that Ackermann's Function is not |
|
17 |
Primitive Recursive, In: Huet \& Plotkin, eds., Logical Environments |
|
18 |
(CUP, 1993), 317-338. |
|
19 |
||
20 |
See also E. Mendelson, Introduction to Mathematical Logic. (Van |
|
21 |
Nostrand, 1964), page 250, exercise 11. |
|
22 |
\medskip |
|
23 |
*} |
|
24 |
||
25 |
||
27626 | 26 |
subsection{* Ackermann's Function *} |
11024 | 27 |
|
27626 | 28 |
fun ack :: "nat => nat => nat" where |
29 |
"ack 0 n = Suc n" | |
|
30 |
"ack (Suc m) 0 = ack m 1" | |
|
31 |
"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)" |
|
11024 | 32 |
|
33 |
||
34 |
text {* PROPERTY A 4 *} |
|
35 |
||
27626 | 36 |
lemma less_ack2 [iff]: "j < ack i j" |
37 |
by (induct i j rule: ack.induct) simp_all |
|
11024 | 38 |
|
39 |
||
40 |
text {* PROPERTY A 5-, the single-step lemma *} |
|
41 |
||
27626 | 42 |
lemma ack_less_ack_Suc2 [iff]: "ack i j < ack i (Suc j)" |
43 |
by (induct i j rule: ack.induct) simp_all |
|
11024 | 44 |
|
45 |
||
46 |
text {* PROPERTY A 5, monotonicity for @{text "<"} *} |
|
47 |
||
27626 | 48 |
lemma ack_less_mono2: "j < k ==> ack i j < ack i k" |
49 |
using lift_Suc_mono_less[where f = "ack i"] |
|
50 |
by (metis ack_less_ack_Suc2) |
|
11024 | 51 |
|
52 |
||
53 |
text {* PROPERTY A 5', monotonicity for @{text \<le>} *} |
|
54 |
||
27626 | 55 |
lemma ack_le_mono2: "j \<le> k ==> ack i j \<le> ack i k" |
56 |
apply (simp add: order_le_less) |
|
57 |
apply (blast intro: ack_less_mono2) |
|
58 |
done |
|
3335 | 59 |
|
11024 | 60 |
|
61 |
text {* PROPERTY A 6 *} |
|
62 |
||
27626 | 63 |
lemma ack2_le_ack1 [iff]: "ack i (Suc j) \<le> ack (Suc i) j" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
64 |
proof (induct j) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
65 |
case 0 show ?case by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
66 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
67 |
case (Suc j) show ?case |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
68 |
by (auto intro!: ack_le_mono2) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
69 |
(metis Suc Suc_leI Suc_lessI less_ack2 linorder_not_less) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25157
diff
changeset
|
70 |
qed |
11024 | 71 |
|
72 |
||
73 |
text {* PROPERTY A 7-, the single-step lemma *} |
|
74 |
||
27626 | 75 |
lemma ack_less_ack_Suc1 [iff]: "ack i j < ack (Suc i) j" |
76 |
by (blast intro: ack_less_mono2 less_le_trans) |
|
11024 | 77 |
|
78 |
||
19676 | 79 |
text {* PROPERTY A 4'? Extra lemma needed for @{term CONSTANT} case, constant functions *} |
11024 | 80 |
|
27626 | 81 |
lemma less_ack1 [iff]: "i < ack i j" |
82 |
apply (induct i) |
|
83 |
apply simp_all |
|
84 |
apply (blast intro: Suc_leI le_less_trans) |
|
85 |
done |
|
11024 | 86 |
|
87 |
||
88 |
text {* PROPERTY A 8 *} |
|
89 |
||
27626 | 90 |
lemma ack_1 [simp]: "ack (Suc 0) j = j + 2" |
91 |
by (induct j) simp_all |
|
11024 | 92 |
|
93 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
94 |
text {* PROPERTY A 9. The unary @{text 1} and @{text 2} in @{term |
11024 | 95 |
ack} is essential for the rewriting. *} |
96 |
||
27626 | 97 |
lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3" |
98 |
by (induct j) simp_all |
|
3335 | 99 |
|
100 |
||
11024 | 101 |
text {* PROPERTY A 7, monotonicity for @{text "<"} [not clear why |
102 |
@{thm [source] ack_1} is now needed first!] *} |
|
103 |
||
27626 | 104 |
lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k" |
34055 | 105 |
proof (induct i k rule: ack.induct) |
106 |
case (1 n) show ?case |
|
107 |
by (simp, metis ack_less_ack_Suc1 less_ack2 less_trans_Suc) |
|
108 |
next |
|
109 |
case (2 m) thus ?case by simp |
|
110 |
next |
|
111 |
case (3 m n) thus ?case |
|
112 |
by (simp, blast intro: less_trans ack_less_mono2) |
|
113 |
qed |
|
11024 | 114 |
|
27626 | 115 |
lemma ack_less_mono1: "i < j ==> ack i k < ack j k" |
116 |
apply (drule less_imp_Suc_add) |
|
117 |
apply (blast intro!: ack_less_mono1_aux) |
|
118 |
done |
|
11024 | 119 |
|
120 |
||
121 |
text {* PROPERTY A 7', monotonicity for @{text "\<le>"} *} |
|
122 |
||
27626 | 123 |
lemma ack_le_mono1: "i \<le> j ==> ack i k \<le> ack j k" |
124 |
apply (simp add: order_le_less) |
|
125 |
apply (blast intro: ack_less_mono1) |
|
126 |
done |
|
11024 | 127 |
|
128 |
||
129 |
text {* PROPERTY A 10 *} |
|
130 |
||
27626 | 131 |
lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j" |
132 |
apply (simp add: numerals) |
|
133 |
apply (rule ack2_le_ack1 [THEN [2] less_le_trans]) |
|
134 |
apply simp |
|
135 |
apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans]) |
|
136 |
apply (rule ack_less_mono1 [THEN ack_less_mono2]) |
|
137 |
apply (simp add: le_imp_less_Suc le_add2) |
|
138 |
done |
|
11024 | 139 |
|
3335 | 140 |
|
11024 | 141 |
text {* PROPERTY A 11 *} |
3335 | 142 |
|
27626 | 143 |
lemma ack_add_bound: "ack i1 j + ack i2 j < ack (4 + (i1 + i2)) j" |
144 |
apply (rule less_trans [of _ "ack (Suc (Suc 0)) (ack (i1 + i2) j)"]) |
|
145 |
prefer 2 |
|
146 |
apply (rule ack_nest_bound [THEN less_le_trans]) |
|
147 |
apply (simp add: Suc3_eq_add_3) |
|
148 |
apply simp |
|
149 |
apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1]) |
|
150 |
apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1]) |
|
151 |
apply auto |
|
152 |
done |
|
11024 | 153 |
|
154 |
||
155 |
text {* PROPERTY A 12. Article uses existential quantifier but the ALF proof |
|
156 |
used @{text "k + 4"}. Quantified version must be nested @{text |
|
157 |
"\<exists>k'. \<forall>i j. ..."} *} |
|
3335 | 158 |
|
27626 | 159 |
lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j" |
160 |
apply (rule less_trans [of _ "ack k j + ack 0 j"]) |
|
46546 | 161 |
apply (blast intro: add_less_mono) |
27626 | 162 |
apply (rule ack_add_bound [THEN less_le_trans]) |
163 |
apply simp |
|
164 |
done |
|
165 |
||
166 |
||
167 |
subsection{*Primitive Recursive Functions*} |
|
168 |
||
169 |
primrec hd0 :: "nat list => nat" where |
|
170 |
"hd0 [] = 0" | |
|
171 |
"hd0 (m # ms) = m" |
|
11024 | 172 |
|
173 |
||
27626 | 174 |
text {* Inductive definition of the set of primitive recursive functions of type @{typ "nat list => nat"}. *} |
11024 | 175 |
|
27626 | 176 |
definition SC :: "nat list => nat" where |
177 |
"SC l = Suc (hd0 l)" |
|
178 |
||
179 |
definition CONSTANT :: "nat => nat list => nat" where |
|
180 |
"CONSTANT k l = k" |
|
181 |
||
182 |
definition PROJ :: "nat => nat list => nat" where |
|
183 |
"PROJ i l = hd0 (drop i l)" |
|
184 |
||
185 |
definition |
|
186 |
COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat" |
|
187 |
where "COMP g fs l = g (map (\<lambda>f. f l) fs)" |
|
188 |
||
189 |
definition PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat" |
|
190 |
where |
|
191 |
"PREC f g l = |
|
192 |
(case l of |
|
193 |
[] => 0 |
|
194 |
| x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)" |
|
195 |
-- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *} |
|
196 |
||
197 |
inductive PRIMREC :: "(nat list => nat) => bool" where |
|
198 |
SC: "PRIMREC SC" | |
|
199 |
CONSTANT: "PRIMREC (CONSTANT k)" | |
|
200 |
PROJ: "PRIMREC (PROJ i)" | |
|
201 |
COMP: "PRIMREC g ==> \<forall>f \<in> set fs. PRIMREC f ==> PRIMREC (COMP g fs)" | |
|
202 |
PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)" |
|
203 |
||
204 |
||
205 |
text {* Useful special cases of evaluation *} |
|
206 |
||
207 |
lemma SC [simp]: "SC (x # l) = Suc x" |
|
208 |
by (simp add: SC_def) |
|
209 |
||
210 |
lemma CONSTANT [simp]: "CONSTANT k l = k" |
|
211 |
by (simp add: CONSTANT_def) |
|
212 |
||
213 |
lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" |
|
214 |
by (simp add: PROJ_def) |
|
215 |
||
216 |
lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" |
|
217 |
by (simp add: COMP_def) |
|
218 |
||
219 |
lemma PREC_0 [simp]: "PREC f g (0 # l) = f l" |
|
220 |
by (simp add: PREC_def) |
|
221 |
||
222 |
lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" |
|
223 |
by (simp add: PREC_def) |
|
224 |
||
3335 | 225 |
|
11024 | 226 |
text {* MAIN RESULT *} |
227 |
||
27626 | 228 |
lemma SC_case: "SC l < ack 1 (listsum l)" |
229 |
apply (unfold SC_def) |
|
230 |
apply (induct l) |
|
231 |
apply (simp_all add: le_add1 le_imp_less_Suc) |
|
232 |
done |
|
11024 | 233 |
|
27626 | 234 |
lemma CONSTANT_case: "CONSTANT k l < ack k (listsum l)" |
235 |
by simp |
|
3335 | 236 |
|
27626 | 237 |
lemma PROJ_case: "PROJ i l < ack 0 (listsum l)" |
238 |
apply (simp add: PROJ_def) |
|
239 |
apply (induct l arbitrary:i) |
|
240 |
apply (auto simp add: drop_Cons split: nat.split) |
|
241 |
apply (blast intro: less_le_trans le_add2) |
|
242 |
done |
|
11024 | 243 |
|
244 |
||
245 |
text {* @{term COMP} case *} |
|
3335 | 246 |
|
27626 | 247 |
lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l)) |
248 |
==> \<exists>k. \<forall>l. listsum (map (\<lambda>f. f l) fs) < ack k (listsum l)" |
|
249 |
apply (induct fs) |
|
250 |
apply (rule_tac x = 0 in exI) |
|
251 |
apply simp |
|
252 |
apply simp |
|
253 |
apply (blast intro: add_less_mono ack_add_bound less_trans) |
|
254 |
done |
|
11024 | 255 |
|
256 |
lemma COMP_case: |
|
27626 | 257 |
"\<forall>l. g l < ack kg (listsum l) ==> |
258 |
\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l)) |
|
259 |
==> \<exists>k. \<forall>l. COMP g fs l < ack k (listsum l)" |
|
260 |
apply (unfold COMP_def) |
|
34055 | 261 |
apply (drule COMP_map_aux) |
262 |
apply (meson ack_less_mono2 ack_nest_bound less_trans) |
|
27626 | 263 |
done |
11024 | 264 |
|
265 |
||
266 |
text {* @{term PREC} case *} |
|
3335 | 267 |
|
11024 | 268 |
lemma PREC_case_aux: |
27626 | 269 |
"\<forall>l. f l + listsum l < ack kf (listsum l) ==> |
270 |
\<forall>l. g l + listsum l < ack kg (listsum l) ==> |
|
271 |
PREC f g l + listsum l < ack (Suc (kf + kg)) (listsum l)" |
|
272 |
apply (unfold PREC_def) |
|
273 |
apply (case_tac l) |
|
274 |
apply simp_all |
|
275 |
apply (blast intro: less_trans) |
|
276 |
apply (erule ssubst) -- {* get rid of the needless assumption *} |
|
277 |
apply (induct_tac a) |
|
278 |
apply simp_all |
|
279 |
txt {* base case *} |
|
280 |
apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans) |
|
281 |
txt {* induction step *} |
|
282 |
apply (rule Suc_leI [THEN le_less_trans]) |
|
283 |
apply (rule le_refl [THEN add_le_mono, THEN le_less_trans]) |
|
284 |
prefer 2 |
|
285 |
apply (erule spec) |
|
286 |
apply (simp add: le_add2) |
|
287 |
txt {* final part of the simplification *} |
|
288 |
apply simp |
|
289 |
apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans]) |
|
290 |
apply (erule ack_less_mono2) |
|
291 |
done |
|
11024 | 292 |
|
293 |
lemma PREC_case: |
|
27626 | 294 |
"\<forall>l. f l < ack kf (listsum l) ==> |
295 |
\<forall>l. g l < ack kg (listsum l) ==> |
|
296 |
\<exists>k. \<forall>l. PREC f g l < ack k (listsum l)" |
|
297 |
by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2) |
|
11024 | 298 |
|
27626 | 299 |
lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (listsum l)" |
300 |
apply (erule PRIMREC.induct) |
|
301 |
apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+ |
|
302 |
done |
|
11024 | 303 |
|
27626 | 304 |
theorem ack_not_PRIMREC: |
305 |
"\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack x x)" |
|
306 |
apply (rule notI) |
|
307 |
apply (erule ack_bounds_PRIMREC [THEN exE]) |
|
308 |
apply (rule less_irrefl [THEN notE]) |
|
309 |
apply (drule_tac x = "[x]" in spec) |
|
310 |
apply simp |
|
311 |
done |
|
3335 | 312 |
|
313 |
end |