src/HOL/Divides.thy
changeset 47160 8ada79014cb2
parent 47159 978c00c20a59
child 47162 9d7d919b9fd8
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:27:49 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:34:04 2012 +0200
     1.3 @@ -463,6 +463,12 @@
     1.4  lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
     1.5    using mod_minus_minus [of "-a" b] by simp
     1.6  
     1.7 +lemma div_minus1_right [simp]: "a div (-1) = -a"
     1.8 +  using div_minus_right [of a 1] by simp
     1.9 +
    1.10 +lemma mod_minus1_right [simp]: "a mod (-1) = 0"
    1.11 +  using mod_minus_right [of a 1] by simp
    1.12 +
    1.13  end
    1.14  
    1.15  
    1.16 @@ -1661,16 +1667,6 @@
    1.17  
    1.18  text{*Special-case simplification *}
    1.19  
    1.20 -lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
    1.21 -apply (cut_tac a = a and b = "-1" in neg_mod_sign)
    1.22 -apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
    1.23 -apply (auto simp del: neg_mod_sign neg_mod_bound)
    1.24 -done (* FIXME: generalize *)
    1.25 -
    1.26 -lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
    1.27 -by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
    1.28 -(* FIXME: generalize *)
    1.29 -
    1.30  (** The last remaining special cases for constant arithmetic:
    1.31      1 div z and 1 mod z **)
    1.32