src/HOLCF/CompactBasis.thy
 author huffman Tue Oct 12 06:20:05 2010 -0700 (2010-10-12) changeset 40006 116e94f9543b parent 39986 38677db30cad child 40497 d2e876d6da8c permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
1 (*  Title:      HOLCF/CompactBasis.thy
2     Author:     Brian Huffman
3 *)
5 header {* A compact basis for powerdomains *}
7 theory CompactBasis
8 imports Bifinite
9 begin
11 default_sort bifinite
13 subsection {* A compact basis for powerdomains *}
15 typedef 'a pd_basis =
16   "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
17 by (rule_tac x="{arbitrary}" in exI, simp)
19 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
20 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
22 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
23 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
25 text {* The powerdomain basis type is countable. *}
27 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
28 proof -
29   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
30     using compact_basis.countable ..
31   hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
32     by (rule inj_image_eq_iff)
33   have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
34     by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
35   thus ?thesis by - (rule exI)
36   (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
37 qed
39 subsection {* Unit and plus constructors *}
41 definition
42   PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
43   "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
45 definition
46   PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
47   "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
49 lemma Rep_PDUnit:
50   "Rep_pd_basis (PDUnit x) = {x}"
51 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
53 lemma Rep_PDPlus:
54   "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
55 unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
57 lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
58 unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
60 lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
61 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
63 lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
64 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
66 lemma PDPlus_absorb: "PDPlus t t = t"
67 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
69 lemma pd_basis_induct1:
70   assumes PDUnit: "\<And>a. P (PDUnit a)"
71   assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
72   shows "P x"
73 apply (induct x, unfold pd_basis_def, clarify)
74 apply (erule (1) finite_ne_induct)
75 apply (cut_tac a=x in PDUnit)
76 apply (simp add: PDUnit_def)
77 apply (drule_tac a=x in PDPlus)
78 apply (simp add: PDUnit_def PDPlus_def
79   Abs_pd_basis_inverse [unfolded pd_basis_def])
80 done
82 lemma pd_basis_induct:
83   assumes PDUnit: "\<And>a. P (PDUnit a)"
84   assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
85   shows "P x"
86 apply (induct x rule: pd_basis_induct1)
87 apply (rule PDUnit, erule PDPlus [OF PDUnit])
88 done
90 subsection {* Fold operator *}
92 definition
93   fold_pd ::
94     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
95   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
97 lemma fold_pd_PDUnit:
98   assumes "class.ab_semigroup_idem_mult f"
99   shows "fold_pd g f (PDUnit x) = g x"
100 unfolding fold_pd_def Rep_PDUnit by simp
102 lemma fold_pd_PDPlus:
103   assumes "class.ab_semigroup_idem_mult f"
104   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
105 proof -
106   interpret ab_semigroup_idem_mult f by fact
107   show ?thesis unfolding fold_pd_def Rep_PDPlus
108     by (simp add: image_Un fold1_Un2)
109 qed
111 end