rename locales;
add completion_approx constant to ideal_completion locale;
add new set-like syntax for powerdomains;
reorganized proofs
--- a/src/HOLCF/CompactBasis.thy Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy Fri May 16 23:25:37 2008 +0200
@@ -52,7 +52,7 @@
lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
apply (rule idealI)
apply (rule_tac x=z in exI)
-apply (fast intro: refl)
+apply fast
apply (rule_tac x=z in bexI, fast)
apply fast
apply (fast intro: trans_less)
@@ -116,7 +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 plotkin_order = preorder r +
+locale basis_take = 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"
@@ -125,28 +125,28 @@
assumes finite_range_take: "finite (range (take n))"
assumes take_covers: "\<exists>n. take n a = a"
-locale bifinite_basis = plotkin_order r +
+locale ideal_completion = basis_take 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"
+ fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
+ assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
+ assumes cont_rep: "cont rep"
+ assumes rep_principal: "\<And>a. rep (principal a) = {b. r b a}"
+ assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
begin
-lemma finite_take_approxes: "finite (take n ` approxes x)"
+lemma finite_take_rep: "finite (take n ` rep x)"
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
lemma basis_fun_lemma0:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "\<exists>u. f ` take i ` approxes x <<| u"
+ shows "\<exists>u. f ` take i ` rep x <<| u"
apply (rule finite_directed_has_lub)
apply (rule finite_imageI)
-apply (rule finite_take_approxes)
+apply (rule finite_take_rep)
apply (subst image_image)
apply (rule directed_image_ideal)
-apply (rule ideal_approxes)
+apply (rule ideal_rep)
apply (rule f_mono)
apply (erule take_mono)
done
@@ -154,7 +154,7 @@
lemma basis_fun_lemma1:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "chain (\<lambda>i. lub (f ` take i ` approxes x))"
+ shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
apply (rule chainI)
apply (rule is_lub_thelub0)
apply (rule basis_fun_lemma0, erule f_mono)
@@ -168,7 +168,7 @@
lemma basis_fun_lemma2:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "f ` approxes x <<| (\<Squnion>i. lub (f ` take i ` approxes x))"
+ shows "f ` rep x <<| (\<Squnion>i. lub (f ` take i ` rep x))"
apply (rule is_lubI)
apply (rule ub_imageI, rename_tac a)
apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
@@ -191,74 +191,80 @@
lemma basis_fun_lemma:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "\<exists>u. f ` approxes x <<| u"
+ shows "\<exists>u. f ` rep x <<| u"
by (rule exI, rule basis_fun_lemma2, erule f_mono)
-lemma approxes_mono: "x \<sqsubseteq> y \<Longrightarrow> approxes x \<subseteq> approxes y"
-apply (drule cont_approxes [THEN cont2mono, THEN monofunE])
+lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
+apply (drule cont_rep [THEN cont2mono, THEN monofunE])
apply (simp add: set_cpo_simps)
done
-lemma approxes_contlub:
- "chain Y \<Longrightarrow> approxes (\<Squnion>i. Y i) = (\<Union>i. approxes (Y i))"
-by (simp add: cont2contlubE [OF cont_approxes] set_cpo_simps)
+lemma rep_contlub:
+ "chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
+by (simp add: cont2contlubE [OF cont_rep] set_cpo_simps)
-lemma less_def: "(x \<sqsubseteq> y) = (approxes x \<subseteq> approxes y)"
-by (rule iffI [OF approxes_mono subset_approxesD])
+lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
+by (rule iffI [OF rep_mono subset_repD])
-lemma approxes_eq: "approxes x = {a. principal a \<sqsubseteq> x}"
-unfolding less_def approxes_principal
+lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
+unfolding less_def rep_principal
apply safe
-apply (erule (1) idealD3 [OF ideal_approxes])
+apply (erule (1) idealD3 [OF ideal_rep])
apply (erule subsetD, simp add: refl)
done
-lemma mem_approxes_iff: "(a \<in> approxes x) = (principal a \<sqsubseteq> x)"
-by (simp add: approxes_eq)
+lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
+by (simp add: rep_eq)
+
+lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
+by (simp add: rep_eq)
-lemma principal_less_iff: "(principal a \<sqsubseteq> x) = (a \<in> approxes x)"
-by (simp add: approxes_eq)
+lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> r a b"
+by (simp add: principal_less_iff_mem_rep rep_principal)
-lemma approxesD: "a \<in> approxes x \<Longrightarrow> principal a \<sqsubseteq> x"
-by (simp add: approxes_eq)
+lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> r a b \<and> r b a"
+unfolding po_eq_conv [where 'a='b] principal_less_iff ..
+
+lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
+by (simp add: rep_eq)
lemma principal_mono: "r a b \<Longrightarrow> principal a \<sqsubseteq> principal b"
-by (rule approxesD, simp add: approxes_principal)
+by (simp add: principal_less_iff)
lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_less_iff
+unfolding principal_less_iff_mem_rep
by (simp add: less_def subset_eq)
-lemma lub_principal_approxes: "principal ` approxes x <<| x"
+lemma lub_principal_rep: "principal ` rep x <<| x"
apply (rule is_lubI)
apply (rule ub_imageI)
-apply (erule approxesD)
+apply (erule repD)
apply (subst less_def)
apply (rule subsetI)
apply (drule (1) ub_imageD)
-apply (simp add: approxes_eq)
+apply (simp add: rep_eq)
done
definition
basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
- "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` approxes x)))"
+ "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
lemma basis_fun_beta:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "basis_fun f\<cdot>x = lub (f ` approxes x)"
+ shows "basis_fun f\<cdot>x = lub (f ` rep x)"
unfolding basis_fun_def
proof (rule beta_cfun)
- have lub: "\<And>x. \<exists>u. f ` approxes x <<| u"
+ have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
using f_mono by (rule basis_fun_lemma)
- show cont: "cont (\<lambda>x. lub (f ` approxes x))"
+ show cont: "cont (\<lambda>x. lub (f ` rep x))"
apply (rule contI2)
apply (rule monofunI)
apply (rule is_lub_thelub0 [OF lub ub_imageI])
apply (rule is_ub_thelub0 [OF lub imageI])
- apply (erule (1) subsetD [OF approxes_mono])
+ apply (erule (1) subsetD [OF rep_mono])
apply (rule is_lub_thelub0 [OF lub ub_imageI])
- apply (simp add: approxes_contlub, clarify)
+ apply (simp add: rep_contlub, clarify)
apply (erule rev_trans_less [OF is_ub_thelub])
apply (erule is_ub_thelub0 [OF lub imageI])
done
@@ -269,7 +275,7 @@
assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
shows "basis_fun f\<cdot>(principal a) = f a"
apply (subst basis_fun_beta, erule f_mono)
-apply (subst approxes_principal)
+apply (subst rep_principal)
apply (rule lub_image_principal, erule f_mono)
done
@@ -290,10 +296,24 @@
done
lemma compact_principal: "compact (principal a)"
-by (rule compactI2, simp add: principal_less_iff approxes_contlub)
+by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
+
+definition
+ completion_approx :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where
+ "completion_approx = (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
-lemma chain_basis_fun_take:
- "chain (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
+lemma completion_approx_beta:
+ "completion_approx i\<cdot>x = (\<Squnion>a\<in>rep x. principal (take i a))"
+unfolding completion_approx_def
+by (simp add: basis_fun_beta principal_mono take_mono)
+
+lemma completion_approx_principal:
+ "completion_approx i\<cdot>(principal a) = principal (take i a)"
+unfolding completion_approx_def
+by (simp add: basis_fun_principal principal_mono take_mono)
+
+lemma chain_completion_approx: "chain completion_approx"
+unfolding completion_approx_def
apply (rule chainI)
apply (rule basis_fun_mono)
apply (erule principal_mono [OF take_mono])
@@ -301,53 +321,56 @@
apply (rule principal_mono [OF take_chain])
done
-lemma lub_basis_fun_take:
- "(\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x) = x"
- apply (simp add: basis_fun_beta principal_mono take_mono)
+lemma lub_completion_approx: "(\<Squnion>i. completion_approx i\<cdot>x) = x"
+unfolding completion_approx_beta
apply (subst image_image [where f=principal, symmetric])
- apply (rule unique_lub [OF _ lub_principal_approxes])
+ apply (rule unique_lub [OF _ lub_principal_rep])
apply (rule basis_fun_lemma2, erule principal_mono)
done
-lemma basis_fun_take_eq_principal:
- "\<exists>a\<in>approxes x.
- basis_fun (\<lambda>a. principal (take i a))\<cdot>x = principal (take i a)"
- apply (simp add: basis_fun_beta principal_mono take_mono)
+lemma completion_approx_eq_principal:
+ "\<exists>a\<in>rep x. completion_approx i\<cdot>x = principal (take i a)"
+unfolding completion_approx_beta
apply (subst image_image [where f=principal, symmetric])
- apply (subgoal_tac "finite (principal ` take i ` approxes x)")
- apply (subgoal_tac "directed (principal ` take i ` approxes x)")
+ apply (subgoal_tac "finite (principal ` take i ` rep x)")
+ apply (subgoal_tac "directed (principal ` take i ` rep x)")
apply (drule (1) lub_finite_directed_in_self, fast)
apply (subst image_image)
apply (rule directed_image_ideal)
- apply (rule ideal_approxes)
+ apply (rule ideal_rep)
apply (erule principal_mono [OF take_mono])
apply (rule finite_imageI)
- apply (rule finite_take_approxes)
+ apply (rule finite_take_rep)
+done
+
+lemma completion_approx_idem:
+ "completion_approx i\<cdot>(completion_approx i\<cdot>x) = completion_approx i\<cdot>x"
+using completion_approx_eq_principal [where i=i and x=x]
+by (auto simp add: completion_approx_principal take_take)
+
+lemma finite_fixes_completion_approx:
+ "finite {x. completion_approx i\<cdot>x = x}" (is "finite ?S")
+apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
+apply (erule finite_subset)
+apply (rule finite_imageI)
+apply (rule finite_range_take)
+apply (clarify, erule subst)
+apply (cut_tac x=x and i=i in completion_approx_eq_principal)
+apply fast
done
lemma principal_induct:
assumes adm: "adm P"
assumes P: "\<And>a. P (principal a)"
shows "P x"
- apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
- apply (simp add: lub_basis_fun_take)
+ apply (subgoal_tac "P (\<Squnion>i. completion_approx i\<cdot>x)")
+ apply (simp add: lub_completion_approx)
apply (rule admD [OF adm])
- apply (simp add: chain_basis_fun_take)
- apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
+ apply (simp add: chain_completion_approx)
+ apply (cut_tac x=x and i=i in completion_approx_eq_principal)
apply (clarify, simp add: P)
done
-lemma finite_fixes_basis_fun_take:
- "finite {x. basis_fun (\<lambda>a. principal (take i a))\<cdot>x = x}" (is "finite ?S")
-apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
-apply (erule finite_subset)
-apply (rule finite_imageI)
-apply (rule finite_range_take)
-apply (clarify, erule subst)
-apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
-apply fast
-done
-
end
@@ -359,7 +382,7 @@
by (fast intro: compact_approx)
lemma compact_Rep_compact_basis [simp]: "compact (Rep_compact_basis a)"
-by (rule Rep_compact_basis [simplified])
+by (rule Rep_compact_basis [unfolded mem_Collect_eq])
lemma Rep_Abs_compact_basis_approx [simp]:
"Rep_compact_basis (Abs_compact_basis (approx n\<cdot>x)) = approx n\<cdot>x"
@@ -520,7 +543,7 @@
done
interpretation compact_basis:
- bifinite_basis [sq_le compact_approx Rep_compact_basis compacts]
+ ideal_completion [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"
@@ -620,12 +643,14 @@
"('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
-lemma (in ab_semigroup_idem_mult) fold_pd_PDUnit:
- "fold_pd g (op *) (PDUnit x) = g x"
+lemma fold_pd_PDUnit:
+ includes ab_semigroup_idem_mult f
+ shows "fold_pd g f (PDUnit x) = g x"
unfolding fold_pd_def Rep_PDUnit by simp
-lemma (in ab_semigroup_idem_mult) fold_pd_PDPlus:
- "fold_pd g (op *) (PDPlus t u) = fold_pd g (op *) t * fold_pd g (op *) u"
+lemma fold_pd_PDPlus:
+ includes ab_semigroup_idem_mult f
+ shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
text {* approx-pd *}
--- a/src/HOLCF/ConvexPD.thy Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy Fri May 16 23:25:37 2008 +0200
@@ -148,14 +148,11 @@
done
lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
-by (rule Rep_convex_pd [simplified])
+by (rule Rep_convex_pd [unfolded mem_Collect_eq])
lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
unfolding less_convex_pd_def less_set_eq .
-
-subsection {* Principal ideals *}
-
definition
convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
"convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
@@ -168,7 +165,7 @@
done
interpretation convex_pd:
- bifinite_basis [convex_le approx_pd convex_principal Rep_convex_pd]
+ ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
apply unfold_locales
apply (rule approx_pd_convex_le)
apply (rule approx_pd_idem)
@@ -183,13 +180,16 @@
done
lemma convex_principal_less_iff [simp]:
- "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
-unfolding less_convex_pd_def Rep_convex_principal less_set_eq
-by (fast intro: convex_le_refl elim: convex_le_trans)
+ "convex_principal t \<sqsubseteq> convex_principal u \<longleftrightarrow> t \<le>\<natural> u"
+by (rule convex_pd.principal_less_iff)
+
+lemma convex_principal_eq_iff [simp]:
+ "convex_principal t = convex_principal u \<longleftrightarrow> t \<le>\<natural> u \<and> u \<le>\<natural> t"
+by (rule convex_pd.principal_eq_iff)
lemma convex_principal_mono:
"t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
-by (rule convex_principal_less_iff [THEN iffD2])
+by (rule convex_pd.principal_mono)
lemma compact_convex_principal: "compact (convex_principal t)"
by (rule convex_pd.compact_principal)
@@ -198,7 +198,7 @@
by (induct ys rule: convex_pd.principal_induct, simp, simp)
instance convex_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: convex_pd_minimal)
+by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
by (rule convex_pd_minimal [THEN UU_I, symmetric])
@@ -209,51 +209,27 @@
instance convex_pd :: (profinite) approx ..
defs (overloaded)
- approx_convex_pd_def:
- "approx \<equiv> (\<lambda>n. convex_pd.basis_fun (\<lambda>t. convex_principal (approx_pd n t)))"
+ approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
+
+instance convex_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_convex_pd_def)
+apply (simp add: convex_pd.chain_completion_approx)
+apply (rule convex_pd.lub_completion_approx)
+apply (rule convex_pd.completion_approx_idem)
+apply (rule convex_pd.finite_fixes_completion_approx)
+done
+
+instance convex_pd :: (bifinite) bifinite ..
lemma approx_convex_principal [simp]:
"approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
unfolding approx_convex_pd_def
-apply (rule convex_pd.basis_fun_principal)
-apply (erule convex_principal_mono [OF approx_pd_convex_mono])
-done
-
-lemma chain_approx_convex_pd:
- "chain (approx :: nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd)"
-unfolding approx_convex_pd_def
-by (rule convex_pd.chain_basis_fun_take)
-
-lemma lub_approx_convex_pd:
- "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a convex_pd)"
-unfolding approx_convex_pd_def
-by (rule convex_pd.lub_basis_fun_take)
-
-lemma approx_convex_pd_idem:
- "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule convex_pd.completion_approx_principal)
lemma approx_eq_convex_principal:
"\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
unfolding approx_convex_pd_def
-by (rule convex_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_convex_pd:
- "finite {xs::'a convex_pd. approx n\<cdot>xs = xs}"
-unfolding approx_convex_pd_def
-by (rule convex_pd.finite_fixes_basis_fun_take)
-
-instance convex_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_convex_pd)
-apply (rule lub_approx_convex_pd)
-apply (rule approx_convex_pd_idem)
-apply (rule finite_fixes_approx_convex_pd)
-done
-
-instance convex_pd :: (bifinite) bifinite ..
+by (rule convex_pd.completion_approx_eq_principal)
lemma compact_imp_convex_principal:
"compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
@@ -266,10 +242,7 @@
lemma convex_principal_induct:
"\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_convex_principal)
-apply (clarify, simp)
-done
+by (rule convex_pd.principal_induct)
lemma convex_principal_induct2:
"\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -282,54 +255,12 @@
done
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
definition
convex_unit :: "'a \<rightarrow> 'a convex_pd" where
"convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
-lemma convex_unit_Rep_compact_basis [simp]:
- "convex_unit\<cdot>(Rep_compact_basis a) = convex_principal (PDUnit a)"
-unfolding convex_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule convex_principal_mono)
-apply (erule PDUnit_convex_mono)
-done
-
-lemma convex_unit_strict [simp]: "convex_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_convex_unit [simp]:
- "approx n\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma convex_unit_less_iff [simp]:
- "(convex_unit\<cdot>x \<sqsubseteq> convex_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
- apply (rule bifinite_less_ext)
- apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
- apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
- apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
- apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma convex_unit_eq_iff [simp]:
- "(convex_unit\<cdot>x = convex_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma convex_unit_strict_iff [simp]: "(convex_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
-
-lemma compact_convex_unit_iff [simp]:
- "compact (convex_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
definition
convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
"convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
@@ -340,40 +271,69 @@
(infixl "+\<natural>" 65) where
"xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
+syntax
+ "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
+
+translations
+ "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
+ "{x}\<natural>" == "CONST convex_unit\<cdot>x"
+
+lemma convex_unit_Rep_compact_basis [simp]:
+ "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
+unfolding convex_unit_def
+by (simp add: compact_basis.basis_fun_principal
+ convex_principal_mono PDUnit_convex_mono)
+
lemma convex_plus_principal [simp]:
- "convex_plus\<cdot>(convex_principal t)\<cdot>(convex_principal u) =
- convex_principal (PDPlus t u)"
+ "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
unfolding convex_plus_def
by (simp add: convex_pd.basis_fun_principal
convex_pd.basis_fun_mono PDPlus_convex_mono)
+lemma approx_convex_unit [simp]:
+ "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
lemma approx_convex_plus [simp]:
- "approx n\<cdot>(convex_plus\<cdot>xs\<cdot>ys) = convex_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+ "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
-lemma convex_plus_commute: "convex_plus\<cdot>xs\<cdot>ys = convex_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: convex_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
lemma convex_plus_assoc:
- "convex_plus\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>zs = convex_plus\<cdot>xs\<cdot>(convex_plus\<cdot>ys\<cdot>zs)"
+ "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
apply (rule_tac xs=zs in convex_principal_induct, simp)
apply (simp add: PDPlus_assoc)
done
-lemma convex_plus_absorb: "convex_plus\<cdot>xs\<cdot>xs = xs"
+lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
+apply (induct xs ys rule: convex_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma convex_plus_absorb: "xs +\<natural> xs = xs"
apply (induct xs rule: convex_principal_induct, simp)
apply (simp add: PDPlus_absorb)
done
+interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
+ by unfold_locales
+ (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
+
+lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
+by (rule aci_convex_plus.mult_left_commute)
+
+lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
+by (rule aci_convex_plus.mult_left_idem)
+
+lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
+
lemma convex_unit_less_plus_iff [simp]:
- "(convex_unit\<cdot>x \<sqsubseteq> convex_plus\<cdot>ys\<cdot>zs) =
- (convex_unit\<cdot>x \<sqsubseteq> ys \<and> convex_unit\<cdot>x \<sqsubseteq> zs)"
+ "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
apply (rule iffI)
apply (subgoal_tac
- "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
+ "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
@@ -383,16 +343,15 @@
apply simp
apply simp
apply (erule conjE)
- apply (subst convex_plus_absorb [of "convex_unit\<cdot>x", symmetric])
+ apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
lemma convex_plus_less_unit_iff [simp]:
- "(convex_plus\<cdot>xs\<cdot>ys \<sqsubseteq> convex_unit\<cdot>z) =
- (xs \<sqsubseteq> convex_unit\<cdot>z \<and> ys \<sqsubseteq> convex_unit\<cdot>z)"
+ "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
apply (rule iffI)
apply (subgoal_tac
- "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
+ "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
@@ -402,18 +361,46 @@
apply simp
apply simp
apply (erule conjE)
- apply (subst convex_plus_absorb [of "convex_unit\<cdot>z", symmetric])
+ apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
+lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+ apply (rule bifinite_less_ext)
+ apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+ apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+ apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+ apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
+lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>"
+unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
+
+lemma compact_convex_unit_iff [simp]:
+ "compact {x}\<natural> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_convex_plus [simp]:
+ "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
+apply (drule compact_imp_convex_principal)+
+apply (auto simp add: compact_convex_principal)
+done
+
subsection {* Induction rules *}
lemma convex_pd_induct1:
assumes P: "adm P"
- assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
- assumes insert:
- "\<And>x ys. \<lbrakk>P (convex_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>(convex_unit\<cdot>x)\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<natural>"
+ assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
shows "P (xs::'a convex_pd)"
apply (induct xs rule: convex_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct1)
@@ -426,8 +413,8 @@
lemma convex_pd_induct:
assumes P: "adm P"
- assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
- assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>xs\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<natural>"
+ assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
shows "P (xs::'a convex_pd)"
apply (induct xs rule: convex_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct)
@@ -443,9 +430,10 @@
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
"convex_bind_basis = fold_pd
(\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
- (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+ (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
-lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_convex_bind:
+ "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
apply unfold_locales
apply (simp add: convex_plus_assoc)
apply (simp add: convex_plus_commute)
@@ -456,11 +444,11 @@
"convex_bind_basis (PDUnit a) =
(\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
"convex_bind_basis (PDPlus t u) =
- (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
+ (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
unfolding convex_bind_basis_def
apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
+apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
+apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
done
lemma monofun_LAM:
@@ -487,12 +475,11 @@
done
lemma convex_bind_unit [simp]:
- "convex_bind\<cdot>(convex_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+ "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
by (induct x rule: compact_basis_induct, simp, simp)
lemma convex_bind_plus [simp]:
- "convex_bind\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>f =
- convex_plus\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>(convex_bind\<cdot>ys\<cdot>f)"
+ "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -503,7 +490,7 @@
definition
convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
- "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_unit\<cdot>(f\<cdot>x)))"
+ "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
definition
convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
@@ -514,17 +501,15 @@
unfolding convex_map_def by simp
lemma convex_map_plus [simp]:
- "convex_map\<cdot>f\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
- convex_plus\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>(convex_map\<cdot>f\<cdot>ys)"
+ "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
unfolding convex_map_def by simp
lemma convex_join_unit [simp]:
- "convex_join\<cdot>(convex_unit\<cdot>xs) = xs"
+ "convex_join\<cdot>{xs}\<natural> = xs"
unfolding convex_join_def by simp
lemma convex_join_plus [simp]:
- "convex_join\<cdot>(convex_plus\<cdot>xss\<cdot>yss) =
- convex_plus\<cdot>(convex_join\<cdot>xss)\<cdot>(convex_join\<cdot>yss)"
+ "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
unfolding convex_join_def by simp
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
@@ -571,12 +556,11 @@
done
lemma convex_to_upper_unit [simp]:
- "convex_to_upper\<cdot>(convex_unit\<cdot>x) = upper_unit\<cdot>x"
+ "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
by (induct x rule: compact_basis_induct, simp, simp)
lemma convex_to_upper_plus [simp]:
- "convex_to_upper\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
- upper_plus\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper\<cdot>ys)"
+ "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
lemma approx_convex_to_upper:
@@ -601,12 +585,11 @@
done
lemma convex_to_lower_unit [simp]:
- "convex_to_lower\<cdot>(convex_unit\<cdot>x) = lower_unit\<cdot>x"
+ "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
by (induct x rule: compact_basis_induct, simp, simp)
lemma convex_to_lower_plus [simp]:
- "convex_to_lower\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
- lower_plus\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower\<cdot>ys)"
+ "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
lemma approx_convex_to_lower:
@@ -629,4 +612,19 @@
apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
done
+lemmas convex_plus_less_plus_iff =
+ convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
+
+lemmas convex_pd_less_simps =
+ convex_unit_less_plus_iff
+ convex_plus_less_unit_iff
+ convex_plus_less_plus_iff
+ convex_unit_less_iff
+ convex_to_upper_unit
+ convex_to_upper_plus
+ convex_to_lower_unit
+ convex_to_lower_plus
+ upper_pd_less_simps
+ lower_pd_less_simps
+
end
--- a/src/HOLCF/LowerPD.thy Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Fri May 16 23:25:37 2008 +0200
@@ -103,13 +103,7 @@
done
lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
-by (rule Rep_lower_pd [simplified])
-
-lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
-unfolding less_lower_pd_def less_set_eq .
-
-
-subsection {* Principal ideals *}
+by (rule Rep_lower_pd [unfolded mem_Collect_eq])
definition
lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
@@ -123,7 +117,7 @@
done
interpretation lower_pd:
- bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
+ ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
apply unfold_locales
apply (rule approx_pd_lower_le)
apply (rule approx_pd_idem)
@@ -138,32 +132,25 @@
done
lemma lower_principal_less_iff [simp]:
- "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
-unfolding less_lower_pd_def Rep_lower_principal less_set_eq
-by (fast intro: lower_le_refl elim: lower_le_trans)
+ "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
+by (rule lower_pd.principal_less_iff)
+
+lemma lower_principal_eq_iff:
+ "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
+by (rule lower_pd.principal_eq_iff)
lemma lower_principal_mono:
"t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
-by (rule lower_principal_less_iff [THEN iffD2])
+by (rule lower_pd.principal_mono)
lemma compact_lower_principal: "compact (lower_principal t)"
-apply (rule compactI2)
-apply (simp add: less_lower_pd_def)
-apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
-apply (simp add: Rep_lower_principal set_cpo_simps)
-apply (simp add: subset_eq)
-apply (drule spec, drule mp, rule lower_le_refl)
-apply (erule exE, rename_tac i)
-apply (rule_tac x=i in exI)
-apply clarify
-apply (erule (1) lower_le.idealD3 [OF ideal_Rep_lower_pd])
-done
+by (rule lower_pd.compact_principal)
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
instance lower_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: lower_pd_minimal)
+by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
by (rule lower_pd_minimal [THEN UU_I, symmetric])
@@ -174,51 +161,27 @@
instance lower_pd :: (profinite) approx ..
defs (overloaded)
- approx_lower_pd_def:
- "approx \<equiv> (\<lambda>n. lower_pd.basis_fun (\<lambda>t. lower_principal (approx_pd n t)))"
+ approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
+
+instance lower_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_lower_pd_def)
+apply (simp add: lower_pd.chain_completion_approx)
+apply (rule lower_pd.lub_completion_approx)
+apply (rule lower_pd.completion_approx_idem)
+apply (rule lower_pd.finite_fixes_completion_approx)
+done
+
+instance lower_pd :: (bifinite) bifinite ..
lemma approx_lower_principal [simp]:
"approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
-apply (rule lower_pd.basis_fun_principal)
-apply (erule lower_principal_mono [OF approx_pd_lower_mono])
-done
-
-lemma chain_approx_lower_pd:
- "chain (approx :: nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.chain_basis_fun_take)
-
-lemma lub_approx_lower_pd:
- "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.lub_basis_fun_take)
-
-lemma approx_lower_pd_idem:
- "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule lower_pd.completion_approx_principal)
lemma approx_eq_lower_principal:
"\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
-by (rule lower_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_lower_pd:
- "finite {xs::'a lower_pd. approx n\<cdot>xs = xs}"
-unfolding approx_lower_pd_def
-by (rule lower_pd.finite_fixes_basis_fun_take)
-
-instance lower_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_lower_pd)
-apply (rule lub_approx_lower_pd)
-apply (rule approx_lower_pd_idem)
-apply (rule finite_fixes_approx_lower_pd)
-done
-
-instance lower_pd :: (bifinite) bifinite ..
+by (rule lower_pd.completion_approx_eq_principal)
lemma compact_imp_lower_principal:
"compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
@@ -231,10 +194,7 @@
lemma lower_principal_induct:
"\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_lower_principal)
-apply (clarify, simp)
-done
+by (rule lower_pd.principal_induct)
lemma lower_principal_induct2:
"\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -247,54 +207,12 @@
done
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
definition
lower_unit :: "'a \<rightarrow> 'a lower_pd" where
"lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
-lemma lower_unit_Rep_compact_basis [simp]:
- "lower_unit\<cdot>(Rep_compact_basis a) = lower_principal (PDUnit a)"
-unfolding lower_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule lower_principal_mono)
-apply (erule PDUnit_lower_mono)
-done
-
-lemma lower_unit_strict [simp]: "lower_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_lower_unit [simp]:
- "approx n\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma lower_unit_less_iff [simp]:
- "(lower_unit\<cdot>x \<sqsubseteq> lower_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
- apply (rule bifinite_less_ext)
- apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
- apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
- apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
- apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma lower_unit_eq_iff [simp]:
- "(lower_unit\<cdot>x = lower_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma lower_unit_strict_iff [simp]: "(lower_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
-
-lemma compact_lower_unit_iff [simp]:
- "compact (lower_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
definition
lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
"lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
@@ -305,79 +223,89 @@
(infixl "+\<flat>" 65) where
"xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
+syntax
+ "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
+
+translations
+ "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
+ "{x}\<flat>" == "CONST lower_unit\<cdot>x"
+
+lemma lower_unit_Rep_compact_basis [simp]:
+ "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
+unfolding lower_unit_def
+by (simp add: compact_basis.basis_fun_principal
+ lower_principal_mono PDUnit_lower_mono)
+
lemma lower_plus_principal [simp]:
- "lower_plus\<cdot>(lower_principal t)\<cdot>(lower_principal u) =
- lower_principal (PDPlus t u)"
+ "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
unfolding lower_plus_def
by (simp add: lower_pd.basis_fun_principal
lower_pd.basis_fun_mono PDPlus_lower_mono)
+lemma approx_lower_unit [simp]:
+ "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
lemma approx_lower_plus [simp]:
- "approx n\<cdot>(lower_plus\<cdot>xs\<cdot>ys) = lower_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+ "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
-lemma lower_plus_commute: "lower_plus\<cdot>xs\<cdot>ys = lower_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: lower_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
-lemma lower_plus_assoc:
- "lower_plus\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>zs = lower_plus\<cdot>xs\<cdot>(lower_plus\<cdot>ys\<cdot>zs)"
+lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
apply (rule_tac xs=zs in lower_principal_induct, simp)
apply (simp add: PDPlus_assoc)
done
-lemma lower_plus_absorb: "lower_plus\<cdot>xs\<cdot>xs = xs"
+lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
+apply (induct xs ys rule: lower_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma lower_plus_absorb: "xs +\<flat> xs = xs"
apply (induct xs rule: lower_principal_induct, simp)
apply (simp add: PDPlus_absorb)
done
-lemma lower_plus_less1: "xs \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+ by unfold_locales
+ (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
+
+lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
+by (rule aci_lower_plus.mult_left_commute)
+
+lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
+by (rule aci_lower_plus.mult_left_idem)
+
+lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
+
+lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
apply (induct xs ys rule: lower_principal_induct2, simp, simp)
apply (simp add: PDPlus_lower_less)
done
-lemma lower_plus_less2: "ys \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
by (subst lower_plus_commute, rule lower_plus_less1)
-lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs"
+lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
apply (subst lower_plus_absorb [of zs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
lemma lower_plus_less_iff:
- "(lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs) = (xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs)"
+ "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
apply safe
apply (erule trans_less [OF lower_plus_less1])
apply (erule trans_less [OF lower_plus_less2])
apply (erule (1) lower_plus_least)
done
-lemma lower_plus_strict_iff [simp]:
- "(lower_plus\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<and> ys = \<bottom>)"
-apply safe
-apply (rule UU_I, erule subst, rule lower_plus_less1)
-apply (rule UU_I, erule subst, rule lower_plus_less2)
-apply (rule lower_plus_absorb)
-done
-
-lemma lower_plus_strict1 [simp]: "lower_plus\<cdot>\<bottom>\<cdot>ys = ys"
-apply (rule antisym_less [OF _ lower_plus_less2])
-apply (simp add: lower_plus_least)
-done
-
-lemma lower_plus_strict2 [simp]: "lower_plus\<cdot>xs\<cdot>\<bottom> = xs"
-apply (rule antisym_less [OF _ lower_plus_less1])
-apply (simp add: lower_plus_least)
-done
-
lemma lower_unit_less_plus_iff:
- "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
- (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
+ "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
apply (rule iffI)
apply (subgoal_tac
- "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
+ "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
@@ -391,19 +319,65 @@
apply (erule trans_less [OF _ lower_plus_less2])
done
+lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+ apply (rule bifinite_less_ext)
+ apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+ apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+ apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+ apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
lemmas lower_pd_less_simps =
lower_unit_less_iff
lower_plus_less_iff
lower_unit_less_plus_iff
+lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
+unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
+
+lemma lower_plus_strict_iff [simp]:
+ "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
+apply safe
+apply (rule UU_I, erule subst, rule lower_plus_less1)
+apply (rule UU_I, erule subst, rule lower_plus_less2)
+apply (rule lower_plus_absorb)
+done
+
+lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
+apply (rule antisym_less [OF _ lower_plus_less2])
+apply (simp add: lower_plus_least)
+done
+
+lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
+apply (rule antisym_less [OF _ lower_plus_less1])
+apply (simp add: lower_plus_least)
+done
+
+lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_lower_plus [simp]:
+ "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
+apply (drule compact_imp_lower_principal)+
+apply (auto simp add: compact_lower_principal)
+done
+
subsection {* Induction rules *}
lemma lower_pd_induct1:
assumes P: "adm P"
- assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
+ assumes unit: "\<And>x. P {x}\<flat>"
assumes insert:
- "\<And>x ys. \<lbrakk>P (lower_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>(lower_unit\<cdot>x)\<cdot>ys)"
+ "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
shows "P (xs::'a lower_pd)"
apply (induct xs rule: lower_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct1)
@@ -416,8 +390,8 @@
lemma lower_pd_induct:
assumes P: "adm P"
- assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
- assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>xs\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<flat>"
+ assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
shows "P (xs::'a lower_pd)"
apply (induct xs rule: lower_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct)
@@ -433,9 +407,10 @@
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
"lower_bind_basis = fold_pd
(\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
- (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+ (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
-lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_lower_bind:
+ "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
@@ -446,11 +421,11 @@
"lower_bind_basis (PDUnit a) =
(\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
"lower_bind_basis (PDPlus t u) =
- (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
+ (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
unfolding lower_bind_basis_def
apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
+apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
+apply (rule fold_pd_PDPlus [OF ACI_lower_bind])
done
lemma lower_bind_basis_mono:
@@ -474,12 +449,11 @@
done
lemma lower_bind_unit [simp]:
- "lower_bind\<cdot>(lower_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+ "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
by (induct x rule: compact_basis_induct, simp, simp)
lemma lower_bind_plus [simp]:
- "lower_bind\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>f =
- lower_plus\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>(lower_bind\<cdot>ys\<cdot>f)"
+ "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -490,28 +464,26 @@
definition
lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
- "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_unit\<cdot>(f\<cdot>x)))"
+ "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))"
definition
lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
"lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
lemma lower_map_unit [simp]:
- "lower_map\<cdot>f\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(f\<cdot>x)"
+ "lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>"
unfolding lower_map_def by simp
lemma lower_map_plus [simp]:
- "lower_map\<cdot>f\<cdot>(lower_plus\<cdot>xs\<cdot>ys) =
- lower_plus\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>(lower_map\<cdot>f\<cdot>ys)"
+ "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
unfolding lower_map_def by simp
lemma lower_join_unit [simp]:
- "lower_join\<cdot>(lower_unit\<cdot>xs) = xs"
+ "lower_join\<cdot>{xs}\<flat> = xs"
unfolding lower_join_def by simp
lemma lower_join_plus [simp]:
- "lower_join\<cdot>(lower_plus\<cdot>xss\<cdot>yss) =
- lower_plus\<cdot>(lower_join\<cdot>xss)\<cdot>(lower_join\<cdot>yss)"
+ "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
unfolding lower_join_def by simp
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
--- a/src/HOLCF/UpperPD.thy Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/UpperPD.thy Fri May 16 23:25:37 2008 +0200
@@ -101,7 +101,7 @@
done
lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
-by (rule Rep_upper_pd [simplified])
+by (rule Rep_upper_pd [unfolded mem_Collect_eq])
definition
upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
@@ -110,12 +110,12 @@
lemma Rep_upper_principal:
"Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
unfolding upper_principal_def
-apply (rule Abs_upper_pd_inverse [simplified])
+apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
apply (rule upper_le.ideal_principal)
done
interpretation upper_pd:
- bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd]
+ ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
apply unfold_locales
apply (rule approx_pd_upper_le)
apply (rule approx_pd_idem)
@@ -130,9 +130,12 @@
done
lemma upper_principal_less_iff [simp]:
- "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
-unfolding less_upper_pd_def Rep_upper_principal less_set_eq
-by (fast intro: upper_le_refl elim: upper_le_trans)
+ "upper_principal t \<sqsubseteq> upper_principal u \<longleftrightarrow> t \<le>\<sharp> u"
+by (rule upper_pd.principal_less_iff)
+
+lemma upper_principal_eq_iff:
+ "upper_principal t = upper_principal u \<longleftrightarrow> t \<le>\<sharp> u \<and> u \<le>\<sharp> t"
+by (rule upper_pd.principal_eq_iff)
lemma upper_principal_mono:
"t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
@@ -145,7 +148,7 @@
by (induct ys rule: upper_pd.principal_induct, simp, simp)
instance upper_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: upper_pd_minimal)
+by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
by (rule upper_pd_minimal [THEN UU_I, symmetric])
@@ -156,51 +159,27 @@
instance upper_pd :: (profinite) approx ..
defs (overloaded)
- approx_upper_pd_def:
- "approx \<equiv> (\<lambda>n. upper_pd.basis_fun (\<lambda>t. upper_principal (approx_pd n t)))"
+ approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
+
+instance upper_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_upper_pd_def)
+apply (simp add: upper_pd.chain_completion_approx)
+apply (rule upper_pd.lub_completion_approx)
+apply (rule upper_pd.completion_approx_idem)
+apply (rule upper_pd.finite_fixes_completion_approx)
+done
+
+instance upper_pd :: (bifinite) bifinite ..
lemma approx_upper_principal [simp]:
"approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
unfolding approx_upper_pd_def
-apply (rule upper_pd.basis_fun_principal)
-apply (erule upper_principal_mono [OF approx_pd_upper_mono])
-done
-
-lemma chain_approx_upper_pd:
- "chain (approx :: nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd)"
-unfolding approx_upper_pd_def
-by (rule upper_pd.chain_basis_fun_take)
-
-lemma lub_approx_upper_pd:
- "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a upper_pd)"
-unfolding approx_upper_pd_def
-by (rule upper_pd.lub_basis_fun_take)
-
-lemma approx_upper_pd_idem:
- "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule upper_pd.completion_approx_principal)
lemma approx_eq_upper_principal:
"\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
unfolding approx_upper_pd_def
-by (rule upper_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_upper_pd:
- "finite {xs::'a upper_pd. approx n\<cdot>xs = xs}"
-unfolding approx_upper_pd_def
-by (rule upper_pd.finite_fixes_basis_fun_take)
-
-instance upper_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_upper_pd)
-apply (rule lub_approx_upper_pd)
-apply (rule approx_upper_pd_idem)
-apply (rule finite_fixes_approx_upper_pd)
-done
-
-instance upper_pd :: (bifinite) bifinite ..
+by (rule upper_pd.completion_approx_eq_principal)
lemma compact_imp_upper_principal:
"compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
@@ -213,10 +192,7 @@
lemma upper_principal_induct:
"\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_upper_principal)
-apply (clarify, simp)
-done
+by (rule upper_pd.principal_induct)
lemma upper_principal_induct2:
"\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -229,54 +205,12 @@
done
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
definition
upper_unit :: "'a \<rightarrow> 'a upper_pd" where
"upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
-lemma upper_unit_Rep_compact_basis [simp]:
- "upper_unit\<cdot>(Rep_compact_basis a) = upper_principal (PDUnit a)"
-unfolding upper_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule upper_principal_mono)
-apply (erule PDUnit_upper_mono)
-done
-
-lemma upper_unit_strict [simp]: "upper_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_upper_unit [simp]:
- "approx n\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma upper_unit_less_iff [simp]:
- "(upper_unit\<cdot>x \<sqsubseteq> upper_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
- apply (rule bifinite_less_ext)
- apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
- apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
- apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
- apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma upper_unit_eq_iff [simp]:
- "(upper_unit\<cdot>x = upper_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma upper_unit_strict_iff [simp]: "(upper_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
-
-lemma compact_upper_unit_iff [simp]:
- "compact (upper_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
definition
upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
"upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
@@ -287,67 +221,89 @@
(infixl "+\<sharp>" 65) where
"xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
+syntax
+ "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
+
+translations
+ "{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>"
+ "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
+
+lemma upper_unit_Rep_compact_basis [simp]:
+ "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
+unfolding upper_unit_def
+by (simp add: compact_basis.basis_fun_principal
+ upper_principal_mono PDUnit_upper_mono)
+
lemma upper_plus_principal [simp]:
- "upper_plus\<cdot>(upper_principal t)\<cdot>(upper_principal u) =
- upper_principal (PDPlus t u)"
+ "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
unfolding upper_plus_def
by (simp add: upper_pd.basis_fun_principal
upper_pd.basis_fun_mono PDPlus_upper_mono)
+lemma approx_upper_unit [simp]:
+ "approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
lemma approx_upper_plus [simp]:
- "approx n\<cdot>(upper_plus\<cdot>xs\<cdot>ys) = upper_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+ "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
-lemma upper_plus_commute: "upper_plus\<cdot>xs\<cdot>ys = upper_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: upper_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
-lemma upper_plus_assoc:
- "upper_plus\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>zs = upper_plus\<cdot>xs\<cdot>(upper_plus\<cdot>ys\<cdot>zs)"
+lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
apply (rule_tac xs=zs in upper_principal_induct, simp)
apply (simp add: PDPlus_assoc)
done
-lemma upper_plus_absorb: "upper_plus\<cdot>xs\<cdot>xs = xs"
+lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
+apply (induct xs ys rule: upper_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
apply (induct xs rule: upper_principal_induct, simp)
apply (simp add: PDPlus_absorb)
done
-lemma upper_plus_less1: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> xs"
+interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
+ by unfold_locales
+ (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
+
+lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
+by (rule aci_upper_plus.mult_left_commute)
+
+lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
+by (rule aci_upper_plus.mult_left_idem)
+
+lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
+
+lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
apply (induct xs ys rule: upper_principal_induct2, simp, simp)
apply (simp add: PDPlus_upper_less)
done
-lemma upper_plus_less2: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> ys"
+lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
by (subst upper_plus_commute, rule upper_plus_less1)
-lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs"
+lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
apply (subst upper_plus_absorb [of xs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
lemma upper_less_plus_iff:
- "(xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs) = (xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs)"
+ "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
apply safe
apply (erule trans_less [OF _ upper_plus_less1])
apply (erule trans_less [OF _ upper_plus_less2])
apply (erule (1) upper_plus_greatest)
done
-lemma upper_plus_strict1 [simp]: "upper_plus\<cdot>\<bottom>\<cdot>ys = \<bottom>"
-by (rule UU_I, rule upper_plus_less1)
-
-lemma upper_plus_strict2 [simp]: "upper_plus\<cdot>xs\<cdot>\<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_less2)
-
lemma upper_plus_less_unit_iff:
- "(upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> upper_unit\<cdot>z) =
- (xs \<sqsubseteq> upper_unit\<cdot>z \<or> ys \<sqsubseteq> upper_unit\<cdot>z)"
+ "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
apply (rule iffI)
apply (subgoal_tac
- "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
+ "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
@@ -361,19 +317,62 @@
apply (erule trans_less [OF upper_plus_less2])
done
+lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+ apply (rule bifinite_less_ext)
+ apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+ apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+ apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+ apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
lemmas upper_pd_less_simps =
upper_unit_less_iff
upper_less_plus_iff
upper_plus_less_unit_iff
+lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>"
+unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
+by (rule UU_I, rule upper_plus_less1)
+
+lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
+by (rule UU_I, rule upper_plus_less2)
+
+lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
+
+lemma upper_plus_strict_iff [simp]:
+ "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
+apply (rule iffI)
+apply (erule rev_mp)
+apply (rule upper_principal_induct2 [where xs=xs and ys=ys], simp, simp)
+apply (simp add: inst_upper_pd_pcpo upper_principal_eq_iff
+ upper_le_PDPlus_PDUnit_iff)
+apply auto
+done
+
+lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_upper_plus [simp]:
+ "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
+apply (drule compact_imp_upper_principal)+
+apply (auto simp add: compact_upper_principal)
+done
+
subsection {* Induction rules *}
lemma upper_pd_induct1:
assumes P: "adm P"
- assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
- assumes insert:
- "\<And>x ys. \<lbrakk>P (upper_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>(upper_unit\<cdot>x)\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<sharp>"
+ assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
shows "P (xs::'a upper_pd)"
apply (induct xs rule: upper_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct1)
@@ -386,8 +385,8 @@
lemma upper_pd_induct:
assumes P: "adm P"
- assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
- assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>xs\<cdot>ys)"
+ assumes unit: "\<And>x. P {x}\<sharp>"
+ assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
shows "P (xs::'a upper_pd)"
apply (induct xs rule: upper_principal_induct, rule P)
apply (induct_tac t rule: pd_basis_induct)
@@ -403,9 +402,10 @@
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
"upper_bind_basis = fold_pd
(\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
- (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+ (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
-lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_upper_bind:
+ "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)
@@ -416,11 +416,11 @@
"upper_bind_basis (PDUnit a) =
(\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
"upper_bind_basis (PDPlus t u) =
- (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
+ (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
unfolding upper_bind_basis_def
apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
+apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
+apply (rule fold_pd_PDPlus [OF ACI_upper_bind])
done
lemma upper_bind_basis_mono:
@@ -444,12 +444,11 @@
done
lemma upper_bind_unit [simp]:
- "upper_bind\<cdot>(upper_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+ "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x"
by (induct x rule: compact_basis_induct, simp, simp)
lemma upper_bind_plus [simp]:
- "upper_bind\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>f =
- upper_plus\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>(upper_bind\<cdot>ys\<cdot>f)"
+ "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -460,28 +459,26 @@
definition
upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
- "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_unit\<cdot>(f\<cdot>x)))"
+ "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
definition
upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
"upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
lemma upper_map_unit [simp]:
- "upper_map\<cdot>f\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(f\<cdot>x)"
+ "upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>"
unfolding upper_map_def by simp
lemma upper_map_plus [simp]:
- "upper_map\<cdot>f\<cdot>(upper_plus\<cdot>xs\<cdot>ys) =
- upper_plus\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>(upper_map\<cdot>f\<cdot>ys)"
+ "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
unfolding upper_map_def by simp
lemma upper_join_unit [simp]:
- "upper_join\<cdot>(upper_unit\<cdot>xs) = xs"
+ "upper_join\<cdot>{xs}\<sharp> = xs"
unfolding upper_join_def by simp
lemma upper_join_plus [simp]:
- "upper_join\<cdot>(upper_plus\<cdot>xss\<cdot>yss) =
- upper_plus\<cdot>(upper_join\<cdot>xss)\<cdot>(upper_join\<cdot>yss)"
+ "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
unfolding upper_join_def by simp
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"