diff -r c62b4ff97bfc -r b525988432e9 src/HOLCF/CompactBasis.thy
--- 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