author haftmann Tue Oct 11 16:44:13 2016 +0200 (2016-10-11) changeset 64163 62c9e5c05928 parent 64162 03057a8fdd1f child 64164 38c407446400
stripped dependency on pragmatic type class semiring_div
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.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.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.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.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.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')