# HG changeset patch # User nipkow # Date 1428423716 -7200 # Node ID fc4c896c8e74764624e82b4bbeb7aede00889d8d # Parent 09317aff0ff9df9a7536bc858fcc07f0c8f2cb24 Removed mcard because it is equal to size diff -r 09317aff0ff9 -r fc4c896c8e74 NEWS --- a/NEWS Tue Apr 07 15:14:14 2015 +0200 +++ b/NEWS Tue Apr 07 18:21:56 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] diff -r 09317aff0ff9 -r fc4c896c8e74 src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Tue Apr 07 15:14:14 2015 +0200 +++ b/src/HOL/Library/DAList_Multiset.thy Tue Apr 07 18:21:56 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 \ nat)" .. lemma [code, code del]: "msetsum = msetsum" .. @@ -388,14 +388,14 @@ apply (auto simp: ac_simps) done -lemma mcard_fold: "mcard A = Multiset.fold (\_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _") +lemma size_fold: "size A = Multiset.fold (\_. 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 (\a n. op + n) 0 ms" - unfolding mcard_fold +lemma size_Bag[code]: "size (Bag ms) = DAList_Multiset.fold (\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" diff -r 09317aff0ff9 -r fc4c896c8e74 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Apr 07 15:14:14 2015 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Apr 07 18:21:56 2015 +0200 @@ -674,6 +674,20 @@ then show ?thesis by blast qed +lemma size_mset_mono: assumes "A \ B" + shows "size A \ 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) \ size M" +by (rule size_mset_mono[OF multiset_filter_subset]) + +lemma size_Diff_submset: + "M \ M' \ 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 \ \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 \ M \ 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 (\_. 1) M)" +proof (induct M) + case empty then show ?case by simp +next + case (add M x) then show ?case + by (cases "x \ 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 \ 'a multiset" where "Union_mset MM \ msetsum MM" @@ -1343,68 +1370,6 @@ qed -subsection {* Cardinality *} - -definition mcard :: "'a multiset \ nat" -where - "mcard = msetsum \ image_mset (\_. 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 \ 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 \ 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 \ B" - shows "mcard A \ 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) \ mcard M" - by (rule mcard_mono[OF multiset_filter_subset]) - -lemma mcard_1_singleton: - assumes card: "mcard AA = 1" - shows "\A. AA = {#A#}" - using card by (cases AA) auto - -lemma mcard_Diff_subset: - assumes "M \ 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 \ 'a \ '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 \ count M x \ replicate_mset n x \ 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 \ 'a list \ bool option" where "ms_lesseq_impl [] ys = Some (ys \ [])" @@ -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 \ 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 \ rel_mset R M N" + "rel_mset' R M N \ 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 \ 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: "\M N a b. P M N \ 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 \ {#}" 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