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