# 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 \ (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) \ 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 "\ 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 "\ 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: