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.5  
     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.9  
    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.14      by (simp add: dvd_add_right_iff)
    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.20  
    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.29  
    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')