1.1 --- a/src/HOL/Complex/ex/MIR.thy Mon Jul 14 11:19:43 2008 +0200
1.2 +++ b/src/HOL/Complex/ex/MIR.thy Mon Jul 14 16:13:42 2008 +0200
1.3 @@ -761,12 +761,12 @@
1.4 have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
1.5 moreover {assume "abs c > 1" and gp: "?g > 1" with prems
1.6 have th: "dvdnumcoeff t ?g" by simp
1.7 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
1.8 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
1.9 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
1.10 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
1.11 moreover {assume "abs c = 0 \<and> ?g > 1"
1.12 with prems have th: "dvdnumcoeff t ?g" by simp
1.13 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
1.14 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
1.15 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
1.16 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
1.17 hence ?case by simp }
1.18 moreover {assume "abs c > 1" and g0:"?g = 0"
1.19 from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
1.20 @@ -779,17 +779,17 @@
1.21 have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
1.22 moreover {assume "abs c > 1" and gp: "?g > 1" with prems
1.23 have th: "dvdnumcoeff t ?g" by simp
1.24 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
1.25 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
1.26 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
1.27 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
1.28 moreover {assume "abs c = 0 \<and> ?g > 1"
1.29 with prems have th: "dvdnumcoeff t ?g" by simp
1.30 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
1.31 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
1.32 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
1.33 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
1.34 hence ?case by simp }
1.35 moreover {assume "abs c > 1" and g0:"?g = 0"
1.36 from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
1.37 ultimately show ?case by blast
1.38 -qed(auto simp add: zgcd_dvd1)
1.39 +qed(auto simp add: zgcd_zdvd1)
1.40
1.41 lemma dvdnumcoeff_aux2:
1.42 assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
1.43 @@ -1067,8 +1067,8 @@
1.44 from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
1.45 let ?tt = "reducecoeffh ?t' ?g'"
1.46 let ?t = "Inum bs ?tt"
1.47 - have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
1.48 - have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
1.49 + have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
1.50 + have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
1.51 have gpdgp: "?g' dvd ?g'" by simp
1.52 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
1.53 have th2:"real ?g' * ?t = Inum bs ?t'" by simp
1.54 @@ -1101,8 +1101,8 @@
1.55 moreover {assume "?g'=1" hence ?thesis using prems
1.56 by (auto simp add: Let_def simp_num_pair_def)}
1.57 moreover {assume g'1:"?g'>1"
1.58 - have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
1.59 - have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
1.60 + have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
1.61 + have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
1.62 have gpdgp: "?g' dvd ?g'" by simp
1.63 from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
1.64 from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
1.65 @@ -1240,8 +1240,8 @@
1.66 from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
1.67 let ?tt = "reducecoeffh t ?g'"
1.68 let ?t = "Inum bs ?tt"
1.69 - have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
1.70 - have gpdd: "?g' dvd d" by (simp add: zgcd_dvd1)
1.71 + have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
1.72 + have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1)
1.73 have gpdgp: "?g' dvd ?g'" by simp
1.74 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
1.75 have th2:"real ?g' * ?t = Inum bs t" by simp
1.76 @@ -4173,7 +4173,7 @@
1.77 by (induct p rule: isrlfm.induct, auto)
1.78 lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
1.79 proof-
1.80 - from zgcd_dvd1 have th: "zgcd i j dvd i" by blast
1.81 + from zgcd_zdvd1 have th: "zgcd i j dvd i" by blast
1.82 from zdvd_imp_le[OF th ip] show ?thesis .
1.83 qed
1.84
2.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Jul 14 11:19:43 2008 +0200
2.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Jul 14 16:13:42 2008 +0200
2.3 @@ -573,17 +573,17 @@
2.4 have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
2.5 moreover {assume "abs c > 1" and gp: "?g > 1" with prems
2.6 have th: "dvdnumcoeff t ?g" by simp
2.7 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
2.8 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
2.9 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
2.10 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
2.11 moreover {assume "abs c = 0 \<and> ?g > 1"
2.12 with prems have th: "dvdnumcoeff t ?g" by simp
2.13 - have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
2.14 - from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
2.15 + have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
2.16 + from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
2.17 hence ?case by simp }
2.18 moreover {assume "abs c > 1" and g0:"?g = 0"
2.19 from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
2.20 ultimately show ?case by blast
2.21 -qed(auto simp add: zgcd_dvd1)
2.22 +qed(auto simp add: zgcd_zdvd1)
2.23
2.24 lemma dvdnumcoeff_aux2:
2.25 assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
2.26 @@ -753,8 +753,8 @@
2.27 from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
2.28 let ?tt = "reducecoeffh ?t' ?g'"
2.29 let ?t = "Inum bs ?tt"
2.30 - have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
2.31 - have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
2.32 + have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
2.33 + have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
2.34 have gpdgp: "?g' dvd ?g'" by simp
2.35 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
2.36 have th2:"real ?g' * ?t = Inum bs ?t'" by simp
2.37 @@ -787,8 +787,8 @@
2.38 moreover {assume "?g'=1" hence ?thesis using prems
2.39 by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
2.40 moreover {assume g'1:"?g'>1"
2.41 - have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
2.42 - have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
2.43 + have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
2.44 + have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)
2.45 have gpdgp: "?g' dvd ?g'" by simp
2.46 from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
2.47 from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
3.1 --- a/src/HOL/Library/Abstract_Rat.thy Mon Jul 14 11:19:43 2008 +0200
3.2 +++ b/src/HOL/Library/Abstract_Rat.thy Mon Jul 14 16:13:42 2008 +0200
3.3 @@ -44,7 +44,7 @@
3.4 let ?g' = "zgcd ?a' ?b'"
3.5 from anz bnz have "?g \<noteq> 0" by simp with zgcd_pos[of a b]
3.6 have gpos: "?g > 0" by arith
3.7 - have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
3.8 + have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
3.9 from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
3.10 anz bnz
3.11 have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
3.12 @@ -296,10 +296,8 @@
3.13 let ?g = "zgcd (a * b' + b * a') (b*b')"
3.14 have gz: "?g \<noteq> 0" using z by simp
3.15 have ?thesis using aa' bb' z gz
3.16 - of_int_div[where ?'a = 'a,
3.17 - OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
3.18 - of_int_div[where ?'a = 'a,
3.19 - OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
3.20 + 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,
3.21 + OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
3.22 by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
3.23 ultimately have ?thesis using aa' bb'
3.24 by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
3.25 @@ -320,8 +318,8 @@
3.26 {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
3.27 let ?g="zgcd (a*a') (b*b')"
3.28 have gz: "?g \<noteq> 0" using z by simp
3.29 - from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]]
3.30 - of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]]
3.31 + from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]]
3.32 + of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]]
3.33 have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
3.34 ultimately show ?thesis by blast
3.35 qed
4.1 --- a/src/HOL/Library/Primes.thy Mon Jul 14 11:19:43 2008 +0200
4.2 +++ b/src/HOL/Library/Primes.thy Mon Jul 14 16:13:42 2008 +0200
4.3 @@ -12,7 +12,7 @@
4.4
4.5 definition
4.6 coprime :: "nat => nat => bool" where
4.7 - "coprime m n \<longleftrightarrow> (gcd m n = 1)"
4.8 + "coprime m n \<longleftrightarrow> gcd m n = 1"
4.9
4.10 definition
4.11 prime :: "nat \<Rightarrow> bool" where
4.12 @@ -314,7 +314,7 @@
4.13 assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
4.14 from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b]
4.15 have th: "gcd a b dvd d" by blast
4.16 - from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d =gcd a b" by blast
4.17 + from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d = gcd a b" by blast
4.18 qed
4.19
4.20 lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
4.21 @@ -351,7 +351,7 @@
4.22 thus ?thesis by blast
4.23 qed
4.24
4.25 -lemma gcd_mult_distrib: "gcd (a * c) (b * c) = c * gcd a b"
4.26 +lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
4.27 by(simp add: gcd_mult_distrib2 mult_commute)
4.28
4.29 lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
4.30 @@ -388,19 +388,20 @@
4.31 lemma gcd_mult': "gcd b (a * b) = b"
4.32 by (simp add: gcd_mult mult_commute[of a b])
4.33
4.34 -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"
4.35 +lemma gcd_add: "gcd(a + b) b = gcd a b"
4.36 + "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
4.37 apply (simp_all add: gcd_add1)
4.38 by (simp add: gcd_commute gcd_add1)
4.39
4.40 -lemma gcd_sub: "b <= a ==> gcd (a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
4.41 +lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
4.42 proof-
4.43 {fix a b assume H: "b \<le> (a::nat)"
4.44 hence th: "a - b + b = a" by arith
4.45 - from gcd_add(1)[of "a - b" b] th have "gcd (a - b) b = gcd a b" by simp}
4.46 + from gcd_add(1)[of "a - b" b] th have "gcd(a - b) b = gcd a b" by simp}
4.47 note th = this
4.48 {
4.49 assume ab: "b \<le> a"
4.50 - from th[OF ab] show "gcd (a - b) b = gcd a b" by blast
4.51 + from th[OF ab] show "gcd (a - b) b = gcd a b" by blast
4.52 next
4.53 assume ab: "a \<le> b"
4.54 from th[OF ab] show "gcd a (b - a) = gcd a b"
4.55 @@ -448,7 +449,7 @@
4.56 shows "coprime d (a * b)"
4.57 proof-
4.58 from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute)
4.59 - from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a * b) = 1"
4.60 + from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a*b) = 1"
4.61 by (simp add: gcd_commute)
4.62 thus ?thesis unfolding coprime_def .
4.63 qed
4.64 @@ -530,10 +531,11 @@
4.65 hence ?thesis by blast }
4.66 ultimately show ?thesis by blast
4.67 qed
4.68 -lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b ^ n"
4.69 +
4.70 +lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b^n"
4.71 proof-
4.72 let ?g = "gcd (a^n) (b^n)"
4.73 - let ?gn = "gcd a b ^ n"
4.74 + let ?gn = "gcd a b^n"
4.75 {fix e assume H: "e dvd a^n" "e dvd b^n"
4.76 from bezout_gcd_pow[of a n b] obtain x y
4.77 where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast