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