1 (* Title: HOL/ex/Primrec |
1 (* Title: HOL/ex/Primrec.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
5 |
6 Primitive Recursive Functions |
6 Primitive Recursive Functions. Demonstrates recursive definitions, |
7 |
7 the TFL package. |
8 Proof adopted from |
|
9 Nora Szasz, |
|
10 A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, |
|
11 In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. |
|
12 |
|
13 See also E. Mendelson, Introduction to Mathematical Logic. |
|
14 (Van Nostrand, 1964), page 250, exercise 11. |
|
15 |
|
16 Demonstrates recursive definitions, the TFL package |
|
17 *) |
8 *) |
18 |
9 |
19 Primrec = Main + |
10 header {* Primitive Recursive Functions *} |
20 |
11 |
21 consts ack :: "nat * nat => nat" |
12 theory Primrec = Main: |
22 recdef ack "less_than <*lex*> less_than" |
13 |
23 "ack (0,n) = Suc n" |
14 text {* |
24 "ack (Suc m,0) = (ack (m, 1))" |
15 Proof adopted from |
25 "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))" |
16 |
26 |
17 Nora Szasz, A Machine Checked Proof that Ackermann's Function is not |
27 consts list_add :: nat list => nat |
18 Primitive Recursive, In: Huet \& Plotkin, eds., Logical Environments |
|
19 (CUP, 1993), 317-338. |
|
20 |
|
21 See also E. Mendelson, Introduction to Mathematical Logic. (Van |
|
22 Nostrand, 1964), page 250, exercise 11. |
|
23 \medskip |
|
24 *} |
|
25 |
|
26 consts ack :: "nat * nat => nat" |
|
27 recdef ack "less_than <*lex*> less_than" |
|
28 "ack (0, n) = Suc n" |
|
29 "ack (Suc m, 0) = ack (m, 1)" |
|
30 "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))" |
|
31 |
|
32 consts list_add :: "nat list => nat" |
28 primrec |
33 primrec |
29 "list_add [] = 0" |
34 "list_add [] = 0" |
30 "list_add (m#ms) = m + list_add ms" |
35 "list_add (m # ms) = m + list_add ms" |
31 |
36 |
32 consts zeroHd :: nat list => nat |
37 consts zeroHd :: "nat list => nat" |
33 primrec |
38 primrec |
34 "zeroHd [] = 0" |
39 "zeroHd [] = 0" |
35 "zeroHd (m#ms) = m" |
40 "zeroHd (m # ms) = m" |
36 |
41 |
37 |
42 |
38 (** The set of primitive recursive functions of type nat list => nat **) |
43 text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *} |
39 consts |
44 |
40 PRIMREC :: (nat list => nat) set |
45 constdefs |
41 SC :: nat list => nat |
46 SC :: "nat list => nat" |
42 CONST :: [nat, nat list] => nat |
47 "SC l == Suc (zeroHd l)" |
43 PROJ :: [nat, nat list] => nat |
48 |
44 COMP :: [nat list => nat, (nat list => nat)list, nat list] => nat |
49 CONST :: "nat => nat list => nat" |
45 PREC :: [nat list => nat, nat list => nat, nat list] => nat |
50 "CONST k l == k" |
46 |
51 |
47 defs |
52 PROJ :: "nat => nat list => nat" |
48 |
53 "PROJ i l == zeroHd (drop i l)" |
49 SC_def "SC l == Suc (zeroHd l)" |
54 |
50 |
55 COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat" |
51 CONST_def "CONST k l == k" |
56 "COMP g fs l == g (map (\<lambda>f. f l) fs)" |
52 |
57 |
53 PROJ_def "PROJ i l == zeroHd (drop i l)" |
58 PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat" |
54 |
59 "PREC f g l == |
55 COMP_def "COMP g fs l == g (map (%f. f l) fs)" |
60 case l of |
56 |
61 [] => 0 |
57 (*Note that g is applied first to PREC f g y and then to y!*) |
62 | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x" |
58 PREC_def "PREC f g l == case l of |
63 -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *} |
59 [] => 0 |
64 |
60 | x#l' => nat_rec (f l') (%y r. g (r#y#l')) x" |
65 consts PRIMREC :: "(nat list => nat) set" |
61 |
|
62 |
|
63 inductive PRIMREC |
66 inductive PRIMREC |
64 intrs |
67 intros |
65 SC "SC : PRIMREC" |
68 SC: "SC \<in> PRIMREC" |
66 CONST "CONST k : PRIMREC" |
69 CONST: "CONST k \<in> PRIMREC" |
67 PROJ "PROJ i : PRIMREC" |
70 PROJ: "PROJ i \<in> PRIMREC" |
68 COMP "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC" |
71 COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC" |
69 PREC "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC" |
72 PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> PRIMREC" |
70 monos lists_mono |
73 |
|
74 |
|
75 text {* Useful special cases of evaluation *} |
|
76 |
|
77 lemma SC [simp]: "SC (x # l) = Suc x" |
|
78 apply (simp add: SC_def) |
|
79 done |
|
80 |
|
81 lemma CONST [simp]: "CONST k l = k" |
|
82 apply (simp add: CONST_def) |
|
83 done |
|
84 |
|
85 lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" |
|
86 apply (simp add: PROJ_def) |
|
87 done |
|
88 |
|
89 lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" |
|
90 apply (simp add: COMP_def) |
|
91 done |
|
92 |
|
93 lemma PREC_0 [simp]: "PREC f g (0 # l) = f l" |
|
94 apply (simp add: PREC_def) |
|
95 done |
|
96 |
|
97 lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" |
|
98 apply (simp add: PREC_def) |
|
99 done |
|
100 |
|
101 |
|
102 text {* PROPERTY A 4 *} |
|
103 |
|
104 lemma less_ack2 [iff]: "j < ack (i, j)" |
|
105 apply (induct i j rule: ack.induct) |
|
106 apply simp_all |
|
107 done |
|
108 |
|
109 |
|
110 text {* PROPERTY A 5-, the single-step lemma *} |
|
111 |
|
112 lemma ack_less_ack_Suc2 [iff]: "ack(i, j) < ack (i, Suc j)" |
|
113 apply (induct i j rule: ack.induct) |
|
114 apply simp_all |
|
115 done |
|
116 |
|
117 |
|
118 text {* PROPERTY A 5, monotonicity for @{text "<"} *} |
|
119 |
|
120 lemma ack_less_mono2: "j < k ==> ack (i, j) < ack (i, k)" |
|
121 apply (induct i k rule: ack.induct) |
|
122 apply simp_all |
|
123 apply (blast elim!: less_SucE intro: less_trans) |
|
124 done |
|
125 |
|
126 |
|
127 text {* PROPERTY A 5', monotonicity for @{text \<le>} *} |
|
128 |
|
129 lemma ack_le_mono2: "j \<le> k ==> ack (i, j) \<le> ack (i, k)" |
|
130 apply (simp add: order_le_less) |
|
131 apply (blast intro: ack_less_mono2) |
|
132 done |
|
133 |
|
134 |
|
135 text {* PROPERTY A 6 *} |
|
136 |
|
137 lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \<le> ack (Suc i, j)" |
|
138 apply (induct j) |
|
139 apply simp_all |
|
140 apply (blast intro: ack_le_mono2 less_ack2 [THEN Suc_leI] le_trans) |
|
141 done |
|
142 |
|
143 |
|
144 text {* PROPERTY A 7-, the single-step lemma *} |
|
145 |
|
146 lemma ack_less_ack_Suc1 [iff]: "ack (i, j) < ack (Suc i, j)" |
|
147 apply (blast intro: ack_less_mono2 less_le_trans) |
|
148 done |
|
149 |
|
150 |
|
151 text {* PROPERTY A 4'? Extra lemma needed for @{term CONST} case, constant functions *} |
|
152 |
|
153 lemma less_ack1 [iff]: "i < ack (i, j)" |
|
154 apply (induct i) |
|
155 apply simp_all |
|
156 apply (blast intro: Suc_leI le_less_trans) |
|
157 done |
|
158 |
|
159 |
|
160 text {* PROPERTY A 8 *} |
|
161 |
|
162 lemma ack_1 [simp]: "ack (1, j) = j + #2" |
|
163 apply (induct j) |
|
164 apply simp_all |
|
165 done |
|
166 |
|
167 |
|
168 text {* PROPERTY A 9. The unary @{term 1} and @{term 2} in @{term |
|
169 ack} is essential for the rewriting. *} |
|
170 |
|
171 lemma ack_2 [simp]: "ack (2, j) = #2 * j + #3" |
|
172 apply (induct j) |
|
173 apply simp_all |
|
174 done |
|
175 |
|
176 |
|
177 text {* PROPERTY A 7, monotonicity for @{text "<"} [not clear why |
|
178 @{thm [source] ack_1} is now needed first!] *} |
|
179 |
|
180 lemma ack_less_mono1_aux: "ack (i, k) < ack (Suc (i +i'), k)" |
|
181 apply (induct i k rule: ack.induct) |
|
182 apply simp_all |
|
183 prefer 2 |
|
184 apply (blast intro: less_trans ack_less_mono2) |
|
185 apply (induct_tac i' n rule: ack.induct) |
|
186 apply simp_all |
|
187 apply (blast intro: Suc_leI [THEN le_less_trans] ack_less_mono2) |
|
188 done |
|
189 |
|
190 lemma ack_less_mono1: "i < j ==> ack (i, k) < ack (j, k)" |
|
191 apply (drule less_imp_Suc_add) |
|
192 apply (blast intro!: ack_less_mono1_aux) |
|
193 done |
|
194 |
|
195 |
|
196 text {* PROPERTY A 7', monotonicity for @{text "\<le>"} *} |
|
197 |
|
198 lemma ack_le_mono1: "i \<le> j ==> ack (i, k) \<le> ack (j, k)" |
|
199 apply (simp add: order_le_less) |
|
200 apply (blast intro: ack_less_mono1) |
|
201 done |
|
202 |
|
203 |
|
204 text {* PROPERTY A 10 *} |
|
205 |
|
206 lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (#2 + (i1 + i2), j)" |
|
207 apply (simp add: numerals) |
|
208 apply (rule ack2_le_ack1 [THEN [2] less_le_trans]) |
|
209 apply simp |
|
210 apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans]) |
|
211 apply (rule ack_less_mono1 [THEN ack_less_mono2]) |
|
212 apply (simp add: le_imp_less_Suc le_add2) |
|
213 done |
|
214 |
|
215 |
|
216 text {* PROPERTY A 11 *} |
|
217 |
|
218 lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (#4 + (i1 + i2), j)" |
|
219 apply (rule_tac j = "ack (2, ack (i1 + i2, j))" in less_trans) |
|
220 prefer 2 |
|
221 apply (rule ack_nest_bound [THEN less_le_trans]) |
|
222 apply (simp add: Suc3_eq_add_3) |
|
223 apply simp |
|
224 apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1]) |
|
225 apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1]) |
|
226 apply auto |
|
227 done |
|
228 |
|
229 |
|
230 text {* PROPERTY A 12. Article uses existential quantifier but the ALF proof |
|
231 used @{text "k + 4"}. Quantified version must be nested @{text |
|
232 "\<exists>k'. \<forall>i j. ..."} *} |
|
233 |
|
234 lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (#4 + k, j)" |
|
235 apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans) |
|
236 prefer 2 |
|
237 apply (rule ack_add_bound [THEN less_le_trans]) |
|
238 apply simp |
|
239 apply (rule add_less_mono less_ack2 | assumption)+ |
|
240 done |
|
241 |
|
242 |
|
243 |
|
244 text {* Inductive definition of the @{term PR} functions *} |
|
245 |
|
246 text {* MAIN RESULT *} |
|
247 |
|
248 lemma SC_case: "SC l < ack (1, list_add l)" |
|
249 apply (unfold SC_def) |
|
250 apply (induct l) |
|
251 apply (simp_all add: le_add1 le_imp_less_Suc) |
|
252 done |
|
253 |
|
254 lemma CONST_case: "CONST k l < ack (k, list_add l)" |
|
255 apply simp |
|
256 done |
|
257 |
|
258 lemma PROJ_case [rule_format]: "\<forall>i. PROJ i l < ack (0, list_add l)" |
|
259 apply (simp add: PROJ_def) |
|
260 apply (induct l) |
|
261 apply simp_all |
|
262 apply (rule allI) |
|
263 apply (case_tac i) |
|
264 apply (simp (no_asm_simp) add: le_add1 le_imp_less_Suc) |
|
265 apply (simp (no_asm_simp)) |
|
266 apply (blast intro: less_le_trans intro!: le_add2) |
|
267 done |
|
268 |
|
269 |
|
270 text {* @{term COMP} case *} |
|
271 |
|
272 lemma COMP_map_aux: "fs \<in> lists (PRIMREC \<inter> {f. \<exists>kf. \<forall>l. f l < ack (kf, list_add l)}) |
|
273 ==> \<exists>k. \<forall>l. list_add (map (\<lambda>f. f l) fs) < ack (k, list_add l)" |
|
274 apply (erule lists.induct) |
|
275 apply (rule_tac x = 0 in exI) |
|
276 apply simp |
|
277 apply safe |
|
278 apply simp |
|
279 apply (rule exI) |
|
280 apply (blast intro: add_less_mono ack_add_bound less_trans) |
|
281 done |
|
282 |
|
283 lemma COMP_case: |
|
284 "\<forall>l. g l < ack (kg, list_add l) ==> |
|
285 fs \<in> lists(PRIMREC Int {f. \<exists>kf. \<forall>l. f l < ack(kf, list_add l)}) |
|
286 ==> \<exists>k. \<forall>l. COMP g fs l < ack(k, list_add l)" |
|
287 apply (unfold COMP_def) |
|
288 apply (frule Int_lower1 [THEN lists_mono, THEN subsetD]) |
|
289 apply (erule COMP_map_aux [THEN exE]) |
|
290 apply (rule exI) |
|
291 apply (rule allI) |
|
292 apply (drule spec)+ |
|
293 apply (erule less_trans) |
|
294 apply (blast intro: ack_less_mono2 ack_nest_bound less_trans) |
|
295 done |
|
296 |
|
297 |
|
298 text {* @{term PREC} case *} |
|
299 |
|
300 lemma PREC_case_aux: |
|
301 "\<forall>l. f l + list_add l < ack (kf, list_add l) ==> |
|
302 \<forall>l. g l + list_add l < ack (kg, list_add l) ==> |
|
303 PREC f g l + list_add l < ack (Suc (kf + kg), list_add l)" |
|
304 apply (unfold PREC_def) |
|
305 apply (case_tac l) |
|
306 apply simp_all |
|
307 apply (blast intro: less_trans) |
|
308 apply (erule ssubst) -- {* get rid of the needless assumption *} |
|
309 apply (induct_tac a) |
|
310 apply simp_all |
|
311 txt {* base case *} |
|
312 apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans) |
|
313 txt {* induction step *} |
|
314 apply (rule Suc_leI [THEN le_less_trans]) |
|
315 apply (rule le_refl [THEN add_le_mono, THEN le_less_trans]) |
|
316 prefer 2 |
|
317 apply (erule spec) |
|
318 apply (simp add: le_add2) |
|
319 txt {* final part of the simplification *} |
|
320 apply simp |
|
321 apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans]) |
|
322 apply (erule ack_less_mono2) |
|
323 done |
|
324 |
|
325 lemma PREC_case: |
|
326 "\<forall>l. f l < ack (kf, list_add l) ==> |
|
327 \<forall>l. g l < ack (kg, list_add l) ==> |
|
328 \<exists>k. \<forall>l. PREC f g l < ack (k, list_add l)" |
|
329 apply (rule exI) |
|
330 apply (rule allI) |
|
331 apply (rule le_less_trans [OF le_add1 PREC_case_aux]) |
|
332 apply (blast intro: ack_add_bound2)+ |
|
333 done |
|
334 |
|
335 lemma ack_bounds_PRIMREC: "f \<in> PRIMREC ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)" |
|
336 apply (erule PRIMREC.induct) |
|
337 apply (blast intro: SC_case CONST_case PROJ_case COMP_case PREC_case)+ |
|
338 done |
|
339 |
|
340 lemma ack_not_PRIMREC: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> PRIMREC" |
|
341 apply (rule notI) |
|
342 apply (erule ack_bounds_PRIMREC [THEN exE]) |
|
343 apply (rule less_irrefl) |
|
344 apply (drule_tac x = "[x]" in spec) |
|
345 apply simp |
|
346 done |
71 |
347 |
72 end |
348 end |