# HG changeset patch
# User chaieb
# Date 1216640230 -7200
# Node ID 3b5425dead982f0a2a7ad3a266b8e5ed07eb58df
# Parent  4b1642284dd74b35d55e7af9e311efd527aeb590
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy

diff -r 4b1642284dd7 -r 3b5425dead98 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Mon Jul 21 13:37:05 2008 +0200
+++ b/src/HOL/Library/Primes.thy	Mon Jul 21 13:37:10 2008 +0200
@@ -117,7 +117,6 @@
 lemma divides_mul_r: "(a::nat) dvd b ==> (a * c) dvd (b * c)" by presburger
 lemma divides_cases: "(n::nat) dvd m ==> m = 0 \<or> m = n \<or> 2 * n <= m" 
   by (auto simp add: dvd_def)
-lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
 
 lemma divides_div_not: "(x::nat) = (q * n) + r \<Longrightarrow> 0 < r \<Longrightarrow> r < n ==> ~(n dvd x)"
 proof(auto simp add: dvd_def)
@@ -178,236 +177,6 @@
 lemma divides_rexp: 
   "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
 
-text {* The Bezout theorem is a bit ugly for N; it'd be easier for Z *}
-lemma ind_euclid: 
-  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
-  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
-  shows "P a b"
-proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
-  fix n a b
-  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
-  have "a = b \<or> a < b \<or> b < a" by arith
-  moreover {assume eq: "a= b"
-    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
-  moreover
-  {assume lt: "a < b"
-    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
-    moreover
-    {assume "a =0" with z c have "P a b" by blast }
-    moreover
-    {assume ab: "a + b - a < n"
-      have th0: "a + b - a = a + (b - a)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P a b" by (simp add: th0[symmetric])}
-    ultimately have "P a b" by blast}
-  moreover
-  {assume lt: "a > b"
-    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
-    moreover
-    {assume "b =0" with z c have "P a b" by blast }
-    moreover
-    {assume ab: "b + a - b < n"
-      have th0: "b + a - b = b + (a - b)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P b a" by (simp add: th0[symmetric])
-      hence "P a b" using c by blast }
-    ultimately have "P a b" by blast}
-ultimately  show "P a b" by blast
-qed
-
-lemma bezout_lemma: 
-  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)"
-  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)"
-using ex
-apply clarsimp
-apply (rule_tac x="d" in exI, simp add: dvd_add)
-apply (case_tac "a * x = b * y + d" , simp_all)
-apply (rule_tac x="x + y" in exI)
-apply (rule_tac x="y" in exI)
-apply algebra
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="x + y" in exI)
-apply algebra
-done
-
-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)"
-apply(induct a b rule: ind_euclid)
-apply blast
-apply clarify
-apply (rule_tac x="a" in exI, simp add: dvd_add)
-apply clarsimp
-apply (rule_tac x="d" in exI)
-apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
-apply (rule_tac x="x+y" in exI)
-apply (rule_tac x="y" in exI)
-apply algebra
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="x+y" in exI)
-apply algebra
-done
-
-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)"
-using bezout_add[of a b]
-apply clarsimp
-apply (rule_tac x="d" in exI, simp)
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="y" in exI)
-apply auto
-done
-
-text {* We can get a stronger version with a nonzeroness assumption. *}
-
-lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
-  shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
-proof-
-  from nz have ap: "a > 0" by simp
- from bezout_add[of a b] 
- 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
- moreover
- {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
-   from H have ?thesis by blast }
- moreover
- {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
-   {assume b0: "b = 0" with H  have ?thesis by simp}
-   moreover 
-   {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
-     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
-     moreover
-     {assume db: "d=b"
-       from prems have ?thesis apply simp
-	 apply (rule exI[where x = b], simp)
-	 apply (rule exI[where x = b])
-	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
-    moreover
-    {assume db: "d < b" 
-	{assume "x=0" hence ?thesis  using prems by simp }
-	moreover
-	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
-	  
-	  from db have "d \<le> b - 1" by simp
-	  hence "d*b \<le> b*(b - 1)" by simp
-	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
-	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
-	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" by simp
-	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
-	    by (simp only: mult_assoc right_distrib)
-	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
-	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
-	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
-	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
-	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
-	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
-	  hence ?thesis using H(1,2)
-	    apply -
-	    apply (rule exI[where x=d], simp)
-	    apply (rule exI[where x="(b - 1) * y"])
-	    by (rule exI[where x="x*(b - 1) - d"], simp)}
-	ultimately have ?thesis by blast}
-    ultimately have ?thesis by blast}
-  ultimately have ?thesis by blast}
- ultimately show ?thesis by blast
-qed
-
-text {* Greatest common divisor. *}
-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"
-proof(auto)
-  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
-  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
-  have th: "gcd a b dvd d" by blast
-  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
-qed
-
-lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
-  shows "gcd x y = gcd u v"
-proof-
-  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
-  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
-qed
-
-lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
-proof-
-  let ?g = "gcd a b"
-  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
-  from d(1,2) have "d dvd ?g" by simp
-  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
-  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
-  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k"
-    by (simp only: diff_mult_distrib)
-  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g"
-    by (simp add: k mult_assoc)
-  thus ?thesis by blast
-qed
-
-lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
-  shows "\<exists>x y. a * x = b * y + gcd a b"
-proof-
-  let ?g = "gcd a b"
-  from bezout_add_strong[OF a, of b]
-  obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
-  from d(1,2) have "d dvd ?g" by simp
-  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
-  from d(3) have "a * x * k = (b * y + d) *k " by auto 
-  hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
-  thus ?thesis by blast
-qed
-
-lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
-by(simp add: gcd_mult_distrib2 mult_commute)
-
-lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  let ?g = "gcd a b"
-  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
-    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
-      by blast
-    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
-    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
-      by (simp only: diff_mult_distrib)
-    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d" 
-      by (simp add: k[symmetric] mult_assoc)
-    hence ?lhs by blast}
-  moreover
-  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
-    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y" 
-      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
-    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
-    have ?rhs by auto}
-  ultimately show ?thesis by blast
-qed
-
-lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
-proof-
-  let ?g = "gcd a b"
-    have dv: "?g dvd a*x" "?g dvd b * y" 
-      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
-    from dvd_add[OF dv] H
-    show ?thesis by auto
-qed
-
-lemma gcd_mult': "gcd b (a * b) = b"
-by (simp add: gcd_mult mult_commute[of a b]) 
-
-lemma gcd_add: "gcd(a + b) b = gcd a b" 
-  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
-apply (simp_all add: gcd_add1)
-by (simp add: gcd_commute gcd_add1)
-
-lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
-proof-
-  {fix a b assume H: "b \<le> (a::nat)"
-    hence th: "a - b + b = a" by arith
-    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
-  note th = this
-{
-  assume ab: "b \<le> a"
-  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
-next
-  assume ab: "a \<le> b"
-  from th[OF ab] show "gcd a (b - a) = gcd a b" 
-    by (simp add: gcd_commute)}
-qed
-
 text {* Coprimality *}
 
 lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"