1.1 --- a/src/HOL/Library/Multiset.thy	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -572,47 +572,65 @@
     1.4  
     1.5  subsubsection {* Size *}
     1.6  
     1.7 -instantiation multiset :: (type) size
     1.8 -begin
     1.9 -
    1.10 -definition size_def:
    1.11 -  "size M = setsum (count M) (set_of M)"
    1.12 -
    1.13 +definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
    1.14 +
    1.15 +lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
    1.16 +  by (auto simp: wcount_def add_mult_distrib)
    1.17 +
    1.18 +definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
    1.19 +  "size_multiset f M = setsum (wcount f M) (set_of M)"
    1.20 +
    1.21 +lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
    1.22 +
    1.23 +instantiation multiset :: (type) size begin
    1.24 +definition size_multiset where
    1.25 +  size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)"
    1.26  instance ..
    1.27 -
    1.28  end
    1.29  
    1.30 +lemmas size_multiset_overloaded_eq =
    1.31 +  size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
    1.32 +
    1.33 +lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
    1.34 +by (simp add: size_multiset_def)
    1.35 +
    1.36  lemma size_empty [simp]: "size {#} = 0"
    1.37 -by (simp add: size_def)
    1.38 +by (simp add: size_multiset_overloaded_def)
    1.39 +
    1.40 +lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
    1.41 +by (simp add: size_multiset_eq)
    1.42  
    1.43  lemma size_single [simp]: "size {#b#} = 1"
    1.44 -by (simp add: size_def)
    1.45 -
    1.46 -lemma setsum_count_Int:
    1.47 -  "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
    1.48 +by (simp add: size_multiset_overloaded_def)
    1.49 +
    1.50 +lemma setsum_wcount_Int:
    1.51 +  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
    1.52  apply (induct rule: finite_induct)
    1.53   apply simp
    1.54 -apply (simp add: Int_insert_left set_of_def)
    1.55 +apply (simp add: Int_insert_left set_of_def wcount_def)
    1.56  done
    1.57  
    1.58 +lemma size_multiset_union [simp]:
    1.59 +  "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
    1.60 +apply (simp add: size_multiset_def setsum_Un_nat setsum_addf setsum_wcount_Int wcount_union)
    1.61 +apply (subst Int_commute)
    1.62 +apply (simp add: setsum_wcount_Int)
    1.63 +done
    1.64 +
    1.65  lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
    1.66 -apply (unfold size_def)
    1.67 -apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
    1.68 - prefer 2
    1.69 - apply (rule ext, simp)
    1.70 -apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
    1.71 -apply (subst Int_commute)
    1.72 -apply (simp (no_asm_simp) add: setsum_count_Int)
    1.73 -done
    1.74 +by (auto simp add: size_multiset_overloaded_def)
    1.75 +
    1.76 +lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})"
    1.77 +by (auto simp add: size_multiset_eq multiset_eq_iff)
    1.78  
    1.79  lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
    1.80 -by (auto simp add: size_def multiset_eq_iff)
    1.81 +by (auto simp add: size_multiset_overloaded_def)
    1.82  
    1.83  lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
    1.84  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
    1.85  
    1.86  lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
    1.87 -apply (unfold size_def)
    1.88 +apply (unfold size_multiset_overloaded_eq)
    1.89  apply (drule setsum_SucD)
    1.90  apply auto
    1.91  done
    1.92 @@ -1309,7 +1327,7 @@
    1.93  
    1.94  lemma size_eq_mcard:
    1.95    "size = mcard"
    1.96 -  by (simp add: fun_eq_iff size_def mcard_unfold_setsum)
    1.97 +  by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
    1.98  
    1.99  lemma mcard_multiset_of:
   1.100    "mcard (multiset_of xs) = length xs"
   1.101 @@ -3017,4 +3035,23 @@
   1.102  theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
   1.103           rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
   1.104  
   1.105 +
   1.106 +subsection {* Size setup *}
   1.107 +
   1.108 +lemma multiset_size_o_map: "size_multiset g \<circ> mmap f = size_multiset (g \<circ> f)"
   1.109 +apply (rule ext)
   1.110 +apply (unfold o_apply)
   1.111 +apply (induct_tac x)
   1.112 +apply auto
   1.113 +done
   1.114 +
   1.115 +setup {*
   1.116 +BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
   1.117 +  @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
   1.118 +    size_union}
   1.119 +  @{thms multiset_size_o_map}
   1.120 +*}
   1.121 +
   1.122 +hide_const (open) wcount
   1.123 +
   1.124  end