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

   580 

   581 instantiation multiset :: (pt) pt

   582 begin

   583 

   584 definition

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

   586 

   587 instance 

   588 proof

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

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

   591     unfolding permute_multiset_def

   592     by (induct_tac M) (simp_all)

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

   594     unfolding permute_multiset_def

   595     by (induct_tac M) (simp_all)

   596 qed

   597 

   598 end

   599 

   600 lemma permute_multiset [simp]:

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

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

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

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

   605   unfolding permute_multiset_def

   606   by (simp_all)

   607 

   608 

   751   (* multisets *)

   752   permute_multiset

  1977 

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

  1979 

  1980 lemma set_of_eqvt[eqvt]:

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

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

  1983 

  1984 lemma supp_set_of:

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

  1986   apply (rule supp_fun_app_eqvt)

  1987   unfolding eqvt_def

  1988   apply(perm_simp)

  1989   apply(simp)

  1990   done

  1991 

  1992 lemma Union_finite_multiset:

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

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

  1995 proof - 

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

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

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

  1999     by (simp only: image_Collect)

  2000 qed

  2001 

  2002 lemma Union_supports_multiset:

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

  2004 proof -

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

  2006     unfolding permute_multiset_def 

  2007     apply(induct M)

  2008     apply(simp_all)

  2009     done

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

  2011     unfolding supports_def

  2012     apply(clarify)

  2013     apply(rule sw)

  2014     apply(rule swap_fresh_fresh)

  2015     apply(simp_all only: fresh_def)

  2016     apply(auto)

  2017     apply(metis neq0_conv)+

  2018     done

  2019 qed

  2020 

  2021 lemma Union_included_multiset:

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

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

  2024 proof -

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

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

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

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

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

  2030 qed

  2031 

  2032 lemma supp_of_multisets:

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

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

  2035 apply(rule subset_antisym)

  2036 apply(rule supp_is_subset)

  2037 apply(rule Union_supports_multiset)

  2038 apply(rule Union_finite_multiset)

  2039 apply(rule Union_included_multiset)

  2040 done

  2041 

  2042 lemma multisets_supp_finite:

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

  2044   shows "finite (supp M)"

  2045 by (simp only: supp_of_multisets Union_finite_multiset)

  2046 

  2047 lemma supp_of_multiset_union:

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

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

  2050   by (auto simp add: supp_of_multisets)

  2051 

  2052 lemma supp_empty_mset [simp]:

  2053   shows "supp {#} = {}"

  2054   unfolding supp_def

  2055   by simp

  2056 

  2057 instance multiset :: (fs) fs

  2058   apply (default)

  2059   apply (rule multisets_supp_finite)

  2060   done