src/HOL/Divides.thy
 changeset 54230 b1d955791529 parent 54227 63b441f49645 child 54489 03ff4d1e6784
```     1.1 --- a/src/HOL/Divides.thy	Thu Oct 31 16:54:22 2013 +0100
1.2 +++ b/src/HOL/Divides.thy	Fri Nov 01 18:51:14 2013 +0100
1.3 @@ -439,24 +439,23 @@
1.4
1.5  text {* Subtraction respects modular equivalence. *}
1.6
1.7 -lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
1.8 -  unfolding diff_minus
1.9 -  by (intro mod_add_cong mod_minus_cong) simp_all
1.10 -
1.11 -lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
1.12 -  unfolding diff_minus
1.13 -  by (intro mod_add_cong mod_minus_cong) simp_all
1.14 -
1.15 -lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
1.16 -  unfolding diff_minus
1.17 -  by (intro mod_add_cong mod_minus_cong) simp_all
1.18 +lemma mod_diff_left_eq:
1.19 +  "(a - b) mod c = (a mod c - b) mod c"
1.20 +  using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
1.21 +
1.22 +lemma mod_diff_right_eq:
1.23 +  "(a - b) mod c = (a - b mod c) mod c"
1.24 +  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
1.25 +
1.26 +lemma mod_diff_eq:
1.27 +  "(a - b) mod c = (a mod c - b mod c) mod c"
1.28 +  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
1.29
1.30  lemma mod_diff_cong:
1.31    assumes "a mod c = a' mod c"
1.32    assumes "b mod c = b' mod c"
1.33    shows "(a - b) mod c = (a' - b') mod c"
1.34 -  unfolding diff_minus using assms
1.35 -  by (intro mod_add_cong mod_minus_cong)
1.36 +  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
1.37
1.38  lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
1.39  apply (case_tac "y = 0") apply simp
1.40 @@ -502,10 +501,7 @@
1.41
1.42  lemma minus_mod_self1 [simp]:
1.43    "(b - a) mod b = - a mod b"
1.44 -proof -
1.45 -  have "b - a = - a + b" by (simp add: diff_minus add.commute)
1.46 -  then show ?thesis by simp
1.47 -qed
1.48 +  using mod_add_self2 [of "- a" b] by simp
1.49
1.50  end
1.51
1.52 @@ -1749,7 +1745,7 @@
1.53    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1.54
1.55    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac