src/HOLCF/CompactBasis.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/CompactBasis.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,111 +0,0 @@
     1.4 -(*  Title:      HOLCF/CompactBasis.thy
     1.5 -    Author:     Brian Huffman
     1.6 -*)
     1.7 -
     1.8 -header {* A compact basis for powerdomains *}
     1.9 -
    1.10 -theory CompactBasis
    1.11 -imports Bifinite
    1.12 -begin
    1.13 -
    1.14 -default_sort "domain"
    1.15 -
    1.16 -subsection {* A compact basis for powerdomains *}
    1.17 -
    1.18 -typedef 'a pd_basis =
    1.19 -  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
    1.20 -by (rule_tac x="{arbitrary}" in exI, simp)
    1.21 -
    1.22 -lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
    1.23 -by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
    1.24 -
    1.25 -lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
    1.26 -by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
    1.27 -
    1.28 -text {* The powerdomain basis type is countable. *}
    1.29 -
    1.30 -lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
    1.31 -proof -
    1.32 -  obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
    1.33 -    using compact_basis.countable ..
    1.34 -  hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
    1.35 -    by (rule inj_image_eq_iff)
    1.36 -  have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
    1.37 -    by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
    1.38 -  thus ?thesis by - (rule exI)
    1.39 -  (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
    1.40 -qed
    1.41 -
    1.42 -subsection {* Unit and plus constructors *}
    1.43 -
    1.44 -definition
    1.45 -  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
    1.46 -  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
    1.47 -
    1.48 -definition
    1.49 -  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
    1.50 -  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
    1.51 -
    1.52 -lemma Rep_PDUnit:
    1.53 -  "Rep_pd_basis (PDUnit x) = {x}"
    1.54 -unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
    1.55 -
    1.56 -lemma Rep_PDPlus:
    1.57 -  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
    1.58 -unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
    1.59 -
    1.60 -lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
    1.61 -unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
    1.62 -
    1.63 -lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
    1.64 -unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
    1.65 -
    1.66 -lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
    1.67 -unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
    1.68 -
    1.69 -lemma PDPlus_absorb: "PDPlus t t = t"
    1.70 -unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
    1.71 -
    1.72 -lemma pd_basis_induct1:
    1.73 -  assumes PDUnit: "\<And>a. P (PDUnit a)"
    1.74 -  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
    1.75 -  shows "P x"
    1.76 -apply (induct x, unfold pd_basis_def, clarify)
    1.77 -apply (erule (1) finite_ne_induct)
    1.78 -apply (cut_tac a=x in PDUnit)
    1.79 -apply (simp add: PDUnit_def)
    1.80 -apply (drule_tac a=x in PDPlus)
    1.81 -apply (simp add: PDUnit_def PDPlus_def
    1.82 -  Abs_pd_basis_inverse [unfolded pd_basis_def])
    1.83 -done
    1.84 -
    1.85 -lemma pd_basis_induct:
    1.86 -  assumes PDUnit: "\<And>a. P (PDUnit a)"
    1.87 -  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
    1.88 -  shows "P x"
    1.89 -apply (induct x rule: pd_basis_induct1)
    1.90 -apply (rule PDUnit, erule PDPlus [OF PDUnit])
    1.91 -done
    1.92 -
    1.93 -subsection {* Fold operator *}
    1.94 -
    1.95 -definition
    1.96 -  fold_pd ::
    1.97 -    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
    1.98 -  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
    1.99 -
   1.100 -lemma fold_pd_PDUnit:
   1.101 -  assumes "class.ab_semigroup_idem_mult f"
   1.102 -  shows "fold_pd g f (PDUnit x) = g x"
   1.103 -unfolding fold_pd_def Rep_PDUnit by simp
   1.104 -
   1.105 -lemma fold_pd_PDPlus:
   1.106 -  assumes "class.ab_semigroup_idem_mult f"
   1.107 -  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   1.108 -proof -
   1.109 -  interpret ab_semigroup_idem_mult f by fact
   1.110 -  show ?thesis unfolding fold_pd_def Rep_PDPlus
   1.111 -    by (simp add: image_Un fold1_Un2)
   1.112 -qed
   1.113 -
   1.114 -end