src/HOL/Library/Multiset.thy
 changeset 58098 ff478d85129b parent 58035 177eeda93a8c child 58247 98d0f85d247f
1.1 --- a/src/HOL/Library/Multiset.thy	Fri Aug 29 11:24:31 2014 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Aug 30 11:15:47 2014 +0200
1.3 @@ -262,6 +262,18 @@
1.4    "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
1.5    by (rule_tac x = "M - {#x#}" in exI, simp)
1.8 +  assumes "c \<in># B" and "b \<noteq> c"
1.9 +  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
1.10 +proof -
1.11 +  from `c \<in># B` obtain A where B: "B = A + {#c#}"
1.12 +    by (blast dest: multi_member_split)
1.13 +  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
1.14 +  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.15 +    by (simp add: ac_simps)
1.16 +  then show ?thesis using B by simp
1.17 +qed
1.18 +
1.20  subsubsection {* Pointwise ordering induced by count *}
1.22 @@ -712,39 +724,18 @@
1.24  subsubsection {* Strong induction and subset induction for multisets *}
1.26 -text {* Well-foundedness of proper subset operator: *}
1.27 -
1.28 -text {* proper multiset subset *}
1.29 -
1.30 -definition
1.31 -  mset_less_rel :: "('a multiset * 'a multiset) set" where
1.32 -  "mset_less_rel = {(A,B). A < B}"
1.33 -
1.35 -  assumes "c \<in># B" and "b \<noteq> c"
1.36 -  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
1.37 -proof -
1.38 -  from `c \<in># B` obtain A where B: "B = A + {#c#}"
1.39 -    by (blast dest: multi_member_split)
1.40 -  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
1.41 -  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.42 -    by (simp add: ac_simps)
1.43 -  then show ?thesis using B by simp
1.44 -qed
1.45 -
1.46 -lemma wf_mset_less_rel: "wf mset_less_rel"
1.47 -apply (unfold mset_less_rel_def)
1.48 +text {* Well-foundedness of strict subset relation *}
1.49 +
1.50 +lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}"
1.51  apply (rule wf_measure [THEN wf_subset, where f1=size])
1.52  apply (clarsimp simp: measure_def inv_image_def mset_less_size)
1.53  done
1.55 -text {* The induction rules: *}
1.56 -
1.57  lemma full_multiset_induct [case_names less]:
1.58  assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
1.59  shows "P B"
1.60 -apply (rule wf_mset_less_rel [THEN wf_induct])
1.61 -apply (rule ih, auto simp: mset_less_rel_def)
1.62 +apply (rule wf_less_mset_rel [THEN wf_induct])
1.63 +apply (rule ih, auto)
1.64  done
1.66  lemma multi_subset_induct [consumes 2, case_names empty add]: