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.8 +context comm_monoid_add
     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.28 -context comm_monoid_add
    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)