src/HOLCF/fix.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 300 3fb8c0256bec
permissions -rw-r--r--
tidying
     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 val iterate_0 = prove_goal Fix.thy "iterate(0,F,x) = x"
    16  (fn prems =>
    17 	[
    18 	(resolve_tac (nat_recs iterate_def) 1)
    19 	]);
    20 
    21 val iterate_Suc = prove_goal Fix.thy "iterate(Suc(n),F,x) = F[iterate(n,F,x)]"
    22  (fn prems =>
    23 	[
    24 	(resolve_tac (nat_recs iterate_def) 1)
    25 	]);
    26 
    27 val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
    28 
    29 val iterate_Suc2 = prove_goal Fix.thy "iterate(Suc(n),F,x) = iterate(n,F,F[x])"
    30  (fn prems =>
    31 	[
    32 	(nat_ind_tac "n" 1),
    33 	(simp_tac iterate_ss 1),
    34 	(asm_simp_tac iterate_ss 1)
    35 	]);
    36 
    37 (* ------------------------------------------------------------------------ *)
    38 (* the sequence of function itertaions is a chain                           *)
    39 (* This property is essential since monotonicity of iterate makes no sense  *)
    40 (* ------------------------------------------------------------------------ *)
    41 
    42 val is_chain_iterate2 = prove_goalw Fix.thy [is_chain] 
    43 	" x << F[x] ==> is_chain(%i.iterate(i,F,x))"
    44  (fn prems =>
    45 	[
    46 	(cut_facts_tac prems 1),
    47 	(strip_tac 1),
    48 	(simp_tac iterate_ss 1),
    49 	(nat_ind_tac "i" 1),
    50 	(asm_simp_tac iterate_ss 1),
    51 	(asm_simp_tac iterate_ss 1),
    52 	(etac monofun_cfun_arg 1)
    53 	]);
    54 
    55 
    56 val is_chain_iterate = prove_goal Fix.thy  
    57 	"is_chain(%i.iterate(i,F,UU))"
    58  (fn prems =>
    59 	[
    60 	(rtac is_chain_iterate2 1),
    61 	(rtac minimal 1)
    62 	]);
    63 
    64 
    65 (* ------------------------------------------------------------------------ *)
    66 (* Kleene's fixed point theorems for continuous functions in pointed        *)
    67 (* omega cpo's                                                              *)
    68 (* ------------------------------------------------------------------------ *)
    69 
    70 
    71 val Ifix_eq = prove_goalw Fix.thy  [Ifix_def] "Ifix(F)=F[Ifix(F)]"
    72  (fn prems =>
    73 	[
    74 	(rtac (contlub_cfun_arg RS ssubst) 1),
    75 	(rtac is_chain_iterate 1),
    76 	(rtac antisym_less 1),
    77 	(rtac lub_mono 1),
    78 	(rtac is_chain_iterate 1),
    79 	(rtac ch2ch_fappR 1),
    80 	(rtac is_chain_iterate 1),
    81 	(rtac allI 1),
    82 	(rtac (iterate_Suc RS subst) 1),
    83 	(rtac (is_chain_iterate RS is_chainE RS spec) 1),
    84 	(rtac is_lub_thelub 1),
    85 	(rtac ch2ch_fappR 1),
    86 	(rtac is_chain_iterate 1),
    87 	(rtac ub_rangeI 1),
    88 	(rtac allI 1),
    89 	(rtac (iterate_Suc RS subst) 1),
    90 	(rtac is_ub_thelub 1),
    91 	(rtac is_chain_iterate 1)
    92 	]);
    93 
    94 
    95 val Ifix_least = prove_goalw Fix.thy [Ifix_def] "F[x]=x ==> Ifix(F) << x"
    96  (fn prems =>
    97 	[
    98 	(cut_facts_tac prems 1),
    99 	(rtac is_lub_thelub 1),
   100 	(rtac is_chain_iterate 1),
   101 	(rtac ub_rangeI 1),
   102 	(strip_tac 1),
   103 	(nat_ind_tac "i" 1),
   104 	(asm_simp_tac iterate_ss 1),
   105 	(asm_simp_tac iterate_ss 1),
   106 	(res_inst_tac [("t","x")] subst 1),
   107 	(atac 1),
   108 	(etac monofun_cfun_arg 1)
   109 	]);
   110 
   111 
   112 (* ------------------------------------------------------------------------ *)
   113 (* monotonicity and continuity of iterate                                   *)
   114 (* ------------------------------------------------------------------------ *)
   115 
   116 val monofun_iterate = prove_goalw Fix.thy  [monofun] "monofun(iterate(i))"
   117  (fn prems =>
   118 	[
   119 	(strip_tac 1),
   120 	(nat_ind_tac "i" 1),
   121 	(asm_simp_tac iterate_ss 1),
   122 	(asm_simp_tac iterate_ss 1),
   123 	(rtac (less_fun RS iffD2) 1),
   124 	(rtac allI 1),
   125 	(rtac monofun_cfun 1),
   126 	(atac 1),
   127 	(rtac (less_fun RS iffD1 RS spec) 1),
   128 	(atac 1)
   129 	]);
   130 
   131 (* ------------------------------------------------------------------------ *)
   132 (* the following lemma uses contlub_cfun which itself is based on a         *)
   133 (* diagonalisation lemma for continuous functions with two arguments.       *)
   134 (* In this special case it is the application function fapp                 *)
   135 (* ------------------------------------------------------------------------ *)
   136 
   137 val contlub_iterate = prove_goalw Fix.thy  [contlub] "contlub(iterate(i))"
   138  (fn prems =>
   139 	[
   140 	(strip_tac 1),
   141 	(nat_ind_tac "i" 1),
   142 	(asm_simp_tac iterate_ss 1),
   143 	(rtac (lub_const RS thelubI RS sym) 1),
   144 	(asm_simp_tac iterate_ss 1),
   145 	(rtac ext 1),
   146 	(rtac (thelub_fun RS ssubst) 1),
   147 	(rtac is_chainI 1),
   148 	(rtac allI 1),
   149 	(rtac (less_fun RS iffD2) 1),
   150 	(rtac allI 1),
   151 	(rtac (is_chainE RS spec) 1),
   152 	(rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
   153 	(rtac allI 1),
   154 	(rtac monofun_fapp2 1),
   155 	(atac 1),
   156 	(rtac ch2ch_fun 1),
   157 	(rtac (monofun_iterate RS ch2ch_monofun) 1),
   158 	(atac 1),
   159 	(rtac (thelub_fun RS ssubst) 1),
   160 	(rtac (monofun_iterate RS ch2ch_monofun) 1),
   161 	(atac 1),
   162 	(rtac contlub_cfun  1),
   163 	(atac 1),
   164 	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
   165 	]);
   166 
   167 
   168 val contX_iterate = prove_goal Fix.thy "contX(iterate(i))"
   169  (fn prems =>
   170 	[
   171 	(rtac monocontlub2contX 1),
   172 	(rtac monofun_iterate 1),
   173 	(rtac contlub_iterate 1)
   174 	]);
   175 
   176 (* ------------------------------------------------------------------------ *)
   177 (* a lemma about continuity of iterate in its third argument                *)
   178 (* ------------------------------------------------------------------------ *)
   179 
   180 val monofun_iterate2 = prove_goal Fix.thy "monofun(iterate(n,F))"
   181  (fn prems =>
   182 	[
   183 	(rtac monofunI 1),
   184 	(strip_tac 1),
   185 	(nat_ind_tac "n" 1),
   186 	(asm_simp_tac iterate_ss 1),
   187 	(asm_simp_tac iterate_ss 1),
   188 	(etac monofun_cfun_arg 1)
   189 	]);
   190 
   191 val contlub_iterate2 = prove_goal Fix.thy "contlub(iterate(n,F))"
   192  (fn prems =>
   193 	[
   194 	(rtac contlubI 1),
   195 	(strip_tac 1),
   196 	(nat_ind_tac "n" 1),
   197 	(simp_tac iterate_ss 1),
   198 	(simp_tac iterate_ss 1),
   199 	(res_inst_tac [("t","iterate(n1, F, lub(range(%u. Y(u))))"),
   200 	("s","lub(range(%i. iterate(n1, F, Y(i))))")] ssubst 1),
   201 	(atac 1),
   202 	(rtac contlub_cfun_arg 1),
   203 	(etac (monofun_iterate2 RS ch2ch_monofun) 1)
   204 	]);
   205 
   206 val contX_iterate2 = prove_goal Fix.thy "contX(iterate(n,F))"
   207  (fn prems =>
   208 	[
   209 	(rtac monocontlub2contX 1),
   210 	(rtac monofun_iterate2 1),
   211 	(rtac contlub_iterate2 1)
   212 	]);
   213 
   214 (* ------------------------------------------------------------------------ *)
   215 (* monotonicity and continuity of Ifix                                      *)
   216 (* ------------------------------------------------------------------------ *)
   217 
   218 val monofun_Ifix = prove_goalw Fix.thy  [monofun,Ifix_def] "monofun(Ifix)"
   219  (fn prems =>
   220 	[
   221 	(strip_tac 1),
   222 	(rtac lub_mono 1),
   223 	(rtac is_chain_iterate 1),
   224 	(rtac is_chain_iterate 1),
   225 	(rtac allI 1),
   226 	(rtac (less_fun RS iffD1 RS spec) 1),
   227 	(etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1)
   228 	]);
   229 
   230 
   231 (* ------------------------------------------------------------------------ *)
   232 (* since iterate is not monotone in its first argument, special lemmas must *)
   233 (* be derived for lubs in this argument                                     *)
   234 (* ------------------------------------------------------------------------ *)
   235 
   236 val is_chain_iterate_lub = prove_goal Fix.thy   
   237 "is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate(ia,Y(i),UU))))"
   238  (fn prems =>
   239 	[
   240 	(cut_facts_tac prems 1),
   241 	(rtac is_chainI 1),
   242 	(strip_tac 1),
   243 	(rtac lub_mono 1),
   244 	(rtac is_chain_iterate 1),
   245 	(rtac is_chain_iterate 1),
   246 	(strip_tac 1),
   247 	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS is_chainE 
   248          RS spec) 1)
   249 	]);
   250 
   251 (* ------------------------------------------------------------------------ *)
   252 (* this exchange lemma is analog to the one for monotone functions          *)
   253 (* observe that monotonicity is not really needed. The propagation of       *)
   254 (* chains is the essential argument which is usually derived from monot.    *)
   255 (* ------------------------------------------------------------------------ *)
   256 
   257 val contlub_Ifix_lemma1 = prove_goal Fix.thy 
   258 "is_chain(Y) ==> iterate(n,lub(range(Y)),y) = lub(range(%i. iterate(n,Y(i),y)))"
   259  (fn prems =>
   260 	[
   261 	(cut_facts_tac prems 1),
   262 	(rtac (thelub_fun RS subst) 1),
   263 	(rtac (monofun_iterate RS ch2ch_monofun) 1),
   264 	(atac 1),
   265 	(rtac fun_cong 1),
   266 	(rtac (contlub_iterate RS contlubE RS spec RS mp RS ssubst) 1),
   267 	(atac 1),
   268 	(rtac refl 1)
   269 	]);
   270 
   271 
   272 val ex_lub_iterate = prove_goal Fix.thy  "is_chain(Y) ==>\
   273 \         lub(range(%i. lub(range(%ia. iterate(i,Y(ia),UU))))) =\
   274 \         lub(range(%i. lub(range(%ia. iterate(ia,Y(i),UU)))))"
   275  (fn prems =>
   276 	[
   277 	(cut_facts_tac prems 1),
   278 	(rtac antisym_less 1),
   279 	(rtac is_lub_thelub 1),
   280 	(rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
   281 	(atac 1),
   282 	(rtac is_chain_iterate 1),
   283 	(rtac ub_rangeI 1),
   284 	(strip_tac 1),
   285 	(rtac lub_mono 1),
   286 	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1),
   287 	(etac is_chain_iterate_lub 1),
   288 	(strip_tac 1),
   289 	(rtac is_ub_thelub 1),
   290 	(rtac is_chain_iterate 1),
   291 	(rtac is_lub_thelub 1),
   292 	(etac is_chain_iterate_lub 1),
   293 	(rtac ub_rangeI 1),
   294 	(strip_tac 1),
   295 	(rtac lub_mono 1),
   296 	(rtac is_chain_iterate 1),
   297 	(rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
   298 	(atac 1),
   299 	(rtac is_chain_iterate 1),
   300 	(strip_tac 1),
   301 	(rtac is_ub_thelub 1),
   302 	(etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
   303 	]);
   304 
   305 
   306 val contlub_Ifix = prove_goalw Fix.thy  [contlub,Ifix_def] "contlub(Ifix)"
   307  (fn prems =>
   308 	[
   309 	(strip_tac 1),
   310 	(rtac (contlub_Ifix_lemma1 RS ext RS ssubst) 1),
   311 	(atac 1),
   312 	(etac ex_lub_iterate 1)
   313 	]);
   314 
   315 
   316 val contX_Ifix = prove_goal Fix.thy "contX(Ifix)"
   317  (fn prems =>
   318 	[
   319 	(rtac monocontlub2contX 1),
   320 	(rtac monofun_Ifix 1),
   321 	(rtac contlub_Ifix 1)
   322 	]);
   323 
   324 (* ------------------------------------------------------------------------ *)
   325 (* propagate properties of Ifix to its continuous counterpart               *)
   326 (* ------------------------------------------------------------------------ *)
   327 
   328 val fix_eq = prove_goalw Fix.thy  [fix_def] "fix[F]=F[fix[F]]"
   329  (fn prems =>
   330 	[
   331 	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1),
   332 	(rtac Ifix_eq 1)
   333 	]);
   334 
   335 val fix_least = prove_goalw Fix.thy [fix_def] "F[x]=x ==> fix[F] << x"
   336  (fn prems =>
   337 	[
   338 	(cut_facts_tac prems 1),
   339 	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1),
   340 	(etac Ifix_least 1)
   341 	]);
   342 
   343 
   344 val fix_eq2 = prove_goal Fix.thy "f == fix[F] ==> f = F[f]"
   345  (fn prems =>
   346 	[
   347 	(rewrite_goals_tac prems),
   348 	(rtac fix_eq 1)
   349 	]);
   350 
   351 val fix_eq3 = prove_goal Fix.thy "f == fix[F] ==> f[x] = F[f][x]"
   352  (fn prems =>
   353 	[
   354 	(rtac trans 1),
   355 	(rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1),
   356 	(rtac refl 1)
   357 	]);
   358 
   359 fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
   360 
   361 val fix_eq4 = prove_goal Fix.thy "f = fix[F] ==> f = F[f]"
   362  (fn prems =>
   363 	[
   364 	(cut_facts_tac prems 1),
   365 	(hyp_subst_tac 1),
   366 	(rtac fix_eq 1)
   367 	]);
   368 
   369 val fix_eq5 = prove_goal Fix.thy "f = fix[F] ==> f[x] = F[f][x]"
   370  (fn prems =>
   371 	[
   372 	(rtac trans 1),
   373 	(rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1),
   374 	(rtac refl 1)
   375 	]);
   376 
   377 fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
   378 
   379 fun fix_prover thy fixdef thm = prove_goal thy thm
   380  (fn prems =>
   381         [
   382         (rtac trans 1),
   383         (rtac (fixdef RS fix_eq4) 1),
   384         (rtac trans 1),
   385         (rtac beta_cfun 1),
   386         (contX_tacR 1),
   387         (rtac refl 1)
   388         ]);
   389 
   390 (* ------------------------------------------------------------------------ 
   391 
   392 given the definition
   393 
   394 smap_def
   395   "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
   396 
   397 use fix_prover for 
   398 
   399 val smap_def2 = fix_prover Stream2.thy smap_def 
   400         "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
   401 
   402    ------------------------------------------------------------------------ *)
   403 
   404 (* ------------------------------------------------------------------------ *)
   405 (* better access to definitions                                             *)
   406 (* ------------------------------------------------------------------------ *)
   407 
   408 
   409 val Ifix_def2 = prove_goal Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))"
   410  (fn prems =>
   411 	[
   412 	(rtac ext 1),
   413 	(rewrite_goals_tac [Ifix_def]),
   414 	(rtac refl 1)
   415 	]);
   416 
   417 (* ------------------------------------------------------------------------ *)
   418 (* direct connection between fix and iteration without Ifix                 *)
   419 (* ------------------------------------------------------------------------ *)
   420 
   421 val fix_def2 = prove_goalw Fix.thy [fix_def]
   422  "fix[F] = lub(range(%i. iterate(i,F,UU)))"
   423  (fn prems =>
   424 	[
   425 	(fold_goals_tac [Ifix_def]),
   426 	(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1)
   427 	]);
   428 
   429 
   430 (* ------------------------------------------------------------------------ *)
   431 (* Lemmas about admissibility and fixed point induction                     *)
   432 (* ------------------------------------------------------------------------ *)
   433 
   434 (* ------------------------------------------------------------------------ *)
   435 (* access to definitions                                                    *)
   436 (* ------------------------------------------------------------------------ *)
   437 
   438 val adm_def2 = prove_goalw Fix.thy [adm_def]
   439 	"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
   440  (fn prems =>
   441 	[
   442 	(rtac refl 1)
   443 	]);
   444 
   445 val admw_def2 = prove_goalw Fix.thy [admw_def]
   446 	"admw(P) = (!F.((!n.P(iterate(n,F,UU)))-->\
   447 \			 P(lub(range(%i.iterate(i,F,UU))))))"
   448  (fn prems =>
   449 	[
   450 	(rtac refl 1)
   451 	]);
   452 
   453 (* ------------------------------------------------------------------------ *)
   454 (* an admissible formula is also weak admissible                            *)
   455 (* ------------------------------------------------------------------------ *)
   456 
   457 val adm_impl_admw = prove_goalw  Fix.thy [admw_def] "adm(P)==>admw(P)"
   458  (fn prems =>
   459 	[
   460 	(cut_facts_tac prems 1),
   461 	(strip_tac 1),
   462 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   463 	(atac 1),
   464 	(rtac is_chain_iterate 1),
   465 	(atac 1)
   466 	]);
   467 
   468 (* ------------------------------------------------------------------------ *)
   469 (* fixed point induction                                                    *)
   470 (* ------------------------------------------------------------------------ *)
   471 
   472 val fix_ind = prove_goal  Fix.thy  
   473 "[| adm(P);P(UU);!!x. P(x) ==> P(F[x])|] ==> P(fix[F])"
   474  (fn prems =>
   475 	[
   476 	(cut_facts_tac prems 1),
   477 	(rtac (fix_def2 RS ssubst) 1),
   478 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   479 	(atac 1),
   480 	(rtac is_chain_iterate 1),
   481 	(rtac allI 1),
   482 	(nat_ind_tac "i" 1),
   483 	(rtac (iterate_0 RS ssubst) 1),
   484 	(atac 1),
   485 	(rtac (iterate_Suc RS ssubst) 1),
   486 	(resolve_tac prems 1),
   487 	(atac 1)
   488 	]);
   489 
   490 (* ------------------------------------------------------------------------ *)
   491 (* computational induction for weak admissible formulae                     *)
   492 (* ------------------------------------------------------------------------ *)
   493 
   494 val wfix_ind = prove_goal  Fix.thy  
   495 "[| admw(P); !n. P(iterate(n,F,UU))|] ==> P(fix[F])"
   496  (fn prems =>
   497 	[
   498 	(cut_facts_tac prems 1),
   499 	(rtac (fix_def2 RS ssubst) 1),
   500 	(rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
   501 	(atac 1),
   502 	(rtac allI 1),
   503 	(etac spec 1)
   504 	]);
   505 
   506 (* ------------------------------------------------------------------------ *)
   507 (* for chain-finite (easy) types every formula is admissible                *)
   508 (* ------------------------------------------------------------------------ *)
   509 
   510 val adm_max_in_chain = prove_goalw  Fix.thy  [adm_def]
   511 "!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y)) ==> adm(P::'a=>bool)"
   512  (fn prems =>
   513 	[
   514 	(cut_facts_tac prems 1),
   515 	(strip_tac 1),
   516 	(rtac exE 1),
   517 	(rtac mp 1),
   518 	(etac spec 1),
   519 	(atac 1),
   520 	(rtac (lub_finch1 RS thelubI RS ssubst) 1),
   521 	(atac 1),
   522 	(atac 1),
   523 	(etac spec 1)
   524 	]);
   525 
   526 
   527 val adm_chain_finite = prove_goalw  Fix.thy  [chain_finite_def]
   528 	"chain_finite(x::'a) ==> adm(P::'a=>bool)"
   529  (fn prems =>
   530 	[
   531 	(cut_facts_tac prems 1),
   532 	(etac adm_max_in_chain 1)
   533 	]);
   534 
   535 (* ------------------------------------------------------------------------ *)
   536 (* flat types are chain_finite                                              *)
   537 (* ------------------------------------------------------------------------ *)
   538 
   539 val flat_imp_chain_finite = prove_goalw  Fix.thy  [flat_def,chain_finite_def]
   540 	"flat(x::'a)==>chain_finite(x::'a)"
   541  (fn prems =>
   542 	[
   543 	(rewrite_goals_tac [max_in_chain_def]),
   544 	(cut_facts_tac prems 1),
   545 	(strip_tac 1),
   546 	(res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1),
   547 	(res_inst_tac [("x","0")] exI 1),
   548 	(strip_tac 1),
   549 	(rtac trans 1),
   550 	(etac spec 1),
   551 	(rtac sym 1),
   552 	(etac spec 1),
   553 	(rtac (chain_mono2 RS exE) 1),
   554 	(fast_tac HOL_cs 1),
   555 	(atac 1),
   556 	(res_inst_tac [("x","Suc(x)")] exI 1),
   557 	(strip_tac 1),
   558 	(rtac disjE 1),
   559 	(atac 3),
   560 	(rtac mp 1),
   561 	(dtac spec 1),
   562 	(etac spec 1),
   563 	(etac (le_imp_less_or_eq RS disjE) 1),
   564 	(etac (chain_mono RS mp) 1),
   565 	(atac 1),
   566 	(hyp_subst_tac 1),
   567 	(rtac refl_less 1),
   568 	(res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
   569 	(atac 2),
   570 	(rtac mp 1),
   571 	(etac spec 1),
   572 	(asm_simp_tac nat_ss 1)
   573 	]);
   574 
   575 
   576 val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
   577 (* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
   578 
   579 val flat_void = prove_goalw Fix.thy [flat_def] "flat(UU::void)"
   580  (fn prems =>
   581 	[
   582 	(strip_tac 1),
   583 	(rtac disjI1 1),
   584 	(rtac unique_void2 1)
   585 	]);
   586 
   587 (* ------------------------------------------------------------------------ *)
   588 (* continuous isomorphisms are strict                                       *)
   589 (* a prove for embedding projection pairs is similar                        *)
   590 (* ------------------------------------------------------------------------ *)
   591 
   592 val iso_strict = prove_goal  Fix.thy  
   593 "!!f g.[|!y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
   594 \ ==> f[UU]=UU & g[UU]=UU"
   595  (fn prems =>
   596 	[
   597 	(rtac conjI 1),
   598 	(rtac UU_I 1),
   599 	(res_inst_tac [("s","f[g[UU::'b]]"),("t","UU::'b")] subst 1),
   600 	(etac spec 1),
   601 	(rtac (minimal RS monofun_cfun_arg) 1),
   602 	(rtac UU_I 1),
   603 	(res_inst_tac [("s","g[f[UU::'a]]"),("t","UU::'a")] subst 1),
   604 	(etac spec 1),
   605 	(rtac (minimal RS monofun_cfun_arg) 1)
   606 	]);
   607 
   608 
   609 val isorep_defined = prove_goal Fix.thy 
   610 	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> rep[z]~=UU"
   611  (fn prems =>
   612 	[
   613 	(cut_facts_tac prems 1),
   614 	(etac swap 1),
   615 	(dtac notnotD 1),
   616 	(dres_inst_tac [("f","abs")] cfun_arg_cong 1),
   617 	(etac box_equals 1),
   618 	(fast_tac HOL_cs 1),
   619 	(etac (iso_strict RS conjunct1) 1),
   620 	(atac 1)
   621 	]);
   622 
   623 val isoabs_defined = prove_goal Fix.thy 
   624 	"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> abs[z]~=UU"
   625  (fn prems =>
   626 	[
   627 	(cut_facts_tac prems 1),
   628 	(etac swap 1),
   629 	(dtac notnotD 1),
   630 	(dres_inst_tac [("f","rep")] cfun_arg_cong 1),
   631 	(etac box_equals 1),
   632 	(fast_tac HOL_cs 1),
   633 	(etac (iso_strict RS conjunct2) 1),
   634 	(atac 1)
   635 	]);
   636 
   637 (* ------------------------------------------------------------------------ *)
   638 (* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
   639 (* ------------------------------------------------------------------------ *)
   640 
   641 val chfin2chfin = prove_goalw  Fix.thy  [chain_finite_def]
   642 "!!f g.[|chain_finite(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
   643 \ ==> chain_finite(y::'b)"
   644  (fn prems =>
   645 	[
   646 	(rewrite_goals_tac [max_in_chain_def]),
   647 	(strip_tac 1),
   648 	(rtac exE 1),
   649 	(res_inst_tac [("P","is_chain(%i.g[Y(i)])")] mp 1),
   650 	(etac spec 1),
   651 	(etac ch2ch_fappR 1),
   652 	(rtac exI 1),
   653 	(strip_tac 1),
   654 	(res_inst_tac [("s","f[g[Y(x)]]"),("t","Y(x)")] subst 1),
   655 	(etac spec 1),
   656 	(res_inst_tac [("s","f[g[Y(j)]]"),("t","Y(j)")] subst 1),
   657 	(etac spec 1),
   658 	(rtac cfun_arg_cong 1),
   659 	(rtac mp 1),
   660 	(etac spec 1),
   661 	(atac 1)
   662 	]);
   663 
   664 val flat2flat = prove_goalw  Fix.thy  [flat_def]
   665 "!!f g.[|flat(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
   666 \ ==> flat(y::'b)"
   667  (fn prems =>
   668 	[
   669 	(strip_tac 1),
   670 	(rtac disjE 1),
   671 	(res_inst_tac [("P","g[x]<<g[y]")] mp 1),
   672 	(etac monofun_cfun_arg 2),
   673 	(dtac spec 1),
   674 	(etac spec 1),
   675 	(rtac disjI1 1),
   676 	(rtac trans 1),
   677 	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
   678 	(etac spec 1),
   679 	(etac cfun_arg_cong 1),
   680 	(rtac (iso_strict RS conjunct1) 1),
   681 	(atac 1),
   682 	(atac 1),
   683 	(rtac disjI2 1),
   684 	(res_inst_tac [("s","f[g[x]]"),("t","x")] subst 1),
   685 	(etac spec 1),
   686 	(res_inst_tac [("s","f[g[y]]"),("t","y")] subst 1),
   687 	(etac spec 1),
   688 	(etac cfun_arg_cong 1)
   689 	]);
   690 
   691 (* ------------------------------------------------------------------------ *)
   692 (* admissibility of special formulae and propagation                        *)
   693 (* ------------------------------------------------------------------------ *)
   694 
   695 val adm_less = prove_goalw  Fix.thy [adm_def]
   696 	"[|contX(u);contX(v)|]==> adm(%x.u(x)<<v(x))"
   697  (fn prems =>
   698 	[
   699 	(cut_facts_tac prems 1),
   700 	(strip_tac 1),
   701 	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   702 	(atac 1),
   703 	(etac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   704 	(atac 1),
   705 	(rtac lub_mono 1),
   706 	(cut_facts_tac prems 1),
   707 	(etac (contX2mono RS ch2ch_monofun) 1),
   708 	(atac 1),
   709 	(cut_facts_tac prems 1),
   710 	(etac (contX2mono RS ch2ch_monofun) 1),
   711 	(atac 1),
   712 	(atac 1)
   713 	]);
   714 
   715 val adm_conj = prove_goal  Fix.thy  
   716 	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
   717  (fn prems =>
   718 	[
   719 	(cut_facts_tac prems 1),
   720 	(rtac (adm_def2 RS iffD2) 1),
   721 	(strip_tac 1),
   722 	(rtac conjI 1),
   723 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   724 	(atac 1),
   725 	(atac 1),
   726 	(fast_tac HOL_cs 1),
   727 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   728 	(atac 1),
   729 	(atac 1),
   730 	(fast_tac HOL_cs 1)
   731 	]);
   732 
   733 val adm_cong = prove_goal  Fix.thy  
   734 	"(!x. P(x) = Q(x)) ==> adm(P)=adm(Q)"
   735  (fn prems =>
   736 	[
   737 	(cut_facts_tac prems 1),
   738 	(res_inst_tac [("s","P"),("t","Q")] subst 1),
   739 	(rtac refl 2),
   740 	(rtac ext 1),
   741 	(etac spec 1)
   742 	]);
   743 
   744 val adm_not_free = prove_goalw  Fix.thy [adm_def] "adm(%x.t)"
   745  (fn prems =>
   746 	[
   747 	(fast_tac HOL_cs 1)
   748 	]);
   749 
   750 val adm_not_less = prove_goalw  Fix.thy [adm_def]
   751 	"contX(t) ==> adm(%x.~ t(x) << u)"
   752  (fn prems =>
   753 	[
   754 	(cut_facts_tac prems 1),
   755 	(strip_tac 1),
   756 	(rtac contrapos 1),
   757 	(etac spec 1),
   758 	(rtac trans_less 1),
   759 	(atac 2),
   760 	(etac (contX2mono RS monofun_fun_arg) 1),
   761 	(rtac is_ub_thelub 1),
   762 	(atac 1)
   763 	]);
   764 
   765 val adm_all = prove_goal  Fix.thy  
   766 	" !y.adm(P(y)) ==> adm(%x.!y.P(y,x))"
   767  (fn prems =>
   768 	[
   769 	(cut_facts_tac prems 1),
   770 	(rtac (adm_def2 RS iffD2) 1),
   771 	(strip_tac 1),
   772 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   773 	(etac spec 1),
   774 	(atac 1),
   775 	(rtac allI 1),
   776 	(dtac spec 1),
   777 	(etac spec 1)
   778 	]);
   779 
   780 val adm_subst = prove_goal  Fix.thy  
   781 	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
   782  (fn prems =>
   783 	[
   784 	(cut_facts_tac prems 1),
   785 	(rtac (adm_def2 RS iffD2) 1),
   786 	(strip_tac 1),
   787 	(rtac (contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   788 	(atac 1),
   789 	(atac 1),
   790 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   791 	(atac 1),
   792 	(rtac (contX2mono RS ch2ch_monofun) 1),
   793 	(atac 1),
   794 	(atac 1),
   795 	(atac 1)
   796 	]);
   797 
   798 val adm_UU_not_less = prove_goal  Fix.thy "adm(%x.~ UU << t(x))"
   799  (fn prems =>
   800 	[
   801 	(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
   802 	(asm_simp_tac Cfun_ss 1),
   803 	(rtac adm_not_free 1)
   804 	]);
   805 
   806 val adm_not_UU = prove_goalw  Fix.thy [adm_def] 
   807 	"contX(t)==> adm(%x.~ t(x) = UU)"
   808  (fn prems =>
   809 	[
   810 	(cut_facts_tac prems 1),
   811 	(strip_tac 1),
   812 	(rtac contrapos 1),
   813 	(etac spec 1),
   814 	(rtac (chain_UU_I RS spec) 1),
   815 	(rtac (contX2mono RS ch2ch_monofun) 1),
   816 	(atac 1),
   817 	(atac 1),
   818 	(rtac (contX2contlub RS contlubE RS spec RS mp RS subst) 1),
   819 	(atac 1),
   820 	(atac 1),
   821 	(atac 1)
   822 	]);
   823 
   824 val adm_eq = prove_goal  Fix.thy 
   825 	"[|contX(u);contX(v)|]==> adm(%x.u(x)= v(x))"
   826  (fn prems =>
   827 	[
   828 	(rtac (adm_cong RS iffD1) 1),
   829 	(rtac allI 1),
   830 	(rtac iffI 1),
   831 	(rtac antisym_less 1),
   832 	(rtac antisym_less_inverse 3),
   833 	(atac 3),
   834 	(etac conjunct1 1),
   835 	(etac conjunct2 1),
   836 	(rtac adm_conj 1),
   837 	(rtac adm_less 1),
   838 	(resolve_tac prems 1),
   839 	(resolve_tac prems 1),
   840 	(rtac adm_less 1),
   841 	(resolve_tac prems 1),
   842 	(resolve_tac prems 1)
   843 	]);
   844 
   845 
   846 (* ------------------------------------------------------------------------ *)
   847 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
   848 (* ------------------------------------------------------------------------ *)
   849 
   850 val adm_disj_lemma1 = prove_goal  Pcpo.thy 
   851 "[| is_chain(Y); !n.P(Y(n))|Q(Y(n))|]\
   852 \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
   853  (fn prems =>
   854 	[
   855 	(cut_facts_tac prems 1),
   856 	(fast_tac HOL_cs 1)
   857 	]);
   858 
   859 val adm_disj_lemma2 = prove_goal  Fix.thy  
   860 "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
   861 \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
   862  (fn prems =>
   863 	[
   864 	(cut_facts_tac prems 1),
   865 	(etac exE 1),
   866 	(etac conjE 1),
   867 	(etac conjE 1),
   868 	(res_inst_tac [("s","lub(range(X))"),("t","lub(range(Y))")] ssubst 1),
   869 	(atac 1),
   870 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   871 	(atac 1),
   872 	(atac 1),
   873 	(atac 1)
   874 	]);
   875 
   876 val adm_disj_lemma3 = prove_goal  Fix.thy
   877 "[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
   878 \         is_chain(%m. if(m < Suc(i),Y(Suc(i)),Y(m)))"
   879  (fn prems =>
   880 	[
   881 	(cut_facts_tac prems 1),
   882 	(rtac is_chainI 1),
   883 	(rtac allI 1),
   884 	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   885 	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
   886 	(rtac iffI 1),
   887 	(etac FalseE 2),
   888 	(rtac notE 1),
   889 	(rtac (not_less_eq RS iffD2) 1),
   890 	(atac 1),
   891 	(atac 1),
   892 	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
   893 	(asm_simp_tac nat_ss  1),
   894 	(rtac iffI 1),
   895 	(etac FalseE 2),
   896 	(rtac notE 1),
   897 	(etac less_not_sym 1),	
   898 	(atac 1),
   899 	(asm_simp_tac Cfun_ss  1),
   900 	(etac (is_chainE RS spec) 1),
   901 	(hyp_subst_tac 1),
   902 	(asm_simp_tac nat_ss 1),
   903 	(rtac refl_less 1),
   904 	(asm_simp_tac nat_ss 1),
   905 	(rtac refl_less 1)
   906 	]);
   907 
   908 val adm_disj_lemma4 = prove_goal  Fix.thy
   909 "[| ! j. i < j --> Q(Y(j)) |] ==>\
   910 \	 ! n. Q(if(n < Suc(i),Y(Suc(i)),Y(n)))"
   911  (fn prems =>
   912 	[
   913 	(cut_facts_tac prems 1),
   914 	(rtac allI 1),
   915 	(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
   916 	(res_inst_tac[("s","Y(Suc(i))"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")]
   917 		ssubst 1),
   918 	(asm_simp_tac nat_ss 1),
   919 	(etac allE 1),
   920 	(rtac mp 1),
   921 	(atac 1),
   922 	(asm_simp_tac nat_ss 1),
   923 	(res_inst_tac[("s","Y(n)"),("t","if(n<Suc(i),Y(Suc(i)),Y(n))")] 
   924 		ssubst 1),
   925 	(asm_simp_tac nat_ss 1),
   926 	(hyp_subst_tac 1),
   927 	(dtac spec 1),
   928 	(rtac mp 1),
   929 	(atac 1),
   930 	(asm_simp_tac nat_ss 1),
   931 	(res_inst_tac [("s","Y(n)"),("t","if(n < Suc(i),Y(Suc(i)),Y(n))")] 
   932 		ssubst 1),
   933 	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   934 	(rtac iffI 1),
   935 	(etac FalseE 2),
   936 	(rtac notE 1),
   937 	(etac less_not_sym 1),	
   938 	(atac 1),
   939 	(asm_simp_tac nat_ss 1),
   940 	(dtac spec 1),
   941 	(rtac mp 1),
   942 	(atac 1),
   943 	(etac Suc_lessD 1)
   944 	]);
   945 
   946 val adm_disj_lemma5 = prove_goal  Fix.thy
   947 "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
   948 \         lub(range(Y)) = lub(range(%m. if(m < Suc(i),Y(Suc(i)),Y(m))))"
   949  (fn prems =>
   950 	[
   951 	(cut_facts_tac prems 1),
   952 	(rtac lub_equal2 1),
   953 	(atac 2),
   954 	(rtac adm_disj_lemma3 2),
   955 	(atac 2),
   956 	(atac 2),
   957 	(res_inst_tac [("x","i")] exI 1),
   958 	(strip_tac 1),
   959 	(res_inst_tac [("s","False"),("t","ia < Suc(i)")] ssubst 1),
   960 	(rtac iffI 1),
   961 	(etac FalseE 2),
   962 	(rtac notE 1),
   963 	(rtac (not_less_eq RS iffD2) 1),
   964 	(atac 1),
   965 	(atac 1),
   966 	(rtac (if_False RS ssubst) 1),
   967 	(rtac refl 1)
   968 	]);
   969 
   970 val adm_disj_lemma6 = prove_goal  Fix.thy
   971 "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
   972 \         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
   973  (fn prems =>
   974 	[
   975 	(cut_facts_tac prems 1),
   976 	(etac exE 1),
   977 	(res_inst_tac [("x","%m.if(m< Suc(i),Y(Suc(i)),Y(m))")] exI 1),
   978 	(rtac conjI 1),
   979 	(rtac adm_disj_lemma3 1),
   980 	(atac 1),
   981 	(atac 1),
   982 	(rtac conjI 1),
   983 	(rtac adm_disj_lemma4 1),
   984 	(atac 1),
   985 	(rtac adm_disj_lemma5 1),
   986 	(atac 1),
   987 	(atac 1)
   988 	]);
   989 
   990 
   991 val adm_disj_lemma7 = prove_goal  Fix.thy 
   992 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
   993 \         is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
   994  (fn prems =>
   995 	[
   996 	(cut_facts_tac prems 1),
   997 	(rtac is_chainI 1),
   998 	(rtac allI 1),
   999 	(rtac chain_mono3 1),
  1000 	(atac 1),
  1001 	(rtac theleast2 1),
  1002 	(rtac conjI 1),
  1003 	(rtac Suc_lessD 1),
  1004 	(etac allE 1),
  1005 	(etac exE 1),
  1006 	(rtac (theleast1 RS conjunct1) 1),
  1007 	(atac 1),
  1008 	(etac allE 1),
  1009 	(etac exE 1),
  1010 	(rtac (theleast1 RS conjunct2) 1),
  1011 	(atac 1)
  1012 	]);
  1013 
  1014 val adm_disj_lemma8 = prove_goal  Fix.thy 
  1015 "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
  1016  (fn prems =>
  1017 	[
  1018 	(cut_facts_tac prems 1),
  1019 	(strip_tac 1),
  1020 	(etac allE 1),
  1021 	(etac exE 1),
  1022 	(etac (theleast1 RS conjunct2) 1)
  1023 	]);
  1024 
  1025 val adm_disj_lemma9 = prove_goal  Fix.thy
  1026 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
  1027 \         lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
  1028  (fn prems =>
  1029 	[
  1030 	(cut_facts_tac prems 1),
  1031 	(rtac antisym_less 1),
  1032 	(rtac lub_mono 1),
  1033 	(atac 1),
  1034 	(rtac adm_disj_lemma7 1),
  1035 	(atac 1),
  1036 	(atac 1),
  1037 	(strip_tac 1),
  1038 	(rtac (chain_mono RS mp) 1),
  1039 	(atac 1),
  1040 	(etac allE 1),
  1041 	(etac exE 1),
  1042 	(rtac (theleast1 RS conjunct1) 1),
  1043 	(atac 1),
  1044 	(rtac lub_mono3 1),
  1045 	(rtac adm_disj_lemma7 1),
  1046 	(atac 1),
  1047 	(atac 1),
  1048 	(atac 1),
  1049 	(strip_tac 1),
  1050 	(rtac exI 1),
  1051 	(rtac (chain_mono RS mp) 1),
  1052 	(atac 1),
  1053 	(rtac lessI 1)
  1054 	]);
  1055 
  1056 val adm_disj_lemma10 = prove_goal  Fix.thy
  1057 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
  1058 \         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
  1059  (fn prems =>
  1060 	[
  1061 	(cut_facts_tac prems 1),
  1062 	(res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1),
  1063 	(rtac conjI 1),
  1064 	(rtac adm_disj_lemma7 1),
  1065 	(atac 1),
  1066 	(atac 1),
  1067 	(rtac conjI 1),
  1068 	(rtac adm_disj_lemma8 1),
  1069 	(atac 1),
  1070 	(rtac adm_disj_lemma9 1),
  1071 	(atac 1),
  1072 	(atac 1)
  1073 	]);
  1074 
  1075 val adm_disj = prove_goal  Fix.thy  
  1076 	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
  1077  (fn prems =>
  1078 	[
  1079 	(cut_facts_tac prems 1),
  1080 	(rtac (adm_def2 RS iffD2) 1),
  1081 	(strip_tac 1),
  1082 	(rtac (adm_disj_lemma1 RS disjE) 1),
  1083 	(atac 1),
  1084 	(atac 1),
  1085 	(rtac disjI2 1),
  1086 	(rtac adm_disj_lemma2 1),
  1087 	(atac 1),
  1088 	(rtac adm_disj_lemma6 1),
  1089 	(atac 1),
  1090 	(atac 1),
  1091 	(rtac disjI1 1),
  1092 	(rtac adm_disj_lemma2 1),
  1093 	(atac 1),
  1094 	(rtac adm_disj_lemma10 1),
  1095 	(atac 1),
  1096 	(atac 1)
  1097 	]);
  1098 
  1099 val adm_impl = prove_goal  Fix.thy  
  1100 	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
  1101  (fn prems =>
  1102 	[
  1103 	(cut_facts_tac prems 1),
  1104 	(res_inst_tac [("P2","%x.~P(x)|Q(x)")] (adm_cong RS iffD1) 1),
  1105 	(fast_tac HOL_cs 1),
  1106 	(rtac adm_disj 1),
  1107 	(atac 1),
  1108 	(atac 1)
  1109 	]);
  1110 
  1111 
  1112 val adm_all2 = (allI RS adm_all);
  1113 
  1114 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
  1115 	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
  1116 	];
  1117 
  1118 (* ------------------------------------------------------------------------- *)
  1119 (* a result about functions with flat codomain                               *)
  1120 (* ------------------------------------------------------------------------- *)
  1121 
  1122 val flat_codom = prove_goalw Fix.thy [flat_def]
  1123 "[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
  1124  (fn prems =>
  1125 	[
  1126 	(cut_facts_tac prems 1),
  1127 	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
  1128 	(rtac disjI1 1),
  1129 	(rtac UU_I 1),
  1130 	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
  1131 	(atac 1),
  1132 	(rtac (minimal RS monofun_cfun_arg) 1),
  1133 	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
  1134 	(etac disjI1 1),
  1135 	(rtac disjI2 1),
  1136 	(rtac allI 1),
  1137 	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
  1138 	(atac 1),
  1139 	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
  1140 	(etac allE 1),(etac allE 1),
  1141 	(dtac mp 1),
  1142 	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
  1143 	(etac disjE 1),
  1144 	(contr_tac 1),
  1145 	(atac 1),
  1146 	(etac allE 1),
  1147 	(etac allE 1),
  1148 	(dtac mp 1),
  1149 	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
  1150 	(etac disjE 1),
  1151 	(contr_tac 1),
  1152 	(atac 1)
  1153 	]);