# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID 7f9b686bf30a3c3d0e56c8888775d7754a62a87e
# Parent  34f2fe40dc7b4b069c832296eda4df0ecbf14b4b
size function for multisets

diff -r 34f2fe40dc7b -r 7f9b686bf30a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -572,47 +572,65 @@
 
 subsubsection {* Size *}
 
-instantiation multiset :: (type) size
-begin
-
-definition size_def:
-  "size M = setsum (count M) (set_of M)"
-
+definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
+
+lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
+  by (auto simp: wcount_def add_mult_distrib)
+
+definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
+  "size_multiset f M = setsum (wcount f M) (set_of M)"
+
+lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
+
+instantiation multiset :: (type) size begin
+definition size_multiset where
+  size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)"
 instance ..
-
 end
 
+lemmas size_multiset_overloaded_eq =
+  size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
+
+lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
+by (simp add: size_multiset_def)
+
 lemma size_empty [simp]: "size {#} = 0"
-by (simp add: size_def)
+by (simp add: size_multiset_overloaded_def)
+
+lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
+by (simp add: size_multiset_eq)
 
 lemma size_single [simp]: "size {#b#} = 1"
-by (simp add: size_def)
-
-lemma setsum_count_Int:
-  "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
+by (simp add: size_multiset_overloaded_def)
+
+lemma setsum_wcount_Int:
+  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
 apply (induct rule: finite_induct)
  apply simp
-apply (simp add: Int_insert_left set_of_def)
+apply (simp add: Int_insert_left set_of_def wcount_def)
+done
+
+lemma size_multiset_union [simp]:
+  "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
+apply (simp add: size_multiset_def setsum_Un_nat setsum_addf setsum_wcount_Int wcount_union)
+apply (subst Int_commute)
+apply (simp add: setsum_wcount_Int)
 done
 
 lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
-apply (unfold size_def)
-apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
- prefer 2
- apply (rule ext, simp)
-apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
-apply (subst Int_commute)
-apply (simp (no_asm_simp) add: setsum_count_Int)
-done
+by (auto simp add: size_multiset_overloaded_def)
+
+lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})"
+by (auto simp add: size_multiset_eq multiset_eq_iff)
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-by (auto simp add: size_def multiset_eq_iff)
+by (auto simp add: size_multiset_overloaded_def)
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
 by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
 
 lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
-apply (unfold size_def)
+apply (unfold size_multiset_overloaded_eq)
 apply (drule setsum_SucD)
 apply auto
 done
@@ -1309,7 +1327,7 @@
 
 lemma size_eq_mcard:
   "size = mcard"
-  by (simp add: fun_eq_iff size_def mcard_unfold_setsum)
+  by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
 
 lemma mcard_multiset_of:
   "mcard (multiset_of xs) = length xs"
@@ -3017,4 +3035,23 @@
 theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
          rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
 
+
+subsection {* Size setup *}
+
+lemma multiset_size_o_map: "size_multiset g \<circ> mmap f = size_multiset (g \<circ> f)"
+apply (rule ext)
+apply (unfold o_apply)
+apply (induct_tac x)
+apply auto
+done
+
+setup {*
+BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
+  @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
+    size_union}
+  @{thms multiset_size_o_map}
+*}
+
+hide_const (open) wcount
+
 end