260 |
260 |
261 lemma multi_member_split: |
261 lemma multi_member_split: |
262 "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" |
262 "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" |
263 by (rule_tac x = "M - {#x#}" in exI, simp) |
263 by (rule_tac x = "M - {#x#}" in exI, simp) |
264 |
264 |
|
265 lemma multiset_add_sub_el_shuffle: |
|
266 assumes "c \<in># B" and "b \<noteq> c" |
|
267 shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}" |
|
268 proof - |
|
269 from `c \<in># B` obtain A where B: "B = A + {#c#}" |
|
270 by (blast dest: multi_member_split) |
|
271 have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp |
|
272 then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" |
|
273 by (simp add: ac_simps) |
|
274 then show ?thesis using B by simp |
|
275 qed |
|
276 |
265 |
277 |
266 subsubsection {* Pointwise ordering induced by count *} |
278 subsubsection {* Pointwise ordering induced by count *} |
267 |
279 |
268 instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le |
280 instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le |
269 begin |
281 begin |
710 qed |
722 qed |
711 |
723 |
712 |
724 |
713 subsubsection {* Strong induction and subset induction for multisets *} |
725 subsubsection {* Strong induction and subset induction for multisets *} |
714 |
726 |
715 text {* Well-foundedness of proper subset operator: *} |
727 text {* Well-foundedness of strict subset relation *} |
716 |
728 |
717 text {* proper multiset subset *} |
729 lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}" |
718 |
|
719 definition |
|
720 mset_less_rel :: "('a multiset * 'a multiset) set" where |
|
721 "mset_less_rel = {(A,B). A < B}" |
|
722 |
|
723 lemma multiset_add_sub_el_shuffle: |
|
724 assumes "c \<in># B" and "b \<noteq> c" |
|
725 shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}" |
|
726 proof - |
|
727 from `c \<in># B` obtain A where B: "B = A + {#c#}" |
|
728 by (blast dest: multi_member_split) |
|
729 have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp |
|
730 then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" |
|
731 by (simp add: ac_simps) |
|
732 then show ?thesis using B by simp |
|
733 qed |
|
734 |
|
735 lemma wf_mset_less_rel: "wf mset_less_rel" |
|
736 apply (unfold mset_less_rel_def) |
|
737 apply (rule wf_measure [THEN wf_subset, where f1=size]) |
730 apply (rule wf_measure [THEN wf_subset, where f1=size]) |
738 apply (clarsimp simp: measure_def inv_image_def mset_less_size) |
731 apply (clarsimp simp: measure_def inv_image_def mset_less_size) |
739 done |
732 done |
740 |
733 |
741 text {* The induction rules: *} |
|
742 |
|
743 lemma full_multiset_induct [case_names less]: |
734 lemma full_multiset_induct [case_names less]: |
744 assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B" |
735 assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B" |
745 shows "P B" |
736 shows "P B" |
746 apply (rule wf_mset_less_rel [THEN wf_induct]) |
737 apply (rule wf_less_mset_rel [THEN wf_induct]) |
747 apply (rule ih, auto simp: mset_less_rel_def) |
738 apply (rule ih, auto) |
748 done |
739 done |
749 |
740 |
750 lemma multi_subset_induct [consumes 2, case_names empty add]: |
741 lemma multi_subset_induct [consumes 2, case_names empty add]: |
751 assumes "F \<le> A" |
742 assumes "F \<le> A" |
752 and empty: "P {#}" |
743 and empty: "P {#}" |