src/HOLCF/Fix.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 5656 f8389824189b
permissions -rw-r--r--
made tutorial first;
     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 qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
    16  (fn prems =>
    17         [
    18         (induct_tac "n" 1),
    19         (Simp_tac 1),
    20         (stac iterate_Suc 1),
    21         (stac iterate_Suc 1),
    22         (etac ssubst 1),
    23         (rtac refl 1)
    24         ]);
    25 
    26 (* ------------------------------------------------------------------------ *)
    27 (* the sequence of function itertaions is a chain                           *)
    28 (* This property is essential since monotonicity of iterate makes no sense  *)
    29 (* ------------------------------------------------------------------------ *)
    30 
    31 qed_goalw "chain_iterate2" thy [chain] 
    32         " x << F`x ==> chain (%i. iterate i F x)"
    33  (fn prems =>
    34         [
    35         (cut_facts_tac prems 1),
    36         (strip_tac 1),
    37         (Simp_tac 1),
    38         (induct_tac "i" 1),
    39         (Asm_simp_tac 1),
    40         (Asm_simp_tac 1),
    41         (etac monofun_cfun_arg 1)
    42         ]);
    43 
    44 
    45 qed_goal "chain_iterate" thy  
    46         "chain (%i. iterate i F UU)"
    47  (fn prems =>
    48         [
    49         (rtac chain_iterate2 1),
    50         (rtac minimal 1)
    51         ]);
    52 
    53 
    54 (* ------------------------------------------------------------------------ *)
    55 (* Kleene's fixed point theorems for continuous functions in pointed        *)
    56 (* omega cpo's                                                              *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 
    60 qed_goalw "Ifix_eq" thy  [Ifix_def] "Ifix F =F`(Ifix F)"
    61  (fn prems =>
    62         [
    63         (stac contlub_cfun_arg 1),
    64         (rtac chain_iterate 1),
    65         (rtac antisym_less 1),
    66         (rtac lub_mono 1),
    67         (rtac chain_iterate 1),
    68         (rtac ch2ch_Rep_CFunR 1),
    69         (rtac chain_iterate 1),
    70         (rtac allI 1),
    71         (rtac (iterate_Suc RS subst) 1),
    72         (rtac (chain_iterate RS chainE RS spec) 1),
    73         (rtac is_lub_thelub 1),
    74         (rtac ch2ch_Rep_CFunR 1),
    75         (rtac chain_iterate 1),
    76         (rtac ub_rangeI 1),
    77         (rtac allI 1),
    78         (rtac (iterate_Suc RS subst) 1),
    79         (rtac is_ub_thelub 1),
    80         (rtac chain_iterate 1)
    81         ]);
    82 
    83 
    84 qed_goalw "Ifix_least" thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
    85  (fn prems =>
    86         [
    87         (cut_facts_tac prems 1),
    88         (rtac is_lub_thelub 1),
    89         (rtac chain_iterate 1),
    90         (rtac ub_rangeI 1),
    91         (strip_tac 1),
    92         (induct_tac "i" 1),
    93         (Asm_simp_tac 1),
    94         (Asm_simp_tac 1),
    95         (res_inst_tac [("t","x")] subst 1),
    96         (atac 1),
    97         (etac monofun_cfun_arg 1)
    98         ]);
    99 
   100 
   101 (* ------------------------------------------------------------------------ *)
   102 (* monotonicity and continuity of iterate                                   *)
   103 (* ------------------------------------------------------------------------ *)
   104 
   105 qed_goalw "monofun_iterate" thy  [monofun] "monofun(iterate(i))"
   106  (fn prems =>
   107         [
   108         (strip_tac 1),
   109         (induct_tac "i" 1),
   110         (Asm_simp_tac 1),
   111         (Asm_simp_tac 1),
   112         (rtac (less_fun RS iffD2) 1),
   113         (rtac allI 1),
   114         (rtac monofun_cfun 1),
   115         (atac 1),
   116         (rtac (less_fun RS iffD1 RS spec) 1),
   117         (atac 1)
   118         ]);
   119 
   120 (* ------------------------------------------------------------------------ *)
   121 (* the following lemma uses contlub_cfun which itself is based on a         *)
   122 (* diagonalisation lemma for continuous functions with two arguments.       *)
   123 (* In this special case it is the application function Rep_CFun                 *)
   124 (* ------------------------------------------------------------------------ *)
   125 
   126 qed_goalw "contlub_iterate" thy  [contlub] "contlub(iterate(i))"
   127  (fn prems =>
   128         [
   129         (strip_tac 1),
   130         (induct_tac "i" 1),
   131         (Asm_simp_tac 1),
   132         (rtac (lub_const RS thelubI RS sym) 1),
   133         (Asm_simp_tac 1),
   134         (rtac ext 1),
   135         (stac thelub_fun 1),
   136         (rtac chainI 1),
   137         (rtac allI 1),
   138         (rtac (less_fun RS iffD2) 1),
   139         (rtac allI 1),
   140         (rtac (chainE RS spec) 1),
   141         (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
   142         (rtac allI 1),
   143         (rtac monofun_Rep_CFun2 1),
   144         (atac 1),
   145         (rtac ch2ch_fun 1),
   146         (rtac (monofun_iterate RS ch2ch_monofun) 1),
   147         (atac 1),
   148         (stac thelub_fun 1),
   149         (rtac (monofun_iterate RS ch2ch_monofun) 1),
   150         (atac 1),
   151         (rtac contlub_cfun  1),
   152         (atac 1),
   153         (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
   154         ]);
   155 
   156 
   157 qed_goal "cont_iterate" thy "cont(iterate(i))"
   158  (fn prems =>
   159         [
   160         (rtac monocontlub2cont 1),
   161         (rtac monofun_iterate 1),
   162         (rtac contlub_iterate 1)
   163         ]);
   164 
   165 (* ------------------------------------------------------------------------ *)
   166 (* a lemma about continuity of iterate in its third argument                *)
   167 (* ------------------------------------------------------------------------ *)
   168 
   169 qed_goal "monofun_iterate2" thy "monofun(iterate n F)"
   170  (fn prems =>
   171         [
   172         (rtac monofunI 1),
   173         (strip_tac 1),
   174         (induct_tac "n" 1),
   175         (Asm_simp_tac 1),
   176         (Asm_simp_tac 1),
   177         (etac monofun_cfun_arg 1)
   178         ]);
   179 
   180 qed_goal "contlub_iterate2" thy "contlub(iterate n F)"
   181  (fn prems =>
   182         [
   183         (rtac contlubI 1),
   184         (strip_tac 1),
   185         (induct_tac "n" 1),
   186         (Simp_tac 1),
   187         (Simp_tac 1),
   188         (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
   189         ("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1),
   190         (atac 1),
   191         (rtac contlub_cfun_arg 1),
   192         (etac (monofun_iterate2 RS ch2ch_monofun) 1)
   193         ]);
   194 
   195 qed_goal "cont_iterate2" thy "cont (iterate n F)"
   196  (fn prems =>
   197         [
   198         (rtac monocontlub2cont 1),
   199         (rtac monofun_iterate2 1),
   200         (rtac contlub_iterate2 1)
   201         ]);
   202 
   203 (* ------------------------------------------------------------------------ *)
   204 (* monotonicity and continuity of Ifix                                      *)
   205 (* ------------------------------------------------------------------------ *)
   206 
   207 qed_goalw "monofun_Ifix" thy  [monofun,Ifix_def] "monofun(Ifix)"
   208  (fn prems =>
   209         [
   210         (strip_tac 1),
   211         (rtac lub_mono 1),
   212         (rtac chain_iterate 1),
   213         (rtac chain_iterate 1),
   214         (rtac allI 1),
   215         (rtac (less_fun RS iffD1 RS spec) 1),
   216         (etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1)
   217         ]);
   218 
   219 (* ------------------------------------------------------------------------ *)
   220 (* since iterate is not monotone in its first argument, special lemmas must *)
   221 (* be derived for lubs in this argument                                     *)
   222 (* ------------------------------------------------------------------------ *)
   223 
   224 qed_goal "chain_iterate_lub" thy   
   225 "chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
   226  (fn prems =>
   227         [
   228         (cut_facts_tac prems 1),
   229         (rtac chainI 1),
   230         (strip_tac 1),
   231         (rtac lub_mono 1),
   232         (rtac chain_iterate 1),
   233         (rtac chain_iterate 1),
   234         (strip_tac 1),
   235         (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE 
   236          RS spec) 1)
   237         ]);
   238 
   239 (* ------------------------------------------------------------------------ *)
   240 (* this exchange lemma is analog to the one for monotone functions          *)
   241 (* observe that monotonicity is not really needed. The propagation of       *)
   242 (* chains is the essential argument which is usually derived from monot.    *)
   243 (* ------------------------------------------------------------------------ *)
   244 
   245 qed_goal "contlub_Ifix_lemma1" thy 
   246 "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
   247  (fn prems =>
   248         [
   249         (cut_facts_tac prems 1),
   250         (rtac (thelub_fun RS subst) 1),
   251         (rtac (monofun_iterate RS ch2ch_monofun) 1),
   252         (atac 1),
   253         (rtac fun_cong 1),
   254         (stac (contlub_iterate RS contlubE RS spec RS mp) 1),
   255         (atac 1),
   256         (rtac refl 1)
   257         ]);
   258 
   259 
   260 qed_goal "ex_lub_iterate" thy  "chain(Y) ==>\
   261 \         lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
   262 \         lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
   263  (fn prems =>
   264         [
   265         (cut_facts_tac prems 1),
   266         (rtac antisym_less 1),
   267         (rtac is_lub_thelub 1),
   268         (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
   269         (atac 1),
   270         (rtac chain_iterate 1),
   271         (rtac ub_rangeI 1),
   272         (strip_tac 1),
   273         (rtac lub_mono 1),
   274         (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1),
   275         (etac chain_iterate_lub 1),
   276         (strip_tac 1),
   277         (rtac is_ub_thelub 1),
   278         (rtac chain_iterate 1),
   279         (rtac is_lub_thelub 1),
   280         (etac chain_iterate_lub 1),
   281         (rtac ub_rangeI 1),
   282         (strip_tac 1),
   283         (rtac lub_mono 1),
   284         (rtac chain_iterate 1),
   285         (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
   286         (atac 1),
   287         (rtac chain_iterate 1),
   288         (strip_tac 1),
   289         (rtac is_ub_thelub 1),
   290         (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
   291         ]);
   292 
   293 
   294 qed_goalw "contlub_Ifix" thy  [contlub,Ifix_def] "contlub(Ifix)"
   295  (fn prems =>
   296         [
   297         (strip_tac 1),
   298         (stac (contlub_Ifix_lemma1 RS ext) 1),
   299         (atac 1),
   300         (etac ex_lub_iterate 1)
   301         ]);
   302 
   303 
   304 qed_goal "cont_Ifix" thy "cont(Ifix)"
   305  (fn prems =>
   306         [
   307         (rtac monocontlub2cont 1),
   308         (rtac monofun_Ifix 1),
   309         (rtac contlub_Ifix 1)
   310         ]);
   311 
   312 (* ------------------------------------------------------------------------ *)
   313 (* propagate properties of Ifix to its continuous counterpart               *)
   314 (* ------------------------------------------------------------------------ *)
   315 
   316 qed_goalw "fix_eq" thy  [fix_def] "fix`F = F`(fix`F)"
   317  (fn prems =>
   318         [
   319         (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
   320         (rtac Ifix_eq 1)
   321         ]);
   322 
   323 qed_goalw "fix_least" thy [fix_def] "F`x = x ==> fix`F << x"
   324  (fn prems =>
   325         [
   326         (cut_facts_tac prems 1),
   327         (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
   328         (etac Ifix_least 1)
   329         ]);
   330 
   331 
   332 qed_goal "fix_eqI" thy
   333 "[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"
   334  (fn prems =>
   335         [
   336         (cut_facts_tac prems 1),
   337         (rtac antisym_less 1),
   338         (etac allE 1),
   339         (etac mp 1),
   340         (rtac (fix_eq RS sym) 1),
   341         (etac fix_least 1)
   342         ]);
   343 
   344 
   345 qed_goal "fix_eq2" thy "f == fix`F ==> f = F`f"
   346  (fn prems =>
   347         [
   348         (rewrite_goals_tac prems),
   349         (rtac fix_eq 1)
   350         ]);
   351 
   352 qed_goal "fix_eq3" thy "f == fix`F ==> f`x = F`f`x"
   353  (fn prems =>
   354         [
   355         (rtac trans 1),
   356         (rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1),
   357         (rtac refl 1)
   358         ]);
   359 
   360 fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
   361 
   362 qed_goal "fix_eq4" thy "f = fix`F ==> f = F`f"
   363  (fn prems =>
   364         [
   365         (cut_facts_tac prems 1),
   366         (hyp_subst_tac 1),
   367         (rtac fix_eq 1)
   368         ]);
   369 
   370 qed_goal "fix_eq5" thy "f = fix`F ==> f`x = F`f`x"
   371  (fn prems =>
   372         [
   373         (rtac trans 1),
   374         (rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1),
   375         (rtac refl 1)
   376         ]);
   377 
   378 fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
   379 
   380 (* proves the unfolding theorem for function equations f = fix`... *)
   381 fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
   382         (rtac trans 1),
   383         (rtac (fixeq RS fix_eq4) 1),
   384         (rtac trans 1),
   385         (rtac beta_cfun 1),
   386         (Simp_tac 1)
   387         ]);
   388 
   389 (* proves the unfolding theorem for function definitions f == fix`... *)
   390 fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
   391         (rtac trans 1),
   392         (rtac (fix_eq2) 1),
   393         (rtac fixdef 1),
   394         (rtac beta_cfun 1),
   395         (Simp_tac 1)
   396         ]);
   397 
   398 (* proves an application case for a function from its unfolding thm *)
   399 fun case_prover thy unfold s = prove_goal thy s (fn prems => [
   400 	(cut_facts_tac prems 1),
   401 	(rtac trans 1),
   402 	(stac unfold 1),
   403 	Auto_tac
   404 	]);
   405 
   406 (* ------------------------------------------------------------------------ *)
   407 (* better access to definitions                                             *)
   408 (* ------------------------------------------------------------------------ *)
   409 
   410 
   411 qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
   412  (fn prems =>
   413         [
   414         (rtac ext 1),
   415         (rewtac Ifix_def),
   416         (rtac refl 1)
   417         ]);
   418 
   419 (* ------------------------------------------------------------------------ *)
   420 (* direct connection between fix and iteration without Ifix                 *)
   421 (* ------------------------------------------------------------------------ *)
   422 
   423 qed_goalw "fix_def2" thy [fix_def]
   424  "fix`F = lub(range(%i. iterate i F UU))"
   425  (fn prems =>
   426         [
   427         (fold_goals_tac [Ifix_def]),
   428         (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
   429         ]);
   430 
   431 
   432 (* ------------------------------------------------------------------------ *)
   433 (* Lemmas about admissibility and fixed point induction                     *)
   434 (* ------------------------------------------------------------------------ *)
   435 
   436 (* ------------------------------------------------------------------------ *)
   437 (* access to definitions                                                    *)
   438 (* ------------------------------------------------------------------------ *)
   439 
   440 qed_goalw "admI" thy [adm_def]
   441         "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
   442  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
   443 
   444 qed_goalw "admD" thy [adm_def]
   445         "!!P. [| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
   446  (fn prems => [fast_tac HOL_cs 1]);
   447 
   448 qed_goalw "admw_def2" thy [admw_def]
   449         "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
   450 \                        P (lub(range(%i. iterate i F UU))))"
   451  (fn prems =>
   452         [
   453         (rtac refl 1)
   454         ]);
   455 
   456 (* ------------------------------------------------------------------------ *)
   457 (* an admissible formula is also weak admissible                            *)
   458 (* ------------------------------------------------------------------------ *)
   459 
   460 qed_goalw "adm_impl_admw"  thy [admw_def] "!!P. adm(P)==>admw(P)"
   461  (fn prems =>
   462         [
   463         (strip_tac 1),
   464         (etac admD 1),
   465         (rtac chain_iterate 1),
   466         (atac 1)
   467         ]);
   468 
   469 (* ------------------------------------------------------------------------ *)
   470 (* fixed point induction                                                    *)
   471 (* ------------------------------------------------------------------------ *)
   472 
   473 qed_goal "fix_ind"  thy  
   474 "[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
   475  (fn prems =>
   476         [
   477         (cut_facts_tac prems 1),
   478         (stac fix_def2 1),
   479         (etac admD 1),
   480         (rtac chain_iterate 1),
   481         (rtac allI 1),
   482         (induct_tac "i" 1),
   483         (stac iterate_0 1),
   484         (atac 1),
   485         (stac iterate_Suc 1),
   486         (resolve_tac prems 1),
   487         (atac 1)
   488         ]);
   489 
   490 qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
   491 \       P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
   492         (cut_facts_tac prems 1),
   493 	(asm_simp_tac HOL_ss 1),
   494 	(etac fix_ind 1),
   495 	(atac 1),
   496 	(eresolve_tac prems 1)]);
   497 	
   498 (* ------------------------------------------------------------------------ *)
   499 (* computational induction for weak admissible formulae                     *)
   500 (* ------------------------------------------------------------------------ *)
   501 
   502 qed_goal "wfix_ind"  thy  
   503 "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
   504  (fn prems =>
   505         [
   506         (cut_facts_tac prems 1),
   507         (stac fix_def2 1),
   508         (rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
   509         (atac 1),
   510         (rtac allI 1),
   511         (etac spec 1)
   512         ]);
   513 
   514 qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
   515 \       !n. P(iterate n F UU) |] ==> P f" (fn prems => [
   516         (cut_facts_tac prems 1),
   517 	(asm_simp_tac HOL_ss 1),
   518 	(etac wfix_ind 1),
   519 	(atac 1)]);
   520 
   521 (* ------------------------------------------------------------------------ *)
   522 (* for chain-finite (easy) types every formula is admissible                *)
   523 (* ------------------------------------------------------------------------ *)
   524 
   525 qed_goalw "adm_max_in_chain"  thy  [adm_def]
   526 "!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
   527  (fn prems =>
   528         [
   529         (cut_facts_tac prems 1),
   530         (strip_tac 1),
   531         (rtac exE 1),
   532         (rtac mp 1),
   533         (etac spec 1),
   534         (atac 1),
   535         (stac (lub_finch1 RS thelubI) 1),
   536         (atac 1),
   537         (atac 1),
   538         (etac spec 1)
   539         ]);
   540 
   541 bind_thm ("adm_chfin" ,chfin RS adm_max_in_chain);
   542 
   543 (* ------------------------------------------------------------------------ *)
   544 (* some lemmata for functions with flat/chfin domain/range types	    *)
   545 (* ------------------------------------------------------------------------ *)
   546 
   547 qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
   548     (fn _ => [
   549 	strip_tac 1,
   550 	dtac chfin_Rep_CFunR 1,
   551 	eres_inst_tac [("x","s")] allE 1,
   552 	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
   553 
   554 (* adm_flat not needed any more, since it is a special case of adm_chfindom *)
   555 
   556 (* ------------------------------------------------------------------------ *)
   557 (* improved admisibility introduction                                       *)
   558 (* ------------------------------------------------------------------------ *)
   559 
   560 qed_goalw "admI2" thy [adm_def]
   561  "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
   562 \ ==> P(lub (range Y))) ==> adm P" 
   563  (fn prems => [
   564         strip_tac 1,
   565         etac increasing_chain_adm_lemma 1, atac 1,
   566         eresolve_tac prems 1, atac 1, atac 1]);
   567 
   568 
   569 (* ------------------------------------------------------------------------ *)
   570 (* admissibility of special formulae and propagation                        *)
   571 (* ------------------------------------------------------------------------ *)
   572 
   573 qed_goalw "adm_less"  thy [adm_def]
   574         "[|cont u;cont v|]==> adm(%x. u x << v x)"
   575  (fn prems =>
   576         [
   577         (cut_facts_tac prems 1),
   578         (strip_tac 1),
   579         (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   580         (atac 1),
   581         (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   582         (atac 1),
   583         (rtac lub_mono 1),
   584         (cut_facts_tac prems 1),
   585         (etac (cont2mono RS ch2ch_monofun) 1),
   586         (atac 1),
   587         (cut_facts_tac prems 1),
   588         (etac (cont2mono RS ch2ch_monofun) 1),
   589         (atac 1),
   590         (atac 1)
   591         ]);
   592 Addsimps [adm_less];
   593 
   594 qed_goal "adm_conj"  thy  
   595         "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)"
   596  (fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
   597 Addsimps [adm_conj];
   598 
   599 qed_goalw "adm_not_free"  thy [adm_def] "adm(%x. t)"
   600  (fn prems => [fast_tac HOL_cs 1]);
   601 Addsimps [adm_not_free];
   602 
   603 qed_goalw "adm_not_less"  thy [adm_def]
   604         "!!t. cont t ==> adm(%x.~ (t x) << u)"
   605  (fn prems =>
   606         [
   607         (strip_tac 1),
   608         (rtac contrapos 1),
   609         (etac spec 1),
   610         (rtac trans_less 1),
   611         (atac 2),
   612         (etac (cont2mono RS monofun_fun_arg) 1),
   613         (rtac is_ub_thelub 1),
   614         (atac 1)
   615         ]);
   616 
   617 qed_goal "adm_all" thy  
   618         "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
   619  (fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
   620 
   621 bind_thm ("adm_all2", allI RS adm_all);
   622 
   623 qed_goal "adm_subst"  thy  
   624         "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))"
   625  (fn prems =>
   626         [
   627         (rtac admI 1),
   628         (stac (cont2contlub RS contlubE RS spec RS mp) 1),
   629         (atac 1),
   630         (atac 1),
   631         (etac admD 1),
   632         (etac (cont2mono RS ch2ch_monofun) 1),
   633         (atac 1),
   634         (atac 1)
   635         ]);
   636 
   637 qed_goal "adm_UU_not_less"  thy "adm(%x.~ UU << t(x))"
   638  (fn prems => [Simp_tac 1]);
   639 
   640 qed_goalw "adm_not_UU"  thy [adm_def] 
   641         "!!t. cont(t)==> adm(%x.~ (t x) = UU)"
   642  (fn prems =>
   643         [
   644         (strip_tac 1),
   645         (rtac contrapos 1),
   646         (etac spec 1),
   647         (rtac (chain_UU_I RS spec) 1),
   648         (rtac (cont2mono RS ch2ch_monofun) 1),
   649         (atac 1),
   650         (atac 1),
   651         (rtac (cont2contlub RS contlubE RS spec RS mp RS subst) 1),
   652         (atac 1),
   653         (atac 1),
   654         (atac 1)
   655         ]);
   656 
   657 qed_goal "adm_eq"  thy 
   658         "!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
   659  (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
   660 
   661 
   662 
   663 (* ------------------------------------------------------------------------ *)
   664 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
   665 (* ------------------------------------------------------------------------ *)
   666 
   667 local
   668 
   669   val adm_disj_lemma1 = prove_goal HOL.thy 
   670   "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
   671  (fn prems =>
   672         [
   673         (cut_facts_tac prems 1),
   674         (fast_tac HOL_cs 1)
   675         ]);
   676 
   677   val adm_disj_lemma2 = prove_goal thy  
   678   "!!Q. [| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
   679   \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
   680  (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
   681 
   682   val adm_disj_lemma3 = prove_goalw thy [chain]
   683   "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)"
   684  (fn _ =>
   685         [
   686         Asm_simp_tac 1,
   687         safe_tac HOL_cs,
   688         subgoal_tac "ia = i" 1,
   689         Asm_simp_tac 1,
   690         trans_tac 1
   691         ]);
   692 
   693   val adm_disj_lemma4 = prove_goal Nat.thy
   694   "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
   695  (fn _ =>
   696         [
   697         Asm_simp_tac 1,
   698         strip_tac 1,
   699         etac allE 1,
   700         etac mp 1,
   701         trans_tac 1
   702         ]);
   703 
   704   val adm_disj_lemma5 = prove_goal thy
   705   "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
   706   \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
   707  (fn prems =>
   708         [
   709         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
   710         atac 2,
   711         Asm_simp_tac 1,
   712         res_inst_tac [("x","i")] exI 1,
   713         strip_tac 1,
   714         trans_tac 1
   715         ]);
   716 
   717   val adm_disj_lemma6 = prove_goal thy
   718   "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
   719   \         ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
   720  (fn prems =>
   721         [
   722         (cut_facts_tac prems 1),
   723         (etac exE 1),
   724         (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
   725         (rtac conjI 1),
   726         (rtac adm_disj_lemma3 1),
   727         (atac 1),
   728         (rtac conjI 1),
   729         (rtac adm_disj_lemma4 1),
   730         (atac 1),
   731         (rtac adm_disj_lemma5 1),
   732         (atac 1),
   733         (atac 1)
   734         ]);
   735 
   736   val adm_disj_lemma7 = prove_goal thy 
   737   "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
   738   \         chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
   739  (fn prems =>
   740         [
   741         (cut_facts_tac prems 1),
   742         (rtac chainI 1),
   743         (rtac allI 1),
   744         (rtac chain_mono3 1),
   745         (atac 1),
   746         (rtac Least_le 1),
   747         (rtac conjI 1),
   748         (rtac Suc_lessD 1),
   749         (etac allE 1),
   750         (etac exE 1),
   751         (rtac (LeastI RS conjunct1) 1),
   752         (atac 1),
   753         (etac allE 1),
   754         (etac exE 1),
   755         (rtac (LeastI RS conjunct2) 1),
   756         (atac 1)
   757         ]);
   758 
   759   val adm_disj_lemma8 = prove_goal thy 
   760   "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
   761  (fn prems =>
   762         [
   763         (cut_facts_tac prems 1),
   764         (strip_tac 1),
   765         (etac allE 1),
   766         (etac exE 1),
   767         (etac (LeastI RS conjunct2) 1)
   768         ]);
   769 
   770   val adm_disj_lemma9 = prove_goal thy
   771   "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   772   \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
   773  (fn prems =>
   774         [
   775         (cut_facts_tac prems 1),
   776         (rtac antisym_less 1),
   777         (rtac lub_mono 1),
   778         (atac 1),
   779         (rtac adm_disj_lemma7 1),
   780         (atac 1),
   781         (atac 1),
   782         (strip_tac 1),
   783         (rtac (chain_mono RS mp) 1),
   784         (atac 1),
   785         (etac allE 1),
   786         (etac exE 1),
   787         (rtac (LeastI RS conjunct1) 1),
   788         (atac 1),
   789         (rtac lub_mono3 1),
   790         (rtac adm_disj_lemma7 1),
   791         (atac 1),
   792         (atac 1),
   793         (atac 1),
   794         (strip_tac 1),
   795         (rtac exI 1),
   796         (rtac (chain_mono RS mp) 1),
   797         (atac 1),
   798         (rtac lessI 1)
   799         ]);
   800 
   801   val adm_disj_lemma10 = prove_goal thy
   802   "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   803   \         ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
   804  (fn prems =>
   805         [
   806         (cut_facts_tac prems 1),
   807         (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
   808         (rtac conjI 1),
   809         (rtac adm_disj_lemma7 1),
   810         (atac 1),
   811         (atac 1),
   812         (rtac conjI 1),
   813         (rtac adm_disj_lemma8 1),
   814         (atac 1),
   815         (rtac adm_disj_lemma9 1),
   816         (atac 1),
   817         (atac 1)
   818         ]);
   819 
   820   val adm_disj_lemma12 = prove_goal thy
   821   "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
   822  (fn prems =>
   823         [
   824         (cut_facts_tac prems 1),
   825         (etac adm_disj_lemma2 1),
   826         (etac adm_disj_lemma6 1),
   827         (atac 1)
   828         ]);
   829 
   830 in
   831 
   832 val adm_lemma11 = prove_goal thy
   833 "[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
   834  (fn prems =>
   835         [
   836         (cut_facts_tac prems 1),
   837         (etac adm_disj_lemma2 1),
   838         (etac adm_disj_lemma10 1),
   839         (atac 1)
   840         ]);
   841 
   842 val adm_disj = prove_goal thy  
   843         "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
   844  (fn prems =>
   845         [
   846         (rtac admI 1),
   847         (rtac (adm_disj_lemma1 RS disjE) 1),
   848         (atac 1),
   849         (rtac disjI2 1),
   850         (etac adm_disj_lemma12 1),
   851         (atac 1),
   852         (atac 1),
   853         (rtac disjI1 1),
   854         (etac adm_lemma11 1),
   855         (atac 1),
   856         (atac 1)
   857         ]);
   858 
   859 end;
   860 
   861 bind_thm("adm_lemma11",adm_lemma11);
   862 bind_thm("adm_disj",adm_disj);
   863 
   864 qed_goal "adm_imp"  thy  
   865         "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)" (K [
   866         (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
   867          (etac ssubst 1),
   868          (etac adm_disj 1),
   869          (atac 1),
   870         (Simp_tac 1)
   871         ]);
   872 
   873 Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
   874 \           ==> adm (%x. P x = Q x)";
   875 by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
   876 by (Asm_simp_tac 1);
   877 by (rtac ext 1);
   878 by (fast_tac HOL_cs 1);
   879 qed"adm_iff";
   880 
   881 
   882 qed_goal "adm_not_conj"  thy  
   883 "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
   884         cut_facts_tac prems 1,
   885         subgoal_tac 
   886         "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
   887         rtac ext 2,
   888         fast_tac HOL_cs 2,
   889         etac ssubst 1,
   890         etac adm_disj 1,
   891         atac 1]);
   892 
   893 val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
   894         adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less,
   895         adm_iff];
   896 
   897 Addsimps adm_lemmas;