Fixed proofs.
authorchaieb
Mon Jul 14 16:13:42 2008 +0200 (2008-07-14)
changeset 27567e3fe9a327c63
parent 27566 6b20092af078
child 27568 9949dc7a24de
Fixed proofs.
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Primes.thy
     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