src/HOLCF/Up.thy
changeset 15593 24d770bbc44a
parent 15577 e16da3068ad6
child 15599 10cedbd5289e
     1.1 --- a/src/HOLCF/Up.thy	Tue Mar 08 00:28:46 2005 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Tue Mar 08 00:32:10 2005 +0100
     1.3 @@ -12,12 +12,9 @@
     1.4  imports Cfun Sum_Type Datatype
     1.5  begin
     1.6  
     1.7 -(* new type for lifting *)
     1.8 +subsection {* Definition of new type for lifting *}
     1.9  
    1.10 -typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
    1.11 -by auto
    1.12 -
    1.13 -instance u :: (sq_ord)sq_ord ..
    1.14 +typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
    1.15  
    1.16  consts
    1.17    Iup         :: "'a => ('a)u"
    1.18 @@ -27,15 +24,8 @@
    1.19    Iup_def:     "Iup x == Abs_Up(Inr(x))"
    1.20    Ifup_def:    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
    1.21  
    1.22 -defs (overloaded)
    1.23 -  less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
    1.24 -               Inl(y1) => True          
    1.25 -             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
    1.26 -                                            | Inr(z2) => y2<<z2))"
    1.27 -
    1.28  lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
    1.29 -apply (simp (no_asm) add: Up_def Abs_Up_inverse)
    1.30 -done
    1.31 +by (simp add: Up_def Abs_Up_inverse)
    1.32  
    1.33  lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
    1.34  apply (unfold Iup_def)
    1.35 @@ -61,15 +51,13 @@
    1.36  apply (rule Rep_Up_inverse)
    1.37  done
    1.38  
    1.39 -lemma inject_Iup: "Iup x=Iup y ==> x=y"
    1.40 +lemma inject_Iup [dest!]: "Iup x=Iup y ==> x=y"
    1.41  apply (unfold Iup_def)
    1.42  apply (rule inj_Inr [THEN injD])
    1.43  apply (rule inj_Abs_Up [THEN injD])
    1.44  apply assumption
    1.45  done
    1.46  
    1.47 -declare inject_Iup [dest!]
    1.48 -
    1.49  lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
    1.50  apply (unfold Iup_def)
    1.51  apply (rule notI)
    1.52 @@ -79,7 +67,6 @@
    1.53  apply (erule inj_Abs_Up [THEN injD])
    1.54  done
    1.55  
    1.56 -
    1.57  lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    1.58  apply (rule Exh_Up [THEN disjE])
    1.59  apply fast
    1.60 @@ -87,57 +74,43 @@
    1.61  apply fast
    1.62  done
    1.63  
    1.64 -lemma Ifup1: "Ifup(f)(Abs_Up(Inl ()))=UU"
    1.65 +lemma Ifup1 [simp]: "Ifup(f)(Abs_Up(Inl ()))=UU"
    1.66  apply (unfold Ifup_def)
    1.67  apply (subst Abs_Up_inverse2)
    1.68  apply (subst sum_case_Inl)
    1.69  apply (rule refl)
    1.70  done
    1.71  
    1.72 -lemma Ifup2: 
    1.73 -        "Ifup(f)(Iup(x))=f$x"
    1.74 +lemma Ifup2 [simp]: "Ifup(f)(Iup(x))=f$x"
    1.75  apply (unfold Ifup_def Iup_def)
    1.76  apply (subst Abs_Up_inverse2)
    1.77  apply (subst sum_case_Inr)
    1.78  apply (rule refl)
    1.79  done
    1.80  
    1.81 -lemmas Up0_ss = Ifup1 Ifup2
    1.82 +subsection {* Ordering on type @{typ "'a u"} *}
    1.83 +
    1.84 +instance u :: (sq_ord) sq_ord ..
    1.85  
    1.86 -declare Ifup1 [simp] Ifup2 [simp]
    1.87 +defs (overloaded)
    1.88 +  less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
    1.89 +               Inl(y1) => True          
    1.90 +             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
    1.91 +                                            | Inr(z2) => y2<<z2))"
    1.92  
    1.93 -lemma less_up1a: 
    1.94 +lemma less_up1a [iff]: 
    1.95          "Abs_Up(Inl ())<< z"
    1.96 -apply (unfold less_up_def)
    1.97 -apply (subst Abs_Up_inverse2)
    1.98 -apply (subst sum_case_Inl)
    1.99 -apply (rule TrueI)
   1.100 -done
   1.101 +by (simp add: less_up_def Abs_Up_inverse2)
   1.102  
   1.103 -lemma less_up1b: 
   1.104 +lemma less_up1b [iff]: 
   1.105          "~(Iup x) << (Abs_Up(Inl ()))"
   1.106 -apply (unfold Iup_def less_up_def)
   1.107 -apply (rule notI)
   1.108 -apply (rule iffD1)
   1.109 -prefer 2 apply (assumption)
   1.110 -apply (subst Abs_Up_inverse2)
   1.111 -apply (subst Abs_Up_inverse2)
   1.112 -apply (subst sum_case_Inr)
   1.113 -apply (subst sum_case_Inl)
   1.114 -apply (rule refl)
   1.115 -done
   1.116 +by (simp add: Iup_def less_up_def Abs_Up_inverse2)
   1.117  
   1.118 -lemma less_up1c: 
   1.119 +lemma less_up1c [iff]: 
   1.120          "(Iup x) << (Iup y)=(x<<y)"
   1.121 -apply (unfold Iup_def less_up_def)
   1.122 -apply (subst Abs_Up_inverse2)
   1.123 -apply (subst Abs_Up_inverse2)
   1.124 -apply (subst sum_case_Inr)
   1.125 -apply (subst sum_case_Inr)
   1.126 -apply (rule refl)
   1.127 -done
   1.128 +by (simp add: Iup_def less_up_def Abs_Up_inverse2)
   1.129  
   1.130 -declare less_up1a [iff] less_up1b [iff] less_up1c [iff]
   1.131 +subsection {* Type @{typ "'a u"} is a partial order *}
   1.132  
   1.133  lemma refl_less_up: "(p::'a u) << p"
   1.134  apply (rule_tac p = "p" in upE)
   1.135 @@ -167,16 +140,11 @@
   1.136  apply (blast intro: trans_less)
   1.137  done
   1.138  
   1.139 -(* Class Instance u::(pcpo)po *)
   1.140 +instance u :: (pcpo) po
   1.141 +by intro_classes
   1.142 +  (assumption | rule refl_less_up antisym_less_up trans_less_up)+
   1.143  
   1.144 -instance u :: (pcpo)po
   1.145 -apply (intro_classes)
   1.146 -apply (rule refl_less_up)
   1.147 -apply (rule antisym_less_up, assumption+)
   1.148 -apply (rule trans_less_up, assumption+)
   1.149 -done
   1.150 -
   1.151 -(* for compatibility with old HOLCF-Version *)
   1.152 +text {* for compatibility with old HOLCF-Version *}
   1.153  lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of                 
   1.154                  Inl(y1) => True  
   1.155                | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False  
   1.156 @@ -185,49 +153,14 @@
   1.157  apply (rule refl)
   1.158  done
   1.159  
   1.160 -(* -------------------------------------------------------------------------*)
   1.161 -(* type ('a)u is pointed                                                    *)
   1.162 -(* ------------------------------------------------------------------------ *)
   1.163 -
   1.164 -lemma minimal_up: "Abs_Up(Inl ()) << z"
   1.165 -apply (simp (no_asm) add: less_up1a)
   1.166 -done
   1.167 -
   1.168 -lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
   1.169 -
   1.170 -lemma least_up: "EX x::'a u. ALL y. x<<y"
   1.171 -apply (rule_tac x = "Abs_Up (Inl ())" in exI)
   1.172 -apply (rule minimal_up [THEN allI])
   1.173 -done
   1.174 -
   1.175 -(* -------------------------------------------------------------------------*)
   1.176 -(* access to less_up in class po                                          *)
   1.177 -(* ------------------------------------------------------------------------ *)
   1.178 -
   1.179 -lemma less_up2b: "~ Iup(x) << Abs_Up(Inl ())"
   1.180 -apply (simp (no_asm) add: less_up1b)
   1.181 -done
   1.182 -
   1.183 -lemma less_up2c: "(Iup(x)<<Iup(y)) = (x<<y)"
   1.184 -apply (simp (no_asm) add: less_up1c)
   1.185 -done
   1.186 -
   1.187 -(* ------------------------------------------------------------------------ *)
   1.188 -(* Iup and Ifup are monotone                                               *)
   1.189 -(* ------------------------------------------------------------------------ *)
   1.190 +subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
   1.191  
   1.192  lemma monofun_Iup: "monofun(Iup)"
   1.193 -
   1.194 -apply (unfold monofun)
   1.195 -apply (intro strip)
   1.196 -apply (erule less_up2c [THEN iffD2])
   1.197 -done
   1.198 +by (simp add: monofun)
   1.199  
   1.200  lemma monofun_Ifup1: "monofun(Ifup)"
   1.201 -apply (unfold monofun)
   1.202 -apply (intro strip)
   1.203 -apply (rule less_fun [THEN iffD2])
   1.204 -apply (intro strip)
   1.205 +apply (rule monofunI [rule_format])
   1.206 +apply (rule less_fun [THEN iffD2, rule_format])
   1.207  apply (rule_tac p = "xa" in upE)
   1.208  apply simp
   1.209  apply simp
   1.210 @@ -235,8 +168,7 @@
   1.211  done
   1.212  
   1.213  lemma monofun_Ifup2: "monofun(Ifup(f))"
   1.214 -apply (unfold monofun)
   1.215 -apply (intro strip)
   1.216 +apply (rule monofunI [rule_format])
   1.217  apply (rule_tac p = "x" in upE)
   1.218  apply simp
   1.219  apply simp
   1.220 @@ -246,17 +178,12 @@
   1.221  apply (erule monofun_cfun_arg)
   1.222  done
   1.223  
   1.224 -(* ------------------------------------------------------------------------ *)
   1.225 -(* Some kind of surjectivity lemma                                          *)
   1.226 -(* ------------------------------------------------------------------------ *)
   1.227 +subsection {* Type @{typ "'a u"} is a cpo *}
   1.228 +
   1.229 +text {* Some kind of surjectivity lemma *}
   1.230  
   1.231  lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
   1.232 -apply simp
   1.233 -done
   1.234 -
   1.235 -(* ------------------------------------------------------------------------ *)
   1.236 -(* ('a)u is a cpo                                                           *)
   1.237 -(* ------------------------------------------------------------------------ *)
   1.238 +by simp
   1.239  
   1.240  lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]  
   1.241        ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   1.242 @@ -265,10 +192,10 @@
   1.243  apply (rule_tac p = "Y (i) " in upE)
   1.244  apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
   1.245  apply (erule sym)
   1.246 -apply (rule minimal_up)
   1.247 +apply (rule less_up1a)
   1.248  apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
   1.249  apply assumption
   1.250 -apply (rule less_up2c [THEN iffD2])
   1.251 +apply (rule less_up1c [THEN iffD2])
   1.252  apply (rule is_ub_thelub)
   1.253  apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.254  apply (rule_tac p = "u" in upE)
   1.255 @@ -277,12 +204,12 @@
   1.256  apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
   1.257  apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   1.258  apply assumption
   1.259 -apply (rule less_up2b)
   1.260 +apply (rule less_up1b)
   1.261  apply (erule subst)
   1.262  apply (erule ub_rangeD)
   1.263  apply (rule_tac t = "u" in up_lemma1 [THEN subst])
   1.264  apply assumption
   1.265 -apply (rule less_up2c [THEN iffD2])
   1.266 +apply (rule less_up1c [THEN iffD2])
   1.267  apply (rule is_lub_thelub)
   1.268  apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.269  apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
   1.270 @@ -295,12 +222,8 @@
   1.271  apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
   1.272  apply assumption
   1.273  apply (rule refl_less)
   1.274 -apply (rule notE)
   1.275 -apply (drule spec)
   1.276 -apply (drule spec)
   1.277 -apply assumption
   1.278 -apply assumption
   1.279 -apply (rule minimal_up)
   1.280 +apply simp
   1.281 +apply (rule less_up1a)
   1.282  done
   1.283  
   1.284  lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
   1.285 @@ -316,60 +239,55 @@
   1.286  *)
   1.287  
   1.288  lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
   1.289 -apply (rule disjE)
   1.290 -apply (rule_tac [2] exI)
   1.291 -apply (erule_tac [2] lub_up1a)
   1.292 -prefer 2 apply (assumption)
   1.293 -apply (rule_tac [2] exI)
   1.294 -apply (erule_tac [2] lub_up1b)
   1.295 -prefer 2 apply (assumption)
   1.296 -apply fast
   1.297 -done
   1.298 -
   1.299 -(* Class instance of  ('a)u for class pcpo *)
   1.300 -
   1.301 -instance u :: (pcpo)pcpo
   1.302 -apply (intro_classes)
   1.303 -apply (erule cpo_up)
   1.304 -apply (rule least_up)
   1.305 +apply (case_tac "\<exists> i x. Y i = Iup x")
   1.306 +apply (rule exI)
   1.307 +apply (erule lub_up1a)
   1.308 +apply assumption
   1.309 +apply (rule exI)
   1.310 +apply (erule lub_up1b)
   1.311 +apply simp
   1.312  done
   1.313  
   1.314 -constdefs  
   1.315 -        up  :: "'a -> ('a)u"
   1.316 -       "up  == (LAM x. Iup(x))"
   1.317 -        fup :: "('a->'c)-> ('a)u -> 'c"
   1.318 -       "fup == (LAM f p. Ifup(f)(p))"
   1.319 +instance u :: (pcpo) cpo
   1.320 +by intro_classes (rule cpo_up)
   1.321 +
   1.322 +subsection {* Type @{typ "'a u"} is pointed *}
   1.323  
   1.324 -translations
   1.325 -"case l of up$x => t1" == "fup$(LAM x. t1)$l"
   1.326 +lemma minimal_up: "Abs_Up(Inl ()) << z"
   1.327 +by (rule less_up1a)
   1.328  
   1.329 -(* for compatibility with old HOLCF-Version *)
   1.330 -lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
   1.331 -apply (simp add: UU_def UU_up_def)
   1.332 +lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
   1.333 +
   1.334 +lemma least_up: "EX x::'a u. ALL y. x<<y"
   1.335 +apply (rule_tac x = "Abs_Up (Inl ())" in exI)
   1.336 +apply (rule minimal_up [THEN allI])
   1.337  done
   1.338  
   1.339 -(* -------------------------------------------------------------------------*)
   1.340 -(* some lemmas restated for class pcpo                                      *)
   1.341 -(* ------------------------------------------------------------------------ *)
   1.342 +instance u :: (pcpo) pcpo
   1.343 +by intro_classes (rule least_up)
   1.344 +
   1.345 +text {* for compatibility with old HOLCF-Version *}
   1.346 +lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
   1.347 +by (simp add: UU_def UU_up_def)
   1.348 +
   1.349 +text {* some lemmas restated for class pcpo *}
   1.350  
   1.351  lemma less_up3b: "~ Iup(x) << UU"
   1.352  apply (subst inst_up_pcpo)
   1.353 -apply (rule less_up2b)
   1.354 +apply (rule less_up1b)
   1.355  done
   1.356  
   1.357 -lemma defined_Iup2: "Iup(x) ~= UU"
   1.358 +lemma defined_Iup2 [iff]: "Iup(x) ~= UU"
   1.359  apply (subst inst_up_pcpo)
   1.360  apply (rule defined_Iup)
   1.361  done
   1.362 -declare defined_Iup2 [iff]
   1.363  
   1.364 -(* ------------------------------------------------------------------------ *)
   1.365 -(* continuity for Iup                                                       *)
   1.366 -(* ------------------------------------------------------------------------ *)
   1.367 +subsection {* Continuity of @{term Iup} and @{term Ifup} *}
   1.368 +
   1.369 +text {* continuity for @{term Iup} *}
   1.370  
   1.371  lemma contlub_Iup: "contlub(Iup)"
   1.372 -apply (rule contlubI)
   1.373 -apply (intro strip)
   1.374 +apply (rule contlubI [rule_format])
   1.375  apply (rule trans)
   1.376  apply (rule_tac [2] thelub_up1a [symmetric])
   1.377  prefer 3 apply fast
   1.378 @@ -382,20 +300,16 @@
   1.379  apply simp
   1.380  done
   1.381  
   1.382 -lemma cont_Iup: "cont(Iup)"
   1.383 +lemma cont_Iup [iff]: "cont(Iup)"
   1.384  apply (rule monocontlub2cont)
   1.385  apply (rule monofun_Iup)
   1.386  apply (rule contlub_Iup)
   1.387  done
   1.388 -declare cont_Iup [iff]
   1.389  
   1.390 -(* ------------------------------------------------------------------------ *)
   1.391 -(* continuity for Ifup                                                     *)
   1.392 -(* ------------------------------------------------------------------------ *)
   1.393 +text {* continuity for @{term Ifup} *}
   1.394  
   1.395  lemma contlub_Ifup1: "contlub(Ifup)"
   1.396 -apply (rule contlubI)
   1.397 -apply (intro strip)
   1.398 +apply (rule contlubI [rule_format])
   1.399  apply (rule trans)
   1.400  apply (rule_tac [2] thelub_fun [symmetric])
   1.401  apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
   1.402 @@ -407,10 +321,8 @@
   1.403  apply (erule contlub_cfun_fun)
   1.404  done
   1.405  
   1.406 -
   1.407  lemma contlub_Ifup2: "contlub(Ifup(f))"
   1.408 -apply (rule contlubI)
   1.409 -apply (intro strip)
   1.410 +apply (rule contlubI [rule_format])
   1.411  apply (rule disjE)
   1.412  defer 1
   1.413  apply (subst thelub_up1a)
   1.414 @@ -464,13 +376,20 @@
   1.415  apply (rule contlub_Ifup2)
   1.416  done
   1.417  
   1.418 +subsection {* Continuous versions of constants *}
   1.419  
   1.420 -(* ------------------------------------------------------------------------ *)
   1.421 -(* continuous versions of lemmas for ('a)u                                  *)
   1.422 -(* ------------------------------------------------------------------------ *)
   1.423 +constdefs  
   1.424 +        up  :: "'a -> ('a)u"
   1.425 +       "up  == (LAM x. Iup(x))"
   1.426 +        fup :: "('a->'c)-> ('a)u -> 'c"
   1.427 +       "fup == (LAM f p. Ifup(f)(p))"
   1.428 +
   1.429 +translations
   1.430 +"case l of up$x => t1" == "fup$(LAM x. t1)$l"
   1.431 +
   1.432 +text {* continuous versions of lemmas for @{typ "('a)u"} *}
   1.433  
   1.434  lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
   1.435 -
   1.436  apply (unfold up_def)
   1.437  apply simp
   1.438  apply (subst inst_up_pcpo)
   1.439 @@ -483,10 +402,8 @@
   1.440  apply auto
   1.441  done
   1.442  
   1.443 -lemma defined_up: " up$x ~= UU"
   1.444 -apply (unfold up_def)
   1.445 -apply auto
   1.446 -done
   1.447 +lemma defined_up [simp]: " up$x ~= UU"
   1.448 +by (simp add: up_def)
   1.449  
   1.450  lemma upE1: 
   1.451          "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
   1.452 @@ -499,7 +416,7 @@
   1.453  
   1.454  lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
   1.455  
   1.456 -lemma fup1: "fup$f$UU=UU"
   1.457 +lemma fup1 [simp]: "fup$f$UU=UU"
   1.458  apply (unfold up_def fup_def)
   1.459  apply (subst inst_up_pcpo)
   1.460  apply (subst beta_cfun)
   1.461 @@ -509,7 +426,7 @@
   1.462  apply simp
   1.463  done
   1.464  
   1.465 -lemma fup2: "fup$f$(up$x)=f$x"
   1.466 +lemma fup2 [simp]: "fup$f$(up$x)=f$x"
   1.467  apply (unfold up_def fup_def)
   1.468  apply (simplesubst beta_cfun)
   1.469  apply (rule cont_Iup)
   1.470 @@ -521,16 +438,10 @@
   1.471  done
   1.472  
   1.473  lemma less_up4b: "~ up$x << UU"
   1.474 -apply (unfold up_def fup_def)
   1.475 -apply simp
   1.476 -apply (rule less_up3b)
   1.477 -done
   1.478 +by (simp add: up_def fup_def less_up3b)
   1.479  
   1.480 -lemma less_up4c: 
   1.481 -         "(up$x << up$y) = (x<<y)"
   1.482 -apply (unfold up_def fup_def)
   1.483 -apply simp
   1.484 -done
   1.485 +lemma less_up4c: "(up$x << up$y) = (x<<y)"
   1.486 +by (simp add: up_def fup_def)
   1.487  
   1.488  lemma thelub_up2a: 
   1.489  "[| chain(Y); EX i x. Y(i) = up$x |] ==> 
   1.490 @@ -553,34 +464,25 @@
   1.491  apply simp
   1.492  done
   1.493  
   1.494 -
   1.495 -
   1.496  lemma thelub_up2b: 
   1.497  "[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
   1.498  apply (unfold up_def fup_def)
   1.499  apply (subst inst_up_pcpo)
   1.500 -apply (rule thelub_up1b)
   1.501 -apply assumption
   1.502 -apply (intro strip)
   1.503 -apply (drule spec)
   1.504 -apply (drule spec)
   1.505 +apply (erule thelub_up1b)
   1.506  apply simp
   1.507  done
   1.508  
   1.509 -
   1.510  lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
   1.511  apply (rule iffI)
   1.512  apply (erule exE)
   1.513  apply simp
   1.514 -apply (rule defined_up)
   1.515  apply (rule_tac p = "z" in upE1)
   1.516 -apply (erule notE)
   1.517 -apply assumption
   1.518 +apply simp
   1.519  apply (erule exI)
   1.520  done
   1.521  
   1.522 -
   1.523 -lemma thelub_up2a_rev: "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
   1.524 +lemma thelub_up2a_rev:
   1.525 +  "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
   1.526  apply (rule exE)
   1.527  apply (rule chain_UU_I_inverse2)
   1.528  apply (rule up_lemma2 [THEN iffD1])
   1.529 @@ -590,10 +492,9 @@
   1.530  apply assumption
   1.531  done
   1.532  
   1.533 -lemma thelub_up2b_rev: "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
   1.534 -apply (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
   1.535 -done
   1.536 -
   1.537 +lemma thelub_up2b_rev:
   1.538 +  "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
   1.539 +by (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
   1.540  
   1.541  lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |  
   1.542                     lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   1.543 @@ -611,17 +512,13 @@
   1.544  
   1.545  lemma fup3: "fup$up$x=x"
   1.546  apply (rule_tac p = "x" in upE1)
   1.547 -apply (simp add: fup1 fup2)
   1.548 -apply (simp add: fup1 fup2)
   1.549 +apply simp
   1.550 +apply simp
   1.551  done
   1.552  
   1.553 -(* ------------------------------------------------------------------------ *)
   1.554 -(* install simplifier for ('a)u                                             *)
   1.555 -(* ------------------------------------------------------------------------ *)
   1.556 +text {* for backward compatibility *}
   1.557  
   1.558 -declare fup1 [simp] fup2 [simp] defined_up [simp]
   1.559 +lemmas less_up2b = less_up1b
   1.560 +lemmas less_up2c = less_up1c
   1.561  
   1.562  end
   1.563 -
   1.564 -
   1.565 -