author chaieb Mon Jul 21 13:37:10 2008 +0200 (2008-07-21) changeset 27670 3b5425dead98 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
```     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.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.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.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.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.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.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)"
```