author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 51623 | 1194b438426a |
child 55808 | 488c3e8282c8 |
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 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
69 |
|
51599 | 70 |
text {* Raw operations on lists *} |
71 |
||
72 |
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" |
|
73 |
where |
|
74 |
"join_raw f xs ys = foldr (\<lambda>(k, v). map_default k v (%v'. f k (v', v))) ys xs" |
|
75 |
||
76 |
lemma join_raw_Nil [simp]: |
|
77 |
"join_raw f xs [] = xs" |
|
78 |
by (simp add: join_raw_def) |
|
79 |
||
80 |
lemma join_raw_Cons [simp]: |
|
81 |
"join_raw f xs ((k, v) # ys) = map_default k v (%v'. f k (v', v)) (join_raw f xs ys)" |
|
82 |
by (simp add: join_raw_def) |
|
83 |
||
84 |
lemma map_of_join_raw: |
|
85 |
assumes "distinct (map fst ys)" |
|
86 |
shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v => |
|
87 |
(case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))" |
|
88 |
using assms |
|
89 |
apply (induct ys) |
|
90 |
apply (auto simp add: map_of_map_default split: option.split) |
|
91 |
apply (metis map_of_eq_None_iff option.simps(2) weak_map_of_SomeI) |
|
92 |
by (metis Some_eq_map_of_iff map_of_eq_None_iff option.simps(2)) |
|
93 |
||
94 |
lemma distinct_join_raw: |
|
95 |
assumes "distinct (map fst xs)" |
|
96 |
shows "distinct (map fst (join_raw f xs ys))" |
|
97 |
using assms |
|
98 |
proof (induct ys) |
|
99 |
case (Cons y ys) |
|
100 |
thus ?case by (cases y) (simp add: distinct_map_default) |
|
101 |
qed auto |
|
102 |
||
103 |
definition |
|
104 |
"subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs" |
|
105 |
||
106 |
lemma map_of_subtract_entries_raw: |
|
107 |
assumes "distinct (map fst ys)" |
|
108 |
shows "map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => |
|
109 |
(case map_of ys x of None => Some v | Some v' => Some (v - v')))" |
|
110 |
using assms unfolding subtract_entries_raw_def |
|
111 |
apply (induct ys) |
|
112 |
apply auto |
|
113 |
apply (simp split: option.split) |
|
114 |
apply (simp add: map_of_map_entry) |
|
115 |
apply (auto split: option.split) |
|
116 |
apply (metis map_of_eq_None_iff option.simps(3) option.simps(4)) |
|
117 |
by (metis map_of_eq_None_iff option.simps(4) option.simps(5)) |
|
118 |
||
119 |
lemma distinct_subtract_entries_raw: |
|
120 |
assumes "distinct (map fst xs)" |
|
121 |
shows "distinct (map fst (subtract_entries_raw xs ys))" |
|
122 |
using assms |
|
123 |
unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry) |
|
124 |
||
125 |
||
126 |
text {* Operations on alists with distinct keys *} |
|
127 |
||
128 |
lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" |
|
129 |
is join_raw |
|
130 |
by (simp add: distinct_join_raw) |
|
131 |
||
132 |
lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" |
|
133 |
is subtract_entries_raw |
|
134 |
by (simp add: distinct_subtract_entries_raw) |
|
135 |
||
136 |
||
137 |
text {* Implementing multisets by means of association lists *} |
|
138 |
||
139 |
definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat" where |
|
140 |
"count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)" |
|
141 |
||
142 |
lemma count_of_multiset: |
|
143 |
"count_of xs \<in> multiset" |
|
144 |
proof - |
|
145 |
let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)}" |
|
146 |
have "?A \<subseteq> dom (map_of xs)" |
|
147 |
proof |
|
148 |
fix x |
|
149 |
assume "x \<in> ?A" |
|
150 |
then have "0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)" by simp |
|
151 |
then have "map_of xs x \<noteq> None" by (cases "map_of xs x") auto |
|
152 |
then show "x \<in> dom (map_of xs)" by auto |
|
153 |
qed |
|
154 |
with finite_dom_map_of [of xs] have "finite ?A" |
|
155 |
by (auto intro: finite_subset) |
|
156 |
then show ?thesis |
|
157 |
by (simp add: count_of_def fun_eq_iff multiset_def) |
|
158 |
qed |
|
159 |
||
160 |
lemma count_simps [simp]: |
|
161 |
"count_of [] = (\<lambda>_. 0)" |
|
162 |
"count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)" |
|
163 |
by (simp_all add: count_of_def fun_eq_iff) |
|
164 |
||
165 |
lemma count_of_empty: |
|
166 |
"x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0" |
|
167 |
by (induct xs) (simp_all add: count_of_def) |
|
168 |
||
169 |
lemma count_of_filter: |
|
170 |
"count_of (List.filter (P \<circ> fst) xs) x = (if P x then count_of xs x else 0)" |
|
171 |
by (induct xs) auto |
|
172 |
||
173 |
lemma count_of_map_default [simp]: |
|
174 |
"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)" |
|
175 |
unfolding count_of_def by (simp add: map_of_map_default split: option.split) |
|
176 |
||
177 |
lemma count_of_join_raw: |
|
178 |
"distinct (map fst ys) ==> count_of xs x + count_of ys x = count_of (join_raw (%x (x, y). x + y) xs ys) x" |
|
179 |
unfolding count_of_def by (simp add: map_of_join_raw split: option.split) |
|
180 |
||
181 |
lemma count_of_subtract_entries_raw: |
|
182 |
"distinct (map fst ys) ==> count_of xs x - count_of ys x = count_of (subtract_entries_raw xs ys) x" |
|
183 |
unfolding count_of_def by (simp add: map_of_subtract_entries_raw split: option.split) |
|
184 |
||
185 |
||
186 |
text {* Code equations for multiset operations *} |
|
187 |
||
188 |
definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset" where |
|
189 |
"Bag xs = Abs_multiset (count_of (DAList.impl_of xs))" |
|
190 |
||
191 |
code_datatype Bag |
|
192 |
||
193 |
lemma count_Bag [simp, code]: |
|
194 |
"count (Bag xs) = count_of (DAList.impl_of xs)" |
|
195 |
by (simp add: Bag_def count_of_multiset Abs_multiset_inverse) |
|
196 |
||
197 |
lemma Mempty_Bag [code]: |
|
198 |
"{#} = Bag (DAList.empty)" |
|
199 |
by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def) |
|
200 |
||
201 |
lemma single_Bag [code]: |
|
202 |
"{#x#} = Bag (DAList.update x 1 DAList.empty)" |
|
203 |
by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq) |
|
204 |
||
205 |
lemma union_Bag [code]: |
|
206 |
"Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)" |
|
207 |
by (rule multiset_eqI) (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def) |
|
208 |
||
209 |
lemma minus_Bag [code]: |
|
210 |
"Bag xs - Bag ys = Bag (subtract_entries xs ys)" |
|
211 |
by (rule multiset_eqI) |
|
212 |
(simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def) |
|
213 |
||
214 |
lemma filter_Bag [code]: |
|
215 |
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)" |
|
216 |
by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq) |
|
217 |
||
218 |
lemma mset_less_eq_Bag [code]: |
|
219 |
"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)" |
|
220 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
221 |
proof |
|
222 |
assume ?lhs then show ?rhs |
|
223 |
by (auto simp add: mset_le_def) |
|
224 |
next |
|
225 |
assume ?rhs |
|
226 |
show ?lhs |
|
227 |
proof (rule mset_less_eqI) |
|
228 |
fix x |
|
229 |
from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x" |
|
230 |
by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty) |
|
231 |
then show "count (Bag xs) x \<le> count A x" |
|
232 |
by (simp add: mset_le_def) |
|
233 |
qed |
|
234 |
qed |
|
235 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
236 |
declare multiset_inter_def [code] |
51623 | 237 |
declare sup_multiset_def [code] |
238 |
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
|
239 |
|
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
240 |
instantiation multiset :: (exhaustive) exhaustive |
51599 | 241 |
begin |
242 |
||
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
243 |
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
|
244 |
where |
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset
|
245 |
"exhaustive_multiset f i = Quickcheck_Exhaustive.exhaustive (\<lambda>xs. f (Bag xs)) i" |
51599 | 246 |
|
247 |
instance .. |
|
248 |
||
249 |
end |
|
250 |
||
251 |
end |
|
252 |