src/HOL/IntDiv.thy
changeset 29405 98ab21b14f09
parent 29404 ee15ccdeaa72
child 29410 97916a925a69
     1.1 --- a/src/HOL/IntDiv.thy	Thu Jan 08 08:36:16 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 09:12:29 2009 -0800
     1.3 @@ -776,7 +776,7 @@
     1.4  apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
     1.5  done
     1.6  
     1.7 -instance int :: semiring_div
     1.8 +instance int :: ring_div
     1.9  proof
    1.10    fix a b c :: int
    1.11    assume not0: "b \<noteq> 0"
    1.12 @@ -818,14 +818,8 @@
    1.13  lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    1.14  by (rule mod_add_self2) (* already declared [simp] *)
    1.15  
    1.16 -lemma zmod_zdiff1_eq: fixes a::int
    1.17 -  shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
    1.18 -proof -
    1.19 -  have "?l = (c + (a mod c - b mod c)) mod c"
    1.20 -    using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
    1.21 -  also have "\<dots> = ?r" by simp
    1.22 -  finally show ?thesis .
    1.23 -qed
    1.24 +lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
    1.25 +by (rule mod_diff_eq)
    1.26  
    1.27  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
    1.28  
    1.29 @@ -1423,20 +1417,13 @@
    1.30  
    1.31  text {* by Brian Huffman *}
    1.32  lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
    1.33 -by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
    1.34 +by (rule mod_minus_eq [symmetric])
    1.35  
    1.36  lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
    1.37 -by (simp only: diff_def zmod_zadd_left_eq [symmetric])
    1.38 +by (rule mod_diff_left_eq [symmetric])
    1.39  
    1.40  lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
    1.41 -proof -
    1.42 -  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
    1.43 -    by (simp only: zminus_zmod)
    1.44 -  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
    1.45 -    by (simp only: zmod_zadd_right_eq [symmetric])
    1.46 -  thus "(x - y mod m) mod m = (x - y) mod m"
    1.47 -    by (simp only: diff_def)
    1.48 -qed
    1.49 +by (rule mod_diff_right_eq [symmetric])
    1.50  
    1.51  lemmas zmod_simps =
    1.52    IntDiv.zmod_zadd_left_eq  [symmetric]