src/HOLCF/CompactBasis.thy
 author haftmann Tue, 04 May 2010 08:55:43 +0200 changeset 36635 080b755377c0 parent 36452 d37c6eed8117 child 39967 1c6dce3ef477 permissions -rw-r--r--
locale predicates of classes carry a mandatory "class" prefix
```
(*  Title:      HOLCF/CompactBasis.thy
Author:     Brian Huffman
*)

header {* Compact bases of domains *}

theory CompactBasis
imports Completion
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
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

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
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 (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 (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)
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 (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 (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 (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
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

subsection {* A compact basis for powerdomains *}

typedef 'a pd_basis =
"{S::'a::profinite 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)"
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp

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

definition
PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
"PDUnit = (\<lambda>x. Abs_pd_basis {x})"

definition
PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
"PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"

lemma Rep_PDUnit:
"Rep_pd_basis (PDUnit x) = {x}"
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)

lemma Rep_PDPlus:
"Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)

lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp

lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)

lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)

lemma PDPlus_absorb: "PDPlus t t = t"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)

lemma pd_basis_induct1:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
shows "P x"
apply (induct x, unfold pd_basis_def, clarify)
apply (erule (1) finite_ne_induct)
apply (cut_tac a=x in PDUnit)
apply (drule_tac a=x in PDPlus)
Abs_pd_basis_inverse [unfolded pd_basis_def])
done

lemma pd_basis_induct:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
shows "P x"
apply (induct x rule: pd_basis_induct1)
apply (rule PDUnit, erule PDPlus [OF PDUnit])
done

text {* fold-pd *}

definition
fold_pd ::
"('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 fold_pd_PDUnit:
assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDUnit x) = g x"
unfolding fold_pd_def Rep_PDUnit by simp

lemma fold_pd_PDPlus:
assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
interpret ab_semigroup_idem_mult f by fact
show ?thesis unfolding fold_pd_def Rep_PDPlus
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))"

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)
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_take Rep_PDUnit Rep_PDPlus image_Un)
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
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 (rule inj_onI, simp add: Rep_pd_basis_inject)
done

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

end
```