Removed mcard because it is equal to size
authornipkow
Tue Apr 07 18:21:56 2015 +0200 (2015-04-07)
changeset 59949fc4c896c8e74
parent 59947 09317aff0ff9
child 59950 364b0512ce74
Removed mcard because it is equal to size
NEWS
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/NEWS	Tue Apr 07 15:14:14 2015 +0200
     1.2 +++ b/NEWS	Tue Apr 07 18:21:56 2015 +0200
     1.3 @@ -302,6 +302,7 @@
     1.4    - Renamed
     1.5        in_multiset_of ~> in_multiset_in_set
     1.6      INCOMPATIBILITY.
     1.7 +  - Removed mcard, is equal to size.
     1.8    - Added attributes:
     1.9        image_mset.id [simp]
    1.10        image_mset_id [simp]
     2.1 --- a/src/HOL/Library/DAList_Multiset.thy	Tue Apr 07 15:14:14 2015 +0200
     2.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Tue Apr 07 18:21:56 2015 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  
     2.5  lemma [code, code del]: "count = count" ..
     2.6  
     2.7 -lemma [code, code del]: "mcard = mcard" ..
     2.8 +lemma [code, code del]: "size = (size :: _ multiset \<Rightarrow> nat)" ..
     2.9  
    2.10  lemma [code, code del]: "msetsum = msetsum" ..
    2.11  
    2.12 @@ -388,14 +388,14 @@
    2.13    apply (auto simp: ac_simps)
    2.14    done
    2.15  
    2.16 -lemma mcard_fold: "mcard A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
    2.17 +lemma size_fold: "size A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
    2.18  proof -
    2.19    interpret comp_fun_commute ?f by default auto
    2.20    show ?thesis by (induct A) auto
    2.21  qed
    2.22  
    2.23 -lemma mcard_Bag[code]: "mcard (Bag ms) = DAList_Multiset.fold (\<lambda>a n. op + n) 0 ms"
    2.24 -  unfolding mcard_fold
    2.25 +lemma size_Bag[code]: "size (Bag ms) = DAList_Multiset.fold (\<lambda>a n. op + n) 0 ms"
    2.26 +  unfolding size_fold
    2.27  proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp)
    2.28    fix a n x
    2.29    show "n + x = (Suc ^^ n) x"
     3.1 --- a/src/HOL/Library/Multiset.thy	Tue Apr 07 15:14:14 2015 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Tue Apr 07 18:21:56 2015 +0200
     3.3 @@ -674,6 +674,20 @@
     3.4    then show ?thesis by blast
     3.5  qed
     3.6  
     3.7 +lemma size_mset_mono: assumes "A \<le> B"
     3.8 +  shows "size A \<le> size(B::_ multiset)"
     3.9 +proof -
    3.10 +  from assms[unfolded mset_le_exists_conv]
    3.11 +  obtain C where B: "B = A + C" by auto
    3.12 +  show ?thesis unfolding B by (induct C, auto)
    3.13 +qed
    3.14 +
    3.15 +lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
    3.16 +by (rule size_mset_mono[OF multiset_filter_subset])
    3.17 +
    3.18 +lemma size_Diff_submset:
    3.19 +  "M \<le> M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
    3.20 +by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
    3.21  
    3.22  subsection {* Induction and case splits *}
    3.23  
    3.24 @@ -728,6 +742,9 @@
    3.25  qed
    3.26  
    3.27  
    3.28 +lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
    3.29 +by (cases M) auto
    3.30 +
    3.31  subsubsection {* Strong induction and subset induction for multisets *}
    3.32  
    3.33  text {* Well-foundedness of strict subset relation *}
    3.34 @@ -1255,6 +1272,16 @@
    3.35    shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
    3.36    by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
    3.37  
    3.38 +lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
    3.39 +proof (induct M)
    3.40 +  case empty then show ?case by simp
    3.41 +next
    3.42 +  case (add M x) then show ?case
    3.43 +    by (cases "x \<in> set_of M")
    3.44 +      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
    3.45 +qed
    3.46 +
    3.47 +
    3.48  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
    3.49    "Union_mset MM \<equiv> msetsum MM"
    3.50  
    3.51 @@ -1343,68 +1370,6 @@
    3.52  qed
    3.53  
    3.54  
    3.55 -subsection {* Cardinality *}
    3.56 -
    3.57 -definition mcard :: "'a multiset \<Rightarrow> nat"
    3.58 -where
    3.59 -  "mcard = msetsum \<circ> image_mset (\<lambda>_. 1)"
    3.60 -
    3.61 -lemma mcard_empty [simp]:
    3.62 -  "mcard {#} = 0"
    3.63 -  by (simp add: mcard_def)
    3.64 -
    3.65 -lemma mcard_singleton [simp]:
    3.66 -  "mcard {#a#} = Suc 0"
    3.67 -  by (simp add: mcard_def)
    3.68 -
    3.69 -lemma mcard_plus [simp]:
    3.70 -  "mcard (M + N) = mcard M + mcard N"
    3.71 -  by (simp add: mcard_def)
    3.72 -
    3.73 -lemma mcard_empty_iff [simp]:
    3.74 -  "mcard M = 0 \<longleftrightarrow> M = {#}"
    3.75 -  by (induct M) simp_all
    3.76 -
    3.77 -lemma mcard_unfold_setsum:
    3.78 -  "mcard M = setsum (count M) (set_of M)"
    3.79 -proof (induct M)
    3.80 -  case empty then show ?case by simp
    3.81 -next
    3.82 -  case (add M x) then show ?case
    3.83 -    by (cases "x \<in> set_of M")
    3.84 -      (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp)
    3.85 -qed
    3.86 -
    3.87 -lemma size_eq_mcard:
    3.88 -  "size = mcard"
    3.89 -  by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
    3.90 -
    3.91 -lemma mcard_multiset_of:
    3.92 -  "mcard (multiset_of xs) = length xs"
    3.93 -  by (induct xs) simp_all
    3.94 -
    3.95 -lemma mcard_mono: assumes "A \<le> B"
    3.96 -  shows "mcard A \<le> mcard B"
    3.97 -proof -
    3.98 -  from assms[unfolded mset_le_exists_conv]
    3.99 -  obtain C where B: "B = A + C" by auto
   3.100 -  show ?thesis unfolding B by (induct C, auto)
   3.101 -qed
   3.102 -
   3.103 -lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
   3.104 -  by (rule mcard_mono[OF multiset_filter_subset])
   3.105 -
   3.106 -lemma mcard_1_singleton:
   3.107 -  assumes card: "mcard AA = 1"
   3.108 -  shows "\<exists>A. AA = {#A#}"
   3.109 -  using card by (cases AA) auto
   3.110 -
   3.111 -lemma mcard_Diff_subset:
   3.112 -  assumes "M \<le> M'"
   3.113 -  shows "mcard (M' - M) = mcard M' - mcard M"
   3.114 -  by (metis add_diff_cancel_left' assms mcard_plus mset_le_exists_conv)
   3.115 -
   3.116 -
   3.117  subsection {* Replicate operation *}
   3.118  
   3.119  definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
   3.120 @@ -1425,7 +1390,7 @@
   3.121  lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
   3.122    by (auto split: if_splits)
   3.123  
   3.124 -lemma mcard_replicate_mset[simp]: "mcard (replicate_mset n M) = n"
   3.125 +lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   3.126    by (induct n, simp_all)
   3.127  
   3.128  lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
   3.129 @@ -2200,7 +2165,7 @@
   3.130    apply (simp_all add: add.commute)
   3.131    done
   3.132  
   3.133 -declare mcard_multiset_of [code]
   3.134 +declare size_multiset_of [code]
   3.135  
   3.136  fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   3.137    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   3.138 @@ -2277,10 +2242,6 @@
   3.139    then show ?thesis by simp
   3.140  qed
   3.141  
   3.142 -lemma [code]:
   3.143 -  "size = mcard"
   3.144 -  by (fact size_eq_mcard)
   3.145 -
   3.146  text {*
   3.147    Exercise for the casual reader: add implementations for @{const le_multiset}
   3.148    and @{const less_multiset} (multiset order).
   3.149 @@ -2386,7 +2347,7 @@
   3.150    have xs': "xs' = take j xsa @ x # drop j xsa"
   3.151      using ms_x j_len nth_j Cons.prems xsa_def
   3.152      by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
   3.153 -      length_drop mcard_multiset_of)
   3.154 +      length_drop size_multiset_of)
   3.155    have j_len': "j \<le> length xsa"
   3.156      using j_len xs' xsa_def
   3.157      by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
   3.158 @@ -2512,17 +2473,13 @@
   3.159  qed
   3.160  
   3.161  lemma rel_mset'_imp_rel_mset:
   3.162 -"rel_mset' R M N \<Longrightarrow> rel_mset R M N"
   3.163 +  "rel_mset' R M N \<Longrightarrow> rel_mset R M N"
   3.164  apply(induct rule: rel_mset'.induct)
   3.165  using rel_mset_Zero rel_mset_Plus by auto
   3.166  
   3.167 -lemma mcard_image_mset[simp]: "mcard (image_mset f M) = mcard M"
   3.168 -  unfolding size_eq_mcard[symmetric] by (rule size_image_mset)
   3.169 -
   3.170 -lemma rel_mset_mcard:
   3.171 -  assumes "rel_mset R M N"
   3.172 -  shows "mcard M = mcard N"
   3.173 -using assms unfolding multiset.rel_compp_Grp Grp_def by auto
   3.174 +lemma rel_mset_size:
   3.175 +  "rel_mset R M N \<Longrightarrow> size M = size N"
   3.176 +unfolding multiset.rel_compp_Grp Grp_def by auto
   3.177  
   3.178  lemma multiset_induct2[case_names empty addL addR]:
   3.179  assumes empty: "P {#} {#}"
   3.180 @@ -2534,12 +2491,12 @@
   3.181    apply(induct M rule: multiset_induct, erule addR, erule addR)
   3.182  done
   3.183  
   3.184 -lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
   3.185 -assumes c: "mcard M = mcard N"
   3.186 +lemma multiset_induct2_size[consumes 1, case_names empty add]:
   3.187 +assumes c: "size M = size N"
   3.188  and empty: "P {#} {#}"
   3.189  and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
   3.190  shows "P M N"
   3.191 -using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   3.192 +using c proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   3.193    case (less M)  show ?case
   3.194    proof(cases "M = {#}")
   3.195      case True hence "N = {#}" using less.prems by auto
   3.196 @@ -2548,7 +2505,7 @@
   3.197      case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
   3.198      have "N \<noteq> {#}" using False less.prems by auto
   3.199      then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
   3.200 -    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
   3.201 +    have "size M1 = size N1" using less.prems unfolding M N by auto
   3.202      thus ?thesis using M N less.hyps add by auto
   3.203    qed
   3.204  qed
   3.205 @@ -2615,9 +2572,9 @@
   3.206  lemma rel_mset_imp_rel_mset':
   3.207  assumes "rel_mset R M N"
   3.208  shows "rel_mset' R M N"
   3.209 -using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   3.210 +using assms proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   3.211    case (less M)
   3.212 -  have c: "mcard M = mcard N" using rel_mset_mcard[OF less.prems] .
   3.213 +  have c: "size M = size N" using rel_mset_size[OF less.prems] .
   3.214    show ?case
   3.215    proof(cases "M = {#}")
   3.216      case True hence "N = {#}" using c by simp