--- a/Nominal/Nominal2_Base.thy	Sat Dec 17 17:51:01 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Feb 17 11:50:09 2012 +0000
@@ -576,6 +576,36 @@
 end
 
 
+subsection {* Permutations for @{typ "'a multiset"} *}
+
+instantiation multiset :: (pt) pt
+begin
+
+definition
+  "p \<bullet> M = {# p \<bullet> x. x :# M #}"
+
+instance 
+proof
+  fix M :: "'a multiset" and p q :: "perm"
+  show "0 \<bullet> M = M" 
+    unfolding permute_multiset_def
+    by (induct_tac M) (simp_all)
+  show "(p + q) \<bullet> M = p \<bullet> q \<bullet> M" 
+    unfolding permute_multiset_def
+    by (induct_tac M) (simp_all)
+qed
+
+end
+
+lemma permute_multiset [simp]:
+  fixes M N::"('a::pt) multiset"
+  shows "(p \<bullet> {#}) = ({#} ::('a::pt) multiset)"
+  and   "(p \<bullet> {# x #}) = {# p \<bullet> x #}"
+  and   "(p \<bullet> (M + N)) = (p \<bullet> M) + (p \<bullet> N)"
+  unfolding permute_multiset_def
+  by (simp_all)
+
+
 subsection {* Permutations for @{typ "'a fset"} *}
 
 lemma permute_fset_rsp[quot_respect]:
@@ -718,6 +748,8 @@
   (* fsets *)
   permute_fset fset_eqvt
 
+  (* multisets *)
+  permute_multiset
 
 
 subsection {* perm_simp infrastructure *}
@@ -1943,6 +1975,90 @@
 by (simp add: supp_set)
 
 
+subsection {* Type @{typ "'a multiset"} is finitely supported *}
+
+lemma set_of_eqvt[eqvt]:
+  shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+by (induct M) (simp_all add: insert_eqvt empty_eqvt)
+
+lemma supp_set_of:
+  shows "supp (set_of M) \<subseteq> supp M"
+  apply (rule supp_fun_app_eqvt)
+  unfolding eqvt_def
+  apply(perm_simp)
+  apply(simp)
+  done
+
+lemma Union_finite_multiset:
+  fixes M::"'a::fs multiset"
+  shows "finite (\<Union>{supp x | x. x \<in># M})"
+proof - 
+  have "finite (\<Union>(supp ` {x. x \<in># M}))"
+    by (induct M) (simp_all add: Collect_imp_eq Collect_neg_eq finite_supp)
+  then show "finite (\<Union>{supp x | x. x \<in># M})"
+    by (simp only: image_Collect)
+qed
+
+lemma Union_supports_multiset:
+  shows "\<Union>{supp x | x. x :# M} supports M"
+proof -
+  have sw: "\<And>a b. ((\<And>x. x :# M \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x) \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> M = M)"
+    unfolding permute_multiset_def 
+    apply(induct M)
+    apply(simp_all)
+    done
+  show "(\<Union>{supp x | x. x :# M}) supports M"
+    unfolding supports_def
+    apply(clarify)
+    apply(rule sw)
+    apply(rule swap_fresh_fresh)
+    apply(simp_all only: fresh_def)
+    apply(auto)
+    apply(metis neq0_conv)+
+    done
+qed
+
+lemma Union_included_multiset:
+  fixes M::"('a::fs multiset)" 
+  shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
+proof -
+  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
+  also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
+  also have "... = supp (set_of M)" by (simp add: subst supp_of_finite_sets)
+  also have " ... \<subseteq> supp M" by (rule supp_set_of)
+  finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
+qed
+
+lemma supp_of_multisets:
+  fixes M::"('a::fs multiset)"
+  shows "(supp M) = (\<Union>{supp x | x. x :# M})"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_multiset)
+apply(rule Union_finite_multiset)
+apply(rule Union_included_multiset)
+done
+
+lemma multisets_supp_finite:
+  fixes M::"('a::fs multiset)"
+  shows "finite (supp M)"
+by (simp only: supp_of_multisets Union_finite_multiset)
+
+lemma supp_of_multiset_union:
+  fixes M N::"('a::fs) multiset"
+  shows "supp (M + N) = supp M \<union> supp N"
+  by (auto simp add: supp_of_multisets)
+
+lemma supp_empty_mset [simp]:
+  shows "supp {#} = {}"
+  unfolding supp_def
+  by simp
+
+instance multiset :: (fs) fs
+  apply (default)
+  apply (rule multisets_supp_finite)
+  done
+
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
 lemma supp_fset [simp]: