# HG changeset patch
# User huffman
# Date 1206574036 -3600
# Node ID 57a626f64875513fcce7794c0b519b94d3cea301
# Parent  945d8d7a66ec82c14b8aa1e69130a254a5cf2b26
make preorder locale into a superclass of class po

diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -11,21 +11,18 @@
 
 subsection {* Ideals over a preorder *}
 
-locale preorder =
-  fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool"
-  assumes refl: "r x x"
-  assumes trans: "\<lbrakk>r x y; r y z\<rbrakk> \<Longrightarrow> r x z"
+context preorder
 begin
 
 definition
   ideal :: "'a set \<Rightarrow> bool" where
-  "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>
-    (\<forall>x y. r x y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
+  "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>
+    (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
 
 lemma idealI:
   assumes "\<exists>x. x \<in> A"
-  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
-  assumes "\<And>x y. \<lbrakk>r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
+  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+  assumes "\<And>x y. \<lbrakk>x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
   shows "ideal A"
 unfolding ideal_def using prems by fast
 
@@ -34,36 +31,36 @@
 unfolding ideal_def by fast
 
 lemma idealD2:
-  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
+  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
 unfolding ideal_def by fast
 
 lemma idealD3:
-  "\<lbrakk>ideal A; r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
+  "\<lbrakk>ideal A; x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
 unfolding ideal_def by fast
 
 lemma ideal_directed_finite:
   assumes A: "ideal A"
-  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. r x z"
+  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<sqsubseteq> z"
 apply (induct U set: finite)
 apply (simp add: idealD1 [OF A])
 apply (simp, clarify, rename_tac y)
 apply (drule (1) idealD2 [OF A])
 apply (clarify, erule_tac x=z in rev_bexI)
-apply (fast intro: trans)
+apply (fast intro: trans_less)
 done
 
-lemma ideal_principal: "ideal {x. r x z}"
+lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
 apply (rule idealI)
 apply (rule_tac x=z in exI)
 apply (fast intro: refl)
 apply (rule_tac x=z in bexI, fast)
-apply (fast intro: refl)
-apply (fast intro: trans)
+apply fast
+apply (fast intro: trans_less)
 done
 
 lemma directed_image_ideal:
   assumes A: "ideal A"
-  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
+  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "directed (f ` A)"
 apply (rule directedI)
 apply (cut_tac idealD1 [OF A], fast)
@@ -78,21 +75,21 @@
 lemma adm_ideal: "adm (\<lambda>A. ideal A)"
 unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
 
-end
-
-subsection {* Defining functions in terms of basis elements *}
-
-lemma (in preorder) lub_image_principal:
-  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
-  shows "(\<Squnion>x\<in>{x. r x y}. f x) = f y"
+lemma lub_image_principal:
+  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  shows "(\<Squnion>x\<in>{x. x \<sqsubseteq> y}. f x) = f y"
 apply (rule thelubI)
 apply (rule is_lub_maximal)
 apply (rule ub_imageI)
 apply (simp add: f)
 apply (rule imageI)
-apply (simp add: refl)
+apply simp
 done
 
+end
+
+subsection {* Defining functions in terms of basis elements *}
+
 lemma finite_directed_contains_lub:
   "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
 apply (drule (1) directed_finiteD, rule subset_refl)
@@ -119,14 +116,7 @@
 lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
 by (erule exE, drule lubI, erule is_lub_lub)
 
-locale bifinite_basis = preorder +
-  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
-  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
-  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
-  assumes cont_approxes: "cont approxes"
-  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
-  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
-
+locale plotkin_order = preorder r +
   fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
   assumes take_less: "r (take n a) a"
   assumes take_take: "take n (take n a) = take n a"
@@ -134,6 +124,14 @@
   assumes take_chain: "r (take n a) (take (Suc n) a)"
   assumes finite_range_take: "finite (range (take n))"
   assumes take_covers: "\<exists>n. take n a = a"
+
+locale bifinite_basis = plotkin_order r +
+  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
+  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
+  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
+  assumes cont_approxes: "cont approxes"
+  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
+  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
 begin
 
 lemma finite_take_approxes: "finite (take n ` approxes x)"
@@ -161,7 +159,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_chain]])
+ apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply simp
@@ -186,7 +184,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_less]])
+ apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
  apply (erule (1) ub_imageD)
 done
 
@@ -285,7 +283,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma, erule f_mono)
  apply (rule ub_imageI, rename_tac a)
- apply (rule trans_less [OF less])
+ apply (rule sq_le.trans_less [OF less])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma, erule g_mono)
  apply (erule imageI)
