# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426860375 0
# Node ID 66fc7122f51a865a0657e9fe6b88b5d54d96c4ab
# Parent  93d4169e07dc78f96c66654e8ceef2a619d89d4a# Parent  96abba46955f65a5fd1d6ff656a46b0a43f6e8b7
Merge

diff -r 96abba46955f -r 66fc7122f51a src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Thu Mar 19 22:31:23 2015 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Mar 20 14:06:15 2015 +0000
@@ -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 96abba46955f -r 66fc7122f51a src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Mar 19 22:31:23 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 20 14:06:15 2015 +0000
@@ -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))