add class ring_div; generalize mod/diff/minus proofs for class ring_div
authorhuffman
Thu Jan 08 09:12:29 2009 -0800 (2009-01-08)
changeset 2940598ab21b14f09
parent 29404 ee15ccdeaa72
child 29406 54bac26089bd
add class ring_div; generalize mod/diff/minus proofs for class ring_div
src/HOL/Divides.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Jan 08 08:36:16 2009 -0800
     1.2 +++ b/src/HOL/Divides.thy	Thu Jan 08 09:12:29 2009 -0800
     1.3 @@ -267,6 +267,55 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class ring_div = semiring_div + comm_ring_1
     1.8 +begin
     1.9 +
    1.10 +text {* Negation respects modular equivalence. *}
    1.11 +
    1.12 +lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
    1.13 +proof -
    1.14 +  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
    1.15 +    by (simp only: mod_div_equality)
    1.16 +  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
    1.17 +    by (simp only: minus_add_distrib minus_mult_left add_ac)
    1.18 +  also have "\<dots> = (- (a mod b)) mod b"
    1.19 +    by (rule mod_mult_self1)
    1.20 +  finally show ?thesis .
    1.21 +qed
    1.22 +
    1.23 +lemma mod_minus_cong:
    1.24 +  assumes "a mod b = a' mod b"
    1.25 +  shows "(- a) mod b = (- a') mod b"
    1.26 +proof -
    1.27 +  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
    1.28 +    unfolding assms ..
    1.29 +  thus ?thesis
    1.30 +    by (simp only: mod_minus_eq [symmetric])
    1.31 +qed
    1.32 +
    1.33 +text {* Subtraction respects modular equivalence. *}
    1.34 +
    1.35 +lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
    1.36 +  unfolding diff_minus
    1.37 +  by (intro mod_add_cong mod_minus_cong) simp_all
    1.38 +
    1.39 +lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
    1.40 +  unfolding diff_minus
    1.41 +  by (intro mod_add_cong mod_minus_cong) simp_all
    1.42 +
    1.43 +lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
    1.44 +  unfolding diff_minus
    1.45 +  by (intro mod_add_cong mod_minus_cong) simp_all
    1.46 +
    1.47 +lemma mod_diff_cong:
    1.48 +  assumes "a mod c = a' mod c"
    1.49 +  assumes "b mod c = b' mod c"
    1.50 +  shows "(a - b) mod c = (a' - b') mod c"
    1.51 +  unfolding diff_minus using assms
    1.52 +  by (intro mod_add_cong mod_minus_cong)
    1.53 +
    1.54 +end
    1.55 +
    1.56  
    1.57  subsection {* Division on @{typ nat} *}
    1.58  
     2.1 --- a/src/HOL/IntDiv.thy	Thu Jan 08 08:36:16 2009 -0800
     2.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 09:12:29 2009 -0800
     2.3 @@ -776,7 +776,7 @@
     2.4  apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
     2.5  done
     2.6  
     2.7 -instance int :: semiring_div
     2.8 +instance int :: ring_div
     2.9  proof
    2.10    fix a b c :: int
    2.11    assume not0: "b \<noteq> 0"
    2.12 @@ -818,14 +818,8 @@
    2.13  lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    2.14  by (rule mod_add_self2) (* already declared [simp] *)
    2.15  
    2.16 -lemma zmod_zdiff1_eq: fixes a::int
    2.17 -  shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
    2.18 -proof -
    2.19 -  have "?l = (c + (a mod c - b mod c)) mod c"
    2.20 -    using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
    2.21 -  also have "\<dots> = ?r" by simp
    2.22 -  finally show ?thesis .
    2.23 -qed
    2.24 +lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
    2.25 +by (rule mod_diff_eq)
    2.26  
    2.27  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
    2.28  
    2.29 @@ -1423,20 +1417,13 @@
    2.30  
    2.31  text {* by Brian Huffman *}
    2.32  lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
    2.33 -by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
    2.34 +by (rule mod_minus_eq [symmetric])
    2.35  
    2.36  lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
    2.37 -by (simp only: diff_def zmod_zadd_left_eq [symmetric])
    2.38 +by (rule mod_diff_left_eq [symmetric])
    2.39  
    2.40  lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
    2.41 -proof -
    2.42 -  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
    2.43 -    by (simp only: zminus_zmod)
    2.44 -  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
    2.45 -    by (simp only: zmod_zadd_right_eq [symmetric])
    2.46 -  thus "(x - y mod m) mod m = (x - y) mod m"
    2.47 -    by (simp only: diff_def)
    2.48 -qed
    2.49 +by (rule mod_diff_right_eq [symmetric])
    2.50  
    2.51  lemmas zmod_simps =
    2.52    IntDiv.zmod_zadd_left_eq  [symmetric]