src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 64164 38c407446400
parent 64163 62c9e5c05928
child 64177 006f303fb173
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Oct 11 16:44:13 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Oct 12 20:38:47 2016 +0200
     1.3 @@ -6,39 +6,6 @@
     1.4  imports "~~/src/HOL/GCD" Factorial_Ring
     1.5  begin
     1.6  
     1.7 -class divide_modulo = semidom_divide + modulo +
     1.8 -  assumes div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
     1.9 -begin
    1.10 -
    1.11 -lemma zero_mod_left [simp]: "0 mod a = 0"
    1.12 -  using div_mod_equality[of 0 a 0] by simp
    1.13 -
    1.14 -lemma dvd_mod_iff [simp]: 
    1.15 -  assumes "k dvd n"
    1.16 -  shows   "(k dvd m mod n) = (k dvd m)"
    1.17 -proof -
    1.18 -  thm div_mod_equality
    1.19 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    1.20 -    by (simp add: dvd_add_right_iff)
    1.21 -  also have "(m div n) * n + m mod n = m"
    1.22 -    using div_mod_equality[of m n 0] by simp
    1.23 -  finally show ?thesis .
    1.24 -qed
    1.25 -
    1.26 -lemma mod_0_imp_dvd: 
    1.27 -  assumes "a mod b = 0"
    1.28 -  shows   "b dvd a"
    1.29 -proof -
    1.30 -  have "b dvd ((a div b) * b)" by simp
    1.31 -  also have "(a div b) * b = a"
    1.32 -    using div_mod_equality[of a b 0] by (simp add: assms)
    1.33 -  finally show ?thesis .
    1.34 -qed
    1.35 -
    1.36 -end
    1.37 -
    1.38 -
    1.39 -
    1.40  text \<open>
    1.41    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
    1.42    implemented. It must provide:
    1.43 @@ -50,7 +17,7 @@
    1.44    The existence of these functions makes it possible to derive gcd and lcm functions 
    1.45    for any Euclidean semiring.
    1.46  \<close> 
    1.47 -class euclidean_semiring = divide_modulo + normalization_semidom + 
    1.48 +class euclidean_semiring = semiring_modulo + normalization_semidom + 
    1.49    fixes euclidean_size :: "'a \<Rightarrow> nat"
    1.50    assumes size_0 [simp]: "euclidean_size 0 = 0"
    1.51    assumes mod_size_less: 
    1.52 @@ -59,6 +26,30 @@
    1.53      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    1.54  begin
    1.55  
    1.56 +lemma zero_mod_left [simp]: "0 mod a = 0"
    1.57 +  using mod_div_equality [of 0 a] by simp
    1.58 +
    1.59 +lemma dvd_mod_iff: 
    1.60 +  assumes "k dvd n"
    1.61 +  shows   "(k dvd m mod n) = (k dvd m)"
    1.62 +proof -
    1.63 +  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    1.64 +    by (simp add: dvd_add_right_iff)
    1.65 +  also have "(m div n) * n + m mod n = m"
    1.66 +    using mod_div_equality [of m n] by simp
    1.67 +  finally show ?thesis .
    1.68 +qed
    1.69 +
    1.70 +lemma mod_0_imp_dvd: 
    1.71 +  assumes "a mod b = 0"
    1.72 +  shows   "b dvd a"
    1.73 +proof -
    1.74 +  have "b dvd ((a div b) * b)" by simp
    1.75 +  also have "(a div b) * b = a"
    1.76 +    using mod_div_equality [of a b] by (simp add: assms)
    1.77 +  finally show ?thesis .
    1.78 +qed
    1.79 +
    1.80  lemma euclidean_size_normalize [simp]:
    1.81    "euclidean_size (normalize a) = euclidean_size a"
    1.82  proof (cases "a = 0")
    1.83 @@ -81,36 +72,11 @@
    1.84    obtains s and t where "a = s * b + t" 
    1.85      and "euclidean_size t < euclidean_size b"
    1.86  proof -
    1.87 -  from div_mod_equality [of a b 0] 
    1.88 +  from mod_div_equality [of a b] 
    1.89       have "a = a div b * b + a mod b" by simp
    1.90    with that and assms show ?thesis by (auto simp add: mod_size_less)
    1.91  qed
    1.92  
    1.93 -lemma zero_mod_left [simp]: "0 mod a = 0"
    1.94 -  using div_mod_equality[of 0 a 0] by simp
    1.95 -
    1.96 -lemma dvd_mod_iff [simp]: 
    1.97 -  assumes "k dvd n"
    1.98 -  shows   "(k dvd m mod n) = (k dvd m)"
    1.99 -proof -
   1.100 -  thm div_mod_equality
   1.101 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
   1.102 -    by (simp add: dvd_add_right_iff)
   1.103 -  also have "(m div n) * n + m mod n = m"
   1.104 -    using div_mod_equality[of m n 0] by simp
   1.105 -  finally show ?thesis .
   1.106 -qed
   1.107 -
   1.108 -lemma mod_0_imp_dvd: 
   1.109 -  assumes "a mod b = 0"
   1.110 -  shows   "b dvd a"
   1.111 -proof -
   1.112 -  have "b dvd ((a div b) * b)" by simp
   1.113 -  also have "(a div b) * b = a"
   1.114 -    using div_mod_equality[of a b 0] by (simp add: assms)
   1.115 -  finally show ?thesis .
   1.116 -qed
   1.117 -
   1.118  lemma dvd_euclidean_size_eq_imp_dvd:
   1.119    assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
   1.120    shows "a dvd b"
   1.121 @@ -118,7 +84,7 @@
   1.122    assume "\<not> a dvd b"
   1.123    hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
   1.124    then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   1.125 -  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by simp
   1.126 +  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
   1.127    from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
   1.128      with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   1.129    with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
   1.130 @@ -541,7 +507,7 @@
   1.131                (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps)
   1.132        also have "s' * x + t' * y = r'" by fact
   1.133        also have "s * x + t * y = r" by fact
   1.134 -      also have "r' - r' div r * r = r' mod r" using div_mod_equality[of r' r]
   1.135 +      also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
   1.136          by (simp add: algebra_simps)
   1.137        finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" .
   1.138      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')