merged

--- a/NEWS	Tue Apr 07 17:24:55 2015 +0200
+++ b/NEWS	Tue Apr 07 18:22:06 2015 +0200
@@ -302,6 +302,7 @@
   - Renamed
       in_multiset_of ~> in_multiset_in_set
     INCOMPATIBILITY.
+  - Removed mcard, is equal to size.
   - Added attributes:
       image_mset.id [simp]
       image_mset_id [simp]

--- a/src/HOL/Library/DAList_Multiset.thy	Tue Apr 07 17:24:55 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Tue Apr 07 18:22:06 2015 +0200
@@ -28,7 +28,7 @@
 
 lemma [code, code del]: "count = count" ..
 
-lemma [code, code del]: "mcard = mcard" ..
+lemma [code, code del]: "size = (size :: _ multiset \<Rightarrow> nat)" ..
 
 lemma [code, code del]: "msetsum = msetsum" ..
 
@@ -388,14 +388,14 @@
   apply (auto simp: ac_simps)
   done
 
-lemma mcard_fold: "mcard A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
+lemma size_fold: "size A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
 proof -
   interpret comp_fun_commute ?f by default auto
   show ?thesis by (induct A) auto
 qed
 
-lemma mcard_Bag[code]: "mcard (Bag ms) = DAList_Multiset.fold (\<lambda>a n. op + n) 0 ms"
-  unfolding mcard_fold
+lemma size_Bag[code]: "size (Bag ms) = DAList_Multiset.fold (\<lambda>a n. op + n) 0 ms"
+  unfolding size_fold
 proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp)
   fix a n x
   show "n + x = (Suc ^^ n) x"

--- a/src/HOL/Library/Multiset.thy	Tue Apr 07 17:24:55 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Apr 07 18:22:06 2015 +0200
@@ -674,6 +674,20 @@
   then show ?thesis by blast
 qed
 
+lemma size_mset_mono: assumes "A \<le> B"
+  shows "size A \<le> size(B::_ multiset)"
+proof -
+  from assms[unfolded mset_le_exists_conv]
+  obtain C where B: "B = A + C" by auto
+  show ?thesis unfolding B by (induct C, auto)
+qed
+
+lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
+by (rule size_mset_mono[OF multiset_filter_subset])
+
+lemma size_Diff_submset:
+  "M \<le> M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
+by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
 
 subsection {* Induction and case splits *}
 
@@ -728,6 +742,9 @@
 qed
 
 
+lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
+by (cases M) auto
+
 subsubsection {* Strong induction and subset induction for multisets *}
 
 text {* Well-foundedness of strict subset relation *}
@@ -1255,6 +1272,16 @@
   shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
   by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
 
+lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
+proof (induct M)
+  case empty then show ?case by simp
+next
+  case (add M x) then show ?case
+    by (cases "x \<in> set_of M")
+      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
+qed
+
+
 abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
   "Union_mset MM \<equiv> msetsum MM"
 
@@ -1343,68 +1370,6 @@
 qed
 
 
