--- 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)