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.6  
     1.7 +lemma multiset_add_sub_el_shuffle: 
     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.19  
    1.20  subsubsection {* Pointwise ordering induced by count *}
    1.21  
    1.22 @@ -712,39 +724,18 @@
    1.23  
    1.24  subsubsection {* Strong induction and subset induction for multisets *}
    1.25  
    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.34 -lemma multiset_add_sub_el_shuffle: 
    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.54  
    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.65  
    1.66  lemma multi_subset_induct [consumes 2, case_names empty add]: