--- 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
--- 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]:
--- 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]:
--- 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 *}
--- 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 *}
--- 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]: