author | wenzelm |
Mon, 11 Feb 2008 21:32:12 +0100 | |
changeset 26059 | b67a225b50fd |
parent 26056 | 6a0801279f4c |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
12560 | 1 |
(* Title: ZF/Induct/Primrec.thy |
12088 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
12610 | 5 |
*) |
12088 | 6 |
|
12610 | 7 |
header {* Primitive Recursive Functions: the inductive definition *} |
12088 | 8 |
|
16417 | 9 |
theory Primrec imports Main begin |
12560 | 10 |
|
12610 | 11 |
text {* |
12 |
Proof adopted from \cite{szasz}. |
|
13 |
||
14 |
See also \cite[page 250, exercise 11]{mendelson}. |
|
15 |
*} |
|
16 |
||
17 |
||
18 |
subsection {* Basic definitions *} |
|
19 |
||
24893 | 20 |
definition |
21 |
SC :: "i" where |
|
12610 | 22 |
"SC == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. succ(x), l)" |
12560 | 23 |
|
24893 | 24 |
definition |
25 |
CONSTANT :: "i=>i" where |
|
19676 | 26 |
"CONSTANT(k) == \<lambda>l \<in> list(nat). k" |
12560 | 27 |
|
24893 | 28 |
definition |
29 |
PROJ :: "i=>i" where |
|
12610 | 30 |
"PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. x, drop(i,l))" |
12560 | 31 |
|
24893 | 32 |
definition |
33 |
COMP :: "[i,i]=>i" where |
|
26059 | 34 |
"COMP(g,fs) == \<lambda>l \<in> list(nat). g ` map(\<lambda>f. f`l, fs)" |
12610 | 35 |
|
24893 | 36 |
definition |
37 |
PREC :: "[i,i]=>i" where |
|
12610 | 38 |
"PREC(f,g) == |
39 |
\<lambda>l \<in> list(nat). list_case(0, |
|
40 |
\<lambda>x xs. rec(x, f`xs, \<lambda>y r. g ` Cons(r, Cons(y, xs))), l)" |
|
41 |
-- {* Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}! *} |
|
12560 | 42 |
|
12088 | 43 |
consts |
12610 | 44 |
ACK :: "i=>i" |
12560 | 45 |
primrec |
12610 | 46 |
"ACK(0) = SC" |
19676 | 47 |
"ACK(succ(i)) = PREC (CONSTANT (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))" |
12560 | 48 |
|
24892 | 49 |
abbreviation |
50 |
ack :: "[i,i]=>i" where |
|
51 |
"ack(x,y) == ACK(x) ` [y]" |
|
12560 | 52 |
|
53 |
||
12610 | 54 |
text {* |
55 |
\medskip Useful special cases of evaluation. |
|
56 |
*} |
|
12560 | 57 |
|
58 |
lemma SC: "[| x \<in> nat; l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)" |
|
12610 | 59 |
by (simp add: SC_def) |
12560 | 60 |
|
19676 | 61 |
lemma CONSTANT: "l \<in> list(nat) ==> CONSTANT(k) ` l = k" |
62 |
by (simp add: CONSTANT_def) |
|
12560 | 63 |
|
64 |
lemma PROJ_0: "[| x \<in> nat; l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x" |
|
12610 | 65 |
by (simp add: PROJ_def) |
12560 | 66 |
|
67 |
lemma COMP_1: "l \<in> list(nat) ==> COMP(g,[f]) ` l = g` [f`l]" |
|
12610 | 68 |
by (simp add: COMP_def) |
12560 | 69 |
|
70 |
lemma PREC_0: "l \<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l" |
|
12610 | 71 |
by (simp add: PREC_def) |
12560 | 72 |
|
12610 | 73 |
lemma PREC_succ: |
74 |
"[| x \<in> nat; l \<in> list(nat) |] |
|
75 |
==> PREC(f,g) ` (Cons(succ(x),l)) = |
|
76 |
g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))" |
|
77 |
by (simp add: PREC_def) |
|
12560 | 78 |
|
79 |
||
12610 | 80 |
subsection {* Inductive definition of the PR functions *} |
81 |
||
12560 | 82 |
consts |
12610 | 83 |
prim_rec :: i |
12088 | 84 |
|
85 |
inductive |
|
12610 | 86 |
domains prim_rec \<subseteq> "list(nat)->nat" |
12560 | 87 |
intros |
88 |
"SC \<in> prim_rec" |
|
19676 | 89 |
"k \<in> nat ==> CONSTANT(k) \<in> prim_rec" |
12560 | 90 |
"i \<in> nat ==> PROJ(i) \<in> prim_rec" |
12610 | 91 |
"[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs) \<in> prim_rec" |
92 |
"[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g) \<in> prim_rec" |
|
93 |
monos list_mono |
|
19676 | 94 |
con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def |
12610 | 95 |
type_intros nat_typechecks list.intros |
26059 | 96 |
lam_type list_case_type drop_type map_type |
12610 | 97 |
apply_type rec_type |
12560 | 98 |
|
99 |
||
12610 | 100 |
lemma prim_rec_into_fun [TC]: "c \<in> prim_rec ==> c \<in> list(nat) -> nat" |
101 |
by (erule subsetD [OF prim_rec.dom_subset]) |
|
12560 | 102 |
|
103 |
lemmas [TC] = apply_type [OF prim_rec_into_fun] |
|
104 |
||
105 |
declare prim_rec.intros [TC] |
|
106 |
declare nat_into_Ord [TC] |
|
107 |
declare rec_type [TC] |
|
108 |
||
12610 | 109 |
lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i) \<in> prim_rec" |
18415 | 110 |
by (induct set: nat) simp_all |
12560 | 111 |
|
12610 | 112 |
lemma ack_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) \<in> nat" |
113 |
by auto |
|
12560 | 114 |
|
12610 | 115 |
|
116 |
subsection {* Ackermann's function cases *} |
|
12560 | 117 |
|
12610 | 118 |
lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)" |
119 |
-- {* PROPERTY A 1 *} |
|
120 |
by (simp add: SC) |
|
121 |
||
12560 | 122 |
lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)" |
12610 | 123 |
-- {* PROPERTY A 2 *} |
19676 | 124 |
by (simp add: CONSTANT PREC_0) |
12560 | 125 |
|
126 |
lemma ack_succ_succ: |
|
12610 | 127 |
"[| i\<in>nat; j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))" |
128 |
-- {* PROPERTY A 3 *} |
|
19676 | 129 |
by (simp add: CONSTANT PREC_succ COMP_1 PROJ_0) |
12560 | 130 |
|
12610 | 131 |
lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type |
132 |
and [simp del] = ACK.simps |
|
12560 | 133 |
|
134 |
||
18415 | 135 |
lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)" |
12610 | 136 |
-- {* PROPERTY A 4 *} |
20503 | 137 |
apply (induct i arbitrary: j set: nat) |
12610 | 138 |
apply simp |
139 |
apply (induct_tac j) |
|
140 |
apply (erule_tac [2] succ_leI [THEN lt_trans1]) |
|
141 |
apply (rule nat_0I [THEN nat_0_le, THEN lt_trans]) |
|
142 |
apply auto |
|
143 |
done |
|
12560 | 144 |
|
145 |
lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))" |
|
12610 | 146 |
-- {* PROPERTY A 5-, the single-step lemma *} |
18415 | 147 |
by (induct set: nat) (simp_all add: lt_ack2) |
12560 | 148 |
|
149 |
lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)" |
|
12610 | 150 |
-- {* PROPERTY A 5, monotonicity for @{text "<"} *} |
151 |
apply (frule lt_nat_in_nat, assumption) |
|
152 |
apply (erule succ_lt_induct) |
|
153 |
apply assumption |
|
154 |
apply (rule_tac [2] lt_trans) |
|
155 |
apply (auto intro: ack_lt_ack_succ2) |
|
156 |
done |
|
12560 | 157 |
|
158 |
lemma ack_le_mono2: "[|j\<le>k; i\<in>nat; k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)" |
|
12610 | 159 |
-- {* PROPERTY A 5', monotonicity for @{text \<le>} *} |
160 |
apply (rule_tac f = "\<lambda>j. ack (i,j) " in Ord_lt_mono_imp_le_mono) |
|
161 |
apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+ |
|
162 |
done |
|
12560 | 163 |
|
164 |
lemma ack2_le_ack1: |
|
12610 | 165 |
"[| i\<in>nat; j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)" |
166 |
-- {* PROPERTY A 6 *} |
|
167 |
apply (induct_tac j) |
|
168 |
apply simp_all |
|
169 |
apply (rule ack_le_mono2) |
|
170 |
apply (rule lt_ack2 [THEN succ_leI, THEN le_trans]) |
|
171 |
apply auto |
|
172 |
done |
|
12560 | 173 |
|
174 |
lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)" |
|
12610 | 175 |
-- {* PROPERTY A 7-, the single-step lemma *} |
176 |
apply (rule ack_lt_mono2 [THEN lt_trans2]) |
|
177 |
apply (rule_tac [4] ack2_le_ack1) |
|
178 |
apply auto |
|
179 |
done |
|
12560 | 180 |
|
181 |
lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)" |
|
12610 | 182 |
-- {* PROPERTY A 7, monotonicity for @{text "<"} *} |
183 |
apply (frule lt_nat_in_nat, assumption) |
|
184 |
apply (erule succ_lt_induct) |
|
185 |
apply assumption |
|
186 |
apply (rule_tac [2] lt_trans) |
|
187 |
apply (auto intro: ack_lt_ack_succ1) |
|
188 |
done |
|
12560 | 189 |
|
190 |
lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)" |
|
12610 | 191 |
-- {* PROPERTY A 7', monotonicity for @{text \<le>} *} |
192 |
apply (rule_tac f = "\<lambda>j. ack (j,k) " in Ord_lt_mono_imp_le_mono) |
|
193 |
apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+ |
|
194 |
done |
|
12560 | 195 |
|
196 |
lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))" |
|
12610 | 197 |
-- {* PROPERTY A 8 *} |
18415 | 198 |
by (induct set: nat) simp_all |
12560 | 199 |
|
200 |
lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))" |
|
12610 | 201 |
-- {* PROPERTY A 9 *} |
18415 | 202 |
by (induct set: nat) (simp_all add: ack_1) |
12560 | 203 |
|
204 |
lemma ack_nest_bound: |
|
12610 | 205 |
"[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |] |
206 |
==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)" |
|
207 |
-- {* PROPERTY A 10 *} |
|
208 |
apply (rule lt_trans2 [OF _ ack2_le_ack1]) |
|
209 |
apply simp |
|
210 |
apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1]) |
|
211 |
apply auto |
|
212 |
apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2]) |
|
213 |
done |
|
12560 | 214 |
|
215 |
lemma ack_add_bound: |
|
12610 | 216 |
"[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |] |
217 |
==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)" |
|
218 |
-- {* PROPERTY A 11 *} |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
219 |
apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans) |
12610 | 220 |
apply (simp add: ack_2) |
221 |
apply (rule_tac [2] ack_nest_bound [THEN lt_trans2]) |
|
222 |
apply (rule add_le_mono [THEN leI, THEN leI]) |
|
223 |
apply (auto intro: add_le_self add_le_self2 ack_le_mono1) |
|
224 |
done |
|
12560 | 225 |
|
226 |
lemma ack_add_bound2: |
|
12610 | 227 |
"[| i < ack(k,j); j \<in> nat; k \<in> nat |] |
12560 | 228 |
==> i#+j < ack(succ(succ(succ(succ(k)))), j)" |
12610 | 229 |
-- {* PROPERTY A 12. *} |
230 |
-- {* Article uses existential quantifier but the ALF proof used @{term "k#+#4"}. *} |
|
231 |
-- {* Quantified version must be nested @{text "\<exists>k'. \<forall>i,j \<dots>"}. *} |
|
232 |
apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans) |
|
233 |
apply (rule_tac [2] ack_add_bound [THEN lt_trans2]) |
|
234 |
apply (rule add_lt_mono) |
|
235 |
apply auto |
|
236 |
done |
|
12560 | 237 |
|
12610 | 238 |
|
239 |
subsection {* Main result *} |
|
12560 | 240 |
|
241 |
declare list_add_type [simp] |
|
242 |
||
243 |
lemma SC_case: "l \<in> list(nat) ==> SC ` l < ack(1, list_add(l))" |
|
12610 | 244 |
apply (unfold SC_def) |
245 |
apply (erule list.cases) |
|
246 |
apply (simp add: succ_iff) |
|
247 |
apply (simp add: ack_1 add_le_self) |
|
248 |
done |
|
12560 | 249 |
|
250 |
lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)" |
|
19676 | 251 |
-- {* PROPERTY A 4'? Extra lemma needed for @{text CONSTANT} case, constant functions. *} |
12610 | 252 |
apply (induct_tac i) |
253 |
apply (simp add: nat_0_le) |
|
254 |
apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1]) |
|
255 |
apply auto |
|
256 |
done |
|
12560 | 257 |
|
19676 | 258 |
lemma CONSTANT_case: |
259 |
"[| l \<in> list(nat); k \<in> nat |] ==> CONSTANT(k) ` l < ack(k, list_add(l))" |
|
260 |
by (simp add: CONSTANT_def lt_ack1) |
|
12560 | 261 |
|
12610 | 262 |
lemma PROJ_case [rule_format]: |
12560 | 263 |
"l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))" |
12610 | 264 |
apply (unfold PROJ_def) |
265 |
apply simp |
|
266 |
apply (erule list.induct) |
|
267 |
apply (simp add: nat_0_le) |
|
268 |
apply simp |
|
269 |
apply (rule ballI) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12610
diff
changeset
|
270 |
apply (erule_tac n = i in natE) |
12610 | 271 |
apply (simp add: add_le_self) |
272 |
apply simp |
|
273 |
apply (erule bspec [THEN lt_trans2]) |
|
274 |
apply (rule_tac [2] add_le_self2 [THEN succ_leI]) |
|
275 |
apply auto |
|
276 |
done |
|
12560 | 277 |
|
12610 | 278 |
text {* |
279 |
\medskip @{text COMP} case. |
|
280 |
*} |
|
12560 | 281 |
|
282 |
lemma COMP_map_lemma: |
|
12610 | 283 |
"fs \<in> list({f \<in> prim_rec. \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))}) |
284 |
==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). |
|
285 |
list_add(map(\<lambda>f. f ` l, fs)) < ack(k, list_add(l))" |
|
18415 | 286 |
apply (induct set: list) |
12610 | 287 |
apply (rule_tac x = 0 in bexI) |
288 |
apply (simp_all add: lt_ack1 nat_0_le) |
|
289 |
apply clarify |
|
290 |
apply (rule ballI [THEN bexI]) |
|
291 |
apply (rule add_lt_mono [THEN lt_trans]) |
|
292 |
apply (rule_tac [5] ack_add_bound) |
|
293 |
apply blast |
|
294 |
apply auto |
|
295 |
done |
|
12560 | 296 |
|
12610 | 297 |
lemma COMP_case: |
298 |
"[| kg\<in>nat; |
|
299 |
\<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)); |
|
300 |
fs \<in> list({f \<in> prim_rec . |
|
301 |
\<exists>kf \<in> nat. \<forall>l \<in> list(nat). |
|
12560 | 302 |
f`l < ack(kf, list_add(l))}) |] |
303 |
==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))" |
|
12610 | 304 |
apply (simp add: COMP_def) |
305 |
apply (frule list_CollectD) |
|
306 |
apply (erule COMP_map_lemma [THEN bexE]) |
|
307 |
apply (rule ballI [THEN bexI]) |
|
308 |
apply (erule bspec [THEN lt_trans]) |
|
309 |
apply (rule_tac [2] lt_trans) |
|
310 |
apply (rule_tac [3] ack_nest_bound) |
|
311 |
apply (erule_tac [2] bspec [THEN ack_lt_mono2]) |
|
312 |
apply auto |
|
313 |
done |
|
12560 | 314 |
|
12610 | 315 |
text {* |
316 |
\medskip @{text PREC} case. |
|
317 |
*} |
|
12560 | 318 |
|
12610 | 319 |
lemma PREC_case_lemma: |
320 |
"[| \<forall>l \<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); |
|
321 |
\<forall>l \<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); |
|
322 |
f \<in> prim_rec; kf\<in>nat; |
|
323 |
g \<in> prim_rec; kg\<in>nat; |
|
12560 | 324 |
l \<in> list(nat) |] |
325 |
==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))" |
|
12610 | 326 |
apply (unfold PREC_def) |
327 |
apply (erule list.cases) |
|
328 |
apply (simp add: lt_trans [OF nat_le_refl lt_ack2]) |
|
329 |
apply simp |
|
330 |
apply (erule ssubst) -- {* get rid of the needless assumption *} |
|
331 |
apply (induct_tac a) |
|
332 |
apply simp_all |
|
333 |
txt {* base case *} |
|
334 |
apply (rule lt_trans, erule bspec, assumption) |
|
335 |
apply (simp add: add_le_self [THEN ack_lt_mono1]) |
|
336 |
txt {* ind step *} |
|
337 |
apply (rule succ_leI [THEN lt_trans1]) |
|
338 |
apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1) |
|
339 |
apply (erule_tac [2] bspec) |
|
340 |
apply (rule nat_le_refl [THEN add_le_mono]) |
|
341 |
apply typecheck |
|
342 |
apply (simp add: add_le_self2) |
|
343 |
txt {* final part of the simplification *} |
|
344 |
apply simp |
|
345 |
apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1]) |
|
346 |
apply (erule_tac [4] ack_lt_mono2) |
|
347 |
apply auto |
|
348 |
done |
|
12560 | 349 |
|
350 |
lemma PREC_case: |
|
12610 | 351 |
"[| f \<in> prim_rec; kf\<in>nat; |
352 |
g \<in> prim_rec; kg\<in>nat; |
|
353 |
\<forall>l \<in> list(nat). f`l < ack(kf, list_add(l)); |
|
354 |
\<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)) |] |
|
355 |
==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))" |
|
356 |
apply (rule ballI [THEN bexI]) |
|
357 |
apply (rule lt_trans1 [OF add_le_self PREC_case_lemma]) |
|
358 |
apply typecheck |
|
359 |
apply (blast intro: ack_add_bound2 list_add_type)+ |
|
360 |
done |
|
12560 | 361 |
|
362 |
lemma ack_bounds_prim_rec: |
|
12610 | 363 |
"f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))" |
18415 | 364 |
apply (induct set: prim_rec) |
19676 | 365 |
apply (auto intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case) |
12610 | 366 |
done |
12560 | 367 |
|
12610 | 368 |
theorem ack_not_prim_rec: |
369 |
"(\<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. ack(x,x), l)) \<notin> prim_rec" |
|
370 |
apply (rule notI) |
|
371 |
apply (drule ack_bounds_prim_rec) |
|
372 |
apply force |
|
373 |
done |
|
12088 | 374 |
|
375 |
end |