src/HOL/Library/Multiset.thy
changeset 67656 59feb83c6ab9
parent 67398 5eb932e604a2
child 68249 949d93804740
equal deleted inserted replaced
67655:8f4810b9d9d1 67656:59feb83c6ab9
  2405   using assms by induct simp_all
  2405   using assms by induct simp_all
  2406 
  2406 
  2407 lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
  2407 lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
  2408   by (induction M) auto
  2408   by (induction M) auto
  2409 
  2409 
       
  2410 lemma Union_image_single_mset[simp]: "\<Union># (image_mset (\<lambda>x. {#x#}) m) = m"
       
  2411 by(induction m) auto
       
  2412 
  2410 
  2413 
  2411 context comm_monoid_mult
  2414 context comm_monoid_mult
  2412 begin
  2415 begin
  2413 
  2416 
  2414 sublocale prod_mset: comm_monoid_mset times 1
  2417 sublocale prod_mset: comm_monoid_mset times 1