src/HOL/NumberTheory/IntPrimes.thy

 
 lemma zcong_refl [simp]: "[k = k] (mod m)"
   by (unfold zcong_def, auto)
 
 lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
-  apply (unfold zcong_def dvd_def, auto)
-   apply (rule_tac [!] x = "-k" in exI, auto)
-  done
+  unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
 
 lemma zcong_zadd:
     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
   apply (unfold zcong_def)
   apply (rule_tac s = "(a - b) + (c - d)" in subst)

    apply (rule_tac [2] zdvd_zdiff, auto)
   done
 
 lemma zcong_trans:
     "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
-  apply (unfold zcong_def dvd_def, auto)
-  apply (rule_tac x = "k + ka" in exI)
-  apply (simp add: zadd_ac zadd_zmult_distrib2)
+  unfolding zcong_def
+  apply (auto elim!: dvdE simp add: ring_simps)
+  unfolding left_distrib [symmetric]
+  apply (rule dvd_mult dvd_refl)+
   done
 
 lemma zcong_zmult:
     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
   apply (rule_tac b = "b * c" in zcong_trans)

   by (simp add: zmult_commute zcong_cancel)
 
 lemma zcong_zgcd_zmult_zmod:
   "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
     ==> [a = b] (mod m * n)"
-  apply (unfold zcong_def dvd_def, auto)
+  apply (auto simp add: zcong_def dvd_def)
   apply (subgoal_tac "m dvd n * ka")
    apply (subgoal_tac "m dvd ka")
     apply (case_tac [2] "0 \<le> ka")
   apply (metis zdvd_mult_div_cancel zdvd_refl zdvd_zminus2_iff zdvd_zmultD2 zgcd_zminus zmult_commute zmult_zminus zrelprime_zdvd_zmult)
   apply (metis IntDiv.zdvd_abs1 abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)

   apply (rule_tac x = "a mod m" in exI, auto)
   apply (metis zmult_div_cancel)
   done
 
 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
-  apply (unfold zcong_def dvd_def, auto)
-   apply (rule_tac [!] x = "-k" in exI, auto)
+  unfolding zcong_def
+  apply (auto elim!: dvdE simp add: ring_simps)
+  apply (rule_tac x = "-k" in exI) apply simp
   done
 
 lemma zgcd_zcong_zgcd:
   "0 < m ==>
     zgcd a m = 1 ==> [a = b] (mod m) ==> zgcd b m = 1"

 
 subsection {* Modulo *}
 
 lemma zmod_zdvd_zmod:
     "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
-  apply (unfold dvd_def, auto)
-  apply (subst zcong_zmod_eq [symmetric])
-   prefer 2
-   apply (subst zcong_iff_lin)
-   apply (rule_tac x = "k * (a div (m * k))" in exI)
-   apply (simp add:zmult_assoc [symmetric], assumption)
-  done
+  by (rule zmod_zmod_cancel) 
 
 
 subsection {* Extended GCD *}
 
 declare xzgcda.simps [simp del]