src/HOL/GCD.thy
changeset 31706 1db0c8f235fb
parent 30738 0842e906300c
child 31709 061f01ee9978
     1.1 --- a/src/HOL/GCD.thy	Tue Jun 16 22:07:39 2009 -0700
     1.2 +++ b/src/HOL/GCD.thy	Wed Jun 17 16:55:01 2009 -0700
     1.3 @@ -1,202 +1,563 @@
     1.4 -(*  Title:      HOL/GCD.thy
     1.5 -    Author:     Christophe Tabacznyj and Lawrence C Paulson
     1.6 -    Copyright   1996  University of Cambridge
     1.7 +(*  Title:      GCD.thy
     1.8 +    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     1.9 +                Thomas M. Rasmussen, Jeremy Avigad
    1.10 +
    1.11 +
    1.12 +This file deals with the functions gcd and lcm, and properties of
    1.13 +primes. Definitions and lemmas are proved uniformly for the natural
    1.14 +numbers and integers.
    1.15 +
    1.16 +This file combines and revises a number of prior developments.
    1.17 +
    1.18 +The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    1.19 +and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    1.20 +gcd, lcm, and prime for the natural numbers.
    1.21 +
    1.22 +The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    1.23 +extended gcd, lcm, primes to the integers. Amine Chaieb provided
    1.24 +another extension of the notions to the integers, and added a number
    1.25 +of results to "Primes" and "GCD". IntPrimes also defined and developed
    1.26 +the congruence relations on the integers. The notion was extended to
    1.27 +the natural numbers by Chiaeb.
    1.28 +
    1.29  *)
    1.30  
    1.31 -header {* The Greatest Common Divisor *}
    1.32 +
    1.33 +header {* GCD *}
    1.34  
    1.35  theory GCD
    1.36 -imports Main
    1.37 +imports NatTransfer
    1.38 +begin
    1.39 +
    1.40 +declare One_nat_def [simp del]
    1.41 +
    1.42 +subsection {* gcd *}
    1.43 +
    1.44 +class gcd = one +
    1.45 +
    1.46 +fixes
    1.47 +  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    1.48 +  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.49 +
    1.50  begin
    1.51  
    1.52 -text {*
    1.53 -  See \cite{davenport92}. \bigskip
    1.54 -*}
    1.55 +abbreviation
    1.56 +  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.57 +where
    1.58 +  "coprime x y == (gcd x y = 1)"
    1.59 +
    1.60 +end
    1.61 +
    1.62 +class prime = one +
    1.63 +
    1.64 +fixes
    1.65 +  prime :: "'a \<Rightarrow> bool"
    1.66 +
    1.67 +
    1.68 +(* definitions for the natural numbers *)
    1.69 +
    1.70 +instantiation nat :: gcd
    1.71 +
    1.72 +begin
    1.73  
    1.74 -subsection {* Specification of GCD on nats *}
    1.75 +fun
    1.76 +  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.77 +where
    1.78 +  "gcd_nat x y =
    1.79 +   (if y = 0 then x else gcd y (x mod y))"
    1.80 +
    1.81 +definition
    1.82 +  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.83 +where
    1.84 +  "lcm_nat x y = x * y div (gcd x y)"
    1.85 +
    1.86 +instance proof qed
    1.87 +
    1.88 +end
    1.89 +
    1.90 +
    1.91 +instantiation nat :: prime
    1.92 +
    1.93 +begin
    1.94  
    1.95  definition
    1.96 -  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    1.97 -  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    1.98 -    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    1.99 +  prime_nat :: "nat \<Rightarrow> bool"
   1.100 +where
   1.101 +  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
   1.102 +
   1.103 +instance proof qed
   1.104  
   1.105 -text {* Uniqueness *}
   1.106 +end
   1.107 +
   1.108  
   1.109 -lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
   1.110 -  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
   1.111 +(* definitions for the integers *)
   1.112 +
   1.113 +instantiation int :: gcd
   1.114  
   1.115 -text {* Connection to divides relation *}
   1.116 +begin
   1.117  
   1.118 -lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
   1.119 -  by (auto simp add: is_gcd_def)
   1.120 +definition
   1.121 +  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   1.122 +where
   1.123 +  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
   1.124  
   1.125 -text {* Commutativity *}
   1.126 +definition
   1.127 +  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   1.128 +where
   1.129 +  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
   1.130  
   1.131 -lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
   1.132 -  by (auto simp add: is_gcd_def)
   1.133 +instance proof qed
   1.134 +
   1.135 +end
   1.136  
   1.137  
   1.138 -subsection {* GCD on nat by Euclid's algorithm *}
   1.139 +instantiation int :: prime
   1.140 +
   1.141 +begin
   1.142 +
   1.143 +definition
   1.144 +  prime_int :: "int \<Rightarrow> bool"
   1.145 +where
   1.146 +  "prime_int p = prime (nat p)"
   1.147 +
   1.148 +instance proof qed
   1.149 +
   1.150 +end
   1.151 +
   1.152 +
   1.153 +subsection {* Set up Transfer *}
   1.154 +
   1.155 +
   1.156 +lemma transfer_nat_int_gcd:
   1.157 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   1.158 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   1.159 +  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   1.160 +  unfolding gcd_int_def lcm_int_def prime_int_def
   1.161 +  by auto
   1.162  
   1.163 -fun
   1.164 -  gcd  :: "nat => nat => nat"
   1.165 -where
   1.166 -  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
   1.167 -lemma gcd_induct [case_names "0" rec]:
   1.168 +lemma transfer_nat_int_gcd_closures:
   1.169 +  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   1.170 +  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   1.171 +  by (auto simp add: gcd_int_def lcm_int_def)
   1.172 +
   1.173 +declare TransferMorphism_nat_int[transfer add return:
   1.174 +    transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   1.175 +
   1.176 +lemma transfer_int_nat_gcd:
   1.177 +  "gcd (int x) (int y) = int (gcd x y)"
   1.178 +  "lcm (int x) (int y) = int (lcm x y)"
   1.179 +  "prime (int x) = prime x"
   1.180 +  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
   1.181 +
   1.182 +lemma transfer_int_nat_gcd_closures:
   1.183 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   1.184 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   1.185 +  by (auto simp add: gcd_int_def lcm_int_def)
   1.186 +
   1.187 +declare TransferMorphism_int_nat[transfer add return:
   1.188 +    transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   1.189 +
   1.190 +
   1.191 +
   1.192 +subsection {* GCD *}
   1.193 +
   1.194 +(* was gcd_induct *)
   1.195 +lemma nat_gcd_induct:
   1.196    fixes m n :: nat
   1.197    assumes "\<And>m. P m 0"
   1.198      and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   1.199    shows "P m n"
   1.200 -proof (induct m n rule: gcd.induct)
   1.201 -  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
   1.202 -qed
   1.203 +  apply (rule gcd_nat.induct)
   1.204 +  apply (case_tac "y = 0")
   1.205 +  using assms apply simp_all
   1.206 +done
   1.207 +
   1.208 +(* specific to int *)
   1.209 +
   1.210 +lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
   1.211 +  by (simp add: gcd_int_def)
   1.212 +
   1.213 +lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
   1.214 +  by (simp add: gcd_int_def)
   1.215 +
   1.216 +lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
   1.217 +  by (simp add: gcd_int_def)
   1.218 +
   1.219 +lemma int_gcd_cases:
   1.220 +  fixes x :: int and y
   1.221 +  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   1.222 +      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   1.223 +      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   1.224 +      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   1.225 +  shows "P (gcd x y)"
   1.226 +by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
   1.227  
   1.228 -lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
   1.229 -  by simp
   1.230 +lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
   1.231 +  by (simp add: gcd_int_def)
   1.232 +
   1.233 +lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
   1.234 +  by (simp add: lcm_int_def)
   1.235 +
   1.236 +lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
   1.237 +  by (simp add: lcm_int_def)
   1.238 +
   1.239 +lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
   1.240 +  by (simp add: lcm_int_def)
   1.241  
   1.242 -lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
   1.243 +lemma int_lcm_cases:
   1.244 +  fixes x :: int and y
   1.245 +  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   1.246 +      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   1.247 +      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   1.248 +      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   1.249 +  shows "P (lcm x y)"
   1.250 +by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
   1.251 +
   1.252 +lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
   1.253 +  by (simp add: lcm_int_def)
   1.254 +
   1.255 +(* was gcd_0, etc. *)
   1.256 +lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
   1.257    by simp
   1.258  
   1.259 -lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
   1.260 +(* was igcd_0, etc. *)
   1.261 +lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
   1.262 +  by (unfold gcd_int_def, auto)
   1.263 +
   1.264 +lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
   1.265    by simp
   1.266  
   1.267 -lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
   1.268 +lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
   1.269 +  by (unfold gcd_int_def, auto)
   1.270 +
   1.271 +lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
   1.272 +  by (case_tac "y = 0", auto)
   1.273 +
   1.274 +(* weaker, but useful for the simplifier *)
   1.275 +
   1.276 +lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   1.277 +  by simp
   1.278 +
   1.279 +lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   1.280    by simp
   1.281  
   1.282 -lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
   1.283 -  unfolding One_nat_def by (rule gcd_1)
   1.284 +lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   1.285 +  by (simp add: One_nat_def)
   1.286 +
   1.287 +lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
   1.288 +  by (simp add: gcd_int_def)
   1.289  
   1.290 -declare gcd.simps [simp del]
   1.291 +lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
   1.292 +  by simp
   1.293 +
   1.294 +lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
   1.295 +  by (subst int_gcd_abs, auto simp add: gcd_int_def)
   1.296 +
   1.297 +declare gcd_nat.simps [simp del]
   1.298  
   1.299  text {*
   1.300    \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   1.301    conjunctions don't seem provable separately.
   1.302  *}
   1.303  
   1.304 -lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
   1.305 -  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
   1.306 -  apply (induct m n rule: gcd_induct)
   1.307 -     apply (simp_all add: gcd_non_0)
   1.308 +lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
   1.309 +  and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
   1.310 +  apply (induct m n rule: nat_gcd_induct)
   1.311 +  apply (simp_all add: nat_gcd_non_0)
   1.312    apply (blast dest: dvd_mod_imp_dvd)
   1.313 -  done
   1.314 +done
   1.315 +
   1.316 +thm nat_gcd_dvd1 [transferred]
   1.317 +
   1.318 +lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
   1.319 +  apply (subst int_gcd_abs)
   1.320 +  apply (rule dvd_trans)
   1.321 +  apply (rule nat_gcd_dvd1 [transferred])
   1.322 +  apply auto
   1.323 +done
   1.324  
   1.325 -text {*
   1.326 -  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   1.327 -  naturals, if @{term k} divides @{term m} and @{term k} divides
   1.328 -  @{term n} then @{term k} divides @{term "gcd m n"}.
   1.329 -*}
   1.330 +lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
   1.331 +  apply (subst int_gcd_abs)
   1.332 +  apply (rule dvd_trans)
   1.333 +  apply (rule nat_gcd_dvd2 [transferred])
   1.334 +  apply auto
   1.335 +done
   1.336 +
   1.337 +lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   1.338 +  by (rule dvd_imp_le, auto)
   1.339 +
   1.340 +lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   1.341 +  by (rule dvd_imp_le, auto)
   1.342 +
   1.343 +lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   1.344 +  by (rule zdvd_imp_le, auto)
   1.345  
   1.346 -lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   1.347 -  by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
   1.348 +lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   1.349 +  by (rule zdvd_imp_le, auto)
   1.350 +
   1.351 +lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   1.352 +  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
   1.353 +
   1.354 +lemma int_gcd_greatest:
   1.355 +  assumes "(k::int) dvd m" and "k dvd n"
   1.356 +  shows "k dvd gcd m n"
   1.357 +
   1.358 +  apply (subst int_gcd_abs)
   1.359 +  apply (subst abs_dvd_iff [symmetric])
   1.360 +  apply (rule nat_gcd_greatest [transferred])
   1.361 +  using prems apply auto
   1.362 +done
   1.363  
   1.364 -text {*
   1.365 -  \medskip Function gcd yields the Greatest Common Divisor.
   1.366 -*}
   1.367 +lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
   1.368 +    (k dvd m & k dvd n)"
   1.369 +  by (blast intro!: nat_gcd_greatest intro: dvd_trans)
   1.370 +
   1.371 +lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   1.372 +  by (blast intro!: int_gcd_greatest intro: dvd_trans)
   1.373  
   1.374 -lemma is_gcd: "is_gcd m n (gcd m n) "
   1.375 -  by (simp add: is_gcd_def gcd_greatest)
   1.376 +lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   1.377 +  by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
   1.378  
   1.379 +lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   1.380 +  by (auto simp add: gcd_int_def)
   1.381  
   1.382 -subsection {* Derived laws for GCD *}
   1.383 +lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   1.384 +  by (insert nat_gcd_zero [of m n], arith)
   1.385  
   1.386 -lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   1.387 -  by (blast intro!: gcd_greatest intro: dvd_trans)
   1.388 +lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   1.389 +  by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
   1.390 +
   1.391 +lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
   1.392 +  by (rule dvd_anti_sym, auto)
   1.393  
   1.394 -lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   1.395 -  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   1.396 +lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
   1.397 +  by (auto simp add: gcd_int_def nat_gcd_commute)
   1.398 +
   1.399 +lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   1.400 +  apply (rule dvd_anti_sym)
   1.401 +  apply (blast intro: dvd_trans)+
   1.402 +done
   1.403  
   1.404 -lemma gcd_commute: "gcd m n = gcd n m"
   1.405 -  apply (rule is_gcd_unique)
   1.406 -   apply (rule is_gcd)
   1.407 -  apply (subst is_gcd_commute)
   1.408 -  apply (simp add: is_gcd)
   1.409 -  done
   1.410 +lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   1.411 +  by (auto simp add: gcd_int_def nat_gcd_assoc)
   1.412 +
   1.413 +lemma nat_gcd_left_commute: "gcd (k::nat) (gcd m n) = gcd m (gcd k n)"
   1.414 +  apply (rule nat_gcd_commute [THEN trans])
   1.415 +  apply (rule nat_gcd_assoc [THEN trans])
   1.416 +  apply (rule nat_gcd_commute [THEN arg_cong])
   1.417 +done
   1.418 +
   1.419 +lemma int_gcd_left_commute: "gcd (k::int) (gcd m n) = gcd m (gcd k n)"
   1.420 +  apply (rule int_gcd_commute [THEN trans])
   1.421 +  apply (rule int_gcd_assoc [THEN trans])
   1.422 +  apply (rule int_gcd_commute [THEN arg_cong])
   1.423 +done
   1.424 +
   1.425 +lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
   1.426 +  -- {* gcd is an AC-operator *}
   1.427  
   1.428 -lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
   1.429 -  apply (rule is_gcd_unique)
   1.430 -   apply (rule is_gcd)
   1.431 -  apply (simp add: is_gcd_def)
   1.432 -  apply (blast intro: dvd_trans)
   1.433 -  done
   1.434 +lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
   1.435 +
   1.436 +lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
   1.437 +  by (subst nat_gcd_commute, simp)
   1.438 +
   1.439 +lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
   1.440 +  by (subst nat_gcd_commute, simp add: One_nat_def)
   1.441 +
   1.442 +lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
   1.443 +  by (subst int_gcd_commute, simp)
   1.444  
   1.445 -lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
   1.446 -  by (simp add: gcd_commute)
   1.447 +lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
   1.448 +    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.449 +  apply auto
   1.450 +  apply (rule dvd_anti_sym)
   1.451 +  apply (erule (1) nat_gcd_greatest)
   1.452 +  apply auto
   1.453 +done
   1.454  
   1.455 -lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
   1.456 -  unfolding One_nat_def by (rule gcd_1_left)
   1.457 +lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   1.458 +    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.459 +  apply (case_tac "d = 0")
   1.460 +  apply force
   1.461 +  apply (rule iffI)
   1.462 +  apply (rule zdvd_anti_sym)
   1.463 +  apply arith
   1.464 +  apply (subst int_gcd_pos)
   1.465 +  apply clarsimp
   1.466 +  apply (drule_tac x = "d + 1" in spec)
   1.467 +  apply (frule zdvd_imp_le)
   1.468 +  apply (auto intro: int_gcd_greatest)
   1.469 +done
   1.470  
   1.471  text {*
   1.472    \medskip Multiplication laws
   1.473  *}
   1.474  
   1.475 -lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
   1.476 +lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   1.477      -- {* \cite[page 27]{davenport92} *}
   1.478 -  apply (induct m n rule: gcd_induct)
   1.479 -   apply simp
   1.480 +  apply (induct m n rule: nat_gcd_induct)
   1.481 +  apply simp
   1.482    apply (case_tac "k = 0")
   1.483 -   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   1.484 -  done
   1.485 +  apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
   1.486 +done
   1.487  
   1.488 -lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
   1.489 -  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   1.490 -  done
   1.491 +lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   1.492 +  apply (subst (1 2) int_gcd_abs)
   1.493 +  apply (simp add: abs_mult)
   1.494 +  apply (rule nat_gcd_mult_distrib [transferred])
   1.495 +  apply auto
   1.496 +done
   1.497  
   1.498 -lemma gcd_self [simp, algebra]: "gcd k k = k"
   1.499 -  apply (rule gcd_mult [of k 1, simplified])
   1.500 -  done
   1.501 +lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
   1.502 +  by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
   1.503  
   1.504 -lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
   1.505 -  apply (insert gcd_mult_distrib2 [of m k n])
   1.506 +lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
   1.507 +  by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
   1.508 +
   1.509 +lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   1.510 +  apply (insert nat_gcd_mult_distrib [of m k n])
   1.511    apply simp
   1.512    apply (erule_tac t = m in ssubst)
   1.513    apply simp
   1.514    done
   1.515  
   1.516 -lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
   1.517 -  by (auto intro: relprime_dvd_mult dvd_mult2)
   1.518 +lemma int_coprime_dvd_mult:
   1.519 +  assumes "coprime (k::int) n" and "k dvd m * n"
   1.520 +  shows "k dvd m"
   1.521  
   1.522 -lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   1.523 +  using prems
   1.524 +  apply (subst abs_dvd_iff [symmetric])
   1.525 +  apply (subst dvd_abs_iff [symmetric])
   1.526 +  apply (subst (asm) int_gcd_abs)
   1.527 +  apply (rule nat_coprime_dvd_mult [transferred])
   1.528 +  apply auto
   1.529 +  apply (subst abs_mult [symmetric], auto)
   1.530 +done
   1.531 +
   1.532 +lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   1.533 +    (k dvd m * n) = (k dvd m)"
   1.534 +  by (auto intro: nat_coprime_dvd_mult)
   1.535 +
   1.536 +lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
   1.537 +    (k dvd m * n) = (k dvd m)"
   1.538 +  by (auto intro: int_coprime_dvd_mult)
   1.539 +
   1.540 +lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   1.541    apply (rule dvd_anti_sym)
   1.542 -   apply (rule gcd_greatest)
   1.543 -    apply (rule_tac n = k in relprime_dvd_mult)
   1.544 -     apply (simp add: gcd_assoc)
   1.545 -     apply (simp add: gcd_commute)
   1.546 -    apply (simp_all add: mult_commute)
   1.547 -  done
   1.548 +  apply (rule nat_gcd_greatest)
   1.549 +  apply (rule_tac n = k in nat_coprime_dvd_mult)
   1.550 +  apply (simp add: nat_gcd_assoc)
   1.551 +  apply (simp add: nat_gcd_commute)
   1.552 +  apply (simp_all add: mult_commute)
   1.553 +done
   1.554  
   1.555 +lemma int_gcd_mult_cancel:
   1.556 +  assumes "coprime (k::int) n"
   1.557 +  shows "gcd (k * m) n = gcd m n"
   1.558 +
   1.559 +  using prems
   1.560 +  apply (subst (1 2) int_gcd_abs)
   1.561 +  apply (subst abs_mult)
   1.562 +  apply (rule nat_gcd_mult_cancel [transferred])
   1.563 +  apply (auto simp add: int_gcd_abs [symmetric])
   1.564 +done
   1.565  
   1.566  text {* \medskip Addition laws *}
   1.567  
   1.568 -lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
   1.569 -  by (cases "n = 0") (auto simp add: gcd_non_0)
   1.570 +lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
   1.571 +  apply (case_tac "n = 0")
   1.572 +  apply (simp_all add: nat_gcd_non_0)
   1.573 +done
   1.574 +
   1.575 +lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
   1.576 +  apply (subst (1 2) nat_gcd_commute)
   1.577 +  apply (subst add_commute)
   1.578 +  apply simp
   1.579 +done
   1.580 +
   1.581 +(* to do: add the other variations? *)
   1.582 +
   1.583 +lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   1.584 +  by (subst nat_gcd_add1 [symmetric], auto)
   1.585 +
   1.586 +lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.587 +  apply (subst nat_gcd_commute)
   1.588 +  apply (subst nat_gcd_diff1 [symmetric])
   1.589 +  apply auto
   1.590 +  apply (subst nat_gcd_commute)
   1.591 +  apply (subst nat_gcd_diff1)
   1.592 +  apply assumption
   1.593 +  apply (rule nat_gcd_commute)
   1.594 +done
   1.595 +
   1.596 +lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.597 +  apply (frule_tac b = y and a = x in pos_mod_sign)
   1.598 +  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   1.599 +  apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
   1.600 +    zmod_zminus1_eq_if)
   1.601 +  apply (frule_tac a = x in pos_mod_bound)
   1.602 +  apply (subst (1 2) nat_gcd_commute)
   1.603 +  apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
   1.604 +    nat_le_eq_zle)
   1.605 +done
   1.606  
   1.607 -lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
   1.608 -proof -
   1.609 -  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
   1.610 -  also have "... = gcd (n + m) m" by (simp add: add_commute)
   1.611 -  also have "... = gcd n m" by simp
   1.612 -  also have  "... = gcd m n" by (rule gcd_commute)
   1.613 -  finally show ?thesis .
   1.614 -qed
   1.615 +lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
   1.616 +  apply (case_tac "y = 0")
   1.617 +  apply force
   1.618 +  apply (case_tac "y > 0")
   1.619 +  apply (subst int_gcd_non_0, auto)
   1.620 +  apply (insert int_gcd_non_0 [of "-y" "-x"])
   1.621 +  apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
   1.622 +done
   1.623 +
   1.624 +lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   1.625 +  apply (case_tac "n = 0", force)
   1.626 +  apply (subst (1 2) int_gcd_red)
   1.627 +  apply auto
   1.628 +done
   1.629 +
   1.630 +lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.631 +  apply (subst int_gcd_commute)
   1.632 +  apply (subst add_commute)
   1.633 +  apply (subst int_gcd_add1)
   1.634 +  apply (subst int_gcd_commute)
   1.635 +  apply (rule refl)
   1.636 +done
   1.637  
   1.638 -lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
   1.639 -  apply (subst add_commute)
   1.640 -  apply (rule gcd_add2)
   1.641 -  done
   1.642 +lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   1.643 +  by (induct k, simp_all add: ring_simps)
   1.644  
   1.645 -lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
   1.646 -  by (induct k) (simp_all add: add_assoc)
   1.647 +lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   1.648 +  apply (subgoal_tac "ALL s. ALL m. ALL n.
   1.649 +      gcd m (int (s::nat) * m + n) = gcd m n")
   1.650 +  apply (case_tac "k >= 0")
   1.651 +  apply (drule_tac x = "nat k" in spec, force)
   1.652 +  apply (subst (1 2) int_gcd_neg2 [symmetric])
   1.653 +  apply (drule_tac x = "nat (- k)" in spec)
   1.654 +  apply (drule_tac x = "m" in spec)
   1.655 +  apply (drule_tac x = "-n" in spec)
   1.656 +  apply auto
   1.657 +  apply (rule nat_induct)
   1.658 +  apply auto
   1.659 +  apply (auto simp add: left_distrib)
   1.660 +  apply (subst add_assoc)
   1.661 +  apply simp
   1.662 +done
   1.663  
   1.664 -lemma gcd_dvd_prod: "gcd m n dvd m * n" 
   1.665 +(* to do: differences, and all variations of addition rules
   1.666 +    as simplification rules for nat and int *)
   1.667 +
   1.668 +lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   1.669    using mult_dvd_mono [of 1] by auto
   1.670  
   1.671 -text {*
   1.672 -  \medskip Division by gcd yields rrelatively primes.
   1.673 -*}
   1.674 +(* to do: add the three variations of these, and for ints? *)
   1.675 +
   1.676  
   1.677 -lemma div_gcd_relprime:
   1.678 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.679 -  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
   1.680 +subsection {* Coprimality *}
   1.681 +
   1.682 +lemma nat_div_gcd_coprime [intro]:
   1.683 +  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   1.684 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.685  proof -
   1.686    let ?g = "gcd a b"
   1.687    let ?a' = "a div ?g"
   1.688 @@ -207,42 +568,551 @@
   1.689    from dvdg dvdg' obtain ka kb ka' kb' where
   1.690        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   1.691      unfolding dvd_def by blast
   1.692 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
   1.693 +  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.694 +    by simp_all
   1.695    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.696      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   1.697        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.698 -  have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
   1.699 -  then have gp: "?g > 0" by simp
   1.700 -  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.701 +  have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
   1.702 +  then have gp: "?g > 0" by arith
   1.703 +  from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.704    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   1.705  qed
   1.706  
   1.707 +lemma int_div_gcd_coprime [intro]:
   1.708 +  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   1.709 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.710  
   1.711 -lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.712 -proof(auto)
   1.713 -  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   1.714 -  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   1.715 -  have th: "gcd a b dvd d" by blast
   1.716 -  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   1.717 +  apply (subst (1 2 3) int_gcd_abs)
   1.718 +  apply (subst (1 2) abs_div)
   1.719 +  apply auto
   1.720 +  prefer 3
   1.721 +  apply (rule nat_div_gcd_coprime [transferred])
   1.722 +  using nz apply (auto simp add: int_gcd_abs [symmetric])
   1.723 +done
   1.724 +
   1.725 +lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.726 +  using nat_gcd_unique[of 1 a b, simplified] by auto
   1.727 +
   1.728 +lemma nat_coprime_Suc_0:
   1.729 +    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   1.730 +  using nat_coprime by (simp add: One_nat_def)
   1.731 +
   1.732 +lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
   1.733 +    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.734 +  using int_gcd_unique [of 1 a b]
   1.735 +  apply clarsimp
   1.736 +  apply (erule subst)
   1.737 +  apply (rule iffI)
   1.738 +  apply force
   1.739 +  apply (drule_tac x = "abs e" in exI)
   1.740 +  apply (case_tac "e >= 0")
   1.741 +  apply force
   1.742 +  apply force
   1.743 +done
   1.744 +
   1.745 +lemma nat_gcd_coprime:
   1.746 +  assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.747 +    b: "b = b' * gcd a b"
   1.748 +  shows    "coprime a' b'"
   1.749 +
   1.750 +  apply (subgoal_tac "a' = a div gcd a b")
   1.751 +  apply (erule ssubst)
   1.752 +  apply (subgoal_tac "b' = b div gcd a b")
   1.753 +  apply (erule ssubst)
   1.754 +  apply (rule nat_div_gcd_coprime)
   1.755 +  using prems
   1.756 +  apply force
   1.757 +  apply (subst (1) b)
   1.758 +  using z apply force
   1.759 +  apply (subst (1) a)
   1.760 +  using z apply force
   1.761 +done
   1.762 +
   1.763 +lemma int_gcd_coprime:
   1.764 +  assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.765 +    b: "b = b' * gcd a b"
   1.766 +  shows    "coprime a' b'"
   1.767 +
   1.768 +  apply (subgoal_tac "a' = a div gcd a b")
   1.769 +  apply (erule ssubst)
   1.770 +  apply (subgoal_tac "b' = b div gcd a b")
   1.771 +  apply (erule ssubst)
   1.772 +  apply (rule int_div_gcd_coprime)
   1.773 +  using prems
   1.774 +  apply force
   1.775 +  apply (subst (1) b)
   1.776 +  using z apply force
   1.777 +  apply (subst (1) a)
   1.778 +  using z apply force
   1.779 +done
   1.780 +
   1.781 +lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   1.782 +    shows "coprime d (a * b)"
   1.783 +  apply (subst nat_gcd_commute)
   1.784 +  using da apply (subst nat_gcd_mult_cancel)
   1.785 +  apply (subst nat_gcd_commute, assumption)
   1.786 +  apply (subst nat_gcd_commute, rule db)
   1.787 +done
   1.788 +
   1.789 +lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
   1.790 +    shows "coprime d (a * b)"
   1.791 +  apply (subst int_gcd_commute)
   1.792 +  using da apply (subst int_gcd_mult_cancel)
   1.793 +  apply (subst int_gcd_commute, assumption)
   1.794 +  apply (subst int_gcd_commute, rule db)
   1.795 +done
   1.796 +
   1.797 +lemma nat_coprime_lmult:
   1.798 +  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   1.799 +proof -
   1.800 +  have "gcd d a dvd gcd d (a * b)"
   1.801 +    by (rule nat_gcd_greatest, auto)
   1.802 +  with dab show ?thesis
   1.803 +    by auto
   1.804 +qed
   1.805 +
   1.806 +lemma int_coprime_lmult:
   1.807 +  assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
   1.808 +proof -
   1.809 +  have "gcd d a dvd gcd d (a * b)"
   1.810 +    by (rule int_gcd_greatest, auto)
   1.811 +  with dab show ?thesis
   1.812 +    by auto
   1.813 +qed
   1.814 +
   1.815 +lemma nat_coprime_rmult:
   1.816 +  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
   1.817 +proof -
   1.818 +  have "gcd d b dvd gcd d (a * b)"
   1.819 +    by (rule nat_gcd_greatest, auto intro: dvd_mult)
   1.820 +  with dab show ?thesis
   1.821 +    by auto
   1.822 +qed
   1.823 +
   1.824 +lemma int_coprime_rmult:
   1.825 +  assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   1.826 +proof -
   1.827 +  have "gcd d b dvd gcd d (a * b)"
   1.828 +    by (rule int_gcd_greatest, auto intro: dvd_mult)
   1.829 +  with dab show ?thesis
   1.830 +    by auto
   1.831 +qed
   1.832 +
   1.833 +lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
   1.834 +    coprime d a \<and>  coprime d b"
   1.835 +  using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
   1.836 +    nat_coprime_mult[of d a b]
   1.837 +  by blast
   1.838 +
   1.839 +lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
   1.840 +    coprime d a \<and>  coprime d b"
   1.841 +  using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
   1.842 +    int_coprime_mult[of d a b]
   1.843 +  by blast
   1.844 +
   1.845 +lemma nat_gcd_coprime_exists:
   1.846 +    assumes nz: "gcd (a::nat) b \<noteq> 0"
   1.847 +    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.848 +  apply (rule_tac x = "a div gcd a b" in exI)
   1.849 +  apply (rule_tac x = "b div gcd a b" in exI)
   1.850 +  using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
   1.851 +done
   1.852 +
   1.853 +lemma int_gcd_coprime_exists:
   1.854 +    assumes nz: "gcd (a::int) b \<noteq> 0"
   1.855 +    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.856 +  apply (rule_tac x = "a div gcd a b" in exI)
   1.857 +  apply (rule_tac x = "b div gcd a b" in exI)
   1.858 +  using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
   1.859 +done
   1.860 +
   1.861 +lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   1.862 +  by (induct n, simp_all add: nat_coprime_mult)
   1.863 +
   1.864 +lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   1.865 +  by (induct n, simp_all add: int_coprime_mult)
   1.866 +
   1.867 +lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.868 +  apply (rule nat_coprime_exp)
   1.869 +  apply (subst nat_gcd_commute)
   1.870 +  apply (rule nat_coprime_exp)
   1.871 +  apply (subst nat_gcd_commute, assumption)
   1.872 +done
   1.873 +
   1.874 +lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.875 +  apply (rule int_coprime_exp)
   1.876 +  apply (subst int_gcd_commute)
   1.877 +  apply (rule int_coprime_exp)
   1.878 +  apply (subst int_gcd_commute, assumption)
   1.879 +done
   1.880 +
   1.881 +lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   1.882 +proof (cases)
   1.883 +  assume "a = 0 & b = 0"
   1.884 +  thus ?thesis by simp
   1.885 +  next assume "~(a = 0 & b = 0)"
   1.886 +  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   1.887 +    by auto
   1.888 +  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   1.889 +      ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   1.890 +    apply (subst (1 2) mult_commute)
   1.891 +    apply (subst nat_gcd_mult_distrib [symmetric])
   1.892 +    apply simp
   1.893 +    done
   1.894 +  also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   1.895 +    apply (subst div_power)
   1.896 +    apply auto
   1.897 +    apply (rule dvd_div_mult_self)
   1.898 +    apply (rule dvd_power_same)
   1.899 +    apply auto
   1.900 +    done
   1.901 +  also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   1.902 +    apply (subst div_power)
   1.903 +    apply auto
   1.904 +    apply (rule dvd_div_mult_self)
   1.905 +    apply (rule dvd_power_same)
   1.906 +    apply auto
   1.907 +    done
   1.908 +  finally show ?thesis .
   1.909 +qed
   1.910 +
   1.911 +lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   1.912 +  apply (subst (1 2) int_gcd_abs)
   1.913 +  apply (subst (1 2) power_abs)
   1.914 +  apply (rule nat_gcd_exp [where n = n, transferred])
   1.915 +  apply auto
   1.916 +done
   1.917 +
   1.918 +lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.919 +  using nat_coprime_dvd_mult_iff[of d a b]
   1.920 +  by (auto simp add: mult_commute)
   1.921 +
   1.922 +lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.923 +  using int_coprime_dvd_mult_iff[of d a b]
   1.924 +  by (auto simp add: mult_commute)
   1.925 +
   1.926 +lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
   1.927 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.928 +proof-
   1.929 +  let ?g = "gcd a b"
   1.930 +  {assume "?g = 0" with dc have ?thesis by auto}
   1.931 +  moreover
   1.932 +  {assume z: "?g \<noteq> 0"
   1.933 +    from nat_gcd_coprime_exists[OF z]
   1.934 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.935 +      by blast
   1.936 +    have thb: "?g dvd b" by auto
   1.937 +    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   1.938 +    with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   1.939 +    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.940 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   1.941 +    with z have th_1: "a' dvd b' * c" by auto
   1.942 +    from nat_coprime_dvd_mult[OF ab'(3)] th_1
   1.943 +    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   1.944 +    from ab' have "a = ?g*a'" by algebra
   1.945 +    with thb thc have ?thesis by blast }
   1.946 +  ultimately show ?thesis by blast
   1.947 +qed
   1.948 +
   1.949 +lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
   1.950 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.951 +proof-
   1.952 +  let ?g = "gcd a b"
   1.953 +  {assume "?g = 0" with dc have ?thesis by auto}
   1.954 +  moreover
   1.955 +  {assume z: "?g \<noteq> 0"
   1.956 +    from int_gcd_coprime_exists[OF z]
   1.957 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.958 +      by blast
   1.959 +    have thb: "?g dvd b" by auto
   1.960 +    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   1.961 +    with dc have th0: "a' dvd b*c"
   1.962 +      using dvd_trans[of a' a "b*c"] by simp
   1.963 +    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.964 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   1.965 +    with z have th_1: "a' dvd b' * c" by auto
   1.966 +    from int_coprime_dvd_mult[OF ab'(3)] th_1
   1.967 +    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   1.968 +    from ab' have "a = ?g*a'" by algebra
   1.969 +    with thb thc have ?thesis by blast }
   1.970 +  ultimately show ?thesis by blast
   1.971  qed
   1.972  
   1.973 -lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
   1.974 -  shows "gcd x y = gcd u v"
   1.975 +lemma nat_pow_divides_pow:
   1.976 +  assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   1.977 +  shows "a dvd b"
   1.978 +proof-
   1.979 +  let ?g = "gcd a b"
   1.980 +  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   1.981 +  {assume "?g = 0" with ab n have ?thesis by auto }
   1.982 +  moreover
   1.983 +  {assume z: "?g \<noteq> 0"
   1.984 +    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   1.985 +    from nat_gcd_coprime_exists[OF z]
   1.986 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.987 +      by blast
   1.988 +    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   1.989 +      by (simp add: ab'(1,2)[symmetric])
   1.990 +    hence "?g^n*a'^n dvd ?g^n *b'^n"
   1.991 +      by (simp only: power_mult_distrib mult_commute)
   1.992 +    with zn z n have th0:"a'^n dvd b'^n" by auto
   1.993 +    have "a' dvd a'^n" by (simp add: m)
   1.994 +    with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.995 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   1.996 +    from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
   1.997 +    have "a' dvd b'" by (subst (asm) mult_commute, blast)
   1.998 +    hence "a'*?g dvd b'*?g" by simp
   1.999 +    with ab'(1,2)  have ?thesis by simp }
  1.1000 +  ultimately show ?thesis by blast
  1.1001 +qed
  1.1002 +
  1.1003 +lemma int_pow_divides_pow:
  1.1004 +  assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1.1005 +  shows "a dvd b"
  1.1006  proof-
  1.1007 -  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
  1.1008 -  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
  1.1009 +  let ?g = "gcd a b"
  1.1010 +  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1.1011 +  {assume "?g = 0" with ab n have ?thesis by auto }
  1.1012 +  moreover
  1.1013 +  {assume z: "?g \<noteq> 0"
  1.1014 +    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
  1.1015 +    from int_gcd_coprime_exists[OF z]
  1.1016 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1.1017 +      by blast
  1.1018 +    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1.1019 +      by (simp add: ab'(1,2)[symmetric])
  1.1020 +    hence "?g^n*a'^n dvd ?g^n *b'^n"
  1.1021 +      by (simp only: power_mult_distrib mult_commute)
  1.1022 +    with zn z n have th0:"a'^n dvd b'^n" by auto
  1.1023 +    have "a' dvd a'^n" by (simp add: m)
  1.1024 +    with th0 have "a' dvd b'^n"
  1.1025 +      using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1.1026 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
  1.1027 +    from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
  1.1028 +    have "a' dvd b'" by (subst (asm) mult_commute, blast)
  1.1029 +    hence "a'*?g dvd b'*?g" by simp
  1.1030 +    with ab'(1,2)  have ?thesis by simp }
  1.1031 +  ultimately show ?thesis by blast
  1.1032 +qed
  1.1033 +
  1.1034 +lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
  1.1035 +  by (auto intro: nat_pow_divides_pow dvd_power_same)
  1.1036 +
  1.1037 +lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
  1.1038 +  by (auto intro: int_pow_divides_pow dvd_power_same)
  1.1039 +
  1.1040 +lemma nat_divides_mult:
  1.1041 +  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1.1042 +  shows "m * n dvd r"
  1.1043 +proof-
  1.1044 +  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1.1045 +    unfolding dvd_def by blast
  1.1046 +  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
  1.1047 +  hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
  1.1048 +  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1.1049 +  from n' k show ?thesis unfolding dvd_def by auto
  1.1050 +qed
  1.1051 +
  1.1052 +lemma int_divides_mult:
  1.1053 +  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1.1054 +  shows "m * n dvd r"
  1.1055 +proof-
  1.1056 +  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1.1057 +    unfolding dvd_def by blast
  1.1058 +  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
  1.1059 +  hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
  1.1060 +  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1.1061 +  from n' k show ?thesis unfolding dvd_def by auto
  1.1062  qed
  1.1063  
  1.1064 -lemma ind_euclid: 
  1.1065 -  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
  1.1066 -  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
  1.1067 +lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
  1.1068 +  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
  1.1069 +  apply force
  1.1070 +  apply (rule nat_dvd_diff)
  1.1071 +  apply auto
  1.1072 +done
  1.1073 +
  1.1074 +lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
  1.1075 +  using nat_coprime_plus_one by (simp add: One_nat_def)
  1.1076 +
  1.1077 +lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
  1.1078 +  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
  1.1079 +  apply force
  1.1080 +  apply (rule dvd_diff)
  1.1081 +  apply auto
  1.1082 +done
  1.1083 +
  1.1084 +lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1.1085 +  using nat_coprime_plus_one [of "n - 1"]
  1.1086 +    nat_gcd_commute [of "n - 1" n] by auto
  1.1087 +
  1.1088 +lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
  1.1089 +  using int_coprime_plus_one [of "n - 1"]
  1.1090 +    int_gcd_commute [of "n - 1" n] by auto
  1.1091 +
  1.1092 +lemma nat_setprod_coprime [rule_format]:
  1.1093 +    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
  1.1094 +  apply (case_tac "finite A")
  1.1095 +  apply (induct set: finite)
  1.1096 +  apply (auto simp add: nat_gcd_mult_cancel)
  1.1097 +done
  1.1098 +
  1.1099 +lemma int_setprod_coprime [rule_format]:
  1.1100 +    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
  1.1101 +  apply (case_tac "finite A")
  1.1102 +  apply (induct set: finite)
  1.1103 +  apply (auto simp add: int_gcd_mult_cancel)
  1.1104 +done
  1.1105 +
  1.1106 +lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1.1107 +  unfolding prime_nat_def
  1.1108 +  apply (subst even_mult_two_ex)
  1.1109 +  apply clarify
  1.1110 +  apply (drule_tac x = 2 in spec)
  1.1111 +  apply auto
  1.1112 +done
  1.1113 +
  1.1114 +lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1.1115 +  unfolding prime_int_def
  1.1116 +  apply (frule nat_prime_odd)
  1.1117 +  apply (auto simp add: even_nat_def)
  1.1118 +done
  1.1119 +
  1.1120 +lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1121 +    x dvd b \<Longrightarrow> x = 1"
  1.1122 +  apply (subgoal_tac "x dvd gcd a b")
  1.1123 +  apply simp
  1.1124 +  apply (erule (1) nat_gcd_greatest)
  1.1125 +done
  1.1126 +
  1.1127 +lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1128 +    x dvd b \<Longrightarrow> abs x = 1"
  1.1129 +  apply (subgoal_tac "x dvd gcd a b")
  1.1130 +  apply simp
  1.1131 +  apply (erule (1) int_gcd_greatest)
  1.1132 +done
  1.1133 +
  1.1134 +lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1.1135 +    coprime d e"
  1.1136 +  apply (auto simp add: dvd_def)
  1.1137 +  apply (frule int_coprime_lmult)
  1.1138 +  apply (subst int_gcd_commute)
  1.1139 +  apply (subst (asm) (2) int_gcd_commute)
  1.1140 +  apply (erule int_coprime_lmult)
  1.1141 +done
  1.1142 +
  1.1143 +lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1144 +apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
  1.1145 +done
  1.1146 +
  1.1147 +lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1148 +apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
  1.1149 +done
  1.1150 +
  1.1151 +
  1.1152 +subsection {* Bezout's theorem *}
  1.1153 +
  1.1154 +(* Function bezw returns a pair of witnesses to Bezout's theorem --
  1.1155 +   see the theorems that follow the definition. *)
  1.1156 +fun
  1.1157 +  bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1.1158 +where
  1.1159 +  "bezw x y =
  1.1160 +  (if y = 0 then (1, 0) else
  1.1161 +      (snd (bezw y (x mod y)),
  1.1162 +       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1.1163 +
  1.1164 +lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1.1165 +
  1.1166 +lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1.1167 +       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1.1168 +  by simp
  1.1169 +
  1.1170 +declare bezw.simps [simp del]
  1.1171 +
  1.1172 +lemma bezw_aux [rule_format]:
  1.1173 +    "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1.1174 +proof (induct x y rule: nat_gcd_induct)
  1.1175 +  fix m :: nat
  1.1176 +  show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1.1177 +    by auto
  1.1178 +  next fix m :: nat and n
  1.1179 +    assume ngt0: "n > 0" and
  1.1180 +      ih: "fst (bezw n (m mod n)) * int n +
  1.1181 +        snd (bezw n (m mod n)) * int (m mod n) =
  1.1182 +        int (gcd n (m mod n))"
  1.1183 +    thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1.1184 +      apply (simp add: bezw_non_0 nat_gcd_non_0)
  1.1185 +      apply (erule subst)
  1.1186 +      apply (simp add: ring_simps)
  1.1187 +      apply (subst mod_div_equality [of m n, symmetric])
  1.1188 +      (* applying simp here undoes the last substitution!
  1.1189 +         what is procedure cancel_div_mod? *)
  1.1190 +      apply (simp only: ring_simps zadd_int [symmetric]
  1.1191 +        zmult_int [symmetric])
  1.1192 +      done
  1.1193 +qed
  1.1194 +
  1.1195 +lemma int_bezout:
  1.1196 +  fixes x y
  1.1197 +  shows "EX u v. u * (x::int) + v * y = gcd x y"
  1.1198 +proof -
  1.1199 +  have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1.1200 +      EX u v. u * x + v * y = gcd x y"
  1.1201 +    apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1.1202 +    apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1.1203 +    apply (unfold gcd_int_def)
  1.1204 +    apply simp
  1.1205 +    apply (subst bezw_aux [symmetric])
  1.1206 +    apply auto
  1.1207 +    done
  1.1208 +  have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1.1209 +      (x \<le> 0 \<and> y \<le> 0)"
  1.1210 +    by auto
  1.1211 +  moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1.1212 +    by (erule (1) bezout_aux)
  1.1213 +  moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1.1214 +    apply (insert bezout_aux [of x "-y"])
  1.1215 +    apply auto
  1.1216 +    apply (rule_tac x = u in exI)
  1.1217 +    apply (rule_tac x = "-v" in exI)
  1.1218 +    apply (subst int_gcd_neg2 [symmetric])
  1.1219 +    apply auto
  1.1220 +    done
  1.1221 +  moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1.1222 +    apply (insert bezout_aux [of "-x" y])
  1.1223 +    apply auto
  1.1224 +    apply (rule_tac x = "-u" in exI)
  1.1225 +    apply (rule_tac x = v in exI)
  1.1226 +    apply (subst int_gcd_neg1 [symmetric])
  1.1227 +    apply auto
  1.1228 +    done
  1.1229 +  moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1.1230 +    apply (insert bezout_aux [of "-x" "-y"])
  1.1231 +    apply auto
  1.1232 +    apply (rule_tac x = "-u" in exI)
  1.1233 +    apply (rule_tac x = "-v" in exI)
  1.1234 +    apply (subst int_gcd_neg1 [symmetric])
  1.1235 +    apply (subst int_gcd_neg2 [symmetric])
  1.1236 +    apply auto
  1.1237 +    done
  1.1238 +  ultimately show ?thesis by blast
  1.1239 +qed
  1.1240 +
  1.1241 +text {* versions of Bezout for nat, by Amine Chaieb *}
  1.1242 +
  1.1243 +lemma ind_euclid:
  1.1244 +  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1.1245 +  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1.1246    shows "P a b"
  1.1247  proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1.1248    fix n a b
  1.1249    assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1.1250    have "a = b \<or> a < b \<or> b < a" by arith
  1.1251    moreover {assume eq: "a= b"
  1.1252 -    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
  1.1253 +    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1.1254 +    by simp}
  1.1255    moreover
  1.1256    {assume lt: "a < b"
  1.1257      hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1.1258 @@ -269,65 +1139,67 @@
  1.1259  ultimately  show "P a b" by blast
  1.1260  qed
  1.1261  
  1.1262 -lemma bezout_lemma: 
  1.1263 -  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1264 -  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1.1265 -using ex
  1.1266 -apply clarsimp
  1.1267 -apply (rule_tac x="d" in exI, simp add: dvd_add)
  1.1268 -apply (case_tac "a * x = b * y + d" , simp_all)
  1.1269 -apply (rule_tac x="x + y" in exI)
  1.1270 -apply (rule_tac x="y" in exI)
  1.1271 -apply algebra
  1.1272 -apply (rule_tac x="x" in exI)
  1.1273 -apply (rule_tac x="x + y" in exI)
  1.1274 -apply algebra
  1.1275 +lemma nat_bezout_lemma:
  1.1276 +  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1277 +    (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1278 +  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1.1279 +    (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1.1280 +  using ex
  1.1281 +  apply clarsimp
  1.1282 +  apply (rule_tac x="d" in exI, simp add: dvd_add)
  1.1283 +  apply (case_tac "a * x = b * y + d" , simp_all)
  1.1284 +  apply (rule_tac x="x + y" in exI)
  1.1285 +  apply (rule_tac x="y" in exI)
  1.1286 +  apply algebra
  1.1287 +  apply (rule_tac x="x" in exI)
  1.1288 +  apply (rule_tac x="x + y" in exI)
  1.1289 +  apply algebra
  1.1290  done
  1.1291  
  1.1292 -lemma bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1293 -apply(induct a b rule: ind_euclid)
  1.1294 -apply blast
  1.1295 -apply clarify
  1.1296 -apply (rule_tac x="a" in exI, simp add: dvd_add)
  1.1297 -apply clarsimp
  1.1298 -apply (rule_tac x="d" in exI)
  1.1299 -apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1.1300 -apply (rule_tac x="x+y" in exI)
  1.1301 -apply (rule_tac x="y" in exI)
  1.1302 -apply algebra
  1.1303 -apply (rule_tac x="x" in exI)
  1.1304 -apply (rule_tac x="x+y" in exI)
  1.1305 -apply algebra
  1.1306 +lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1307 +    (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1308 +  apply(induct a b rule: ind_euclid)
  1.1309 +  apply blast
  1.1310 +  apply clarify
  1.1311 +  apply (rule_tac x="a" in exI, simp add: dvd_add)
  1.1312 +  apply clarsimp
  1.1313 +  apply (rule_tac x="d" in exI)
  1.1314 +  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1.1315 +  apply (rule_tac x="x+y" in exI)
  1.1316 +  apply (rule_tac x="y" in exI)
  1.1317 +  apply algebra
  1.1318 +  apply (rule_tac x="x" in exI)
  1.1319 +  apply (rule_tac x="x+y" in exI)
  1.1320 +  apply algebra
  1.1321  done
  1.1322  
  1.1323 -lemma bezout: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)"
  1.1324 -using bezout_add[of a b]
  1.1325 -apply clarsimp
  1.1326 -apply (rule_tac x="d" in exI, simp)
  1.1327 -apply (rule_tac x="x" in exI)
  1.1328 -apply (rule_tac x="y" in exI)
  1.1329 -apply auto
  1.1330 +lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1331 +    (a * x - b * y = d \<or> b * x - a * y = d)"
  1.1332 +  using nat_bezout_add[of a b]
  1.1333 +  apply clarsimp
  1.1334 +  apply (rule_tac x="d" in exI, simp)
  1.1335 +  apply (rule_tac x="x" in exI)
  1.1336 +  apply (rule_tac x="y" in exI)
  1.1337 +  apply auto
  1.1338  done
  1.1339  
  1.1340 -
  1.1341 -text {* We can get a stronger version with a nonzeroness assumption. *}
  1.1342 -lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
  1.1343 -
  1.1344 -lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  1.1345 +lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  1.1346    shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1.1347  proof-
  1.1348 -  from nz have ap: "a > 0" by simp
  1.1349 - from bezout_add[of a b] 
  1.1350 - have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1.1351 + from nz have ap: "a > 0" by simp
  1.1352 + from nat_bezout_add[of a b]
  1.1353 + have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1.1354 +   (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1.1355   moreover
  1.1356 - {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1.1357 -   from H have ?thesis by blast }
  1.1358 +    {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1.1359 +     from H have ?thesis by blast }
  1.1360   moreover
  1.1361   {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1.1362     {assume b0: "b = 0" with H  have ?thesis by simp}
  1.1363 -   moreover 
  1.1364 +   moreover
  1.1365     {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1.1366 -     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
  1.1367 +     from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1.1368 +       by auto
  1.1369       moreover
  1.1370       {assume db: "d=b"
  1.1371         from prems have ?thesis apply simp
  1.1372 @@ -335,18 +1207,22 @@
  1.1373  	 apply (rule exI[where x = b])
  1.1374  	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1.1375      moreover
  1.1376 -    {assume db: "d < b" 
  1.1377 +    {assume db: "d < b"
  1.1378  	{assume "x=0" hence ?thesis  using prems by simp }
  1.1379  	moreover
  1.1380  	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1.1381 -	  
  1.1382  	  from db have "d \<le> b - 1" by simp
  1.1383  	  hence "d*b \<le> b*(b - 1)" by simp
  1.1384  	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1.1385  	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1.1386 -	  from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
  1.1387 +	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1.1388 +            by simp
  1.1389 +	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1.1390 +	    by (simp only: mult_assoc right_distrib)
  1.1391 +	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1.1392 +            by algebra
  1.1393  	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1.1394 -	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
  1.1395 +	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1.1396  	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1.1397  	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1.1398  	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1.1399 @@ -361,156 +1237,156 @@
  1.1400   ultimately show ?thesis by blast
  1.1401  qed
  1.1402  
  1.1403 -
  1.1404 -lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
  1.1405 -proof-
  1.1406 -  let ?g = "gcd a b"
  1.1407 -  from bezout[of a b] obtain d x y where d: "d dvd a" "d dvd b" "a * x - b * y = d \<or> b * x - a * y = d" by blast
  1.1408 -  from d(1,2) have "d dvd ?g" by simp
  1.1409 -  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1.1410 -  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
  1.1411 -  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k" 
  1.1412 -    by (algebra add: diff_mult_distrib)
  1.1413 -  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g" 
  1.1414 -    by (simp add: k mult_assoc)
  1.1415 -  thus ?thesis by blast
  1.1416 -qed
  1.1417 -
  1.1418 -lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
  1.1419 +lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
  1.1420    shows "\<exists>x y. a * x = b * y + gcd a b"
  1.1421  proof-
  1.1422    let ?g = "gcd a b"
  1.1423 -  from bezout_add_strong[OF a, of b]
  1.1424 +  from nat_bezout_add_strong[OF a, of b]
  1.1425    obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1.1426    from d(1,2) have "d dvd ?g" by simp
  1.1427    then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1.1428 -  from d(3) have "a * x * k = (b * y + d) *k " by algebra
  1.1429 +  from d(3) have "a * x * k = (b * y + d) *k " by auto
  1.1430    hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1.1431    thus ?thesis by blast
  1.1432  qed
  1.1433  
  1.1434 -lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
  1.1435 -by(simp add: gcd_mult_distrib2 mult_commute)
  1.1436 +
  1.1437 +subsection {* LCM *}
  1.1438 +
  1.1439 +lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1.1440 +  by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1.1441 +    zmult_int [symmetric] gcd_int_def)
  1.1442 +
  1.1443 +lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
  1.1444 +  unfolding lcm_nat_def
  1.1445 +  by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
  1.1446 +
  1.1447 +lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
  1.1448 +  unfolding lcm_int_def gcd_int_def
  1.1449 +  apply (subst int_mult [symmetric])
  1.1450 +  apply (subst nat_prod_gcd_lcm [symmetric])
  1.1451 +  apply (subst nat_abs_mult_distrib [symmetric])
  1.1452 +  apply (simp, simp add: abs_mult)
  1.1453 +done
  1.1454 +
  1.1455 +lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
  1.1456 +  unfolding lcm_nat_def by simp
  1.1457 +
  1.1458 +lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
  1.1459 +  unfolding lcm_int_def by simp
  1.1460 +
  1.1461 +lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
  1.1462 +  unfolding lcm_nat_def by simp
  1.1463 +
  1.1464 +lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
  1.1465 +  unfolding lcm_nat_def by (simp add: One_nat_def)
  1.1466 +
  1.1467 +lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
  1.1468 +  unfolding lcm_int_def by simp
  1.1469 +
  1.1470 +lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
  1.1471 +  unfolding lcm_nat_def by simp
  1.1472  
  1.1473 -lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
  1.1474 -  (is "?lhs \<longleftrightarrow> ?rhs")
  1.1475 -proof-
  1.1476 -  let ?g = "gcd a b"
  1.1477 -  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
  1.1478 -    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
  1.1479 -      by blast
  1.1480 -    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
  1.1481 -    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
  1.1482 -      by (simp only: diff_mult_distrib)
  1.1483 -    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d"
  1.1484 -      by (simp add: k[symmetric] mult_assoc)
  1.1485 -    hence ?lhs by blast}
  1.1486 +lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
  1.1487 +  unfolding lcm_int_def by simp
  1.1488 +
  1.1489 +lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
  1.1490 +  unfolding lcm_nat_def by simp
  1.1491 +
  1.1492 +lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
  1.1493 +  unfolding lcm_nat_def by (simp add: One_nat_def)
  1.1494 +
  1.1495 +lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
  1.1496 +  unfolding lcm_int_def by simp
  1.1497 +
  1.1498 +lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
  1.1499 +  unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
  1.1500 +
  1.1501 +lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
  1.1502 +  unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
  1.1503 +
  1.1504 +(* to do: show lcm is associative, and then declare ac simps *)
  1.1505 +
  1.1506 +lemma nat_lcm_pos:
  1.1507 +  assumes mpos: "(m::nat) > 0"
  1.1508 +  and npos: "n>0"
  1.1509 +  shows "lcm m n > 0"
  1.1510 +proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
  1.1511 +  assume h:"m*n div gcd m n = 0"
  1.1512 +  from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
  1.1513 +  hence gcdp: "gcd m n > 0" by simp
  1.1514 +  with h
  1.1515 +  have "m*n < gcd m n"
  1.1516 +    by (cases "m * n < gcd m n")
  1.1517 +       (auto simp add: div_if[OF gcdp, where m="m*n"])
  1.1518    moreover
  1.1519 -  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
  1.1520 -    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
  1.1521 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
  1.1522 -    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
  1.1523 -    have ?rhs by auto}
  1.1524 -  ultimately show ?thesis by blast
  1.1525 -qed
  1.1526 -
  1.1527 -lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
  1.1528 -proof-
  1.1529 -  let ?g = "gcd a b"
  1.1530 -    have dv: "?g dvd a*x" "?g dvd b * y" 
  1.1531 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
  1.1532 -    from dvd_add[OF dv] H
  1.1533 -    show ?thesis by auto
  1.1534 +  have "gcd m n dvd m" by simp
  1.1535 +  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
  1.1536 +  with npos have t1:"gcd m n*n \<le> m*n" by simp
  1.1537 +  have "gcd m n \<le> gcd m n*n" using npos by simp
  1.1538 +  with t1 have "gcd m n \<le> m*n" by arith
  1.1539 +  ultimately show "False" by simp
  1.1540  qed
  1.1541  
  1.1542 -lemma gcd_mult': "gcd b (a * b) = b"
  1.1543 -by (simp add: gcd_mult mult_commute[of a b]) 
  1.1544 -
  1.1545 -lemma gcd_add: "gcd(a + b) b = gcd a b" 
  1.1546 -  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
  1.1547 -apply (simp_all add: gcd_add1)
  1.1548 -by (simp add: gcd_commute gcd_add1)
  1.1549 -
  1.1550 -lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
  1.1551 -proof-
  1.1552 -  {fix a b assume H: "b \<le> (a::nat)"
  1.1553 -    hence th: "a - b + b = a" by arith
  1.1554 -    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
  1.1555 -  note th = this
  1.1556 -{
  1.1557 -  assume ab: "b \<le> a"
  1.1558 -  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
  1.1559 -next
  1.1560 -  assume ab: "a \<le> b"
  1.1561 -  from th[OF ab] show "gcd a (b - a) = gcd a b" 
  1.1562 -    by (simp add: gcd_commute)}
  1.1563 -qed
  1.1564 -
  1.1565 +lemma int_lcm_pos:
  1.1566 +  assumes mneq0: "(m::int) ~= 0"
  1.1567 +  and npos: "n ~= 0"
  1.1568 +  shows "lcm m n > 0"
  1.1569  
  1.1570 -subsection {* LCM defined by GCD *}
  1.1571 -
  1.1572 -
  1.1573 -definition
  1.1574 -  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1.1575 -where
  1.1576 -  lcm_def: "lcm m n = m * n div gcd m n"
  1.1577 -
  1.1578 -lemma prod_gcd_lcm:
  1.1579 -  "m * n = gcd m n * lcm m n"
  1.1580 -  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  1.1581 +  apply (subst int_lcm_abs)
  1.1582 +  apply (rule nat_lcm_pos [transferred])
  1.1583 +  using prems apply auto
  1.1584 +done
  1.1585  
  1.1586 -lemma lcm_0 [simp]: "lcm m 0 = 0"
  1.1587 -  unfolding lcm_def by simp
  1.1588 -
  1.1589 -lemma lcm_1 [simp]: "lcm m 1 = m"
  1.1590 -  unfolding lcm_def by simp
  1.1591 -
  1.1592 -lemma lcm_0_left [simp]: "lcm 0 n = 0"
  1.1593 -  unfolding lcm_def by simp
  1.1594 -
  1.1595 -lemma lcm_1_left [simp]: "lcm 1 m = m"
  1.1596 -  unfolding lcm_def by simp
  1.1597 -
  1.1598 -lemma dvd_pos:
  1.1599 +lemma nat_dvd_pos:
  1.1600    fixes n m :: nat
  1.1601    assumes "n > 0" and "m dvd n"
  1.1602    shows "m > 0"
  1.1603  using assms by (cases m) auto
  1.1604  
  1.1605 -lemma lcm_least:
  1.1606 -  assumes "m dvd k" and "n dvd k"
  1.1607 +lemma nat_lcm_least:
  1.1608 +  assumes "(m::nat) dvd k" and "n dvd k"
  1.1609    shows "lcm m n dvd k"
  1.1610  proof (cases k)
  1.1611    case 0 then show ?thesis by auto
  1.1612  next
  1.1613    case (Suc _) then have pos_k: "k > 0" by auto
  1.1614 -  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1.1615 -  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  1.1616 +  from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1.1617 +  with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  1.1618    from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1.1619    from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1.1620    from pos_k k_m have pos_p: "p > 0" by auto
  1.1621    from pos_k k_n have pos_q: "q > 0" by auto
  1.1622    have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1.1623 -    by (simp add: mult_ac gcd_mult_distrib2)
  1.1624 +    by (simp add: mult_ac nat_gcd_mult_distrib)
  1.1625    also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1.1626      by (simp add: k_m [symmetric] k_n [symmetric])
  1.1627    also have "\<dots> = k * p * q * gcd m n"
  1.1628 -    by (simp add: mult_ac gcd_mult_distrib2)
  1.1629 +    by (simp add: mult_ac nat_gcd_mult_distrib)
  1.1630    finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1.1631      by (simp only: k_m [symmetric] k_n [symmetric])
  1.1632    then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1.1633      by (simp add: mult_ac)
  1.1634    with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1.1635      by simp
  1.1636 -  with prod_gcd_lcm [of m n]
  1.1637 +  with nat_prod_gcd_lcm [of m n]
  1.1638    have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1.1639      by (simp add: mult_ac)
  1.1640 -  with pos_gcd have "lcm m n * gcd q p = k" by simp
  1.1641 +  with pos_gcd have "lcm m n * gcd q p = k" by auto
  1.1642    then show ?thesis using dvd_def by auto
  1.1643  qed
  1.1644  
  1.1645 -lemma lcm_dvd1 [iff]:
  1.1646 -  "m dvd lcm m n"
  1.1647 +lemma int_lcm_least:
  1.1648 +  assumes "(m::int) dvd k" and "n dvd k"
  1.1649 +  shows "lcm m n dvd k"
  1.1650 +
  1.1651 +  apply (subst int_lcm_abs)
  1.1652 +  apply (rule dvd_trans)
  1.1653 +  apply (rule nat_lcm_least [transferred, of _ "abs k" _])
  1.1654 +  using prems apply auto
  1.1655 +done
  1.1656 +
  1.1657 +lemma nat_lcm_dvd1 [iff]: "(m::nat) dvd lcm m n"
  1.1658  proof (cases m)
  1.1659    case 0 then show ?thesis by simp
  1.1660  next
  1.1661 @@ -524,264 +1400,323 @@
  1.1662      then have npos: "n > 0" by simp
  1.1663      have "gcd m n dvd n" by simp
  1.1664      then obtain k where "n = gcd m n * k" using dvd_def by auto
  1.1665 -    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
  1.1666 -    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
  1.1667 -    finally show ?thesis by (simp add: lcm_def)
  1.1668 -  qed
  1.1669 -qed
  1.1670 -
  1.1671 -lemma lcm_dvd2 [iff]: 
  1.1672 -  "n dvd lcm m n"
  1.1673 -proof (cases n)
  1.1674 -  case 0 then show ?thesis by simp
  1.1675 -next
  1.1676 -  case (Suc _)
  1.1677 -  then have npos: "n > 0" by simp
  1.1678 -  show ?thesis
  1.1679 -  proof (cases m)
  1.1680 -    case 0 then show ?thesis by simp
  1.1681 -  next
  1.1682 -    case (Suc _)
  1.1683 -    then have mpos: "m > 0" by simp
  1.1684 -    have "gcd m n dvd m" by simp
  1.1685 -    then obtain k where "m = gcd m n * k" using dvd_def by auto
  1.1686 -    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
  1.1687 -    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
  1.1688 -    finally show ?thesis by (simp add: lcm_def)
  1.1689 +    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1.1690 +      by (simp add: mult_ac)
  1.1691 +    also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
  1.1692 +    finally show ?thesis by (simp add: lcm_nat_def)
  1.1693    qed
  1.1694  qed
  1.1695  
  1.1696 -lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
  1.1697 -  by (simp add: gcd_commute)
  1.1698 +lemma int_lcm_dvd1 [iff]: "(m::int) dvd lcm m n"
  1.1699 +  apply (subst int_lcm_abs)
  1.1700 +  apply (rule dvd_trans)
  1.1701 +  prefer 2
  1.1702 +  apply (rule nat_lcm_dvd1 [transferred])
  1.1703 +  apply auto
  1.1704 +done
  1.1705 +
  1.1706 +lemma nat_lcm_dvd2 [iff]: "(n::nat) dvd lcm m n"
  1.1707 +  by (subst nat_lcm_commute, rule nat_lcm_dvd1)
  1.1708 +
  1.1709 +lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
  1.1710 +  by (subst int_lcm_commute, rule int_lcm_dvd1)
  1.1711 +
  1.1712 +lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
  1.1713 +    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1.1714 +  by (auto intro: dvd_anti_sym nat_lcm_least)
  1.1715  
  1.1716 -lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
  1.1717 -  apply (subgoal_tac "n = m + (n - m)")
  1.1718 -  apply (erule ssubst, rule gcd_add1_eq, simp)  
  1.1719 -  done
  1.1720 +lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1.1721 +    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1.1722 +  by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
  1.1723 +
  1.1724 +lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1.1725 +  apply (rule sym)
  1.1726 +  apply (subst nat_lcm_unique [symmetric])
  1.1727 +  apply auto
  1.1728 +done
  1.1729 +
  1.1730 +lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
  1.1731 +  apply (rule sym)
  1.1732 +  apply (subst int_lcm_unique [symmetric])
  1.1733 +  apply auto
  1.1734 +done
  1.1735 +
  1.1736 +lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1.1737 +  by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
  1.1738 +
  1.1739 +lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
  1.1740 +  by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
  1.1741 +
  1.1742  
  1.1743  
  1.1744 -subsection {* GCD and LCM on integers *}
  1.1745 -
  1.1746 -definition
  1.1747 -  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
  1.1748 -  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
  1.1749 +subsection {* Primes *}
  1.1750  
  1.1751 -lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
  1.1752 -by (simp add: zgcd_def int_dvd_iff)
  1.1753 +(* Is there a better way to handle these, rather than making them
  1.1754 +   elim rules? *)
  1.1755  
  1.1756 -lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
  1.1757 -by (simp add: zgcd_def int_dvd_iff)
  1.1758 +lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1.1759 +  by (unfold prime_nat_def, auto)
  1.1760  
  1.1761 -lemma zgcd_pos: "zgcd i j \<ge> 0"
  1.1762 -by (simp add: zgcd_def)
  1.1763 +lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1.1764 +  by (unfold prime_nat_def, auto)
  1.1765  
  1.1766 -lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
  1.1767 -by (simp add: zgcd_def gcd_zero)
  1.1768 +lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1.1769 +  by (unfold prime_nat_def, auto)
  1.1770  
  1.1771 -lemma zgcd_commute: "zgcd i j = zgcd j i"
  1.1772 -unfolding zgcd_def by (simp add: gcd_commute)
  1.1773 +lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1.1774 +  by (unfold prime_nat_def, auto)
  1.1775  
  1.1776 -lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
  1.1777 -unfolding zgcd_def by simp
  1.1778 +lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1.1779 +  by (unfold prime_nat_def, auto)
  1.1780  
  1.1781 -lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
  1.1782 -unfolding zgcd_def by simp
  1.1783 +lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1.1784 +  by (unfold prime_nat_def, auto)
  1.1785 +
  1.1786 +lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1.1787 +  by (unfold prime_nat_def, auto)
  1.1788 +
  1.1789 +lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1.1790 +  by (unfold prime_int_def prime_nat_def, auto)
  1.1791  
  1.1792 -  (* should be solved by algebra*)
  1.1793 -lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
  1.1794 -  unfolding zgcd_def
  1.1795 -proof -
  1.1796 -  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
  1.1797 -  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
  1.1798 -  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
  1.1799 -  have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
  1.1800 -    unfolding dvd_def
  1.1801 -    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
  1.1802 -  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
  1.1803 -    unfolding dvd_def by blast
  1.1804 -  from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
  1.1805 -  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
  1.1806 -  then show ?thesis
  1.1807 -    apply (subst abs_dvd_iff [symmetric])
  1.1808 -    apply (subst dvd_abs_iff [symmetric])
  1.1809 -    apply (unfold dvd_def)
  1.1810 -    apply (rule_tac x = "int h'" in exI, simp)
  1.1811 -    done
  1.1812 -qed
  1.1813 +lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1.1814 +  by (unfold prime_int_def prime_nat_def, auto)
  1.1815 +
  1.1816 +lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1.1817 +  by (unfold prime_int_def prime_nat_def, auto)
  1.1818  
  1.1819 -lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
  1.1820 +lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1.1821 +  by (unfold prime_int_def prime_nat_def, auto)
  1.1822 +
  1.1823 +lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1.1824 +  by (unfold prime_int_def prime_nat_def, auto)
  1.1825  
  1.1826 -lemma zgcd_greatest:
  1.1827 -  assumes "k dvd m" and "k dvd n"
  1.1828 -  shows "k dvd zgcd m n"
  1.1829 -proof -
  1.1830 -  let ?k' = "nat \<bar>k\<bar>"
  1.1831 -  let ?m' = "nat \<bar>m\<bar>"
  1.1832 -  let ?n' = "nat \<bar>n\<bar>"
  1.1833 -  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
  1.1834 -    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
  1.1835 -  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
  1.1836 -    unfolding zgcd_def by (simp only: zdvd_int)
  1.1837 -  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
  1.1838 -  then show "k dvd zgcd m n" by simp
  1.1839 -qed
  1.1840 +thm prime_nat_def;
  1.1841 +thm prime_nat_def [transferred];
  1.1842 +
  1.1843 +lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1.1844 +    m = 1 \<or> m = p))"
  1.1845 +  using prime_nat_def [transferred]
  1.1846 +    apply (case_tac "p >= 0")
  1.1847 +    by (blast, auto simp add: int_prime_ge_0)
  1.1848 +
  1.1849 +(* To do: determine primality of any numeral *)
  1.1850 +
  1.1851 +lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
  1.1852 +  by (simp add: prime_nat_def)
  1.1853 +
  1.1854 +lemma int_zero_not_prime [simp]: "~prime (0::int)"
  1.1855 +  by (simp add: prime_int_def)
  1.1856 +
  1.1857 +lemma nat_one_not_prime [simp]: "~prime (1::nat)"
  1.1858 +  by (simp add: prime_nat_def)
  1.1859  
  1.1860 -lemma div_zgcd_relprime:
  1.1861 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  1.1862 -  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
  1.1863 -proof -
  1.1864 -  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
  1.1865 -  let ?g = "zgcd a b"
  1.1866 -  let ?a' = "a div ?g"
  1.1867 -  let ?b' = "b div ?g"
  1.1868 -  let ?g' = "zgcd ?a' ?b'"
  1.1869 -  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
  1.1870 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
  1.1871 -  from dvdg dvdg' obtain ka kb ka' kb' where
  1.1872 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
  1.1873 -    unfolding dvd_def by blast
  1.1874 -  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
  1.1875 -  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  1.1876 -    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
  1.1877 -      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  1.1878 -  have "?g \<noteq> 0" using nz by simp
  1.1879 -  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
  1.1880 -  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  1.1881 -  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
  1.1882 -  with zgcd_pos show "?g' = 1" by simp
  1.1883 -qed
  1.1884 +lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
  1.1885 +  by (simp add: prime_nat_def One_nat_def)
  1.1886 +
  1.1887 +lemma int_one_not_prime [simp]: "~prime (1::int)"
  1.1888 +  by (simp add: prime_int_def)
  1.1889 +
  1.1890 +lemma nat_two_is_prime [simp]: "prime (2::nat)"
  1.1891 +  apply (auto simp add: prime_nat_def)
  1.1892 +  apply (case_tac m)
  1.1893 +  apply (auto dest!: dvd_imp_le)
  1.1894 +  done
  1.1895  
  1.1896 -lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
  1.1897 -  by (simp add: zgcd_def abs_if)
  1.1898 -
  1.1899 -lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
  1.1900 -  by (simp add: zgcd_def abs_if)
  1.1901 +lemma int_two_is_prime [simp]: "prime (2::int)"
  1.1902 +  by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
  1.1903  
  1.1904 -lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
  1.1905 -  apply (frule_tac b = n and a = m in pos_mod_sign)
  1.1906 -  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
  1.1907 -  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
  1.1908 -  apply (frule_tac a = m in pos_mod_bound)
  1.1909 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
  1.1910 +lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1911 +  apply (unfold prime_nat_def)
  1.1912 +  apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
  1.1913 +  done
  1.1914 +
  1.1915 +lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1916 +  apply (unfold prime_int_altdef)
  1.1917 +  apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
  1.1918    done
  1.1919  
  1.1920 -lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
  1.1921 -  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
  1.1922 -  apply (auto simp add: linorder_neq_iff zgcd_non_0)
  1.1923 -  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
  1.1924 -  done
  1.1925 +lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1926 +  by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
  1.1927 +
  1.1928 +lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1929 +  by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
  1.1930 +
  1.1931 +lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
  1.1932 +    p dvd m * n = (p dvd m \<or> p dvd n)"
  1.1933 +  by (rule iffI, rule nat_prime_dvd_mult, auto)
  1.1934  
  1.1935 -lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
  1.1936 -  by (simp add: zgcd_def abs_if)
  1.1937 +lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
  1.1938 +    p dvd m * n = (p dvd m \<or> p dvd n)"
  1.1939 +  by (rule iffI, rule int_prime_dvd_mult, auto)
  1.1940  
  1.1941 -lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
  1.1942 -  by (simp add: zgcd_def abs_if)
  1.1943 -
  1.1944 -lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
  1.1945 -  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
  1.1946 +lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1947 +    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1.1948 +  unfolding prime_nat_def dvd_def apply auto
  1.1949 +  apply (subgoal_tac "k > 1")
  1.1950 +  apply force
  1.1951 +  apply (subgoal_tac "k ~= 0")
  1.1952 +  apply force
  1.1953 +  apply (rule notI)
  1.1954 +  apply force
  1.1955 +done
  1.1956  
  1.1957 -lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
  1.1958 -  by (simp add: zgcd_def gcd_1_left)
  1.1959 -
  1.1960 -lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
  1.1961 -  by (simp add: zgcd_def gcd_assoc)
  1.1962 +(* there's a lot of messing around with signs of products here --
  1.1963 +   could this be made more automatic? *)
  1.1964 +lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1965 +    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1.1966 +  unfolding prime_int_altdef dvd_def
  1.1967 +  apply auto
  1.1968 +  apply (rule_tac x = m in exI)
  1.1969 +  apply (rule_tac x = k in exI)
  1.1970 +  apply (auto simp add: mult_compare_simps)
  1.1971 +  apply (subgoal_tac "k > 0")
  1.1972 +  apply arith
  1.1973 +  apply (case_tac "k <= 0")
  1.1974 +  apply (subgoal_tac "m * k <= 0")
  1.1975 +  apply force
  1.1976 +  apply (subst zero_compare_simps(8))
  1.1977 +  apply auto
  1.1978 +  apply (subgoal_tac "m * k <= 0")
  1.1979 +  apply force
  1.1980 +  apply (subst zero_compare_simps(8))
  1.1981 +  apply auto
  1.1982 +done
  1.1983  
  1.1984 -lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
  1.1985 -  apply (rule zgcd_commute [THEN trans])
  1.1986 -  apply (rule zgcd_assoc [THEN trans])
  1.1987 -  apply (rule zgcd_commute [THEN arg_cong])
  1.1988 -  done
  1.1989 +lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
  1.1990 +    n > 0 --> (p dvd x^n --> p dvd x)"
  1.1991 +  by (induct n rule: nat_induct, auto)
  1.1992  
  1.1993 -lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
  1.1994 -  -- {* addition is an AC-operator *}
  1.1995 +lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
  1.1996 +    n > 0 --> (p dvd x^n --> p dvd x)"
  1.1997 +  apply (induct n rule: nat_induct, auto)
  1.1998 +  apply (frule int_prime_ge_0)
  1.1999 +  apply auto
  1.2000 +done
  1.2001 +
  1.2002 +lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.2003 +    coprime a (p^m)"
  1.2004 +  apply (rule nat_coprime_exp)
  1.2005 +  apply (subst nat_gcd_commute)
  1.2006 +  apply (erule (1) nat_prime_imp_coprime)
  1.2007 +done
  1.2008  
  1.2009 -lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
  1.2010 -  by (simp del: minus_mult_right [symmetric]
  1.2011 -      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
  1.2012 -          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
  1.2013 +lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.2014 +    coprime a (p^m)"
  1.2015 +  apply (rule int_coprime_exp)
  1.2016 +  apply (subst int_gcd_commute)
  1.2017 +  apply (erule (1) int_prime_imp_coprime)
  1.2018 +done
  1.2019  
  1.2020 -lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
  1.2021 -  by (simp add: abs_if zgcd_zmult_distrib2)
  1.2022 +lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.2023 +  apply (rule nat_prime_imp_coprime, assumption)
  1.2024 +  apply (unfold prime_nat_def, auto)
  1.2025 +done
  1.2026  
  1.2027 -lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
  1.2028 -  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
  1.2029 +lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.2030 +  apply (rule int_prime_imp_coprime, assumption)
  1.2031 +  apply (unfold prime_int_altdef, clarify)
  1.2032 +  apply (drule_tac x = q in spec)
  1.2033 +  apply (drule_tac x = p in spec)
  1.2034 +  apply auto
  1.2035 +done
  1.2036  
  1.2037 -lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
  1.2038 -  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
  1.2039 +lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.2040 +    coprime (p^m) (q^n)"
  1.2041 +  by (rule nat_coprime_exp2, rule nat_primes_coprime)
  1.2042  
  1.2043 -lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
  1.2044 -  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
  1.2045 +lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.2046 +    coprime (p^m) (q^n)"
  1.2047 +  by (rule int_coprime_exp2, rule int_primes_coprime)
  1.2048  
  1.2049 -
  1.2050 -definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
  1.2051 +lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1.2052 +  apply (induct n rule: nat_less_induct)
  1.2053 +  apply (case_tac "n = 0")
  1.2054 +  using nat_two_is_prime apply blast
  1.2055 +  apply (case_tac "prime n")
  1.2056 +  apply blast
  1.2057 +  apply (subgoal_tac "n > 1")
  1.2058 +  apply (frule (1) nat_not_prime_eq_prod)
  1.2059 +  apply (auto intro: dvd_mult dvd_mult2)
  1.2060 +done
  1.2061  
  1.2062 -lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
  1.2063 -by(simp add:zlcm_def dvd_int_iff)
  1.2064 +(* An Isar version:
  1.2065 +
  1.2066 +lemma nat_prime_factor_b:
  1.2067 +  fixes n :: nat
  1.2068 +  assumes "n \<noteq> 1"
  1.2069 +  shows "\<exists>p. prime p \<and> p dvd n"
  1.2070  
  1.2071 -lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
  1.2072 -by(simp add:zlcm_def dvd_int_iff)
  1.2073 -
  1.2074 -
  1.2075 -lemma dvd_imp_dvd_zlcm1:
  1.2076 -  assumes "k dvd i" shows "k dvd (zlcm i j)"
  1.2077 -proof -
  1.2078 -  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
  1.2079 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  1.2080 -  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  1.2081 +using `n ~= 1`
  1.2082 +proof (induct n rule: nat_less_induct)
  1.2083 +  fix n :: nat
  1.2084 +  assume "n ~= 1" and
  1.2085 +    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1.2086 +  thus "\<exists>p. prime p \<and> p dvd n"
  1.2087 +  proof -
  1.2088 +  {
  1.2089 +    assume "n = 0"
  1.2090 +    moreover note nat_two_is_prime
  1.2091 +    ultimately have ?thesis
  1.2092 +      by (auto simp del: nat_two_is_prime)
  1.2093 +  }
  1.2094 +  moreover
  1.2095 +  {
  1.2096 +    assume "prime n"
  1.2097 +    hence ?thesis by auto
  1.2098 +  }
  1.2099 +  moreover
  1.2100 +  {
  1.2101 +    assume "n ~= 0" and "~ prime n"
  1.2102 +    with `n ~= 1` have "n > 1" by auto
  1.2103 +    with `~ prime n` and nat_not_prime_eq_prod obtain m k where
  1.2104 +      "n = m * k" and "1 < m" and "m < n" by blast
  1.2105 +    with ih obtain p where "prime p" and "p dvd m" by blast
  1.2106 +    with `n = m * k` have ?thesis by auto
  1.2107 +  }
  1.2108 +  ultimately show ?thesis by blast
  1.2109 +  qed
  1.2110  qed
  1.2111  
  1.2112 -lemma dvd_imp_dvd_zlcm2:
  1.2113 -  assumes "k dvd j" shows "k dvd (zlcm i j)"
  1.2114 -proof -
  1.2115 -  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
  1.2116 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  1.2117 -  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  1.2118 +*)
  1.2119 +
  1.2120 +text {* One property of coprimality is easier to prove via prime factors. *}
  1.2121 +
  1.2122 +lemma nat_prime_divprod_pow:
  1.2123 +  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1.2124 +  shows "p^n dvd a \<or> p^n dvd b"
  1.2125 +proof-
  1.2126 +  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1.2127 +      apply (cases "n=0", simp_all)
  1.2128 +      apply (cases "a=1", simp_all) done}
  1.2129 +  moreover
  1.2130 +  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1.2131 +    then obtain m where m: "n = Suc m" by (cases n, auto)
  1.2132 +    from n have "p dvd p^n" by (intro dvd_power, auto)
  1.2133 +    also note pab
  1.2134 +    finally have pab': "p dvd a * b".
  1.2135 +    from nat_prime_dvd_mult[OF p pab']
  1.2136 +    have "p dvd a \<or> p dvd b" .
  1.2137 +    moreover
  1.2138 +    {assume pa: "p dvd a"
  1.2139 +      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1.2140 +      from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1.2141 +      with p have "coprime b p"
  1.2142 +        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1.2143 +      hence pnb: "coprime (p^n) b"
  1.2144 +        by (subst nat_gcd_commute, rule nat_coprime_exp)
  1.2145 +      from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
  1.2146 +    moreover
  1.2147 +    {assume pb: "p dvd b"
  1.2148 +      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1.2149 +      from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
  1.2150 +        by auto
  1.2151 +      with p have "coprime a p"
  1.2152 +        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1.2153 +      hence pna: "coprime (p^n) a"
  1.2154 +        by (subst nat_gcd_commute, rule nat_coprime_exp)
  1.2155 +      from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
  1.2156 +    ultimately have ?thesis by blast}
  1.2157 +  ultimately show ?thesis by blast
  1.2158  qed
  1.2159  
  1.2160 -
  1.2161 -lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
  1.2162 -by (case_tac "d <0", simp_all)
  1.2163 -
  1.2164 -lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
  1.2165 -by (case_tac "d<0", simp_all)
  1.2166 -
  1.2167 -(* lcm a b is positive for positive a and b *)
  1.2168 -
  1.2169 -lemma lcm_pos: 
  1.2170 -  assumes mpos: "m > 0"
  1.2171 -  and npos: "n>0"
  1.2172 -  shows "lcm m n > 0"
  1.2173 -proof(rule ccontr, simp add: lcm_def gcd_zero)
  1.2174 -assume h:"m*n div gcd m n = 0"
  1.2175 -from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
  1.2176 -hence gcdp: "gcd m n > 0" by simp
  1.2177 -with h
  1.2178 -have "m*n < gcd m n"
  1.2179 -  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
  1.2180 -moreover 
  1.2181 -have "gcd m n dvd m" by simp
  1.2182 - with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
  1.2183 - with npos have t1:"gcd m n *n \<le> m*n" by simp
  1.2184 - have "gcd m n \<le> gcd m n*n" using npos by simp
  1.2185 - with t1 have "gcd m n \<le> m*n" by arith
  1.2186 -ultimately show "False" by simp
  1.2187 -qed
  1.2188 -
  1.2189 -lemma zlcm_pos: 
  1.2190 -  assumes anz: "a \<noteq> 0"
  1.2191 -  and bnz: "b \<noteq> 0" 
  1.2192 -  shows "0 < zlcm a b"
  1.2193 -proof-
  1.2194 -  let ?na = "nat (abs a)"
  1.2195 -  let ?nb = "nat (abs b)"
  1.2196 -  have nap: "?na >0" using anz by simp
  1.2197 -  have nbp: "?nb >0" using bnz by simp
  1.2198 -  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
  1.2199 -  thus ?thesis by (simp add: zlcm_def)
  1.2200 -qed
  1.2201 -
  1.2202 -lemma zgcd_code [code]:
  1.2203 -  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1.2204 -  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
  1.2205 -
  1.2206  end