Fixed proofs.
--- a/src/HOL/Complex/ex/MIR.thy Mon Jul 14 11:19:43 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Mon Jul 14 16:13:42 2008 +0200
@@ -761,12 +761,12 @@
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
@@ -779,17 +779,17 @@
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
ultimately show ?case by blast
-qed(auto simp add: zgcd_dvd1)
+qed(auto simp add: zgcd_zdvd1)
lemma dvdnumcoeff_aux2:
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -1067,8 +1067,8 @@
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
let ?tt = "reducecoeffh ?t' ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -1101,8 +1101,8 @@
moreover {assume "?g'=1" hence ?thesis using prems
by (auto simp add: Let_def simp_num_pair_def)}
moreover {assume g'1:"?g'>1"
- have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
have gpdgp: "?g' dvd ?g'" by simp
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
@@ -1240,8 +1240,8 @@
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
let ?tt = "reducecoeffh t ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
- have gpdd: "?g' dvd d" by (simp add: zgcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+ have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs t" by simp
@@ -4173,7 +4173,7 @@
by (induct p rule: isrlfm.induct, auto)
lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
proof-
- from zgcd_dvd1 have th: "zgcd i j dvd i" by blast
+ from zgcd_zdvd1 have th: "zgcd i j dvd i" by blast
from zdvd_imp_le[OF th ip] show ?thesis .
qed
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Jul 14 11:19:43 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Jul 14 16:13:42 2008 +0200
@@ -573,17 +573,17 @@
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
ultimately show ?case by blast
-qed(auto simp add: zgcd_dvd1)
+qed(auto simp add: zgcd_zdvd1)
lemma dvdnumcoeff_aux2:
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -753,8 +753,8 @@
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
let ?tt = "reducecoeffh ?t' ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -787,8 +787,8 @@
moreover {assume "?g'=1" hence ?thesis using prems
by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
moreover {assume g'1:"?g'>1"
- have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
have gpdgp: "?g' dvd ?g'" by simp
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
--- a/src/HOL/Library/Abstract_Rat.thy Mon Jul 14 11:19:43 2008 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Jul 14 16:13:42 2008 +0200
@@ -44,7 +44,7 @@
let ?g' = "zgcd ?a' ?b'"
from anz bnz have "?g \<noteq> 0" by simp with zgcd_pos[of a b]
have gpos: "?g > 0" by arith
- have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
+ have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
anz bnz
have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
@@ -296,10 +296,8 @@
let ?g = "zgcd (a * b' + b * a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
have ?thesis using aa' bb' z gz
- of_int_div[where ?'a = 'a,
- OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
- of_int_div[where ?'a = 'a,
- OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
+ of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a * b' + b * a'" and j="b*b'"]] of_int_div[where ?'a = 'a,
+ OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
ultimately have ?thesis using aa' bb'
by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
@@ -320,8 +318,8 @@
{assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
let ?g="zgcd (a*a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
- from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]]
- of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]]
+ from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]]
+ of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]]
have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
ultimately show ?thesis by blast
qed
--- a/src/HOL/Library/Primes.thy Mon Jul 14 11:19:43 2008 +0200
+++ b/src/HOL/Library/Primes.thy Mon Jul 14 16:13:42 2008 +0200
@@ -12,7 +12,7 @@
definition
coprime :: "nat => nat => bool" where
- "coprime m n \<longleftrightarrow> (gcd m n = 1)"
+ "coprime m n \<longleftrightarrow> gcd m n = 1"
definition
prime :: "nat \<Rightarrow> bool" where
@@ -314,7 +314,7 @@
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
+ 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"
@@ -351,7 +351,7 @@
thus ?thesis by blast
qed
-lemma gcd_mult_distrib: "gcd (a * c) (b * c) = c * gcd a b"
+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"
@@ -388,19 +388,20 @@
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"
+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"
+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}
+ 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
+ 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"
@@ -448,7 +449,7 @@
shows "coprime d (a * b)"
proof-
from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute)
- from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a * b) = 1"
+ from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a*b) = 1"
by (simp add: gcd_commute)
thus ?thesis unfolding coprime_def .
qed
@@ -530,10 +531,11 @@
hence ?thesis by blast }
ultimately show ?thesis by blast
qed
-lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b ^ n"
+
+lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b^n"
proof-
let ?g = "gcd (a^n) (b^n)"
- let ?gn = "gcd a b ^ n"
+ let ?gn = "gcd a b^n"
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast