2 (* Author: Florian Haftmann, TU Muenchen *)
4 header {* A dedicated set type which is executable on its finite part *}
7 imports More_Set More_List
10 subsection {* Lifting *}
12 typedef (open) 'a set = "UNIV :: 'a set set"
13 morphisms member Set by rule+
16 lemma member_Set [simp]:
18 by (rule Set_inverse) rule
20 lemma Set_member [simp]:
22 by (fact member_inverse)
24 lemma Set_inject [simp]:
25 "Set A = Set B \<longleftrightarrow> A = B"
26 by (simp add: Set_inject)
29 "A = B \<longleftrightarrow> member A = member B"
30 by (simp add: member_inject)
31 hide_fact (open) set_eq_iff
34 "member A = member B \<Longrightarrow> A = B"
35 by (simp add: Cset.set_eq_iff)
36 hide_fact (open) set_eqI
38 subsection {* Lattice instantiation *}
40 instantiation Cset.set :: (type) boolean_algebra
43 definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
44 [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
46 definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
47 [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
49 definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
50 [simp]: "inf A B = Set (member A \<inter> member B)"
52 definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
53 [simp]: "sup A B = Set (member A \<union> member B)"
55 definition bot_set :: "'a Cset.set" where
56 [simp]: "bot = Set {}"
58 definition top_set :: "'a Cset.set" where
59 [simp]: "top = Set UNIV"
61 definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
62 [simp]: "- A = Set (- (member A))"
64 definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
65 [simp]: "A - B = Set (member A - member B)"
68 qed (auto intro: Cset.set_eqI)
72 instantiation Cset.set :: (type) complete_lattice
75 definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
76 [simp]: "Inf_set As = Set (Inf (image member As))"
78 definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
79 [simp]: "Sup_set As = Set (Sup (image member As))"
82 qed (auto simp add: le_fun_def le_bool_def)
87 subsection {* Basic operations *}
89 abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
90 hide_const (open) empty
92 abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
93 hide_const (open) UNIV
95 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
96 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
98 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
99 [simp]: "insert x A = Set (Set.insert x (member A))"
101 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
102 [simp]: "remove x A = Set (More_Set.remove x (member A))"
104 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
105 [simp]: "map f A = Set (image f (member A))"
107 enriched_type map: map
108 by (simp_all add: fun_eq_iff image_compose)
110 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
111 [simp]: "filter P A = Set (More_Set.project P (member A))"
113 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
114 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
116 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
117 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
119 definition card :: "'a Cset.set \<Rightarrow> nat" where
120 [simp]: "card A = Finite_Set.card (member A)"
122 context complete_lattice
125 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
126 [simp]: "Infimum A = Inf (member A)"
128 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
129 [simp]: "Supremum A = Sup (member A)"
133 subsection {* More operations *}
135 text {* conversion from @{typ "'a list"} *}
137 definition set :: "'a list \<Rightarrow> 'a Cset.set" where
138 "set xs = Set (List.set xs)"
139 hide_const (open) set
141 text {* conversion from @{typ "'a Predicate.pred"} *}
143 definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
144 where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
146 definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
147 where "of_pred = Cset.Set \<circ> Predicate.eval"
149 definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
150 where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
152 text {* monad operations *}
154 definition single :: "'a \<Rightarrow> 'a Cset.set" where
157 definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
158 (infixl "\<guillemotright>=" 70)
159 where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
161 subsection {* Simplified simprules *}
163 lemma empty_simp [simp]: "member Cset.empty = {}"
166 lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
169 lemma is_empty_simp [simp]:
170 "is_empty A \<longleftrightarrow> member A = {}"
171 by (simp add: More_Set.is_empty_def)
172 declare is_empty_def [simp del]
174 lemma remove_simp [simp]:
175 "remove x A = Set (member A - {x})"
176 by (simp add: More_Set.remove_def)
177 declare remove_def [simp del]
179 lemma filter_simp [simp]:
180 "filter P A = Set {x \<in> member A. P x}"
181 by (simp add: More_Set.project_def)
182 declare filter_def [simp del]
184 lemma member_set [simp]:
185 "member (Cset.set xs) = set xs"
186 by (simp add: set_def)
187 hide_fact (open) member_set set_def
189 lemma set_simps [simp]:
190 "Cset.set [] = Cset.empty"
191 "Cset.set (x # xs) = insert x (Cset.set xs)"
192 by(simp_all add: Cset.set_def)
194 lemma member_SUPR [simp]:
195 "member (SUPR A f) = SUPR A (member \<circ> f)"
196 unfolding SUPR_def by simp
198 lemma member_bind [simp]:
199 "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
200 by (simp add: bind_def Cset.set_eq_iff)
202 lemma member_single [simp]:
203 "member (single a) = {a}"
204 by(simp add: single_def)
206 lemma single_sup_simps [simp]:
207 shows single_sup: "sup (single a) A = insert a A"
208 and sup_single: "sup A (single a) = insert a A"
209 by(auto simp add: Cset.set_eq_iff)
211 lemma single_bind [simp]:
212 "single a \<guillemotright>= B = B a"
213 by(simp add: bind_def single_def)
216 "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
217 by(simp add: bind_def)
219 lemma bind_single [simp]:
220 "A \<guillemotright>= single = A"
221 by(simp add: bind_def single_def)
223 lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
224 by(auto simp add: Cset.set_eq_iff)
226 lemma empty_bind [simp]:
227 "Cset.empty \<guillemotright>= f = Cset.empty"
228 by(simp add: Cset.set_eq_iff)
230 lemma member_of_pred [simp]:
231 "member (of_pred P) = {x. Predicate.eval P x}"
232 by(simp add: of_pred_def Collect_def)
234 lemma member_of_seq [simp]:
235 "member (of_seq xq) = {x. Predicate.member xq x}"
236 by(simp add: of_seq_def eval_member)
238 lemma eval_pred_of_cset [simp]:
239 "Predicate.eval (pred_of_cset A) = Cset.member A"
240 by(simp add: pred_of_cset_def)
242 subsection {* Default implementations *}
244 lemma set_code [code]:
245 "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
246 proof(rule ext, rule Cset.set_eqI)
248 show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
249 by(induct xs rule: rev_induct)(simp_all)
252 lemma single_code [code]:
253 "single a = insert a Cset.empty"
254 by(simp add: Cset.single_def)
256 lemma of_pred_code [code]:
257 "of_pred (Predicate.Seq f) = (case f () of
258 Predicate.Empty \<Rightarrow> Cset.empty
259 | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
260 | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
261 by(auto split: seq.split
262 simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
264 lemma of_seq_code [code]:
265 "of_seq Predicate.Empty = Cset.empty"
266 "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
267 "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
268 by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
270 declare mem_def [simp del]
272 no_notation bind (infixl "\<guillemotright>=" 70)
274 hide_const (open) is_empty insert remove map filter forall exists card
275 Inter Union bind single of_pred of_seq
277 hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def
278 bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind
279 member_single single_sup_simps single_sup sup_single single_bind
280 bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
281 eval_pred_of_cset set_code single_code of_pred_code of_seq_code