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> _)"