stripped dependency on pragmatic type class semiring_div
authorhaftmann
Tue Oct 11 16:44:13 2016 +0200 (2016-10-11)
changeset 6416362c9e5c05928
parent 64162 03057a8fdd1f
child 64164 38c407446400
stripped dependency on pragmatic type class semiring_div
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Oct 12 11:31:08 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Oct 11 16:44:13 2016 +0200
     1.3 @@ -6,6 +6,39 @@
     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 @@ -17,7 +50,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 = semiring_div + normalization_semidom + 
    1.48 +class euclidean_semiring = divide_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 @@ -53,13 +86,39 @@
    1.53    with that and assms show ?thesis by (auto simp add: mod_size_less)
    1.54  qed
    1.55  
    1.56 +lemma zero_mod_left [simp]: "0 mod a = 0"
    1.57 +  using div_mod_equality[of 0 a 0] by simp
    1.58 +
    1.59 +lemma dvd_mod_iff [simp]: 
    1.60 +  assumes "k dvd n"
    1.61 +  shows   "(k dvd m mod n) = (k dvd m)"
    1.62 +proof -
    1.63 +  thm div_mod_equality
    1.64 +  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    1.65 +    by (simp add: dvd_add_right_iff)
    1.66 +  also have "(m div n) * n + m mod n = m"
    1.67 +    using div_mod_equality[of m n 0] by simp
    1.68 +  finally show ?thesis .
    1.69 +qed
    1.70 +
    1.71 +lemma mod_0_imp_dvd: 
    1.72 +  assumes "a mod b = 0"
    1.73 +  shows   "b dvd a"
    1.74 +proof -
    1.75 +  have "b dvd ((a div b) * b)" by simp
    1.76 +  also have "(a div b) * b = a"
    1.77 +    using div_mod_equality[of a b 0] by (simp add: assms)
    1.78 +  finally show ?thesis .
    1.79 +qed
    1.80 +
    1.81  lemma dvd_euclidean_size_eq_imp_dvd:
    1.82    assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
    1.83    shows "a dvd b"
    1.84  proof (rule ccontr)
    1.85    assume "\<not> a dvd b"
    1.86 +  hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
    1.87    then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
    1.88 -  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
    1.89 +  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by simp
    1.90    from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
    1.91      with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
    1.92    with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
    1.93 @@ -434,8 +493,6 @@
    1.94  class euclidean_ring = euclidean_semiring + idom
    1.95  begin
    1.96  
    1.97 -subclass ring_div ..
    1.98 -
    1.99  function euclid_ext_aux :: "'a \<Rightarrow> _" where
   1.100    "euclid_ext_aux r' r s' s t' t = (
   1.101       if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r')
   1.102 @@ -484,7 +541,7 @@
   1.103                (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps)
   1.104        also have "s' * x + t' * y = r'" by fact
   1.105        also have "s * x + t * y = r" by fact
   1.106 -      also have "r' - r' div r * r = r' mod r" using mod_div_equality[of r' r]
   1.107 +      also have "r' - r' div r * r = r' mod r" using div_mod_equality[of r' r]
   1.108          by (simp add: algebra_simps)
   1.109        finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" .
   1.110      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')