# HG changeset patch # User chaieb # Date 1216044822 -7200 # Node ID e3fe9a327c63e4cfa2c72d479b869f27fcda5ce5 # Parent 6b20092af078d4c9d9f3dbef73297c10407abbc8 Fixed proofs. diff -r 6b20092af078 -r e3fe9a327c63 src/HOL/Complex/ex/MIR.thy --- 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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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) \ 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' \ 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 \ 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 diff -r 6b20092af078 -r e3fe9a327c63 src/HOL/Complex/ex/ReflectedFerrack.thy --- 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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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) \ 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' \ n" . from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] diff -r 6b20092af078 -r e3fe9a327c63 src/HOL/Library/Abstract_Rat.thy --- 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 \ 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' \ 0" "?b' \ 0" @@ -296,10 +296,8 @@ let ?g = "zgcd (a * b' + b * a') (b*b')" have gz: "?g \ 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 \ 0" "a' \ 0" "b \ 0" "b' \ 0" let ?g="zgcd (a*a') (b*b')" have gz: "?g \ 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 diff -r 6b20092af078 -r e3fe9a327c63 src/HOL/Library/Primes.thy --- 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 \ (gcd m n = 1)" + "coprime m n \ gcd m n = 1" definition prime :: "nat \ bool" where @@ -314,7 +314,7 @@ assume H: "d dvd a" "d dvd b" "\e. e dvd a \ e dvd b \ 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: "\d. d dvd x \ d dvd y \ d dvd u \ 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: "(\x y. a * x - b * y = d \ b * x - a * y = d) \ 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 \ (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 \ 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 \ 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 \ b ^ n * x - a ^ n * y = ?gn" by blast