7 *) |
7 *) |
8 |
8 |
9 header {* Fixed point operator and admissibility *} |
9 header {* Fixed point operator and admissibility *} |
10 |
10 |
11 theory Fix |
11 theory Fix |
12 imports Cfun Cprod |
12 imports Cfun Cprod Adm |
13 begin |
13 begin |
14 |
14 |
15 subsection {* Definitions *} |
15 subsection {* Definitions *} |
16 |
16 |
17 consts |
17 consts |
18 |
18 |
19 iterate :: "nat=>('a->'a)=>'a=>'a" |
19 iterate :: "nat=>('a->'a)=>'a=>'a" |
20 Ifix :: "('a->'a)=>'a" |
20 Ifix :: "('a->'a)=>'a" |
21 "fix" :: "('a->'a)->'a" |
21 "fix" :: "('a->'a)->'a" |
22 adm :: "('a::cpo=>bool)=>bool" |
|
23 admw :: "('a=>bool)=>bool" |
22 admw :: "('a=>bool)=>bool" |
24 |
23 |
25 primrec |
24 primrec |
26 iterate_0: "iterate 0 F x = x" |
25 iterate_0: "iterate 0 F x = x" |
27 iterate_Suc: "iterate (Suc n) F x = F$(iterate n F x)" |
26 iterate_Suc: "iterate (Suc n) F x = F$(iterate n F x)" |
28 |
27 |
29 defs |
28 defs |
30 |
29 |
31 Ifix_def: "Ifix F == lub(range(%i. iterate i F UU))" |
30 Ifix_def: "Ifix F == lub(range(%i. iterate i F UU))" |
32 fix_def: "fix == (LAM f. Ifix f)" |
31 fix_def: "fix == (LAM f. Ifix f)" |
33 |
|
34 adm_def: "adm P == !Y. chain(Y) --> |
|
35 (!i. P(Y i)) --> P(lub(range Y))" |
|
36 |
32 |
37 admw_def: "admw P == !F. (!n. P (iterate n F UU)) --> |
33 admw_def: "admw P == !F. (!n. P (iterate n F UU)) --> |
38 P (lub(range (%i. iterate i F UU)))" |
34 P (lub(range (%i. iterate i F UU)))" |
39 |
35 |
40 subsection {* Binder syntax for @{term fix} *} |
36 subsection {* Binder syntax for @{term fix} *} |
306 apply simp |
284 apply simp |
307 apply (erule wfix_ind) |
285 apply (erule wfix_ind) |
308 apply assumption |
286 apply assumption |
309 done |
287 done |
310 |
288 |
311 text {* for chain-finite (easy) types every formula is admissible *} |
|
312 |
|
313 lemma adm_max_in_chain: |
|
314 "!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)" |
|
315 apply (unfold adm_def) |
|
316 apply (intro strip) |
|
317 apply (rule exE) |
|
318 apply (rule mp) |
|
319 apply (erule spec) |
|
320 apply assumption |
|
321 apply (subst lub_finch1 [THEN thelubI]) |
|
322 apply assumption |
|
323 apply assumption |
|
324 apply (erule spec) |
|
325 done |
|
326 |
|
327 lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard] |
|
328 |
|
329 text {* some lemmata for functions with flat/chfin domain/range types *} |
|
330 |
|
331 lemma adm_chfindom: "adm (%(u::'a::cpo->'b::chfin). P(u$s))" |
|
332 apply (unfold adm_def) |
|
333 apply (intro strip) |
|
334 apply (drule chfin_Rep_CFunR) |
|
335 apply (erule_tac x = "s" in allE) |
|
336 apply clarsimp |
|
337 done |
|
338 |
|
339 (* adm_flat not needed any more, since it is a special case of adm_chfindom *) |
|
340 |
|
341 text {* improved admissibility introduction *} |
|
342 |
|
343 lemma admI2: |
|
344 "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |] |
|
345 ==> P(lub (range Y))) ==> adm P" |
|
346 apply (unfold adm_def) |
|
347 apply (intro strip) |
|
348 apply (erule increasing_chain_adm_lemma) |
|
349 apply assumption |
|
350 apply fast |
|
351 done |
|
352 |
|
353 text {* admissibility of special formulae and propagation *} |
|
354 |
|
355 lemma adm_less [simp]: "[|cont u;cont v|]==> adm(%x. u x << v x)" |
|
356 apply (unfold adm_def) |
|
357 apply (intro strip) |
|
358 apply (frule_tac f = "u" in cont2mono [THEN ch2ch_monofun]) |
|
359 apply assumption |
|
360 apply (frule_tac f = "v" in cont2mono [THEN ch2ch_monofun]) |
|
361 apply assumption |
|
362 apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) |
|
363 apply assumption |
|
364 apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) |
|
365 apply assumption |
|
366 apply (blast intro: lub_mono) |
|
367 done |
|
368 |
|
369 lemma adm_conj [simp]: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)" |
|
370 by (fast elim: admD intro: admI) |
|
371 |
|
372 lemma adm_not_free [simp]: "adm(%x. t)" |
|
373 apply (unfold adm_def) |
|
374 apply fast |
|
375 done |
|
376 |
|
377 lemma adm_not_less: "cont t ==> adm(%x.~ (t x) << u)" |
|
378 apply (unfold adm_def) |
|
379 apply (intro strip) |
|
380 apply (rule contrapos_nn) |
|
381 apply (erule spec) |
|
382 apply (rule trans_less) |
|
383 prefer 2 apply (assumption) |
|
384 apply (erule cont2mono [THEN monofun_fun_arg]) |
|
385 apply (rule is_ub_thelub) |
|
386 apply assumption |
|
387 done |
|
388 |
|
389 lemma adm_all: "!y. adm(P y) ==> adm(%x.!y. P y x)" |
|
390 by (fast intro: admI elim: admD) |
|
391 |
|
392 lemmas adm_all2 = allI [THEN adm_all, standard] |
|
393 |
|
394 lemma adm_subst: "[|cont t; adm P|] ==> adm(%x. P (t x))" |
|
395 apply (rule admI) |
|
396 apply (simplesubst cont2contlub [THEN contlubE, THEN spec, THEN mp]) |
|
397 apply assumption |
|
398 apply assumption |
|
399 apply (erule admD) |
|
400 apply (erule cont2mono [THEN ch2ch_monofun]) |
|
401 apply assumption |
|
402 apply assumption |
|
403 done |
|
404 |
|
405 lemma adm_UU_not_less: "adm(%x.~ UU << t(x))" |
|
406 by simp |
|
407 |
|
408 lemma adm_not_UU: "cont(t)==> adm(%x.~ (t x) = UU)" |
|
409 apply (unfold adm_def) |
|
410 apply (intro strip) |
|
411 apply (rule contrapos_nn) |
|
412 apply (erule spec) |
|
413 apply (rule chain_UU_I [THEN spec]) |
|
414 apply (erule cont2mono [THEN ch2ch_monofun]) |
|
415 apply assumption |
|
416 apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN subst]) |
|
417 apply assumption |
|
418 apply assumption |
|
419 done |
|
420 |
|
421 lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)" |
|
422 by (simp add: po_eq_conv) |
|
423 |
|
424 text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *} |
|
425 |
|
426 lemma adm_disj_lemma1: |
|
427 "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)" |
|
428 apply (erule contrapos_pp) |
|
429 apply clarsimp |
|
430 apply (rule exI) |
|
431 apply (rule conjI) |
|
432 apply (drule spec, erule mp) |
|
433 apply (rule le_maxI1) |
|
434 apply (drule spec, erule mp) |
|
435 apply (rule le_maxI2) |
|
436 done |
|
437 |
|
438 lemma adm_disj_lemma2: "[| adm P; \<exists>X. chain X & (!n. P(X n)) & |
|
439 lub(range Y)=lub(range X)|] ==> P(lub(range Y))" |
|
440 by (force elim: admD) |
|
441 |
|
442 lemma adm_disj_lemma3: |
|
443 "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> |
|
444 chain(%m. Y (LEAST j. m\<le>j \<and> P(Y j)))" |
|
445 apply (rule chainI) |
|
446 apply (erule chain_mono3) |
|
447 apply (rule Least_le) |
|
448 apply (rule conjI) |
|
449 apply (rule Suc_leD) |
|
450 apply (erule allE) |
|
451 apply (erule exE) |
|
452 apply (erule LeastI [THEN conjunct1]) |
|
453 apply (erule allE) |
|
454 apply (erule exE) |
|
455 apply (erule LeastI [THEN conjunct2]) |
|
456 done |
|
457 |
|
458 lemma adm_disj_lemma4: |
|
459 "[| \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> ! m. P(Y(LEAST j::nat. m\<le>j & P(Y j)))" |
|
460 apply (rule allI) |
|
461 apply (erule allE) |
|
462 apply (erule exE) |
|
463 apply (erule LeastI [THEN conjunct2]) |
|
464 done |
|
465 |
|
466 lemma adm_disj_lemma5: |
|
467 "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> |
|
468 lub(range(Y)) = (LUB m. Y(LEAST j. m\<le>j & P(Y j)))" |
|
469 apply (rule antisym_less) |
|
470 apply (rule lub_mono) |
|
471 apply assumption |
|
472 apply (erule adm_disj_lemma3) |
|
473 apply assumption |
|
474 apply (rule allI) |
|
475 apply (erule chain_mono3) |
|
476 apply (erule allE) |
|
477 apply (erule exE) |
|
478 apply (erule LeastI [THEN conjunct1]) |
|
479 apply (rule lub_mono3) |
|
480 apply (erule adm_disj_lemma3) |
|
481 apply assumption |
|
482 apply assumption |
|
483 apply (rule allI) |
|
484 apply (rule exI) |
|
485 apply (rule refl_less) |
|
486 done |
|
487 |
|
488 lemma adm_disj_lemma6: |
|
489 "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> |
|
490 \<exists>X. chain X & (\<forall>n. P(X n)) & lub(range Y) = lub(range X)" |
|
491 apply (rule_tac x = "%m. Y (LEAST j. m\<le>j & P (Y j))" in exI) |
|
492 apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5) |
|
493 done |
|
494 |
|
495 lemma adm_disj_lemma7: |
|
496 "[| adm(P); chain(Y); \<forall>i. \<exists>j\<ge>i. P(Y j) |]==>P(lub(range(Y)))" |
|
497 apply (erule adm_disj_lemma2) |
|
498 apply (erule adm_disj_lemma6) |
|
499 apply assumption |
|
500 done |
|
501 |
|
502 lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)" |
|
503 apply (rule admI) |
|
504 apply (erule adm_disj_lemma1 [THEN disjE]) |
|
505 apply (rule disjI1) |
|
506 apply (erule adm_disj_lemma7) |
|
507 apply assumption |
|
508 apply assumption |
|
509 apply (rule disjI2) |
|
510 apply (erule adm_disj_lemma7) |
|
511 apply assumption |
|
512 apply assumption |
|
513 done |
|
514 |
|
515 lemma adm_imp: "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)" |
|
516 by (subst imp_conv_disj, rule adm_disj) |
|
517 |
|
518 lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] |
|
519 ==> adm (%x. P x = Q x)" |
|
520 by (subst iff_conv_conj_imp, rule adm_conj) |
|
521 |
|
522 lemma adm_not_conj: "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))" |
|
523 by (subst de_Morgan_conj, rule adm_disj) |
|
524 |
|
525 lemmas adm_lemmas = adm_not_free adm_imp adm_disj adm_eq adm_not_UU |
|
526 adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff |
|
527 |
|
528 declare adm_lemmas [simp] |
|
529 |
|
530 end |
289 end |
531 |
290 |