added lemma about 'mult', as suggested by Bertram Felgenhauer
authorblanchet
Tue Nov 29 08:32:44 2016 +0100 (2016-11-29)
changeset 64531166a2563e0ca
parent 64530 a720c3911308
child 64532 fc2835a932d9
added lemma about 'mult', as suggested by Bertram Felgenhauer
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Nov 28 15:09:23 2016 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Nov 29 08:32:44 2016 +0100
     1.3 @@ -2825,6 +2825,9 @@
     1.4    thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
     1.5  qed
     1.6  
     1.7 +lemmas mult_cancel_add_mset =
     1.8 +  mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
     1.9 +
    1.10  lemma mult_cancel_max:
    1.11    assumes "trans s" and "irrefl s"
    1.12    shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")