src/HOL/Library/Multiset.thy
changeset 59949 fc4c896c8e74
parent 59815 cce82e360c2f
child 59958 4538d41e8e54
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Apr 07 15:14:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Apr 07 18:21:56 2015 +0200
     1.3 @@ -674,6 +674,20 @@
     1.4    then show ?thesis by blast
     1.5  qed
     1.6  
     1.7 +lemma size_mset_mono: assumes "A \<le> B"
     1.8 +  shows "size A \<le> size(B::_ multiset)"
     1.9 +proof -
    1.10 +  from assms[unfolded mset_le_exists_conv]
    1.11 +  obtain C where B: "B = A + C" by auto
    1.12 +  show ?thesis unfolding B by (induct C, auto)
    1.13 +qed
    1.14 +
    1.15 +lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
    1.16 +by (rule size_mset_mono[OF multiset_filter_subset])
    1.17 +
    1.18 +lemma size_Diff_submset:
    1.19 +  "M \<le> M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
    1.20 +by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
    1.21  
    1.22  subsection {* Induction and case splits *}
    1.23  
    1.24 @@ -728,6 +742,9 @@
    1.25  qed
    1.26  
    1.27  
    1.28 +lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
    1.29 +by (cases M) auto
    1.30 +
    1.31  subsubsection {* Strong induction and subset induction for multisets *}
    1.32  
    1.33  text {* Well-foundedness of strict subset relation *}
    1.34 @@ -1255,6 +1272,16 @@
    1.35    shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
    1.36    by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
    1.37  
    1.38 +lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
    1.39 +proof (induct M)
    1.40 +  case empty then show ?case by simp
    1.41 +next
    1.42 +  case (add M x) then show ?case
    1.43 +    by (cases "x \<in> set_of M")
    1.44 +      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
    1.45 +qed
    1.46 +
    1.47 +
    1.48  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
    1.49    "Union_mset MM \<equiv> msetsum MM"
    1.50  
    1.51 @@ -1343,68 +1370,6 @@
    1.52  qed
    1.53  
    1.54  
    1.55 -subsection {* Cardinality *}
    1.56 -
    1.57 -definition mcard :: "'a multiset \<Rightarrow> nat"
    1.58 -where
    1.59 -  "mcard = msetsum \<circ> image_mset (\<lambda>_. 1)"
    1.60 -
    1.61 -lemma mcard_empty [simp]:
    1.62 -  "mcard {#} = 0"
    1.63 -  by (simp add: mcard_def)
    1.64 -
    1.65 -lemma mcard_singleton [simp]:
    1.66 -  "mcard {#a#} = Suc 0"
    1.67 -  by (simp add: mcard_def)
    1.68 -
    1.69 -lemma mcard_plus [simp]:
    1.70 -  "mcard (M + N) = mcard M + mcard N"
    1.71 -  by (simp add: mcard_def)
    1.72 -
    1.73 -lemma mcard_empty_iff [simp]:
    1.74 -  "mcard M = 0 \<longleftrightarrow> M = {#}"
    1.75 -  by (induct M) simp_all
    1.76 -
    1.77 -lemma mcard_unfold_setsum:
    1.78 -  "mcard M = setsum (count M) (set_of M)"
    1.79 -proof (induct M)
    1.80 -  case empty then show ?case by simp
    1.81 -next
    1.82 -  case (add M x) then show ?case
    1.83 -    by (cases "x \<in> set_of M")
    1.84 -      (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp)
    1.85 -qed
    1.86 -
    1.87 -lemma size_eq_mcard:
    1.88 -  "size = mcard"
    1.89 -  by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
    1.90 -
    1.91 -lemma mcard_multiset_of:
    1.92 -  "mcard (multiset_of xs) = length xs"
    1.93 -  by (induct xs) simp_all
    1.94 -
    1.95 -lemma mcard_mono: assumes "A \<le> B"
    1.96 -  shows "mcard A \<le> mcard B"
    1.97 -proof -
    1.98 -  from assms[unfolded mset_le_exists_conv]
    1.99 -  obtain C where B: "B = A + C" by auto
   1.100 -  show ?thesis unfolding B by (induct C, auto)
   1.101 -qed
   1.102 -
   1.103 -lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
   1.104 -  by (rule mcard_mono[OF multiset_filter_subset])
   1.105 -
   1.106 -lemma mcard_1_singleton:
   1.107 -  assumes card: "mcard AA = 1"
   1.108 -  shows "\<exists>A. AA = {#A#}"
   1.109 -  using card by (cases AA) auto
   1.110 -
   1.111 -lemma mcard_Diff_subset:
   1.112 -  assumes "M \<le> M'"
   1.113 -  shows "mcard (M' - M) = mcard M' - mcard M"
   1.114 -  by (metis add_diff_cancel_left' assms mcard_plus mset_le_exists_conv)
   1.115 -
   1.116 -
   1.117  subsection {* Replicate operation *}
   1.118  
   1.119  definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
   1.120 @@ -1425,7 +1390,7 @@
   1.121  lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
   1.122    by (auto split: if_splits)
   1.123  
   1.124 -lemma mcard_replicate_mset[simp]: "mcard (replicate_mset n M) = n"
   1.125 +lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   1.126    by (induct n, simp_all)
   1.127  
   1.128  lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
   1.129 @@ -2200,7 +2165,7 @@
   1.130    apply (simp_all add: add.commute)
   1.131    done
   1.132  
   1.133 -declare mcard_multiset_of [code]
   1.134 +declare size_multiset_of [code]
   1.135  
   1.136  fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   1.137    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   1.138 @@ -2277,10 +2242,6 @@
   1.139    then show ?thesis by simp
   1.140  qed
   1.141  
   1.142 -lemma [code]:
   1.143 -  "size = mcard"
   1.144 -  by (fact size_eq_mcard)
   1.145 -
   1.146  text {*
   1.147    Exercise for the casual reader: add implementations for @{const le_multiset}
   1.148    and @{const less_multiset} (multiset order).
   1.149 @@ -2386,7 +2347,7 @@
   1.150    have xs': "xs' = take j xsa @ x # drop j xsa"
   1.151      using ms_x j_len nth_j Cons.prems xsa_def
   1.152      by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
   1.153 -      length_drop mcard_multiset_of)
   1.154 +      length_drop size_multiset_of)
   1.155    have j_len': "j \<le> length xsa"
   1.156      using j_len xs' xsa_def
   1.157      by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
   1.158 @@ -2512,17 +2473,13 @@
   1.159  qed
   1.160  
   1.161  lemma rel_mset'_imp_rel_mset:
   1.162 -"rel_mset' R M N \<Longrightarrow> rel_mset R M N"
   1.163 +  "rel_mset' R M N \<Longrightarrow> rel_mset R M N"
   1.164  apply(induct rule: rel_mset'.induct)
   1.165  using rel_mset_Zero rel_mset_Plus by auto
   1.166  
   1.167 -lemma mcard_image_mset[simp]: "mcard (image_mset f M) = mcard M"
   1.168 -  unfolding size_eq_mcard[symmetric] by (rule size_image_mset)
   1.169 -
   1.170 -lemma rel_mset_mcard:
   1.171 -  assumes "rel_mset R M N"
   1.172 -  shows "mcard M = mcard N"
   1.173 -using assms unfolding multiset.rel_compp_Grp Grp_def by auto
   1.174 +lemma rel_mset_size:
   1.175 +  "rel_mset R M N \<Longrightarrow> size M = size N"
   1.176 +unfolding multiset.rel_compp_Grp Grp_def by auto
   1.177  
   1.178  lemma multiset_induct2[case_names empty addL addR]:
   1.179  assumes empty: "P {#} {#}"
   1.180 @@ -2534,12 +2491,12 @@
   1.181    apply(induct M rule: multiset_induct, erule addR, erule addR)
   1.182  done
   1.183  
   1.184 -lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
   1.185 -assumes c: "mcard M = mcard N"
   1.186 +lemma multiset_induct2_size[consumes 1, case_names empty add]:
   1.187 +assumes c: "size M = size N"
   1.188  and empty: "P {#} {#}"
   1.189  and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
   1.190  shows "P M N"
   1.191 -using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   1.192 +using c proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   1.193    case (less M)  show ?case
   1.194    proof(cases "M = {#}")
   1.195      case True hence "N = {#}" using less.prems by auto
   1.196 @@ -2548,7 +2505,7 @@
   1.197      case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
   1.198      have "N \<noteq> {#}" using False less.prems by auto
   1.199      then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
   1.200 -    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
   1.201 +    have "size M1 = size N1" using less.prems unfolding M N by auto
   1.202      thus ?thesis using M N less.hyps add by auto
   1.203    qed
   1.204  qed
   1.205 @@ -2615,9 +2572,9 @@
   1.206  lemma rel_mset_imp_rel_mset':
   1.207  assumes "rel_mset R M N"
   1.208  shows "rel_mset' R M N"
   1.209 -using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   1.210 +using assms proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   1.211    case (less M)
   1.212 -  have c: "mcard M = mcard N" using rel_mset_mcard[OF less.prems] .
   1.213 +  have c: "size M = size N" using rel_mset_size[OF less.prems] .
   1.214    show ?case
   1.215    proof(cases "M = {#}")
   1.216      case True hence "N = {#}" using c by simp