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
authorchaieb
Mon Jul 21 13:37:10 2008 +0200 (2008-07-21)
changeset 276703b5425dead98
parent 27669 4b1642284dd7
child 27671 f938cd3fa820
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
src/HOL/Library/Primes.thy
     1.1 --- a/src/HOL/Library/Primes.thy	Mon Jul 21 13:37:05 2008 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Mon Jul 21 13:37:10 2008 +0200
     1.3 @@ -117,7 +117,6 @@
     1.4  lemma divides_mul_r: "(a::nat) dvd b ==> (a * c) dvd (b * c)" by presburger
     1.5  lemma divides_cases: "(n::nat) dvd m ==> m = 0 \<or> m = n \<or> 2 * n <= m" 
     1.6    by (auto simp add: dvd_def)
     1.7 -lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
     1.8  
     1.9  lemma divides_div_not: "(x::nat) = (q * n) + r \<Longrightarrow> 0 < r \<Longrightarrow> r < n ==> ~(n dvd x)"
    1.10  proof(auto simp add: dvd_def)
    1.11 @@ -178,236 +177,6 @@
    1.12  lemma divides_rexp: 
    1.13    "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
    1.14  
    1.15 -text {* The Bezout theorem is a bit ugly for N; it'd be easier for Z *}
    1.16 -lemma ind_euclid: 
    1.17 -  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
    1.18 -  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
    1.19 -  shows "P a b"
    1.20 -proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
    1.21 -  fix n a b
    1.22 -  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
    1.23 -  have "a = b \<or> a < b \<or> b < a" by arith
    1.24 -  moreover {assume eq: "a= b"
    1.25 -    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
    1.26 -  moreover
    1.27 -  {assume lt: "a < b"
    1.28 -    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
    1.29 -    moreover
    1.30 -    {assume "a =0" with z c have "P a b" by blast }
    1.31 -    moreover
    1.32 -    {assume ab: "a + b - a < n"
    1.33 -      have th0: "a + b - a = a + (b - a)" using lt by arith
    1.34 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
    1.35 -      have "P a b" by (simp add: th0[symmetric])}
    1.36 -    ultimately have "P a b" by blast}
    1.37 -  moreover
    1.38 -  {assume lt: "a > b"
    1.39 -    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
    1.40 -    moreover
    1.41 -    {assume "b =0" with z c have "P a b" by blast }
    1.42 -    moreover
    1.43 -    {assume ab: "b + a - b < n"
    1.44 -      have th0: "b + a - b = b + (a - b)" using lt by arith
    1.45 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
    1.46 -      have "P b a" by (simp add: th0[symmetric])
    1.47 -      hence "P a b" using c by blast }
    1.48 -    ultimately have "P a b" by blast}
    1.49 -ultimately  show "P a b" by blast
    1.50 -qed
    1.51 -
    1.52 -lemma bezout_lemma: 
    1.53 -  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.54 -  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.55 -using ex
    1.56 -apply clarsimp
    1.57 -apply (rule_tac x="d" in exI, simp add: dvd_add)
    1.58 -apply (case_tac "a * x = b * y + d" , simp_all)
    1.59 -apply (rule_tac x="x + y" in exI)
    1.60 -apply (rule_tac x="y" in exI)
    1.61 -apply algebra
    1.62 -apply (rule_tac x="x" in exI)
    1.63 -apply (rule_tac x="x + y" in exI)
    1.64 -apply algebra
    1.65 -done
    1.66 -
    1.67 -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.68 -apply(induct a b rule: ind_euclid)
    1.69 -apply blast
    1.70 -apply clarify
    1.71 -apply (rule_tac x="a" in exI, simp add: dvd_add)
    1.72 -apply clarsimp
    1.73 -apply (rule_tac x="d" in exI)
    1.74 -apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
    1.75 -apply (rule_tac x="x+y" in exI)
    1.76 -apply (rule_tac x="y" in exI)
    1.77 -apply algebra
    1.78 -apply (rule_tac x="x" in exI)
    1.79 -apply (rule_tac x="x+y" in exI)
    1.80 -apply algebra
    1.81 -done
    1.82 -
    1.83 -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.84 -using bezout_add[of a b]
    1.85 -apply clarsimp
    1.86 -apply (rule_tac x="d" in exI, simp)
    1.87 -apply (rule_tac x="x" in exI)
    1.88 -apply (rule_tac x="y" in exI)
    1.89 -apply auto
    1.90 -done
    1.91 -
    1.92 -text {* We can get a stronger version with a nonzeroness assumption. *}
    1.93 -
    1.94 -lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
    1.95 -  shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
    1.96 -proof-
    1.97 -  from nz have ap: "a > 0" by simp
    1.98 - from bezout_add[of a b] 
    1.99 - 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.100 - moreover
   1.101 - {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
   1.102 -   from H have ?thesis by blast }
   1.103 - moreover
   1.104 - {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
   1.105 -   {assume b0: "b = 0" with H  have ?thesis by simp}
   1.106 -   moreover 
   1.107 -   {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
   1.108 -     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
   1.109 -     moreover
   1.110 -     {assume db: "d=b"
   1.111 -       from prems have ?thesis apply simp
   1.112 -	 apply (rule exI[where x = b], simp)
   1.113 -	 apply (rule exI[where x = b])
   1.114 -	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
   1.115 -    moreover
   1.116 -    {assume db: "d < b" 
   1.117 -	{assume "x=0" hence ?thesis  using prems by simp }
   1.118 -	moreover
   1.119 -	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
   1.120 -	  
   1.121 -	  from db have "d \<le> b - 1" by simp
   1.122 -	  hence "d*b \<le> b*(b - 1)" by simp
   1.123 -	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
   1.124 -	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
   1.125 -	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" by simp
   1.126 -	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
   1.127 -	    by (simp only: mult_assoc right_distrib)
   1.128 -	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
   1.129 -	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
   1.130 -	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
   1.131 -	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
   1.132 -	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
   1.133 -	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
   1.134 -	  hence ?thesis using H(1,2)
   1.135 -	    apply -
   1.136 -	    apply (rule exI[where x=d], simp)
   1.137 -	    apply (rule exI[where x="(b - 1) * y"])
   1.138 -	    by (rule exI[where x="x*(b - 1) - d"], simp)}
   1.139 -	ultimately have ?thesis by blast}
   1.140 -    ultimately have ?thesis by blast}
   1.141 -  ultimately have ?thesis by blast}
   1.142 - ultimately show ?thesis by blast
   1.143 -qed
   1.144 -
   1.145 -text {* Greatest common divisor. *}
   1.146 -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.147 -proof(auto)
   1.148 -  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   1.149 -  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   1.150 -  have th: "gcd a b dvd d" by blast
   1.151 -  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   1.152 -qed
   1.153 -
   1.154 -lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
   1.155 -  shows "gcd x y = gcd u v"
   1.156 -proof-
   1.157 -  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
   1.158 -  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
   1.159 -qed
   1.160 -
   1.161 -lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   1.162 -proof-
   1.163 -  let ?g = "gcd a b"
   1.164 -  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.165 -  from d(1,2) have "d dvd ?g" by simp
   1.166 -  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   1.167 -  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
   1.168 -  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k"
   1.169 -    by (simp only: diff_mult_distrib)
   1.170 -  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g"
   1.171 -    by (simp add: k mult_assoc)
   1.172 -  thus ?thesis by blast
   1.173 -qed
   1.174 -
   1.175 -lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
   1.176 -  shows "\<exists>x y. a * x = b * y + gcd a b"
   1.177 -proof-
   1.178 -  let ?g = "gcd a b"
   1.179 -  from bezout_add_strong[OF a, of b]
   1.180 -  obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
   1.181 -  from d(1,2) have "d dvd ?g" by simp
   1.182 -  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   1.183 -  from d(3) have "a * x * k = (b * y + d) *k " by auto 
   1.184 -  hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
   1.185 -  thus ?thesis by blast
   1.186 -qed
   1.187 -
   1.188 -lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
   1.189 -by(simp add: gcd_mult_distrib2 mult_commute)
   1.190 -
   1.191 -lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
   1.192 -  (is "?lhs \<longleftrightarrow> ?rhs")
   1.193 -proof-
   1.194 -  let ?g = "gcd a b"
   1.195 -  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
   1.196 -    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
   1.197 -      by blast
   1.198 -    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
   1.199 -    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
   1.200 -      by (simp only: diff_mult_distrib)
   1.201 -    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d" 
   1.202 -      by (simp add: k[symmetric] mult_assoc)
   1.203 -    hence ?lhs by blast}
   1.204 -  moreover
   1.205 -  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
   1.206 -    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y" 
   1.207 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
   1.208 -    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
   1.209 -    have ?rhs by auto}
   1.210 -  ultimately show ?thesis by blast
   1.211 -qed
   1.212 -
   1.213 -lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
   1.214 -proof-
   1.215 -  let ?g = "gcd a b"
   1.216 -    have dv: "?g dvd a*x" "?g dvd b * y" 
   1.217 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
   1.218 -    from dvd_add[OF dv] H
   1.219 -    show ?thesis by auto
   1.220 -qed
   1.221 -
   1.222 -lemma gcd_mult': "gcd b (a * b) = b"
   1.223 -by (simp add: gcd_mult mult_commute[of a b]) 
   1.224 -
   1.225 -lemma gcd_add: "gcd(a + b) b = gcd a b" 
   1.226 -  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
   1.227 -apply (simp_all add: gcd_add1)
   1.228 -by (simp add: gcd_commute gcd_add1)
   1.229 -
   1.230 -lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
   1.231 -proof-
   1.232 -  {fix a b assume H: "b \<le> (a::nat)"
   1.233 -    hence th: "a - b + b = a" by arith
   1.234 -    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
   1.235 -  note th = this
   1.236 -{
   1.237 -  assume ab: "b \<le> a"
   1.238 -  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
   1.239 -next
   1.240 -  assume ab: "a \<le> b"
   1.241 -  from th[OF ab] show "gcd a (b - a) = gcd a b" 
   1.242 -    by (simp add: gcd_commute)}
   1.243 -qed
   1.244 -
   1.245  text {* Coprimality *}
   1.246  
   1.247  lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"