# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1487249662 -3600
# Node ID 52e2c99f37115936d2fbe9a5ad69ca965764fd30
# Parent  7fd4130cd0a43ce099fa335fdc92ed9aed38fb34
use the cancellation simprocs directly

diff -r 7fd4130cd0a4 -r 52e2c99f3711 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 16 09:45:03 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 16 13:54:22 2017 +0100
@@ -940,21 +940,8 @@
 
 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)
-
-lemma mset_diff_add_eq2:
-  "i \<le> (j::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = (m - (repeat_mset (j-i) u + n))"
-  by (auto simp: multiset_eq_iff nat_diff_add_eq2)
-
-lemma mset_eq_add_iff1:
-   "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_eq_add_iff1)
-
-lemma mset_eq_add_iff2:
-   "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (m = repeat_mset (j-i) u + n)"
-  by (auto simp: multiset_eq_iff nat_eq_add_iff2)
+lemma repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close>
+  unfolding iterate_add_def by (induction n) auto
 
 lemma mset_subseteq_add_iff1:
   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
@@ -966,14 +953,13 @@
 
 lemma mset_subset_add_iff1:
   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
-  unfolding subset_mset_def by (simp add: mset_eq_add_iff1 mset_subseteq_add_iff1)
+  unfolding subset_mset_def repeat_mset_iterate_add
+  by (simp add: iterate_add_eq_add_iff1 mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add])
 
 lemma mset_subset_add_iff2:
   "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 repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close>
-  unfolding iterate_add_def by (induction n) auto
+  unfolding subset_mset_def repeat_mset_iterate_add
+  by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])
 
 ML_file "multiset_simprocs.ML"
 
diff -r 7fd4130cd0a4 -r 52e2c99f3711 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Feb 16 09:45:03 2017 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Feb 16 13:54:22 2017 +0100
@@ -251,29 +251,19 @@
     by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
 qed
 
-lemma mset_less_add_iff1:
-  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (repeat_mset (i-j) u + m < n)"
-  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
-
-lemma mset_less_add_iff2:
-     "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (m < repeat_mset (j-i) u + n)"
-  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
-
-ML_file "multiset_order_simprocs.ML"
-
 simproc_setup msetless_cancel
   ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + 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 n") =
-  \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
+  \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
 
 simproc_setup msetle_cancel
   ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    "add_mset a m \<le> n" | "m \<le> add_mset a n" |
    "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
    "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
-  \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>
+  \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
 
 
 subsection \<open>Additional facts and instantiations\<close>
diff -r 7fd4130cd0a4 -r 52e2c99f3711 src/HOL/Library/multiset_order_simprocs.ML
--- a/src/HOL/Library/multiset_order_simprocs.ML	Thu Feb 16 09:45:03 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Author: Mathias Fleury, MPII
-
-
-Simprocs for multisets ordering, based on the simprocs for nat numerals.
-*)
-
-signature MULTISET_ORDER_SIMPROCS =
-sig
-  val less_cancel_msets: Proof.context -> cterm -> thm option
-  val le_cancel_msets: Proof.context -> cterm -> thm option
-end;
-
-structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS =
-struct
-
-structure LessCancelMultiset = Cancel_Fun
- (open Cancel_Data
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
-  val bal_add1 = @{thm mset_less_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
-  val bal_add2 = @{thm mset_less_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
-);
-
-structure LeCancelMultiset = Cancel_Fun
- (open Cancel_Data
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
-  val bal_add1 = @{thm mset_le_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
-  val bal_add2 = @{thm mset_le_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
-);
-
-val less_cancel_msets = LessCancelMultiset.proc;
-val le_cancel_msets = LeCancelMultiset.proc;
-
-end