adding simplification patterns to multiset simprocs
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Mon Feb 13 16:03:55 2017 +0100 (2017-02-13)
changeset 6502887e003397834
parent 65027 2b8583507891
child 65029 00731700e54f
adding simplification patterns to multiset simprocs
src/HOL/Library/Multiset_Order.thy
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:53 2017 +0100
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:55 2017 +0100
     1.3 @@ -263,12 +263,16 @@
     1.4  
     1.5  simproc_setup msetless_cancel
     1.6    ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
     1.7 -   "add_mset a m < n" | "m < add_mset a n") =
     1.8 +   "add_mset a m < n" | "m < add_mset a n" |
     1.9 +   "replicate_mset p a < n" | "m < replicate_mset p a" |
    1.10 +   "repeat_mset p m < n" | "m < repeat_mset p n") =
    1.11    \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
    1.12  
    1.13  simproc_setup msetle_cancel
    1.14    ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    1.15 -   "add_mset a m \<le> n" | "m \<le> add_mset a n") =
    1.16 +   "add_mset a m \<le> n" | "m \<le> add_mset a n" |
    1.17 +   "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
    1.18 +   "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
    1.19    \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>
    1.20  
    1.21