src/HOLCF/cont.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     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 val contlubI = prove_goalw Cont.thy [contlub]
    16 	"! Y. is_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 val contlubE = prove_goalw Cont.thy [contlub]
    25 	" contlub(f)==>\
    26 \         ! Y. is_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 val contXI = prove_goalw Cont.thy [contX]
    35  "! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> contX(f)"
    36 (fn prems =>
    37 	[
    38 	(cut_facts_tac prems 1),
    39 	(atac 1)
    40 	]);
    41 
    42 val contXE = prove_goalw Cont.thy [contX]
    43  "contX(f) ==> ! Y. is_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 val monofunI = prove_goalw Cont.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 val monofunE = prove_goalw Cont.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)  <==> contX(f)                      *)
    70 (* ------------------------------------------------------------------------ *)
    71 
    72 (* ------------------------------------------------------------------------ *)
    73 (* monotone functions map chains to chains                                  *)
    74 (* ------------------------------------------------------------------------ *)
    75 
    76 val ch2ch_monofun= prove_goal Cont.thy 
    77 	"[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
    78 (fn prems =>
    79 	[
    80 	(cut_facts_tac prems 1),
    81 	(rtac is_chainI 1),
    82 	(rtac allI 1),
    83 	(etac (monofunE RS spec RS spec RS mp) 1),
    84 	(etac (is_chainE RS spec) 1)
    85 	]);
    86 
    87 (* ------------------------------------------------------------------------ *)
    88 (* monotone functions map upper bound to upper bounds                       *)
    89 (* ------------------------------------------------------------------------ *)
    90 
    91 val ub2ub_monofun = prove_goal Cont.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)  ==> contX(f)                     *)
   104 (* ------------------------------------------------------------------------ *)
   105 
   106 val monocontlub2contX = prove_goalw Cont.thy [contX]
   107 	"[|monofun(f);contlub(f)|] ==> contX(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 val binchain_contX =  prove_goal Cont.thy
   124 "[| contX(f); x << y |]  ==> range(%i. f(if(i = 0,x,y))) <<| f(y)"
   125 (fn prems => 
   126 	[
   127 	(cut_facts_tac prems 1),
   128 	(rtac subst 1), 
   129 	(etac (contXE 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: contX(f) ==> monofun(f) & contlub(f)                      *)
   137 (* part1:         contX(f) ==> monofun(f                                    *)
   138 (* ------------------------------------------------------------------------ *)
   139 
   140 val contX2mono =  prove_goalw Cont.thy [monofun]
   141 	"contX(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,x,y)")] subst 1),
   147 	(rtac (binchain_contX RS is_ub_lub) 2),
   148 	(atac 2),
   149 	(atac 2),
   150 	(simp_tac nat_ss 1)
   151 	]);
   152 
   153 (* ------------------------------------------------------------------------ *)
   154 (* right to left: contX(f) ==> monofun(f) & contlub(f)                      *)
   155 (* part2:         contX(f) ==>              contlub(f)                      *)
   156 (* ------------------------------------------------------------------------ *)
   157 
   158 val contX2contlub = prove_goalw Cont.thy [contlub]
   159 	"contX(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 (contXE RS spec RS mp) 1),
   166 	(atac 1)
   167 	]);
   168 
   169 (* ------------------------------------------------------------------------ *)
   170 (* The following results are about a curried function that is monotone      *)
   171 (* in both arguments                                                        *)
   172 (* ------------------------------------------------------------------------ *)
   173 
   174 val ch2ch_MF2L = prove_goal Cont.thy 
   175 "[|monofun(MF2::('a::po=>'b::po=>'c::po));\
   176 \	is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
   177 (fn prems =>
   178 	[
   179 	(cut_facts_tac prems 1),
   180 	(etac (ch2ch_monofun RS ch2ch_fun) 1),
   181 	(atac 1)
   182 	]);
   183 
   184 
   185 val ch2ch_MF2R = prove_goal Cont.thy "[|monofun(MF2(f)::('b::po=>'c::po));\
   186 \	is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
   187 (fn prems =>
   188 	[
   189 	(cut_facts_tac prems 1),
   190 	(etac ch2ch_monofun 1),
   191 	(atac 1)
   192 	]);
   193 
   194 val ch2ch_MF2LR = prove_goal Cont.thy 
   195 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   196 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   197 \	is_chain(F); is_chain(Y)|] ==> \
   198 \  is_chain(%i. MF2(F(i))(Y(i)))"
   199 (fn prems =>
   200 	[
   201 	(cut_facts_tac prems 1),
   202 	(rtac is_chainI 1),
   203 	(strip_tac 1 ),
   204 	(rtac trans_less 1),
   205 	(etac (ch2ch_MF2L RS is_chainE RS spec) 1),
   206 	(atac 1),
   207 	((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
   208 	(etac (is_chainE RS spec) 1)
   209 	]);
   210 
   211 val ch2ch_lubMF2R = prove_goal Cont.thy 
   212 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   213 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   214 \	is_chain(F);is_chain(Y)|] ==> \
   215 \	is_chain(%j. lub(range(%i. MF2(F(j),Y(i)))))"
   216 (fn prems =>
   217 	[
   218 	(cut_facts_tac prems 1),
   219 	(rtac (lub_mono RS allI RS is_chainI) 1),
   220 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   221 	(atac 1),
   222 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   223 	(atac 1),
   224 	(strip_tac 1),
   225 	(rtac (is_chainE RS spec) 1),
   226 	(etac ch2ch_MF2L 1),
   227 	(atac 1)
   228 	]);
   229 
   230 
   231 val ch2ch_lubMF2L = prove_goal Cont.thy 
   232 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   233 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   234 \	is_chain(F);is_chain(Y)|] ==> \
   235 \	is_chain(%i. lub(range(%j. MF2(F(j),Y(i)))))"
   236 (fn prems =>
   237 	[
   238 	(cut_facts_tac prems 1),
   239 	(rtac (lub_mono RS allI RS is_chainI) 1),
   240 	(etac ch2ch_MF2L 1),
   241 	(atac 1),
   242 	(etac ch2ch_MF2L 1),
   243 	(atac 1),
   244 	(strip_tac 1),
   245 	(rtac (is_chainE RS spec) 1),
   246 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   247 	(atac 1)
   248 	]);
   249 
   250 
   251 val lub_MF2_mono = prove_goal Cont.thy 
   252 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   253 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   254 \	is_chain(F)|] ==> \
   255 \	monofun(% x.lub(range(% j.MF2(F(j),x))))"
   256 (fn prems =>
   257 	[
   258 	(cut_facts_tac prems 1),
   259 	(rtac monofunI 1),
   260 	(strip_tac 1),
   261 	(rtac lub_mono 1),
   262 	(etac ch2ch_MF2L 1),
   263 	(atac 1),
   264 	(etac ch2ch_MF2L 1),
   265 	(atac 1),
   266 	(strip_tac 1),
   267 	((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
   268 	(atac 1)
   269 	]);
   270 
   271 
   272 val ex_lubMF2 = prove_goal Cont.thy 
   273 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   274 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   275 \	is_chain(F); is_chain(Y)|] ==> \
   276 \		lub(range(%j. lub(range(%i. MF2(F(j),Y(i)))))) =\
   277 \		lub(range(%i. lub(range(%j. MF2(F(j),Y(i))))))"
   278 (fn prems =>
   279 	[
   280 	(cut_facts_tac prems 1),
   281 	(rtac antisym_less 1),
   282 	(rtac is_lub_thelub 1),
   283 	(etac ch2ch_lubMF2R 1),
   284 	(atac 1),(atac 1),(atac 1),
   285 	(rtac ub_rangeI 1),
   286 	(strip_tac 1),
   287 	(rtac lub_mono 1),
   288 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   289 	(atac 1),
   290 	(etac ch2ch_lubMF2L 1),
   291 	(atac 1),(atac 1),(atac 1),
   292 	(strip_tac 1),
   293 	(rtac is_ub_thelub 1),
   294 	(etac ch2ch_MF2L 1),(atac 1),
   295 	(rtac is_lub_thelub 1),
   296 	(etac ch2ch_lubMF2L 1),
   297 	(atac 1),(atac 1),(atac 1),
   298 	(rtac ub_rangeI 1),
   299 	(strip_tac 1),
   300 	(rtac lub_mono 1),
   301 	(etac ch2ch_MF2L 1),(atac 1),
   302 	(etac ch2ch_lubMF2R 1),
   303 	(atac 1),(atac 1),(atac 1),
   304 	(strip_tac 1),
   305 	(rtac is_ub_thelub 1),
   306 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   307 	(atac 1)
   308 	]);
   309 
   310 (* ------------------------------------------------------------------------ *)
   311 (* The following results are about a curried function that is continuous    *)
   312 (* in both arguments                                                        *)
   313 (* ------------------------------------------------------------------------ *)
   314 
   315 val diag_lubCF2_1 = prove_goal Cont.thy 
   316 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   317 \ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
   318 \ lub(range(%i. CF2(FY(i))(TY(i))))"
   319 (fn prems =>
   320 	[
   321 	(cut_facts_tac prems 1),
   322 	(rtac antisym_less 1),
   323 	(rtac is_lub_thelub 1),
   324 	(rtac ch2ch_lubMF2L 1),
   325 	(rtac contX2mono 1),
   326 	(atac 1),
   327 	(rtac allI 1),
   328 	(rtac contX2mono 1),
   329 	(etac spec 1),
   330 	(atac 1),
   331 	(atac 1),
   332 	(rtac ub_rangeI 1),
   333 	(strip_tac 1 ),
   334 	(rtac is_lub_thelub 1),
   335 	((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
   336 	(atac 1),
   337 	(rtac ub_rangeI 1),
   338 	(strip_tac 1 ),
   339 	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   340 	(rtac trans_less 1),
   341 	(rtac is_ub_thelub 2),
   342 	(rtac (chain_mono RS mp) 1),
   343 	((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
   344 	(atac 1),
   345 	(atac 1),
   346 	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
   347 	(rtac allI 1),
   348 	((rtac contX2mono 1) THEN (etac spec 1)),
   349 	(atac 1),
   350 	(atac 1),
   351 	(hyp_subst_tac 1),
   352 	(rtac is_ub_thelub 1),
   353 	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
   354 	(rtac allI 1),
   355 	((rtac contX2mono 1) THEN (etac spec 1)),
   356 	(atac 1),
   357 	(atac 1),
   358 	(rtac trans_less 1),
   359 	(rtac is_ub_thelub 2),
   360 	(res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
   361 	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
   362 	(atac 1),
   363 	(atac 1),
   364 	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
   365 	(rtac allI 1),
   366 	((rtac contX2mono 1) THEN (etac spec 1)),
   367 	(atac 1),
   368 	(atac 1),
   369 	(rtac lub_mono 1),
   370 	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
   371 	(rtac allI 1),
   372 	((rtac contX2mono 1) THEN (etac spec 1)),
   373 	(atac 1),
   374 	(atac 1),
   375 	(rtac ch2ch_lubMF2L 1),
   376 	(rtac contX2mono 1),
   377 	(atac 1),
   378 	(rtac allI 1),
   379 	((rtac contX2mono 1) THEN (etac spec 1)),
   380 	(atac 1),
   381 	(atac 1),
   382 	(strip_tac 1 ),
   383 	(rtac is_ub_thelub 1),
   384 	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
   385 	(atac 1)
   386 	]);
   387 
   388 
   389 val diag_lubCF2_2 = prove_goal Cont.thy 
   390 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   391 \ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
   392 \ lub(range(%i. CF2(FY(i))(TY(i))))"
   393 (fn prems =>
   394 	[
   395 	(cut_facts_tac prems 1),
   396 	(rtac trans 1),
   397 	(rtac ex_lubMF2 1),
   398 	(rtac ((hd prems) RS contX2mono) 1), 
   399 	(rtac allI 1),
   400 	(rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
   401 	(atac 1),
   402 	(atac 1),
   403 	(rtac diag_lubCF2_1 1),
   404 	(atac 1),
   405 	(atac 1),
   406 	(atac 1),
   407 	(atac 1)
   408 	]);
   409 
   410 
   411 val contlub_CF2 = prove_goal Cont.thy 
   412 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   413 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
   414 (fn prems =>
   415 	[
   416 	(cut_facts_tac prems 1),
   417 	(rtac ((hd prems) RS contX2contlub RS contlubE RS 
   418 		spec RS mp RS ssubst) 1),
   419 	(atac 1),
   420 	(rtac (thelub_fun RS ssubst) 1),
   421 	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1), 
   422 	(atac 1),
   423 	(rtac trans 1),
   424 	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS 
   425 	contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   426 	(atac 1),
   427 	(rtac diag_lubCF2_2 1),
   428 	(atac 1),
   429 	(atac 1),
   430 	(atac 1),
   431 	(atac 1)
   432 	]);
   433 
   434 (* ------------------------------------------------------------------------ *)
   435 (* The following results are about application for functions in 'a=>'b      *)
   436 (* ------------------------------------------------------------------------ *)
   437 
   438 val monofun_fun_fun = prove_goal Cont.thy 
   439 	"f1 << f2 ==> f1(x) << f2(x)"
   440 (fn prems =>
   441 	[
   442 	(cut_facts_tac prems 1),
   443 	(etac (less_fun RS iffD1 RS spec) 1)
   444 	]);
   445 
   446 val monofun_fun_arg = prove_goal Cont.thy 
   447 	"[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
   448 (fn prems =>
   449 	[
   450 	(cut_facts_tac prems 1),
   451 	(etac (monofunE RS spec RS spec RS mp) 1),
   452 	(atac 1)
   453 	]);
   454 
   455 val monofun_fun = prove_goal Cont.thy 
   456 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
   457 (fn prems =>
   458 	[
   459 	(cut_facts_tac prems 1),
   460 	(rtac trans_less 1),
   461 	(etac monofun_fun_arg 1),
   462 	(atac 1),
   463 	(etac monofun_fun_fun 1)
   464 	]);
   465 
   466 
   467 (* ------------------------------------------------------------------------ *)
   468 (* The following results are about the propagation of monotonicity and      *)
   469 (* continuity                                                               *)
   470 (* ------------------------------------------------------------------------ *)
   471 
   472 val mono2mono_MF1L = prove_goal Cont.thy 
   473 	"[|monofun(c1)|] ==> monofun(%x. c1(x,y))"
   474 (fn prems =>
   475 	[
   476 	(cut_facts_tac prems 1),
   477 	(rtac monofunI 1),
   478 	(strip_tac 1),
   479 	(etac (monofun_fun_arg RS monofun_fun_fun) 1),
   480 	(atac 1)
   481 	]);
   482 
   483 val contX2contX_CF1L = prove_goal Cont.thy 
   484 	"[|contX(c1)|] ==> contX(%x. c1(x,y))"
   485 (fn prems =>
   486 	[
   487 	(cut_facts_tac prems 1),
   488 	(rtac monocontlub2contX 1),
   489 	(etac (contX2mono RS mono2mono_MF1L) 1),
   490 	(rtac contlubI 1),
   491 	(strip_tac 1),
   492 	(rtac ((hd prems) RS contX2contlub RS 
   493 		contlubE RS spec RS mp RS ssubst) 1),
   494 	(atac 1),
   495 	(rtac (thelub_fun RS ssubst) 1),
   496 	(rtac ch2ch_monofun 1),
   497 	(etac contX2mono 1),
   498 	(atac 1),
   499 	(rtac refl 1)
   500 	]);
   501 
   502 (*********  Note "(%x.%y.c1(x,y)) = c1" ***********)
   503 
   504 val mono2mono_MF1L_rev = prove_goal Cont.thy
   505 	"!y.monofun(%x.c1(x,y)) ==> monofun(c1)"
   506 (fn prems =>
   507 	[
   508 	(cut_facts_tac prems 1),
   509 	(rtac monofunI 1),
   510 	(strip_tac 1),
   511 	(rtac (less_fun RS iffD2) 1),
   512 	(strip_tac 1),
   513 	(rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
   514 	(atac 1)
   515 	]);
   516 
   517 val contX2contX_CF1L_rev = prove_goal Cont.thy
   518 	"!y.contX(%x.c1(x,y)) ==> contX(c1)"
   519 (fn prems =>
   520 	[
   521 	(cut_facts_tac prems 1),
   522 	(rtac monocontlub2contX 1),
   523 	(rtac (contX2mono RS allI RS mono2mono_MF1L_rev ) 1),
   524 	(etac spec 1),
   525 	(rtac contlubI 1),
   526 	(strip_tac 1),
   527 	(rtac ext 1),
   528 	(rtac (thelub_fun RS ssubst) 1),
   529 	(rtac (contX2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
   530 	(etac spec 1),
   531 	(atac 1),
   532 	(rtac 
   533 	((hd prems) RS spec RS contX2contlub RS contlubE RS spec RS mp) 1),
   534 	(atac 1)
   535 	]);
   536 
   537 
   538 (* ------------------------------------------------------------------------ *)
   539 (* What D.A.Schmidt calls continuity of abstraction                         *)
   540 (* never used here                                                          *)
   541 (* ------------------------------------------------------------------------ *)
   542 
   543 val contlub_abstraction = prove_goal Cont.thy
   544 "[|is_chain(Y::nat=>'a);!y.contX(%x.(c::'a=>'b=>'c)(x,y))|] ==>\
   545 \ (%y.lub(range(%i.c(Y(i),y)))) = (lub(range(%i.%y.c(Y(i),y))))"
   546  (fn prems =>
   547 	[
   548 	(cut_facts_tac prems 1),
   549 	(rtac trans 1),
   550 	(rtac (contX2contlub RS contlubE RS spec RS mp) 2),
   551 	(atac 3),
   552 	(etac contX2contX_CF1L_rev 2),
   553 	(rtac ext 1), 
   554 	(rtac (contX2contlub RS contlubE RS spec RS mp RS sym) 1),
   555 	(etac spec 1),
   556 	(atac 1)
   557 	]);
   558 
   559 
   560 val mono2mono_app = prove_goal Cont.thy 
   561 "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
   562 \	 monofun(%x.(ft(x))(tt(x)))"
   563  (fn prems =>
   564 	[
   565 	(cut_facts_tac prems 1),
   566 	(rtac monofunI 1),
   567 	(strip_tac 1),
   568 	(res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1),
   569 	(etac spec 1),
   570 	(etac spec 1),
   571 	(etac (monofunE RS spec RS spec RS mp) 1),
   572 	(atac 1),
   573 	(etac (monofunE RS spec RS spec RS mp) 1),
   574 	(atac 1)
   575 	]);
   576 
   577 val contX2contlub_app = prove_goal Cont.thy 
   578 "[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
   579 \	 contlub(%x.(ft(x))(tt(x)))"
   580  (fn prems =>
   581 	[
   582 	(cut_facts_tac prems 1),
   583 	(rtac contlubI 1),
   584 	(strip_tac 1),
   585 	(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
   586 	(rtac contX2contlub 1),
   587 	(resolve_tac prems 1),
   588 	(atac 1),
   589 	(rtac contlub_CF2 1),
   590 	(resolve_tac prems 1),
   591 	(resolve_tac prems 1),
   592 	(atac 1),
   593 	(rtac (contX2mono RS ch2ch_monofun) 1),
   594 	(resolve_tac prems 1),
   595 	(atac 1)
   596 	]);
   597 
   598 
   599 val contX2contX_app = prove_goal Cont.thy 
   600 "[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
   601 \	 contX(%x.(ft(x))(tt(x)))"
   602  (fn prems =>
   603 	[
   604 	(rtac monocontlub2contX 1),
   605 	(rtac mono2mono_app 1),
   606 	(rtac contX2mono 1),
   607 	(resolve_tac prems 1),
   608 	(strip_tac 1),
   609 	(rtac contX2mono 1),
   610 	(cut_facts_tac prems 1),
   611 	(etac spec 1),
   612 	(rtac contX2mono 1),
   613 	(resolve_tac prems 1),
   614 	(rtac contX2contlub_app 1),
   615 	(resolve_tac prems 1),
   616 	(resolve_tac prems 1),
   617 	(resolve_tac prems 1)
   618 	]);
   619 
   620 
   621 val contX2contX_app2 = (allI RSN (2,contX2contX_app));
   622 (*  [| contX(?ft); !!x. contX(?ft(x)); contX(?tt) |] ==>                 *)
   623 (*                                      contX(%x. ?ft(x,?tt(x)))         *)
   624 
   625 
   626 (* ------------------------------------------------------------------------ *)
   627 (* The identity function is continuous                                      *)
   628 (* ------------------------------------------------------------------------ *)
   629 
   630 val contX_id = prove_goal Cont.thy "contX(% x.x)"
   631  (fn prems =>
   632 	[
   633 	(rtac contXI 1),
   634 	(strip_tac 1),
   635 	(etac thelubE 1),
   636 	(rtac refl 1)
   637 	]);
   638 
   639 
   640 
   641 (* ------------------------------------------------------------------------ *)
   642 (* constant functions are continuous                                        *)
   643 (* ------------------------------------------------------------------------ *)
   644 
   645 val contX_const = prove_goalw Cont.thy [contX] "contX(%x.c)"
   646  (fn prems =>
   647 	[
   648 	(strip_tac 1),
   649 	(rtac is_lubI 1),
   650 	(rtac conjI 1),
   651 	(rtac ub_rangeI 1),
   652 	(strip_tac 1),
   653 	(rtac refl_less 1),
   654 	(strip_tac 1),
   655 	(dtac ub_rangeE 1),
   656 	(etac spec 1)
   657 	]);
   658 
   659 
   660 val contX2contX_app3 = prove_goal Cont.thy 
   661  "[|contX(f);contX(t) |] ==> contX(%x. f(t(x)))"
   662  (fn prems =>
   663 	[
   664 	(cut_facts_tac prems 1),
   665 	(rtac contX2contX_app2 1),
   666 	(rtac contX_const 1),
   667 	(atac 1),
   668 	(atac 1)
   669 	]);
   670