586 subsection {* Permutations for @{typ "'a multiset"} *}

   587 

   588 instantiation multiset :: (pt) pt

   589 begin

   590 

   591 definition

   592   "p \<bullet> M = {# p \<bullet> x. x :# M #}"

   593 

   594 instance 

   595 proof

   596   fix M :: "'a multiset" and p q :: "perm"

   597   show "0 \<bullet> M = M" 

   598     unfolding permute_multiset_def

   599     by (induct_tac M) (simp_all)

   600   show "(p + q) \<bullet> M = p \<bullet> q \<bullet> M" 

   601     unfolding permute_multiset_def

   602     by (induct_tac M) (simp_all)

   603 qed

   604 

   605 end

   606 

   607 lemma permute_multiset [simp]:

   608   fixes M N::"('a::pt) multiset"

   609   shows "(p \<bullet> {#}) = ({#} ::('a::pt) multiset)"

   610   and   "(p \<bullet> {# x #}) = {# p \<bullet> x #}"

   611   and   "(p \<bullet> (M + N)) = (p \<bullet> M) + (p \<bullet> N)"

   612   unfolding permute_multiset_def

   613   by (simp_all)

   614 

  2008 

  2009 subsection {* Type @{typ "'a multiset"} is finitely supported *}

  2010 

  2011 lemma set_of_eqvt[eqvt]:

  2012   shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"

  2013 by (induct M) (simp_all add: insert_eqvt empty_eqvt)

  2014 

  2015 lemma supp_set_of:

  2016   shows "supp (set_of M) \<subseteq> supp M"

  2017   apply (rule supp_fun_app_eqvt)

  2018   unfolding eqvt_def

  2019   apply(perm_simp)

  2020   apply(simp)

  2021   done

  2022 

  2023 lemma Union_finite_multiset:

  2024   fixes M::"'a::fs multiset"

  2025   shows "finite (\<Union>{supp x | x. x \<in># M})"

  2026 proof - 

  2027   have "finite (\<Union>(supp ` {x. x \<in># M}))"

  2028     by (induct M) (simp_all add: Collect_imp_eq Collect_neg_eq finite_supp)

  2029   then show "finite (\<Union>{supp x | x. x \<in># M})"

  2030     by (simp only: image_Collect)

  2031 qed

  2032 

  2033 lemma Union_supports_multiset:

  2034   shows "\<Union>{supp x | x. x :# M} supports M"

  2035 proof -

  2036   have sw: "\<And>a b. ((\<And>x. x :# M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"

  2037     unfolding permute_multiset_def 

  2038     apply(induct M)

  2039     apply(simp_all)

  2040     done

  2041   show "(\<Union>{supp x | x. x :# M}) supports M"

  2042     unfolding supports_def

  2043     apply(clarify)

  2044     apply(rule sw)

  2045     apply(rule swap_fresh_fresh)

  2046     apply(simp_all only: fresh_def)

  2047     apply(auto)

  2048     apply(metis neq0_conv)+

  2049     done

  2050 qed

  2051 

  2052 lemma Union_included_multiset:

  2053   fixes M::"('a::fs multiset)" 

  2054   shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"

  2055 proof -

  2056   have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp

  2057   also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto

  2058   also have "... = supp (set_of M)" by (simp add: subst supp_of_finite_sets)

  2059   also have " ... \<subseteq> supp M" by (rule supp_set_of)

  2060   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .

  2061 qed

  2062 

  2063 lemma supp_of_multisets:

  2064   fixes M::"('a::fs multiset)"

  2065   shows "(supp M) = (\<Union>{supp x | x. x :# M})"

  2066 apply(rule subset_antisym)

  2067 apply(rule supp_is_subset)

  2068 apply(rule Union_supports_multiset)

  2069 apply(rule Union_finite_multiset)

  2070 apply(rule Union_included_multiset)

  2071 done

  2072 

  2073 lemma multisets_supp_finite:

  2074   fixes M::"('a::fs multiset)"

  2075   shows "finite (supp M)"

  2076 by (simp only: supp_of_multisets Union_finite_multiset)

  2077 

  2078 lemma supp_of_multiset_union:

  2079   fixes M N::"('a::fs) multiset"

  2080   shows "supp (M + N) = supp M \<union> supp N"

  2081   by (auto simp add: supp_of_multisets)

  2082 

  2083 lemma supp_empty_mset [simp]:

  2084   shows "supp {#} = {}"

  2085   unfolding supp_def

  2086   by simp

  2087 

  2088 instance multiset :: (fs) fs

  2089   apply (default)

  2090   apply (rule multisets_supp_finite)

  2091   done