|
1 (* Title: HOL/ex/Primrec |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Primitive Recursive Functions |
|
7 |
|
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 |
|
17 |
|
18 (** Useful special cases of evaluation ***) |
|
19 |
|
20 goalw thy [SC_def] "SC (x#l) = Suc x"; |
|
21 by (Asm_simp_tac 1); |
|
22 qed "SC"; |
|
23 |
|
24 goalw thy [CONST_def] "CONST k l = k"; |
|
25 by (Asm_simp_tac 1); |
|
26 qed "CONST"; |
|
27 |
|
28 goalw thy [PROJ_def] "PROJ(0) (x#l) = x"; |
|
29 by (Asm_simp_tac 1); |
|
30 qed "PROJ_0"; |
|
31 |
|
32 goalw thy [COMP_def] "COMP g [f] l = g [f l]"; |
|
33 by (Asm_simp_tac 1); |
|
34 qed "COMP_1"; |
|
35 |
|
36 goalw thy [PREC_def] "PREC f g (0#l) = f l"; |
|
37 by (Asm_simp_tac 1); |
|
38 qed "PREC_0"; |
|
39 |
|
40 goalw thy [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)"; |
|
41 by (Asm_simp_tac 1); |
|
42 qed "PREC_Suc"; |
|
43 |
|
44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; |
|
45 |
|
46 |
|
47 Addsimps ack.rules; |
|
48 |
|
49 (*PROPERTY A 4*) |
|
50 goal thy "j < ack(i,j)"; |
|
51 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
|
52 by (ALLGOALS Asm_simp_tac); |
|
53 by (ALLGOALS trans_tac); |
|
54 qed "less_ack2"; |
|
55 |
|
56 AddIffs [less_ack2]; |
|
57 |
|
58 (*PROPERTY A 5-, the single-step lemma*) |
|
59 goal thy "ack(i,j) < ack(i, Suc(j))"; |
|
60 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
|
61 by (ALLGOALS Asm_simp_tac); |
|
62 qed "ack_less_ack_Suc2"; |
|
63 |
|
64 AddIffs [ack_less_ack_Suc2]; |
|
65 |
|
66 (*PROPERTY A 5, monotonicity for < *) |
|
67 goal thy "j<k --> ack(i,j) < ack(i,k)"; |
|
68 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
|
69 by (ALLGOALS Asm_simp_tac); |
|
70 by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1); |
|
71 qed_spec_mp "ack_less_mono2"; |
|
72 |
|
73 (*PROPERTY A 5', monotonicity for<=*) |
|
74 goal thy "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)"; |
|
75 by (full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
|
76 by (blast_tac (!claset addIs [ack_less_mono2]) 1); |
|
77 qed "ack_le_mono2"; |
|
78 |
|
79 (*PROPERTY A 6*) |
|
80 goal thy "ack(i, Suc(j)) <= ack(Suc(i), j)"; |
|
81 by (induct_tac "j" 1); |
|
82 by (ALLGOALS Asm_simp_tac); |
|
83 by (blast_tac (!claset addIs [ack_le_mono2, less_ack2 RS Suc_leI, |
|
84 le_trans]) 1); |
|
85 qed "ack2_le_ack1"; |
|
86 |
|
87 AddIffs [ack2_le_ack1]; |
|
88 |
|
89 (*PROPERTY A 7-, the single-step lemma*) |
|
90 goal thy "ack(i,j) < ack(Suc(i),j)"; |
|
91 by (blast_tac (!claset addIs [ack_less_mono2, less_le_trans]) 1); |
|
92 qed "ack_less_ack_Suc1"; |
|
93 |
|
94 AddIffs [ack_less_ack_Suc1]; |
|
95 |
|
96 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) |
|
97 goal thy "i < ack(i,j)"; |
|
98 by (induct_tac "i" 1); |
|
99 by (ALLGOALS Asm_simp_tac); |
|
100 by (blast_tac (!claset addIs [Suc_leI, le_less_trans]) 1); |
|
101 qed "less_ack1"; |
|
102 AddIffs [less_ack1]; |
|
103 |
|
104 (*PROPERTY A 8*) |
|
105 goal thy "ack(1,j) = Suc(Suc(j))"; |
|
106 by (induct_tac "j" 1); |
|
107 by (ALLGOALS Asm_simp_tac); |
|
108 qed "ack_1"; |
|
109 Addsimps [ack_1]; |
|
110 |
|
111 (*PROPERTY A 9*) |
|
112 goal thy "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))"; |
|
113 by (induct_tac "j" 1); |
|
114 by (ALLGOALS Asm_simp_tac); |
|
115 qed "ack_2"; |
|
116 Addsimps [ack_2]; |
|
117 |
|
118 |
|
119 (*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*) |
|
120 goal thy "ack(i,k) < ack(Suc(i+i'),k)"; |
|
121 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
|
122 by (ALLGOALS Asm_full_simp_tac); |
|
123 by (blast_tac (!claset addIs [less_trans, ack_less_mono2]) 2); |
|
124 by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1); |
|
125 by (ALLGOALS Asm_simp_tac); |
|
126 by (blast_tac (!claset addIs [less_trans, ack_less_mono2]) 1); |
|
127 by (blast_tac (!claset addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); |
|
128 val lemma = result(); |
|
129 |
|
130 goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)"; |
|
131 be less_natE 1; |
|
132 by (blast_tac (!claset addSIs [lemma]) 1); |
|
133 qed "ack_less_mono1"; |
|
134 |
|
135 (*PROPERTY A 7', monotonicity for<=*) |
|
136 goal thy "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)"; |
|
137 by (full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
|
138 by (blast_tac (!claset addIs [ack_less_mono1]) 1); |
|
139 qed "ack_le_mono1"; |
|
140 |
|
141 (*PROPERTY A 10*) |
|
142 goal thy "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)"; |
|
143 by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1); |
|
144 by (Asm_simp_tac 1); |
|
145 by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1); |
|
146 by (rtac (ack_less_mono1 RS ack_less_mono2) 1); |
|
147 by (simp_tac (!simpset addsimps [le_imp_less_Suc, le_add2]) 1); |
|
148 qed "ack_nest_bound"; |
|
149 |
|
150 (*PROPERTY A 11*) |
|
151 goal thy "ack(i1,j) + ack(i2,j) < ack(Suc(Suc(Suc(Suc(i1+i2)))), j)"; |
|
152 by (res_inst_tac [("j", "ack(Suc(1), ack(i1 + i2, j))")] less_trans 1); |
|
153 by (Asm_simp_tac 1); |
|
154 by (rtac (ack_nest_bound RS less_le_trans) 2); |
|
155 by (Asm_simp_tac 2); |
|
156 by (blast_tac (!claset addSIs [le_add1, le_add2] |
|
157 addIs [le_imp_less_Suc, ack_le_mono1, le_SucI, |
|
158 add_le_mono]) 1); |
|
159 qed "ack_add_bound"; |
|
160 |
|
161 (*PROPERTY A 12. Article uses existential quantifier but the ALF proof |
|
162 used k+4. Quantified version must be nested EX k'. ALL i,j... *) |
|
163 goal thy "!!i j k. i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)"; |
|
164 by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1); |
|
165 by (rtac (ack_add_bound RS less_le_trans) 2); |
|
166 by (Asm_simp_tac 2); |
|
167 by (REPEAT (ares_tac ([add_less_mono, less_ack2]) 1)); |
|
168 qed "ack_add_bound2"; |
|
169 |
|
170 |
|
171 (*** Inductive definition of the PR functions ***) |
|
172 |
|
173 (*** MAIN RESULT ***) |
|
174 |
|
175 goalw thy [SC_def] "SC l < ack(1, list_add l)"; |
|
176 by (induct_tac "l" 1); |
|
177 by (ALLGOALS (simp_tac (!simpset addsimps [le_add1, le_imp_less_Suc]))); |
|
178 qed "SC_case"; |
|
179 |
|
180 goal thy "CONST k l < ack(k, list_add l)"; |
|
181 by (Simp_tac 1); |
|
182 qed "CONST_case"; |
|
183 |
|
184 goalw thy [PROJ_def] "ALL i. PROJ i l < ack(0, list_add l)"; |
|
185 by (Simp_tac 1); |
|
186 by (induct_tac "l" 1); |
|
187 by (ALLGOALS Asm_simp_tac); |
|
188 by (rtac allI 1); |
|
189 by (exhaust_tac "i" 1); |
|
190 by (asm_simp_tac (!simpset addsimps [le_add1, le_imp_less_Suc]) 1); |
|
191 by (Asm_simp_tac 1); |
|
192 by (blast_tac (!claset addIs [less_le_trans] |
|
193 addSIs [le_add2]) 1); |
|
194 qed_spec_mp "PROJ_case"; |
|
195 |
|
196 (** COMP case **) |
|
197 |
|
198 goal thy |
|
199 "!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
|
200 \ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; |
|
201 by (etac lists.induct 1); |
|
202 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); |
|
203 by (safe_tac (!claset)); |
|
204 by (Asm_simp_tac 1); |
|
205 by (blast_tac (!claset addIs [add_less_mono, ack_add_bound, less_trans]) 1); |
|
206 qed "COMP_map_lemma"; |
|
207 |
|
208 goalw thy [COMP_def] |
|
209 "!!g. [| ALL l. g l < ack(kg, list_add l); \ |
|
210 \ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ |
|
211 \ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)"; |
|
212 by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1); |
|
213 by (etac (COMP_map_lemma RS exE) 1); |
|
214 by (rtac exI 1); |
|
215 by (rtac allI 1); |
|
216 by (REPEAT (dtac spec 1)); |
|
217 by (etac less_trans 1); |
|
218 by (blast_tac (!claset addIs [ack_less_mono2, ack_nest_bound, less_trans]) 1); |
|
219 qed "COMP_case"; |
|
220 |
|
221 (** PREC case **) |
|
222 |
|
223 goalw thy [PREC_def] |
|
224 "!!f g. [| ALL l. f l + list_add l < ack(kf, list_add l); \ |
|
225 \ ALL l. g l + list_add l < ack(kg, list_add l) \ |
|
226 \ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)"; |
|
227 by (exhaust_tac "l" 1); |
|
228 by (ALLGOALS Asm_simp_tac); |
|
229 by (blast_tac (!claset addIs [less_trans]) 1); |
|
230 by (etac ssubst 1); (*get rid of the needless assumption*) |
|
231 by (induct_tac "a" 1); |
|
232 by (ALLGOALS Asm_simp_tac); |
|
233 (*base case*) |
|
234 by (blast_tac (!claset addIs [le_add1 RS le_imp_less_Suc RS ack_less_mono1, |
|
235 less_trans]) 1); |
|
236 (*induction step*) |
|
237 by (rtac (Suc_leI RS le_less_trans) 1); |
|
238 by (rtac (le_refl RS add_le_mono RS le_less_trans) 1); |
|
239 by (etac spec 2); |
|
240 by (asm_simp_tac (!simpset addsimps [le_add2]) 1); |
|
241 (*final part of the simplification*) |
|
242 by (Asm_simp_tac 1); |
|
243 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); |
|
244 by (etac ack_less_mono2 1); |
|
245 qed "PREC_case_lemma"; |
|
246 |
|
247 goal thy |
|
248 "!!f g. [| ALL l. f l < ack(kf, list_add l); \ |
|
249 \ ALL l. g l < ack(kg, list_add l) \ |
|
250 \ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; |
|
251 br exI 1; |
|
252 br allI 1; |
|
253 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); |
|
254 by (REPEAT (blast_tac (!claset addIs [ack_add_bound2]) 1)); |
|
255 qed "PREC_case"; |
|
256 |
|
257 goal thy "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)"; |
|
258 by (etac PRIMREC.induct 1); |
|
259 by (ALLGOALS |
|
260 (blast_tac (!claset addIs [SC_case, CONST_case, PROJ_case, COMP_case, |
|
261 PREC_case]))); |
|
262 qed "ack_bounds_PRIMREC"; |
|
263 |
|
264 goal thy "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC"; |
|
265 by (rtac notI 1); |
|
266 by (etac (ack_bounds_PRIMREC RS exE) 1); |
|
267 by (rtac less_irrefl 1); |
|
268 by (dres_inst_tac [("x", "[x]")] spec 1); |
|
269 by (Asm_full_simp_tac 1); |
|
270 qed "ack_not_PRIMREC"; |
|
271 |