# HG changeset patch
# User chaieb
# Date 1216640225 -7200
# Node ID 4b1642284dd74b35d55e7af9e311efd527aeb590
# Parent  6eb20b2cecf8448484d333f63cf6a92b206361ce
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy

diff -r 6eb20b2cecf8 -r 4b1642284dd7 src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Mon Jul 21 13:36:59 2008 +0200
+++ b/src/HOL/Library/GCD.thy	Mon Jul 21 13:37:05 2008 +0200
@@ -52,16 +52,16 @@
   case (1 m n) with assms show ?case by (cases "n = 0") simp_all
 qed
 
-lemma gcd_0 [simp]: "gcd m 0 = m"
+lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
   by simp
 
-lemma gcd_0_left [simp]: "gcd 0 m = m"
+lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
   by simp
 
 lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
   by simp
 
-lemma gcd_1 [simp]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
   by simp
 
 declare gcd.simps [simp del]
@@ -71,8 +71,8 @@
   conjunctions don't seem provable separately.
 *}
 
-lemma gcd_dvd1 [iff]: "gcd m n dvd m"
-  and gcd_dvd2 [iff]: "gcd m n dvd n"
+lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
+  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
   apply (induct m n rule: gcd_induct)
      apply (simp_all add: gcd_non_0)
   apply (blast dest: dvd_mod_imp_dvd)
@@ -97,10 +97,10 @@
 
 subsection {* Derived laws for GCD *}
 
-lemma gcd_greatest_iff [iff]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
+lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   by (blast intro!: gcd_greatest intro: dvd_trans)
 
-lemma gcd_zero: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
+lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
 
 lemma gcd_commute: "gcd m n = gcd n m"
@@ -117,7 +117,7 @@
   apply (blast intro: dvd_trans)
   done
 
-lemma gcd_1_left [simp]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
   by (simp add: gcd_commute)
 
 text {*
@@ -132,11 +132,11 @@
    apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   done
 
-lemma gcd_mult [simp]: "gcd k (k * n) = k"
+lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
   apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   done
 
-lemma gcd_self [simp]: "gcd k k = k"
+lemma gcd_self [simp, algebra]: "gcd k k = k"
   apply (rule gcd_mult [of k 1, simplified])
   done
 
@@ -163,13 +163,13 @@
 
 text {* \medskip Addition laws *}
 
-lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
+lemma gcd_add1 [simp,algebra]: "gcd (m + n) n = gcd m n"
   apply (case_tac "n = 0")
    apply (simp_all add: gcd_non_0)
   apply (simp add: mod_add_self2)
   done
 
-lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
+lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
 proof -
   have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
   also have "... = gcd (n + m) m" by (simp add: add_commute)
@@ -178,15 +178,15 @@
   finally show ?thesis .
 qed
 
-lemma gcd_add2' [simp]: "gcd m (n + m) = gcd m n"
+lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
   apply (subst add_commute)
   apply (rule gcd_add2)
   done
 
-lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
+lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
   by (induct k) (simp_all add: add_assoc)
 
-lemma gcd_dvd_prod: "gcd m n dvd m * n"
+lemma gcd_dvd_prod: "gcd m n dvd m * n" 
   using mult_dvd_mono [of 1] by auto
 
 text {*
@@ -216,8 +216,239 @@
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
 qed
 
+
+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 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 divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
+
+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 "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
+
+
+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 (algebra add: 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 algebra
+  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
+
+
 subsection {* LCM defined by GCD *}
 
+
 definition
   lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
@@ -324,7 +555,7 @@
 
 lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
   apply (subgoal_tac "n = m + (n - m)")
-   apply (erule ssubst, rule gcd_add1_eq, simp)
+  apply (erule ssubst, rule gcd_add1_eq, simp)  
   done
 
 
@@ -334,27 +565,28 @@
   zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
 
-lemma zgcd_zdvd1 [iff,simp]: "zgcd i j dvd i"
+lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
   by (simp add: zgcd_def int_dvd_iff)
 
-lemma zgcd_zdvd2 [iff,simp]: "zgcd i j dvd j"
+lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
   by (simp add: zgcd_def int_dvd_iff)
 
 lemma zgcd_pos: "zgcd i j \<ge> 0"
   by (simp add: zgcd_def)
 
-lemma zgcd0 [simp]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
+lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
   by (simp add: zgcd_def gcd_zero) arith
 
 lemma zgcd_commute: "zgcd i j = zgcd j i"
   unfolding zgcd_def by (simp add: gcd_commute)
 
-lemma zgcd_zminus [simp]: "zgcd (- i) j = zgcd i j"
+lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
   unfolding zgcd_def by simp
 
-lemma zgcd_zminus2 [simp]: "zgcd i (- j) = zgcd i j"
+lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
   unfolding zgcd_def by simp
 
+  (* should be solved by algebra*)
 lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   unfolding zgcd_def
 proof -
@@ -418,12 +650,10 @@
   with zgcd_pos show "?g' = 1" by simp
 qed
 
-    (* IntPrimes stuff *)
-
-lemma zgcd_0 [simp]: "zgcd m 0 = abs m"
+lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
   by (simp add: zgcd_def abs_if)
 
-lemma zgcd_0_left [simp]: "zgcd 0 m = abs m"
+lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
   by (simp add: zgcd_def abs_if)
 
 lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
@@ -440,16 +670,16 @@
   apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
   done
 
-lemma zgcd_1 [simp]: "zgcd m 1 = 1"
+lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
   by (simp add: zgcd_def abs_if)
 
-lemma zgcd_0_1_iff [simp]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
+lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
   by (simp add: zgcd_def abs_if)
 
-lemma zgcd_greatest_iff: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
+lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
   by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
 
-lemma zgcd_1_left [simp]: "zgcd 1 m = 1"
+lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
   by (simp add: zgcd_def gcd_1_left)
 
 lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
@@ -484,10 +714,10 @@
 
 definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
 
-lemma dvd_zlcm_self1[simp]: "i dvd zlcm i j"
+lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
 by(simp add:zlcm_def dvd_int_iff)
 
-lemma dvd_zlcm_self2[simp]: "j dvd zlcm i j"
+lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
 by(simp add:zlcm_def dvd_int_iff)