move lemmas into locales;
authorhuffman
Thu Jun 19 22:50:58 2008 +0200 (2008-06-19)
changeset 27289c49d427867aa
parent 27288 274b80691259
child 27290 784620cccb80
move lemmas into locales;
restructure some proofs
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Thu Jun 19 22:43:59 2008 +0200
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Jun 19 22:50:58 2008 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4  lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
     1.5  by (simp add: rep_eq)
     1.6  
     1.7 -lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
     1.8 +lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
     1.9  by (simp add: principal_less_iff_mem_rep rep_principal)
    1.10  
    1.11  lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
    1.12 @@ -250,7 +250,7 @@
    1.13  by (simp add: rep_eq)
    1.14  
    1.15  lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
    1.16 -by (simp add: principal_less_iff)
    1.17 +by (simp only: principal_less_iff)
    1.18  
    1.19  lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
    1.20  unfolding principal_less_iff_mem_rep
    1.21 @@ -316,7 +316,7 @@
    1.22   apply (erule imageI)
    1.23  done
    1.24  
    1.25 -lemma compact_principal: "compact (principal a)"
    1.26 +lemma compact_principal [simp]: "compact (principal a)"
    1.27  by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
    1.28  
    1.29  definition
    1.30 @@ -392,6 +392,16 @@
    1.31   apply (clarify, simp add: P)
    1.32  done
    1.33  
    1.34 +lemma principal_induct2:
    1.35 +  "\<lbrakk>\<And>y. adm (\<lambda>x. P x y); \<And>x. adm (\<lambda>y. P x y);
    1.36 +    \<And>a b. P (principal a) (principal b)\<rbrakk> \<Longrightarrow> P x y"
    1.37 +apply (rule_tac x=y in spec)
    1.38 +apply (rule_tac x=x in principal_induct, simp)
    1.39 +apply (rule allI, rename_tac y)
    1.40 +apply (rule_tac x=y in principal_induct, simp)
    1.41 +apply simp
    1.42 +done
    1.43 +
    1.44  lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
    1.45  apply (drule adm_compact_neq [OF _ cont_id])
    1.46  apply (drule admD2 [where Y="\<lambda>n. completion_approx n\<cdot>x"])
    1.47 @@ -412,17 +422,9 @@
    1.48  typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
    1.49  by (fast intro: compact_approx)
    1.50  
    1.51 -lemma compact_Rep_compact_basis [simp]: "compact (Rep_compact_basis a)"
    1.52 +lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
    1.53  by (rule Rep_compact_basis [unfolded mem_Collect_eq])
    1.54  
    1.55 -lemma Rep_Abs_compact_basis_approx [simp]:
    1.56 -  "Rep_compact_basis (Abs_compact_basis (approx n\<cdot>x)) = approx n\<cdot>x"
    1.57 -by (rule Abs_compact_basis_inverse, simp)
    1.58 -
    1.59 -lemma compact_imp_Rep_compact_basis:
    1.60 -  "compact x \<Longrightarrow> \<exists>y. x = Rep_compact_basis y"
    1.61 -by (rule exI, rule Abs_compact_basis_inverse [symmetric], simp)
    1.62 -
    1.63  instantiation compact_basis :: (profinite) sq_ord
    1.64  begin
    1.65  
    1.66 @@ -438,81 +440,7 @@
    1.67  by (rule typedef_po
    1.68      [OF type_definition_compact_basis compact_le_def])
    1.69  
    1.70 -text {* minimal compact element *}
    1.71 -
    1.72 -definition
    1.73 -  compact_bot :: "'a::bifinite compact_basis" where
    1.74 -  "compact_bot = Abs_compact_basis \<bottom>"
    1.75 -
    1.76 -lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
    1.77 -unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
    1.78 -
    1.79 -lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
    1.80 -unfolding compact_le_def Rep_compact_bot by simp
    1.81 -
    1.82 -text {* compacts *}
    1.83 -
    1.84 -definition
    1.85 -  compacts :: "'a \<Rightarrow> 'a compact_basis set" where
    1.86 -  "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
    1.87 -
    1.88 -lemma ideal_compacts: "sq_le.ideal (compacts w)"
    1.89 -unfolding compacts_def
    1.90 - apply (rule sq_le.idealI)
    1.91 -   apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    1.92 -   apply (simp add: approx_less)
    1.93 -  apply simp
    1.94 -  apply (cut_tac a=x in compact_Rep_compact_basis)
    1.95 -  apply (cut_tac a=y in compact_Rep_compact_basis)
    1.96 -  apply (drule bifinite_compact_eq_approx)
    1.97 -  apply (drule bifinite_compact_eq_approx)
    1.98 -  apply (clarify, rename_tac i j)
    1.99 -  apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
   1.100 -  apply (simp add: approx_less compact_le_def)
   1.101 -  apply (erule subst, erule subst)
   1.102 -  apply (simp add: monofun_cfun chain_mono [OF chain_approx])
   1.103 - apply (simp add: compact_le_def)
   1.104 - apply (erule (1) trans_less)
   1.105 -done
   1.106 -
   1.107 -lemma compacts_Rep_compact_basis:
   1.108 -  "compacts (Rep_compact_basis b) = {a. a \<sqsubseteq> b}"
   1.109 -unfolding compacts_def compact_le_def ..
   1.110 -
   1.111 -lemma cont_compacts: "cont compacts"
   1.112 -unfolding compacts_def
   1.113 -apply (rule contI2)
   1.114 -apply (rule monofunI)
   1.115 -apply (simp add: set_cpo_simps)
   1.116 -apply (fast intro: trans_less)
   1.117 -apply (simp add: set_cpo_simps)
   1.118 -apply clarify
   1.119 -apply simp
   1.120 -apply (erule (1) compactD2 [OF compact_Rep_compact_basis])
   1.121 -done
   1.122 -
   1.123 -lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
   1.124 -apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
   1.125 -apply (rule admD, simp, simp)
   1.126 -apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
   1.127 -apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
   1.128 -apply (simp add: compacts_def Abs_compact_basis_inverse)
   1.129 -done
   1.130 -
   1.131 -lemma compacts_mono: "x \<sqsubseteq> y \<Longrightarrow> compacts x \<subseteq> compacts y"
   1.132 -unfolding compacts_def by (fast intro: trans_less)
   1.133 -
   1.134 -lemma less_compact_basis_iff: "(x \<sqsubseteq> y) = (compacts x \<subseteq> compacts y)"
   1.135 -by (rule iffI [OF compacts_mono compacts_lessD])
   1.136 -
   1.137 -lemma compact_basis_induct:
   1.138 -  "\<lbrakk>adm P; \<And>a. P (Rep_compact_basis a)\<rbrakk> \<Longrightarrow> P x"
   1.139 -apply (erule approx_induct)
   1.140 -apply (drule_tac x="Abs_compact_basis (approx n\<cdot>x)" in meta_spec)
   1.141 -apply (simp add: Abs_compact_basis_inverse)
   1.142 -done
   1.143 -
   1.144 -text {* approximation on compact bases *}
   1.145 +text {* Take function for compact basis *}
   1.146  
   1.147  definition
   1.148    compact_approx :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
   1.149 @@ -525,84 +453,128 @@
   1.150  
   1.151  lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
   1.152  
   1.153 -lemma compact_approx_le: "compact_approx n a \<sqsubseteq> a"
   1.154 -unfolding compact_le_def
   1.155 -by (simp add: Rep_compact_approx approx_less)
   1.156 -
   1.157 -lemma compact_approx_mono1:
   1.158 -  "i \<le> j \<Longrightarrow> compact_approx i a \<sqsubseteq> compact_approx j a"
   1.159 -unfolding compact_le_def
   1.160 -apply (simp add: Rep_compact_approx)
   1.161 -apply (rule chain_mono, simp, assumption)
   1.162 -done
   1.163 -
   1.164 -lemma compact_approx_mono:
   1.165 -  "a \<sqsubseteq> b \<Longrightarrow> compact_approx n a \<sqsubseteq> compact_approx n b"
   1.166 -unfolding compact_le_def
   1.167 -apply (simp add: Rep_compact_approx)
   1.168 -apply (erule monofun_cfun_arg)
   1.169 -done
   1.170 +interpretation compact_basis:
   1.171 +  basis_take [sq_le compact_approx]
   1.172 +proof
   1.173 +  fix n :: nat and a :: "'a compact_basis"
   1.174 +  show "compact_approx n a \<sqsubseteq> a"
   1.175 +    unfolding compact_le_def
   1.176 +    by (simp add: Rep_compact_approx approx_less)
   1.177 +next
   1.178 +  fix n :: nat and a :: "'a compact_basis"
   1.179 +  show "compact_approx n (compact_approx n a) = compact_approx n a"
   1.180 +    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_approx)
   1.181 +next
   1.182 +  fix n :: nat and a b :: "'a compact_basis"
   1.183 +  assume "a \<sqsubseteq> b" thus "compact_approx n a \<sqsubseteq> compact_approx n b"
   1.184 +    unfolding compact_le_def Rep_compact_approx
   1.185 +    by (rule monofun_cfun_arg)
   1.186 +next
   1.187 +  fix n :: nat and a :: "'a compact_basis"
   1.188 +  show "\<And>n a. compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
   1.189 +    unfolding compact_le_def Rep_compact_approx
   1.190 +    by (rule chainE, simp)
   1.191 +next
   1.192 +  fix n :: nat
   1.193 +  show "finite (range (compact_approx n))"
   1.194 +    apply (rule finite_imageD [where f="Rep_compact_basis"])
   1.195 +    apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
   1.196 +    apply (clarsimp simp add: Rep_compact_approx)
   1.197 +    apply (rule finite_range_approx)
   1.198 +    apply (rule inj_onI, simp add: Rep_compact_basis_inject)
   1.199 +    done
   1.200 +next
   1.201 +  fix a :: "'a compact_basis"
   1.202 +  show "\<exists>n. compact_approx n a = a"
   1.203 +    apply (simp add: Rep_compact_basis_inject [symmetric])
   1.204 +    apply (simp add: Rep_compact_approx)
   1.205 +    apply (rule bifinite_compact_eq_approx)
   1.206 +    apply (rule compact_Rep_compact_basis)
   1.207 +    done
   1.208 +qed
   1.209  
   1.210 -lemma ex_compact_approx_eq: "\<exists>n. compact_approx n a = a"
   1.211 -apply (simp add: Rep_compact_basis_inject [symmetric])
   1.212 -apply (simp add: Rep_compact_approx)
   1.213 -apply (rule bifinite_compact_eq_approx)
   1.214 -apply (rule compact_Rep_compact_basis)
   1.215 -done
   1.216 -
   1.217 -lemma compact_approx_idem:
   1.218 -  "compact_approx n (compact_approx n a) = compact_approx n a"
   1.219 -apply (rule Rep_compact_basis_inject [THEN iffD1])
   1.220 -apply (simp add: Rep_compact_approx)
   1.221 -done
   1.222 +text {* Ideal completion *}
   1.223  
   1.224 -lemma finite_fixes_compact_approx: "finite {a. compact_approx n a = a}"
   1.225 -apply (subgoal_tac "finite (Rep_compact_basis ` {a. compact_approx n a = a})")
   1.226 -apply (erule finite_imageD)
   1.227 -apply (rule inj_onI, simp add: Rep_compact_basis_inject)
   1.228 -apply (rule finite_subset [OF _ finite_fixes_approx [where i=n]])
   1.229 -apply (rule subsetI, clarify, rename_tac a)
   1.230 -apply (simp add: Rep_compact_basis_inject [symmetric])
   1.231 -apply (simp add: Rep_compact_approx)
   1.232 -done
   1.233 -
   1.234 -lemma finite_range_compact_approx: "finite (range (compact_approx n))"
   1.235 -apply (cut_tac n=n in finite_fixes_compact_approx)
   1.236 -apply (simp add: idem_fixes_eq_range compact_approx_idem)
   1.237 -apply (simp add: image_def)
   1.238 -done
   1.239 +definition
   1.240 +  compacts :: "'a \<Rightarrow> 'a compact_basis set" where
   1.241 +  "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
   1.242  
   1.243  interpretation compact_basis:
   1.244    ideal_completion [sq_le compact_approx Rep_compact_basis compacts]
   1.245 -proof (unfold_locales)
   1.246 -  fix n :: nat and a b :: "'a compact_basis" and x :: "'a"
   1.247 -  show "compact_approx n a \<sqsubseteq> a"
   1.248 -    by (rule compact_approx_le)
   1.249 -  show "compact_approx n (compact_approx n a) = compact_approx n a"
   1.250 -    by (rule compact_approx_idem)
   1.251 -  show "compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
   1.252 -    by (rule compact_approx_mono1, simp)
   1.253 -  show "finite (range (compact_approx n))"
   1.254 -    by (rule finite_range_compact_approx)
   1.255 -  show "\<exists>n\<Colon>nat. compact_approx n a = a"
   1.256 -    by (rule ex_compact_approx_eq)
   1.257 -  show "preorder.ideal sq_le (compacts x)"
   1.258 -    by (rule ideal_compacts)
   1.259 +proof
   1.260 +  fix w :: 'a
   1.261 +  show "preorder.ideal sq_le (compacts w)"
   1.262 +  proof (rule sq_le.idealI)
   1.263 +    show "\<exists>x. x \<in> compacts w"
   1.264 +      unfolding compacts_def
   1.265 +      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
   1.266 +      apply (simp add: Abs_compact_basis_inverse approx_less)
   1.267 +      done
   1.268 +  next
   1.269 +    fix x y :: "'a compact_basis"
   1.270 +    assume "x \<in> compacts w" "y \<in> compacts w"
   1.271 +    thus "\<exists>z \<in> compacts w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   1.272 +      unfolding compacts_def
   1.273 +      apply simp
   1.274 +      apply (cut_tac a=x in compact_Rep_compact_basis)
   1.275 +      apply (cut_tac a=y in compact_Rep_compact_basis)
   1.276 +      apply (drule bifinite_compact_eq_approx)
   1.277 +      apply (drule bifinite_compact_eq_approx)
   1.278 +      apply (clarify, rename_tac i j)
   1.279 +      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
   1.280 +      apply (simp add: compact_le_def)
   1.281 +      apply (simp add: Abs_compact_basis_inverse approx_less)
   1.282 +      apply (erule subst, erule subst)
   1.283 +      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
   1.284 +      done
   1.285 +  next
   1.286 +    fix x y :: "'a compact_basis"
   1.287 +    assume "x \<sqsubseteq> y" "y \<in> compacts w" thus "x \<in> compacts w"
   1.288 +      unfolding compacts_def
   1.289 +      apply simp
   1.290 +      apply (simp add: compact_le_def)
   1.291 +      apply (erule (1) trans_less)
   1.292 +      done
   1.293 +  qed
   1.294 +next
   1.295    show "cont compacts"
   1.296 -    by (rule cont_compacts)
   1.297 -  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
   1.298 -    by (rule compacts_Rep_compact_basis)
   1.299 +    unfolding compacts_def
   1.300 +    apply (rule contI2)
   1.301 +    apply (rule monofunI)
   1.302 +    apply (simp add: set_cpo_simps)
   1.303 +    apply (fast intro: trans_less)
   1.304 +    apply (simp add: set_cpo_simps)
   1.305 +    apply clarify
   1.306 +    apply simp
   1.307 +    apply (erule (1) compactD2 [OF compact_Rep_compact_basis])
   1.308 +    done
   1.309  next
   1.310 -  fix n :: nat and a b :: "'a compact_basis"
   1.311 -  assume "a \<sqsubseteq> b"
   1.312 -  thus "compact_approx n a \<sqsubseteq> compact_approx n b"
   1.313 -    by (rule compact_approx_mono)
   1.314 +  fix a :: "'a compact_basis"
   1.315 +  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
   1.316 +    unfolding compacts_def compact_le_def ..
   1.317  next
   1.318    fix x y :: "'a"
   1.319    assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y"
   1.320 -    by (rule compacts_lessD)
   1.321 +    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
   1.322 +    apply (rule admD, simp, simp)
   1.323 +    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
   1.324 +    apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
   1.325 +    apply (simp add: compacts_def Abs_compact_basis_inverse)
   1.326 +    done
   1.327  qed
   1.328  
   1.329 +text {* minimal compact element *}
   1.330 +
   1.331 +definition
   1.332 +  compact_bot :: "'a::bifinite compact_basis" where
   1.333 +  "compact_bot = Abs_compact_basis \<bottom>"
   1.334 +
   1.335 +lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
   1.336 +unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
   1.337 +
   1.338 +lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
   1.339 +unfolding compact_le_def Rep_compact_bot by simp
   1.340 +
   1.341  
   1.342  subsection {* A compact basis for powerdomains *}
   1.343  
   1.344 @@ -705,37 +677,27 @@
   1.345  
   1.346  lemma approx_pd_idem: "approx_pd n (approx_pd n t) = approx_pd n t"
   1.347  apply (induct t rule: pd_basis_induct)
   1.348 -apply (simp add: compact_approx_idem)
   1.349 +apply (simp add: compact_basis.take_take)
   1.350  apply simp
   1.351  done
   1.352  
   1.353 -lemma range_image_f: "range (image f) = Pow (range f)"
   1.354 -apply (safe, fast)
   1.355 -apply (rule_tac x="f -` x" in range_eqI)
   1.356 -apply (simp, fast)
   1.357 -done
   1.358 -
   1.359  lemma finite_range_approx_pd: "finite (range (approx_pd n))"
   1.360 -apply (subgoal_tac "finite (Rep_pd_basis ` range (approx_pd n))")
   1.361 -apply (erule finite_imageD)
   1.362 +apply (rule finite_imageD [where f="Rep_pd_basis"])
   1.363 +apply (rule finite_subset [where B="Pow (range (compact_approx n))"])
   1.364 +apply (clarsimp simp add: Rep_approx_pd)
   1.365 +apply (simp add: compact_basis.finite_range_take)
   1.366  apply (rule inj_onI, simp add: Rep_pd_basis_inject)
   1.367 -apply (subst image_image)
   1.368 -apply (subst Rep_approx_pd)
   1.369 -apply (simp only: range_composition)
   1.370 -apply (rule finite_subset [OF image_mono [OF subset_UNIV]])
   1.371 -apply (simp add: range_image_f)
   1.372 -apply (rule finite_range_compact_approx)
   1.373  done
   1.374  
   1.375 -lemma ex_approx_pd_eq: "\<exists>n. approx_pd n t = t"
   1.376 +lemma approx_pd_covers: "\<exists>n. approx_pd n t = t"
   1.377  apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. approx_pd m t = t", fast)
   1.378  apply (induct t rule: pd_basis_induct)
   1.379 -apply (cut_tac a=a in ex_compact_approx_eq)
   1.380 +apply (cut_tac a=a in compact_basis.take_covers)
   1.381  apply (clarify, rule_tac x=n in exI)
   1.382  apply (clarify, simp)
   1.383  apply (rule antisym_less)
   1.384 -apply (rule compact_approx_le)
   1.385 -apply (drule_tac a=a in compact_approx_mono1)
   1.386 +apply (rule compact_basis.take_less)
   1.387 +apply (drule_tac a=a in compact_basis.take_chain_le)
   1.388  apply simp
   1.389  apply (clarify, rename_tac i j)
   1.390  apply (rule_tac x="max i j" in exI, simp)
     2.1 --- a/src/HOLCF/ConvexPD.thy	Thu Jun 19 22:43:59 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Jun 19 22:50:58 2008 +0200
     2.3 @@ -117,16 +117,16 @@
     2.4  apply (simp add: 4)
     2.5  done
     2.6  
     2.7 -lemma approx_pd_convex_mono1:
     2.8 -  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<natural> approx_pd j t"
     2.9 +lemma approx_pd_convex_chain:
    2.10 +  "approx_pd n t \<le>\<natural> approx_pd (Suc n) t"
    2.11  apply (induct t rule: pd_basis_induct)
    2.12 -apply (simp add: compact_approx_mono1)
    2.13 +apply (simp add: compact_basis.take_chain)
    2.14  apply (simp add: PDPlus_convex_mono)
    2.15  done
    2.16  
    2.17  lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
    2.18  apply (induct t rule: pd_basis_induct)
    2.19 -apply (simp add: compact_approx_le)
    2.20 +apply (simp add: compact_basis.take_less)
    2.21  apply (simp add: PDPlus_convex_mono)
    2.22  done
    2.23  
    2.24 @@ -134,7 +134,7 @@
    2.25    "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
    2.26  apply (erule convex_le_induct)
    2.27  apply (erule (1) convex_le_trans)
    2.28 -apply (simp add: compact_approx_mono)
    2.29 +apply (simp add: compact_basis.take_mono)
    2.30  apply (simp add: PDPlus_convex_mono)
    2.31  done
    2.32  
    2.33 @@ -170,29 +170,16 @@
    2.34  apply (rule approx_pd_convex_le)
    2.35  apply (rule approx_pd_idem)
    2.36  apply (erule approx_pd_convex_mono)
    2.37 -apply (rule approx_pd_convex_mono1, simp)
    2.38 +apply (rule approx_pd_convex_chain)
    2.39  apply (rule finite_range_approx_pd)
    2.40 -apply (rule ex_approx_pd_eq)
    2.41 +apply (rule approx_pd_covers)
    2.42  apply (rule ideal_Rep_convex_pd)
    2.43  apply (rule cont_Rep_convex_pd)
    2.44  apply (rule Rep_convex_principal)
    2.45  apply (simp only: less_convex_pd_def less_set_eq)
    2.46  done
    2.47  
    2.48 -lemma convex_principal_less_iff [simp]:
    2.49 -  "convex_principal t \<sqsubseteq> convex_principal u \<longleftrightarrow> t \<le>\<natural> u"
    2.50 -by (rule convex_pd.principal_less_iff)
    2.51 -
    2.52 -lemma convex_principal_eq_iff [simp]:
    2.53 -  "convex_principal t = convex_principal u \<longleftrightarrow> t \<le>\<natural> u \<and> u \<le>\<natural> t"
    2.54 -by (rule convex_pd.principal_eq_iff)
    2.55 -
    2.56 -lemma convex_principal_mono:
    2.57 -  "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
    2.58 -by (rule convex_pd.principal_mono)
    2.59 -
    2.60 -lemma compact_convex_principal: "compact (convex_principal t)"
    2.61 -by (rule convex_pd.compact_principal)
    2.62 +text {* Convex powerdomain is pointed *}
    2.63  
    2.64  lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    2.65  by (induct ys rule: convex_pd.principal_induct, simp, simp)
    2.66 @@ -203,8 +190,7 @@
    2.67  lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
    2.68  by (rule convex_pd_minimal [THEN UU_I, symmetric])
    2.69  
    2.70 -
    2.71 -subsection {* Approximation *}
    2.72 +text {* Convex powerdomain is profinite *}
    2.73  
    2.74  instantiation convex_pd :: (profinite) profinite
    2.75  begin
    2.76 @@ -234,24 +220,6 @@
    2.77  unfolding approx_convex_pd_def
    2.78  by (rule convex_pd.completion_approx_eq_principal)
    2.79  
    2.80 -lemma compact_imp_convex_principal:
    2.81 -  "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
    2.82 -by (rule convex_pd.compact_imp_principal)
    2.83 -
    2.84 -lemma convex_principal_induct:
    2.85 -  "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
    2.86 -by (rule convex_pd.principal_induct)
    2.87 -
    2.88 -lemma convex_principal_induct2:
    2.89 -  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
    2.90 -    \<And>t u. P (convex_principal t) (convex_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
    2.91 -apply (rule_tac x=ys in spec)
    2.92 -apply (rule_tac xs=xs in convex_principal_induct, simp)
    2.93 -apply (rule allI, rename_tac ys)
    2.94 -apply (rule_tac xs=ys in convex_principal_induct, simp)
    2.95 -apply simp
    2.96 -done
    2.97 -
    2.98  
    2.99  subsection {* Monadic unit and plus *}
   2.100  
   2.101 @@ -279,8 +247,7 @@
   2.102  lemma convex_unit_Rep_compact_basis [simp]:
   2.103    "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
   2.104  unfolding convex_unit_def
   2.105 -by (simp add: compact_basis.basis_fun_principal
   2.106 -    convex_principal_mono PDUnit_convex_mono)
   2.107 +by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
   2.108  
   2.109  lemma convex_plus_principal [simp]:
   2.110    "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
   2.111 @@ -290,28 +257,28 @@
   2.112  
   2.113  lemma approx_convex_unit [simp]:
   2.114    "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
   2.115 -apply (induct x rule: compact_basis_induct, simp)
   2.116 +apply (induct x rule: compact_basis.principal_induct, simp)
   2.117  apply (simp add: approx_Rep_compact_basis)
   2.118  done
   2.119  
   2.120  lemma approx_convex_plus [simp]:
   2.121    "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
   2.122 -by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.123 +by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   2.124  
   2.125  lemma convex_plus_assoc:
   2.126    "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
   2.127 -apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
   2.128 -apply (rule_tac xs=zs in convex_principal_induct, simp)
   2.129 +apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
   2.130 +apply (rule_tac x=zs in convex_pd.principal_induct, simp)
   2.131  apply (simp add: PDPlus_assoc)
   2.132  done
   2.133  
   2.134  lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
   2.135 -apply (induct xs ys rule: convex_principal_induct2, simp, simp)
   2.136 +apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
   2.137  apply (simp add: PDPlus_commute)
   2.138  done
   2.139  
   2.140  lemma convex_plus_absorb: "xs +\<natural> xs = xs"
   2.141 -apply (induct xs rule: convex_principal_induct, simp)
   2.142 +apply (induct xs rule: convex_pd.principal_induct, simp)
   2.143  apply (simp add: PDPlus_absorb)
   2.144  done
   2.145  
   2.146 @@ -334,9 +301,9 @@
   2.147      "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
   2.148     apply (drule admD, rule chain_approx)
   2.149      apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.150 -    apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.151 -    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.152 -    apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_convex_principal, simp)
   2.153 +    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   2.154 +    apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   2.155 +    apply (cut_tac x="approx i\<cdot>zs" in convex_pd.compact_imp_principal, simp)
   2.156      apply (clarify, simp)
   2.157     apply simp
   2.158    apply simp
   2.159 @@ -352,9 +319,9 @@
   2.160      "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
   2.161     apply (drule admD, rule chain_approx)
   2.162      apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.163 -    apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
   2.164 -    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.165 -    apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
   2.166 +    apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   2.167 +    apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   2.168 +    apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
   2.169      apply (clarify, simp)
   2.170     apply simp
   2.171    apply simp
   2.172 @@ -367,9 +334,9 @@
   2.173   apply (rule iffI)
   2.174    apply (rule bifinite_less_ext)
   2.175    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   2.176 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.177 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   2.178 -  apply (clarify, simp add: compact_le_def)
   2.179 +  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   2.180 +  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   2.181 +  apply clarsimp
   2.182   apply (erule monofun_cfun_arg)
   2.183  done
   2.184  
   2.185 @@ -388,9 +355,7 @@
   2.186  
   2.187  lemma compact_convex_plus [simp]:
   2.188    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
   2.189 -apply (drule compact_imp_convex_principal)+
   2.190 -apply (auto simp add: compact_convex_principal)
   2.191 -done
   2.192 +by (auto dest!: convex_pd.compact_imp_principal)
   2.193  
   2.194  
   2.195  subsection {* Induction rules *}
   2.196 @@ -400,8 +365,8 @@
   2.197    assumes unit: "\<And>x. P {x}\<natural>"
   2.198    assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
   2.199    shows "P (xs::'a convex_pd)"
   2.200 -apply (induct xs rule: convex_principal_induct, rule P)
   2.201 -apply (induct_tac t rule: pd_basis_induct1)
   2.202 +apply (induct xs rule: convex_pd.principal_induct, rule P)
   2.203 +apply (induct_tac a rule: pd_basis_induct1)
   2.204  apply (simp only: convex_unit_Rep_compact_basis [symmetric])
   2.205  apply (rule unit)
   2.206  apply (simp only: convex_unit_Rep_compact_basis [symmetric]
   2.207 @@ -414,8 +379,8 @@
   2.208    assumes unit: "\<And>x. P {x}\<natural>"
   2.209    assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
   2.210    shows "P (xs::'a convex_pd)"
   2.211 -apply (induct xs rule: convex_principal_induct, rule P)
   2.212 -apply (induct_tac t rule: pd_basis_induct)
   2.213 +apply (induct xs rule: convex_pd.principal_induct, rule P)
   2.214 +apply (induct_tac a rule: pd_basis_induct)
   2.215  apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
   2.216  apply (simp only: convex_plus_principal [symmetric] plus)
   2.217  done
   2.218 @@ -457,8 +422,8 @@
   2.219    "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
   2.220  apply (erule convex_le_induct)
   2.221  apply (erule (1) trans_less)
   2.222 -apply (simp add: monofun_LAM compact_le_def monofun_cfun)
   2.223 -apply (simp add: monofun_LAM compact_le_def monofun_cfun)
   2.224 +apply (simp add: monofun_LAM monofun_cfun)
   2.225 +apply (simp add: monofun_LAM monofun_cfun)
   2.226  done
   2.227  
   2.228  definition
   2.229 @@ -474,11 +439,11 @@
   2.230  
   2.231  lemma convex_bind_unit [simp]:
   2.232    "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
   2.233 -by (induct x rule: compact_basis_induct, simp, simp)
   2.234 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   2.235  
   2.236  lemma convex_bind_plus [simp]:
   2.237    "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
   2.238 -by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.239 +by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   2.240  
   2.241  lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   2.242  unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
   2.243 @@ -549,22 +514,36 @@
   2.244    "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
   2.245  unfolding convex_to_upper_def
   2.246  apply (rule convex_pd.basis_fun_principal)
   2.247 -apply (rule upper_principal_mono)
   2.248 +apply (rule upper_pd.principal_mono)
   2.249  apply (erule convex_le_imp_upper_le)
   2.250  done
   2.251  
   2.252  lemma convex_to_upper_unit [simp]:
   2.253    "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
   2.254 -by (induct x rule: compact_basis_induct, simp, simp)
   2.255 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   2.256  
   2.257  lemma convex_to_upper_plus [simp]:
   2.258    "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
   2.259 -by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.260 +by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   2.261  
   2.262  lemma approx_convex_to_upper:
   2.263    "approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)"
   2.264  by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.265  
   2.266 +lemma convex_to_upper_bind [simp]:
   2.267 +  "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   2.268 +    upper_bind\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper oo f)"
   2.269 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.270 +
   2.271 +lemma convex_to_upper_map [simp]:
   2.272 +  "convex_to_upper\<cdot>(convex_map\<cdot>f\<cdot>xs) = upper_map\<cdot>f\<cdot>(convex_to_upper\<cdot>xs)"
   2.273 +by (simp add: convex_map_def upper_map_def cfcomp_LAM)
   2.274 +
   2.275 +lemma convex_to_upper_join [simp]:
   2.276 +  "convex_to_upper\<cdot>(convex_join\<cdot>xss) =
   2.277 +    upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper"
   2.278 +by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun)
   2.279 +
   2.280  text {* Convex to lower *}
   2.281  
   2.282  lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
   2.283 @@ -578,22 +557,36 @@
   2.284    "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
   2.285  unfolding convex_to_lower_def
   2.286  apply (rule convex_pd.basis_fun_principal)
   2.287 -apply (rule lower_principal_mono)
   2.288 +apply (rule lower_pd.principal_mono)
   2.289  apply (erule convex_le_imp_lower_le)
   2.290  done
   2.291  
   2.292  lemma convex_to_lower_unit [simp]:
   2.293    "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
   2.294 -by (induct x rule: compact_basis_induct, simp, simp)
   2.295 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   2.296  
   2.297  lemma convex_to_lower_plus [simp]:
   2.298    "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
   2.299 -by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.300 +by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   2.301  
   2.302  lemma approx_convex_to_lower:
   2.303    "approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)"
   2.304  by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.305  
   2.306 +lemma convex_to_lower_bind [simp]:
   2.307 +  "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
   2.308 +    lower_bind\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower oo f)"
   2.309 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.310 +
   2.311 +lemma convex_to_lower_map [simp]:
   2.312 +  "convex_to_lower\<cdot>(convex_map\<cdot>f\<cdot>xs) = lower_map\<cdot>f\<cdot>(convex_to_lower\<cdot>xs)"
   2.313 +by (simp add: convex_map_def lower_map_def cfcomp_LAM)
   2.314 +
   2.315 +lemma convex_to_lower_join [simp]:
   2.316 +  "convex_to_lower\<cdot>(convex_join\<cdot>xss) =
   2.317 +    lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower"
   2.318 +by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun)
   2.319 +
   2.320  text {* Ordering property *}
   2.321  
   2.322  lemma convex_pd_less_iff:
   2.323 @@ -604,8 +597,8 @@
   2.324   apply (rule bifinite_less_ext)
   2.325   apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.326   apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.327 - apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
   2.328 - apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.329 + apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   2.330 + apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
   2.331   apply clarify
   2.332   apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   2.333  done
     3.1 --- a/src/HOLCF/LowerPD.thy	Thu Jun 19 22:43:59 2008 +0200
     3.2 +++ b/src/HOLCF/LowerPD.thy	Thu Jun 19 22:50:58 2008 +0200
     3.3 @@ -72,23 +72,23 @@
     3.4  apply (simp add: lower_le_PDPlus_iff 3)
     3.5  done
     3.6  
     3.7 -lemma approx_pd_lower_mono1:
     3.8 -  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<flat> approx_pd j t"
     3.9 +lemma approx_pd_lower_chain:
    3.10 +  "approx_pd n t \<le>\<flat> approx_pd (Suc n) t"
    3.11  apply (induct t rule: pd_basis_induct)
    3.12 -apply (simp add: compact_approx_mono1)
    3.13 +apply (simp add: compact_basis.take_chain)
    3.14  apply (simp add: PDPlus_lower_mono)
    3.15  done
    3.16  
    3.17  lemma approx_pd_lower_le: "approx_pd i t \<le>\<flat> t"
    3.18  apply (induct t rule: pd_basis_induct)
    3.19 -apply (simp add: compact_approx_le)
    3.20 +apply (simp add: compact_basis.take_less)
    3.21  apply (simp add: PDPlus_lower_mono)
    3.22  done
    3.23  
    3.24  lemma approx_pd_lower_mono:
    3.25    "t \<le>\<flat> u \<Longrightarrow> approx_pd n t \<le>\<flat> approx_pd n u"
    3.26  apply (erule lower_le_induct)
    3.27 -apply (simp add: compact_approx_mono)
    3.28 +apply (simp add: compact_basis.take_mono)
    3.29  apply (simp add: lower_le_PDUnit_PDPlus_iff)
    3.30  apply (simp add: lower_le_PDPlus_iff)
    3.31  done
    3.32 @@ -122,29 +122,16 @@
    3.33  apply (rule approx_pd_lower_le)
    3.34  apply (rule approx_pd_idem)
    3.35  apply (erule approx_pd_lower_mono)
    3.36 -apply (rule approx_pd_lower_mono1, simp)
    3.37 +apply (rule approx_pd_lower_chain)
    3.38  apply (rule finite_range_approx_pd)
    3.39 -apply (rule ex_approx_pd_eq)
    3.40 +apply (rule approx_pd_covers)
    3.41  apply (rule ideal_Rep_lower_pd)
    3.42  apply (rule cont_Rep_lower_pd)
    3.43  apply (rule Rep_lower_principal)
    3.44  apply (simp only: less_lower_pd_def less_set_eq)
    3.45  done
    3.46  
    3.47 -lemma lower_principal_less_iff [simp]:
    3.48 -  "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
    3.49 -by (rule lower_pd.principal_less_iff)
    3.50 -
    3.51 -lemma lower_principal_eq_iff:
    3.52 -  "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
    3.53 -by (rule lower_pd.principal_eq_iff)
    3.54 -
    3.55 -lemma lower_principal_mono:
    3.56 -  "t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
    3.57 -by (rule lower_pd.principal_mono)
    3.58 -
    3.59 -lemma compact_lower_principal: "compact (lower_principal t)"
    3.60 -by (rule lower_pd.compact_principal)
    3.61 +text {* Lower powerdomain is pointed *}
    3.62  
    3.63  lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    3.64  by (induct ys rule: lower_pd.principal_induct, simp, simp)
    3.65 @@ -155,8 +142,7 @@
    3.66  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    3.67  by (rule lower_pd_minimal [THEN UU_I, symmetric])
    3.68  
    3.69 -
    3.70 -subsection {* Approximation *}
    3.71 +text {* Lower powerdomain is profinite *}
    3.72  
    3.73  instantiation lower_pd :: (profinite) profinite
    3.74  begin
    3.75 @@ -186,24 +172,6 @@
    3.76  unfolding approx_lower_pd_def
    3.77  by (rule lower_pd.completion_approx_eq_principal)
    3.78  
    3.79 -lemma compact_imp_lower_principal:
    3.80 -  "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
    3.81 -by (rule lower_pd.compact_imp_principal)
    3.82 -
    3.83 -lemma lower_principal_induct:
    3.84 -  "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
    3.85 -by (rule lower_pd.principal_induct)
    3.86 -
    3.87 -lemma lower_principal_induct2:
    3.88 -  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
    3.89 -    \<And>t u. P (lower_principal t) (lower_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
    3.90 -apply (rule_tac x=ys in spec)
    3.91 -apply (rule_tac xs=xs in lower_principal_induct, simp)
    3.92 -apply (rule allI, rename_tac ys)
    3.93 -apply (rule_tac xs=ys in lower_principal_induct, simp)
    3.94 -apply simp
    3.95 -done
    3.96 -
    3.97  
    3.98  subsection {* Monadic unit and plus *}
    3.99  
   3.100 @@ -231,8 +199,7 @@
   3.101  lemma lower_unit_Rep_compact_basis [simp]:
   3.102    "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
   3.103  unfolding lower_unit_def
   3.104 -by (simp add: compact_basis.basis_fun_principal
   3.105 -    lower_principal_mono PDUnit_lower_mono)
   3.106 +by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono)
   3.107  
   3.108  lemma lower_plus_principal [simp]:
   3.109    "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
   3.110 @@ -242,27 +209,27 @@
   3.111  
   3.112  lemma approx_lower_unit [simp]:
   3.113    "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
   3.114 -apply (induct x rule: compact_basis_induct, simp)
   3.115 +apply (induct x rule: compact_basis.principal_induct, simp)
   3.116  apply (simp add: approx_Rep_compact_basis)
   3.117  done
   3.118  
   3.119  lemma approx_lower_plus [simp]:
   3.120    "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
   3.121 -by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   3.122 +by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
   3.123  
   3.124  lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
   3.125 -apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
   3.126 -apply (rule_tac xs=zs in lower_principal_induct, simp)
   3.127 +apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
   3.128 +apply (rule_tac x=zs in lower_pd.principal_induct, simp)
   3.129  apply (simp add: PDPlus_assoc)
   3.130  done
   3.131  
   3.132  lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
   3.133 -apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   3.134 +apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
   3.135  apply (simp add: PDPlus_commute)
   3.136  done
   3.137  
   3.138  lemma lower_plus_absorb: "xs +\<flat> xs = xs"
   3.139 -apply (induct xs rule: lower_principal_induct, simp)
   3.140 +apply (induct xs rule: lower_pd.principal_induct, simp)
   3.141  apply (simp add: PDPlus_absorb)
   3.142  done
   3.143  
   3.144 @@ -279,7 +246,7 @@
   3.145  lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
   3.146  
   3.147  lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
   3.148 -apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   3.149 +apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
   3.150  apply (simp add: PDPlus_lower_less)
   3.151  done
   3.152  
   3.153 @@ -306,9 +273,9 @@
   3.154      "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
   3.155     apply (drule admD, rule chain_approx)
   3.156      apply (drule_tac f="approx i" in monofun_cfun_arg)
   3.157 -    apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   3.158 -    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
   3.159 -    apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_lower_principal, simp)
   3.160 +    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   3.161 +    apply (cut_tac x="approx i\<cdot>ys" in lower_pd.compact_imp_principal, simp)
   3.162 +    apply (cut_tac x="approx i\<cdot>zs" in lower_pd.compact_imp_principal, simp)
   3.163      apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff)
   3.164     apply simp
   3.165    apply simp
   3.166 @@ -321,9 +288,9 @@
   3.167   apply (rule iffI)
   3.168    apply (rule bifinite_less_ext)
   3.169    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   3.170 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   3.171 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   3.172 -  apply (clarify, simp add: compact_le_def)
   3.173 +  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   3.174 +  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   3.175 +  apply clarsimp
   3.176   apply (erule monofun_cfun_arg)
   3.177  done
   3.178  
   3.179 @@ -332,8 +299,14 @@
   3.180    lower_plus_less_iff
   3.181    lower_unit_less_plus_iff
   3.182  
   3.183 +lemma fooble:
   3.184 +  fixes f :: "'a::po \<Rightarrow> 'b::po"
   3.185 +  assumes f: "\<And>x y. f x \<sqsubseteq> f y \<longleftrightarrow> x \<sqsubseteq> y"
   3.186 +  shows "f x = f y \<longleftrightarrow> x = y"
   3.187 +unfolding po_eq_conv by (simp add: f)
   3.188 +
   3.189  lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
   3.190 -unfolding po_eq_conv by simp
   3.191 +by (rule lower_unit_less_iff [THEN fooble])
   3.192  
   3.193  lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
   3.194  unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
   3.195 @@ -364,9 +337,7 @@
   3.196  
   3.197  lemma compact_lower_plus [simp]:
   3.198    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
   3.199 -apply (drule compact_imp_lower_principal)+
   3.200 -apply (auto simp add: compact_lower_principal)
   3.201 -done
   3.202 +by (auto dest!: lower_pd.compact_imp_principal)
   3.203  
   3.204  
   3.205  subsection {* Induction rules *}
   3.206 @@ -377,8 +348,8 @@
   3.207    assumes insert:
   3.208      "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
   3.209    shows "P (xs::'a lower_pd)"
   3.210 -apply (induct xs rule: lower_principal_induct, rule P)
   3.211 -apply (induct_tac t rule: pd_basis_induct1)
   3.212 +apply (induct xs rule: lower_pd.principal_induct, rule P)
   3.213 +apply (induct_tac a rule: pd_basis_induct1)
   3.214  apply (simp only: lower_unit_Rep_compact_basis [symmetric])
   3.215  apply (rule unit)
   3.216  apply (simp only: lower_unit_Rep_compact_basis [symmetric]
   3.217 @@ -391,8 +362,8 @@
   3.218    assumes unit: "\<And>x. P {x}\<flat>"
   3.219    assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
   3.220    shows "P (xs::'a lower_pd)"
   3.221 -apply (induct xs rule: lower_principal_induct, rule P)
   3.222 -apply (induct_tac t rule: pd_basis_induct)
   3.223 +apply (induct xs rule: lower_pd.principal_induct, rule P)
   3.224 +apply (induct_tac a rule: pd_basis_induct)
   3.225  apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
   3.226  apply (simp only: lower_plus_principal [symmetric] plus)
   3.227  done
   3.228 @@ -430,7 +401,7 @@
   3.229    "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
   3.230  unfolding expand_cfun_less
   3.231  apply (erule lower_le_induct, safe)
   3.232 -apply (simp add: compact_le_def monofun_cfun)
   3.233 +apply (simp add: monofun_cfun)
   3.234  apply (simp add: rev_trans_less [OF lower_plus_less1])
   3.235  apply (simp add: lower_plus_less_iff)
   3.236  done
   3.237 @@ -448,11 +419,11 @@
   3.238  
   3.239  lemma lower_bind_unit [simp]:
   3.240    "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
   3.241 -by (induct x rule: compact_basis_induct, simp, simp)
   3.242 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   3.243  
   3.244  lemma lower_bind_plus [simp]:
   3.245    "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
   3.246 -by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   3.247 +by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
   3.248  
   3.249  lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   3.250  unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
     4.1 --- a/src/HOLCF/UpperPD.thy	Thu Jun 19 22:43:59 2008 +0200
     4.2 +++ b/src/HOLCF/UpperPD.thy	Thu Jun 19 22:50:58 2008 +0200
     4.3 @@ -70,23 +70,23 @@
     4.4  apply (simp add: upper_le_PDPlus_iff 3)
     4.5  done
     4.6  
     4.7 -lemma approx_pd_upper_mono1:
     4.8 -  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<sharp> approx_pd j t"
     4.9 +lemma approx_pd_upper_chain:
    4.10 +  "approx_pd n t \<le>\<sharp> approx_pd (Suc n) t"
    4.11  apply (induct t rule: pd_basis_induct)
    4.12 -apply (simp add: compact_approx_mono1)
    4.13 +apply (simp add: compact_basis.take_chain)
    4.14  apply (simp add: PDPlus_upper_mono)
    4.15  done
    4.16  
    4.17  lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
    4.18  apply (induct t rule: pd_basis_induct)
    4.19 -apply (simp add: compact_approx_le)
    4.20 +apply (simp add: compact_basis.take_less)
    4.21  apply (simp add: PDPlus_upper_mono)
    4.22  done
    4.23  
    4.24  lemma approx_pd_upper_mono:
    4.25    "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
    4.26  apply (erule upper_le_induct)
    4.27 -apply (simp add: compact_approx_mono)
    4.28 +apply (simp add: compact_basis.take_mono)
    4.29  apply (simp add: upper_le_PDPlus_PDUnit_iff)
    4.30  apply (simp add: upper_le_PDPlus_iff)
    4.31  done
    4.32 @@ -120,29 +120,16 @@
    4.33  apply (rule approx_pd_upper_le)
    4.34  apply (rule approx_pd_idem)
    4.35  apply (erule approx_pd_upper_mono)
    4.36 -apply (rule approx_pd_upper_mono1, simp)
    4.37 +apply (rule approx_pd_upper_chain)
    4.38  apply (rule finite_range_approx_pd)
    4.39 -apply (rule ex_approx_pd_eq)
    4.40 +apply (rule approx_pd_covers)
    4.41  apply (rule ideal_Rep_upper_pd)
    4.42  apply (rule cont_Rep_upper_pd)
    4.43  apply (rule Rep_upper_principal)
    4.44  apply (simp only: less_upper_pd_def less_set_eq)
    4.45  done
    4.46  
    4.47 -lemma upper_principal_less_iff [simp]:
    4.48 -  "upper_principal t \<sqsubseteq> upper_principal u \<longleftrightarrow> t \<le>\<sharp> u"
    4.49 -by (rule upper_pd.principal_less_iff)
    4.50 -
    4.51 -lemma upper_principal_eq_iff:
    4.52 -  "upper_principal t = upper_principal u \<longleftrightarrow> t \<le>\<sharp> u \<and> u \<le>\<sharp> t"
    4.53 -by (rule upper_pd.principal_eq_iff)
    4.54 -
    4.55 -lemma upper_principal_mono:
    4.56 -  "t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
    4.57 -by (rule upper_pd.principal_mono)
    4.58 -
    4.59 -lemma compact_upper_principal: "compact (upper_principal t)"
    4.60 -by (rule upper_pd.compact_principal)
    4.61 +text {* Upper powerdomain is pointed *}
    4.62  
    4.63  lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    4.64  by (induct ys rule: upper_pd.principal_induct, simp, simp)
    4.65 @@ -153,8 +140,7 @@
    4.66  lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
    4.67  by (rule upper_pd_minimal [THEN UU_I, symmetric])
    4.68  
    4.69 -
    4.70 -subsection {* Approximation *}
    4.71 +text {* Upper powerdomain is profinite *}
    4.72  
    4.73  instantiation upper_pd :: (profinite) profinite
    4.74  begin
    4.75 @@ -184,24 +170,6 @@
    4.76  unfolding approx_upper_pd_def
    4.77  by (rule upper_pd.completion_approx_eq_principal)
    4.78  
    4.79 -lemma compact_imp_upper_principal:
    4.80 -  "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
    4.81 -by (rule upper_pd.compact_imp_principal)
    4.82 -
    4.83 -lemma upper_principal_induct:
    4.84 -  "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
    4.85 -by (rule upper_pd.principal_induct)
    4.86 -
    4.87 -lemma upper_principal_induct2:
    4.88 -  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
    4.89 -    \<And>t u. P (upper_principal t) (upper_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
    4.90 -apply (rule_tac x=ys in spec)
    4.91 -apply (rule_tac xs=xs in upper_principal_induct, simp)
    4.92 -apply (rule allI, rename_tac ys)
    4.93 -apply (rule_tac xs=ys in upper_principal_induct, simp)
    4.94 -apply simp
    4.95 -done
    4.96 -
    4.97  
    4.98  subsection {* Monadic unit and plus *}
    4.99  
   4.100 @@ -229,8 +197,7 @@
   4.101  lemma upper_unit_Rep_compact_basis [simp]:
   4.102    "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
   4.103  unfolding upper_unit_def
   4.104 -by (simp add: compact_basis.basis_fun_principal
   4.105 -    upper_principal_mono PDUnit_upper_mono)
   4.106 +by (simp add: compact_basis.basis_fun_principal PDUnit_upper_mono)
   4.107  
   4.108  lemma upper_plus_principal [simp]:
   4.109    "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
   4.110 @@ -240,27 +207,27 @@
   4.111  
   4.112  lemma approx_upper_unit [simp]:
   4.113    "approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>"
   4.114 -apply (induct x rule: compact_basis_induct, simp)
   4.115 +apply (induct x rule: compact_basis.principal_induct, simp)
   4.116  apply (simp add: approx_Rep_compact_basis)
   4.117  done
   4.118  
   4.119  lemma approx_upper_plus [simp]:
   4.120    "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
   4.121 -by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   4.122 +by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
   4.123  
   4.124  lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
   4.125 -apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
   4.126 -apply (rule_tac xs=zs in upper_principal_induct, simp)
   4.127 +apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
   4.128 +apply (rule_tac x=zs in upper_pd.principal_induct, simp)
   4.129  apply (simp add: PDPlus_assoc)
   4.130  done
   4.131  
   4.132  lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
   4.133 -apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   4.134 +apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
   4.135  apply (simp add: PDPlus_commute)
   4.136  done
   4.137  
   4.138  lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
   4.139 -apply (induct xs rule: upper_principal_induct, simp)
   4.140 +apply (induct xs rule: upper_pd.principal_induct, simp)
   4.141  apply (simp add: PDPlus_absorb)
   4.142  done
   4.143  
   4.144 @@ -277,7 +244,7 @@
   4.145  lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
   4.146  
   4.147  lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
   4.148 -apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   4.149 +apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
   4.150  apply (simp add: PDPlus_upper_less)
   4.151  done
   4.152  
   4.153 @@ -304,9 +271,9 @@
   4.154      "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
   4.155     apply (drule admD, rule chain_approx)
   4.156      apply (drule_tac f="approx i" in monofun_cfun_arg)
   4.157 -    apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
   4.158 -    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)
   4.159 -    apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
   4.160 +    apply (cut_tac x="approx i\<cdot>xs" in upper_pd.compact_imp_principal, simp)
   4.161 +    apply (cut_tac x="approx i\<cdot>ys" in upper_pd.compact_imp_principal, simp)
   4.162 +    apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
   4.163      apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff)
   4.164     apply simp
   4.165    apply simp
   4.166 @@ -319,9 +286,9 @@
   4.167   apply (rule iffI)
   4.168    apply (rule bifinite_less_ext)
   4.169    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   4.170 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   4.171 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   4.172 -  apply (clarify, simp add: compact_le_def)
   4.173 +  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   4.174 +  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   4.175 +  apply clarsimp
   4.176   apply (erule monofun_cfun_arg)
   4.177  done
   4.178  
   4.179 @@ -349,8 +316,8 @@
   4.180    "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   4.181  apply (rule iffI)
   4.182  apply (erule rev_mp)
   4.183 -apply (rule upper_principal_induct2 [where xs=xs and ys=ys], simp, simp)
   4.184 -apply (simp add: inst_upper_pd_pcpo upper_principal_eq_iff
   4.185 +apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
   4.186 +apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff
   4.187                   upper_le_PDPlus_PDUnit_iff)
   4.188  apply auto
   4.189  done
   4.190 @@ -360,9 +327,7 @@
   4.191  
   4.192  lemma compact_upper_plus [simp]:
   4.193    "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
   4.194 -apply (drule compact_imp_upper_principal)+
   4.195 -apply (auto simp add: compact_upper_principal)
   4.196 -done
   4.197 +by (auto dest!: upper_pd.compact_imp_principal)
   4.198  
   4.199  
   4.200  subsection {* Induction rules *}
   4.201 @@ -372,8 +337,8 @@
   4.202    assumes unit: "\<And>x. P {x}\<sharp>"
   4.203    assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
   4.204    shows "P (xs::'a upper_pd)"
   4.205 -apply (induct xs rule: upper_principal_induct, rule P)
   4.206 -apply (induct_tac t rule: pd_basis_induct1)
   4.207 +apply (induct xs rule: upper_pd.principal_induct, rule P)
   4.208 +apply (induct_tac a rule: pd_basis_induct1)
   4.209  apply (simp only: upper_unit_Rep_compact_basis [symmetric])
   4.210  apply (rule unit)
   4.211  apply (simp only: upper_unit_Rep_compact_basis [symmetric]
   4.212 @@ -386,8 +351,8 @@
   4.213    assumes unit: "\<And>x. P {x}\<sharp>"
   4.214    assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
   4.215    shows "P (xs::'a upper_pd)"
   4.216 -apply (induct xs rule: upper_principal_induct, rule P)
   4.217 -apply (induct_tac t rule: pd_basis_induct)
   4.218 +apply (induct xs rule: upper_pd.principal_induct, rule P)
   4.219 +apply (induct_tac a rule: pd_basis_induct)
   4.220  apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
   4.221  apply (simp only: upper_plus_principal [symmetric] plus)
   4.222  done
   4.223 @@ -425,7 +390,7 @@
   4.224    "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
   4.225  unfolding expand_cfun_less
   4.226  apply (erule upper_le_induct, safe)
   4.227 -apply (simp add: compact_le_def monofun_cfun)
   4.228 +apply (simp add: monofun_cfun)
   4.229  apply (simp add: trans_less [OF upper_plus_less1])
   4.230  apply (simp add: upper_less_plus_iff)
   4.231  done
   4.232 @@ -443,11 +408,11 @@
   4.233  
   4.234  lemma upper_bind_unit [simp]:
   4.235    "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x"
   4.236 -by (induct x rule: compact_basis_induct, simp, simp)
   4.237 +by (induct x rule: compact_basis.principal_induct, simp, simp)
   4.238  
   4.239  lemma upper_bind_plus [simp]:
   4.240    "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
   4.241 -by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   4.242 +by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
   4.243  
   4.244  lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   4.245  unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)