src/HOL/Library/Multiset.thy
 changeset 54868 bab6cade3cc5 parent 54295 45a5523d4a63 child 55129 26bd1cba3ab5
```     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Dec 26 22:47:49 2013 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Dec 27 14:35:14 2013 +0100
1.3 @@ -1159,15 +1159,14 @@
1.4  notation times (infixl "*" 70)
1.5  notation Groups.one ("1")
1.6
1.7 -definition (in comm_monoid_add) msetsum :: "'a multiset \<Rightarrow> 'a"
1.9 +begin
1.10 +
1.11 +definition msetsum :: "'a multiset \<Rightarrow> 'a"
1.12  where
1.13    "msetsum = comm_monoid_mset.F plus 0"
1.14
1.15 -definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
1.16 -where
1.17 -  "msetprod = comm_monoid_mset.F times 1"
1.18 -
1.19 -sublocale comm_monoid_add < msetsum!: comm_monoid_mset plus 0
1.20 +sublocale msetsum!: comm_monoid_mset plus 0
1.21  where
1.22    "comm_monoid_mset.F plus 0 = msetsum"
1.23  proof -
1.24 @@ -1175,9 +1174,6 @@
1.25    from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
1.26  qed
1.27
1.29 -begin
1.30 -
1.31  lemma setsum_unfold_msetsum:
1.32    "setsum f A = msetsum (image_mset f (multiset_of_set A))"
1.33    by (cases "finite A") (induct A rule: finite_induct, simp_all)
1.34 @@ -1203,7 +1199,14 @@
1.35  translations
1.36    "SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
1.37
1.38 -sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1
1.39 +context comm_monoid_mult
1.40 +begin
1.41 +
1.42 +definition msetprod :: "'a multiset \<Rightarrow> 'a"
1.43 +where
1.44 +  "msetprod = comm_monoid_mset.F times 1"
1.45 +
1.46 +sublocale msetprod!: comm_monoid_mset times 1
1.47  where
1.48    "comm_monoid_mset.F times 1 = msetprod"
1.49  proof -
1.50 @@ -1211,9 +1214,6 @@
1.51    from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" ..
1.52  qed
1.53
1.54 -context comm_monoid_mult
1.55 -begin
1.56 -
1.57  lemma msetprod_empty:
1.58    "msetprod {#} = 1"
1.59    by (fact msetprod.empty)
```