author | haftmann |
Fri, 09 May 2014 08:13:26 +0200 | |
changeset 56920 | d651b944c67e |
parent 55887 | 25bd4745ee38 |
child 58806 | bb5ab5fce93a |
permissions | -rw-r--r-- |
51599 | 1 |
(* Title: HOL/Library/DAList_Multiset.thy |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Multisets partially implemented by association lists *} |
|
6 |
||
7 |
theory DAList_Multiset |
|
8 |
imports Multiset DAList |
|
9 |
begin |
|
10 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
11 |
text {* Delete prexisting code equations *} |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
12 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
13 |
lemma [code, code del]: |
51623 | 14 |
"{#} = {#}" |
15 |
.. |
|
16 |
||
17 |
lemma [code, code del]: |
|
18 |
"single = single" |
|
19 |
.. |
|
20 |
||
21 |
lemma [code, code del]: |
|
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
22 |
"plus = (plus :: 'a multiset \<Rightarrow> _)" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
23 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
24 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
25 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
26 |
"minus = (minus :: 'a multiset \<Rightarrow> _)" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
27 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
28 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
29 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
30 |
"inf = (inf :: 'a multiset \<Rightarrow> _)" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
31 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
32 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
33 |
lemma [code, code del]: |
51623 | 34 |
"sup = (sup :: 'a multiset \<Rightarrow> _)" |
35 |
.. |
|
36 |
||
37 |
lemma [code, code del]: |
|
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
38 |
"image_mset = image_mset" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
39 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
40 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
41 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
42 |
"Multiset.filter = Multiset.filter" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
43 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
44 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
45 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
46 |
"count = count" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
47 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
48 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
49 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
50 |
"mcard = mcard" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
51 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
52 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
53 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
54 |
"msetsum = msetsum" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
55 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
56 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
57 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
58 |
"msetprod = msetprod" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
59 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
60 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
61 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
62 |
"set_of = set_of" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
63 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
64 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
65 |
lemma [code, code del]: |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
66 |
"sorted_list_of_multiset = sorted_list_of_multiset" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
67 |
.. |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
68 |
|
55808
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
69 |
lemma [code, code del]: |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
70 |
"ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset" |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
71 |
.. |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
72 |
|
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
73 |
lemma [code, code del]: |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
74 |
"ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset" |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
75 |
.. |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
76 |
|
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
77 |
lemma [code, code del]: |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
78 |
"equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
79 |
.. |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
80 |
|
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
81 |
|
51599 | 82 |
text {* Raw operations on lists *} |
83 |
||
84 |
definition join_raw :: "('key \<Rightarrow> 'val \<times> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" |
|
85 |
where |
|
86 |
"join_raw f xs ys = foldr (\<lambda>(k, v). map_default k v (%v'. f k (v', v))) ys xs" |
|
87 |
||
88 |
lemma join_raw_Nil [simp]: |
|
89 |
"join_raw f xs [] = xs" |
|
90 |
by (simp add: join_raw_def) |
|
91 |
||
92 |
lemma join_raw_Cons [simp]: |
|
93 |
"join_raw f xs ((k, v) # ys) = map_default k v (%v'. f k (v', v)) (join_raw f xs ys)" |
|
94 |
by (simp add: join_raw_def) |
|
95 |
||
96 |
lemma map_of_join_raw: |
|
97 |
assumes "distinct (map fst ys)" |
|
98 |
shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v => |
|
99 |
(case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))" |
|
100 |
using assms |
|
101 |
apply (induct ys) |
|
102 |
apply (auto simp add: map_of_map_default split: option.split) |
|
103 |
apply (metis map_of_eq_None_iff option.simps(2) weak_map_of_SomeI) |
|
104 |
by (metis Some_eq_map_of_iff map_of_eq_None_iff option.simps(2)) |
|
105 |
||
106 |
lemma distinct_join_raw: |
|
107 |
assumes "distinct (map fst xs)" |
|
108 |
shows "distinct (map fst (join_raw f xs ys))" |
|
109 |
using assms |
|
110 |
proof (induct ys) |
|
111 |
case (Cons y ys) |
|
112 |
thus ?case by (cases y) (simp add: distinct_map_default) |
|
113 |
qed auto |
|
114 |
||
115 |
definition |
|
116 |
"subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs" |
|
117 |
||
118 |
lemma map_of_subtract_entries_raw: |
|
119 |
assumes "distinct (map fst ys)" |
|
120 |
shows "map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => |
|
121 |
(case map_of ys x of None => Some v | Some v' => Some (v - v')))" |
|
122 |
using assms unfolding subtract_entries_raw_def |
|
123 |
apply (induct ys) |
|
124 |
apply auto |
|
125 |
apply (simp split: option.split) |
|
126 |
apply (simp add: map_of_map_entry) |
|
127 |
apply (auto split: option.split) |
|
128 |
apply (metis map_of_eq_None_iff option.simps(3) option.simps(4)) |
|
129 |
by (metis map_of_eq_None_iff option.simps(4) option.simps(5)) |
|
130 |
||
131 |
lemma distinct_subtract_entries_raw: |
|
132 |
assumes "distinct (map fst xs)" |
|
133 |
shows "distinct (map fst (subtract_entries_raw xs ys))" |
|
134 |
using assms |
|
135 |
unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry) |
|
136 |
||
137 |
||
138 |
text {* Operations on alists with distinct keys *} |
|
139 |
||
140 |
lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" |
|
141 |
is join_raw |
|
142 |
by (simp add: distinct_join_raw) |
|
143 |
||
144 |
lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" |
|
145 |
is subtract_entries_raw |
|
146 |
by (simp add: distinct_subtract_entries_raw) |
|
147 |
||
148 |
||
149 |
text {* Implementing multisets by means of association lists *} |
|
150 |
||
151 |
definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat" where |
|
152 |
"count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)" |
|
153 |
||
154 |
lemma count_of_multiset: |
|
155 |
"count_of xs \<in> multiset" |
|
156 |
proof - |
|
157 |
let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)}" |
|
158 |
have "?A \<subseteq> dom (map_of xs)" |
|
159 |
proof |
|
160 |
fix x |
|
161 |
assume "x \<in> ?A" |
|
162 |
then have "0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)" by simp |
|
163 |
then have "map_of xs x \<noteq> None" by (cases "map_of xs x") auto |
|
164 |
then show "x \<in> dom (map_of xs)" by auto |
|
165 |
qed |
|
166 |
with finite_dom_map_of [of xs] have "finite ?A" |
|
167 |
by (auto intro: finite_subset) |
|
168 |
then show ?thesis |
|
169 |
by (simp add: count_of_def fun_eq_iff multiset_def) |
|
170 |
qed |
|
171 |
||
172 |
lemma count_simps [simp]: |
|
173 |
"count_of [] = (\<lambda>_. 0)" |
|
174 |
"count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)" |
|
175 |
by (simp_all add: count_of_def fun_eq_iff) |
|
176 |
||
177 |
lemma count_of_empty: |
|
178 |
"x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0" |
|
179 |
by (induct xs) (simp_all add: count_of_def) |
|
180 |
||
181 |
lemma count_of_filter: |
|
182 |
"count_of (List.filter (P \<circ> fst) xs) x = (if P x then count_of xs x else 0)" |
|
183 |
by (induct xs) auto |
|
184 |
||
185 |
lemma count_of_map_default [simp]: |
|
186 |
"count_of (map_default x b (%x. x + b) xs) y = (if x = y then count_of xs x + b else count_of xs y)" |
|
187 |
unfolding count_of_def by (simp add: map_of_map_default split: option.split) |
|
188 |
||
189 |
lemma count_of_join_raw: |
|
190 |
"distinct (map fst ys) ==> count_of xs x + count_of ys x = count_of (join_raw (%x (x, y). x + y) xs ys) x" |
|
191 |
unfolding count_of_def by (simp add: map_of_join_raw split: option.split) |
|
192 |
||
193 |
lemma count_of_subtract_entries_raw: |
|
194 |
"distinct (map fst ys) ==> count_of xs x - count_of ys x = count_of (subtract_entries_raw xs ys) x" |
|
195 |
unfolding count_of_def by (simp add: map_of_subtract_entries_raw split: option.split) |
|
196 |
||
197 |
||
198 |
text {* Code equations for multiset operations *} |
|
199 |
||
200 |
definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset" where |
|
201 |
"Bag xs = Abs_multiset (count_of (DAList.impl_of xs))" |
|
202 |
||
203 |
code_datatype Bag |
|
204 |
||
205 |
lemma count_Bag [simp, code]: |
|
206 |
"count (Bag xs) = count_of (DAList.impl_of xs)" |
|
207 |
by (simp add: Bag_def count_of_multiset Abs_multiset_inverse) |
|
208 |
||
209 |
lemma Mempty_Bag [code]: |
|
210 |
"{#} = Bag (DAList.empty)" |
|
211 |
by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def) |
|
212 |
||
213 |
lemma single_Bag [code]: |
|
214 |
"{#x#} = Bag (DAList.update x 1 DAList.empty)" |
|
215 |
by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq) |
|
216 |
||
217 |
lemma union_Bag [code]: |
|
218 |
"Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)" |
|
219 |
by (rule multiset_eqI) (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def) |
|
220 |
||
221 |
lemma minus_Bag [code]: |
|
222 |
"Bag xs - Bag ys = Bag (subtract_entries xs ys)" |
|
223 |
by (rule multiset_eqI) |
|
224 |
(simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def) |
|
225 |
||
226 |
lemma filter_Bag [code]: |
|
227 |
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)" |
|
228 |
by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq) |
|
229 |
||
55808
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
230 |
|
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
231 |
lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1" |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
232 |
by (metis equal_multiset_def eq_iff) |
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
51623
diff
changeset
|
233 |
|
55887 | 234 |
text{* By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}. |
235 |
With equality implemented by @{text"\<le>"}, this leads to three calls of @{text"\<le>"}. |
|
236 |
Here is a more efficient version: *} |
|
237 |
lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
238 |
by (rule less_le_not_le) |
|
239 |
||
240 |
lemma mset_less_eq_Bag0: |
|
51599 | 241 |
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)" |
242 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
243 |
proof |
|
55887 | 244 |
assume ?lhs thus ?rhs by (auto simp add: mset_le_def) |
51599 | 245 |
next |
246 |
assume ?rhs |
|
247 |
show ?lhs |
|
248 |
proof (rule mset_less_eqI) |
|
249 |
fix x |
|
250 |
from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x" |
|
251 |
by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty) |
|
55887 | 252 |
thus "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def) |
51599 | 253 |
qed |
254 |
qed |
|
255 |
||
55887 | 256 |
lemma mset_less_eq_Bag [code]: |
257 |
"Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)" |
|
258 |
proof - |
|
259 |
{ |
|
260 |
fix x n |
|
261 |
assume "(x,n) \<in> set (DAList.impl_of xs)" |
|
262 |
hence "count_of (DAList.impl_of xs) x = n" |
|
263 |
proof (transfer) |
|
264 |
fix x n and xs :: "('a \<times> nat) list" |
|
265 |
show "(distinct \<circ> map fst) xs \<Longrightarrow> (x, n) \<in> set xs \<Longrightarrow> count_of xs x = n" |
|
266 |
proof (induct xs) |
|
267 |
case (Cons ym ys) |
|
268 |
obtain y m where ym: "ym = (y,m)" by force |
|
269 |
note Cons = Cons[unfolded ym] |
|
270 |
show ?case |
|
271 |
proof (cases "x = y") |
|
272 |
case False |
|
273 |
with Cons show ?thesis unfolding ym by auto |
|
274 |
next |
|
275 |
case True |
|
276 |
with Cons(2-3) have "m = n" by force |
|
277 |
with True show ?thesis unfolding ym by auto |
|
278 |
qed |
|
279 |
qed auto |
|
280 |
qed |
|
281 |
} |
|
282 |
thus ?thesis unfolding mset_less_eq_Bag0 by auto |
|
283 |
qed |
|
284 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
285 |
declare multiset_inter_def [code] |
51623 | 286 |
declare sup_multiset_def [code] |
287 |
declare multiset_of.simps [code] |
|
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
288 |
|
55887 | 289 |
|
290 |
fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat)list \<Rightarrow> 'b" where |
|
291 |
"fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)" |
|
292 |
| "fold_impl fn e [] = e" |
|
293 |
||
294 |
definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat)alist \<Rightarrow> 'b" where |
|
295 |
"fold f e al = fold_impl f e (DAList.impl_of al)" |
|
296 |
||
297 |
hide_const (open) fold |
|
298 |
||
299 |
context comp_fun_commute |
|
300 |
begin |
|
301 |
||
302 |
lemma DAList_Multiset_fold: assumes fn: "\<And> a n x. fn a n x = (f a ^^ n) x" |
|
303 |
shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al" |
|
304 |
unfolding DAList_Multiset.fold_def |
|
305 |
proof (induct al) |
|
306 |
fix ys |
|
307 |
let ?inv = "{xs :: ('a \<times> nat)list. (distinct \<circ> map fst) xs}" |
|
308 |
note cs[simp del] = count_simps |
|
309 |
have count[simp]: "\<And> x. count (Abs_multiset (count_of x)) = count_of x" |
|
310 |
by (rule Abs_multiset_inverse[OF count_of_multiset]) |
|
311 |
assume ys: "ys \<in> ?inv" |
|
312 |
thus "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" |
|
313 |
unfolding Bag_def unfolding Alist_inverse[OF ys] |
|
314 |
proof (induct ys arbitrary: e rule: list.induct) |
|
315 |
case Nil |
|
316 |
show ?case |
|
317 |
by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]]) |
|
318 |
(auto, simp add: cs) |
|
319 |
next |
|
320 |
case (Cons pair ys e) |
|
321 |
obtain a n where pair: "pair = (a,n)" by force |
|
322 |
from fn[of a n] have [simp]: "fn a n = (f a ^^ n)" by auto |
|
323 |
have inv: "ys \<in> ?inv" using Cons(2) by auto |
|
324 |
note IH = Cons(1)[OF inv] |
|
325 |
def Ys \<equiv> "Abs_multiset (count_of ys)" |
|
326 |
have id: "Abs_multiset (count_of ((a, n) # ys)) = ((op + {# a #}) ^^ n) Ys" |
|
327 |
unfolding Ys_def |
|
328 |
proof (rule multiset_eqI, unfold count) |
|
329 |
fix c |
|
330 |
show "count_of ((a, n) # ys) c = count ((op + {#a#} ^^ n) (Abs_multiset (count_of ys))) c" (is "?l = ?r") |
|
331 |
proof (cases "c = a") |
|
332 |
case False thus ?thesis unfolding cs by (induct n) auto |
|
333 |
next |
|
334 |
case True |
|
335 |
hence "?l = n" by (simp add: cs) |
|
336 |
also have "n = ?r" unfolding True |
|
337 |
proof (induct n) |
|
338 |
case 0 |
|
339 |
from Cons(2)[unfolded pair] have "a \<notin> fst ` set ys" by auto |
|
340 |
thus ?case by (induct ys) (simp, auto simp: cs) |
|
341 |
qed auto |
|
342 |
finally show ?thesis . |
|
343 |
qed |
|
344 |
qed |
|
345 |
show ?case unfolding pair |
|
346 |
by (simp add: IH[symmetric], unfold id Ys_def[symmetric], |
|
347 |
induct n, auto simp: fold_mset_fun_left_comm[symmetric]) |
|
348 |
qed |
|
349 |
qed |
|
350 |
||
351 |
end |
|
352 |
||
353 |
lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b)alist" is "\<lambda> a b. [(a,b)]" by auto |
|
354 |
||
355 |
lemma image_mset_Bag[code]: |
|
356 |
"image_mset f (Bag ms) = |
|
357 |
DAList_Multiset.fold (\<lambda> a n m. Bag (single_alist_entry (f a) n) + m) {#} ms" |
|
358 |
unfolding image_mset_def |
|
359 |
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1]) |
|
360 |
fix a n m |
|
361 |
show "Bag (single_alist_entry (f a) n) + m = ((op + \<circ> single \<circ> f) a ^^ n) m" (is "?l = ?r") |
|
362 |
proof (rule multiset_eqI) |
|
363 |
fix x |
|
364 |
have "count ?r x = (if x = f a then n + count m x else count m x)" |
|
365 |
by (induct n, auto) |
|
366 |
also have "\<dots> = count ?l x" by (simp add: single_alist_entry.rep_eq) |
|
367 |
finally show "count ?l x = count ?r x" .. |
|
368 |
qed |
|
369 |
qed |
|
370 |
||
371 |
hide_const single_alist_entry |
|
372 |
||
373 |
(* we cannot use (\<lambda> a n. op + (a * n)) for folding, since * is not defined |
|
374 |
in comm_monoid_add *) |
|
375 |
lemma msetsum_Bag[code]: |
|
376 |
"msetsum (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op + a) ^^ n)) 0 ms" |
|
377 |
unfolding msetsum.eq_fold |
|
378 |
by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps) |
|
379 |
||
380 |
(* we cannot use (\<lambda> a n. op * (a ^ n)) for folding, since ^ is not defined |
|
381 |
in comm_monoid_mult *) |
|
382 |
lemma msetprod_Bag[code]: |
|
383 |
"msetprod (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op * a) ^^ n)) 1 ms" |
|
384 |
unfolding msetprod.eq_fold |
|
385 |
by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps) |
|
386 |
||
387 |
lemma mcard_fold: "mcard A = Multiset.fold (\<lambda> _. Suc) 0 A" (is "_ = Multiset.fold ?f _ _") |
|
388 |
proof - |
|
389 |
interpret comp_fun_commute ?f by (default, auto) |
|
390 |
show ?thesis by (induct A) auto |
|
391 |
qed |
|
392 |
||
393 |
lemma mcard_Bag[code]: |
|
394 |
"mcard (Bag ms) = DAList_Multiset.fold (\<lambda> a n. op + n) 0 ms" |
|
395 |
unfolding mcard_fold |
|
396 |
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp) |
|
397 |
fix a n x |
|
398 |
show "n + x = (Suc ^^ n) x" by (induct n) auto |
|
399 |
qed |
|
400 |
||
401 |
||
402 |
lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _") |
|
403 |
proof - |
|
404 |
interpret comp_fun_commute ?f by (default, auto) |
|
405 |
show ?thesis by (induct A, auto) |
|
406 |
qed |
|
407 |
||
408 |
lemma set_of_Bag[code]: |
|
409 |
"set_of (Bag ms) = DAList_Multiset.fold (\<lambda> a n. (if n = 0 then (\<lambda> m. m) else insert a)) {} ms" |
|
410 |
unfolding set_of_fold |
|
411 |
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1]) |
|
412 |
fix a n x |
|
413 |
show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n") |
|
414 |
proof (cases n) |
|
415 |
case (Suc m) |
|
416 |
hence "?l n = insert a x" by simp |
|
417 |
moreover have "?r n = insert a x" unfolding Suc by (induct m) auto |
|
418 |
ultimately show ?thesis by auto |
|
419 |
qed auto |
|
420 |
qed |
|
421 |
||
422 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
423 |
instantiation multiset :: (exhaustive) exhaustive |
51599 | 424 |
begin |
425 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
426 |
definition exhaustive_multiset :: "('a multiset \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
427 |
where |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
428 |
"exhaustive_multiset f i = Quickcheck_Exhaustive.exhaustive (\<lambda>xs. f (Bag xs)) i" |
51599 | 429 |
|
430 |
instance .. |
|
431 |
||
432 |
end |
|
433 |
||
434 |
end |
|
435 |