1(* Title: HOL/HOLCF/Compact_Basis.thy 2 Author: Brian Huffman 3*) 4 5section \<open>A compact basis for powerdomains\<close> 6 7theory Compact_Basis 8imports Universal 9begin 10 11default_sort bifinite 12 13subsection \<open>A compact basis for powerdomains\<close> 14 15definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" 16 17typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" 18 unfolding pd_basis_def 19 apply (rule_tac x="{_}" in exI) 20 apply simp 21 done 22 23lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" 24by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp 25 26lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" 27by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp 28 29text \<open>The powerdomain basis type is countable.\<close> 30 31lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f" 32proof - 33 obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" 34 using compact_basis.countable .. 35 hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" 36 by (rule inj_image_eq_iff) 37 have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))" 38 by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject) 39 thus ?thesis by - (rule exI) 40 (* FIXME: why doesn't ".." or "by (rule exI)" work? *) 41qed 42 43subsection \<open>Unit and plus constructors\<close> 44 45definition 46 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where 47 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" 48 49definition 50 PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where 51 "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" 52 53lemma Rep_PDUnit: 54 "Rep_pd_basis (PDUnit x) = {x}" 55unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) 56 57lemma Rep_PDPlus: 58 "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v" 59unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) 60 61lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)" 62unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp 63 64lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)" 65unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc) 66 67lemma PDPlus_commute: "PDPlus t u = PDPlus u t" 68unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute) 69 70lemma PDPlus_absorb: "PDPlus t t = t" 71unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb) 72 73lemma pd_basis_induct1: 74 assumes PDUnit: "\<And>a. P (PDUnit a)" 75 assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)" 76 shows "P x" 77apply (induct x, unfold pd_basis_def, clarify) 78apply (erule (1) finite_ne_induct) 79apply (cut_tac a=x in PDUnit) 80apply (simp add: PDUnit_def) 81apply (drule_tac a=x in PDPlus) 82apply (simp add: PDUnit_def PDPlus_def 83 Abs_pd_basis_inverse [unfolded pd_basis_def]) 84done 85 86lemma pd_basis_induct: 87 assumes PDUnit: "\<And>a. P (PDUnit a)" 88 assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)" 89 shows "P x" 90apply (induct x rule: pd_basis_induct1) 91apply (rule PDUnit, erule PDPlus [OF PDUnit]) 92done 93 94subsection \<open>Fold operator\<close> 95 96definition 97 fold_pd :: 98 "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" 99 where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)" 100 101lemma fold_pd_PDUnit: 102 assumes "semilattice f" 103 shows "fold_pd g f (PDUnit x) = g x" 104proof - 105 from assms interpret semilattice_set f by (rule semilattice_set.intro) 106 show ?thesis by (simp add: fold_pd_def Rep_PDUnit) 107qed 108 109lemma fold_pd_PDPlus: 110 assumes "semilattice f" 111 shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" 112proof - 113 from assms interpret semilattice_set f by (rule semilattice_set.intro) 114 show ?thesis by (simp add: image_Un fold_pd_def Rep_PDPlus union) 115qed 116 117end 118 119