@@ -371,6 +369,21 @@
   "compact x \<Longrightarrow> \<exists>y. x = Rep_compact_basis y"
 by (rule exI, rule Abs_compact_basis_inverse [symmetric], simp)
 
+instantiation compact_basis :: (profinite) sq_ord
+begin
+
+definition
+  compact_le_def:
+    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
+
+instance ..
+
+end
+
+instance compact_basis :: (profinite) po
+by (rule typedef_po
+    [OF type_definition_compact_basis compact_le_def])
+(*
 definition
   compact_le :: "'a compact_basis \<Rightarrow> 'a compact_basis \<Rightarrow> bool" where
   "compact_le = (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
@@ -389,7 +402,7 @@
 
 interpretation compact_le: preorder [compact_le]
 by (rule preorder.intro, rule compact_le_refl, rule compact_le_trans)
-
+*)
 text {* minimal compact element *}
 
 definition
@@ -399,7 +412,7 @@
 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
 
-lemma compact_minimal [simp]: "compact_le compact_bot a"
+lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
 unfolding compact_le_def Rep_compact_bot by simp
 
 text {* compacts *}
@@ -408,9 +421,10 @@
   compacts :: "'a \<Rightarrow> 'a compact_basis set" where
   "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
-lemma ideal_compacts: "compact_le.ideal (compacts w)"
+lemma ideal_compacts: "preorder.ideal sq_le (compacts w)"
 unfolding compacts_def
- apply (rule compact_le.idealI)
+ apply (rule preorder.idealI)
+    apply (rule preorder_class.axioms)
    apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    apply (simp add: approx_less)
   apply simp
@@ -428,7 +442,7 @@
 done
 
 lemma compacts_Rep_compact_basis:
-  "compacts (Rep_compact_basis b) = {a. compact_le a b}"
+  "compacts (Rep_compact_basis b) = {a. a \<sqsubseteq> b}"
 unfolding compacts_def compact_le_def ..
 
 lemma cont_compacts: "cont compacts"
@@ -477,20 +491,19 @@
 
 lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
 
-lemma compact_approx_le:
-  "compact_le (compact_approx n a) a"
+lemma compact_approx_le: "compact_approx n a \<sqsubseteq> a"
 unfolding compact_le_def
 by (simp add: Rep_compact_approx approx_less)
 
 lemma compact_approx_mono1:
-  "i \<le> j \<Longrightarrow> compact_le (compact_approx i a) (compact_approx j a)"
+  "i \<le> j \<Longrightarrow> compact_approx i a \<sqsubseteq> compact_approx j a"
 unfolding compact_le_def
 apply (simp add: Rep_compact_approx)
 apply (rule chain_mono, simp, assumption)
 done
 
 lemma compact_approx_mono:
-  "compact_le a b \<Longrightarrow> compact_le (compact_approx n a) (compact_approx n b)"
+  "a \<sqsubseteq> b \<Longrightarrow> compact_approx n a \<sqsubseteq> compact_approx n b"
 unfolding compact_le_def
 apply (simp add: Rep_compact_approx)
 apply (erule monofun_cfun_arg)
@@ -526,19 +539,35 @@
 done
 
 interpretation compact_basis:
-  bifinite_basis [compact_le Rep_compact_basis compacts compact_approx]
-apply unfold_locales
-apply (rule ideal_compacts)
-apply (rule cont_compacts)
-apply (rule compacts_Rep_compact_basis)
-apply (erule compacts_lessD)
-apply (rule compact_approx_le)
-apply (rule compact_approx_idem)
-apply (erule compact_approx_mono)
-apply (rule compact_approx_mono1, simp)
-apply (rule finite_range_compact_approx)
-apply (rule ex_compact_approx_eq)
-done
+  bifinite_basis [sq_le compact_approx Rep_compact_basis compacts]
+proof (unfold_locales)
+  fix n :: nat and a b :: "'a compact_basis" and x :: "'a"
+  show "compact_approx n a \<sqsubseteq> a"
+    by (rule compact_approx_le)
+  show "compact_approx n (compact_approx n a) = compact_approx n a"
+    by (rule compact_approx_idem)
+  show "compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
+    by (rule compact_approx_mono1, simp)
+  show "finite (range (compact_approx n))"
+    by (rule finite_range_compact_approx)
+  show "\<exists>n\<Colon>nat. compact_approx n a = a"
+    by (rule ex_compact_approx_eq)
+  show "preorder.ideal sq_le (compacts x)"
+    by (rule ideal_compacts)
+  show "cont compacts"
+    by (rule cont_compacts)
+  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
+    by (rule compacts_Rep_compact_basis)
+next
+  fix n :: nat and a b :: "'a compact_basis"
+  assume "a \<sqsubseteq> b"
+  thus "compact_approx n a \<sqsubseteq> compact_approx n b"
+    by (rule compact_approx_mono)
+next
+  fix x y :: "'a"
+  assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y"
+    by (rule compacts_lessD)
+qed
 
 
 subsection {* A compact basis for powerdomains *}
