src/HOLCF/Up.thy
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Up.thy	Fri Mar 04 23:12:36 2005 +0100
     1.3 @@ -0,0 +1,625 @@
     1.4 +(*  Title:      HOLCF/Up1.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Franz Regensburger
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Lifting.
    1.10 +*)
    1.11 +
    1.12 +header {* The type of lifted values *}
    1.13 +
    1.14 +theory Up = Cfun + Sum_Type + Datatype:
    1.15 +
    1.16 +(* new type for lifting *)
    1.17 +
    1.18 +typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
    1.19 +by auto
    1.20 +
    1.21 +instance u :: (sq_ord)sq_ord ..
    1.22 +
    1.23 +consts
    1.24 +  Iup         :: "'a => ('a)u"
    1.25 +  Ifup        :: "('a->'b)=>('a)u => 'b"
    1.26 +
    1.27 +defs
    1.28 +  Iup_def:     "Iup x == Abs_Up(Inr(x))"
    1.29 +  Ifup_def:    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
    1.30 +
    1.31 +defs (overloaded)
    1.32 +  less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
    1.33 +               Inl(y1) => True          
    1.34 +             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
    1.35 +                                            | Inr(z2) => y2<<z2))"
    1.36 +
    1.37 +lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
    1.38 +apply (simp (no_asm) add: Up_def Abs_Up_inverse)
    1.39 +done
    1.40 +
    1.41 +lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
    1.42 +apply (unfold Iup_def)
    1.43 +apply (rule Rep_Up_inverse [THEN subst])
    1.44 +apply (rule_tac s = "Rep_Up z" in sumE)
    1.45 +apply (rule disjI1)
    1.46 +apply (rule_tac f = "Abs_Up" in arg_cong)
    1.47 +apply (rule unit_eq [THEN subst])
    1.48 +apply assumption
    1.49 +apply (rule disjI2)
    1.50 +apply (rule exI)
    1.51 +apply (rule_tac f = "Abs_Up" in arg_cong)
    1.52 +apply assumption
    1.53 +done
    1.54 +
    1.55 +lemma inj_Abs_Up: "inj(Abs_Up)"
    1.56 +apply (rule inj_on_inverseI)
    1.57 +apply (rule Abs_Up_inverse2)
    1.58 +done
    1.59 +
    1.60 +lemma inj_Rep_Up: "inj(Rep_Up)"
    1.61 +apply (rule inj_on_inverseI)
    1.62 +apply (rule Rep_Up_inverse)
    1.63 +done
    1.64 +
    1.65 +lemma inject_Iup: "Iup x=Iup y ==> x=y"
    1.66 +apply (unfold Iup_def)
    1.67 +apply (rule inj_Inr [THEN injD])
    1.68 +apply (rule inj_Abs_Up [THEN injD])
    1.69 +apply assumption
    1.70 +done
    1.71 +
    1.72 +declare inject_Iup [dest!]
    1.73 +
    1.74 +lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
    1.75 +apply (unfold Iup_def)
    1.76 +apply (rule notI)
    1.77 +apply (rule notE)
    1.78 +apply (rule Inl_not_Inr)
    1.79 +apply (rule sym)
    1.80 +apply (erule inj_Abs_Up [THEN injD])
    1.81 +done
    1.82 +
    1.83 +
    1.84 +lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    1.85 +apply (rule Exh_Up [THEN disjE])
    1.86 +apply fast
    1.87 +apply (erule exE)
    1.88 +apply fast
    1.89 +done
    1.90 +
    1.91 +lemma Ifup1: "Ifup(f)(Abs_Up(Inl ()))=UU"
    1.92 +apply (unfold Ifup_def)
    1.93 +apply (subst Abs_Up_inverse2)
    1.94 +apply (subst sum_case_Inl)
    1.95 +apply (rule refl)
    1.96 +done
    1.97 +
    1.98 +lemma Ifup2: 
    1.99 +        "Ifup(f)(Iup(x))=f$x"
   1.100 +apply (unfold Ifup_def Iup_def)
   1.101 +apply (subst Abs_Up_inverse2)
   1.102 +apply (subst sum_case_Inr)
   1.103 +apply (rule refl)
   1.104 +done
   1.105 +
   1.106 +lemmas Up0_ss = Ifup1 Ifup2
   1.107 +
   1.108 +declare Ifup1 [simp] Ifup2 [simp]
   1.109 +
   1.110 +lemma less_up1a: 
   1.111 +        "Abs_Up(Inl ())<< z"
   1.112 +apply (unfold less_up_def)
   1.113 +apply (subst Abs_Up_inverse2)
   1.114 +apply (subst sum_case_Inl)
   1.115 +apply (rule TrueI)
   1.116 +done
   1.117 +
   1.118 +lemma less_up1b: 
   1.119 +        "~(Iup x) << (Abs_Up(Inl ()))"
   1.120 +apply (unfold Iup_def less_up_def)
   1.121 +apply (rule notI)
   1.122 +apply (rule iffD1)
   1.123 +prefer 2 apply (assumption)
   1.124 +apply (subst Abs_Up_inverse2)
   1.125 +apply (subst Abs_Up_inverse2)
   1.126 +apply (subst sum_case_Inr)
   1.127 +apply (subst sum_case_Inl)
   1.128 +apply (rule refl)
   1.129 +done
   1.130 +
   1.131 +lemma less_up1c: 
   1.132 +        "(Iup x) << (Iup y)=(x<<y)"
   1.133 +apply (unfold Iup_def less_up_def)
   1.134 +apply (subst Abs_Up_inverse2)
   1.135 +apply (subst Abs_Up_inverse2)
   1.136 +apply (subst sum_case_Inr)
   1.137 +apply (subst sum_case_Inr)
   1.138 +apply (rule refl)
   1.139 +done
   1.140 +
   1.141 +declare less_up1a [iff] less_up1b [iff] less_up1c [iff]
   1.142 +
   1.143 +lemma refl_less_up: "(p::'a u) << p"
   1.144 +apply (rule_tac p = "p" in upE)
   1.145 +apply auto
   1.146 +done
   1.147 +
   1.148 +lemma antisym_less_up: "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
   1.149 +apply (rule_tac p = "p1" in upE)
   1.150 +apply simp
   1.151 +apply (rule_tac p = "p2" in upE)
   1.152 +apply (erule sym)
   1.153 +apply simp
   1.154 +apply (rule_tac p = "p2" in upE)
   1.155 +apply simp
   1.156 +apply simp
   1.157 +apply (drule antisym_less, assumption)
   1.158 +apply simp
   1.159 +done
   1.160 +
   1.161 +lemma trans_less_up: "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
   1.162 +apply (rule_tac p = "p1" in upE)
   1.163 +apply simp
   1.164 +apply (rule_tac p = "p2" in upE)
   1.165 +apply simp
   1.166 +apply (rule_tac p = "p3" in upE)
   1.167 +apply auto
   1.168 +apply (blast intro: trans_less)
   1.169 +done
   1.170 +
   1.171 +(* Class Instance u::(pcpo)po *)
   1.172 +
   1.173 +instance u :: (pcpo)po
   1.174 +apply (intro_classes)
   1.175 +apply (rule refl_less_up)
   1.176 +apply (rule antisym_less_up, assumption+)
   1.177 +apply (rule trans_less_up, assumption+)
   1.178 +done
   1.179 +
   1.180 +(* for compatibility with old HOLCF-Version *)
   1.181 +lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of                 
   1.182 +                Inl(y1) => True  
   1.183 +              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False  
   1.184 +                                             | Inr(z2) => y2<<z2))"
   1.185 +apply (fold less_up_def)
   1.186 +apply (rule refl)
   1.187 +done
   1.188 +
   1.189 +(* -------------------------------------------------------------------------*)
   1.190 +(* type ('a)u is pointed                                                    *)
   1.191 +(* ------------------------------------------------------------------------ *)
   1.192 +
   1.193 +lemma minimal_up: "Abs_Up(Inl ()) << z"
   1.194 +apply (simp (no_asm) add: less_up1a)
   1.195 +done
   1.196 +
   1.197 +lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
   1.198 +
   1.199 +lemma least_up: "EX x::'a u. ALL y. x<<y"
   1.200 +apply (rule_tac x = "Abs_Up (Inl ())" in exI)
   1.201 +apply (rule minimal_up [THEN allI])
   1.202 +done
   1.203 +
   1.204 +(* -------------------------------------------------------------------------*)
   1.205 +(* access to less_up in class po                                          *)
   1.206 +(* ------------------------------------------------------------------------ *)
   1.207 +
   1.208 +lemma less_up2b: "~ Iup(x) << Abs_Up(Inl ())"
   1.209 +apply (simp (no_asm) add: less_up1b)
   1.210 +done
   1.211 +
   1.212 +lemma less_up2c: "(Iup(x)<<Iup(y)) = (x<<y)"
   1.213 +apply (simp (no_asm) add: less_up1c)
   1.214 +done
   1.215 +
   1.216 +(* ------------------------------------------------------------------------ *)
   1.217 +(* Iup and Ifup are monotone                                               *)
   1.218 +(* ------------------------------------------------------------------------ *)
   1.219 +
   1.220 +lemma monofun_Iup: "monofun(Iup)"
   1.221 +
   1.222 +apply (unfold monofun)
   1.223 +apply (intro strip)
   1.224 +apply (erule less_up2c [THEN iffD2])
   1.225 +done
   1.226 +
   1.227 +lemma monofun_Ifup1: "monofun(Ifup)"
   1.228 +apply (unfold monofun)
   1.229 +apply (intro strip)
   1.230 +apply (rule less_fun [THEN iffD2])
   1.231 +apply (intro strip)
   1.232 +apply (rule_tac p = "xa" in upE)
   1.233 +apply simp
   1.234 +apply simp
   1.235 +apply (erule monofun_cfun_fun)
   1.236 +done
   1.237 +
   1.238 +lemma monofun_Ifup2: "monofun(Ifup(f))"
   1.239 +apply (unfold monofun)
   1.240 +apply (intro strip)
   1.241 +apply (rule_tac p = "x" in upE)
   1.242 +apply simp
   1.243 +apply simp
   1.244 +apply (rule_tac p = "y" in upE)
   1.245 +apply simp
   1.246 +apply simp
   1.247 +apply (erule monofun_cfun_arg)
   1.248 +done
   1.249 +
   1.250 +(* ------------------------------------------------------------------------ *)
   1.251 +(* Some kind of surjectivity lemma                                          *)
   1.252 +(* ------------------------------------------------------------------------ *)
   1.253 +
   1.254 +lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
   1.255 +apply simp
   1.256 +done
   1.257 +
   1.258 +(* ------------------------------------------------------------------------ *)
   1.259 +(* ('a)u is a cpo                                                           *)
   1.260 +(* ------------------------------------------------------------------------ *)
   1.261 +
   1.262 +lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]  
   1.263 +      ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   1.264 +apply (rule is_lubI)
   1.265 +apply (rule ub_rangeI)
   1.266 +apply (rule_tac p = "Y (i) " in upE)
   1.267 +apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
   1.268 +apply (erule sym)
   1.269 +apply (rule minimal_up)
   1.270 +apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
   1.271 +apply assumption
   1.272 +apply (rule less_up2c [THEN iffD2])
   1.273 +apply (rule is_ub_thelub)
   1.274 +apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.275 +apply (rule_tac p = "u" in upE)
   1.276 +apply (erule exE)
   1.277 +apply (erule exE)
   1.278 +apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
   1.279 +apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   1.280 +apply assumption
   1.281 +apply (rule less_up2b)
   1.282 +apply (erule subst)
   1.283 +apply (erule ub_rangeD)
   1.284 +apply (rule_tac t = "u" in up_lemma1 [THEN subst])
   1.285 +apply assumption
   1.286 +apply (rule less_up2c [THEN iffD2])
   1.287 +apply (rule is_lub_thelub)
   1.288 +apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.289 +apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
   1.290 +done
   1.291 +
   1.292 +lemma lub_up1b: "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())"
   1.293 +apply (rule is_lubI)
   1.294 +apply (rule ub_rangeI)
   1.295 +apply (rule_tac p = "Y (i) " in upE)
   1.296 +apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
   1.297 +apply assumption
   1.298 +apply (rule refl_less)
   1.299 +apply (rule notE)
   1.300 +apply (drule spec)
   1.301 +apply (drule spec)
   1.302 +apply assumption
   1.303 +apply assumption
   1.304 +apply (rule minimal_up)
   1.305 +done
   1.306 +
   1.307 +lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
   1.308 +(*
   1.309 +[| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==>
   1.310 + lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
   1.311 +*)
   1.312 +
   1.313 +lemmas thelub_up1b = lub_up1b [THEN thelubI, standard]
   1.314 +(*
   1.315 +[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   1.316 + lub (range ?Y1) = UU_up
   1.317 +*)
   1.318 +
   1.319 +lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
   1.320 +apply (rule disjE)
   1.321 +apply (rule_tac [2] exI)
   1.322 +apply (erule_tac [2] lub_up1a)
   1.323 +prefer 2 apply (assumption)
   1.324 +apply (rule_tac [2] exI)
   1.325 +apply (erule_tac [2] lub_up1b)
   1.326 +prefer 2 apply (assumption)
   1.327 +apply fast
   1.328 +done
   1.329 +
   1.330 +(* Class instance of  ('a)u for class pcpo *)
   1.331 +
   1.332 +instance u :: (pcpo)pcpo
   1.333 +apply (intro_classes)
   1.334 +apply (erule cpo_up)
   1.335 +apply (rule least_up)
   1.336 +done
   1.337 +
   1.338 +constdefs  
   1.339 +        up  :: "'a -> ('a)u"
   1.340 +       "up  == (LAM x. Iup(x))"
   1.341 +        fup :: "('a->'c)-> ('a)u -> 'c"
   1.342 +       "fup == (LAM f p. Ifup(f)(p))"
   1.343 +
   1.344 +translations
   1.345 +"case l of up$x => t1" == "fup$(LAM x. t1)$l"
   1.346 +
   1.347 +(* for compatibility with old HOLCF-Version *)
   1.348 +lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
   1.349 +apply (simp add: UU_def UU_up_def)
   1.350 +done
   1.351 +
   1.352 +(* -------------------------------------------------------------------------*)
   1.353 +(* some lemmas restated for class pcpo                                      *)
   1.354 +(* ------------------------------------------------------------------------ *)
   1.355 +
   1.356 +lemma less_up3b: "~ Iup(x) << UU"
   1.357 +apply (subst inst_up_pcpo)
   1.358 +apply (rule less_up2b)
   1.359 +done
   1.360 +
   1.361 +lemma defined_Iup2: "Iup(x) ~= UU"
   1.362 +apply (subst inst_up_pcpo)
   1.363 +apply (rule defined_Iup)
   1.364 +done
   1.365 +declare defined_Iup2 [iff]
   1.366 +
   1.367 +(* ------------------------------------------------------------------------ *)
   1.368 +(* continuity for Iup                                                       *)
   1.369 +(* ------------------------------------------------------------------------ *)
   1.370 +
   1.371 +lemma contlub_Iup: "contlub(Iup)"
   1.372 +apply (rule contlubI)
   1.373 +apply (intro strip)
   1.374 +apply (rule trans)
   1.375 +apply (rule_tac [2] thelub_up1a [symmetric])
   1.376 +prefer 3 apply fast
   1.377 +apply (erule_tac [2] monofun_Iup [THEN ch2ch_monofun])
   1.378 +apply (rule_tac f = "Iup" in arg_cong)
   1.379 +apply (rule lub_equal)
   1.380 +apply assumption
   1.381 +apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
   1.382 +apply (erule monofun_Iup [THEN ch2ch_monofun])
   1.383 +apply simp
   1.384 +done
   1.385 +
   1.386 +lemma cont_Iup: "cont(Iup)"
   1.387 +apply (rule monocontlub2cont)
   1.388 +apply (rule monofun_Iup)
   1.389 +apply (rule contlub_Iup)
   1.390 +done
   1.391 +declare cont_Iup [iff]
   1.392 +
   1.393 +(* ------------------------------------------------------------------------ *)
   1.394 +(* continuity for Ifup                                                     *)
   1.395 +(* ------------------------------------------------------------------------ *)
   1.396 +
   1.397 +lemma contlub_Ifup1: "contlub(Ifup)"
   1.398 +apply (rule contlubI)
   1.399 +apply (intro strip)
   1.400 +apply (rule trans)
   1.401 +apply (rule_tac [2] thelub_fun [symmetric])
   1.402 +apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
   1.403 +apply (rule ext)
   1.404 +apply (rule_tac p = "x" in upE)
   1.405 +apply simp
   1.406 +apply (rule lub_const [THEN thelubI, symmetric])
   1.407 +apply simp
   1.408 +apply (erule contlub_cfun_fun)
   1.409 +done
   1.410 +
   1.411 +
   1.412 +lemma contlub_Ifup2: "contlub(Ifup(f))"
   1.413 +apply (rule contlubI)
   1.414 +apply (intro strip)
   1.415 +apply (rule disjE)
   1.416 +defer 1
   1.417 +apply (subst thelub_up1a)
   1.418 +apply assumption
   1.419 +apply assumption
   1.420 +apply simp
   1.421 +prefer 2
   1.422 +apply (subst thelub_up1b)
   1.423 +apply assumption
   1.424 +apply assumption
   1.425 +apply simp
   1.426 +apply (rule chain_UU_I_inverse [symmetric])
   1.427 +apply (rule allI)
   1.428 +apply (rule_tac p = "Y(i)" in upE)
   1.429 +apply simp
   1.430 +apply simp
   1.431 +apply (subst contlub_cfun_arg)
   1.432 +apply  (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.433 +apply (rule lub_equal2)
   1.434 +apply   (rule_tac [2] monofun_Rep_CFun2 [THEN ch2ch_monofun])
   1.435 +apply   (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   1.436 +apply  (erule_tac [2] monofun_Ifup2 [THEN ch2ch_monofun])
   1.437 +apply (rule chain_mono2 [THEN exE])
   1.438 +prefer 2 apply   (assumption)
   1.439 +apply  (erule exE)
   1.440 +apply  (erule exE)
   1.441 +apply  (rule exI)
   1.442 +apply  (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   1.443 +apply   assumption
   1.444 +apply  (rule defined_Iup2)
   1.445 +apply (rule exI)
   1.446 +apply (intro strip)
   1.447 +apply (rule_tac p = "Y (i) " in upE)
   1.448 +prefer 2 apply simp
   1.449 +apply (rule_tac P = "Y (i) = UU" in notE)
   1.450 +apply  fast
   1.451 +apply (subst inst_up_pcpo)
   1.452 +apply assumption
   1.453 +apply fast
   1.454 +done
   1.455 +
   1.456 +lemma cont_Ifup1: "cont(Ifup)"
   1.457 +apply (rule monocontlub2cont)
   1.458 +apply (rule monofun_Ifup1)
   1.459 +apply (rule contlub_Ifup1)
   1.460 +done
   1.461 +
   1.462 +lemma cont_Ifup2: "cont(Ifup(f))"
   1.463 +apply (rule monocontlub2cont)
   1.464 +apply (rule monofun_Ifup2)
   1.465 +apply (rule contlub_Ifup2)
   1.466 +done
   1.467 +
   1.468 +
   1.469 +(* ------------------------------------------------------------------------ *)
   1.470 +(* continuous versions of lemmas for ('a)u                                  *)
   1.471 +(* ------------------------------------------------------------------------ *)
   1.472 +
   1.473 +lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
   1.474 +
   1.475 +apply (unfold up_def)
   1.476 +apply simp
   1.477 +apply (subst inst_up_pcpo)
   1.478 +apply (rule Exh_Up)
   1.479 +done
   1.480 +
   1.481 +lemma inject_up: "up$x=up$y ==> x=y"
   1.482 +apply (unfold up_def)
   1.483 +apply (rule inject_Iup)
   1.484 +apply auto
   1.485 +done
   1.486 +
   1.487 +lemma defined_up: " up$x ~= UU"
   1.488 +apply (unfold up_def)
   1.489 +apply auto
   1.490 +done
   1.491 +
   1.492 +lemma upE1: 
   1.493 +        "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
   1.494 +apply (unfold up_def)
   1.495 +apply (rule upE)
   1.496 +apply (simp only: inst_up_pcpo)
   1.497 +apply fast
   1.498 +apply simp
   1.499 +done
   1.500 +
   1.501 +lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
   1.502 +
   1.503 +lemma fup1: "fup$f$UU=UU"
   1.504 +apply (unfold up_def fup_def)
   1.505 +apply (subst inst_up_pcpo)
   1.506 +apply (subst beta_cfun)
   1.507 +apply (intro up_conts)
   1.508 +apply (subst beta_cfun)
   1.509 +apply (rule cont_Ifup2)
   1.510 +apply simp
   1.511 +done
   1.512 +
   1.513 +lemma fup2: "fup$f$(up$x)=f$x"
   1.514 +apply (unfold up_def fup_def)
   1.515 +apply (simplesubst beta_cfun)
   1.516 +apply (rule cont_Iup)
   1.517 +apply (subst beta_cfun)
   1.518 +apply (intro up_conts)
   1.519 +apply (subst beta_cfun)
   1.520 +apply (rule cont_Ifup2)
   1.521 +apply simp
   1.522 +done
   1.523 +
   1.524 +lemma less_up4b: "~ up$x << UU"
   1.525 +apply (unfold up_def fup_def)
   1.526 +apply simp
   1.527 +apply (rule less_up3b)
   1.528 +done
   1.529 +
   1.530 +lemma less_up4c: 
   1.531 +         "(up$x << up$y) = (x<<y)"
   1.532 +apply (unfold up_def fup_def)
   1.533 +apply simp
   1.534 +done
   1.535 +
   1.536 +lemma thelub_up2a: 
   1.537 +"[| chain(Y); EX i x. Y(i) = up$x |] ==> 
   1.538 +       lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   1.539 +apply (unfold up_def fup_def)
   1.540 +apply (subst beta_cfun)
   1.541 +apply (rule cont_Iup)
   1.542 +apply (subst beta_cfun)
   1.543 +apply (intro up_conts)
   1.544 +apply (subst beta_cfun [THEN ext])
   1.545 +apply (rule cont_Ifup2)
   1.546 +apply (rule thelub_up1a)
   1.547 +apply assumption
   1.548 +apply (erule exE)
   1.549 +apply (erule exE)
   1.550 +apply (rule exI)
   1.551 +apply (rule exI)
   1.552 +apply (erule box_equals)
   1.553 +apply (rule refl)
   1.554 +apply simp
   1.555 +done
   1.556 +
   1.557 +
   1.558 +
   1.559 +lemma thelub_up2b: 
   1.560 +"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
   1.561 +apply (unfold up_def fup_def)
   1.562 +apply (subst inst_up_pcpo)
   1.563 +apply (rule thelub_up1b)
   1.564 +apply assumption
   1.565 +apply (intro strip)
   1.566 +apply (drule spec)
   1.567 +apply (drule spec)
   1.568 +apply simp
   1.569 +done
   1.570 +
   1.571 +
   1.572 +lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
   1.573 +apply (rule iffI)
   1.574 +apply (erule exE)
   1.575 +apply simp
   1.576 +apply (rule defined_up)
   1.577 +apply (rule_tac p = "z" in upE1)
   1.578 +apply (erule notE)
   1.579 +apply assumption
   1.580 +apply (erule exI)
   1.581 +done
   1.582 +
   1.583 +
   1.584 +lemma thelub_up2a_rev: "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
   1.585 +apply (rule exE)
   1.586 +apply (rule chain_UU_I_inverse2)
   1.587 +apply (rule up_lemma2 [THEN iffD1])
   1.588 +apply (erule exI)
   1.589 +apply (rule exI)
   1.590 +apply (rule up_lemma2 [THEN iffD2])
   1.591 +apply assumption
   1.592 +done
   1.593 +
   1.594 +lemma thelub_up2b_rev: "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
   1.595 +apply (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
   1.596 +done
   1.597 +
   1.598 +
   1.599 +lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |  
   1.600 +                   lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   1.601 +apply (rule disjE)
   1.602 +apply (rule_tac [2] disjI1)
   1.603 +apply (rule_tac [2] thelub_up2b)
   1.604 +prefer 2 apply (assumption)
   1.605 +prefer 2 apply (assumption)
   1.606 +apply (rule_tac [2] disjI2)
   1.607 +apply (rule_tac [2] thelub_up2a)
   1.608 +prefer 2 apply (assumption)
   1.609 +prefer 2 apply (assumption)
   1.610 +apply fast
   1.611 +done
   1.612 +
   1.613 +lemma fup3: "fup$up$x=x"
   1.614 +apply (rule_tac p = "x" in upE1)
   1.615 +apply (simp add: fup1 fup2)
   1.616 +apply (simp add: fup1 fup2)
   1.617 +done
   1.618 +
   1.619 +(* ------------------------------------------------------------------------ *)
   1.620 +(* install simplifier for ('a)u                                             *)
   1.621 +(* ------------------------------------------------------------------------ *)
   1.622 +
   1.623 +declare fup1 [simp] fup2 [simp] defined_up [simp]
   1.624 +
   1.625 +end
   1.626 +
   1.627 +
   1.628 +