# HG changeset patch
# User wenzelm
# Date 1426864708 -3600
# Node ID 4ebf2276f58aab757ec22dc1aea57e62070ae7d9
# Parent  66fc7122f51a865a0657e9fe6b88b5d54d96c4ab# Parent  56d2c357e6b52a6e472db760b33c7c2d8179d286
merged

diff -r 56d2c357e6b5 -r 4ebf2276f58a src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Fri Mar 20 14:48:04 2015 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Mar 20 16:18:28 2015 +0100
@@ -99,6 +99,10 @@
   shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
   by (fact div_mult_mult1_if)
 
+lemma numeral_times_minus_swap:
+  fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
+  by (simp add: mult.commute)
+
 ML_file "Tools/numeral_simprocs.ML"
 
 simproc_setup semiring_assoc_fold
diff -r 56d2c357e6b5 -r 4ebf2276f58a src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 20 14:48:04 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 20 16:18:28 2015 +0100
@@ -227,7 +227,7 @@
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val mult_minus_simps =
-    [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}];
+    [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}];
 
 val norm_ss1 =
   simpset_of (put_simpset num_ss @{context}
@@ -381,7 +381,7 @@
   val norm_ss2 =
     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   val norm_ss3 =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))