isabelle: src/HOLCF/Fix.ML@645f46a24c72

     1 (*  Title:      HOLCF/Fix.ML

     2     ID:         $Id$

     3     Author:     Franz Regensburger

     4     Copyright   1993  Technische Universitaet Muenchen

     6 Lemmas for Fix.thy

     7 *)

     9 open Fix;

    11 (* ------------------------------------------------------------------------ *)

    12 (* derive inductive properties of iterate from primitive recursion          *)

    13 (* ------------------------------------------------------------------------ *)

    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         ]);

    26 (* ------------------------------------------------------------------------ *)

    27 (* the sequence of function itertaions is a chain                           *)

    28 (* This property is essential since monotonicity of iterate makes no sense  *)

    29 (* ------------------------------------------------------------------------ *)

    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         ]);

    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         ]);

    54 (* ------------------------------------------------------------------------ *)

    55 (* Kleene's fixed point theorems for continuous functions in pointed        *)

    56 (* omega cpo's                                                              *)

    57 (* ------------------------------------------------------------------------ *)

    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         ]);

    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         ]);

   101 (* ------------------------------------------------------------------------ *)

   102 (* monotonicity and continuity of iterate                                   *)

   103 (* ------------------------------------------------------------------------ *)

   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         ]);

   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 (* ------------------------------------------------------------------------ *)

   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         ]);

   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         ]);

   165 (* ------------------------------------------------------------------------ *)

   166 (* a lemma about continuity of iterate in its third argument                *)

   167 (* ------------------------------------------------------------------------ *)

   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         ]);

   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         ]);

   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         ]);

   203 (* ------------------------------------------------------------------------ *)

   204 (* monotonicity and continuity of Ifix                                      *)

   205 (* ------------------------------------------------------------------------ *)

   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         ]);

   219 (* ------------------------------------------------------------------------ *)

   220 (* since iterate is not monotone in its first argument, special lemmas must *)

   221 (* be derived for lubs in this argument                                     *)

   222 (* ------------------------------------------------------------------------ *)

   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         ]);

   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 (* ------------------------------------------------------------------------ *)

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   312 (* ------------------------------------------------------------------------ *)

   313 (* propagate properties of Ifix to its continuous counterpart               *)

   314 (* ------------------------------------------------------------------------ *)

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   360 fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));

   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         ]);

   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         ]);

   378 fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i));

   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         ]);

   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         ]);

   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 	]);

   406 (* ------------------------------------------------------------------------ *)

   407 (* better access to definitions                                             *)

   408 (* ------------------------------------------------------------------------ *)

   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         ]);

   419 (* ------------------------------------------------------------------------ *)

   420 (* direct connection between fix and iteration without Ifix                 *)

   421 (* ------------------------------------------------------------------------ *)

   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         ]);

   432 (* ------------------------------------------------------------------------ *)

   433 (* Lemmas about admissibility and fixed point induction                     *)

   434 (* ------------------------------------------------------------------------ *)

   436 (* ------------------------------------------------------------------------ *)

   437 (* access to definitions                                                    *)

   438 (* ------------------------------------------------------------------------ *)

   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]);

   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]);

   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         ]);

   456 (* ------------------------------------------------------------------------ *)

   457 (* an admissible formula is also weak admissible                            *)

   458 (* ------------------------------------------------------------------------ *)

   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         ]);

   469 (* ------------------------------------------------------------------------ *)

   470 (* fixed point induction                                                    *)

   471 (* ------------------------------------------------------------------------ *)

   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         ]);

   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)]);

   498 (* ------------------------------------------------------------------------ *)

   499 (* computational induction for weak admissible formulae                     *)

   500 (* ------------------------------------------------------------------------ *)

   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         ]);

   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)]);

   521 (* ------------------------------------------------------------------------ *)

   522 (* for chain-finite (easy) types every formula is admissible                *)

   523 (* ------------------------------------------------------------------------ *)

   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         ]);

   541 bind_thm ("adm_chfin" ,chfin RS adm_max_in_chain);

   543 (* ------------------------------------------------------------------------ *)

   544 (* some lemmata for functions with flat/chfin domain/range types	    *)

   545 (* ------------------------------------------------------------------------ *)

   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]);

   554 (* adm_flat not needed any more, since it is a special case of adm_chfindom *)

   556 (* ------------------------------------------------------------------------ *)

   557 (* improved admisibility introduction                                       *)

   558 (* ------------------------------------------------------------------------ *)

   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]);

   569 (* ------------------------------------------------------------------------ *)

   570 (* admissibility of special formulae and propagation                        *)

   571 (* ------------------------------------------------------------------------ *)

   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];

   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];

   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];

   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         ]);

   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]);

   621 bind_thm ("adm_all2", allI RS adm_all);

   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         ]);

   637 qed_goal "adm_UU_not_less"  thy "adm(%x.~ UU << t(x))"

   638  (fn prems => [Simp_tac 1]);

   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         ]);

   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]);

   663 (* ------------------------------------------------------------------------ *)

   664 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)

   665 (* ------------------------------------------------------------------------ *)

   667 local

   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         ]);

   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]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   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         ]);

   830 in

   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         ]);

   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         ]);

   859 end;

   861 bind_thm("adm_lemma11",adm_lemma11);

   862 bind_thm("adm_disj",adm_disj);

   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         ]);

   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";

   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]);

   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];

   897 Addsimps adm_lemmas;

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--