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 
    1.56 -    (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    1.57 +    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
    1.58  )
    1.59  *}
    1.60