src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 64784 5cb5e7ecb284 parent 64592 7759f1766189 child 64785 ae0bbc8e45ad
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 22:57:39 2017 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:28 2017 +0100
1.3 @@ -1,133 +1,17 @@
1.4 -(* Author: Manuel Eberl *)
1.5 +(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
1.6 +    Author:     Manuel Eberl, TU Muenchen
1.7 +*)
1.8
1.9 -section \<open>Abstract euclidean algorithm\<close>
1.10 +section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
1.11
1.12  theory Euclidean_Algorithm
1.13 -imports "~~/src/HOL/GCD" Factorial_Ring
1.14 -begin
1.15 -
1.16 -text \<open>
1.17 -  A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
1.18 -  implemented. It must provide:
1.19 -  \begin{itemize}
1.20 -  \item division with remainder
1.21 -  \item a size function such that @{term "size (a mod b) < size b"}
1.22 -        for any @{term "b \<noteq> 0"}
1.23 -  \end{itemize}
1.24 -  The existence of these functions makes it possible to derive gcd and lcm functions
1.25 -  for any Euclidean semiring.
1.26 -\<close>
1.27 -class euclidean_semiring = semidom_modulo + normalization_semidom +
1.28 -  fixes euclidean_size :: "'a \<Rightarrow> nat"
1.29 -  assumes size_0 [simp]: "euclidean_size 0 = 0"
1.30 -  assumes mod_size_less:
1.31 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
1.32 -  assumes size_mult_mono:
1.33 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
1.34 +  imports "~~/src/HOL/GCD"
1.35 +    "~~/src/HOL/Number_Theory/Factorial_Ring"
1.36 +    "~~/src/HOL/Number_Theory/Euclidean_Division"
1.37  begin
1.38
1.39 -lemma euclidean_size_normalize [simp]:
1.40 -  "euclidean_size (normalize a) = euclidean_size a"
1.41 -proof (cases "a = 0")
1.42 -  case True
1.43 -  then show ?thesis
1.44 -    by simp
1.45 -next
1.46 -  case [simp]: False
1.47 -  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
1.48 -    by (rule size_mult_mono) simp
1.49 -  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
1.50 -    by (rule size_mult_mono) simp
1.51 -  ultimately show ?thesis
1.52 -    by simp
1.53 -qed
1.54 -
1.55 -lemma euclidean_division:
1.56 -  fixes a :: 'a and b :: 'a
1.57 -  assumes "b \<noteq> 0"
1.58 -  obtains s and t where "a = s * b + t"
1.59 -    and "euclidean_size t < euclidean_size b"
1.60 -proof -
1.61 -  from div_mult_mod_eq [of a b]
1.62 -     have "a = a div b * b + a mod b" by simp
1.63 -  with that and assms show ?thesis by (auto simp add: mod_size_less)
1.64 -qed
1.65 -
1.66 -lemma dvd_euclidean_size_eq_imp_dvd:
1.67 -  assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
1.68 -  shows "a dvd b"
1.69 -proof (rule ccontr)
1.70 -  assume "\<not> a dvd b"
1.71 -  hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
1.72 -  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
1.73 -  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
1.74 -  from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
1.75 -    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
1.76 -  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
1.77 -      using size_mult_mono by force
1.78 -  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
1.79 -  have "euclidean_size (b mod a) < euclidean_size a"
1.80 -      using mod_size_less by blast
1.81 -  ultimately show False using size_eq by simp
1.82 -qed
1.83 -
1.84 -lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
1.85 -  by (subst mult.commute) (rule size_mult_mono)
1.86 -
1.87 -lemma euclidean_size_times_unit:
1.88 -  assumes "is_unit a"
1.89 -  shows   "euclidean_size (a * b) = euclidean_size b"
1.90 -proof (rule antisym)
1.91 -  from assms have [simp]: "a \<noteq> 0" by auto
1.92 -  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
1.93 -  from assms have "is_unit (1 div a)" by simp
1.94 -  hence "1 div a \<noteq> 0" by (intro notI) simp_all
1.95 -  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
1.96 -    by (rule size_mult_mono')
1.97 -  also from assms have "(1 div a) * (a * b) = b"
1.98 -    by (simp add: algebra_simps unit_div_mult_swap)
1.99 -  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
1.100 -qed
1.101 -
1.102 -lemma euclidean_size_unit: "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
1.103 -  using euclidean_size_times_unit[of a 1] by simp
1.104 -
1.105 -lemma unit_iff_euclidean_size:
1.106 -  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
1.107 -proof safe
1.108 -  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
1.109 -  show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
1.110 -qed (auto intro: euclidean_size_unit)
1.111 -
1.112 -lemma euclidean_size_times_nonunit:
1.113 -  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a"
1.114 -  shows   "euclidean_size b < euclidean_size (a * b)"
1.115 -proof (rule ccontr)
1.116 -  assume "\<not>euclidean_size b < euclidean_size (a * b)"
1.117 -  with size_mult_mono'[OF assms(1), of b]
1.118 -    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
1.119 -  have "a * b dvd b"
1.120 -    by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all)
1.121 -  hence "a * b dvd 1 * b" by simp
1.122 -  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
1.123 -  with assms(3) show False by contradiction
1.124 -qed
1.125 -
1.126 -lemma dvd_imp_size_le:
1.127 -  assumes "a dvd b" "b \<noteq> 0"
1.128 -  shows   "euclidean_size a \<le> euclidean_size b"
1.129 -  using assms by (auto elim!: dvdE simp: size_mult_mono)
1.130 -
1.131 -lemma dvd_proper_imp_size_less:
1.132 -  assumes "a dvd b" "\<not>b dvd a" "b \<noteq> 0"
1.133 -  shows   "euclidean_size a < euclidean_size b"
1.134 -proof -
1.135 -  from assms(1) obtain c where "b = a * c" by (erule dvdE)
1.136 -  hence z: "b = c * a" by (simp add: mult.commute)
1.137 -  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
1.138 -  with z assms show ?thesis
1.139 -    by (auto intro!: euclidean_size_times_nonunit simp: )
1.140 -qed
1.141 +context euclidean_semiring
1.142 +begin
1.143
1.144  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.145  where
1.146 @@ -432,7 +316,7 @@
1.147
1.148  end
1.149
1.150 -class euclidean_ring = euclidean_semiring + idom
1.151 +context euclidean_ring
1.152  begin
1.153
1.154  function euclid_ext_aux :: "'a \<Rightarrow> _" where
1.155 @@ -680,27 +564,6 @@
1.156
1.157  subsection \<open>Typical instances\<close>
1.158
1.159 -instantiation nat :: euclidean_semiring
1.160 -begin
1.161 -
1.162 -definition [simp]:
1.163 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
1.164 -
1.165 -instance by standard simp_all
1.166 -
1.167 -end
1.168 -
1.169 -
1.170 -instantiation int :: euclidean_ring
1.171 -begin
1.172 -
1.173 -definition [simp]:
1.174 -  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
1.175 -
1.176 -instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
1.177 -
1.178 -end
1.179 -
1.180  instance nat :: euclidean_semiring_gcd
1.181  proof
1.182    show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"