src/HOLCF/Cont.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5297 410417e0fd04
child 7322 d16d7ddcc842
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Cont.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Cont.thy 
     7 *)
     8 
     9 open Cont;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* access to definition                                                     *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "contlubI" thy [contlub]
    16         "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
    17 \        contlub(f)"
    18 (fn prems =>
    19         [
    20         (cut_facts_tac prems 1),
    21         (atac 1)
    22         ]);
    23 
    24 qed_goalw "contlubE" thy [contlub]
    25         " contlub(f)==>\
    26 \         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
    27 (fn prems =>
    28         [
    29         (cut_facts_tac prems 1),
    30         (atac 1)
    31         ]);
    32 
    33 
    34 qed_goalw "contI" thy [cont]
    35  "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
    36 (fn prems =>
    37         [
    38         (cut_facts_tac prems 1),
    39         (atac 1)
    40         ]);
    41 
    42 qed_goalw "contE" thy [cont]
    43  "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    44 (fn prems =>
    45         [
    46         (cut_facts_tac prems 1),
    47         (atac 1)
    48         ]);
    49 
    50 
    51 qed_goalw "monofunI" thy [monofun]
    52         "! x y. x << y --> f(x) << f(y) ==> monofun(f)"
    53 (fn prems =>
    54         [
    55         (cut_facts_tac prems 1),
    56         (atac 1)
    57         ]);
    58 
    59 qed_goalw "monofunE" thy [monofun]
    60         "monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
    61 (fn prems =>
    62         [
    63         (cut_facts_tac prems 1),
    64         (atac 1)
    65         ]);
    66 
    67 (* ------------------------------------------------------------------------ *)
    68 (* the main purpose of cont.thy is to show:                                 *)
    69 (*              monofun(f) & contlub(f)  <==> cont(f)                      *)
    70 (* ------------------------------------------------------------------------ *)
    71 
    72 (* ------------------------------------------------------------------------ *)
    73 (* monotone functions map chains to chains                                  *)
    74 (* ------------------------------------------------------------------------ *)
    75 
    76 qed_goal "ch2ch_monofun" thy 
    77         "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
    78 (fn prems =>
    79         [
    80         (cut_facts_tac prems 1),
    81         (rtac chainI 1),
    82         (rtac allI 1),
    83         (etac (monofunE RS spec RS spec RS mp) 1),
    84         (etac (chainE RS spec) 1)
    85         ]);
    86 
    87 (* ------------------------------------------------------------------------ *)
    88 (* monotone functions map upper bound to upper bounds                       *)
    89 (* ------------------------------------------------------------------------ *)
    90 
    91 qed_goal "ub2ub_monofun" thy 
    92  "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)"
    93 (fn prems =>
    94         [
    95         (cut_facts_tac prems 1),
    96         (rtac ub_rangeI 1),
    97         (rtac allI 1),
    98         (etac (monofunE RS spec RS spec RS mp) 1),
    99         (etac (ub_rangeE RS spec) 1)
   100         ]);
   101 
   102 (* ------------------------------------------------------------------------ *)
   103 (* left to right: monofun(f) & contlub(f)  ==> cont(f)                     *)
   104 (* ------------------------------------------------------------------------ *)
   105 
   106 qed_goalw "monocontlub2cont" thy [cont]
   107         "[|monofun(f);contlub(f)|] ==> cont(f)"
   108 (fn prems =>
   109         [
   110         (cut_facts_tac prems 1),
   111         (strip_tac 1),
   112         (rtac thelubE 1),
   113         (etac ch2ch_monofun 1),
   114         (atac 1),
   115         (etac (contlubE RS spec RS mp RS sym) 1),
   116         (atac 1)
   117         ]);
   118 
   119 (* ------------------------------------------------------------------------ *)
   120 (* first a lemma about binary chains                                        *)
   121 (* ------------------------------------------------------------------------ *)
   122 
   123 qed_goal "binchain_cont" thy
   124 "[| cont(f); x << y |]  ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
   125 (fn prems => 
   126         [
   127         (cut_facts_tac prems 1),
   128         (rtac subst 1), 
   129         (etac (contE RS spec RS mp) 2),
   130         (etac bin_chain 2),
   131         (res_inst_tac [("y","y")] arg_cong 1),
   132         (etac (lub_bin_chain RS thelubI) 1)
   133         ]);
   134 
   135 (* ------------------------------------------------------------------------ *)
   136 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
   137 (* part1:         cont(f) ==> monofun(f                                    *)
   138 (* ------------------------------------------------------------------------ *)
   139 
   140 qed_goalw "cont2mono" thy [monofun]
   141         "cont(f) ==> monofun(f)"
   142 (fn prems =>
   143         [
   144         (cut_facts_tac prems 1),
   145         (strip_tac 1),
   146         (res_inst_tac [("s","if 0 = 0 then x else y")] subst 1),
   147         (rtac (binchain_cont RS is_ub_lub) 2),
   148         (atac 2),
   149         (atac 2),
   150         (Simp_tac 1)
   151         ]);
   152 
   153 (* ------------------------------------------------------------------------ *)
   154 (* right to left: cont(f) ==> monofun(f) & contlub(f)                      *)
   155 (* part2:         cont(f) ==>              contlub(f)                      *)
   156 (* ------------------------------------------------------------------------ *)
   157 
   158 qed_goalw "cont2contlub" thy [contlub]
   159         "cont(f) ==> contlub(f)"
   160 (fn prems =>
   161         [
   162         (cut_facts_tac prems 1),
   163         (strip_tac 1),
   164         (rtac (thelubI RS sym) 1),
   165         (etac (contE RS spec RS mp) 1),
   166         (atac 1)
   167         ]);
   168 
   169 (* ------------------------------------------------------------------------ *)
   170 (* monotone functions map finite chains to finite chains              	    *)
   171 (* ------------------------------------------------------------------------ *)
   172 
   173 qed_goalw "monofun_finch2finch" thy [finite_chain_def]
   174   "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" 
   175 (fn prems => 
   176 	[
   177 	cut_facts_tac prems 1,
   178 	safe_tac HOL_cs,
   179 	fast_tac (HOL_cs addSEs [ch2ch_monofun]) 1,
   180 	fast_tac (HOL_cs addss (HOL_ss addsimps [max_in_chain_def])) 1
   181 	]);
   182 
   183 (* ------------------------------------------------------------------------ *)
   184 (* The same holds for continuous functions				    *)
   185 (* ------------------------------------------------------------------------ *)
   186 
   187 bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch);
   188 (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *)
   189 
   190 
   191 (* ------------------------------------------------------------------------ *)
   192 (* The following results are about a curried function that is monotone      *)
   193 (* in both arguments                                                        *)
   194 (* ------------------------------------------------------------------------ *)
   195 
   196 qed_goal "ch2ch_MF2L" thy 
   197 "[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
   198 (fn prems =>
   199         [
   200         (cut_facts_tac prems 1),
   201         (etac (ch2ch_monofun RS ch2ch_fun) 1),
   202         (atac 1)
   203         ]);
   204 
   205 
   206 qed_goal "ch2ch_MF2R" thy 
   207 "[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
   208 (fn prems =>
   209         [
   210         (cut_facts_tac prems 1),
   211         (etac ch2ch_monofun 1),
   212         (atac 1)
   213         ]);
   214 
   215 qed_goal "ch2ch_MF2LR" thy 
   216 "[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
   217 \  chain(%i. MF2(F(i))(Y(i)))"
   218  (fn prems =>
   219         [
   220         (cut_facts_tac prems 1),
   221         (rtac chainI 1),
   222         (strip_tac 1 ),
   223         (rtac trans_less 1),
   224         (etac (ch2ch_MF2L RS chainE RS spec) 1),
   225         (atac 1),
   226         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
   227         (etac (chainE RS spec) 1)
   228         ]);
   229 
   230 
   231 qed_goal "ch2ch_lubMF2R" thy 
   232 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   233 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   234 \       chain(F);chain(Y)|] ==> \
   235 \       chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
   236 (fn prems =>
   237         [
   238         (cut_facts_tac prems 1),
   239         (rtac (lub_mono RS allI RS chainI) 1),
   240         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   241         (atac 1),
   242         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   243         (atac 1),
   244         (strip_tac 1),
   245         (rtac (chainE RS spec) 1),
   246         (etac ch2ch_MF2L 1),
   247         (atac 1)
   248         ]);
   249 
   250 
   251 qed_goal "ch2ch_lubMF2L" thy 
   252 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   253 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   254 \       chain(F);chain(Y)|] ==> \
   255 \       chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
   256 (fn prems =>
   257         [
   258         (cut_facts_tac prems 1),
   259         (rtac (lub_mono RS allI RS chainI) 1),
   260         (etac ch2ch_MF2L 1),
   261         (atac 1),
   262         (etac ch2ch_MF2L 1),
   263         (atac 1),
   264         (strip_tac 1),
   265         (rtac (chainE RS spec) 1),
   266         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   267         (atac 1)
   268         ]);
   269 
   270 
   271 qed_goal "lub_MF2_mono" thy 
   272 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   273 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   274 \       chain(F)|] ==> \
   275 \       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
   276 (fn prems =>
   277         [
   278         (cut_facts_tac prems 1),
   279         (rtac monofunI 1),
   280         (strip_tac 1),
   281         (rtac lub_mono 1),
   282         (etac ch2ch_MF2L 1),
   283         (atac 1),
   284         (etac ch2ch_MF2L 1),
   285         (atac 1),
   286         (strip_tac 1),
   287         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
   288         (atac 1)
   289         ]);
   290 
   291 qed_goal "ex_lubMF2" thy 
   292 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   293 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   294 \       chain(F); chain(Y)|] ==> \
   295 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
   296 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
   297  (fn prems =>
   298         [
   299         (cut_facts_tac prems 1),
   300         (rtac antisym_less 1),
   301         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
   302         (etac ch2ch_lubMF2R 1),
   303         (REPEAT (atac 1)),
   304         (strip_tac 1),
   305         (rtac lub_mono 1),
   306         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   307         (atac 1),
   308         (etac ch2ch_lubMF2L 1),
   309         (REPEAT (atac 1)),
   310         (strip_tac 1),
   311         (rtac is_ub_thelub 1),
   312         (etac ch2ch_MF2L 1),
   313         (atac 1),
   314         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
   315         (etac ch2ch_lubMF2L 1),
   316         (REPEAT (atac 1)),
   317         (strip_tac 1),
   318         (rtac lub_mono 1),
   319         (etac ch2ch_MF2L 1),
   320         (atac 1),
   321         (etac ch2ch_lubMF2R 1),
   322         (REPEAT (atac 1)),
   323         (strip_tac 1),
   324         (rtac is_ub_thelub 1),
   325         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   326         (atac 1)
   327         ]);
   328 
   329 
   330 qed_goal "diag_lubMF2_1" thy 
   331 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   332 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   333 \  chain(FY);chain(TY)|] ==>\
   334 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
   335 \ lub(range(%i. MF2(FY(i))(TY(i))))"
   336  (fn prems =>
   337         [
   338         (cut_facts_tac prems 1),
   339         (rtac antisym_less 1),
   340         (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
   341         (etac ch2ch_lubMF2L 1),
   342         (REPEAT (atac 1)),
   343         (strip_tac 1 ),
   344         (rtac lub_mono3 1),
   345         (etac ch2ch_MF2L 1),
   346         (REPEAT (atac 1)),
   347         (etac ch2ch_MF2LR 1),
   348         (REPEAT (atac 1)),
   349         (rtac allI 1),
   350         (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   351         (res_inst_tac [("x","ia")] exI 1),
   352         (rtac (chain_mono RS mp) 1),
   353         (etac allE 1),
   354         (etac ch2ch_MF2R 1),
   355         (REPEAT (atac 1)),
   356         (hyp_subst_tac 1),
   357         (res_inst_tac [("x","ia")] exI 1),
   358         (rtac refl_less 1),
   359         (res_inst_tac [("x","i")] exI 1),
   360         (rtac (chain_mono RS mp) 1),
   361         (etac ch2ch_MF2L 1),
   362         (REPEAT (atac 1)),
   363         (rtac lub_mono 1),
   364         (etac ch2ch_MF2LR 1),
   365         (REPEAT(atac 1)),
   366         (etac ch2ch_lubMF2L 1),
   367         (REPEAT (atac 1)),
   368         (strip_tac 1 ),
   369         (rtac is_ub_thelub 1),
   370         (etac ch2ch_MF2L 1),
   371         (atac 1)
   372         ]);
   373 
   374 qed_goal "diag_lubMF2_2" thy 
   375 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   376 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   377 \  chain(FY);chain(TY)|] ==>\
   378 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
   379 \ lub(range(%i. MF2(FY(i))(TY(i))))"
   380  (fn prems =>
   381         [
   382         (cut_facts_tac prems 1),
   383         (rtac trans 1),
   384         (rtac ex_lubMF2 1),
   385         (REPEAT (atac 1)),
   386         (etac diag_lubMF2_1 1),
   387         (REPEAT (atac 1))
   388         ]);
   389 
   390 
   391 (* ------------------------------------------------------------------------ *)
   392 (* The following results are about a curried function that is continuous    *)
   393 (* in both arguments                                                        *)
   394 (* ------------------------------------------------------------------------ *)
   395 
   396 qed_goal "contlub_CF2" thy 
   397 "[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
   398 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
   399  (fn prems =>
   400         [
   401         (cut_facts_tac prems 1),
   402         (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
   403         (atac 1),
   404         (stac thelub_fun 1),
   405         (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
   406         (atac 1),
   407         (rtac trans 1),
   408         (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS                spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   409         (atac 1),
   410         (rtac diag_lubMF2_2 1),
   411         (etac cont2mono 1),
   412         (rtac allI 1),
   413         (etac allE 1),
   414         (etac cont2mono 1),
   415         (REPEAT (atac 1))
   416         ]);
   417 
   418 (* ------------------------------------------------------------------------ *)
   419 (* The following results are about application for functions in 'a=>'b      *)
   420 (* ------------------------------------------------------------------------ *)
   421 
   422 qed_goal "monofun_fun_fun" thy 
   423         "f1 << f2 ==> f1(x) << f2(x)"
   424 (fn prems =>
   425         [
   426         (cut_facts_tac prems 1),
   427         (etac (less_fun RS iffD1 RS spec) 1)
   428         ]);
   429 
   430 qed_goal "monofun_fun_arg" thy 
   431         "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
   432 (fn prems =>
   433         [
   434         (cut_facts_tac prems 1),
   435         (etac (monofunE RS spec RS spec RS mp) 1),
   436         (atac 1)
   437         ]);
   438 
   439 qed_goal "monofun_fun" thy 
   440 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
   441 (fn prems =>
   442         [
   443         (cut_facts_tac prems 1),
   444         (rtac trans_less 1),
   445         (etac monofun_fun_arg 1),
   446         (atac 1),
   447         (etac monofun_fun_fun 1)
   448         ]);
   449 
   450 
   451 (* ------------------------------------------------------------------------ *)
   452 (* The following results are about the propagation of monotonicity and      *)
   453 (* continuity                                                               *)
   454 (* ------------------------------------------------------------------------ *)
   455 
   456 qed_goal "mono2mono_MF1L" thy 
   457         "[|monofun(c1)|] ==> monofun(%x. c1 x y)"
   458 (fn prems =>
   459         [
   460         (cut_facts_tac prems 1),
   461         (rtac monofunI 1),
   462         (strip_tac 1),
   463         (etac (monofun_fun_arg RS monofun_fun_fun) 1),
   464         (atac 1)
   465         ]);
   466 
   467 qed_goal "cont2cont_CF1L" thy 
   468         "[|cont(c1)|] ==> cont(%x. c1 x y)"
   469 (fn prems =>
   470         [
   471         (cut_facts_tac prems 1),
   472         (rtac monocontlub2cont 1),
   473         (etac (cont2mono RS mono2mono_MF1L) 1),
   474         (rtac contlubI 1),
   475         (strip_tac 1),
   476         (rtac ((hd prems) RS cont2contlub RS 
   477                 contlubE RS spec RS mp RS ssubst) 1),
   478         (atac 1),
   479         (stac thelub_fun 1),
   480         (rtac ch2ch_monofun 1),
   481         (etac cont2mono 1),
   482         (atac 1),
   483         (rtac refl 1)
   484         ]);
   485 
   486 (*********  Note "(%x.%y.c1 x y) = c1" ***********)
   487 
   488 qed_goal "mono2mono_MF1L_rev" thy
   489         "!y. monofun(%x. c1 x y) ==> monofun(c1)"
   490 (fn prems =>
   491         [
   492         (cut_facts_tac prems 1),
   493         (rtac monofunI 1),
   494         (strip_tac 1),
   495         (rtac (less_fun RS iffD2) 1),
   496         (strip_tac 1),
   497         (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
   498         (atac 1)
   499         ]);
   500 
   501 qed_goal "cont2cont_CF1L_rev" thy
   502         "!y. cont(%x. c1 x y) ==> cont(c1)"
   503 (fn prems =>
   504         [
   505         (cut_facts_tac prems 1),
   506         (rtac monocontlub2cont 1),
   507         (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1),
   508         (etac spec 1),
   509         (rtac contlubI 1),
   510         (strip_tac 1),
   511         (rtac ext 1),
   512         (stac thelub_fun 1),
   513         (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
   514         (etac spec 1),
   515         (atac 1),
   516         (rtac 
   517         ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1),
   518         (atac 1)
   519         ]);
   520 
   521 (* ------------------------------------------------------------------------ *)
   522 (* What D.A.Schmidt calls continuity of abstraction                         *)
   523 (* never used here                                                          *)
   524 (* ------------------------------------------------------------------------ *)
   525 
   526 qed_goal "contlub_abstraction" thy
   527 "[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
   528 \ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
   529  (fn prems =>
   530         [
   531         (cut_facts_tac prems 1),
   532         (rtac trans 1),
   533         (rtac (cont2contlub RS contlubE RS spec RS mp) 2),
   534         (atac 3),
   535         (etac cont2cont_CF1L_rev 2),
   536         (rtac ext 1), 
   537         (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1),
   538         (etac spec 1),
   539         (atac 1)
   540         ]);
   541 
   542 qed_goal "mono2mono_app" thy 
   543 "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
   544 \        monofun(%x.(ft(x))(tt(x)))"
   545  (fn prems =>
   546         [
   547         (cut_facts_tac prems 1),
   548         (rtac monofunI 1),
   549         (strip_tac 1),
   550         (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1),
   551         (etac spec 1),
   552         (etac spec 1),
   553         (etac (monofunE RS spec RS spec RS mp) 1),
   554         (atac 1),
   555         (etac (monofunE RS spec RS spec RS mp) 1),
   556         (atac 1)
   557         ]);
   558 
   559 
   560 qed_goal "cont2contlub_app" thy 
   561 "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
   562  (fn prems =>
   563         [
   564         (cut_facts_tac prems 1),
   565         (rtac contlubI 1),
   566         (strip_tac 1),
   567         (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
   568         (etac cont2contlub 1),
   569         (atac 1),
   570         (rtac contlub_CF2 1),
   571         (REPEAT (atac 1)),
   572         (etac (cont2mono RS ch2ch_monofun) 1),
   573         (atac 1)
   574         ]);
   575 
   576 
   577 qed_goal "cont2cont_app" thy 
   578 "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==>\
   579 \        cont(%x.(ft(x))(tt(x)))"
   580  (fn prems =>
   581         [
   582         (rtac monocontlub2cont 1),
   583         (rtac mono2mono_app 1),
   584         (rtac cont2mono 1),
   585         (resolve_tac prems 1),
   586         (strip_tac 1),
   587         (rtac cont2mono 1),
   588         (cut_facts_tac prems 1),
   589         (etac spec 1),
   590         (rtac cont2mono 1),
   591         (resolve_tac prems 1),
   592         (rtac cont2contlub_app 1),
   593         (resolve_tac prems 1),
   594         (resolve_tac prems 1),
   595         (resolve_tac prems 1)
   596         ]);
   597 
   598 
   599 bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
   600 (*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
   601 (*        cont (%x. ?ft x (?tt x))                    *)
   602 
   603 
   604 (* ------------------------------------------------------------------------ *)
   605 (* The identity function is continuous                                      *)
   606 (* ------------------------------------------------------------------------ *)
   607 
   608 qed_goal "cont_id" thy "cont(% x. x)"
   609  (fn prems =>
   610         [
   611         (rtac contI 1),
   612         (strip_tac 1),
   613         (etac thelubE 1),
   614         (rtac refl 1)
   615         ]);
   616 
   617 (* ------------------------------------------------------------------------ *)
   618 (* constant functions are continuous                                        *)
   619 (* ------------------------------------------------------------------------ *)
   620 
   621 qed_goalw "cont_const" thy [cont] "cont(%x. c)"
   622  (fn prems =>
   623         [
   624         (strip_tac 1),
   625         (rtac is_lubI 1),
   626         (rtac conjI 1),
   627         (rtac ub_rangeI 1),
   628         (strip_tac 1),
   629         (rtac refl_less 1),
   630         (strip_tac 1),
   631         (dtac ub_rangeE 1),
   632         (etac spec 1)
   633         ]);
   634 
   635 
   636 qed_goal "cont2cont_app3" thy 
   637  "[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
   638  (fn prems =>
   639         [
   640         (cut_facts_tac prems 1),
   641         (rtac cont2cont_app2 1),
   642         (rtac cont_const 1),
   643         (atac 1),
   644         (atac 1)
   645         ]);
   646 
   647 (* ------------------------------------------------------------------------ *)
   648 (* A non-emptyness result for Cfun                                          *)
   649 (* ------------------------------------------------------------------------ *)
   650 
   651 qed_goal "CfunI" thy "?x:Collect cont"
   652  (fn prems =>
   653         [
   654         (rtac CollectI 1),
   655         (rtac cont_const 1)
   656         ]);
   657 
   658 (* ------------------------------------------------------------------------ *)
   659 (* some properties of flat			 			    *)
   660 (* ------------------------------------------------------------------------ *)
   661 
   662 qed_goalw "flatdom2monofun" thy [monofun]
   663   "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" 
   664 (fn prems => 
   665 	[
   666 	cut_facts_tac prems 1,
   667 	strip_tac 1,
   668 	dtac (ax_flat RS spec RS spec RS mp) 1,
   669 	fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
   670 	]);
   671 
   672 
   673 Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
   674 by(rtac monocontlub2cont 1);
   675 by( atac 1);
   676 by(rtac contlubI 1);
   677 by(strip_tac 1);
   678 by(forward_tac [chfin2finch] 1);
   679 by(rtac antisym_less 1);
   680 by( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
   681                HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);
   682 by(dtac (monofun_finch2finch COMP swap_prems_rl) 1);
   683 by( atac 1);
   684 by(asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1);
   685 by(etac conjE 1);
   686 by(etac exE 1);
   687 by(asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1);
   688 by(etac (monofunE RS spec RS spec RS mp) 1);
   689 by(etac is_ub_thelub 1);
   690 qed "chfindom_monofun2cont";
   691 
   692 bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
   693 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)