src/HOLCF/CompactBasis.thy

domain package: simplify internal proofs of con_rews

(*  Title:      HOLCF/CompactBasis.thy
    Author:     Brian Huffman
*)

header {* Compact bases of domains *}

theory CompactBasis
imports Completion
begin

subsection {* Compact bases of bifinite domains *}

defaultsort 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) sq_ord
begin

definition
  compact_le_def:
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"

instance ..

end

instance compact_basis :: (profinite) po
by (rule typedef_po
    [OF type_definition_compact_basis compact_le_def])

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 sq_le 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_less)
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 sq_le compact_take Rep_compact_basis approximants
proof
  fix w :: 'a
  show "preorder.ideal sq_le (approximants w)"
  proof (rule sq_le.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_less)
      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_less)
      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) trans_less)
      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 trans_less, 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_less)
    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


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 (simp add: PDUnit_def)
apply (drule_tac a=x in PDPlus)
apply (simp add: PDUnit_def PDPlus_def 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 "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 "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 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))"

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)
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 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 antisym_less)
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