src/HOLCF/Up.thy
changeset 16319 1ff2965cc2e7
parent 16215 7ff978ca1920
child 16326 50a613925c4e
     1.1 --- a/src/HOLCF/Up.thy	Wed Jun 08 00:59:46 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jun 08 01:40:39 2005 +0200
     1.3 @@ -15,114 +15,79 @@
     1.4  
     1.5  subsection {* Definition of new type for lifting *}
     1.6  
     1.7 -typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
     1.8 +typedef (Up) 'a u = "UNIV :: 'a option set" ..
     1.9  
    1.10  consts
    1.11 -  Iup         :: "'a => ('a)u"
    1.12 -  Ifup        :: "('a->'b)=>('a)u => 'b::pcpo"
    1.13 +  Iup         :: "'a \<Rightarrow> 'a u"
    1.14 +  Ifup        :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
    1.15  
    1.16  defs
    1.17 -  Iup_def:     "Iup x == Abs_Up(Inr(x))"
    1.18 -  Ifup_def:    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
    1.19 +  Iup_def:     "Iup x \<equiv> Abs_Up (Some x)"
    1.20 +  Ifup_def:    "Ifup f x \<equiv> case Rep_Up x of None \<Rightarrow> \<bottom> | Some z \<Rightarrow> f\<cdot>z"
    1.21  
    1.22  lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
    1.23  by (simp add: Up_def Abs_Up_inverse)
    1.24  
    1.25 -lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
    1.26 +lemma Exh_Up: "z = Abs_Up None \<or> (\<exists>x. z = Iup x)"
    1.27  apply (unfold Iup_def)
    1.28  apply (rule Rep_Up_inverse [THEN subst])
    1.29 -apply (rule_tac s = "Rep_Up z" in sumE)
    1.30 -apply (rule disjI1)
    1.31 -apply (rule_tac f = "Abs_Up" in arg_cong)
    1.32 -apply (rule unit_eq [THEN subst])
    1.33 -apply assumption
    1.34 -apply (rule disjI2)
    1.35 -apply (rule exI)
    1.36 -apply (rule_tac f = "Abs_Up" in arg_cong)
    1.37 -apply assumption
    1.38 +apply (case_tac "Rep_Up z")
    1.39 +apply auto
    1.40  done
    1.41  
    1.42 -lemma inj_Abs_Up: "inj(Abs_Up)"
    1.43 +lemma inj_Abs_Up: "inj Abs_Up" (* worthless *)
    1.44  apply (rule inj_on_inverseI)
    1.45  apply (rule Abs_Up_inverse2)
    1.46  done
    1.47  
    1.48 -lemma inj_Rep_Up: "inj(Rep_Up)"
    1.49 +lemma inj_Rep_Up: "inj Rep_Up" (* worthless *)
    1.50  apply (rule inj_on_inverseI)
    1.51  apply (rule Rep_Up_inverse)
    1.52  done
    1.53  
    1.54 -lemma inject_Iup [dest!]: "Iup x=Iup y ==> x=y"
    1.55 -apply (unfold Iup_def)
    1.56 -apply (rule inj_Inr [THEN injD])
    1.57 -apply (rule inj_Abs_Up [THEN injD])
    1.58 -apply assumption
    1.59 -done
    1.60 +lemma Iup_eq [simp]: "(Iup x = Iup y) = (x = y)"
    1.61 +by (simp add: Iup_def Abs_Up_inject Up_def)
    1.62  
    1.63 -lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
    1.64 -apply (unfold Iup_def)
    1.65 -apply (rule notI)
    1.66 -apply (rule notE)
    1.67 -apply (rule Inl_not_Inr)
    1.68 -apply (rule sym)
    1.69 -apply (erule inj_Abs_Up [THEN injD])
    1.70 -done
    1.71 +lemma Iup_defined [simp]: "Iup x \<noteq> Abs_Up None"
    1.72 +by (simp add: Iup_def Abs_Up_inject Up_def)
    1.73  
    1.74 -lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    1.75 -apply (rule Exh_Up [THEN disjE])
    1.76 -apply fast
    1.77 -apply (erule exE)
    1.78 -apply fast
    1.79 -done
    1.80 +lemma upE: "\<lbrakk>p = Abs_Up None \<Longrightarrow> Q; \<And>x. p = Iup x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.81 +by (rule Exh_Up [THEN disjE], auto)
    1.82  
    1.83 -lemma Ifup1 [simp]: "Ifup(f)(Abs_Up(Inl ()))=UU"
    1.84 -apply (unfold Ifup_def)
    1.85 -apply (subst Abs_Up_inverse2)
    1.86 -apply (subst sum_case_Inl)
    1.87 -apply (rule refl)
    1.88 -done
    1.89 +lemma Ifup1 [simp]: "Ifup f (Abs_Up None) = \<bottom>"
    1.90 +by (simp add: Ifup_def Abs_Up_inverse2)
    1.91  
    1.92 -lemma Ifup2 [simp]: "Ifup(f)(Iup(x))=f$x"
    1.93 -apply (unfold Ifup_def Iup_def)
    1.94 -apply (subst Abs_Up_inverse2)
    1.95 -apply (subst sum_case_Inr)
    1.96 -apply (rule refl)
    1.97 -done
    1.98 +lemma Ifup2 [simp]: "Ifup f (Iup x) = f\<cdot>x"
    1.99 +by (simp add: Ifup_def Iup_def Abs_Up_inverse2)
   1.100  
   1.101  subsection {* Ordering on type @{typ "'a u"} *}
   1.102  
   1.103  instance u :: (sq_ord) sq_ord ..
   1.104  
   1.105  defs (overloaded)
   1.106 -  less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
   1.107 -               Inl(y1) => True          
   1.108 -             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
   1.109 -                                            | Inr(z2) => y2<<z2))"
   1.110 +  less_up_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>x1 x2. case Rep_Up x1 of
   1.111 +               None \<Rightarrow> True
   1.112 +             | Some y1 \<Rightarrow> (case Rep_Up x2 of None \<Rightarrow> False
   1.113 +                                           | Some y2 \<Rightarrow> y1 \<sqsubseteq> y2))"
   1.114  
   1.115 -lemma less_up1a [iff]: 
   1.116 -        "Abs_Up(Inl ())<< z"
   1.117 +lemma minimal_up [iff]: "Abs_Up None \<sqsubseteq> z"
   1.118  by (simp add: less_up_def Abs_Up_inverse2)
   1.119  
   1.120 -lemma less_up1b [iff]: 
   1.121 -        "~(Iup x) << (Abs_Up(Inl ()))"
   1.122 +lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Abs_Up None"
   1.123  by (simp add: Iup_def less_up_def Abs_Up_inverse2)
   1.124  
   1.125 -lemma less_up1c [iff]: 
   1.126 -        "(Iup x) << (Iup y)=(x<<y)"
   1.127 +lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
   1.128  by (simp add: Iup_def less_up_def Abs_Up_inverse2)
   1.129  
   1.130  subsection {* Type @{typ "'a u"} is a partial order *}
   1.131  
   1.132 -lemma refl_less_up: "(p::'a u) << p"
   1.133 -apply (rule_tac p = "p" in upE)
   1.134 -apply auto
   1.135 -done
   1.136 +lemma refl_less_up: "(p::'a u) \<sqsubseteq> p"
   1.137 +by (rule_tac p = "p" in upE, auto)
   1.138  
   1.139 -lemma antisym_less_up: "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
   1.140 +lemma antisym_less_up: "\<lbrakk>(p1::'a u) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2"
   1.141  apply (rule_tac p = "p1" in upE)
   1.142 +apply (rule_tac p = "p2" in upE)
   1.143  apply simp
   1.144 -apply (rule_tac p = "p2" in upE)
   1.145 -apply (erule sym)
   1.146  apply simp
   1.147  apply (rule_tac p = "p2" in upE)
   1.148  apply simp
   1.149 @@ -131,210 +96,104 @@
   1.150  apply simp
   1.151  done
   1.152  
   1.153 -lemma trans_less_up: "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
   1.154 +lemma trans_less_up: "\<lbrakk>(p1::'a u) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3"
   1.155  apply (rule_tac p = "p1" in upE)
   1.156  apply simp
   1.157  apply (rule_tac p = "p2" in upE)
   1.158  apply simp
   1.159  apply (rule_tac p = "p3" in upE)
   1.160 -apply auto
   1.161 -apply (blast intro: trans_less)
   1.162 +apply simp
   1.163 +apply (auto elim: trans_less)
   1.164  done
   1.165  
   1.166  instance u :: (cpo) po
   1.167  by intro_classes
   1.168    (assumption | rule refl_less_up antisym_less_up trans_less_up)+
   1.169  
   1.170 -text {* for compatibility with old HOLCF-Version *}
   1.171 -lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of                 
   1.172 -                Inl(y1) => True  
   1.173 -              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False  
   1.174 -                                             | Inr(z2) => y2<<z2))"
   1.175 -apply (fold less_up_def)
   1.176 -apply (rule refl)
   1.177 -done
   1.178 -
   1.179 -subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
   1.180 -
   1.181 -lemma monofun_Iup: "monofun(Iup)"
   1.182 -by (simp add: monofun_def)
   1.183 -
   1.184 -lemma monofun_Ifup1: "monofun(Ifup)"
   1.185 -apply (rule monofunI)
   1.186 -apply (rule less_fun [THEN iffD2, rule_format])
   1.187 -apply (rule_tac p = "xa" in upE)
   1.188 -apply simp
   1.189 -apply simp
   1.190 -apply (erule monofun_cfun_fun)
   1.191 -done
   1.192 -
   1.193 -lemma monofun_Ifup2: "monofun(Ifup(f))"
   1.194 -apply (rule monofunI)
   1.195 -apply (rule_tac p = "x" in upE)
   1.196 -apply simp
   1.197 -apply simp
   1.198 -apply (rule_tac p = "y" in upE)
   1.199 -apply simp
   1.200 -apply simp
   1.201 -apply (erule monofun_cfun_arg)
   1.202 -done
   1.203 -
   1.204  subsection {* Type @{typ "'a u"} is a cpo *}
   1.205  
   1.206 -text {* Some kind of surjectivity lemma *}
   1.207 -
   1.208 -lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
   1.209 -by simp
   1.210 -
   1.211 -lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]  
   1.212 -      ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   1.213 +lemma is_lub_Iup:
   1.214 +  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
   1.215  apply (rule is_lubI)
   1.216  apply (rule ub_rangeI)
   1.217 -apply (rule_tac p = "Y (i) " in upE)
   1.218 -apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
   1.219 -apply (erule sym)
   1.220 -apply (rule less_up1a)
   1.221 -apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
   1.222 -apply assumption
   1.223 -apply (rule less_up1c [THEN iffD2])
   1.224 -apply (rule is_ub_thelub)
   1.225 -apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.226 -apply (rule_tac p = "u" in upE)
   1.227 -apply (erule exE)
   1.228 -apply (erule exE)
   1.229 -apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
   1.230 -apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
   1.231 -apply assumption
   1.232 -apply (rule less_up1b)
   1.233 -apply (erule subst)
   1.234 -apply (erule ub_rangeD)
   1.235 -apply (rule_tac t = "u" in up_lemma1 [THEN subst])
   1.236 -apply assumption
   1.237 -apply (rule less_up1c [THEN iffD2])
   1.238 -apply (rule is_lub_thelub)
   1.239 -apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.240 -apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
   1.241 -done
   1.242 -
   1.243 -lemma lub_up1b: "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())"
   1.244 -apply (rule is_lubI)
   1.245 +apply (subst Iup_less)
   1.246 +apply (erule is_ub_lub)
   1.247 +apply (rule_tac p="u" in upE)
   1.248 +apply (drule ub_rangeD)
   1.249 +apply simp
   1.250 +apply simp
   1.251 +apply (erule is_lub_lub)
   1.252  apply (rule ub_rangeI)
   1.253 -apply (rule_tac p = "Y (i) " in upE)
   1.254 -apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
   1.255 -apply assumption
   1.256 -apply (rule refl_less)
   1.257 +apply (drule_tac i=i in ub_rangeD)
   1.258  apply simp
   1.259 -apply (rule less_up1a)
   1.260 -done
   1.261 -
   1.262 -lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
   1.263 -(*
   1.264 -[| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==>
   1.265 - lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
   1.266 -*)
   1.267 -
   1.268 -lemmas thelub_up1b = lub_up1b [THEN thelubI, standard]
   1.269 -(*
   1.270 -[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   1.271 - lub (range ?Y1) = UU_up
   1.272 -*)
   1.273 -
   1.274 -text {* New versions where @{typ "'a"} does not have to be a pcpo *}
   1.275 -
   1.276 -lemma up_lemma1a: "EX x. z=Iup(x) ==> Iup(THE a. Iup a = z) = z"
   1.277 -apply (erule exE)
   1.278 -apply (rule theI)
   1.279 -apply (erule sym)
   1.280 -apply simp
   1.281 -apply (erule inject_Iup)
   1.282  done
   1.283  
   1.284  text {* Now some lemmas about chains of @{typ "'a u"} elements *}
   1.285  
   1.286 -lemma up_chain_lemma1:
   1.287 -  "[| chain Y; EX x. Y j = Iup x |] ==> EX x. Y (i + j) = Iup x"
   1.288 +lemma up_lemma1: "z \<noteq> Abs_Up None \<Longrightarrow> Iup (THE a. Iup a = z) = z"
   1.289 +by (rule_tac p="z" in upE, simp_all)
   1.290 +
   1.291 +lemma up_lemma2:
   1.292 +  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Abs_Up None"
   1.293 +apply (erule contrapos_nn)
   1.294  apply (drule_tac x="j" and y="i + j" in chain_mono3)
   1.295  apply (rule le_add2)
   1.296 -apply (rule_tac p="Y (i + j)" in upE)
   1.297 -apply auto
   1.298 +apply (rule_tac p="Y j" in upE)
   1.299 +apply assumption
   1.300 +apply simp
   1.301  done
   1.302  
   1.303 -lemma up_chain_lemma2:
   1.304 -  "[| chain Y; EX x. Y j = Iup x |] ==>
   1.305 -    Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
   1.306 -apply (drule_tac i=i in up_chain_lemma1)
   1.307 -apply assumption
   1.308 -apply (erule up_lemma1a)
   1.309 -done
   1.310 +lemma up_lemma3:
   1.311 +  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
   1.312 +by (rule up_lemma1 [OF up_lemma2])
   1.313  
   1.314 -lemma up_chain_lemma3:
   1.315 -  "[| chain Y; EX x. Y j = Iup x |] ==> chain (%i. THE a. Iup a = Y (i + j))"
   1.316 +lemma up_lemma4:
   1.317 +  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
   1.318  apply (rule chainI)
   1.319 -apply (rule less_up1c [THEN iffD1])
   1.320 -apply (simp only: up_chain_lemma2)
   1.321 +apply (rule Iup_less [THEN iffD1])
   1.322 +apply (subst up_lemma3, assumption+)+
   1.323  apply (simp add: chainE)
   1.324  done
   1.325  
   1.326 -lemma up_chain_lemma4:
   1.327 -  "[| chain Y; EX x. Y j = Iup x |] ==>
   1.328 -    (%i. Y (i + j)) = (%i. Iup (THE a. Iup a = Y (i + j)))"
   1.329 -apply (rule ext)
   1.330 -apply (rule up_chain_lemma2 [symmetric])
   1.331 -apply assumption+
   1.332 -done
   1.333 +lemma up_lemma5:
   1.334 +  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow>
   1.335 +    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
   1.336 +by (rule ext, rule up_lemma3 [symmetric])
   1.337  
   1.338 -lemma is_lub_range_shift:
   1.339 -  "[| chain S; range (%i. S (i + j)) <<| x |] ==> range S <<| x"
   1.340 -apply (rule is_lubI)
   1.341 -apply (rule ub_rangeI)
   1.342 -apply (rule trans_less)
   1.343 -apply (erule chain_mono3)
   1.344 -apply (rule le_add1)
   1.345 -apply (erule is_ub_lub)
   1.346 -apply (erule is_lub_lub)
   1.347 -apply (rule ub_rangeI)
   1.348 -apply (erule ub_rangeD)
   1.349 +lemma up_lemma6:
   1.350 +  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk>  
   1.351 +      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
   1.352 +apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
   1.353 +apply assumption
   1.354 +apply (subst up_lemma5, assumption+)
   1.355 +apply (rule is_lub_Iup)
   1.356 +apply (rule thelubE [OF _ refl])
   1.357 +apply (rule up_lemma4, assumption+)
   1.358  done
   1.359  
   1.360 -lemma is_lub_Iup:
   1.361 -  "range S <<| x \<Longrightarrow> range (%i. Iup (S i)) <<| Iup x"
   1.362 -apply (rule is_lubI)
   1.363 -apply (rule ub_rangeI)
   1.364 -apply (subst less_up1c)
   1.365 -apply (erule is_ub_lub)
   1.366 -apply (rule_tac p=u in upE)
   1.367 -apply (drule ub_rangeD)
   1.368 -apply (simp only: less_up1b)
   1.369 -apply (simp only: less_up1c)
   1.370 -apply (erule is_lub_lub)
   1.371 -apply (rule ub_rangeI)
   1.372 -apply (drule_tac i=i in ub_rangeD)
   1.373 -apply (simp only: less_up1c)
   1.374 +lemma up_chain_cases:
   1.375 +  "chain Y \<Longrightarrow>
   1.376 +   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
   1.377 +   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Abs_Up None))"
   1.378 +apply (rule disjCI)
   1.379 +apply (simp add: expand_fun_eq)
   1.380 +apply (erule exE, rename_tac j)
   1.381 +apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
   1.382 +apply (rule conjI)
   1.383 +apply (simp add: up_lemma4)
   1.384 +apply (rule conjI)
   1.385 +apply (simp add: up_lemma6 [THEN thelubI])
   1.386 +apply (rule_tac x=j in exI)
   1.387 +apply (simp add: up_lemma3)
   1.388  done
   1.389  
   1.390 -lemma lub_up1c: "[|chain(Y); EX x. Y(j)=Iup(x)|]  
   1.391 -      ==> range(Y) <<| Iup(lub(range(%i. THE a. Iup a = Y(i + j))))"
   1.392 -apply (rule_tac j=j in is_lub_range_shift)
   1.393 -apply assumption
   1.394 -apply (subst up_chain_lemma4)
   1.395 -apply assumption+
   1.396 -apply (rule is_lub_Iup)
   1.397 -apply (rule thelubE [OF _ refl])
   1.398 -apply (rule up_chain_lemma3)
   1.399 -apply assumption+
   1.400 -done
   1.401 -
   1.402 -lemmas thelub_up1c = lub_up1c [THEN thelubI, standard]
   1.403 -
   1.404 -lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
   1.405 -apply (case_tac "EX i x. Y i = Iup x")
   1.406 -apply (erule exE)
   1.407 -apply (rule exI)
   1.408 -apply (erule lub_up1c)
   1.409 -apply assumption
   1.410 -apply (rule exI)
   1.411 -apply (erule lub_up1b)
   1.412 -apply simp
   1.413 +lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
   1.414 +apply (frule up_chain_cases, safe)
   1.415 +apply (rule_tac x="Iup (lub (range A))" in exI)
   1.416 +apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
   1.417 +apply (simp add: is_lub_Iup thelubE)
   1.418 +apply (rule_tac x="Abs_Up None" in exI)
   1.419 +apply (rule lub_const)
   1.420  done
   1.421  
   1.422  instance u :: (cpo) cpo
   1.423 @@ -342,13 +201,8 @@
   1.424  
   1.425  subsection {* Type @{typ "'a u"} is pointed *}
   1.426  
   1.427 -lemma minimal_up: "Abs_Up(Inl ()) << z"
   1.428 -by (rule less_up1a)
   1.429 -
   1.430 -lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
   1.431 -
   1.432 -lemma least_up: "EX x::'a u. ALL y. x<<y"
   1.433 -apply (rule_tac x = "Abs_Up (Inl ())" in exI)
   1.434 +lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
   1.435 +apply (rule_tac x = "Abs_Up None" in exI)
   1.436  apply (rule minimal_up [THEN allI])
   1.437  done
   1.438  
   1.439 @@ -356,244 +210,106 @@
   1.440  by intro_classes (rule least_up)
   1.441  
   1.442  text {* for compatibility with old HOLCF-Version *}
   1.443 -lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
   1.444 -by (simp add: UU_def UU_up_def)
   1.445 +lemma inst_up_pcpo: "\<bottom> = Abs_Up None"
   1.446 +by (rule minimal_up [THEN UU_I, symmetric])
   1.447  
   1.448  text {* some lemmas restated for class pcpo *}
   1.449  
   1.450 -lemma less_up3b: "~ Iup(x) << UU"
   1.451 +lemma less_up3b: "~ Iup(x) \<sqsubseteq> \<bottom>"
   1.452  apply (subst inst_up_pcpo)
   1.453 -apply (rule less_up1b)
   1.454 +apply simp
   1.455  done
   1.456  
   1.457 -lemma defined_Iup2 [iff]: "Iup(x) ~= UU"
   1.458 +lemma defined_Iup2 [iff]: "Iup(x) ~= \<bottom>"
   1.459  apply (subst inst_up_pcpo)
   1.460 -apply (rule defined_Iup)
   1.461 +apply (rule Iup_defined)
   1.462  done
   1.463  
   1.464  subsection {* Continuity of @{term Iup} and @{term Ifup} *}
   1.465  
   1.466  text {* continuity for @{term Iup} *}
   1.467  
   1.468 -lemma cont_Iup [iff]: "cont(Iup)"
   1.469 +lemma cont_Iup: "cont Iup"
   1.470  apply (rule contI)
   1.471  apply (rule is_lub_Iup)
   1.472  apply (erule thelubE [OF _ refl])
   1.473  done
   1.474  
   1.475 -lemmas contlub_Iup = cont_Iup [THEN cont2contlub]
   1.476 -
   1.477  text {* continuity for @{term Ifup} *}
   1.478  
   1.479 -lemma contlub_Ifup1: "contlub(Ifup)"
   1.480 -apply (rule contlubI)
   1.481 -apply (rule trans)
   1.482 -apply (rule_tac [2] thelub_fun [symmetric])
   1.483 -apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
   1.484 -apply (rule ext)
   1.485 -apply (rule_tac p = "x" in upE)
   1.486 -apply simp
   1.487 -apply (rule lub_const [THEN thelubI, symmetric])
   1.488 -apply simp
   1.489 -apply (erule contlub_cfun_fun)
   1.490 +lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
   1.491 +apply (rule contI)
   1.492 +apply (rule_tac p="x" in upE)
   1.493 +apply (simp add: lub_const)
   1.494 +apply (simp add: cont_cfun_fun)
   1.495  done
   1.496  
   1.497 -lemma contlub_Ifup2: "contlub(Ifup(f))"
   1.498 -apply (rule contlubI)
   1.499 -apply (case_tac "EX i x. Y i = Iup x")
   1.500 -apply (erule exE)
   1.501 -apply (subst thelub_up1c)
   1.502 -apply assumption
   1.503 -apply assumption
   1.504 -apply simp
   1.505 -prefer 2
   1.506 -apply (subst thelub_up1b)
   1.507 -apply assumption
   1.508 -apply simp
   1.509 -apply simp
   1.510 -apply (rule chain_UU_I_inverse [symmetric])
   1.511 -apply (rule allI)
   1.512 -apply (rule_tac p = "Y(i)" in upE)
   1.513 -apply simp
   1.514 +lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
   1.515 +apply (rule monofunI)
   1.516 +apply (rule_tac p="x" in upE)
   1.517  apply simp
   1.518 -apply (subst contlub_cfun_arg)
   1.519 -apply  (erule up_chain_lemma3)
   1.520 -apply  assumption
   1.521 -apply (rule trans)
   1.522 -prefer 2
   1.523 -apply (rule_tac j=i in lub_range_shift)
   1.524 -apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.525 -apply (rule lub_equal [rule_format])
   1.526 -apply (rule chain_monofun)
   1.527 -apply (erule up_chain_lemma3)
   1.528 -apply assumption
   1.529 -apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
   1.530 -apply (erule chain_shift)
   1.531 -apply (drule_tac i=k in up_chain_lemma1)
   1.532 -apply assumption
   1.533 -apply clarify
   1.534 +apply (rule_tac p="y" in upE)
   1.535  apply simp
   1.536 -apply (subst the_equality)
   1.537 -apply (rule refl)
   1.538 -apply (erule inject_Iup)
   1.539 -apply (rule refl)
   1.540 +apply (simp add: monofun_cfun_arg)
   1.541  done
   1.542  
   1.543 -lemma cont_Ifup1: "cont(Ifup)"
   1.544 -apply (rule monocontlub2cont)
   1.545 -apply (rule monofun_Ifup1)
   1.546 -apply (rule contlub_Ifup1)
   1.547 -done
   1.548 -
   1.549 -lemma cont_Ifup2: "cont(Ifup(f))"
   1.550 -apply (rule monocontlub2cont)
   1.551 -apply (rule monofun_Ifup2)
   1.552 -apply (rule contlub_Ifup2)
   1.553 +lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
   1.554 +apply (rule contI)
   1.555 +apply (frule up_chain_cases, safe)
   1.556 +apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
   1.557 +apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
   1.558 +apply (simp add: cont_cfun_arg)
   1.559 +apply (simp add: thelub_const lub_const)
   1.560  done
   1.561  
   1.562  subsection {* Continuous versions of constants *}
   1.563  
   1.564  constdefs  
   1.565 -        up  :: "'a -> ('a)u"
   1.566 -       "up  == (LAM x. Iup(x))"
   1.567 -        fup :: "('a->'c)-> ('a)u -> 'c::pcpo"
   1.568 -       "fup == (LAM f p. Ifup(f)(p))"
   1.569 +  up  :: "'a \<rightarrow> 'a u"
   1.570 +  "up \<equiv> \<Lambda> x. Iup x"
   1.571 +
   1.572 +  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
   1.573 +  "fup \<equiv> \<Lambda> f p. Ifup f p"
   1.574  
   1.575  translations
   1.576 -"case l of up$x => t1" == "fup$(LAM x. t1)$l"
   1.577 +"case l of up\<cdot>x => t1" == "fup\<cdot>(LAM x. t1)\<cdot>l"
   1.578  
   1.579  text {* continuous versions of lemmas for @{typ "('a)u"} *}
   1.580  
   1.581 -lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
   1.582 -apply (unfold up_def)
   1.583 -apply simp
   1.584 -apply (subst inst_up_pcpo)
   1.585 -apply (rule Exh_Up)
   1.586 -done
   1.587 -
   1.588 -lemma inject_up: "up$x=up$y ==> x=y"
   1.589 -apply (unfold up_def)
   1.590 -apply (rule inject_Iup)
   1.591 -apply auto
   1.592 -done
   1.593 -
   1.594 -lemma defined_up [simp]: " up$x ~= UU"
   1.595 -by (simp add: up_def)
   1.596 -
   1.597 -lemma upE1: 
   1.598 -        "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
   1.599 -apply (unfold up_def)
   1.600 -apply (rule upE)
   1.601 -apply (simp only: inst_up_pcpo)
   1.602 -apply fast
   1.603 -apply simp
   1.604 -done
   1.605 -
   1.606 -lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
   1.607 -
   1.608 -lemma fup1 [simp]: "fup$f$UU=UU"
   1.609 -apply (unfold up_def fup_def)
   1.610 -apply (subst inst_up_pcpo)
   1.611 -apply (subst beta_cfun)
   1.612 -apply (intro up_conts)
   1.613 -apply (subst beta_cfun)
   1.614 -apply (rule cont_Ifup2)
   1.615 -apply simp
   1.616 -done
   1.617 -
   1.618 -lemma fup2 [simp]: "fup$f$(up$x)=f$x"
   1.619 -apply (unfold up_def fup_def)
   1.620 -apply (simplesubst beta_cfun)
   1.621 -apply (rule cont_Iup)
   1.622 -apply (subst beta_cfun)
   1.623 -apply (intro up_conts)
   1.624 -apply (subst beta_cfun)
   1.625 -apply (rule cont_Ifup2)
   1.626 -apply simp
   1.627 +lemma Exh_Up1: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
   1.628 +apply (rule_tac p="z" in upE)
   1.629 +apply (simp add: inst_up_pcpo)
   1.630 +apply (simp add: up_def cont_Iup)
   1.631  done
   1.632  
   1.633 -lemma less_up4b: "~ up$x << UU"
   1.634 -by (simp add: up_def fup_def less_up3b)
   1.635 +lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
   1.636 +by (simp add: up_def cont_Iup)
   1.637  
   1.638 -lemma less_up4c: "(up$x << up$y) = (x<<y)"
   1.639 -by (simp add: up_def fup_def)
   1.640 +lemma up_eq: "(up\<cdot>x = up\<cdot>y) = (x = y)"
   1.641 +by (rule iffI, erule up_inject, simp)
   1.642 +
   1.643 +lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
   1.644 +by (simp add: up_def cont_Iup inst_up_pcpo)
   1.645  
   1.646 -lemma thelub_up2a: 
   1.647 -"[| chain(Y); EX i x. Y(i) = up$x |] ==> 
   1.648 -       lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   1.649 -apply (unfold up_def fup_def)
   1.650 -apply (subst beta_cfun)
   1.651 -apply (rule cont_Iup)
   1.652 -apply (subst beta_cfun)
   1.653 -apply (intro up_conts)
   1.654 -apply (subst beta_cfun [THEN ext])
   1.655 -apply (rule cont_Ifup2)
   1.656 -apply (rule thelub_up1a)
   1.657 -apply assumption
   1.658 -apply (erule exE)
   1.659 -apply (erule exE)
   1.660 -apply (rule exI)
   1.661 -apply (rule exI)
   1.662 -apply (erule box_equals)
   1.663 -apply (rule refl)
   1.664 -apply simp
   1.665 -done
   1.666 +lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   1.667 +by (simp add: eq_UU_iff [symmetric])
   1.668  
   1.669 -lemma thelub_up2b: 
   1.670 -"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
   1.671 -apply (unfold up_def fup_def)
   1.672 -apply (subst inst_up_pcpo)
   1.673 -apply (erule thelub_up1b)
   1.674 -apply simp
   1.675 +lemma up_less: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
   1.676 +by (simp add: up_def cont_Iup)
   1.677 +
   1.678 +lemma upE1: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   1.679 +apply (rule_tac p="p" in upE)
   1.680 +apply (simp add: inst_up_pcpo)
   1.681 +apply (simp add: up_def cont_Iup)
   1.682  done
   1.683  
   1.684 -lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
   1.685 -apply (rule iffI)
   1.686 -apply (erule exE)
   1.687 -apply simp
   1.688 -apply (rule_tac p = "z" in upE1)
   1.689 -apply simp
   1.690 -apply (erule exI)
   1.691 -done
   1.692 -
   1.693 -lemma thelub_up2a_rev:
   1.694 -  "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
   1.695 -apply (rule exE)
   1.696 -apply (rule chain_UU_I_inverse2)
   1.697 -apply (rule up_lemma2 [THEN iffD1])
   1.698 -apply (erule exI)
   1.699 -apply (rule exI)
   1.700 -apply (rule up_lemma2 [THEN iffD2])
   1.701 -apply assumption
   1.702 -done
   1.703 -
   1.704 -lemma thelub_up2b_rev:
   1.705 -  "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
   1.706 -by (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
   1.707 +lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
   1.708 +by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
   1.709  
   1.710 -lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |  
   1.711 -                   lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
   1.712 -apply (rule disjE)
   1.713 -apply (rule_tac [2] disjI1)
   1.714 -apply (rule_tac [2] thelub_up2b)
   1.715 -prefer 2 apply (assumption)
   1.716 -prefer 2 apply (assumption)
   1.717 -apply (rule_tac [2] disjI2)
   1.718 -apply (rule_tac [2] thelub_up2a)
   1.719 -prefer 2 apply (assumption)
   1.720 -prefer 2 apply (assumption)
   1.721 -apply fast
   1.722 -done
   1.723 +lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
   1.724 +by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 )
   1.725  
   1.726 -lemma fup3: "fup$up$x=x"
   1.727 -apply (rule_tac p = "x" in upE1)
   1.728 -apply simp
   1.729 -apply simp
   1.730 -done
   1.731 -
   1.732 -text {* for backward compatibility *}
   1.733 -
   1.734 -lemmas less_up2b = less_up1b
   1.735 -lemmas less_up2c = less_up1c
   1.736 +lemma fup3: "fup\<cdot>up\<cdot>x = x"
   1.737 +by (rule_tac p=x in upE1, simp_all)
   1.738  
   1.739  end