src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 64242 93c6f0da5c70 parent 64240 eabf80376aab child 64243 aee949f6642d
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
1.3 @@ -27,7 +27,7 @@
1.4  begin
1.6  lemma mod_0 [simp]: "0 mod a = 0"
1.7 -  using mod_div_equality [of 0 a] by simp
1.8 +  using div_mult_mod_eq [of 0 a] by simp
1.10  lemma dvd_mod_iff:
1.11    assumes "k dvd n"
1.12 @@ -36,7 +36,7 @@
1.13    from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
1.15    also have "(m div n) * n + m mod n = m"
1.16 -    using mod_div_equality [of m n] by simp
1.17 +    using div_mult_mod_eq [of m n] by simp
1.18    finally show ?thesis .
1.19  qed
1.21 @@ -46,7 +46,7 @@
1.22  proof -
1.23    have "b dvd ((a div b) * b)" by simp
1.24    also have "(a div b) * b = a"
1.25 -    using mod_div_equality [of a b] by (simp add: assms)
1.26 +    using div_mult_mod_eq [of a b] by (simp add: assms)
1.27    finally show ?thesis .
1.28  qed
1.30 @@ -72,7 +72,7 @@
1.31    obtains s and t where "a = s * b + t"
1.32      and "euclidean_size t < euclidean_size b"
1.33  proof -
1.34 -  from mod_div_equality [of a b]
1.35 +  from div_mult_mod_eq [of a b]
1.36       have "a = a div b * b + a mod b" by simp
1.37    with that and assms show ?thesis by (auto simp add: mod_size_less)
1.38  qed
1.39 @@ -507,7 +507,7 @@
1.40                (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
1.41        also have "s' * a + t' * b = r'" by fact
1.42        also have "s * a + t * b = r" by fact
1.43 -      also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
1.44 +      also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
1.45          by (simp add: algebra_simps)
1.46        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
1.47      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')