# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1474191079 -7200
# Node ID ca41b6670904e62b90f5d196069db8d7cbfe74c6
# Parent  36bac3d245d95d916bb05ea32cb4519f1abfd5de
support replicate_mset in multiset simproc

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)
 
 
diff -r 36bac3d245d9 -r ca41b6670904 src/HOL/Library/multiset_simprocs_util.ML
--- a/src/HOL/Library/multiset_simprocs_util.ML	Sun Sep 18 11:31:18 2016 +0200
+++ b/src/HOL/Library/multiset_simprocs_util.ML	Sun Sep 18 11:31:19 2016 +0200
@@ -72,6 +72,7 @@
   @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1)
       if_True if_False not_False_eq_True
       nat_0 nat_numeral nat_neg_numeral add_mset_commute repeat_mset.simps(1)
+      replicate_mset_0 repeat_mset_empty
       arith_simps rel_simps};
 
 
@@ -108,14 +109,21 @@
       if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end
     handle TERM _ => find_first_coeff (t::past) u terms;
 
-(*Split up a sum into the list of its constituent terms, on the way replace all the
-\<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set*)
+(*
+  Split up a sum into the list of its constituent terms, on the way replace:
+  * the \<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set;
+  * the \<open>replicate_mset n a\<close> by \<open>repeat_mset n {#a#}\<close>.
+*)
 fun dest_add_mset (Const (@{const_name add_mset}, T) $ a $
       Const (@{const_name "Groups.zero_class.zero"}, U), ts) =
     Const (@{const_name add_mset}, T) $ a $ typed_zero U :: ts
   | dest_add_mset (Const (@{const_name add_mset}, T) $ a $ mset, ts) =
     dest_add_mset (mset, Const (@{const_name add_mset}, T) $ a $
       typed_zero (fastype_of mset) :: ts)
+  | dest_add_mset (Const (@{const_name replicate_mset},
+      Type (_, [_, Type (_, [T, U])])) $ n $ a, ts) =
+    let val single_a = Const (@{const_name add_mset}, T --> U --> U) $ a $ typed_zero U in
+      fast_mk_repeat_mset (n, single_a) :: ts end
   | dest_add_mset (t, ts) =
     let val (t1,t2) = dest_plus t in
       dest_add_mset (t1, dest_add_mset (t2, ts)) end
@@ -156,7 +164,9 @@
 
 val norm_ss2 =
   simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
-    bin_simps @ @{thms union_mset_add_mset_left union_mset_add_mset_right ac_simps});
+    bin_simps @
+    @{thms union_mset_add_mset_left union_mset_add_mset_right
+        repeat_mset_replicate_mset ac_simps});
 
 fun norm_tac ctxt =
   ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))