-subsection {* Cardinality *}
-
-definition mcard :: "'a multiset \<Rightarrow> nat"
-where
-  "mcard = msetsum \<circ> image_mset (\<lambda>_. 1)"
-
-lemma mcard_empty [simp]:
-  "mcard {#} = 0"
-  by (simp add: mcard_def)
-
-lemma mcard_singleton [simp]:
-  "mcard {#a#} = Suc 0"
-  by (simp add: mcard_def)
-
-lemma mcard_plus [simp]:
-  "mcard (M + N) = mcard M + mcard N"
-  by (simp add: mcard_def)
-
-lemma mcard_empty_iff [simp]:
-  "mcard M = 0 \<longleftrightarrow> M = {#}"
-  by (induct M) simp_all
-
-lemma mcard_unfold_setsum:
-  "mcard M = setsum (count M) (set_of M)"
-proof (induct M)
-  case empty then show ?case by simp
-next
-  case (add M x) then show ?case
-    by (cases "x \<in> set_of M")
-      (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp)
-qed
-
-lemma size_eq_mcard:
-  "size = mcard"
-  by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
-
-lemma mcard_multiset_of:
-  "mcard (multiset_of xs) = length xs"
-  by (induct xs) simp_all
-
-lemma mcard_mono: assumes "A \<le> B"
-  shows "mcard A \<le> mcard B"
-proof -
-  from assms[unfolded mset_le_exists_conv]
-  obtain C where B: "B = A + C" by auto
-  show ?thesis unfolding B by (induct C, auto)
-qed
-
-lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
-  by (rule mcard_mono[OF multiset_filter_subset])
-
-lemma mcard_1_singleton:
-  assumes card: "mcard AA = 1"
-  shows "\<exists>A. AA = {#A#}"
-  using card by (cases AA) auto
-
-lemma mcard_Diff_subset:
-  assumes "M \<le> M'"
-  shows "mcard (M' - M) = mcard M' - mcard M"
-  by (metis add_diff_cancel_left' assms mcard_plus mset_le_exists_conv)
-
-
 subsection {* Replicate operation *}
 
 definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
@@ -1425,7 +1390,7 @@
 lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
   by (auto split: if_splits)
 
-lemma mcard_replicate_mset[simp]: "mcard (replicate_mset n M) = n"
+lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   by (induct n, simp_all)
 
 lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
@@ -2200,7 +2165,7 @@
   apply (simp_all add: add.commute)
   done
 
-declare mcard_multiset_of [code]
+declare size_multiset_of [code]
 
 fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
@@ -2277,10 +2242,6 @@
   then show ?thesis by simp
 qed
 
-lemma [code]:
-  "size = mcard"
-  by (fact size_eq_mcard)
-
 text {*
   Exercise for the casual reader: add implementations for @{const le_multiset}
   and @{const less_multiset} (multiset order).
@@ -2386,7 +2347,7 @@
   have xs': "xs' = take j xsa @ x # drop j xsa"
     using ms_x j_len nth_j Cons.prems xsa_def
     by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
-      length_drop mcard_multiset_of)
+      length_drop size_multiset_of)
   have j_len': "j \<le> length xsa"
     using j_len xs' xsa_def
     by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
@@ -2512,17 +2473,13 @@
 qed
 
 lemma rel_mset'_imp_rel_mset:
-"rel_mset' R M N \<Longrightarrow> rel_mset R M N"
+  "rel_mset' R M N \<Longrightarrow> rel_mset R M N"
 apply(induct rule: rel_mset'.induct)
 using rel_mset_Zero rel_mset_Plus by auto
 
-lemma mcard_image_mset[simp]: "mcard (image_mset f M) = mcard M"
-  unfolding size_eq_mcard[symmetric] by (rule size_image_mset)
-
-lemma rel_mset_mcard:
-  assumes "rel_mset R M N"
-  shows "mcard M = mcard N"
-using assms unfolding multiset.rel_compp_Grp Grp_def by auto
+lemma rel_mset_size:
+  "rel_mset R M N \<Longrightarrow> size M = size N"
+unfolding multiset.rel_compp_Grp Grp_def by auto
 
 lemma multiset_induct2[case_names empty addL addR]:
 assumes empty: "P {#} {#}"
@@ -2534,12 +2491,12 @@
   apply(induct M rule: multiset_induct, erule addR, erule addR)
 done
 
-lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
-assumes c: "mcard M = mcard N"
+lemma multiset_induct2_size[consumes 1, case_names empty add]:
+assumes c: "size M = size N"
 and empty: "P {#} {#}"
 and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
 shows "P M N"
-using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
+using c proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   case (less M)  show ?case
   proof(cases "M = {#}")
     case True hence "N = {#}" using less.prems by auto
@@ -2548,7 +2505,7 @@
     case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
     have "N \<noteq> {#}" using False less.prems by auto
     then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
-    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
+    have "size M1 = size N1" using less.prems unfolding M N by auto
     thus ?thesis using M N less.hyps add by auto
   qed
 qed
@@ -2615,9 +2572,9 @@
 lemma rel_mset_imp_rel_mset':
 assumes "rel_mset R M N"
 shows "rel_mset' R M N"
-using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
+using assms proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   case (less M)
-  have c: "mcard M = mcard N" using rel_mset_mcard[OF less.prems] .
+  have c: "size M = size N" using rel_mset_size[OF less.prems] .
   show ?case
   proof(cases "M = {#}")
     case True hence "N = {#}" using c by simp