author | wenzelm |
Sat, 26 Dec 2015 15:59:27 +0100 | |
changeset 61933 | cf58b5b794b2 |
parent 61343 | 5b5656a63bd6 |
child 63882 | 018998c00003 |
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 |
||
61343 | 9 |
section \<open>Primitive Recursive Functions\<close> |
11024 | 10 |
|
16417 | 11 |
theory Primrec imports Main begin |
11024 | 12 |
|
61343 | 13 |
text \<open> |
11024 | 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 |
|
61343 | 23 |
\<close> |
11024 | 24 |
|
25 |
||
61343 | 26 |
subsection\<open>Ackermann's Function\<close> |
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 |
||
61343 | 34 |
text \<open>PROPERTY A 4\<close> |
11024 | 35 |
|
27626 | 36 |
lemma less_ack2 [iff]: "j < ack i j" |
37 |
by (induct i j rule: ack.induct) simp_all |
|
11024 | 38 |
|
39 |
||
61343 | 40 |
text \<open>PROPERTY A 5-, the single-step lemma\<close> |
11024 | 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 |
||
61933 | 46 |
text \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close> |
11024 | 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 |
||
61933 | 53 |
text \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close> |
11024 | 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 |
|
61343 | 61 |
text \<open>PROPERTY A 6\<close> |
11024 | 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 |
||
61343 | 73 |
text \<open>PROPERTY A 7-, the single-step lemma\<close> |
11024 | 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 |
||
61343 | 79 |
text \<open>PROPERTY A 4'? Extra lemma needed for @{term CONSTANT} case, constant functions\<close> |
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 |
||
61343 | 88 |
text \<open>PROPERTY A 8\<close> |
11024 | 89 |
|
27626 | 90 |
lemma ack_1 [simp]: "ack (Suc 0) j = j + 2" |
91 |
by (induct j) simp_all |
|
11024 | 92 |
|
93 |
||
61933 | 94 |
text \<open>PROPERTY A 9. The unary \<open>1\<close> and \<open>2\<close> in @{term |
61343 | 95 |
ack} is essential for the rewriting.\<close> |
11024 | 96 |
|
27626 | 97 |
lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3" |
98 |
by (induct j) simp_all |
|
3335 | 99 |
|
100 |
||
61933 | 101 |
text \<open>PROPERTY A 7, monotonicity for \<open><\<close> [not clear why |
61343 | 102 |
@{thm [source] ack_1} is now needed first!]\<close> |
11024 | 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 |
||
61933 | 121 |
text \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close> |
11024 | 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 |
||
61343 | 129 |
text \<open>PROPERTY A 10\<close> |
11024 | 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 |
|
61343 | 141 |
text \<open>PROPERTY A 11\<close> |
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 |
||
61343 | 155 |
text \<open>PROPERTY A 12. Article uses existential quantifier but the ALF proof |
61933 | 156 |
used \<open>k + 4\<close>. Quantified version must be nested \<open>\<exists>k'. \<forall>i j. ...\<close>\<close> |
3335 | 157 |
|
27626 | 158 |
lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j" |
159 |
apply (rule less_trans [of _ "ack k j + ack 0 j"]) |
|
46546 | 160 |
apply (blast intro: add_less_mono) |
27626 | 161 |
apply (rule ack_add_bound [THEN less_le_trans]) |
162 |
apply simp |
|
163 |
done |
|
164 |
||
165 |
||
61343 | 166 |
subsection\<open>Primitive Recursive Functions\<close> |
27626 | 167 |
|
168 |
primrec hd0 :: "nat list => nat" where |
|
169 |
"hd0 [] = 0" | |
|
170 |
"hd0 (m # ms) = m" |
|
11024 | 171 |
|
172 |
||
61343 | 173 |
text \<open>Inductive definition of the set of primitive recursive functions of type @{typ "nat list => nat"}.\<close> |
11024 | 174 |
|
27626 | 175 |
definition SC :: "nat list => nat" where |
176 |
"SC l = Suc (hd0 l)" |
|
177 |
||
178 |
definition CONSTANT :: "nat => nat list => nat" where |
|
179 |
"CONSTANT k l = k" |
|
180 |
||
181 |
definition PROJ :: "nat => nat list => nat" where |
|
182 |
"PROJ i l = hd0 (drop i l)" |
|
183 |
||
184 |
definition |
|
185 |
COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat" |
|
186 |
where "COMP g fs l = g (map (\<lambda>f. f l) fs)" |
|
187 |
||
188 |
definition PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat" |
|
189 |
where |
|
190 |
"PREC f g l = |
|
191 |
(case l of |
|
192 |
[] => 0 |
|
55415 | 193 |
| x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)" |
61933 | 194 |
\<comment> \<open>Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}!\<close> |
27626 | 195 |
|
196 |
inductive PRIMREC :: "(nat list => nat) => bool" where |
|
197 |
SC: "PRIMREC SC" | |
|
198 |
CONSTANT: "PRIMREC (CONSTANT k)" | |
|
199 |
PROJ: "PRIMREC (PROJ i)" | |
|
200 |
COMP: "PRIMREC g ==> \<forall>f \<in> set fs. PRIMREC f ==> PRIMREC (COMP g fs)" | |
|
201 |
PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)" |
|
202 |
||
203 |
||
61343 | 204 |
text \<open>Useful special cases of evaluation\<close> |
27626 | 205 |
|
206 |
lemma SC [simp]: "SC (x # l) = Suc x" |
|
207 |
by (simp add: SC_def) |
|
208 |
||
209 |
lemma CONSTANT [simp]: "CONSTANT k l = k" |
|
210 |
by (simp add: CONSTANT_def) |
|
211 |
||
212 |
lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" |
|
213 |
by (simp add: PROJ_def) |
|
214 |
||
215 |
lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" |
|
216 |
by (simp add: COMP_def) |
|
217 |
||
218 |
lemma PREC_0 [simp]: "PREC f g (0 # l) = f l" |
|
219 |
by (simp add: PREC_def) |
|
220 |
||
221 |
lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" |
|
222 |
by (simp add: PREC_def) |
|
223 |
||
3335 | 224 |
|
61343 | 225 |
text \<open>MAIN RESULT\<close> |
11024 | 226 |
|
27626 | 227 |
lemma SC_case: "SC l < ack 1 (listsum l)" |
228 |
apply (unfold SC_def) |
|
229 |
apply (induct l) |
|
230 |
apply (simp_all add: le_add1 le_imp_less_Suc) |
|
231 |
done |
|
11024 | 232 |
|
27626 | 233 |
lemma CONSTANT_case: "CONSTANT k l < ack k (listsum l)" |
234 |
by simp |
|
3335 | 235 |
|
27626 | 236 |
lemma PROJ_case: "PROJ i l < ack 0 (listsum l)" |
237 |
apply (simp add: PROJ_def) |
|
238 |
apply (induct l arbitrary:i) |
|
239 |
apply (auto simp add: drop_Cons split: nat.split) |
|
240 |
apply (blast intro: less_le_trans le_add2) |
|
241 |
done |
|
11024 | 242 |
|
243 |
||
61343 | 244 |
text \<open>@{term COMP} case\<close> |
3335 | 245 |
|
27626 | 246 |
lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l)) |
247 |
==> \<exists>k. \<forall>l. listsum (map (\<lambda>f. f l) fs) < ack k (listsum l)" |
|
248 |
apply (induct fs) |
|
249 |
apply (rule_tac x = 0 in exI) |
|
250 |
apply simp |
|
251 |
apply simp |
|
252 |
apply (blast intro: add_less_mono ack_add_bound less_trans) |
|
253 |
done |
|
11024 | 254 |
|
255 |
lemma COMP_case: |
|
27626 | 256 |
"\<forall>l. g l < ack kg (listsum l) ==> |
257 |
\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l)) |
|
258 |
==> \<exists>k. \<forall>l. COMP g fs l < ack k (listsum l)" |
|
259 |
apply (unfold COMP_def) |
|
34055 | 260 |
apply (drule COMP_map_aux) |
261 |
apply (meson ack_less_mono2 ack_nest_bound less_trans) |
|
27626 | 262 |
done |
11024 | 263 |
|
264 |
||
61343 | 265 |
text \<open>@{term PREC} case\<close> |
3335 | 266 |
|
11024 | 267 |
lemma PREC_case_aux: |
27626 | 268 |
"\<forall>l. f l + listsum l < ack kf (listsum l) ==> |
269 |
\<forall>l. g l + listsum l < ack kg (listsum l) ==> |
|
270 |
PREC f g l + listsum l < ack (Suc (kf + kg)) (listsum l)" |
|
271 |
apply (unfold PREC_def) |
|
272 |
apply (case_tac l) |
|
273 |
apply simp_all |
|
274 |
apply (blast intro: less_trans) |
|
61933 | 275 |
apply (erule ssubst) \<comment> \<open>get rid of the needless assumption\<close> |
27626 | 276 |
apply (induct_tac a) |
277 |
apply simp_all |
|
61343 | 278 |
txt \<open>base case\<close> |
27626 | 279 |
apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans) |
61343 | 280 |
txt \<open>induction step\<close> |
27626 | 281 |
apply (rule Suc_leI [THEN le_less_trans]) |
282 |
apply (rule le_refl [THEN add_le_mono, THEN le_less_trans]) |
|
283 |
prefer 2 |
|
284 |
apply (erule spec) |
|
285 |
apply (simp add: le_add2) |
|
61343 | 286 |
txt \<open>final part of the simplification\<close> |
27626 | 287 |
apply simp |
288 |
apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans]) |
|
289 |
apply (erule ack_less_mono2) |
|
290 |
done |
|
11024 | 291 |
|
292 |
lemma PREC_case: |
|
27626 | 293 |
"\<forall>l. f l < ack kf (listsum l) ==> |
294 |
\<forall>l. g l < ack kg (listsum l) ==> |
|
295 |
\<exists>k. \<forall>l. PREC f g l < ack k (listsum l)" |
|
296 |
by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2) |
|
11024 | 297 |
|
27626 | 298 |
lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (listsum l)" |
299 |
apply (erule PRIMREC.induct) |
|
300 |
apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+ |
|
301 |
done |
|
11024 | 302 |
|
27626 | 303 |
theorem ack_not_PRIMREC: |
304 |
"\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack x x)" |
|
305 |
apply (rule notI) |
|
306 |
apply (erule ack_bounds_PRIMREC [THEN exE]) |
|
307 |
apply (rule less_irrefl [THEN notE]) |
|
308 |
apply (drule_tac x = "[x]" in spec) |
|
309 |
apply simp |
|
310 |
done |
|
3335 | 311 |
|
312 |
end |