515
|
1 |
(* Title: ZF/ex/Primrec
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 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 |
open Primrec;
|
|
18 |
|
|
19 |
val pr_typechecks =
|
|
20 |
nat_typechecks @ list.intrs @
|
|
21 |
[lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
|
|
22 |
|
|
23 |
(** Useful special cases of evaluation ***)
|
|
24 |
|
|
25 |
val pr_ss = arith_ss
|
|
26 |
addsimps list.case_eqns
|
|
27 |
addsimps [list_rec_Nil, list_rec_Cons,
|
|
28 |
drop_0, drop_Nil, drop_succ_Cons,
|
|
29 |
map_Nil, map_Cons]
|
|
30 |
setsolver (type_auto_tac pr_typechecks);
|
|
31 |
|
|
32 |
goalw Primrec.thy [SC_def]
|
|
33 |
"!!x l. [| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
|
|
34 |
by (asm_simp_tac pr_ss 1);
|
|
35 |
val SC = result();
|
|
36 |
|
|
37 |
goalw Primrec.thy [CONST_def]
|
|
38 |
"!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
|
|
39 |
by (asm_simp_tac pr_ss 1);
|
|
40 |
val CONST = result();
|
|
41 |
|
|
42 |
goalw Primrec.thy [PROJ_def]
|
|
43 |
"!!l. [| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
|
|
44 |
by (asm_simp_tac pr_ss 1);
|
|
45 |
val PROJ_0 = result();
|
|
46 |
|
|
47 |
goalw Primrec.thy [COMP_def]
|
|
48 |
"!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
|
|
49 |
by (asm_simp_tac pr_ss 1);
|
|
50 |
val COMP_1 = result();
|
|
51 |
|
|
52 |
goalw Primrec.thy [PREC_def]
|
|
53 |
"!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
|
|
54 |
by (asm_simp_tac pr_ss 1);
|
|
55 |
val PREC_0 = result();
|
|
56 |
|
|
57 |
goalw Primrec.thy [PREC_def]
|
|
58 |
"!!l. [| x:nat; l: list(nat) |] ==> \
|
|
59 |
\ PREC(f,g) ` (Cons(succ(x),l)) = \
|
|
60 |
\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
|
|
61 |
by (asm_simp_tac pr_ss 1);
|
|
62 |
val PREC_succ = result();
|
|
63 |
|
|
64 |
(*** Inductive definition of the PR functions ***)
|
|
65 |
|
|
66 |
(* c: primrec ==> c: list(nat) -> nat *)
|
|
67 |
val primrec_into_fun = primrec.dom_subset RS subsetD;
|
|
68 |
|
|
69 |
val pr_ss = pr_ss
|
|
70 |
setsolver (type_auto_tac ([primrec_into_fun] @
|
|
71 |
pr_typechecks @ primrec.intrs));
|
|
72 |
|
|
73 |
goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
|
|
74 |
by (etac nat_induct 1);
|
|
75 |
by (ALLGOALS (asm_simp_tac pr_ss));
|
|
76 |
val ACK_in_primrec = result();
|
|
77 |
|
|
78 |
val ack_typechecks =
|
|
79 |
[ACK_in_primrec, primrec_into_fun RS apply_type,
|
|
80 |
add_type, list_add_type, nat_into_Ord] @
|
|
81 |
nat_typechecks @ list.intrs @ primrec.intrs;
|
|
82 |
|
|
83 |
(*strict typechecking for the Ackermann proof; instantiates no vars*)
|
|
84 |
fun tc_tac rls =
|
|
85 |
REPEAT
|
|
86 |
(SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
|
|
87 |
|
|
88 |
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j): nat";
|
|
89 |
by (tc_tac []);
|
|
90 |
val ack_type = result();
|
|
91 |
|
|
92 |
(** Ackermann's function cases **)
|
|
93 |
|
|
94 |
(*PROPERTY A 1*)
|
|
95 |
goalw Primrec.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
|
|
96 |
by (asm_simp_tac (pr_ss addsimps [SC]) 1);
|
|
97 |
val ack_0 = result();
|
|
98 |
|
|
99 |
(*PROPERTY A 2*)
|
|
100 |
goalw Primrec.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
|
|
101 |
by (asm_simp_tac (pr_ss addsimps [CONST,PREC_0]) 1);
|
|
102 |
val ack_succ_0 = result();
|
|
103 |
|
|
104 |
(*PROPERTY A 3*)
|
|
105 |
(*Could be proved in Primrec0, like the previous two cases, but using
|
|
106 |
primrec_into_fun makes type-checking easier!*)
|
|
107 |
goalw Primrec.thy [ACK_def]
|
|
108 |
"!!i j. [| i:nat; j:nat |] ==> \
|
|
109 |
\ ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
|
|
110 |
by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
|
|
111 |
val ack_succ_succ = result();
|
|
112 |
|
|
113 |
val ack_ss =
|
|
114 |
pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ,
|
|
115 |
ack_type, nat_into_Ord];
|
|
116 |
|
|
117 |
(*PROPERTY A 4*)
|
|
118 |
goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)";
|
|
119 |
by (etac nat_induct 1);
|
|
120 |
by (asm_simp_tac ack_ss 1);
|
|
121 |
by (rtac ballI 1);
|
|
122 |
by (eres_inst_tac [("n","j")] nat_induct 1);
|
|
123 |
by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
|
|
124 |
asm_simp_tac ack_ss] 1);
|
|
125 |
by (DO_GOAL [etac (succ_leI RS lt_trans1),
|
|
126 |
asm_simp_tac ack_ss] 1);
|
|
127 |
val lt_ack2_lemma = result();
|
|
128 |
val lt_ack2 = standard (lt_ack2_lemma RS bspec);
|
|
129 |
|
|
130 |
(*PROPERTY A 5-, the single-step lemma*)
|
|
131 |
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
|
|
132 |
by (etac nat_induct 1);
|
|
133 |
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [lt_ack2])));
|
|
134 |
val ack_lt_ack_succ2 = result();
|
|
135 |
|
|
136 |
(*PROPERTY A 5, monotonicity for < *)
|
|
137 |
goal Primrec.thy "!!i j k. [| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
|
|
138 |
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
|
|
139 |
by (etac succ_lt_induct 1);
|
|
140 |
by (assume_tac 1);
|
|
141 |
by (rtac lt_trans 2);
|
|
142 |
by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr_typechecks) 1));
|
|
143 |
val ack_lt_mono2 = result();
|
|
144 |
|
|
145 |
(*PROPERTY A 5', monotonicity for le *)
|
|
146 |
goal Primrec.thy
|
|
147 |
"!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)";
|
|
148 |
by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
|
|
149 |
by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
|
|
150 |
val ack_le_mono2 = result();
|
|
151 |
|
|
152 |
(*PROPERTY A 6*)
|
|
153 |
goal Primrec.thy
|
|
154 |
"!!i j. [| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
|
|
155 |
by (nat_ind_tac "j" [] 1);
|
|
156 |
by (ALLGOALS (asm_simp_tac ack_ss));
|
|
157 |
by (rtac ack_le_mono2 1);
|
|
158 |
by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
|
|
159 |
by (REPEAT (ares_tac (ack_typechecks) 1));
|
|
160 |
val ack2_le_ack1 = result();
|
|
161 |
|
|
162 |
(*PROPERTY A 7-, the single-step lemma*)
|
|
163 |
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
|
|
164 |
by (rtac (ack_lt_mono2 RS lt_trans2) 1);
|
|
165 |
by (rtac ack2_le_ack1 4);
|
|
166 |
by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr_typechecks) 1));
|
|
167 |
val ack_lt_ack_succ1 = result();
|
|
168 |
|
|
169 |
(*PROPERTY A 7, monotonicity for < *)
|
|
170 |
goal Primrec.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
|
|
171 |
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
|
|
172 |
by (etac succ_lt_induct 1);
|
|
173 |
by (assume_tac 1);
|
|
174 |
by (rtac lt_trans 2);
|
|
175 |
by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr_typechecks) 1));
|
|
176 |
val ack_lt_mono1 = result();
|
|
177 |
|
|
178 |
(*PROPERTY A 7', monotonicity for le *)
|
|
179 |
goal Primrec.thy
|
|
180 |
"!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
|
|
181 |
by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
|
|
182 |
by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
|
|
183 |
val ack_le_mono1 = result();
|
|
184 |
|
|
185 |
(*PROPERTY A 8*)
|
|
186 |
goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
|
|
187 |
by (etac nat_induct 1);
|
|
188 |
by (ALLGOALS (asm_simp_tac ack_ss));
|
|
189 |
val ack_1 = result();
|
|
190 |
|
|
191 |
(*PROPERTY A 9*)
|
|
192 |
goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
|
|
193 |
by (etac nat_induct 1);
|
|
194 |
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
|
|
195 |
val ack_2 = result();
|
|
196 |
|
|
197 |
(*PROPERTY A 10*)
|
|
198 |
goal Primrec.thy
|
|
199 |
"!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
|
|
200 |
\ ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
|
|
201 |
by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
|
|
202 |
by (asm_simp_tac ack_ss 1);
|
|
203 |
by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
|
|
204 |
by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
|
|
205 |
by (tc_tac []);
|
|
206 |
val ack_nest_bound = result();
|
|
207 |
|
|
208 |
(*PROPERTY A 11*)
|
|
209 |
goal Primrec.thy
|
|
210 |
"!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
|
|
211 |
\ ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
|
|
212 |
by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
|
|
213 |
by (asm_simp_tac (ack_ss addsimps [ack_2]) 1);
|
|
214 |
by (rtac (ack_nest_bound RS lt_trans2) 2);
|
|
215 |
by (asm_simp_tac ack_ss 5);
|
|
216 |
by (rtac (add_le_mono RS leI RS leI) 1);
|
|
217 |
by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
|
|
218 |
ack_typechecks) 1));
|
|
219 |
val ack_add_bound = result();
|
|
220 |
|
|
221 |
(*PROPERTY A 12. Article uses existential quantifier but the ALF proof
|
|
222 |
used k#+4. Quantified version must be nested EX k'. ALL i,j... *)
|
|
223 |
goal Primrec.thy
|
|
224 |
"!!i j k. [| i < ack(k,j); j:nat; k:nat |] ==> \
|
|
225 |
\ i#+j < ack(succ(succ(succ(succ(k)))), j)";
|
|
226 |
by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
|
|
227 |
by (rtac (ack_add_bound RS lt_trans2) 2);
|
|
228 |
by (asm_simp_tac (ack_ss addsimps [add_0_right]) 5);
|
|
229 |
by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
|
|
230 |
val ack_add_bound2 = result();
|
|
231 |
|
|
232 |
(*** MAIN RESULT ***)
|
|
233 |
|
|
234 |
val ack2_ss =
|
|
235 |
ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord];
|
|
236 |
|
|
237 |
goalw Primrec.thy [SC_def]
|
|
238 |
"!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))";
|
|
239 |
by (etac list.elim 1);
|
|
240 |
by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
|
|
241 |
by (asm_simp_tac (ack2_ss addsimps [ack_1, add_le_self]) 1);
|
|
242 |
val SC_case = result();
|
|
243 |
|
|
244 |
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
|
|
245 |
goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i < ack(i,j)";
|
|
246 |
by (etac nat_induct 1);
|
|
247 |
by (asm_simp_tac (ack_ss addsimps [nat_0_le]) 1);
|
|
248 |
by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
|
|
249 |
by (tc_tac []);
|
|
250 |
val lt_ack1 = result();
|
|
251 |
|
|
252 |
goalw Primrec.thy [CONST_def]
|
|
253 |
"!!l. [| l: list(nat); k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
|
|
254 |
by (asm_simp_tac (ack2_ss addsimps [lt_ack1]) 1);
|
|
255 |
val CONST_case = result();
|
|
256 |
|
|
257 |
goalw Primrec.thy [PROJ_def]
|
|
258 |
"!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
|
|
259 |
by (asm_simp_tac ack2_ss 1);
|
|
260 |
by (etac list.induct 1);
|
|
261 |
by (asm_simp_tac (ack2_ss addsimps [nat_0_le]) 1);
|
|
262 |
by (asm_simp_tac ack2_ss 1);
|
|
263 |
by (rtac ballI 1);
|
|
264 |
by (eres_inst_tac [("n","x")] natE 1);
|
|
265 |
by (asm_simp_tac (ack2_ss addsimps [add_le_self]) 1);
|
|
266 |
by (asm_simp_tac ack2_ss 1);
|
|
267 |
by (etac (bspec RS lt_trans2) 1);
|
|
268 |
by (rtac (add_le_self2 RS succ_leI) 2);
|
|
269 |
by (tc_tac []);
|
|
270 |
val PROJ_case_lemma = result();
|
|
271 |
val PROJ_case = PROJ_case_lemma RS bspec;
|
|
272 |
|
|
273 |
(** COMP case **)
|
|
274 |
|
|
275 |
goal Primrec.thy
|
|
276 |
"!!fs. fs : list({f: primrec . \
|
|
277 |
\ EX kf:nat. ALL l:list(nat). \
|
|
278 |
\ f`l < ack(kf, list_add(l))}) \
|
|
279 |
\ ==> EX k:nat. ALL l: list(nat). \
|
|
280 |
\ list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
|
|
281 |
by (etac list.induct 1);
|
|
282 |
by (DO_GOAL [res_inst_tac [("x","0")] bexI,
|
|
283 |
asm_simp_tac (ack2_ss addsimps [lt_ack1, nat_0_le]),
|
|
284 |
resolve_tac nat_typechecks] 1);
|
|
285 |
by (safe_tac ZF_cs);
|
|
286 |
by (asm_simp_tac ack2_ss 1);
|
|
287 |
by (rtac (ballI RS bexI) 1);
|
|
288 |
by (rtac (add_lt_mono RS lt_trans) 1);
|
|
289 |
by (REPEAT (FIRSTGOAL (etac bspec)));
|
|
290 |
by (rtac ack_add_bound 5);
|
|
291 |
by (tc_tac []);
|
|
292 |
val COMP_map_lemma = result();
|
|
293 |
|
|
294 |
goalw Primrec.thy [COMP_def]
|
|
295 |
"!!g. [| g: primrec; kg: nat; \
|
|
296 |
\ ALL l:list(nat). g`l < ack(kg, list_add(l)); \
|
|
297 |
\ fs : list({f: primrec . \
|
|
298 |
\ EX kf:nat. ALL l:list(nat). \
|
|
299 |
\ f`l < ack(kf, list_add(l))}) \
|
|
300 |
\ |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
|
|
301 |
by (asm_simp_tac ZF_ss 1);
|
|
302 |
by (forward_tac [list_CollectD] 1);
|
|
303 |
by (etac (COMP_map_lemma RS bexE) 1);
|
|
304 |
by (rtac (ballI RS bexI) 1);
|
|
305 |
by (etac (bspec RS lt_trans) 1);
|
|
306 |
by (rtac lt_trans 2);
|
|
307 |
by (rtac ack_nest_bound 3);
|
|
308 |
by (etac (bspec RS ack_lt_mono2) 2);
|
|
309 |
by (tc_tac [map_type]);
|
|
310 |
val COMP_case = result();
|
|
311 |
|
|
312 |
(** PREC case **)
|
|
313 |
|
|
314 |
goalw Primrec.thy [PREC_def]
|
|
315 |
"!!f g. [| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
|
|
316 |
\ ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
|
|
317 |
\ f: primrec; kf: nat; \
|
|
318 |
\ g: primrec; kg: nat; \
|
|
319 |
\ l: list(nat) \
|
|
320 |
\ |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
|
|
321 |
by (etac list.elim 1);
|
|
322 |
by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
|
|
323 |
by (asm_simp_tac ack2_ss 1);
|
|
324 |
by (etac ssubst 1); (*get rid of the needless assumption*)
|
|
325 |
by (eres_inst_tac [("n","a")] nat_induct 1);
|
|
326 |
(*base case*)
|
|
327 |
by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,
|
|
328 |
assume_tac, rtac (add_le_self RS ack_lt_mono1),
|
|
329 |
REPEAT o ares_tac (ack_typechecks)] 1);
|
|
330 |
(*ind step*)
|
|
331 |
by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
|
|
332 |
by (rtac (succ_leI RS lt_trans1) 1);
|
|
333 |
by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
|
|
334 |
by (etac bspec 2);
|
|
335 |
by (rtac (nat_le_refl RS add_le_mono) 1);
|
|
336 |
by (tc_tac []);
|
|
337 |
by (asm_simp_tac (ack2_ss addsimps [add_le_self2]) 1);
|
|
338 |
(*final part of the simplification*)
|
|
339 |
by (asm_simp_tac ack2_ss 1);
|
|
340 |
by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
|
|
341 |
by (etac ack_lt_mono2 5);
|
|
342 |
by (tc_tac []);
|
|
343 |
val PREC_case_lemma = result();
|
|
344 |
|
|
345 |
goal Primrec.thy
|
|
346 |
"!!f g. [| f: primrec; kf: nat; \
|
|
347 |
\ g: primrec; kg: nat; \
|
|
348 |
\ ALL l:list(nat). f`l < ack(kf, list_add(l)); \
|
|
349 |
\ ALL l:list(nat). g`l < ack(kg, list_add(l)) \
|
|
350 |
\ |] ==> EX k:nat. ALL l: list(nat). \
|
|
351 |
\ PREC(f,g)`l< ack(k, list_add(l))";
|
|
352 |
by (rtac (ballI RS bexI) 1);
|
|
353 |
by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
|
|
354 |
by (REPEAT
|
|
355 |
(SOMEGOAL
|
|
356 |
(FIRST' [test_assume_tac,
|
|
357 |
match_tac (ack_typechecks),
|
|
358 |
rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
|
|
359 |
val PREC_case = result();
|
|
360 |
|
|
361 |
goal Primrec.thy
|
|
362 |
"!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
|
|
363 |
by (etac primrec.induct 1);
|
|
364 |
by (safe_tac ZF_cs);
|
|
365 |
by (DEPTH_SOLVE
|
|
366 |
(ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
|
|
367 |
bexI, ballI] @ nat_typechecks) 1));
|
|
368 |
val ack_bounds_primrec = result();
|
|
369 |
|
|
370 |
goal Primrec.thy
|
|
371 |
"~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
|
|
372 |
by (rtac notI 1);
|
|
373 |
by (etac (ack_bounds_primrec RS bexE) 1);
|
|
374 |
by (rtac lt_irrefl 1);
|
|
375 |
by (dres_inst_tac [("x", "[x]")] bspec 1);
|
|
376 |
by (asm_simp_tac ack2_ss 1);
|
|
377 |
by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
|
|
378 |
val ack_not_primrec = result();
|
|
379 |
|