diff -r 36bac3d245d9 -r ca41b6670904 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sun Sep 18 11:31:18 2016 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Sep 18 11:31:19 2016 +0200 @@ -874,7 +874,19 @@ interpretation subset_mset: order "op \#" "op <#" by unfold_locales auto -subsubsection \Simprocs\ +subsection \Replicate and repeat operations\ + +definition replicate_mset :: "nat \ 'a \ 'a multiset" where + "replicate_mset n x = (add_mset x ^^ n) {#}" + +lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}" + unfolding replicate_mset_def by simp + +lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)" + unfolding replicate_mset_def by (induct n) (auto intro: add.commute) + +lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)" + unfolding replicate_mset_def by (induct n) auto fun repeat_mset :: "nat \ 'a multiset \ 'a multiset" where "repeat_mset 0 _ = {#}" | @@ -889,6 +901,32 @@ lemma left_diff_repeat_mset_distrib': \repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\ by (auto simp: multiset_eq_iff left_diff_distrib') +lemma left_add_mult_distrib_mset: + "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k" + by (auto simp: multiset_eq_iff add_mult_distrib) + +lemma repeat_mset_distrib: + "repeat_mset (m + n) A = repeat_mset m A + repeat_mset n A" + by (auto simp: multiset_eq_iff Nat.add_mult_distrib) + +lemma repeat_mset_distrib2[simp]: + "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B" + by (auto simp: multiset_eq_iff add_mult_distrib2) + +lemma repeat_mset_replicate_mset[simp]: + "repeat_mset n {#a#} = replicate_mset n a" + by (auto simp: multiset_eq_iff) + +lemma repeat_mset_distrib_add_mset[simp]: + "repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A" + by (auto simp: multiset_eq_iff) + +lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}" + by (induction n) simp_all + + +subsubsection \Simprocs\ + lemma mset_diff_add_eq1: "j \ (i::nat) \ ((repeat_mset i u + m) - (repeat_mset j u + n)) = ((repeat_mset (i-j) u + m) - n)" by (auto simp: multiset_eq_iff nat_diff_add_eq1) @@ -921,41 +959,35 @@ "i \ (j::nat) \ (repeat_mset i u + m \# repeat_mset j u + n) = (m \# repeat_mset (j-i) u + n)" unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2) -lemma left_add_mult_distrib_mset: - "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k" - by (auto simp: multiset_eq_iff add_mult_distrib) - -lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \ A = B \ a = 0" - by (auto simp: multiset_eq_iff) - -lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \ a = b \ A = {#}" - by (auto simp: multiset_eq_iff) - -lemma repeat_mset_distrib [simp]: - "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B" - by (auto simp: multiset_eq_iff add_mult_distrib2) - ML_file "multiset_simprocs_util.ML" ML_file "multiset_simprocs.ML" simproc_setup mseteq_cancel_numerals ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" | - "add_mset a m = n" | "m = add_mset a n") = + "add_mset a m = n" | "m = add_mset a n" | + "replicate_mset p a = n" | "m = replicate_mset p a" | + "repeat_mset p m = n" | "m = repeat_mset p m") = \fn phi => Multiset_Simprocs.eq_cancel_msets\ simproc_setup msetless_cancel_numerals ("(l::'a multiset) + m \# n" | "(l::'a multiset) \# m + n" | - "add_mset a m \# n" | "m \# add_mset a n") = + "add_mset a m \# n" | "m \# add_mset a n" | + "replicate_mset p r \# n" | "m \# replicate_mset p r" | + "repeat_mset p m \# n" | "m \# repeat_mset p m") = \fn phi => Multiset_Simprocs.subset_cancel_msets\ simproc_setup msetle_cancel_numerals ("(l::'a multiset) + m \# n" | "(l::'a multiset) \# m + n" | - "add_mset a m \# n" | "m \# add_mset a n") = + "add_mset a m \# n" | "m \# add_mset a n" | + "replicate_mset p r \# n" | "m \# replicate_mset p r" | + "repeat_mset p m \# n" | "m \# repeat_mset p m") = \fn phi => Multiset_Simprocs.subseteq_cancel_msets\ simproc_setup msetdiff_cancel_numerals ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" | - "add_mset a m - n" | "m - add_mset a n") = + "add_mset a m - n" | "m - add_mset a n" | + "replicate_mset p r - n" | "m - replicate_mset p r" | + "repeat_mset p m - n" | "m - repeat_mset p m") = \fn phi => Multiset_Simprocs.diff_cancel_msets\ @@ -1958,23 +1990,11 @@ qed simp_all -subsection \Replicate operation\ - -definition replicate_mset :: "nat \ 'a \ 'a multiset" where - "replicate_mset n x = (add_mset x ^^ n) {#}" - -lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}" - unfolding replicate_mset_def by simp - -lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)" - unfolding replicate_mset_def by (induct n) (auto intro: add.commute) +subsection \More properties of the replicate and repeat operations\ lemma in_replicate_mset[simp]: "x \# replicate_mset n y \ n > 0 \ x = y" unfolding replicate_mset_def by (induct n) auto -lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)" - unfolding replicate_mset_def by (induct n) auto - lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})" by (auto split: if_splits) @@ -2000,12 +2020,10 @@ m = 0 \ n = 0 \ m = n \ a = b" by (auto simp add: multiset_eq_iff) -lemma repeat_mset_replicate_mset[simp]: - "repeat_mset n {#a#} = replicate_mset n a" +lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \ A = B \ a = 0" by (auto simp: multiset_eq_iff) -lemma repeat_mset_distrib_add_mset[simp]: - "repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A" +lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \ a = b \ A = {#}" by (auto simp: multiset_eq_iff)