@@ -668,7 +697,7 @@
 apply (cut_tac a=a in ex_compact_approx_eq)
 apply (clarify, rule_tac x=n in exI)
 apply (clarify, simp)
-apply (rule compact_le_antisym)
+apply (rule antisym_less)
 apply (rule compact_approx_le)
 apply (drule_tac a=a in compact_approx_mono1)
 apply simp
diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -27,18 +27,18 @@
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
 unfolding convex_le_def Rep_PDUnit by simp
 
-lemma PDUnit_convex_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
+lemma PDUnit_convex_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
 unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono)
 
 lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v"
 unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
 
 lemma convex_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<natural> PDUnit b) = compact_le a b"
+  "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
 
 lemma convex_le_PDUnit_lemma1:
-  "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. compact_le a b)"
+  "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
 using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
 
@@ -47,7 +47,7 @@
 unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast
 
 lemma convex_le_PDUnit_lemma2:
-  "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. compact_le a b)"
+  "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. a \<sqsubseteq> b)"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
 using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
 
@@ -59,8 +59,8 @@
   assumes z: "PDPlus t u \<le>\<natural> z"
   shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w"
 proof (intro exI conjI)
-  let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. compact_le a b}"
-  let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. compact_le a b}"
+  let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. a \<sqsubseteq> b}"
+  let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. a \<sqsubseteq> b}"
   let ?v = "Abs_pd_basis ?A"
   let ?w = "Abs_pd_basis ?B"
   have Rep_v: "Rep_pd_basis ?v = ?A"
@@ -102,7 +102,7 @@
 lemma convex_le_induct [induct set: convex_le]:
   assumes le: "t \<le>\<natural> u"
   assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v"
-  assumes 3: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
+  assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
   shows "P t u"
 using le apply (induct t arbitrary: u rule: pd_basis_induct)
@@ -168,18 +168,18 @@
 done
 
 interpretation convex_pd:
-  bifinite_basis [convex_le convex_principal Rep_convex_pd approx_pd]
+  bifinite_basis [convex_le approx_pd convex_principal Rep_convex_pd]
 apply unfold_locales
-apply (rule ideal_Rep_convex_pd)
-apply (rule cont_Rep_convex_pd)
-apply (rule Rep_convex_principal)
-apply (simp only: less_convex_pd_def less_set_def)
 apply (rule approx_pd_convex_le)
 apply (rule approx_pd_idem)
 apply (erule approx_pd_convex_mono)
 apply (rule approx_pd_convex_mono1, simp)
 apply (rule finite_range_approx_pd)
 apply (rule ex_approx_pd_eq)
+apply (rule ideal_Rep_convex_pd)
+apply (rule cont_Rep_convex_pd)
+apply (rule Rep_convex_principal)
+apply (simp only: less_convex_pd_def less_set_def)
 done
 
 lemma convex_principal_less_iff [simp]:
diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -13,10 +13,10 @@
 
 definition
   lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where
-  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. compact_le x y)"
+  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)"
 
 lemma lower_le_refl [simp]: "t \<le>\<flat> t"
-unfolding lower_le_def by (fast intro: compact_le_refl)
+unfolding lower_le_def by fast
 
 lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v"
 unfolding lower_le_def
@@ -24,7 +24,7 @@
 apply (drule (1) bspec, erule bexE)
 apply (drule (1) bspec, erule bexE)
 apply (erule rev_bexI)
-apply (erule (1) compact_le_trans)
+apply (erule (1) trans_less)
 done
 
 interpretation lower_le: preorder [lower_le]
@@ -34,17 +34,17 @@
 unfolding lower_le_def Rep_PDUnit
 by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])
 
-lemma PDUnit_lower_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
+lemma PDUnit_lower_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
 unfolding lower_le_def Rep_PDUnit by fast
 
 lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
 unfolding lower_le_def Rep_PDPlus by fast
 
 lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
-unfolding lower_le_def Rep_PDPlus by (fast intro: compact_le_refl)
+unfolding lower_le_def Rep_PDPlus by fast
 
 lemma lower_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<flat> PDUnit b) = compact_le a b"
+  "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b"
 unfolding lower_le_def Rep_PDUnit by fast
 
 lemma lower_le_PDUnit_PDPlus_iff:
