src/HOL/HOLCF/CompactBasis.thy
changeset 40774 0437dbc127b3
parent 40497 d2e876d6da8c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/CompactBasis.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,111 @@
     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