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.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.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 =