src/HOL/HOLCF/Compact_Basis.thy
 changeset 41284 6d66975b711f parent 40774 0437dbc127b3 child 41285 efd23c1d9886
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Fri Dec 17 16:43:45 2010 -0800
1.3 @@ -0,0 +1,111 @@
1.4 +(*  Title:      HOLCF/Compact_Basis.thy
1.5 +    Author:     Brian Huffman
1.6 +*)
1.7 +
1.8 +header {* A compact basis for powerdomains *}
1.9 +
1.10 +theory Compact_Basis
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.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
```