112 by (simp add: single.rep_eq) |
106 by (simp add: single.rep_eq) |
113 |
107 |
114 |
108 |
115 subsection \<open>Basic operations\<close> |
109 subsection \<open>Basic operations\<close> |
116 |
110 |
|
111 subsubsection \<open>Conversion to set and membership\<close> |
|
112 |
|
113 definition set_mset :: "'a multiset \<Rightarrow> 'a set" |
|
114 where "set_mset M = {x. count M x > 0}" |
|
115 |
|
116 abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<in>#" 50) |
|
117 where "a \<in># M \<equiv> a \<in> set_mset M" |
|
118 |
|
119 abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<notin>#" 50) |
|
120 where "a \<notin># M \<equiv> a \<notin> set_mset M" |
|
121 |
|
122 context |
|
123 begin |
|
124 |
|
125 qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
126 where "Ball M \<equiv> Set.Ball (set_mset M)" |
|
127 |
|
128 qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
129 where "Bex M \<equiv> Set.Bex (set_mset M)" |
|
130 |
|
131 end |
|
132 |
|
133 syntax |
|
134 "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10) |
|
135 "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10) |
|
136 |
|
137 translations |
|
138 "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)" |
|
139 "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)" |
|
140 |
|
141 lemma count_eq_zero_iff: |
|
142 "count M x = 0 \<longleftrightarrow> x \<notin># M" |
|
143 by (auto simp add: set_mset_def) |
|
144 |
|
145 lemma not_in_iff: |
|
146 "x \<notin># M \<longleftrightarrow> count M x = 0" |
|
147 by (auto simp add: count_eq_zero_iff) |
|
148 |
|
149 lemma count_greater_zero_iff [simp]: |
|
150 "count M x > 0 \<longleftrightarrow> x \<in># M" |
|
151 by (auto simp add: set_mset_def) |
|
152 |
|
153 lemma count_inI: |
|
154 assumes "count M x = 0 \<Longrightarrow> False" |
|
155 shows "x \<in># M" |
|
156 proof (rule ccontr) |
|
157 assume "x \<notin># M" |
|
158 with assms show False by (simp add: not_in_iff) |
|
159 qed |
|
160 |
|
161 lemma in_countE: |
|
162 assumes "x \<in># M" |
|
163 obtains n where "count M x = Suc n" |
|
164 proof - |
|
165 from assms have "count M x > 0" by simp |
|
166 then obtain n where "count M x = Suc n" |
|
167 using gr0_conv_Suc by blast |
|
168 with that show thesis . |
|
169 qed |
|
170 |
|
171 lemma count_greater_eq_Suc_zero_iff [simp]: |
|
172 "count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M" |
|
173 by (simp add: Suc_le_eq) |
|
174 |
|
175 lemma count_greater_eq_one_iff [simp]: |
|
176 "count M x \<ge> 1 \<longleftrightarrow> x \<in># M" |
|
177 by simp |
|
178 |
|
179 lemma set_mset_empty [simp]: |
|
180 "set_mset {#} = {}" |
|
181 by (simp add: set_mset_def) |
|
182 |
|
183 lemma set_mset_single [simp]: |
|
184 "set_mset {#b#} = {b}" |
|
185 by (simp add: set_mset_def) |
|
186 |
|
187 lemma set_mset_eq_empty_iff [simp]: |
|
188 "set_mset M = {} \<longleftrightarrow> M = {#}" |
|
189 by (auto simp add: multiset_eq_iff count_eq_zero_iff) |
|
190 |
|
191 lemma finite_set_mset [iff]: |
|
192 "finite (set_mset M)" |
|
193 using count [of M] by (simp add: multiset_def) |
|
194 |
|
195 |
117 subsubsection \<open>Union\<close> |
196 subsubsection \<open>Union\<close> |
118 |
197 |
119 lemma count_union [simp]: "count (M + N) a = count M a + count N a" |
198 lemma count_union [simp]: |
|
199 "count (M + N) a = count M a + count N a" |
120 by (simp add: plus_multiset.rep_eq) |
200 by (simp add: plus_multiset.rep_eq) |
121 |
201 |
|
202 lemma set_mset_union [simp]: |
|
203 "set_mset (M + N) = set_mset M \<union> set_mset N" |
|
204 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp |
|
205 |
122 |
206 |
123 subsubsection \<open>Difference\<close> |
207 subsubsection \<open>Difference\<close> |
124 |
208 |
125 instantiation multiset :: (type) comm_monoid_diff |
209 instance multiset :: (type) comm_monoid_diff |
126 begin |
210 by standard (transfer; simp add: fun_eq_iff) |
127 |
211 |
128 instance |
212 lemma count_diff [simp]: |
129 by (standard; transfer; simp add: fun_eq_iff) |
213 "count (M - N) a = count M a - count N a" |
130 |
|
131 end |
|
132 |
|
133 lemma count_diff [simp]: "count (M - N) a = count M a - count N a" |
|
134 by (simp add: minus_multiset.rep_eq) |
214 by (simp add: minus_multiset.rep_eq) |
|
215 |
|
216 lemma in_diff_count: |
|
217 "a \<in># M - N \<longleftrightarrow> count N a < count M a" |
|
218 by (simp add: set_mset_def) |
|
219 |
|
220 lemma count_in_diffI: |
|
221 assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False" |
|
222 shows "x \<in># M - N" |
|
223 proof (rule ccontr) |
|
224 assume "x \<notin># M - N" |
|
225 then have "count N x = (count N x - count M x) + count M x" |
|
226 by (simp add: in_diff_count not_less) |
|
227 with assms show False by auto |
|
228 qed |
|
229 |
|
230 lemma in_diff_countE: |
|
231 assumes "x \<in># M - N" |
|
232 obtains n where "count M x = Suc n + count N x" |
|
233 proof - |
|
234 from assms have "count M x - count N x > 0" by (simp add: in_diff_count) |
|
235 then have "count M x > count N x" by simp |
|
236 then obtain n where "count M x = Suc n + count N x" |
|
237 using less_iff_Suc_add by auto |
|
238 with that show thesis . |
|
239 qed |
|
240 |
|
241 lemma in_diffD: |
|
242 assumes "a \<in># M - N" |
|
243 shows "a \<in># M" |
|
244 proof - |
|
245 have "0 \<le> count N a" by simp |
|
246 also from assms have "count N a < count M a" |
|
247 by (simp add: in_diff_count) |
|
248 finally show ?thesis by simp |
|
249 qed |
|
250 |
|
251 lemma set_mset_diff: |
|
252 "set_mset (M - N) = {a. count N a < count M a}" |
|
253 by (simp add: set_mset_def) |
135 |
254 |
136 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |
255 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |
137 by rule (fact Groups.diff_zero, fact Groups.zero_diff) |
256 by rule (fact Groups.diff_zero, fact Groups.zero_diff) |
138 |
257 |
139 lemma diff_cancel[simp]: "A - A = {#}" |
258 lemma diff_cancel [simp]: "A - A = {#}" |
140 by (fact Groups.diff_cancel) |
259 by (fact Groups.diff_cancel) |
141 |
260 |
142 lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)" |
261 lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)" |
143 by (fact add_diff_cancel_right') |
262 by (fact add_diff_cancel_right') |
144 |
263 |
269 where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)" |
403 where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)" |
270 |
404 |
271 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) |
405 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) |
272 where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)" |
406 where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)" |
273 |
407 |
274 abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
408 abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<supseteq>#" 50) |
275 "supseteq_mset A B == B \<subseteq># A" |
409 where "supseteq_mset A B \<equiv> B \<subseteq># A" |
276 |
410 |
277 abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
411 abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<supset>#" 50) |
278 "supset_mset A B == B \<subset># A" |
412 where "supset_mset A B \<equiv> B \<subset># A" |
279 |
413 |
280 notation (input) |
414 notation (input) |
281 subseteq_mset (infix "\<le>#" 50) and |
415 subseteq_mset (infix "\<le>#" 50) and |
282 supseteq_mset (infix "\<ge>#" 50) and |
416 supseteq_mset (infix "\<ge>#" 50) |
283 supseteq_mset (infix "\<supseteq>#" 50) and |
|
284 supset_mset (infix "\<supset>#" 50) |
|
285 |
417 |
286 notation (ASCII) |
418 notation (ASCII) |
287 subseteq_mset (infix "<=#" 50) and |
419 subseteq_mset (infix "<=#" 50) and |
288 subset_mset (infix "<#" 50) and |
420 subset_mset (infix "<#" 50) and |
289 supseteq_mset (infix ">=#" 50) and |
421 supseteq_mset (infix ">=#" 50) and |
290 supset_mset (infix ">#" 50) |
422 supset_mset (infix ">#" 50) |
291 |
423 |
292 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#" |
424 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#" |
293 by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) |
425 by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) |
294 |
426 -- \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
295 lemma mset_less_eqI: "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B" |
427 |
|
428 lemma mset_less_eqI: |
|
429 "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B" |
296 by (simp add: subseteq_mset_def) |
430 by (simp add: subseteq_mset_def) |
297 |
431 |
298 lemma mset_le_exists_conv: "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)" |
432 lemma mset_less_eq_count: |
|
433 "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a" |
|
434 by (simp add: subseteq_mset_def) |
|
435 |
|
436 lemma mset_le_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)" |
299 unfolding subseteq_mset_def |
437 unfolding subseteq_mset_def |
300 apply (rule iffI) |
438 apply (rule iffI) |
301 apply (rule exI [where x = "B - A"]) |
439 apply (rule exI [where x = "B - A"]) |
302 apply (auto intro: multiset_eq_iff [THEN iffD2]) |
440 apply (auto intro: multiset_eq_iff [THEN iffD2]) |
303 done |
441 done |
306 by standard (simp, fact mset_le_exists_conv) |
444 by standard (simp, fact mset_le_exists_conv) |
307 |
445 |
308 declare subset_mset.zero_order[simp del] |
446 declare subset_mset.zero_order[simp del] |
309 -- \<open>this removes some simp rules not in the usual order for multisets\<close> |
447 -- \<open>this removes some simp rules not in the usual order for multisets\<close> |
310 |
448 |
311 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B" |
449 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B" |
312 by (fact subset_mset.add_le_cancel_right) |
450 by (fact subset_mset.add_le_cancel_right) |
313 |
451 |
314 lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<le># C + B \<longleftrightarrow> A \<le># B" |
452 lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B" |
315 by (fact subset_mset.add_le_cancel_left) |
453 by (fact subset_mset.add_le_cancel_left) |
316 |
454 |
317 lemma mset_le_mono_add: "(A::'a multiset) \<le># B \<Longrightarrow> C \<le># D \<Longrightarrow> A + C \<le># B + D" |
455 lemma mset_le_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D" |
318 by (fact subset_mset.add_mono) |
456 by (fact subset_mset.add_mono) |
319 |
457 |
320 lemma mset_le_add_left [simp]: "(A::'a multiset) \<le># A + B" |
458 lemma mset_le_add_left [simp]: "(A::'a multiset) \<subseteq># A + B" |
321 unfolding subseteq_mset_def by auto |
459 unfolding subseteq_mset_def by auto |
322 |
460 |
323 lemma mset_le_add_right [simp]: "B \<le># (A::'a multiset) + B" |
461 lemma mset_le_add_right [simp]: "B \<subseteq># (A::'a multiset) + B" |
324 unfolding subseteq_mset_def by auto |
462 unfolding subseteq_mset_def by auto |
325 |
463 |
326 lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<le># B" |
464 lemma single_subset_iff [simp]: |
327 by (simp add: subseteq_mset_def) |
465 "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M" |
328 |
466 by (auto simp add: subseteq_mset_def Suc_le_eq) |
|
467 |
|
468 lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B" |
|
469 by (simp add: subseteq_mset_def Suc_le_eq) |
|
470 |
329 lemma multiset_diff_union_assoc: |
471 lemma multiset_diff_union_assoc: |
330 fixes A B C D :: "'a multiset" |
472 fixes A B C D :: "'a multiset" |
331 shows "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)" |
473 shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)" |
332 by (simp add: subset_mset.diff_add_assoc) |
474 by (fact subset_mset.diff_add_assoc) |
333 |
475 |
334 lemma mset_le_multiset_union_diff_commute: |
476 lemma mset_le_multiset_union_diff_commute: |
335 fixes A B C D :: "'a multiset" |
477 fixes A B C D :: "'a multiset" |
336 shows "B \<le># A \<Longrightarrow> A - B + C = A + C - B" |
478 shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B" |
337 by (simp add: subset_mset.add_diff_assoc2) |
479 by (fact subset_mset.add_diff_assoc2) |
338 |
480 |
339 lemma diff_le_self[simp]: "(M::'a multiset) - N \<le># M" |
481 lemma diff_le_self[simp]: |
340 by(simp add: subseteq_mset_def) |
482 "(M::'a multiset) - N \<subseteq># M" |
341 |
483 by (simp add: subseteq_mset_def) |
342 lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
484 |
343 apply (clarsimp simp: subset_mset_def subseteq_mset_def) |
485 lemma mset_leD: |
344 apply (erule allE [where x = x]) |
486 assumes "A \<subseteq># B" and "x \<in># A" |
345 apply auto |
487 shows "x \<in># B" |
346 done |
488 proof - |
347 |
489 from \<open>x \<in># A\<close> have "count A x > 0" by simp |
348 lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
490 also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x" |
349 apply (clarsimp simp: subset_mset_def subseteq_mset_def) |
491 by (simp add: subseteq_mset_def) |
350 apply (erule allE [where x = x]) |
492 finally show ?thesis by simp |
351 apply auto |
493 qed |
352 done |
494 |
353 |
495 lemma mset_lessD: |
354 lemma mset_less_insertD: "(A + {#x#} <# B) \<Longrightarrow> (x \<in># B \<and> A <# B)" |
496 "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" |
355 apply (rule conjI) |
497 by (auto intro: mset_leD [of A]) |
356 apply (simp add: mset_lessD) |
498 |
357 apply (clarsimp simp: subset_mset_def subseteq_mset_def) |
499 lemma set_mset_mono: |
358 apply safe |
500 "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B" |
359 apply (erule_tac x = a in allE) |
501 by (metis mset_leD subsetI) |
360 apply (auto split: if_split_asm) |
502 |
361 done |
503 lemma mset_le_insertD: |
362 |
504 "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B" |
363 lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)" |
|
364 apply (rule conjI) |
505 apply (rule conjI) |
365 apply (simp add: mset_leD) |
506 apply (simp add: mset_leD) |
366 apply (force simp: subset_mset_def subseteq_mset_def split: if_split_asm) |
507 apply (clarsimp simp: subset_mset_def subseteq_mset_def) |
|
508 apply safe |
|
509 apply (erule_tac x = a in allE) |
|
510 apply (auto split: if_split_asm) |
367 done |
511 done |
368 |
512 |
369 lemma mset_less_of_empty[simp]: "A <# {#} \<longleftrightarrow> False" |
513 lemma mset_less_insertD: |
|
514 "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B" |
|
515 by (rule mset_le_insertD) simp |
|
516 |
|
517 lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False" |
370 by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff) |
518 by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff) |
371 |
519 |
372 lemma empty_le[simp]: "{#} \<le># A" |
520 lemma empty_le [simp]: "{#} \<subseteq># A" |
373 unfolding mset_le_exists_conv by auto |
521 unfolding mset_le_exists_conv by auto |
374 |
522 |
375 lemma le_empty[simp]: "(M \<le># {#}) = (M = {#})" |
523 lemma insert_subset_eq_iff: |
|
524 "{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}" |
|
525 using le_diff_conv2 [of "Suc 0" "count B a" "count A a"] |
|
526 apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq) |
|
527 apply (rule ccontr) |
|
528 apply (auto simp add: not_in_iff) |
|
529 done |
|
530 |
|
531 lemma insert_union_subset_iff: |
|
532 "{#a#} + A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}" |
|
533 by (auto simp add: insert_subset_eq_iff subset_mset_def insert_DiffM) |
|
534 |
|
535 lemma subset_eq_diff_conv: |
|
536 "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C" |
|
537 by (simp add: subseteq_mset_def le_diff_conv) |
|
538 |
|
539 lemma le_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}" |
376 unfolding mset_le_exists_conv by auto |
540 unfolding mset_le_exists_conv by auto |
377 |
541 |
378 lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}" |
542 lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}" |
379 by (auto simp: subset_mset_def subseteq_mset_def) |
543 by (auto simp: subset_mset_def subseteq_mset_def) |
380 |
544 |
381 lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False" |
545 lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False" |
382 by simp |
546 by simp |
383 |
547 |
384 lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \<Longrightarrow> N <# M" |
548 lemma mset_less_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M" |
385 by (fact subset_mset.add_less_imp_less_right) |
549 by (fact subset_mset.add_less_imp_less_right) |
386 |
550 |
387 lemma mset_less_empty_nonempty: "{#} <# S \<longleftrightarrow> S \<noteq> {#}" |
551 lemma mset_less_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}" |
388 by (fact subset_mset.zero_less_iff_neq_zero) |
552 by (fact subset_mset.zero_less_iff_neq_zero) |
389 |
553 |
390 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} <# B" |
554 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B" |
391 by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff) |
555 by (auto simp: subset_mset_def elim: mset_add) |
392 |
556 |
393 |
557 |
394 subsubsection \<open>Intersection\<close> |
558 subsubsection \<open>Intersection\<close> |
395 |
559 |
396 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where |
560 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where |
397 multiset_inter_def: "inf_subset_mset A B = A - (A - B)" |
561 multiset_inter_def: "inf_subset_mset A B = A - (A - B)" |
398 |
562 |
399 interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#" |
563 interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#" |
400 proof - |
564 proof - |
401 have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat |
565 have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat |
402 by arith |
566 by arith |
403 show "class.semilattice_inf op #\<inter> op \<le># op <#" |
567 show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#" |
404 by standard (auto simp add: multiset_inter_def subseteq_mset_def) |
568 by standard (auto simp add: multiset_inter_def subseteq_mset_def) |
405 qed |
569 qed |
406 |
570 -- \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
407 |
571 |
408 lemma multiset_inter_count [simp]: |
572 lemma multiset_inter_count [simp]: |
409 fixes A B :: "'a multiset" |
573 fixes A B :: "'a multiset" |
410 shows "count (A #\<inter> B) x = min (count A x) (count B x)" |
574 shows "count (A #\<inter> B) x = min (count A x) (count B x)" |
411 by (simp add: multiset_inter_def) |
575 by (simp add: multiset_inter_def) |
|
576 |
|
577 lemma set_mset_inter [simp]: |
|
578 "set_mset (A #\<inter> B) = set_mset A \<inter> set_mset B" |
|
579 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp |
|
580 |
|
581 lemma diff_intersect_left_idem [simp]: |
|
582 "M - M #\<inter> N = M - N" |
|
583 by (simp add: multiset_eq_iff min_def) |
|
584 |
|
585 lemma diff_intersect_right_idem [simp]: |
|
586 "M - N #\<inter> M = M - N" |
|
587 by (simp add: multiset_eq_iff min_def) |
412 |
588 |
413 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" |
589 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" |
414 by (rule multiset_eqI) auto |
590 by (rule multiset_eqI) auto |
415 |
591 |
416 lemma multiset_union_diff_commute: |
592 lemma multiset_union_diff_commute: |
419 proof (rule multiset_eqI) |
595 proof (rule multiset_eqI) |
420 fix x |
596 fix x |
421 from assms have "min (count B x) (count C x) = 0" |
597 from assms have "min (count B x) (count C x) = 0" |
422 by (auto simp add: multiset_eq_iff) |
598 by (auto simp add: multiset_eq_iff) |
423 then have "count B x = 0 \<or> count C x = 0" |
599 then have "count B x = 0 \<or> count C x = 0" |
424 by auto |
600 unfolding min_def by (auto split: if_splits) |
425 then show "count (A + B - C) x = count (A - C + B) x" |
601 then show "count (A + B - C) x = count (A - C + B) x" |
426 by auto |
602 by auto |
427 qed |
603 qed |
428 |
604 |
|
605 lemma disjunct_not_in: |
|
606 "A #\<inter> B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q") |
|
607 proof |
|
608 assume ?P |
|
609 show ?Q |
|
610 proof |
|
611 fix a |
|
612 from \<open>?P\<close> have "min (count A a) (count B a) = 0" |
|
613 by (simp add: multiset_eq_iff) |
|
614 then have "count A a = 0 \<or> count B a = 0" |
|
615 by (cases "count A a \<le> count B a") (simp_all add: min_def) |
|
616 then show "a \<notin># A \<or> a \<notin># B" |
|
617 by (simp add: not_in_iff) |
|
618 qed |
|
619 next |
|
620 assume ?Q |
|
621 show ?P |
|
622 proof (rule multiset_eqI) |
|
623 fix a |
|
624 from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0" |
|
625 by (auto simp add: not_in_iff) |
|
626 then show "count (A #\<inter> B) a = count {#} a" |
|
627 by auto |
|
628 qed |
|
629 qed |
|
630 |
429 lemma empty_inter [simp]: "{#} #\<inter> M = {#}" |
631 lemma empty_inter [simp]: "{#} #\<inter> M = {#}" |
430 by (simp add: multiset_eq_iff) |
632 by (simp add: multiset_eq_iff) |
431 |
633 |
432 lemma inter_empty [simp]: "M #\<inter> {#} = {#}" |
634 lemma inter_empty [simp]: "M #\<inter> {#} = {#}" |
433 by (simp add: multiset_eq_iff) |
635 by (simp add: multiset_eq_iff) |
434 |
636 |
435 lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N" |
637 lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N" |
436 by (simp add: multiset_eq_iff) |
638 by (simp add: multiset_eq_iff not_in_iff) |
437 |
639 |
438 lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}" |
640 lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}" |
439 by (simp add: multiset_eq_iff) |
641 by (auto simp add: multiset_eq_iff elim: mset_add) |
440 |
642 |
441 lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M" |
643 lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M" |
442 by (simp add: multiset_eq_iff) |
644 by (simp add: multiset_eq_iff not_in_iff) |
443 |
645 |
444 lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}" |
646 lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}" |
445 by (simp add: multiset_eq_iff) |
647 by (auto simp add: multiset_eq_iff elim: mset_add) |
|
648 |
|
649 lemma disjunct_set_mset_diff: |
|
650 assumes "M #\<inter> N = {#}" |
|
651 shows "set_mset (M - N) = set_mset M" |
|
652 proof (rule set_eqI) |
|
653 fix a |
|
654 from assms have "a \<notin># M \<or> a \<notin># N" |
|
655 by (simp add: disjunct_not_in) |
|
656 then show "a \<in># M - N \<longleftrightarrow> a \<in># M" |
|
657 by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff) |
|
658 qed |
|
659 |
|
660 lemma at_most_one_mset_mset_diff: |
|
661 assumes "a \<notin># M - {#a#}" |
|
662 shows "set_mset (M - {#a#}) = set_mset M - {a}" |
|
663 using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff) |
|
664 |
|
665 lemma more_than_one_mset_mset_diff: |
|
666 assumes "a \<in># M - {#a#}" |
|
667 shows "set_mset (M - {#a#}) = set_mset M" |
|
668 proof (rule set_eqI) |
|
669 fix b |
|
670 have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith |
|
671 then show "b \<in># M - {#a#} \<longleftrightarrow> b \<in># M" |
|
672 using assms by (auto simp add: in_diff_count) |
|
673 qed |
|
674 |
|
675 lemma inter_iff: |
|
676 "a \<in># A #\<inter> B \<longleftrightarrow> a \<in># A \<and> a \<in># B" |
|
677 by simp |
|
678 |
|
679 lemma inter_union_distrib_left: |
|
680 "A #\<inter> B + C = (A + C) #\<inter> (B + C)" |
|
681 by (simp add: multiset_eq_iff min_add_distrib_left) |
|
682 |
|
683 lemma inter_union_distrib_right: |
|
684 "C + A #\<inter> B = (C + A) #\<inter> (C + B)" |
|
685 using inter_union_distrib_left [of A B C] by (simp add: ac_simps) |
|
686 |
|
687 lemma inter_subset_eq_union: |
|
688 "A #\<inter> B \<subseteq># A + B" |
|
689 by (auto simp add: subseteq_mset_def) |
446 |
690 |
447 |
691 |
448 subsubsection \<open>Bounded union\<close> |
692 subsubsection \<open>Bounded union\<close> |
449 |
693 |
450 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70) |
694 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70) |
451 where "sup_subset_mset A B = A + (B - A)" |
695 where "sup_subset_mset A B = A + (B - A)" -- \<open>FIXME irregular fact name\<close> |
452 |
696 |
453 interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#" |
697 interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#" |
454 proof - |
698 proof - |
455 have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat |
699 have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat |
456 by arith |
700 by arith |
457 show "class.semilattice_sup op #\<union> op \<le># op <#" |
701 show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#" |
458 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
702 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
459 qed |
703 qed |
460 |
704 -- \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
461 lemma sup_subset_mset_count [simp]: "count (A #\<union> B) x = max (count A x) (count B x)" |
705 |
|
706 lemma sup_subset_mset_count [simp]: -- \<open>FIXME irregular fact name\<close> |
|
707 "count (A #\<union> B) x = max (count A x) (count B x)" |
462 by (simp add: sup_subset_mset_def) |
708 by (simp add: sup_subset_mset_def) |
|
709 |
|
710 lemma set_mset_sup [simp]: |
|
711 "set_mset (A #\<union> B) = set_mset A \<union> set_mset B" |
|
712 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count) |
|
713 (auto simp add: not_in_iff elim: mset_add) |
463 |
714 |
464 lemma empty_sup [simp]: "{#} #\<union> M = M" |
715 lemma empty_sup [simp]: "{#} #\<union> M = M" |
465 by (simp add: multiset_eq_iff) |
716 by (simp add: multiset_eq_iff) |
466 |
717 |
467 lemma sup_empty [simp]: "M #\<union> {#} = M" |
718 lemma sup_empty [simp]: "M #\<union> {#} = M" |
468 by (simp add: multiset_eq_iff) |
719 by (simp add: multiset_eq_iff) |
469 |
720 |
470 lemma sup_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}" |
721 lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}" |
|
722 by (simp add: multiset_eq_iff not_in_iff) |
|
723 |
|
724 lemma sup_union_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}" |
471 by (simp add: multiset_eq_iff) |
725 by (simp add: multiset_eq_iff) |
472 |
726 |
473 lemma sup_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}" |
727 lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}" |
|
728 by (simp add: multiset_eq_iff not_in_iff) |
|
729 |
|
730 lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}" |
474 by (simp add: multiset_eq_iff) |
731 by (simp add: multiset_eq_iff) |
475 |
732 |
476 lemma sup_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}" |
733 lemma sup_union_distrib_left: |
477 by (simp add: multiset_eq_iff) |
734 "A #\<union> B + C = (A + C) #\<union> (B + C)" |
478 |
735 by (simp add: multiset_eq_iff max_add_distrib_left) |
479 lemma sup_add_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}" |
736 |
480 by (simp add: multiset_eq_iff) |
737 lemma union_sup_distrib_right: |
|
738 "C + A #\<union> B = (C + A) #\<union> (C + B)" |
|
739 using sup_union_distrib_left [of A B C] by (simp add: ac_simps) |
|
740 |
|
741 lemma union_diff_inter_eq_sup: |
|
742 "A + B - A #\<inter> B = A #\<union> B" |
|
743 by (auto simp add: multiset_eq_iff) |
|
744 |
|
745 lemma union_diff_sup_eq_inter: |
|
746 "A + B - A #\<union> B = A #\<inter> B" |
|
747 by (auto simp add: multiset_eq_iff) |
|
748 |
481 |
749 |
482 subsubsection \<open>Subset is an order\<close> |
750 subsubsection \<open>Subset is an order\<close> |
|
751 |
483 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto |
752 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto |
|
753 |
484 |
754 |
485 subsubsection \<open>Filter (with comprehension syntax)\<close> |
755 subsubsection \<open>Filter (with comprehension syntax)\<close> |
486 |
756 |
487 text \<open>Multiset comprehension\<close> |
757 text \<open>Multiset comprehension\<close> |
488 |
758 |
489 lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" |
759 lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" |
490 is "\<lambda>P M. \<lambda>x. if P x then M x else 0" |
760 is "\<lambda>P M. \<lambda>x. if P x then M x else 0" |
491 by (rule filter_preserves_multiset) |
761 by (rule filter_preserves_multiset) |
492 |
|
493 lemma count_filter_mset [simp]: "count (filter_mset P M) a = (if P a then count M a else 0)" |
|
494 by (simp add: filter_mset.rep_eq) |
|
495 |
|
496 lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}" |
|
497 by (rule multiset_eqI) simp |
|
498 |
|
499 lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})" |
|
500 by (rule multiset_eqI) simp |
|
501 |
|
502 lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N" |
|
503 by (rule multiset_eqI) simp |
|
504 |
|
505 lemma filter_diff_mset [simp]: "filter_mset P (M - N) = filter_mset P M - filter_mset P N" |
|
506 by (rule multiset_eqI) simp |
|
507 |
|
508 lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N" |
|
509 by (rule multiset_eqI) simp |
|
510 |
|
511 lemma multiset_filter_subset[simp]: "filter_mset f M \<le># M" |
|
512 by (simp add: mset_less_eqI) |
|
513 |
|
514 lemma multiset_filter_mono: |
|
515 assumes "A \<le># B" |
|
516 shows "filter_mset f A \<le># filter_mset f B" |
|
517 proof - |
|
518 from assms[unfolded mset_le_exists_conv] |
|
519 obtain C where B: "B = A + C" by auto |
|
520 show ?thesis unfolding B by auto |
|
521 qed |
|
522 |
762 |
523 syntax (ASCII) |
763 syntax (ASCII) |
524 "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})") |
764 "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})") |
525 syntax |
765 syntax |
526 "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})") |
766 "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})") |
527 translations |
767 translations |
528 "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M" |
768 "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M" |
529 |
769 |
530 |
770 lemma count_filter_mset [simp]: |
531 subsubsection \<open>Set of elements\<close> |
771 "count (filter_mset P M) a = (if P a then count M a else 0)" |
532 |
772 by (simp add: filter_mset.rep_eq) |
533 definition set_mset :: "'a multiset \<Rightarrow> 'a set" |
773 |
534 where "set_mset M = {x. x \<in># M}" |
774 lemma set_mset_filter [simp]: |
535 |
775 "set_mset (filter_mset P M) = {a \<in> set_mset M. P a}" |
536 lemma set_mset_empty [simp]: "set_mset {#} = {}" |
776 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp |
537 by (simp add: set_mset_def) |
777 |
538 |
778 lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}" |
539 lemma set_mset_single [simp]: "set_mset {#b#} = {b}" |
779 by (rule multiset_eqI) simp |
540 by (simp add: set_mset_def) |
780 |
541 |
781 lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})" |
542 lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N" |
782 by (rule multiset_eqI) simp |
543 by (auto simp add: set_mset_def) |
783 |
544 |
784 lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N" |
545 lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})" |
785 by (rule multiset_eqI) simp |
546 by (auto simp add: set_mset_def multiset_eq_iff) |
786 |
547 |
787 lemma filter_diff_mset [simp]: "filter_mset P (M - N) = filter_mset P M - filter_mset P N" |
548 lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x \<in># M)" |
788 by (rule multiset_eqI) simp |
549 by (auto simp add: set_mset_def) |
789 |
550 |
790 lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N" |
551 lemma set_mset_filter [simp]: "set_mset {# x\<in>#M. P x #} = set_mset M \<inter> {x. P x}" |
791 by (rule multiset_eqI) simp |
552 by (auto simp add: set_mset_def) |
792 |
553 |
793 lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M" |
554 lemma finite_set_mset [iff]: "finite (set_mset M)" |
794 by (simp add: mset_less_eqI) |
555 using count [of M] by (simp add: multiset_def set_mset_def) |
795 |
556 |
796 lemma multiset_filter_mono: |
557 lemma finite_Collect_mem [iff]: "finite {x. x \<in># M}" |
797 assumes "A \<subseteq># B" |
558 unfolding set_mset_def[symmetric] by simp |
798 shows "filter_mset f A \<subseteq># filter_mset f B" |
559 |
799 proof - |
560 lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B" |
800 from assms[unfolded mset_le_exists_conv] |
561 by (metis mset_leD subsetI mem_set_mset_iff) |
801 obtain C where B: "B = A + C" by auto |
562 |
802 show ?thesis unfolding B by auto |
563 lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)" |
803 qed |
564 by auto |
804 |
|
805 lemma filter_mset_eq_conv: |
|
806 "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q") |
|
807 proof |
|
808 assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count) |
|
809 next |
|
810 assume ?Q |
|
811 then obtain Q where M: "M = N + Q" |
|
812 by (auto simp add: mset_le_exists_conv) |
|
813 then have MN: "M - N = Q" by simp |
|
814 show ?P |
|
815 proof (rule multiset_eqI) |
|
816 fix a |
|
817 from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q" |
|
818 by auto |
|
819 show "count (filter_mset P M) a = count N a" |
|
820 proof (cases "a \<in># M") |
|
821 case True |
|
822 with * show ?thesis |
|
823 by (simp add: not_in_iff M) |
|
824 next |
|
825 case False then have "count M a = 0" |
|
826 by (simp add: not_in_iff) |
|
827 with M show ?thesis by simp |
|
828 qed |
|
829 qed |
|
830 qed |
565 |
831 |
566 |
832 |
567 subsubsection \<open>Size\<close> |
833 subsubsection \<open>Size\<close> |
568 |
834 |
569 definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))" |
835 definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))" |
689 lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}" |
955 lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}" |
690 apply (subst multiset_eq_iff) |
956 apply (subst multiset_eq_iff) |
691 apply auto |
957 apply auto |
692 done |
958 done |
693 |
959 |
694 lemma mset_less_size: "(A::'a multiset) <# B \<Longrightarrow> size A < size B" |
960 lemma mset_less_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B" |
695 proof (induct A arbitrary: B) |
961 proof (induct A arbitrary: B) |
696 case (empty M) |
962 case (empty M) |
697 then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) |
963 then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) |
698 then obtain M' x where "M = M' + {#x#}" |
964 then obtain M' x where "M = M' + {#x#}" |
699 by (blast dest: multi_nonempty_split) |
965 by (blast dest: multi_nonempty_split) |
700 then show ?case by simp |
966 then show ?case by simp |
701 next |
967 next |
702 case (add S x T) |
968 case (add S x T) |
703 have IH: "\<And>B. S <# B \<Longrightarrow> size S < size B" by fact |
969 have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact |
704 have SxsubT: "S + {#x#} <# T" by fact |
970 have SxsubT: "S + {#x#} \<subset># T" by fact |
705 then have "x \<in># T" and "S <# T" by (auto dest: mset_less_insertD) |
971 then have "x \<in># T" and "S \<subset># T" |
|
972 by (auto dest: mset_less_insertD) |
706 then obtain T' where T: "T = T' + {#x#}" |
973 then obtain T' where T: "T = T' + {#x#}" |
707 by (blast dest: multi_member_split) |
974 by (blast dest: multi_member_split) |
708 then have "S <# T'" using SxsubT |
975 then have "S \<subset># T'" using SxsubT |
709 by (blast intro: mset_less_add_bothsides) |
976 by (blast intro: mset_less_add_bothsides) |
710 then have "size S < size T'" using IH by simp |
977 then have "size S < size T'" using IH by simp |
711 then show ?case using T by simp |
978 then show ?case using T by simp |
712 qed |
979 qed |
713 |
980 |
714 |
|
715 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}" |
981 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}" |
716 by (cases M) auto |
982 by (cases M) auto |
717 |
983 |
|
984 |
718 subsubsection \<open>Strong induction and subset induction for multisets\<close> |
985 subsubsection \<open>Strong induction and subset induction for multisets\<close> |
719 |
986 |
720 text \<open>Well-foundedness of strict subset relation\<close> |
987 text \<open>Well-foundedness of strict subset relation\<close> |
721 |
988 |
722 lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}" |
989 lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}" |
723 apply (rule wf_measure [THEN wf_subset, where f1=size]) |
990 apply (rule wf_measure [THEN wf_subset, where f1=size]) |
724 apply (clarsimp simp: measure_def inv_image_def mset_less_size) |
991 apply (clarsimp simp: measure_def inv_image_def mset_less_size) |
725 done |
992 done |
726 |
993 |
727 lemma full_multiset_induct [case_names less]: |
994 lemma full_multiset_induct [case_names less]: |
728 assumes ih: "\<And>B. \<forall>(A::'a multiset). A <# B \<longrightarrow> P A \<Longrightarrow> P B" |
995 assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B" |
729 shows "P B" |
996 shows "P B" |
730 apply (rule wf_less_mset_rel [THEN wf_induct]) |
997 apply (rule wf_less_mset_rel [THEN wf_induct]) |
731 apply (rule ih, auto) |
998 apply (rule ih, auto) |
732 done |
999 done |
733 |
1000 |
734 lemma multi_subset_induct [consumes 2, case_names empty add]: |
1001 lemma multi_subset_induct [consumes 2, case_names empty add]: |
735 assumes "F \<le># A" |
1002 assumes "F \<subseteq># A" |
736 and empty: "P {#}" |
1003 and empty: "P {#}" |
737 and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" |
1004 and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" |
738 shows "P F" |
1005 shows "P F" |
739 proof - |
1006 proof - |
740 from \<open>F \<le># A\<close> |
1007 from \<open>F \<subseteq># A\<close> |
741 show ?thesis |
1008 show ?thesis |
742 proof (induct F) |
1009 proof (induct F) |
743 show "P {#}" by fact |
1010 show "P {#}" by fact |
744 next |
1011 next |
745 fix x F |
1012 fix x F |
746 assume P: "F \<le># A \<Longrightarrow> P F" and i: "F + {#x#} \<le># A" |
1013 assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A" |
747 show "P (F + {#x#})" |
1014 show "P (F + {#x#})" |
748 proof (rule insert) |
1015 proof (rule insert) |
749 from i show "x \<in># A" by (auto dest: mset_le_insertD) |
1016 from i show "x \<in># A" by (auto dest: mset_le_insertD) |
750 from i have "F \<le># A" by (auto dest: mset_le_insertD) |
1017 from i have "F \<subseteq># A" by (auto dest: mset_le_insertD) |
751 with P show "P F" . |
1018 with P show "P F" . |
752 qed |
1019 qed |
753 qed |
1020 qed |
754 qed |
1021 qed |
755 |
1022 |
1670 |
1980 |
1671 lemma mult_implies_one_step: |
1981 lemma mult_implies_one_step: |
1672 "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow> |
1982 "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow> |
1673 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> |
1983 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> |
1674 (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)" |
1984 (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)" |
1675 apply (unfold mult_def mult1_def set_mset_def) |
1985 apply (unfold mult_def mult1_def) |
1676 apply (erule converse_trancl_induct, clarify) |
1986 apply (erule converse_trancl_induct, clarify) |
1677 apply (rule_tac x = M0 in exI, simp, clarify) |
1987 apply (rule_tac x = M0 in exI, simp, clarify) |
1678 apply (case_tac "a \<in># K") |
1988 apply (case_tac "a \<in># K") |
1679 apply (rule_tac x = I in exI) |
1989 apply (rule_tac x = I in exI) |
1680 apply (simp (no_asm)) |
1990 apply (simp (no_asm)) |
1681 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
1991 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
1682 apply (simp (no_asm_simp) add: add.assoc [symmetric]) |
1992 apply (simp (no_asm_simp) add: add.assoc [symmetric]) |
1683 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong) |
1993 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong) |
1684 apply (simp add: diff_union_single_conv) |
1994 apply (simp add: diff_union_single_conv) |
1685 apply (simp (no_asm_use) add: trans_def) |
1995 apply (simp (no_asm_use) add: trans_def) |
1686 apply blast |
1996 apply (metis (no_types, hide_lams) Multiset.diff_right_commute Un_iff diff_single_trivial multi_drop_mem_not_eq) |
1687 apply (subgoal_tac "a \<in># I") |
1997 apply (subgoal_tac "a \<in># I") |
1688 apply (rule_tac x = "I - {#a#}" in exI) |
1998 apply (rule_tac x = "I - {#a#}" in exI) |
1689 apply (rule_tac x = "J + {#a#}" in exI) |
1999 apply (rule_tac x = "J + {#a#}" in exI) |
1690 apply (rule_tac x = "K + Ka" in exI) |
2000 apply (rule_tac x = "K + Ka" in exI) |
1691 apply (rule conjI) |
2001 apply (rule conjI) |
1692 apply (simp add: multiset_eq_iff split: nat_diff_split) |
2002 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1693 apply (rule conjI) |
2003 apply (rule conjI) |
1694 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp) |
2004 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp) |
1695 apply (simp add: multiset_eq_iff split: nat_diff_split) |
2005 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1696 apply (simp (no_asm_use) add: trans_def) |
2006 apply (simp (no_asm_use) add: trans_def) |
|
2007 apply (subgoal_tac "a \<in># (M0 + {#a#})") |
|
2008 apply (simp_all add: not_in_iff) |
1697 apply blast |
2009 apply blast |
1698 apply (subgoal_tac "a \<in># (M0 + {#a#})") |
2010 apply (metis add.comm_neutral add_diff_cancel_right' count_eq_zero_iff diff_single_trivial multi_self_add_other_not_self plus_multiset.rep_eq) |
1699 apply simp |
|
1700 apply (simp (no_asm)) |
|
1701 done |
2011 done |
1702 |
2012 |
1703 lemma one_step_implies_mult_aux: |
2013 lemma one_step_implies_mult_aux: |
1704 "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r) |
2014 "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r) |
1705 \<longrightarrow> (I + K, I + J) \<in> mult r" |
2015 \<longrightarrow> (I + K, I + J) \<in> mult r" |