author chaieb Mon Jul 14 16:13:42 2008 +0200 (2008-07-14) changeset 27567 e3fe9a327c63 parent 27566 6b20092af078 child 27568 9949dc7a24de
Fixed proofs.
 src/HOL/Complex/ex/MIR.thy file | annotate | diff | revisions src/HOL/Complex/ex/ReflectedFerrack.thy file | annotate | diff | revisions src/HOL/Library/Abstract_Rat.thy file | annotate | diff | revisions src/HOL/Library/Primes.thy file | annotate | diff | revisions
```     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.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.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.23      ultimately have ?thesis using aa' bb'
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.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.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.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
```