author | chaieb |

Mon Jul 14 16:13:42 2008 +0200 (2008-07-14) | |

changeset 27567 | e3fe9a327c63 |

parent 27566 | 6b20092af078 |

child 27568 | 9949dc7a24de |

Fixed proofs.

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