117 |
109 |
118 |
110 |
119 subsubsection {* Difference *} |
111 subsubsection {* Difference *} |
120 |
112 |
121 theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |
113 theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |
122 apply (simp add: Mempty_def diff_def) |
114 by (simp add: Mempty_def diff_def) |
123 done |
|
124 |
115 |
125 theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M" |
116 theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M" |
126 apply (simp add: union_def diff_def) |
117 by (simp add: union_def diff_def) |
127 done |
|
128 |
118 |
129 |
119 |
130 subsubsection {* Count of elements *} |
120 subsubsection {* Count of elements *} |
131 |
121 |
132 theorem count_empty [simp]: "count {#} a = 0" |
122 theorem count_empty [simp]: "count {#} a = 0" |
133 apply (simp add: count_def Mempty_def) |
123 by (simp add: count_def Mempty_def) |
134 done |
|
135 |
124 |
136 theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" |
125 theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" |
137 apply (simp add: count_def single_def) |
126 by (simp add: count_def single_def) |
138 done |
|
139 |
127 |
140 theorem count_union [simp]: "count (M + N) a = count M a + count N a" |
128 theorem count_union [simp]: "count (M + N) a = count M a + count N a" |
141 apply (simp add: count_def union_def) |
129 by (simp add: count_def union_def) |
142 done |
|
143 |
130 |
144 theorem count_diff [simp]: "count (M - N) a = count M a - count N a" |
131 theorem count_diff [simp]: "count (M - N) a = count M a - count N a" |
145 apply (simp add: count_def diff_def) |
132 by (simp add: count_def diff_def) |
146 done |
|
147 |
133 |
148 |
134 |
149 subsubsection {* Set of elements *} |
135 subsubsection {* Set of elements *} |
150 |
136 |
151 theorem set_of_empty [simp]: "set_of {#} = {}" |
137 theorem set_of_empty [simp]: "set_of {#} = {}" |
152 apply (simp add: set_of_def) |
138 by (simp add: set_of_def) |
153 done |
|
154 |
139 |
155 theorem set_of_single [simp]: "set_of {#b#} = {b}" |
140 theorem set_of_single [simp]: "set_of {#b#} = {b}" |
156 apply (simp add: set_of_def) |
141 by (simp add: set_of_def) |
157 done |
|
158 |
142 |
159 theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" |
143 theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" |
160 apply (auto simp add: set_of_def) |
144 by (auto simp add: set_of_def) |
161 done |
|
162 |
145 |
163 theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" |
146 theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" |
164 apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) |
147 by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) |
165 done |
|
166 |
148 |
167 theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" |
149 theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" |
168 apply (auto simp add: set_of_def) |
150 by (auto simp add: set_of_def) |
169 done |
|
170 |
151 |
171 |
152 |
172 subsubsection {* Size *} |
153 subsubsection {* Size *} |
173 |
154 |
174 theorem size_empty [simp]: "size {#} = 0" |
155 theorem size_empty [simp]: "size {#} = 0" |
175 apply (simp add: size_def) |
156 by (simp add: size_def) |
176 done |
|
177 |
157 |
178 theorem size_single [simp]: "size {#b#} = 1" |
158 theorem size_single [simp]: "size {#b#} = 1" |
179 apply (simp add: size_def) |
159 by (simp add: size_def) |
180 done |
|
181 |
160 |
182 theorem finite_set_of [iff]: "finite (set_of M)" |
161 theorem finite_set_of [iff]: "finite (set_of M)" |
183 apply (cut_tac x = M in Rep_multiset) |
162 apply (cut_tac x = M in Rep_multiset) |
184 apply (simp add: multiset_def set_of_def count_def) |
163 apply (simp add: multiset_def set_of_def count_def) |
185 done |
164 done |
186 |
165 |
187 theorem setsum_count_Int: |
166 theorem setsum_count_Int: |
188 "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" |
167 "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" |
189 apply (erule finite_induct) |
168 apply (erule finite_induct, simp) |
190 apply simp |
|
191 apply (simp add: Int_insert_left set_of_def) |
169 apply (simp add: Int_insert_left set_of_def) |
192 done |
170 done |
193 |
171 |
194 theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" |
172 theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" |
195 apply (unfold size_def) |
173 apply (unfold size_def) |
196 apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") |
174 apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") |
197 prefer 2 |
175 prefer 2 |
198 apply (rule ext) |
176 apply (rule ext, simp) |
199 apply simp |
|
200 apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int) |
177 apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int) |
201 apply (subst Int_commute) |
178 apply (subst Int_commute) |
202 apply (simp (no_asm_simp) add: setsum_count_Int) |
179 apply (simp (no_asm_simp) add: setsum_count_Int) |
203 done |
180 done |
204 |
181 |
205 theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" |
182 theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" |
206 apply (unfold size_def Mempty_def count_def) |
183 apply (unfold size_def Mempty_def count_def, auto) |
207 apply auto |
|
208 apply (simp add: set_of_def count_def expand_fun_eq) |
184 apply (simp add: set_of_def count_def expand_fun_eq) |
209 done |
185 done |
210 |
186 |
211 theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" |
187 theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" |
212 apply (unfold size_def) |
188 apply (unfold size_def) |
213 apply (drule setsum_SucD) |
189 apply (drule setsum_SucD, auto) |
214 apply auto |
|
215 done |
190 done |
216 |
191 |
217 |
192 |
218 subsubsection {* Equality of multisets *} |
193 subsubsection {* Equality of multisets *} |
219 |
194 |
220 theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" |
195 theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" |
221 apply (simp add: count_def expand_fun_eq) |
196 by (simp add: count_def expand_fun_eq) |
222 done |
|
223 |
197 |
224 theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" |
198 theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" |
225 apply (simp add: single_def Mempty_def expand_fun_eq) |
199 by (simp add: single_def Mempty_def expand_fun_eq) |
226 done |
|
227 |
200 |
228 theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" |
201 theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" |
229 apply (auto simp add: single_def expand_fun_eq) |
202 by (auto simp add: single_def expand_fun_eq) |
230 done |
|
231 |
203 |
232 theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" |
204 theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" |
233 apply (auto simp add: union_def Mempty_def expand_fun_eq) |
205 by (auto simp add: union_def Mempty_def expand_fun_eq) |
234 done |
|
235 |
206 |
236 theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" |
207 theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" |
237 apply (auto simp add: union_def Mempty_def expand_fun_eq) |
208 by (auto simp add: union_def Mempty_def expand_fun_eq) |
238 done |
|
239 |
209 |
240 theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" |
210 theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" |
241 apply (simp add: union_def expand_fun_eq) |
211 by (simp add: union_def expand_fun_eq) |
242 done |
|
243 |
212 |
244 theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" |
213 theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" |
245 apply (simp add: union_def expand_fun_eq) |
214 by (simp add: union_def expand_fun_eq) |
246 done |
|
247 |
215 |
248 theorem union_is_single: |
216 theorem union_is_single: |
249 "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" |
217 "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" |
250 apply (unfold Mempty_def single_def union_def) |
218 apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq) |
251 apply (simp add: add_is_1 expand_fun_eq) |
|
252 apply blast |
219 apply blast |
253 done |
220 done |
254 |
221 |
255 theorem single_is_union: |
222 theorem single_is_union: |
256 "({#a#} = M + N) = |
223 "({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" |
257 ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" |
|
258 apply (unfold Mempty_def single_def union_def) |
224 apply (unfold Mempty_def single_def union_def) |
259 apply (simp add: add_is_1 one_is_add expand_fun_eq) |
225 apply (simp add: add_is_1 one_is_add expand_fun_eq) |
260 apply (blast dest: sym) |
226 apply (blast dest: sym) |
261 done |
227 done |
262 |
228 |
263 theorem add_eq_conv_diff: |
229 theorem add_eq_conv_diff: |
264 "(M + {#a#} = N + {#b#}) = |
230 "(M + {#a#} = N + {#b#}) = |
265 (M = N \<and> a = b \<or> |
231 (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})" |
266 M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})" |
|
267 apply (unfold single_def union_def diff_def) |
232 apply (unfold single_def union_def diff_def) |
268 apply (simp (no_asm) add: expand_fun_eq) |
233 apply (simp (no_asm) add: expand_fun_eq) |
269 apply (rule conjI) |
234 apply (rule conjI, force, safe, simp_all) |
270 apply force |
|
271 apply safe |
|
272 apply simp_all |
|
273 apply (simp add: eq_sym_conv) |
235 apply (simp add: eq_sym_conv) |
274 done |
236 done |
275 |
237 |
276 (* |
238 (* |
277 val prems = Goal |
239 val prems = Goal |
278 "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; |
240 "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; |
279 by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")] |
241 by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")] |
280 measure_induct 1); |
242 measure_induct 1); |
281 by (Clarify_tac 1); |
243 by (Clarify_tac 1) |
282 by (resolve_tac prems 1); |
244 by (resolve_tac prems 1) |
283 by (assume_tac 1); |
245 by (assume_tac 1) |
284 by (Clarify_tac 1); |
246 by (Clarify_tac 1) |
285 by (subgoal_tac "finite G" 1); |
247 by (subgoal_tac "finite G" 1) |
286 by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); |
248 by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); |
287 by (etac allE 1); |
249 by (etac allE 1) |
288 by (etac impE 1); |
250 by (etac impE 1) |
289 by (Blast_tac 2); |
251 by (Blast_tac 2) |
290 by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); |
252 by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); |
291 no_qed(); |
253 no_qed(); |
292 val lemma = result(); |
254 val lemma = result(); |
293 |
255 |
294 val prems = Goal |
256 val prems = Goal |
386 |
337 |
387 |
338 |
388 lemma MCollect_preserves_multiset: |
339 lemma MCollect_preserves_multiset: |
389 "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" |
340 "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" |
390 apply (simp add: multiset_def) |
341 apply (simp add: multiset_def) |
391 apply (rule finite_subset) |
342 apply (rule finite_subset, auto) |
392 apply auto |
|
393 done |
343 done |
394 |
344 |
395 theorem count_MCollect [simp]: |
345 theorem count_MCollect [simp]: |
396 "count {# x:M. P x #} a = (if P a then count M a else 0)" |
346 "count {# x:M. P x #} a = (if P a then count M a else 0)" |
397 apply (unfold count_def MCollect_def) |
347 by (simp add: count_def MCollect_def MCollect_preserves_multiset) |
398 apply (simp add: MCollect_preserves_multiset) |
|
399 done |
|
400 |
348 |
401 theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}" |
349 theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}" |
402 apply (auto simp add: set_of_def) |
350 by (auto simp add: set_of_def) |
403 done |
|
404 |
351 |
405 theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}" |
352 theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}" |
406 apply (subst multiset_eq_conv_count_eq) |
353 by (subst multiset_eq_conv_count_eq, auto) |
407 apply auto |
|
408 done |
|
409 |
354 |
410 declare Rep_multiset_inject [symmetric, simp del] |
355 declare Rep_multiset_inject [symmetric, simp del] |
411 declare multiset_typedef [simp del] |
356 declare multiset_typedef [simp del] |
412 |
357 |
413 theorem add_eq_conv_ex: |
358 theorem add_eq_conv_ex: |
414 "(M + {#a#} = N + {#b#}) = |
359 "(M + {#a#} = N + {#b#}) = |
415 (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" |
360 (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" |
416 apply (auto simp add: add_eq_conv_diff) |
361 by (auto simp add: add_eq_conv_diff) |
417 done |
|
418 |
362 |
419 |
363 |
420 subsection {* Multiset orderings *} |
364 subsection {* Multiset orderings *} |
421 |
365 |
422 subsubsection {* Well-foundedness *} |
366 subsubsection {* Well-foundedness *} |
555 subsubsection {* Closure-free presentation *} |
499 subsubsection {* Closure-free presentation *} |
556 |
500 |
557 (*Badly needed: a linear arithmetic procedure for multisets*) |
501 (*Badly needed: a linear arithmetic procedure for multisets*) |
558 |
502 |
559 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})" |
503 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})" |
560 apply (simp add: multiset_eq_conv_count_eq) |
504 by (simp add: multiset_eq_conv_count_eq) |
561 done |
|
562 |
505 |
563 text {* One direction. *} |
506 text {* One direction. *} |
564 |
507 |
565 lemma mult_implies_one_step: |
508 lemma mult_implies_one_step: |
566 "trans r ==> (M, N) \<in> mult r ==> |
509 "trans r ==> (M, N) \<in> mult r ==> |
567 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> |
510 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> |
568 (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" |
511 (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" |
569 apply (unfold mult_def mult1_def set_of_def) |
512 apply (unfold mult_def mult1_def set_of_def) |
570 apply (erule converse_trancl_induct) |
513 apply (erule converse_trancl_induct, clarify) |
571 apply clarify |
514 apply (rule_tac x = M0 in exI, simp, clarify) |
572 apply (rule_tac x = M0 in exI) |
|
573 apply simp |
|
574 apply clarify |
|
575 apply (case_tac "a :# K") |
515 apply (case_tac "a :# K") |
576 apply (rule_tac x = I in exI) |
516 apply (rule_tac x = I in exI) |
577 apply (simp (no_asm)) |
517 apply (simp (no_asm)) |
578 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
518 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
579 apply (simp (no_asm_simp) add: union_assoc [symmetric]) |
519 apply (simp (no_asm_simp) add: union_assoc [symmetric]) |
586 apply (rule_tac x = "J + {#a#}" in exI) |
526 apply (rule_tac x = "J + {#a#}" in exI) |
587 apply (rule_tac x = "K + Ka" in exI) |
527 apply (rule_tac x = "K + Ka" in exI) |
588 apply (rule conjI) |
528 apply (rule conjI) |
589 apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) |
529 apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) |
590 apply (rule conjI) |
530 apply (rule conjI) |
591 apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong) |
531 apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp) |
592 apply simp |
|
593 apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) |
532 apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) |
594 apply (simp (no_asm_use) add: trans_def) |
533 apply (simp (no_asm_use) add: trans_def) |
595 apply blast |
534 apply blast |
596 apply (subgoal_tac "a :# (M0 + {#a#})") |
535 apply (subgoal_tac "a :# (M0 + {#a#})") |
597 apply simp |
536 apply simp |
598 apply (simp (no_asm)) |
537 apply (simp (no_asm)) |
599 done |
538 done |
600 |
539 |
601 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}" |
540 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}" |
602 apply (simp add: multiset_eq_conv_count_eq) |
541 by (simp add: multiset_eq_conv_count_eq) |
603 done |
|
604 |
542 |
605 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" |
543 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" |
606 apply (erule size_eq_Suc_imp_elem [THEN exE]) |
544 apply (erule size_eq_Suc_imp_elem [THEN exE]) |
607 apply (drule elem_imp_eq_diff_union) |
545 apply (drule elem_imp_eq_diff_union, auto) |
608 apply auto |
|
609 done |
546 done |
610 |
547 |
611 lemma one_step_implies_mult_aux: |
548 lemma one_step_implies_mult_aux: |
612 "trans r ==> |
549 "trans r ==> |
613 \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)) |
550 \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)) |
614 --> (I + K, I + J) \<in> mult r" |
551 --> (I + K, I + J) \<in> mult r" |
615 apply (induct_tac n) |
552 apply (induct_tac n, auto) |
616 apply auto |
553 apply (frule size_eq_Suc_imp_eq_union, clarify) |
617 apply (frule size_eq_Suc_imp_eq_union) |
554 apply (rename_tac "J'", simp) |
618 apply clarify |
555 apply (erule notE, auto) |
619 apply (rename_tac "J'") |
|
620 apply simp |
|
621 apply (erule notE) |
|
622 apply auto |
|
623 apply (case_tac "J' = {#}") |
556 apply (case_tac "J' = {#}") |
624 apply (simp add: mult_def) |
557 apply (simp add: mult_def) |
625 apply (rule r_into_trancl) |
558 apply (rule r_into_trancl) |
626 apply (simp add: mult1_def set_of_def) |
559 apply (simp add: mult1_def set_of_def, blast) |
627 apply blast |
|
628 txt {* Now we know @{term "J' \<noteq> {#}"}. *} |
560 txt {* Now we know @{term "J' \<noteq> {#}"}. *} |
629 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) |
561 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) |
630 apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) |
562 apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) |
631 apply (erule ssubst) |
563 apply (erule ssubst) |
632 apply (simp add: Ball_def) |
564 apply (simp add: Ball_def, auto) |
633 apply auto |
|
634 apply (subgoal_tac |
565 apply (subgoal_tac |
635 "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #}, |
566 "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #}, |
636 (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r") |
567 (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r") |
637 prefer 2 |
568 prefer 2 |
638 apply force |
569 apply force |
792 apply (case_tac "M = {#}") |
708 apply (case_tac "M = {#}") |
793 prefer 2 |
709 prefer 2 |
794 apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") |
710 apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") |
795 prefer 2 |
711 prefer 2 |
796 apply (rule one_step_implies_mult) |
712 apply (rule one_step_implies_mult) |
797 apply (simp only: trans_def) |
713 apply (simp only: trans_def, auto) |
798 apply auto |
|
799 done |
714 done |
800 |
715 |
801 theorem union_upper1: "A <= A + (B::'a::order multiset)" |
716 theorem union_upper1: "A <= A + (B::'a::order multiset)" |
802 apply (subgoal_tac "A + {#} <= A + B") |
717 proof - |
803 prefer 2 |
718 have "A + {#} <= A + B" by (blast intro: union_le_mono) |
804 apply (rule union_le_mono) |
719 thus ?thesis by simp |
805 apply auto |
720 qed |
806 done |
|
807 |
721 |
808 theorem union_upper2: "B <= A + (B::'a::order multiset)" |
722 theorem union_upper2: "B <= A + (B::'a::order multiset)" |
809 apply (subst union_commute, rule union_upper1) |
723 by (subst union_commute, rule union_upper1) |
810 done |
724 |
|
725 |
|
726 subsection {* Link with lists *} |
|
727 |
|
728 consts |
|
729 multiset_of :: "'a list \<Rightarrow> 'a multiset" |
|
730 primrec |
|
731 "multiset_of [] = {#}" |
|
732 "multiset_of (a # x) = multiset_of x + {# a #}" |
|
733 |
|
734 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])" |
|
735 by (induct_tac x, auto) |
|
736 |
|
737 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])" |
|
738 by (induct_tac x, auto) |
|
739 |
|
740 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x" |
|
741 by (induct_tac x, auto) |
|
742 |
|
743 lemma multset_of_append[simp]: |
|
744 "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" |
|
745 by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) |
|
746 |
|
747 lemma surj_multiset_of: "surj multiset_of" |
|
748 apply (unfold surj_def, rule allI) |
|
749 apply (rule_tac M=y in multiset_induct, auto) |
|
750 apply (rule_tac x = "x # xa" in exI, auto) |
|
751 done |
|
752 |
|
753 lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}" |
|
754 by (induct_tac x, auto) |
|
755 |
|
756 lemma distinct_count_atmost_1: |
|
757 "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" |
|
758 apply ( induct_tac x, simp, rule iffI, simp_all) |
|
759 apply (rule conjI) |
|
760 apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) |
|
761 apply (erule_tac x=a in allE, simp, clarify) |
|
762 apply (erule_tac x=aa in allE, simp) |
|
763 done |
|
764 |
|
765 lemma set_eq_iff_multiset_of_eq_distinct: |
|
766 "\<lbrakk>distinct x; distinct y\<rbrakk> |
|
767 \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)" |
|
768 by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) |
|
769 |
|
770 lemma set_eq_iff_multiset_of_remdups_eq: |
|
771 "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" |
|
772 apply (rule iffI) |
|
773 apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) |
|
774 apply (drule distinct_remdups[THEN distinct_remdups |
|
775 [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) |
|
776 apply simp |
|
777 done |
|
778 |
|
779 |
|
780 subsection {* Pointwise ordering induced by count *} |
|
781 |
|
782 consts |
|
783 mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool" |
|
784 |
|
785 syntax |
|
786 "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" ("_ \<le># _" [50,51] 50) |
|
787 translations |
|
788 "x \<le># y" == "mset_le x y" |
|
789 |
|
790 defs |
|
791 mset_le_def: "xs \<le># ys == (! a. count xs a \<le> count ys a)" |
|
792 |
|
793 lemma mset_le_refl[simp]: "xs \<le># xs" |
|
794 by (unfold mset_le_def, auto) |
|
795 |
|
796 lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs" |
|
797 by (unfold mset_le_def, fast intro: order_trans) |
|
798 |
|
799 lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys" |
|
800 apply (unfold mset_le_def) |
|
801 apply (rule multiset_eq_conv_count_eq[THEN iffD2]) |
|
802 apply (blast intro: order_antisym) |
|
803 done |
|
804 |
|
805 lemma mset_le_exists_conv: |
|
806 "(xs \<le># ys) = (? zs. ys = xs + zs)" |
|
807 apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) |
|
808 apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) |
|
809 done |
|
810 |
|
811 lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)" |
|
812 by (unfold mset_le_def, auto) |
|
813 |
|
814 lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)" |
|
815 by (unfold mset_le_def, auto) |
|
816 |
|
817 lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" |
|
818 apply (unfold mset_le_def, auto) |
|
819 apply (erule_tac x=a in allE)+ |
|
820 apply auto |
|
821 done |
|
822 |
|
823 lemma mset_le_add_left[simp]: "xs \<le># xs + ys" |
|
824 by (unfold mset_le_def, auto) |
|
825 |
|
826 lemma mset_le_add_right[simp]: "ys \<le># xs + ys" |
|
827 by (unfold mset_le_def, auto) |
|
828 |
|
829 lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x" |
|
830 by (induct_tac x, auto, rule mset_le_trans, auto) |
811 |
831 |
812 end |
832 end |