
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 \<le>#" "op <#" by unfold_locales auto
 
 
-subsubsection \<open>Simprocs\<close>
+subsection \<open>Replicate and repeat operations\<close>
+
+definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   "repeat_mset 0 _ = {#}" |
@@ -889,6 +901,32 @@
 lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
   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 \<open>Simprocs\<close>
+
 lemma mset_diff_add_eq1:
   "j \<le> (i::nat) \<Longrightarrow> ((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 \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># 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 \<longleftrightarrow> A = B \<or> a = 0"
-  by (auto simp: multiset_eq_iff)
-
-lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> 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") =
   \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
 
 simproc_setup msetless_cancel_numerals
   ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
-   "add_mset a m \<subset># n" | "m \<subset># add_mset a n") =
+   "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
+   "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
+   "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
   \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
 
 simproc_setup msetle_cancel_numerals
   ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
-   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n") =
+   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
+   "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
+   "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
   \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
 
 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") =
   \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
 
 
@@ -1958,23 +1990,11 @@
 qed simp_all
 
 
-subsection \<open>Replicate operation\<close>
-
-definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> '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 \<open>More properties of the replicate and repeat operations\<close>
 
 lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> 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 \<and> n = 0 \<or> m = n \<and> 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 \<longleftrightarrow> A = B \<or> 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 \<longleftrightarrow> a = b \<or> A = {#}"
   by (auto simp: multiset_eq_iff)
 
 




