make preorder locale into a superclass of class po
authorhuffman
Thu Mar 27 00:27:16 2008 +0100 (2008-03-27)
changeset 2642057a626f64875
parent 26419 945d8d7a66ec
child 26421 3dfb36923a56
make preorder locale into a superclass of class po
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Porder.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Wed Mar 26 22:41:58 2008 +0100
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Mar 27 00:27:16 2008 +0100
     1.3 @@ -11,21 +11,18 @@
     1.4  
     1.5  subsection {* Ideals over a preorder *}
     1.6  
     1.7 -locale preorder =
     1.8 -  fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 -  assumes refl: "r x x"
    1.10 -  assumes trans: "\<lbrakk>r x y; r y z\<rbrakk> \<Longrightarrow> r x z"
    1.11 +context preorder
    1.12  begin
    1.13  
    1.14  definition
    1.15    ideal :: "'a set \<Rightarrow> bool" where
    1.16 -  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. r x z \<and> r y z) \<and>
    1.17 -    (\<forall>x y. r x y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
    1.18 +  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z) \<and>
    1.19 +    (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
    1.20  
    1.21  lemma idealI:
    1.22    assumes "\<exists>x. x \<in> A"
    1.23 -  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
    1.24 -  assumes "\<And>x y. \<lbrakk>r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.25 +  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.26 +  assumes "\<And>x y. \<lbrakk>x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.27    shows "ideal A"
    1.28  unfolding ideal_def using prems by fast
    1.29  
    1.30 @@ -34,36 +31,36 @@
    1.31  unfolding ideal_def by fast
    1.32  
    1.33  lemma idealD2:
    1.34 -  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
    1.35 +  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.36  unfolding ideal_def by fast
    1.37  
    1.38  lemma idealD3:
    1.39 -  "\<lbrakk>ideal A; r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.40 +  "\<lbrakk>ideal A; x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.41  unfolding ideal_def by fast
    1.42  
    1.43  lemma ideal_directed_finite:
    1.44    assumes A: "ideal A"
    1.45 -  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. r x z"
    1.46 +  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<sqsubseteq> z"
    1.47  apply (induct U set: finite)
    1.48  apply (simp add: idealD1 [OF A])
    1.49  apply (simp, clarify, rename_tac y)
    1.50  apply (drule (1) idealD2 [OF A])
    1.51  apply (clarify, erule_tac x=z in rev_bexI)
    1.52 -apply (fast intro: trans)
    1.53 +apply (fast intro: trans_less)
    1.54  done
    1.55  
    1.56 -lemma ideal_principal: "ideal {x. r x z}"
    1.57 +lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
    1.58  apply (rule idealI)
    1.59  apply (rule_tac x=z in exI)
    1.60  apply (fast intro: refl)
    1.61  apply (rule_tac x=z in bexI, fast)
    1.62 -apply (fast intro: refl)
    1.63 -apply (fast intro: trans)
    1.64 +apply fast
    1.65 +apply (fast intro: trans_less)
    1.66  done
    1.67  
    1.68  lemma directed_image_ideal:
    1.69    assumes A: "ideal A"
    1.70 -  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.71 +  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.72    shows "directed (f ` A)"
    1.73  apply (rule directedI)
    1.74  apply (cut_tac idealD1 [OF A], fast)
    1.75 @@ -78,21 +75,21 @@
    1.76  lemma adm_ideal: "adm (\<lambda>A. ideal A)"
    1.77  unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
    1.78  
    1.79 -end
    1.80 -
    1.81 -subsection {* Defining functions in terms of basis elements *}
    1.82 -
    1.83 -lemma (in preorder) lub_image_principal:
    1.84 -  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.85 -  shows "(\<Squnion>x\<in>{x. r x y}. f x) = f y"
    1.86 +lemma lub_image_principal:
    1.87 +  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.88 +  shows "(\<Squnion>x\<in>{x. x \<sqsubseteq> y}. f x) = f y"
    1.89  apply (rule thelubI)
    1.90  apply (rule is_lub_maximal)
    1.91  apply (rule ub_imageI)
    1.92  apply (simp add: f)
    1.93  apply (rule imageI)
    1.94 -apply (simp add: refl)
    1.95 +apply simp
    1.96  done
    1.97  
    1.98 +end
    1.99 +
   1.100 +subsection {* Defining functions in terms of basis elements *}
   1.101 +
   1.102  lemma finite_directed_contains_lub:
   1.103    "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
   1.104  apply (drule (1) directed_finiteD, rule subset_refl)
   1.105 @@ -119,14 +116,7 @@
   1.106  lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
   1.107  by (erule exE, drule lubI, erule is_lub_lub)
   1.108  
   1.109 -locale bifinite_basis = preorder +
   1.110 -  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   1.111 -  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
   1.112 -  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
   1.113 -  assumes cont_approxes: "cont approxes"
   1.114 -  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
   1.115 -  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
   1.116 -
   1.117 +locale plotkin_order = preorder r +
   1.118    fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
   1.119    assumes take_less: "r (take n a) a"
   1.120    assumes take_take: "take n (take n a) = take n a"
   1.121 @@ -134,6 +124,14 @@
   1.122    assumes take_chain: "r (take n a) (take (Suc n) a)"
   1.123    assumes finite_range_take: "finite (range (take n))"
   1.124    assumes take_covers: "\<exists>n. take n a = a"
   1.125 +
   1.126 +locale bifinite_basis = plotkin_order r +
   1.127 +  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   1.128 +  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
   1.129 +  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
   1.130 +  assumes cont_approxes: "cont approxes"
   1.131 +  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
   1.132 +  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
   1.133  begin
   1.134  
   1.135  lemma finite_take_approxes: "finite (take n ` approxes x)"
   1.136 @@ -161,7 +159,7 @@
   1.137   apply (rule is_lub_thelub0)
   1.138    apply (rule basis_fun_lemma0, erule f_mono)
   1.139   apply (rule is_ubI, clarsimp, rename_tac a)
   1.140 - apply (rule trans_less [OF f_mono [OF take_chain]])
   1.141 + apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
   1.142   apply (rule is_ub_thelub0)
   1.143    apply (rule basis_fun_lemma0, erule f_mono)
   1.144   apply simp
   1.145 @@ -186,7 +184,7 @@
   1.146   apply (rule is_lub_thelub0)
   1.147    apply (rule basis_fun_lemma0, erule f_mono)
   1.148   apply (rule is_ubI, clarsimp, rename_tac a)
   1.149 - apply (rule trans_less [OF f_mono [OF take_less]])
   1.150 + apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
   1.151   apply (erule (1) ub_imageD)
   1.152  done
   1.153  
   1.154 @@ -285,7 +283,7 @@
   1.155   apply (rule is_lub_thelub0)
   1.156    apply (rule basis_fun_lemma, erule f_mono)
   1.157   apply (rule ub_imageI, rename_tac a)
   1.158 - apply (rule trans_less [OF less])
   1.159 + apply (rule sq_le.trans_less [OF less])
   1.160   apply (rule is_ub_thelub0)
   1.161    apply (rule basis_fun_lemma, erule g_mono)
   1.162   apply (erule imageI)
   1.163 @@ -371,6 +369,21 @@
   1.164    "compact x \<Longrightarrow> \<exists>y. x = Rep_compact_basis y"
   1.165  by (rule exI, rule Abs_compact_basis_inverse [symmetric], simp)
   1.166  
   1.167 +instantiation compact_basis :: (profinite) sq_ord
   1.168 +begin
   1.169 +
   1.170 +definition
   1.171 +  compact_le_def:
   1.172 +    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
   1.173 +
   1.174 +instance ..
   1.175 +
   1.176 +end
   1.177 +
   1.178 +instance compact_basis :: (profinite) po
   1.179 +by (rule typedef_po
   1.180 +    [OF type_definition_compact_basis compact_le_def])
   1.181 +(*
   1.182  definition
   1.183    compact_le :: "'a compact_basis \<Rightarrow> 'a compact_basis \<Rightarrow> bool" where
   1.184    "compact_le = (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
   1.185 @@ -389,7 +402,7 @@
   1.186  
   1.187  interpretation compact_le: preorder [compact_le]
   1.188  by (rule preorder.intro, rule compact_le_refl, rule compact_le_trans)
   1.189 -
   1.190 +*)
   1.191  text {* minimal compact element *}
   1.192  
   1.193  definition
   1.194 @@ -399,7 +412,7 @@
   1.195  lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
   1.196  unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
   1.197  
   1.198 -lemma compact_minimal [simp]: "compact_le compact_bot a"
   1.199 +lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
   1.200  unfolding compact_le_def Rep_compact_bot by simp
   1.201  
   1.202  text {* compacts *}
   1.203 @@ -408,9 +421,10 @@
   1.204    compacts :: "'a \<Rightarrow> 'a compact_basis set" where
   1.205    "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
   1.206  
   1.207 -lemma ideal_compacts: "compact_le.ideal (compacts w)"
   1.208 +lemma ideal_compacts: "preorder.ideal sq_le (compacts w)"
   1.209  unfolding compacts_def
   1.210 - apply (rule compact_le.idealI)
   1.211 + apply (rule preorder.idealI)
   1.212 +    apply (rule preorder_class.axioms)
   1.213     apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
   1.214     apply (simp add: approx_less)
   1.215    apply simp
   1.216 @@ -428,7 +442,7 @@
   1.217  done
   1.218  
   1.219  lemma compacts_Rep_compact_basis:
   1.220 -  "compacts (Rep_compact_basis b) = {a. compact_le a b}"
   1.221 +  "compacts (Rep_compact_basis b) = {a. a \<sqsubseteq> b}"
   1.222  unfolding compacts_def compact_le_def ..
   1.223  
   1.224  lemma cont_compacts: "cont compacts"
   1.225 @@ -477,20 +491,19 @@
   1.226  
   1.227  lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
   1.228  
   1.229 -lemma compact_approx_le:
   1.230 -  "compact_le (compact_approx n a) a"
   1.231 +lemma compact_approx_le: "compact_approx n a \<sqsubseteq> a"
   1.232  unfolding compact_le_def
   1.233  by (simp add: Rep_compact_approx approx_less)
   1.234  
   1.235  lemma compact_approx_mono1:
   1.236 -  "i \<le> j \<Longrightarrow> compact_le (compact_approx i a) (compact_approx j a)"
   1.237 +  "i \<le> j \<Longrightarrow> compact_approx i a \<sqsubseteq> compact_approx j a"
   1.238  unfolding compact_le_def
   1.239  apply (simp add: Rep_compact_approx)
   1.240  apply (rule chain_mono, simp, assumption)
   1.241  done
   1.242  
   1.243  lemma compact_approx_mono:
   1.244 -  "compact_le a b \<Longrightarrow> compact_le (compact_approx n a) (compact_approx n b)"
   1.245 +  "a \<sqsubseteq> b \<Longrightarrow> compact_approx n a \<sqsubseteq> compact_approx n b"
   1.246  unfolding compact_le_def
   1.247  apply (simp add: Rep_compact_approx)
   1.248  apply (erule monofun_cfun_arg)
   1.249 @@ -526,19 +539,35 @@
   1.250  done
   1.251  
   1.252  interpretation compact_basis:
   1.253 -  bifinite_basis [compact_le Rep_compact_basis compacts compact_approx]
   1.254 -apply unfold_locales
   1.255 -apply (rule ideal_compacts)
   1.256 -apply (rule cont_compacts)
   1.257 -apply (rule compacts_Rep_compact_basis)
   1.258 -apply (erule compacts_lessD)
   1.259 -apply (rule compact_approx_le)
   1.260 -apply (rule compact_approx_idem)
   1.261 -apply (erule compact_approx_mono)
   1.262 -apply (rule compact_approx_mono1, simp)
   1.263 -apply (rule finite_range_compact_approx)
   1.264 -apply (rule ex_compact_approx_eq)
   1.265 -done
   1.266 +  bifinite_basis [sq_le compact_approx Rep_compact_basis compacts]
   1.267 +proof (unfold_locales)
   1.268 +  fix n :: nat and a b :: "'a compact_basis" and x :: "'a"
   1.269 +  show "compact_approx n a \<sqsubseteq> a"
   1.270 +    by (rule compact_approx_le)
   1.271 +  show "compact_approx n (compact_approx n a) = compact_approx n a"
   1.272 +    by (rule compact_approx_idem)
   1.273 +  show "compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
   1.274 +    by (rule compact_approx_mono1, simp)
   1.275 +  show "finite (range (compact_approx n))"
   1.276 +    by (rule finite_range_compact_approx)
   1.277 +  show "\<exists>n\<Colon>nat. compact_approx n a = a"
   1.278 +    by (rule ex_compact_approx_eq)
   1.279 +  show "preorder.ideal sq_le (compacts x)"
   1.280 +    by (rule ideal_compacts)
   1.281 +  show "cont compacts"
   1.282 +    by (rule cont_compacts)
   1.283 +  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
   1.284 +    by (rule compacts_Rep_compact_basis)
   1.285 +next
   1.286 +  fix n :: nat and a b :: "'a compact_basis"
   1.287 +  assume "a \<sqsubseteq> b"
   1.288 +  thus "compact_approx n a \<sqsubseteq> compact_approx n b"
   1.289 +    by (rule compact_approx_mono)
   1.290 +next
   1.291 +  fix x y :: "'a"
   1.292 +  assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y"
   1.293 +    by (rule compacts_lessD)
   1.294 +qed
   1.295  
   1.296  
   1.297  subsection {* A compact basis for powerdomains *}
   1.298 @@ -668,7 +697,7 @@
   1.299  apply (cut_tac a=a in ex_compact_approx_eq)
   1.300  apply (clarify, rule_tac x=n in exI)
   1.301  apply (clarify, simp)
   1.302 -apply (rule compact_le_antisym)
   1.303 +apply (rule antisym_less)
   1.304  apply (rule compact_approx_le)
   1.305  apply (drule_tac a=a in compact_approx_mono1)
   1.306  apply simp
     2.1 --- a/src/HOLCF/ConvexPD.thy	Wed Mar 26 22:41:58 2008 +0100
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Mar 27 00:27:16 2008 +0100
     2.3 @@ -27,18 +27,18 @@
     2.4  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
     2.5  unfolding convex_le_def Rep_PDUnit by simp
     2.6  
     2.7 -lemma PDUnit_convex_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
     2.8 +lemma PDUnit_convex_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
     2.9  unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono)
    2.10  
    2.11  lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v"
    2.12  unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
    2.13  
    2.14  lemma convex_le_PDUnit_PDUnit_iff [simp]:
    2.15 -  "(PDUnit a \<le>\<natural> PDUnit b) = compact_le a b"
    2.16 +  "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
    2.17  unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
    2.18  
    2.19  lemma convex_le_PDUnit_lemma1:
    2.20 -  "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. compact_le a b)"
    2.21 +  "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
    2.22  unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    2.23  using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    2.24  
    2.25 @@ -47,7 +47,7 @@
    2.26  unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast
    2.27  
    2.28  lemma convex_le_PDUnit_lemma2:
    2.29 -  "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. compact_le a b)"
    2.30 +  "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
    2.31  unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    2.32  using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    2.33  
    2.34 @@ -59,8 +59,8 @@
    2.35    assumes z: "PDPlus t u \<le>\<natural> z"
    2.36    shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w"
    2.37  proof (intro exI conjI)
    2.38 -  let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. compact_le a b}"
    2.39 -  let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. compact_le a b}"
    2.40 +  let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. a \<sqsubseteq> b}"
    2.41 +  let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. a \<sqsubseteq> b}"
    2.42    let ?v = "Abs_pd_basis ?A"
    2.43    let ?w = "Abs_pd_basis ?B"
    2.44    have Rep_v: "Rep_pd_basis ?v = ?A"
    2.45 @@ -102,7 +102,7 @@
    2.46  lemma convex_le_induct [induct set: convex_le]:
    2.47    assumes le: "t \<le>\<natural> u"
    2.48    assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v"
    2.49 -  assumes 3: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    2.50 +  assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    2.51    assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
    2.52    shows "P t u"
    2.53  using le apply (induct t arbitrary: u rule: pd_basis_induct)
    2.54 @@ -168,18 +168,18 @@
    2.55  done
    2.56  
    2.57  interpretation convex_pd:
    2.58 -  bifinite_basis [convex_le convex_principal Rep_convex_pd approx_pd]
    2.59 +  bifinite_basis [convex_le approx_pd convex_principal Rep_convex_pd]
    2.60  apply unfold_locales
    2.61 -apply (rule ideal_Rep_convex_pd)
    2.62 -apply (rule cont_Rep_convex_pd)
    2.63 -apply (rule Rep_convex_principal)
    2.64 -apply (simp only: less_convex_pd_def less_set_def)
    2.65  apply (rule approx_pd_convex_le)
    2.66  apply (rule approx_pd_idem)
    2.67  apply (erule approx_pd_convex_mono)
    2.68  apply (rule approx_pd_convex_mono1, simp)
    2.69  apply (rule finite_range_approx_pd)
    2.70  apply (rule ex_approx_pd_eq)
    2.71 +apply (rule ideal_Rep_convex_pd)
    2.72 +apply (rule cont_Rep_convex_pd)
    2.73 +apply (rule Rep_convex_principal)
    2.74 +apply (simp only: less_convex_pd_def less_set_def)
    2.75  done
    2.76  
    2.77  lemma convex_principal_less_iff [simp]:
     3.1 --- a/src/HOLCF/LowerPD.thy	Wed Mar 26 22:41:58 2008 +0100
     3.2 +++ b/src/HOLCF/LowerPD.thy	Thu Mar 27 00:27:16 2008 +0100
     3.3 @@ -13,10 +13,10 @@
     3.4  
     3.5  definition
     3.6    lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where
     3.7 -  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. compact_le x y)"
     3.8 +  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)"
     3.9  
    3.10  lemma lower_le_refl [simp]: "t \<le>\<flat> t"
    3.11 -unfolding lower_le_def by (fast intro: compact_le_refl)
    3.12 +unfolding lower_le_def by fast
    3.13  
    3.14  lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v"
    3.15  unfolding lower_le_def
    3.16 @@ -24,7 +24,7 @@
    3.17  apply (drule (1) bspec, erule bexE)
    3.18  apply (drule (1) bspec, erule bexE)
    3.19  apply (erule rev_bexI)
    3.20 -apply (erule (1) compact_le_trans)
    3.21 +apply (erule (1) trans_less)
    3.22  done
    3.23  
    3.24  interpretation lower_le: preorder [lower_le]
    3.25 @@ -34,17 +34,17 @@
    3.26  unfolding lower_le_def Rep_PDUnit
    3.27  by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])
    3.28  
    3.29 -lemma PDUnit_lower_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
    3.30 +lemma PDUnit_lower_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
    3.31  unfolding lower_le_def Rep_PDUnit by fast
    3.32  
    3.33  lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
    3.34  unfolding lower_le_def Rep_PDPlus by fast
    3.35  
    3.36  lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
    3.37 -unfolding lower_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    3.38 +unfolding lower_le_def Rep_PDPlus by fast
    3.39  
    3.40  lemma lower_le_PDUnit_PDUnit_iff [simp]:
    3.41 -  "(PDUnit a \<le>\<flat> PDUnit b) = compact_le a b"
    3.42 +  "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b"
    3.43  unfolding lower_le_def Rep_PDUnit by fast
    3.44  
    3.45  lemma lower_le_PDUnit_PDPlus_iff:
    3.46 @@ -56,7 +56,7 @@
    3.47  
    3.48  lemma lower_le_induct [induct set: lower_le]:
    3.49    assumes le: "t \<le>\<flat> u"
    3.50 -  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    3.51 +  assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    3.52    assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
    3.53    assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
    3.54    shows "P t u"
    3.55 @@ -123,18 +123,18 @@
    3.56  done
    3.57  
    3.58  interpretation lower_pd:
    3.59 -  bifinite_basis [lower_le lower_principal Rep_lower_pd approx_pd]
    3.60 +  bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
    3.61  apply unfold_locales
    3.62 -apply (rule ideal_Rep_lower_pd)
    3.63 -apply (rule cont_Rep_lower_pd)
    3.64 -apply (rule Rep_lower_principal)
    3.65 -apply (simp only: less_lower_pd_def less_set_def)
    3.66  apply (rule approx_pd_lower_le)
    3.67  apply (rule approx_pd_idem)
    3.68  apply (erule approx_pd_lower_mono)
    3.69  apply (rule approx_pd_lower_mono1, simp)
    3.70  apply (rule finite_range_approx_pd)
    3.71  apply (rule ex_approx_pd_eq)
    3.72 +apply (rule ideal_Rep_lower_pd)
    3.73 +apply (rule cont_Rep_lower_pd)
    3.74 +apply (rule Rep_lower_principal)
    3.75 +apply (simp only: less_lower_pd_def less_set_def)
    3.76  done
    3.77  
    3.78  lemma lower_principal_less_iff [simp]:
     4.1 --- a/src/HOLCF/Pcpodef.thy	Wed Mar 26 22:41:58 2008 +0100
     4.2 +++ b/src/HOLCF/Pcpodef.thy	Thu Mar 27 00:27:16 2008 +0100
     4.3 @@ -24,9 +24,9 @@
     4.4    shows "OFCLASS('b, po_class)"
     4.5   apply (intro_classes, unfold less)
     4.6     apply (rule refl_less)
     4.7 -  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
     4.8 -  apply (erule (1) antisym_less)
     4.9 - apply (erule (1) trans_less)
    4.10 +  apply (erule (1) trans_less)
    4.11 + apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
    4.12 + apply (erule (1) antisym_less)
    4.13  done
    4.14  
    4.15  subsection {* Proving a subtype is finite *}
     5.1 --- a/src/HOLCF/Porder.thy	Wed Mar 26 22:41:58 2008 +0100
     5.2 +++ b/src/HOLCF/Porder.thy	Thu Mar 27 00:27:16 2008 +0100
     5.3 @@ -20,10 +20,12 @@
     5.4  notation (xsymbols)
     5.5    sq_le (infixl "\<sqsubseteq>" 55)
     5.6  
     5.7 -class po = sq_ord +
     5.8 +class preorder = sq_ord +
     5.9    assumes refl_less [iff]: "x \<sqsubseteq> x"
    5.10 +  assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    5.11 +
    5.12 +class po = preorder +
    5.13    assumes antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
    5.14 -  assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    5.15  
    5.16  text {* minimal fixes least element *}
    5.17  
     6.1 --- a/src/HOLCF/UpperPD.thy	Wed Mar 26 22:41:58 2008 +0100
     6.2 +++ b/src/HOLCF/UpperPD.thy	Thu Mar 27 00:27:16 2008 +0100
     6.3 @@ -13,10 +13,10 @@
     6.4  
     6.5  definition
     6.6    upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
     6.7 -  "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. compact_le x y)"
     6.8 +  "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)"
     6.9  
    6.10  lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
    6.11 -unfolding upper_le_def by (fast intro: compact_le_refl)
    6.12 +unfolding upper_le_def by fast
    6.13  
    6.14  lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v"
    6.15  unfolding upper_le_def
    6.16 @@ -24,7 +24,7 @@
    6.17  apply (drule (1) bspec, erule bexE)
    6.18  apply (drule (1) bspec, erule bexE)
    6.19  apply (erule rev_bexI)
    6.20 -apply (erule (1) compact_le_trans)
    6.21 +apply (erule (1) trans_less)
    6.22  done
    6.23  
    6.24  interpretation upper_le: preorder [upper_le]
    6.25 @@ -33,17 +33,17 @@
    6.26  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
    6.27  unfolding upper_le_def Rep_PDUnit by simp
    6.28  
    6.29 -lemma PDUnit_upper_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
    6.30 +lemma PDUnit_upper_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
    6.31  unfolding upper_le_def Rep_PDUnit by simp
    6.32  
    6.33  lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
    6.34  unfolding upper_le_def Rep_PDPlus by fast
    6.35  
    6.36  lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
    6.37 -unfolding upper_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    6.38 +unfolding upper_le_def Rep_PDPlus by fast
    6.39  
    6.40  lemma upper_le_PDUnit_PDUnit_iff [simp]:
    6.41 -  "(PDUnit a \<le>\<sharp> PDUnit b) = compact_le a b"
    6.42 +  "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b"
    6.43  unfolding upper_le_def Rep_PDUnit by fast
    6.44  
    6.45  lemma upper_le_PDPlus_PDUnit_iff:
    6.46 @@ -55,7 +55,7 @@
    6.47  
    6.48  lemma upper_le_induct [induct set: upper_le]:
    6.49    assumes le: "t \<le>\<sharp> u"
    6.50 -  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    6.51 +  assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    6.52    assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
    6.53    assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
    6.54    shows "P t u"
    6.55 @@ -115,18 +115,18 @@
    6.56  done
    6.57  
    6.58  interpretation upper_pd:
    6.59 -  bifinite_basis [upper_le upper_principal Rep_upper_pd approx_pd]
    6.60 +  bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd]
    6.61  apply unfold_locales
    6.62 -apply (rule ideal_Rep_upper_pd)
    6.63 -apply (rule cont_Rep_upper_pd)
    6.64 -apply (rule Rep_upper_principal)
    6.65 -apply (simp only: less_upper_pd_def less_set_def)
    6.66  apply (rule approx_pd_upper_le)
    6.67  apply (rule approx_pd_idem)
    6.68  apply (erule approx_pd_upper_mono)
    6.69  apply (rule approx_pd_upper_mono1, simp)
    6.70  apply (rule finite_range_approx_pd)
    6.71  apply (rule ex_approx_pd_eq)
    6.72 +apply (rule ideal_Rep_upper_pd)
    6.73 +apply (rule cont_Rep_upper_pd)
    6.74 +apply (rule Rep_upper_principal)
    6.75 +apply (simp only: less_upper_pd_def less_set_def)
    6.76  done
    6.77  
    6.78  lemma upper_principal_less_iff [simp]: