# HG changeset patch
# User huffman
# Date 1333351096 -7200
# Node ID 262d96552e506f06c2c034f413b03db9b8d736bf
# Parent  4c7548e7df86d574c8fc915c0929556c4c1a28f3
add simp rules for dvd on negative numerals

diff -r 4c7548e7df86 -r 262d96552e50 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Apr 01 23:21:54 2012 +0200
+++ b/src/HOL/Divides.thy	Mon Apr 02 09:18:16 2012 +0200
@@ -2126,11 +2126,15 @@
 
 subsubsection {* The Divides Relation *}
 
-lemmas zdvd_iff_zmod_eq_0_numeral [simp] =
-  dvd_eq_mod_eq_0 [of "numeral x::int" "numeral y::int"]
-  dvd_eq_mod_eq_0 [of "numeral x::int" "neg_numeral y::int"]
-  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
-  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
+lemma dvd_neg_numeral_left [simp]:
+  fixes y :: "'a::comm_ring_1"
+  shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
+  unfolding neg_numeral_def minus_dvd_iff ..
+
+lemma dvd_neg_numeral_right [simp]:
+  fixes x :: "'a::comm_ring_1"
+  shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
+  unfolding neg_numeral_def dvd_minus_iff ..
 
 lemmas dvd_eq_mod_eq_0_numeral [simp] =
   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
diff -r 4c7548e7df86 -r 262d96552e50 src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Apr 01 23:21:54 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Apr 02 09:18:16 2012 +0200
@@ -52,12 +52,6 @@
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def)
      apply auto
-  apply (subgoal_tac "\<not> p dvd 1")
-   apply (rule_tac [2] zdvd_not_zless)
-    apply (subgoal_tac "p dvd 1")
-     prefer 2
-     apply (subst dvd_minus_iff [symmetric])
-     apply auto
   done
 
 lemma inv_not_1:
diff -r 4c7548e7df86 -r 262d96552e50 src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sun Apr 01 23:21:54 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Apr 02 09:18:16 2012 +0200
@@ -60,11 +60,6 @@
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def, auto)
-  apply (subgoal_tac "\<not> p dvd 1")
-   apply (rule_tac [2] zdvd_not_zless)
-    apply (subgoal_tac "p dvd 1")
-     prefer 2
-     apply (subst dvd_minus_iff [symmetric], auto)
   done
 
 lemma inv_not_1: