Theory Compact_Basis

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

section ‹A compact basis for powerdomains›

theory Compact_Basis
imports Universal
begin

subsection ‹A compact basis for powerdomains›

definition "pd_basis = {S::'a::bifinite compact_basis set. finite S ∧ S ≠ {}}"

typedef 'a::bifinite pd_basis = "pd_basis :: 'a compact_basis set set"
proof
  show "{a} ∈ ?pd_basis" for a
    by (simp add: pd_basis_def)
qed

lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
using Rep_pd_basis [of u, unfolded pd_basis_def] by simp

lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u ≠ {}"
using Rep_pd_basis [of u, unfolded pd_basis_def] by simp

text ‹The powerdomain basis type is countable.›

lemma pd_basis_countable: "∃f::'a::bifinite pd_basis ⇒ nat. inj f" (is "Ex ?P")
proof -
  obtain g :: "'a compact_basis ⇒ nat" where "inj g"
    using compact_basis.countable ..
  hence image_g_eq: "g ` A = g ` B ⟷ A = B" for A B
    by (rule inj_image_eq_iff)
  have "inj (λ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 [of ?P])
qed


subsection ‹Unit and plus constructors›

definition
  PDUnit :: "'a::bifinite compact_basis ⇒ 'a pd_basis" where
  "PDUnit = (λx. Abs_pd_basis {x})"

definition
  PDPlus :: "'a::bifinite pd_basis ⇒ 'a pd_basis ⇒ 'a pd_basis" where
  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t ∪ 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 ∪ 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 [case_names PDUnit PDPlus]:
  assumes PDUnit: "⋀a. P (PDUnit a)"
  assumes PDPlus: "⋀a t. P t ⟹ P (PDPlus (PDUnit a) t)"
  shows "P x"
proof (induct x)
  case (Abs_pd_basis y)
  then have "finite y" and "y ≠ {}" by (simp_all add: pd_basis_def)
  then show ?case
  proof (induct rule: finite_ne_induct)
    case (singleton x)
    show ?case by (rule PDUnit [unfolded PDUnit_def])
  next
    case (insert x F)
    from insert(4) have "P (PDPlus (PDUnit x) (Abs_pd_basis F))" by (rule PDPlus)
    with insert(1,2) show ?case
      by (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
  qed
qed

lemma pd_basis_induct [case_names PDUnit PDPlus]:
  assumes PDUnit: "⋀a. P (PDUnit a)"
  assumes PDPlus: "⋀t u. ⟦P t; P u⟧ ⟹ P (PDPlus t u)"
  shows "P x"
  by (induct x rule: pd_basis_induct1) (fact PDUnit, fact PDPlus [OF PDUnit])


subsection ‹Fold operator›

definition
  fold_pd ::
    "('a::bifinite compact_basis ⇒ 'b::type) ⇒ ('b ⇒ 'b ⇒ 'b) ⇒ 'a pd_basis ⇒ 'b"
  where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)"

lemma fold_pd_PDUnit:
  assumes "semilattice f"
  shows "fold_pd g f (PDUnit x) = g x"
proof -
  from assms interpret semilattice_set f by (rule semilattice_set.intro)
  show ?thesis by (simp add: fold_pd_def Rep_PDUnit)
qed

lemma fold_pd_PDPlus:
  assumes "semilattice f"
  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
  from assms interpret semilattice_set f by (rule semilattice_set.intro)
  show ?thesis by (simp add: image_Un fold_pd_def Rep_PDPlus union)
qed

end