@@ -56,7 +56,7 @@
 
 lemma lower_le_induct [induct set: lower_le]:
   assumes le: "t \<le>\<flat> u"
-  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
+  assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
   assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
   shows "P t u"
@@ -123,18 +123,18 @@
 done
 
 interpretation lower_pd:
-  bifinite_basis [lower_le lower_principal Rep_lower_pd approx_pd]
+  bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
 apply unfold_locales
-apply (rule ideal_Rep_lower_pd)
-apply (rule cont_Rep_lower_pd)
-apply (rule Rep_lower_principal)
-apply (simp only: less_lower_pd_def less_set_def)
 apply (rule approx_pd_lower_le)
 apply (rule approx_pd_idem)
 apply (erule approx_pd_lower_mono)
 apply (rule approx_pd_lower_mono1, simp)
 apply (rule finite_range_approx_pd)
 apply (rule ex_approx_pd_eq)
+apply (rule ideal_Rep_lower_pd)
+apply (rule cont_Rep_lower_pd)
+apply (rule Rep_lower_principal)
+apply (simp only: less_lower_pd_def less_set_def)
 done
 
 lemma lower_principal_less_iff [simp]:
diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -24,9 +24,9 @@
   shows "OFCLASS('b, po_class)"
  apply (intro_classes, unfold less)
    apply (rule refl_less)
-  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
-  apply (erule (1) antisym_less)
- apply (erule (1) trans_less)
+  apply (erule (1) trans_less)
+ apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
+ apply (erule (1) antisym_less)
 done
 
 subsection {* Proving a subtype is finite *}
diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/Porder.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -20,10 +20,12 @@
 notation (xsymbols)
   sq_le (infixl "\<sqsubseteq>" 55)
 
-class po = sq_ord +
+class preorder = sq_ord +
   assumes refl_less [iff]: "x \<sqsubseteq> x"
+  assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+
+class po = preorder +
   assumes antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
-  assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
 
 text {* minimal fixes least element *}
 
diff -r 945d8d7a66ec -r 57a626f64875 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Thu Mar 27 00:27:16 2008 +0100
@@ -13,10 +13,10 @@
 
 definition
   upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
-  "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. compact_le x y)"
+  "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)"
 
 lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
-unfolding upper_le_def by (fast intro: compact_le_refl)
+unfolding upper_le_def by fast
 
 lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v"
 unfolding upper_le_def
@@ -24,7 +24,7 @@
 apply (drule (1) bspec, erule bexE)
 apply (drule (1) bspec, erule bexE)
 apply (erule rev_bexI)
-apply (erule (1) compact_le_trans)
+apply (erule (1) trans_less)
 done
 
 interpretation upper_le: preorder [upper_le]
@@ -33,17 +33,17 @@
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
 unfolding upper_le_def Rep_PDUnit by simp
 
-lemma PDUnit_upper_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
+lemma PDUnit_upper_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
 unfolding upper_le_def Rep_PDUnit by simp
 
 lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
 unfolding upper_le_def Rep_PDPlus by fast
 
 lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
-unfolding upper_le_def Rep_PDPlus by (fast intro: compact_le_refl)
+unfolding upper_le_def Rep_PDPlus by fast
 
 lemma upper_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<sharp> PDUnit b) = compact_le a b"
+  "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b"
 unfolding upper_le_def Rep_PDUnit by fast
 
 lemma upper_le_PDPlus_PDUnit_iff:
@@ -55,7 +55,7 @@
 
 lemma upper_le_induct [induct set: upper_le]:
   assumes le: "t \<le>\<sharp> u"
-  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
+  assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
   assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
   shows "P t u"
@@ -115,18 +115,18 @@
 done
 
 interpretation upper_pd:
-  bifinite_basis [upper_le upper_principal Rep_upper_pd approx_pd]
+  bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd]
 apply unfold_locales
-apply (rule ideal_Rep_upper_pd)
-apply (rule cont_Rep_upper_pd)
-apply (rule Rep_upper_principal)
-apply (simp only: less_upper_pd_def less_set_def)
 apply (rule approx_pd_upper_le)
 apply (rule approx_pd_idem)
 apply (erule approx_pd_upper_mono)
 apply (rule approx_pd_upper_mono1, simp)
 apply (rule finite_range_approx_pd)
 apply (rule ex_approx_pd_eq)
+apply (rule ideal_Rep_upper_pd)
+apply (rule cont_Rep_upper_pd)
+apply (rule Rep_upper_principal)
+apply (simp only: less_upper_pd_def less_set_def)
 done
 
 lemma upper_principal_less_iff [simp]: