# HG changeset patch
# User haftmann
# Date 1449934320 -3600
# Node ID e15880ba58ac32be01fad20f92842828fb79ea69
# Parent  c43f87119d80578a5e1c1c2ee6eb1f770649fb8e
modernized

diff -r c43f87119d80 -r e15880ba58ac src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Dec 11 11:31:57 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 12 16:32:00 2015 +0100
@@ -1054,20 +1054,9 @@
 lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
-definition mset_set :: "'a set \<Rightarrow> 'a multiset"
-where
-  "mset_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
-
-interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
-rewrites
-  "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
-proof -
-  interpret comp_fun_commute "\<lambda>x M. {#x#} + M"
-    by standard (simp add: fun_eq_iff ac_simps)
-  show "folding (\<lambda>x M. {#x#} + M)"
-    by standard (fact comp_fun_commute)
-  from mset_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set" ..
-qed
+permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
+  defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
+  by standard (simp add: fun_eq_iff ac_simps)
 
 lemma count_mset_set [simp]:
   "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P")
@@ -1218,15 +1207,8 @@
 context comm_monoid_add
 begin
 
-definition msetsum :: "'a multiset \<Rightarrow> 'a"
-  where "msetsum = comm_monoid_mset.F plus 0"
-
 sublocale msetsum: comm_monoid_mset plus 0
-  rewrites "comm_monoid_mset.F plus 0 = msetsum"
-proof -
-  show "comm_monoid_mset plus 0" ..
-  from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
-qed
+  defines msetsum = msetsum.F ..
 
 lemma (in semiring_1) msetsum_replicate_mset [simp]:
   "msetsum (replicate_mset n a) = of_nat n * a"
@@ -1276,15 +1258,8 @@
 context comm_monoid_mult
 begin
 
-definition msetprod :: "'a multiset \<Rightarrow> 'a"
-  where "msetprod = comm_monoid_mset.F times 1"
-
 sublocale msetprod: comm_monoid_mset times 1
-  rewrites "comm_monoid_mset.F times 1 = msetprod"
-proof -
-  show "comm_monoid_mset times 1" ..
-  show "comm_monoid_mset.F times 1 = msetprod" using msetprod_def ..
-qed
+  defines msetprod = msetprod.F ..
 
 lemma msetprod_empty:
   "msetprod {#} = 1"