--- a/src/HOLCF/CompactBasis.thy Tue Oct 05 17:53:00 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy Wed Oct 06 10:49:27 2010 -0700
@@ -2,174 +2,18 @@
Author: Brian Huffman
*)
-header {* Compact bases of domains *}
+header {* A compact basis for powerdomains *}
theory CompactBasis
-imports Completion Bifinite
-begin
-
-subsection {* Compact bases of bifinite domains *}
-
-default_sort profinite
-
-typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
-by (fast intro: compact_approx)
-
-lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
-by (rule Rep_compact_basis [unfolded mem_Collect_eq])
-
-instantiation compact_basis :: (profinite) below
+imports Algebraic
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])
-
-text {* Take function for compact basis *}
-
-definition
- compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
- "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
-
-lemma Rep_compact_take:
- "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
-unfolding compact_take_def
-by (simp add: Abs_compact_basis_inverse)
-
-lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
-
-interpretation compact_basis:
- basis_take below compact_take
-proof
- fix n :: nat and a :: "'a compact_basis"
- show "compact_take n a \<sqsubseteq> a"
- unfolding compact_le_def
- by (simp add: Rep_compact_take approx_below)
-next
- fix n :: nat and a :: "'a compact_basis"
- show "compact_take n (compact_take n a) = compact_take n a"
- by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
-next
- fix n :: nat and a b :: "'a compact_basis"
- assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
- unfolding compact_le_def Rep_compact_take
- by (rule monofun_cfun_arg)
-next
- fix n :: nat and a :: "'a compact_basis"
- show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
- unfolding compact_le_def Rep_compact_take
- by (rule chainE, simp)
-next
- fix n :: nat
- show "finite (range (compact_take n))"
- apply (rule finite_imageD [where f="Rep_compact_basis"])
- apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
- apply (clarsimp simp add: Rep_compact_take)
- apply (rule finite_range_approx)
- apply (rule inj_onI, simp add: Rep_compact_basis_inject)
- done
-next
- fix a :: "'a compact_basis"
- show "\<exists>n. compact_take n a = a"
- apply (simp add: Rep_compact_basis_inject [symmetric])
- apply (simp add: Rep_compact_take)
- apply (rule profinite_compact_eq_approx)
- apply (rule compact_Rep_compact_basis)
- done
-qed
-
-text {* Ideal completion *}
-
-definition
- approximants :: "'a \<Rightarrow> 'a compact_basis set" where
- "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
-
-interpretation compact_basis:
- ideal_completion below compact_take Rep_compact_basis approximants
-proof
- fix w :: 'a
- show "preorder.ideal below (approximants w)"
- proof (rule below.idealI)
- show "\<exists>x. x \<in> approximants w"
- unfolding approximants_def
- apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
- apply (simp add: Abs_compact_basis_inverse approx_below)
- done
- next
- fix x y :: "'a compact_basis"
- assume "x \<in> approximants w" "y \<in> approximants w"
- thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
- unfolding approximants_def
- apply simp
- apply (cut_tac a=x in compact_Rep_compact_basis)
- apply (cut_tac a=y in compact_Rep_compact_basis)
- apply (drule profinite_compact_eq_approx)
- apply (drule profinite_compact_eq_approx)
- apply (clarify, rename_tac i j)
- apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
- apply (simp add: compact_le_def)
- apply (simp add: Abs_compact_basis_inverse approx_below)
- apply (erule subst, erule subst)
- apply (simp add: monofun_cfun chain_mono [OF chain_approx])
- done
- next
- fix x y :: "'a compact_basis"
- assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
- unfolding approximants_def
- apply simp
- apply (simp add: compact_le_def)
- apply (erule (1) below_trans)
- done
- qed
-next
- fix Y :: "nat \<Rightarrow> 'a"
- assume Y: "chain Y"
- show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
- unfolding approximants_def
- apply safe
- apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
- apply (erule below_trans, rule is_ub_thelub [OF Y])
- done
-next
- fix a :: "'a compact_basis"
- show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
- unfolding approximants_def compact_le_def ..
-next
- fix x y :: "'a"
- assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
- apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
- apply (rule admD, simp, simp)
- apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
- apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
- apply (simp add: approximants_def Abs_compact_basis_inverse)
- done
-qed
-
-text {* minimal compact element *}
-
-definition
- compact_bot :: "'a::bifinite compact_basis" where
- "compact_bot = Abs_compact_basis \<bottom>"
-
-lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
-unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
-
-lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
-unfolding compact_le_def Rep_compact_bot by simp
-
+default_sort sfp
subsection {* A compact basis for powerdomains *}
typedef 'a pd_basis =
- "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
+ "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
by (rule_tac x="{arbitrary}" in exI, simp)
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
@@ -178,7 +22,21 @@
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
-text {* unit and plus *}
+text {* The powerdomain basis type is countable. *}
+
+lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
+proof -
+ obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
+ using compact_basis.countable ..
+ hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
+ by (rule inj_image_eq_iff)
+ have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
+ by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
+ thus ?thesis by - (rule exI)
+ (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
+qed
+
+subsection {* Unit and plus constructors *}
definition
PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
@@ -229,7 +87,7 @@
apply (rule PDUnit, erule PDPlus [OF PDUnit])
done
-text {* fold-pd *}
+subsection {* Fold operator *}
definition
fold_pd ::
@@ -250,52 +108,26 @@
by (simp add: image_Un fold1_Un2)
qed
-text {* Take function for powerdomain basis *}
-
-definition
- pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
- "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
+subsection {* Lemmas for proving if-and-only-if inequalities *}
-lemma Rep_pd_take:
- "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
-unfolding pd_take_def
-apply (rule Abs_pd_basis_inverse)
-apply (simp add: pd_basis_def)
-done
-
-lemma pd_take_simps [simp]:
- "pd_take n (PDUnit a) = PDUnit (compact_take n a)"
- "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
-apply (simp_all add: Rep_pd_basis_inject [symmetric])
-apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
+lemma chain_max_below_iff:
+ assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x"
+apply auto
+apply (erule below_trans [OF chain_mono [OF Y le_maxI1]])
+apply (erule below_trans [OF chain_mono [OF Y le_maxI2]])
+apply (simp add: max_def)
done
-lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
-apply (induct t rule: pd_basis_induct)
-apply (simp add: compact_basis.take_take)
-apply simp
-done
-
-lemma finite_range_pd_take: "finite (range (pd_take n))"
-apply (rule finite_imageD [where f="Rep_pd_basis"])
-apply (rule finite_subset [where B="Pow (range (compact_take n))"])
-apply (clarsimp simp add: Rep_pd_take)
-apply (simp add: compact_basis.finite_range_take)
-apply (rule inj_onI, simp add: Rep_pd_basis_inject)
-done
+lemma all_ex_below_disj_iff:
+ assumes "chain X" and "chain Y"
+ shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
+ (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
+by (metis chain_max_below_iff assms)
-lemma pd_take_covers: "\<exists>n. pd_take n t = t"
-apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
-apply (induct t rule: pd_basis_induct)
-apply (cut_tac a=a in compact_basis.take_covers)
-apply (clarify, rule_tac x=n in exI)
-apply (clarify, simp)
-apply (rule below_antisym)
-apply (rule compact_basis.take_less)
-apply (drule_tac a=a in compact_basis.take_chain_le)
-apply simp
-apply (clarify, rename_tac i j)
-apply (rule_tac x="max i j" in exI, simp)
-done
+lemma all_ex_below_conj_iff:
+ assumes "chain X" and "chain Y" and "chain Z"
+ shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
+ (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
+oops
end