|
1 (* Title: HOLCF/fix.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for fix.thy |
|
7 *) |
|
8 |
|
9 open Fix; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* derive inductive properties of iterate from primitive recursion *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val iterate_0 = prove_goal Fix.thy "iterate(0,F,x) = x" |
|
16 (fn prems => |
|
17 [ |
|
18 (resolve_tac (nat_recs iterate_def) 1) |
|
19 ]); |
|
20 |
|
21 val iterate_Suc = prove_goal Fix.thy "iterate(Suc(n),F,x) = F[iterate(n,F,x)]" |
|
22 (fn prems => |
|
23 [ |
|
24 (resolve_tac (nat_recs iterate_def) 1) |
|
25 ]); |
|
26 |
|
27 val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc]; |
|
28 |
|
29 val iterate_Suc2 = prove_goal Fix.thy "iterate(Suc(n),F,x) = iterate(n,F,F[x])" |
|
30 (fn prems => |
|
31 [ |
|
32 (nat_ind_tac "n" 1), |
|
33 (simp_tac iterate_ss 1), |
|
34 (asm_simp_tac iterate_ss 1) |
|
35 ]); |
|
36 |
|
37 (* ------------------------------------------------------------------------ *) |
|
38 (* the sequence of function itertaions is a chain *) |
|
39 (* This property is essential since monotonicity of iterate makes no sense *) |
|
40 (* ------------------------------------------------------------------------ *) |
|
41 |
|
42 val is_chain_iterate2 = prove_goalw Fix.thy [is_chain] |
|
43 " x << F[x] ==> is_chain(%i.iterate(i,F,x))" |
|
44 (fn prems => |
|
45 [ |
|
46 (cut_facts_tac prems 1), |
|
47 (strip_tac 1), |
|
48 (simp_tac iterate_ss 1), |
|
49 (nat_ind_tac "i" 1), |
|
50 (asm_simp_tac iterate_ss 1), |
|
51 (asm_simp_tac iterate_ss 1), |
|
52 (etac monofun_cfun_arg 1) |
|
53 ]); |
|
54 |
|
55 |
|
56 val is_chain_iterate = prove_goal Fix.thy |
|
57 "is_chain(%i.iterate(i,F,UU))" |
|
58 (fn prems => |
|
59 [ |
|
60 (rtac is_chain_iterate2 1), |
|
61 (rtac minimal 1) |
|
62 ]); |
|
63 |
|
64 |
|
65 (* ------------------------------------------------------------------------ *) |
|
66 (* Kleene's fixed point theorems for continuous functions in pointed *) |
|
67 (* omega cpo's *) |
|
68 (* ------------------------------------------------------------------------ *) |
|
69 |
|
70 |
|
71 val Ifix_eq = prove_goalw Fix.thy [Ifix_def] "Ifix(F)=F[Ifix(F)]" |
|
72 (fn prems => |
|
73 [ |
|
74 (rtac (contlub_cfun_arg RS ssubst) 1), |
|
75 (rtac is_chain_iterate 1), |
|
76 (rtac antisym_less 1), |
|
77 (rtac lub_mono 1), |
|
78 (rtac is_chain_iterate 1), |
|
79 (rtac ch2ch_fappR 1), |
|
80 (rtac is_chain_iterate 1), |
|
81 (rtac allI 1), |
|
82 (rtac (iterate_Suc RS subst) 1), |
|
83 (rtac (is_chain_iterate RS is_chainE RS spec) 1), |
|
84 (rtac is_lub_thelub 1), |
|
85 (rtac ch2ch_fappR 1), |
|
86 (rtac is_chain_iterate 1), |
|
87 (rtac ub_rangeI 1), |
|
88 (rtac allI 1), |
|
89 (rtac (iterate_Suc RS subst) 1), |
|
90 (rtac is_ub_thelub 1), |
|
91 (rtac is_chain_iterate 1) |
|
92 ]); |
|
93 |
|
94 |
|
95 val Ifix_least = prove_goalw Fix.thy [Ifix_def] "F[x]=x ==> Ifix(F) << x" |
|
96 (fn prems => |
|
97 [ |
|
98 (cut_facts_tac prems 1), |
|
99 (rtac is_lub_thelub 1), |
|
100 (rtac is_chain_iterate 1), |
|
101 (rtac ub_rangeI 1), |
|
102 (strip_tac 1), |
|
103 (nat_ind_tac "i" 1), |
|
104 (asm_simp_tac iterate_ss 1), |
|
105 (asm_simp_tac iterate_ss 1), |
|
106 (res_inst_tac [("t","x")] subst 1), |
|
107 (atac 1), |
|
108 (etac monofun_cfun_arg 1) |
|
109 ]); |
|
110 |
|
111 |
|
112 (* ------------------------------------------------------------------------ *) |
|
113 (* monotonicity and continuity of iterate *) |
|
114 (* ------------------------------------------------------------------------ *) |
|
115 |
|
116 val monofun_iterate = prove_goalw Fix.thy [monofun] "monofun(iterate(i))" |
|
117 (fn prems => |
|
118 [ |
|
119 (strip_tac 1), |
|
120 (nat_ind_tac "i" 1), |
|
121 (asm_simp_tac iterate_ss 1), |
|
122 (asm_simp_tac iterate_ss 1), |
|
123 (rtac (less_fun RS iffD2) 1), |
|
124 (rtac allI 1), |
|
125 (rtac monofun_cfun 1), |
|
126 (atac 1), |
|
127 (rtac (less_fun RS iffD1 RS spec) 1), |
|
128 (atac 1) |
|
129 ]); |
|
130 |
|
131 (* ------------------------------------------------------------------------ *) |
|
132 (* the following lemma uses contlub_cfun which itself is based on a *) |
|
133 (* diagonalisation lemma for continuous functions with two arguments. *) |
|
134 (* In this special case it is the application function fapp *) |
|
135 (* ------------------------------------------------------------------------ *) |
|
136 |
|
137 val contlub_iterate = prove_goalw Fix.thy [contlub] "contlub(iterate(i))" |
|
138 (fn prems => |
|
139 [ |
|
140 (strip_tac 1), |
|
141 (nat_ind_tac "i" 1), |
|
142 (asm_simp_tac iterate_ss 1), |
|
143 (rtac (lub_const RS thelubI RS sym) 1), |
|
144 (asm_simp_tac iterate_ss 1), |
|
145 (rtac ext 1), |
|
146 (rtac (thelub_fun RS ssubst) 1), |
|
147 (rtac is_chainI 1), |
|
148 (rtac allI 1), |
|
149 (rtac (less_fun RS iffD2) 1), |
|
150 (rtac allI 1), |
|
151 (rtac (is_chainE RS spec) 1), |
|
152 (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1), |
|
153 (rtac allI 1), |
|
154 (rtac monofun_fapp2 1), |
|
155 (atac 1), |
|
156 (rtac ch2ch_fun 1), |
|
157 (rtac (monofun_iterate RS ch2ch_monofun) 1), |
|
158 (atac 1), |
|
159 (rtac (thelub_fun RS ssubst) 1), |
|
160 (rtac (monofun_iterate RS ch2ch_monofun) 1), |
|
161 (atac 1), |
|
162 (rtac contlub_cfun 1), |
|
163 (atac 1), |
|
164 (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1) |
|
165 ]); |
|
166 |
|
167 |
|
168 val contX_iterate = prove_goal Fix.thy "contX(iterate(i))" |
|
169 (fn prems => |
|
170 [ |
|
171 (rtac monocontlub2contX 1), |
|
172 (rtac monofun_iterate 1), |
|
173 (rtac contlub_iterate 1) |
|
174 ]); |
|
175 |
|
176 (* ------------------------------------------------------------------------ *) |
|
177 (* a lemma about continuity of iterate in its third argument *) |
|
178 (* ------------------------------------------------------------------------ *) |
|
179 |
|
180 val monofun_iterate2 = prove_goal Fix.thy "monofun(iterate(n,F))" |
|
181 (fn prems => |
|
182 [ |
|
183 (rtac monofunI 1), |
|
184 (strip_tac 1), |
|
185 (nat_ind_tac "n" 1), |
|
186 (asm_simp_tac iterate_ss 1), |
|
187 (asm_simp_tac iterate_ss 1), |
|
188 (etac monofun_cfun_arg 1) |
|
189 ]); |
|
190 |
|
191 val contlub_iterate2 = prove_goal Fix.thy "contlub(iterate(n,F))" |
|
192 (fn prems => |
|
193 [ |
|
194 (rtac contlubI 1), |
|
195 (strip_tac 1), |
|
196 (nat_ind_tac "n" 1), |
|
197 (simp_tac iterate_ss 1), |
|
198 (simp_tac iterate_ss 1), |
|
199 (res_inst_tac [("t","iterate(n1, F, lub(range(%u. Y(u))))"), |
|
200 ("s","lub(range(%i. iterate(n1, F, Y(i))))")] ssubst 1), |
|
201 (atac 1), |
|
202 (rtac contlub_cfun_arg 1), |
|
203 (etac (monofun_iterate2 RS ch2ch_monofun) 1) |
|
204 ]); |
|
205 |
|
206 val contX_iterate2 = prove_goal Fix.thy "contX(iterate(n,F))" |
|
207 (fn prems => |
|
208 [ |
|
209 (rtac monocontlub2contX 1), |
|
210 (rtac monofun_iterate2 1), |
|
211 (rtac contlub_iterate2 1) |
|
212 ]); |
|
213 |
|
214 (* ------------------------------------------------------------------------ *) |
|
215 (* monotonicity and continuity of Ifix *) |
|
216 (* ------------------------------------------------------------------------ *) |
|
217 |
|
218 val monofun_Ifix = prove_goalw Fix.thy [monofun,Ifix_def] "monofun(Ifix)" |
|
219 (fn prems => |
|
220 [ |
|
221 (strip_tac 1), |
|
222 (rtac lub_mono 1), |
|
223 (rtac is_chain_iterate 1), |
|
224 (rtac is_chain_iterate 1), |
|
225 (rtac allI 1), |
|
226 (rtac (less_fun RS iffD1 RS spec) 1), |
|
227 (etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1) |
|
228 ]); |
|
229 |
|
230 |
|
231 (* ------------------------------------------------------------------------ *) |
|
232 (* since iterate is not monotone in its first argument, special lemmas must *) |
|
233 (* be derived for lubs in this argument *) |
|
234 (* ------------------------------------------------------------------------ *) |
|
235 |
|
236 val is_chain_iterate_lub = prove_goal Fix.thy |
|
237 "is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate(ia,Y(i),UU))))" |
|
238 (fn prems => |
|
239 [ |
|
240 (cut_facts_tac prems 1), |
|
241 (rtac is_chainI 1), |
|
242 (strip_tac 1), |
|
243 (rtac lub_mono 1), |
|
244 (rtac is_chain_iterate 1), |
|
245 (rtac is_chain_iterate 1), |
|
246 (strip_tac 1), |
|
247 (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS is_chainE |
|
248 RS spec) 1) |
|
249 ]); |
|
250 |
|
251 (* ------------------------------------------------------------------------ *) |
|
252 (* this exchange lemma is analog to the one for monotone functions *) |
|
253 (* observe that monotonicity is not really needed. The propagation of *) |
|
254 (* chains is the essential argument which is usually derived from monot. *) |
|
255 (* ------------------------------------------------------------------------ *) |
|
256 |
|
257 val contlub_Ifix_lemma1 = prove_goal Fix.thy |
|
258 "is_chain(Y) ==> iterate(n,lub(range(Y)),y) = lub(range(%i. iterate(n,Y(i),y)))" |
|
259 (fn prems => |
|
260 [ |
|
261 (cut_facts_tac prems 1), |
|
262 (rtac (thelub_fun RS subst) 1), |
|
263 (rtac (monofun_iterate RS ch2ch_monofun) 1), |
|
264 (atac 1), |
|
265 (rtac fun_cong 1), |
|
266 (rtac (contlub_iterate RS contlubE RS spec RS mp RS ssubst) 1), |
|
267 (atac 1), |
|
268 (rtac refl 1) |
|
269 ]); |
|
270 |
|
271 |
|
272 val ex_lub_iterate = prove_goal Fix.thy "is_chain(Y) ==>\ |
|
273 \ lub(range(%i. lub(range(%ia. iterate(i,Y(ia),UU))))) =\ |
|
274 \ lub(range(%i. lub(range(%ia. iterate(ia,Y(i),UU)))))" |
|
275 (fn prems => |
|
276 [ |
|
277 (cut_facts_tac prems 1), |
|
278 (rtac antisym_less 1), |
|
279 (rtac is_lub_thelub 1), |
|
280 (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1), |
|
281 (atac 1), |
|
282 (rtac is_chain_iterate 1), |
|
283 (rtac ub_rangeI 1), |
|
284 (strip_tac 1), |
|
285 (rtac lub_mono 1), |
|
286 (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1), |
|
287 (etac is_chain_iterate_lub 1), |
|
288 (strip_tac 1), |
|
289 (rtac is_ub_thelub 1), |
|
290 (rtac is_chain_iterate 1), |
|
291 (rtac is_lub_thelub 1), |
|
292 (etac is_chain_iterate_lub 1), |
|
293 (rtac ub_rangeI 1), |
|
294 (strip_tac 1), |
|
295 (rtac lub_mono 1), |
|
296 (rtac is_chain_iterate 1), |
|
297 (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1), |
|
298 (atac 1), |
|
299 (rtac is_chain_iterate 1), |
|
300 (strip_tac 1), |
|
301 (rtac is_ub_thelub 1), |
|
302 (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1) |
|
303 ]); |
|
304 |
|
305 |
|
306 val contlub_Ifix = prove_goalw Fix.thy [contlub,Ifix_def] "contlub(Ifix)" |
|
307 (fn prems => |
|
308 [ |
|
309 (strip_tac 1), |
|
310 (rtac (contlub_Ifix_lemma1 RS ext RS ssubst) 1), |
|
311 (atac 1), |
|
312 (etac ex_lub_iterate 1) |
|
313 ]); |
|
314 |
|
315 |
|
316 val contX_Ifix = prove_goal Fix.thy "contX(Ifix)" |
|
317 (fn prems => |
|
318 [ |
|
319 (rtac monocontlub2contX 1), |
|
320 (rtac monofun_Ifix 1), |
|
321 (rtac contlub_Ifix 1) |
|
322 ]); |
|
323 |
|
324 (* ------------------------------------------------------------------------ *) |
|
325 (* propagate properties of Ifix to its continuous counterpart *) |
|
326 (* ------------------------------------------------------------------------ *) |
|
327 |
|
328 val fix_eq = prove_goalw Fix.thy [fix_def] "fix[F]=F[fix[F]]" |
|
329 (fn prems => |
|
330 [ |
|
331 (asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1), |
|
332 (rtac Ifix_eq 1) |
|
333 ]); |
|
334 |
|
335 val fix_least = prove_goalw Fix.thy [fix_def] "F[x]=x ==> fix[F] << x" |
|
336 (fn prems => |
|
337 [ |
|
338 (cut_facts_tac prems 1), |
|
339 (asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1), |
|
340 (etac Ifix_least 1) |
|
341 ]); |
|
342 |
|
343 |
|
344 val fix_eq2 = prove_goal Fix.thy "f == fix[F] ==> f = F[f]" |
|
345 (fn prems => |
|
346 [ |
|
347 (rewrite_goals_tac prems), |
|
348 (rtac fix_eq 1) |
|
349 ]); |
|
350 |
|
351 val fix_eq3 = prove_goal Fix.thy "f == fix[F] ==> f[x] = F[f][x]" |
|
352 (fn prems => |
|
353 [ |
|
354 (rtac trans 1), |
|
355 (rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1), |
|
356 (rtac refl 1) |
|
357 ]); |
|
358 |
|
359 fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); |
|
360 |
|
361 val fix_eq4 = prove_goal Fix.thy "f = fix[F] ==> f = F[f]" |
|
362 (fn prems => |
|
363 [ |
|
364 (cut_facts_tac prems 1), |
|
365 (hyp_subst_tac 1), |
|
366 (rtac fix_eq 1) |
|
367 ]); |
|
368 |
|
369 val fix_eq5 = prove_goal Fix.thy "f = fix[F] ==> f[x] = F[f][x]" |
|
370 (fn prems => |
|
371 [ |
|
372 (rtac trans 1), |
|
373 (rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1), |
|
374 (rtac refl 1) |
|
375 ]); |
|
376 |
|
377 fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); |
|
378 |
|
379 fun fix_prover thy fixdef thm = prove_goal thy thm |
|
380 (fn prems => |
|
381 [ |
|
382 (rtac trans 1), |
|
383 (rtac (fixdef RS fix_eq4) 1), |
|
384 (rtac trans 1), |
|
385 (rtac beta_cfun 1), |
|
386 (contX_tacR 1), |
|
387 (rtac refl 1) |
|
388 ]); |
|
389 |
|
390 |
|
391 (* ------------------------------------------------------------------------ *) |
|
392 (* better access to definitions *) |
|
393 (* ------------------------------------------------------------------------ *) |
|
394 |
|
395 |
|
396 val Ifix_def2 = prove_goal Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))" |
|
397 (fn prems => |
|
398 [ |
|
399 (rtac ext 1), |
|
400 (rewrite_goals_tac [Ifix_def]), |
|
401 (rtac refl 1) |
|
402 ]); |
|
403 |
|
404 (* ------------------------------------------------------------------------ *) |
|
405 (* direct connection between fix and iteration without Ifix *) |
|
406 (* ------------------------------------------------------------------------ *) |
|
407 |
|
408 val fix_def2 = prove_goalw Fix.thy [fix_def] |
|
409 "fix[F] = lub(range(%i. iterate(i,F,UU)))" |
|
410 (fn prems => |
|
411 [ |
|
412 (fold_goals_tac [Ifix_def]), |
|
413 (asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1) |
|
414 ]); |
|
415 |
|
416 |
|
417 (* ------------------------------------------------------------------------ *) |
|
418 (* Lemmas about admissibility and fixed point induction *) |
|
419 (* ------------------------------------------------------------------------ *) |
|
420 |
|
421 (* ------------------------------------------------------------------------ *) |
|
422 (* access to definitions *) |
|
423 (* ------------------------------------------------------------------------ *) |
|
424 |
|
425 val adm_def2 = prove_goalw Fix.thy [adm_def] |
|
426 "adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))" |
|
427 (fn prems => |
|
428 [ |
|
429 (rtac refl 1) |
|
430 ]); |
|
431 |
|
432 val admw_def2 = prove_goalw Fix.thy [admw_def] |
|
433 "admw(P) = (!F.((!n.P(iterate(n,F,UU)))-->\ |
|
434 \ P(lub(range(%i.iterate(i,F,UU))))))" |
|
435 (fn prems => |
|
436 [ |
|
437 (rtac refl 1) |
|
438 ]); |
|
439 |
|
440 (* ------------------------------------------------------------------------ *) |
|
441 (* an admissible formula is also weak admissible *) |
|
442 (* ------------------------------------------------------------------------ *) |
|
443 |
|
444 val adm_impl_admw = prove_goalw Fix.thy [admw_def] "adm(P)==>admw(P)" |
|
445 (fn prems => |
|
446 [ |
|
447 (cut_facts_tac prems 1), |
|
448 (strip_tac 1), |
|
449 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
450 (atac 1), |
|
451 (rtac is_chain_iterate 1), |
|
452 (atac 1) |
|
453 ]); |
|
454 |
|
455 (* ------------------------------------------------------------------------ *) |
|
456 (* fixed point induction *) |
|
457 (* ------------------------------------------------------------------------ *) |
|
458 |
|
459 val fix_ind = prove_goal Fix.thy |
|
460 "[| adm(P);P(UU);!!x. P(x) ==> P(F[x])|] ==> P(fix[F])" |
|
461 (fn prems => |
|
462 [ |
|
463 (cut_facts_tac prems 1), |
|
464 (rtac (fix_def2 RS ssubst) 1), |
|
465 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
466 (atac 1), |
|
467 (rtac is_chain_iterate 1), |
|
468 (rtac allI 1), |
|
469 (nat_ind_tac "i" 1), |
|
470 (rtac (iterate_0 RS ssubst) 1), |
|
471 (atac 1), |
|
472 (rtac (iterate_Suc RS ssubst) 1), |
|
473 (resolve_tac prems 1), |
|
474 (atac 1) |
|
475 ]); |
|
476 |
|
477 (* ------------------------------------------------------------------------ *) |
|
478 (* computational induction for weak admissible formulae *) |
|
479 (* ------------------------------------------------------------------------ *) |
|
480 |
|
481 val wfix_ind = prove_goal Fix.thy |
|
482 "[| admw(P); !n. P(iterate(n,F,UU))|] ==> P(fix[F])" |
|
483 (fn prems => |
|
484 [ |
|
485 (cut_facts_tac prems 1), |
|
486 (rtac (fix_def2 RS ssubst) 1), |
|
487 (rtac (admw_def2 RS iffD1 RS spec RS mp) 1), |
|
488 (atac 1), |
|
489 (rtac allI 1), |
|
490 (etac spec 1) |
|
491 ]); |
|
492 |
|
493 (* ------------------------------------------------------------------------ *) |
|
494 (* for chain-finite (easy) types every formula is admissible *) |
|
495 (* ------------------------------------------------------------------------ *) |
|
496 |
|
497 val adm_max_in_chain = prove_goalw Fix.thy [adm_def] |
|
498 "!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y)) ==> adm(P::'a=>bool)" |
|
499 (fn prems => |
|
500 [ |
|
501 (cut_facts_tac prems 1), |
|
502 (strip_tac 1), |
|
503 (rtac exE 1), |
|
504 (rtac mp 1), |
|
505 (etac spec 1), |
|
506 (atac 1), |
|
507 (rtac (lub_finch1 RS thelubI RS ssubst) 1), |
|
508 (atac 1), |
|
509 (atac 1), |
|
510 (etac spec 1) |
|
511 ]); |
|
512 |
|
513 |
|
514 val adm_chain_finite = prove_goalw Fix.thy [chain_finite_def] |
|
515 "chain_finite(x::'a) ==> adm(P::'a=>bool)" |
|
516 (fn prems => |
|
517 [ |
|
518 (cut_facts_tac prems 1), |
|
519 (etac adm_max_in_chain 1) |
|
520 ]); |
|
521 |
|
522 (* ------------------------------------------------------------------------ *) |
|
523 (* flat types are chain_finite *) |
|
524 (* ------------------------------------------------------------------------ *) |
|
525 |
|
526 val flat_imp_chain_finite = prove_goalw Fix.thy [flat_def,chain_finite_def] |
|
527 "flat(x::'a)==>chain_finite(x::'a)" |
|
528 (fn prems => |
|
529 [ |
|
530 (rewrite_goals_tac [max_in_chain_def]), |
|
531 (cut_facts_tac prems 1), |
|
532 (strip_tac 1), |
|
533 (res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1), |
|
534 (res_inst_tac [("x","0")] exI 1), |
|
535 (strip_tac 1), |
|
536 (rtac trans 1), |
|
537 (etac spec 1), |
|
538 (rtac sym 1), |
|
539 (etac spec 1), |
|
540 (rtac (chain_mono2 RS exE) 1), |
|
541 (fast_tac HOL_cs 1), |
|
542 (atac 1), |
|
543 (res_inst_tac [("x","Suc(x)")] exI 1), |
|
544 (strip_tac 1), |
|
545 (rtac disjE 1), |
|
546 (atac 3), |
|
547 (rtac mp 1), |
|
548 (dtac spec 1), |
|
549 (etac spec 1), |
|
550 (etac (le_imp_less_or_eq RS disjE) 1), |
|
551 (etac (chain_mono RS mp) 1), |
|
552 (atac 1), |
|
553 (hyp_subst_tac 1), |
|
554 (rtac refl_less 1), |
|
555 (res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1), |
|
556 (atac 2), |
|
557 (rtac mp 1), |
|
558 (etac spec 1), |
|
559 (asm_simp_tac nat_ss 1) |
|
560 ]); |
|
561 |
|
562 |
|
563 val adm_flat = flat_imp_chain_finite RS adm_chain_finite; |
|
564 (* flat(?x::?'a) ==> adm(?P::?'a => bool) *) |
|
565 |
|
566 val flat_void = prove_goalw Fix.thy [flat_def] "flat(UU::void)" |
|
567 (fn prems => |
|
568 [ |
|
569 (strip_tac 1), |
|
570 (rtac disjI1 1), |
|
571 (rtac unique_void2 1) |
|
572 ]); |
|
573 |
|
574 (* ------------------------------------------------------------------------ *) |
|
575 (* continuous isomorphisms are strict *) |
|
576 (* a prove for embedding projection pairs is similar *) |
|
577 (* ------------------------------------------------------------------------ *) |
|
578 |
|
579 val iso_strict = prove_goal Fix.thy |
|
580 "!!f g.[|!y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \ |
|
581 \ ==> f[UU]=UU & g[UU]=UU" |
|
582 (fn prems => |
|
583 [ |
|
584 (rtac conjI 1), |
|
585 (rtac UU_I 1), |
|
586 (res_inst_tac [("s","f[g[UU::'b]]"),("t","UU::'b")] subst 1), |
|
587 (etac spec 1), |
|
588 (rtac (minimal RS monofun_cfun_arg) 1), |
|
589 (rtac UU_I 1), |
|
590 (res_inst_tac [("s","g[f[UU::'a]]"),("t","UU::'a")] subst 1), |
|
591 (etac spec 1), |
|
592 (rtac (minimal RS monofun_cfun_arg) 1) |
|
593 ]); |
|
594 |
|
595 |
|
596 val isorep_defined = prove_goal Fix.thy |
|
597 "[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> rep[z]~=UU" |
|
598 (fn prems => |
|
599 [ |
|
600 (cut_facts_tac prems 1), |
|
601 (etac swap 1), |
|
602 (dtac notnotD 1), |
|
603 (dres_inst_tac [("f","abs")] cfun_arg_cong 1), |
|
604 (etac box_equals 1), |
|
605 (fast_tac HOL_cs 1), |
|
606 (etac (iso_strict RS conjunct1) 1), |
|
607 (atac 1) |
|
608 ]); |
|
609 |
|
610 val isoabs_defined = prove_goal Fix.thy |
|
611 "[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> abs[z]~=UU" |
|
612 (fn prems => |
|
613 [ |
|
614 (cut_facts_tac prems 1), |
|
615 (etac swap 1), |
|
616 (dtac notnotD 1), |
|
617 (dres_inst_tac [("f","rep")] cfun_arg_cong 1), |
|
618 (etac box_equals 1), |
|
619 (fast_tac HOL_cs 1), |
|
620 (etac (iso_strict RS conjunct2) 1), |
|
621 (atac 1) |
|
622 ]); |
|
623 |
|
624 (* ------------------------------------------------------------------------ *) |
|
625 (* propagation of flatness and chainfiniteness by continuous isomorphisms *) |
|
626 (* ------------------------------------------------------------------------ *) |
|
627 |
|
628 val chfin2chfin = prove_goalw Fix.thy [chain_finite_def] |
|
629 "!!f g.[|chain_finite(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \ |
|
630 \ ==> chain_finite(y::'b)" |
|
631 (fn prems => |
|
632 [ |
|
633 (rewrite_goals_tac [max_in_chain_def]), |
|
634 (strip_tac 1), |
|
635 (rtac exE 1), |
|
636 (res_inst_tac [("P","is_chain(%i.g[Y(i)])")] mp 1), |
|
637 (etac spec 1), |
|
638 (etac ch2ch_fappR 1), |
|
639 (rtac exI 1), |
|
640 (strip_tac 1), |
|
641 (res_inst_tac [("s","f[g[Y(x)]]"),("t","Y(x)")] subst 1), |
|
642 (etac spec 1), |
|
643 (res_inst_tac [("s","f[g[Y(j)]]"),("t","Y(j)")] subst 1), |
|
644 (etac spec 1), |
|
645 (rtac cfun_arg_cong 1), |
|
646 (rtac mp 1), |
|
647 (etac spec 1), |
|
648 (atac 1) |
|
649 ]); |
|
650 |
|
651 val flat2flat = prove_goalw Fix.thy [flat_def] |
|
652 "!!f g.[|flat(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \ |
|
653 \ ==> flat(y::'b)" |
|
654 (fn prems => |
|
655 [ |
|
656 (strip_tac 1), |
|
657 (rtac disjE 1), |
|
658 (res_inst_tac [("P","g[x]<<g[y]")] mp 1), |
|
659 (etac monofun_cfun_arg 2), |
|
660 (dtac spec 1), |
|
661 (etac spec 1), |
|
662 (rtac disjI1 1), |
|
663 (rtac trans 1), |
|
664 (res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1), |
|
665 (etac spec 1), |
|
666 (etac cfun_arg_cong 1), |
|
667 (rtac (iso_strict RS conjunct1) 1), |
|
668 (atac 1), |
|
669 (atac 1), |
|
670 (rtac disjI2 1), |
|
671 (res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1), |
|
672 (etac spec 1), |
|
673 (res_inst_tac [("s","f[g[y]]"),("t","y")] subst 1), |
|
674 (etac spec 1), |
|
675 (etac cfun_arg_cong 1) |
|
676 ]); |
|
677 |
|
678 (* ------------------------------------------------------------------------ *) |
|
679 (* admissibility of special formulae and propagation *) |
|
680 (* ------------------------------------------------------------------------ *) |
|
681 |
|
682 val adm_less = prove_goalw Fix.thy [adm_def] |
|
683 "[|contX(u);contX(v)|]==> adm(%x.u(x)<<v(x))" |
|
684 (fn prems => |
|
685 [ |
|
686 (cut_facts_tac prems 1), |
|
687 (strip_tac 1), |
|
688 (etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1), |
|
689 (atac 1), |
|
690 (etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1), |
|
691 (atac 1), |
|
692 (rtac lub_mono 1), |
|
693 (cut_facts_tac prems 1), |
|
694 (etac (contX2mono RS ch2ch_monofun) 1), |
|
695 (atac 1), |
|
696 (cut_facts_tac prems 1), |
|
697 (etac (contX2mono RS ch2ch_monofun) 1), |
|
698 (atac 1), |
|
699 (atac 1) |
|
700 ]); |
|
701 |
|
702 val adm_conj = prove_goal Fix.thy |
|
703 "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))" |
|
704 (fn prems => |
|
705 [ |
|
706 (cut_facts_tac prems 1), |
|
707 (rtac (adm_def2 RS iffD2) 1), |
|
708 (strip_tac 1), |
|
709 (rtac conjI 1), |
|
710 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
711 (atac 1), |
|
712 (atac 1), |
|
713 (fast_tac HOL_cs 1), |
|
714 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
715 (atac 1), |
|
716 (atac 1), |
|
717 (fast_tac HOL_cs 1) |
|
718 ]); |
|
719 |
|
720 val adm_cong = prove_goal Fix.thy |
|
721 "(!x. P(x) = Q(x)) ==> adm(P)=adm(Q)" |
|
722 (fn prems => |
|
723 [ |
|
724 (cut_facts_tac prems 1), |
|
725 (res_inst_tac [("s","P"),("t","Q")] subst 1), |
|
726 (rtac refl 2), |
|
727 (rtac ext 1), |
|
728 (etac spec 1) |
|
729 ]); |
|
730 |
|
731 val adm_not_free = prove_goalw Fix.thy [adm_def] "adm(%x.t)" |
|
732 (fn prems => |
|
733 [ |
|
734 (fast_tac HOL_cs 1) |
|
735 ]); |
|
736 |
|
737 val adm_not_less = prove_goalw Fix.thy [adm_def] |
|
738 "contX(t) ==> adm(%x.~ t(x) << u)" |
|
739 (fn prems => |
|
740 [ |
|
741 (cut_facts_tac prems 1), |
|
742 (strip_tac 1), |
|
743 (rtac contrapos 1), |
|
744 (etac spec 1), |
|
745 (rtac trans_less 1), |
|
746 (atac 2), |
|
747 (etac (contX2mono RS monofun_fun_arg) 1), |
|
748 (rtac is_ub_thelub 1), |
|
749 (atac 1) |
|
750 ]); |
|
751 |
|
752 val adm_all = prove_goal Fix.thy |
|
753 " !y.adm(P(y)) ==> adm(%x.!y.P(y,x))" |
|
754 (fn prems => |
|
755 [ |
|
756 (cut_facts_tac prems 1), |
|
757 (rtac (adm_def2 RS iffD2) 1), |
|
758 (strip_tac 1), |
|
759 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
760 (etac spec 1), |
|
761 (atac 1), |
|
762 (rtac allI 1), |
|
763 (dtac spec 1), |
|
764 (etac spec 1) |
|
765 ]); |
|
766 |
|
767 val adm_subst = prove_goal Fix.thy |
|
768 "[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))" |
|
769 (fn prems => |
|
770 [ |
|
771 (cut_facts_tac prems 1), |
|
772 (rtac (adm_def2 RS iffD2) 1), |
|
773 (strip_tac 1), |
|
774 (rtac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1), |
|
775 (atac 1), |
|
776 (atac 1), |
|
777 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
778 (atac 1), |
|
779 (rtac (contX2mono RS ch2ch_monofun) 1), |
|
780 (atac 1), |
|
781 (atac 1), |
|
782 (atac 1) |
|
783 ]); |
|
784 |
|
785 val adm_UU_not_less = prove_goal Fix.thy "adm(%x.~ UU << t(x))" |
|
786 (fn prems => |
|
787 [ |
|
788 (res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1), |
|
789 (asm_simp_tac Cfun_ss 1), |
|
790 (rtac adm_not_free 1) |
|
791 ]); |
|
792 |
|
793 val adm_not_UU = prove_goalw Fix.thy [adm_def] |
|
794 "contX(t)==> adm(%x.~ t(x) = UU)" |
|
795 (fn prems => |
|
796 [ |
|
797 (cut_facts_tac prems 1), |
|
798 (strip_tac 1), |
|
799 (rtac contrapos 1), |
|
800 (etac spec 1), |
|
801 (rtac (chain_UU_I RS spec) 1), |
|
802 (rtac (contX2mono RS ch2ch_monofun) 1), |
|
803 (atac 1), |
|
804 (atac 1), |
|
805 (rtac (contX2contlub RS contlubE RS spec RS mp RS subst) 1), |
|
806 (atac 1), |
|
807 (atac 1), |
|
808 (atac 1) |
|
809 ]); |
|
810 |
|
811 val adm_eq = prove_goal Fix.thy |
|
812 "[|contX(u);contX(v)|]==> adm(%x.u(x)= v(x))" |
|
813 (fn prems => |
|
814 [ |
|
815 (rtac (adm_cong RS iffD1) 1), |
|
816 (rtac allI 1), |
|
817 (rtac iffI 1), |
|
818 (rtac antisym_less 1), |
|
819 (rtac antisym_less_inverse 3), |
|
820 (atac 3), |
|
821 (etac conjunct1 1), |
|
822 (etac conjunct2 1), |
|
823 (rtac adm_conj 1), |
|
824 (rtac adm_less 1), |
|
825 (resolve_tac prems 1), |
|
826 (resolve_tac prems 1), |
|
827 (rtac adm_less 1), |
|
828 (resolve_tac prems 1), |
|
829 (resolve_tac prems 1) |
|
830 ]); |
|
831 |
|
832 |
|
833 (* ------------------------------------------------------------------------ *) |
|
834 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas *) |
|
835 (* ------------------------------------------------------------------------ *) |
|
836 |
|
837 val adm_disj_lemma1 = prove_goal Pcpo.thy |
|
838 "[| is_chain(Y); !n.P(Y(n))|Q(Y(n))|]\ |
|
839 \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))" |
|
840 (fn prems => |
|
841 [ |
|
842 (cut_facts_tac prems 1), |
|
843 (fast_tac HOL_cs 1) |
|
844 ]); |
|
845 |
|
846 val adm_disj_lemma2 = prove_goal Fix.thy |
|
847 "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\ |
|
848 \ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))" |
|
849 (fn prems => |
|
850 [ |
|
851 (cut_facts_tac prems 1), |
|
852 (etac exE 1), |
|
853 (etac conjE 1), |
|
854 (etac conjE 1), |
|
855 (res_inst_tac [("s","lub(range(X))"),("t","lub(range(Y))")] ssubst 1), |
|
856 (atac 1), |
|
857 (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1), |
|
858 (atac 1), |
|
859 (atac 1), |
|
860 (atac 1) |
|
861 ]); |
|
862 |
|
863 val adm_disj_lemma3 = prove_goal Fix.thy |
|
864 "[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\ |
|
865 \ is_chain(%m. if(m < Suc(i),Y(Suc(i)),Y(m)))" |
|
866 (fn prems => |
|
867 [ |
|
868 (cut_facts_tac prems 1), |
|
869 (rtac is_chainI 1), |
|
870 (rtac allI 1), |
|
871 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
|
872 (res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1), |
|
873 (rtac iffI 1), |
|
874 (etac FalseE 2), |
|
875 (rtac notE 1), |
|
876 (rtac (not_less_eq RS iffD2) 1), |
|
877 (atac 1), |
|
878 (atac 1), |
|
879 (res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1), |
|
880 (asm_simp_tac nat_ss 1), |
|
881 (rtac iffI 1), |
|
882 (etac FalseE 2), |
|
883 (rtac notE 1), |
|
884 (etac (less_not_sym RS mp) 1), |
|
885 (atac 1), |
|
886 (asm_simp_tac Cfun_ss 1), |
|
887 (etac (is_chainE RS spec) 1), |
|
888 (hyp_subst_tac 1), |
|
889 (asm_simp_tac nat_ss 1), |
|
890 (rtac refl_less 1), |
|
891 (asm_simp_tac nat_ss 1), |
|
892 (rtac refl_less 1) |
|
893 ]); |
|
894 |
|
895 val adm_disj_lemma4 = prove_goal Fix.thy |
|
896 "[| ! j. i < j --> Q(Y(j)) |] ==>\ |
|
897 \ ! n. Q(if(n < Suc(i),Y(Suc(i)),Y(n)))" |
|
898 (fn prems => |
|
899 [ |
|
900 (cut_facts_tac prems 1), |
|
901 (rtac allI 1), |
|
902 (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1), |
|
903 (res_inst_tac[("s","Y(Suc(i))"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")] |
|
904 ssubst 1), |
|
905 (asm_simp_tac nat_ss 1), |
|
906 (etac allE 1), |
|
907 (rtac mp 1), |
|
908 (atac 1), |
|
909 (asm_simp_tac nat_ss 1), |
|
910 (res_inst_tac[("s","Y(n)"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")] |
|
911 ssubst 1), |
|
912 (asm_simp_tac nat_ss 1), |
|
913 (hyp_subst_tac 1), |
|
914 (dtac spec 1), |
|
915 (rtac mp 1), |
|
916 (atac 1), |
|
917 (asm_simp_tac nat_ss 1), |
|
918 (res_inst_tac [("s","Y(n)"),("t","if(n < Suc(i),Y(Suc(i)),Y(n))")] |
|
919 ssubst 1), |
|
920 (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1), |
|
921 (rtac iffI 1), |
|
922 (etac FalseE 2), |
|
923 (rtac notE 1), |
|
924 (etac (less_not_sym RS mp) 1), |
|
925 (atac 1), |
|
926 (asm_simp_tac nat_ss 1), |
|
927 (dtac spec 1), |
|
928 (rtac mp 1), |
|
929 (atac 1), |
|
930 (etac Suc_lessD 1) |
|
931 ]); |
|
932 |
|
933 val adm_disj_lemma5 = prove_goal Fix.thy |
|
934 "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\ |
|
935 \ lub(range(Y)) = lub(range(%m. if(m < Suc(i),Y(Suc(i)),Y(m))))" |
|
936 (fn prems => |
|
937 [ |
|
938 (cut_facts_tac prems 1), |
|
939 (rtac lub_equal2 1), |
|
940 (atac 2), |
|
941 (rtac adm_disj_lemma3 2), |
|
942 (atac 2), |
|
943 (atac 2), |
|
944 (res_inst_tac [("x","i")] exI 1), |
|
945 (strip_tac 1), |
|
946 (res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1), |
|
947 (rtac iffI 1), |
|
948 (etac FalseE 2), |
|
949 (rtac notE 1), |
|
950 (rtac (not_less_eq RS iffD2) 1), |
|
951 (atac 1), |
|
952 (atac 1), |
|
953 (rtac (if_False RS ssubst) 1), |
|
954 (rtac refl 1) |
|
955 ]); |
|
956 |
|
957 val adm_disj_lemma6 = prove_goal Fix.thy |
|
958 "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
|
959 \ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))" |
|
960 (fn prems => |
|
961 [ |
|
962 (cut_facts_tac prems 1), |
|
963 (etac exE 1), |
|
964 (res_inst_tac [("x","%m.if(m< Suc(i),Y(Suc(i)),Y(m))")] exI 1), |
|
965 (rtac conjI 1), |
|
966 (rtac adm_disj_lemma3 1), |
|
967 (atac 1), |
|
968 (atac 1), |
|
969 (rtac conjI 1), |
|
970 (rtac adm_disj_lemma4 1), |
|
971 (atac 1), |
|
972 (rtac adm_disj_lemma5 1), |
|
973 (atac 1), |
|
974 (atac 1) |
|
975 ]); |
|
976 |
|
977 |
|
978 val adm_disj_lemma7 = prove_goal Fix.thy |
|
979 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
|
980 \ is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))" |
|
981 (fn prems => |
|
982 [ |
|
983 (cut_facts_tac prems 1), |
|
984 (rtac is_chainI 1), |
|
985 (rtac allI 1), |
|
986 (rtac chain_mono3 1), |
|
987 (atac 1), |
|
988 (rtac theleast2 1), |
|
989 (rtac conjI 1), |
|
990 (rtac Suc_lessD 1), |
|
991 (etac allE 1), |
|
992 (etac exE 1), |
|
993 (rtac (theleast1 RS conjunct1) 1), |
|
994 (atac 1), |
|
995 (etac allE 1), |
|
996 (etac exE 1), |
|
997 (rtac (theleast1 RS conjunct2) 1), |
|
998 (atac 1) |
|
999 ]); |
|
1000 |
|
1001 val adm_disj_lemma8 = prove_goal Fix.thy |
|
1002 "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))" |
|
1003 (fn prems => |
|
1004 [ |
|
1005 (cut_facts_tac prems 1), |
|
1006 (strip_tac 1), |
|
1007 (etac allE 1), |
|
1008 (etac exE 1), |
|
1009 (etac (theleast1 RS conjunct2) 1) |
|
1010 ]); |
|
1011 |
|
1012 val adm_disj_lemma9 = prove_goal Fix.thy |
|
1013 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
|
1014 \ lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))" |
|
1015 (fn prems => |
|
1016 [ |
|
1017 (cut_facts_tac prems 1), |
|
1018 (rtac antisym_less 1), |
|
1019 (rtac lub_mono 1), |
|
1020 (atac 1), |
|
1021 (rtac adm_disj_lemma7 1), |
|
1022 (atac 1), |
|
1023 (atac 1), |
|
1024 (strip_tac 1), |
|
1025 (rtac (chain_mono RS mp) 1), |
|
1026 (atac 1), |
|
1027 (etac allE 1), |
|
1028 (etac exE 1), |
|
1029 (rtac (theleast1 RS conjunct1) 1), |
|
1030 (atac 1), |
|
1031 (rtac lub_mono3 1), |
|
1032 (rtac adm_disj_lemma7 1), |
|
1033 (atac 1), |
|
1034 (atac 1), |
|
1035 (atac 1), |
|
1036 (strip_tac 1), |
|
1037 (rtac exI 1), |
|
1038 (rtac (chain_mono RS mp) 1), |
|
1039 (atac 1), |
|
1040 (rtac lessI 1) |
|
1041 ]); |
|
1042 |
|
1043 val adm_disj_lemma10 = prove_goal Fix.thy |
|
1044 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
|
1045 \ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))" |
|
1046 (fn prems => |
|
1047 [ |
|
1048 (cut_facts_tac prems 1), |
|
1049 (res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1), |
|
1050 (rtac conjI 1), |
|
1051 (rtac adm_disj_lemma7 1), |
|
1052 (atac 1), |
|
1053 (atac 1), |
|
1054 (rtac conjI 1), |
|
1055 (rtac adm_disj_lemma8 1), |
|
1056 (atac 1), |
|
1057 (rtac adm_disj_lemma9 1), |
|
1058 (atac 1), |
|
1059 (atac 1) |
|
1060 ]); |
|
1061 |
|
1062 val adm_disj = prove_goal Fix.thy |
|
1063 "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))" |
|
1064 (fn prems => |
|
1065 [ |
|
1066 (cut_facts_tac prems 1), |
|
1067 (rtac (adm_def2 RS iffD2) 1), |
|
1068 (strip_tac 1), |
|
1069 (rtac (adm_disj_lemma1 RS disjE) 1), |
|
1070 (atac 1), |
|
1071 (atac 1), |
|
1072 (rtac disjI2 1), |
|
1073 (rtac adm_disj_lemma2 1), |
|
1074 (atac 1), |
|
1075 (rtac adm_disj_lemma6 1), |
|
1076 (atac 1), |
|
1077 (atac 1), |
|
1078 (rtac disjI1 1), |
|
1079 (rtac adm_disj_lemma2 1), |
|
1080 (atac 1), |
|
1081 (rtac adm_disj_lemma10 1), |
|
1082 (atac 1), |
|
1083 (atac 1) |
|
1084 ]); |
|
1085 |
|
1086 val adm_impl = prove_goal Fix.thy |
|
1087 "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))" |
|
1088 (fn prems => |
|
1089 [ |
|
1090 (cut_facts_tac prems 1), |
|
1091 (res_inst_tac [("P2","%x.~P(x)|Q(x)")] (adm_cong RS iffD1) 1), |
|
1092 (fast_tac HOL_cs 1), |
|
1093 (rtac adm_disj 1), |
|
1094 (atac 1), |
|
1095 (atac 1) |
|
1096 ]); |
|
1097 |
|
1098 |
|
1099 val adm_all2 = (allI RS adm_all); |
|
1100 |
|
1101 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, |
|
1102 adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less |
|
1103 ]; |
|
1104 |
|
1105 (* ------------------------------------------------------------------------- *) |
|
1106 (* a result about functions with flat codomain *) |
|
1107 (* ------------------------------------------------------------------------- *) |
|
1108 |
|
1109 val flat_codom = prove_goalw Fix.thy [flat_def] |
|
1110 "[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)" |
|
1111 (fn prems => |
|
1112 [ |
|
1113 (cut_facts_tac prems 1), |
|
1114 (res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1), |
|
1115 (rtac disjI1 1), |
|
1116 (rtac UU_I 1), |
|
1117 (res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1), |
|
1118 (atac 1), |
|
1119 (rtac (minimal RS monofun_cfun_arg) 1), |
|
1120 (res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1), |
|
1121 (etac disjI1 1), |
|
1122 (rtac disjI2 1), |
|
1123 (rtac allI 1), |
|
1124 (res_inst_tac [("s","f[x]"),("t","c")] subst 1), |
|
1125 (atac 1), |
|
1126 (res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1), |
|
1127 (etac allE 1),(etac allE 1), |
|
1128 (dtac mp 1), |
|
1129 (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1), |
|
1130 (etac disjE 1), |
|
1131 (contr_tac 1), |
|
1132 (atac 1), |
|
1133 (etac allE 1), |
|
1134 (etac allE 1), |
|
1135 (dtac mp 1), |
|
1136 (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1), |
|
1137 (etac disjE 1), |
|
1138 (contr_tac 1), |
|
1139 (atac 1) |
|
1140 ]); |