src/HOL/Number_Theory/Primes.thy
changeset 62348 9a5f43dac883
parent 61762 d50b993b4fb9
child 62349 7c23469b5118
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
     1.6    apply (unfold prime_def)
     1.7 -  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
     1.8 +  apply (metis gcd_dvd1 gcd_dvd2)
     1.9    done
    1.10  
    1.11  lemma prime_int_altdef:
    1.12 @@ -72,22 +72,22 @@
    1.13      m = 1 \<or> m = p))"
    1.14    apply (simp add: prime_def)
    1.15    apply (auto simp add: )
    1.16 -  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
    1.17 +  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
    1.18    apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
    1.19    done
    1.20  
    1.21  lemma prime_imp_coprime_int:
    1.22    fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
    1.23    apply (unfold prime_int_altdef)
    1.24 -  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
    1.25 +  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
    1.26    done
    1.27  
    1.28  lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
    1.29 -  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
    1.30 +  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
    1.31  
    1.32  lemma prime_dvd_mult_int:
    1.33    fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
    1.34 -  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
    1.35 +  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
    1.36  
    1.37  lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
    1.38      p dvd m * n = (p dvd m \<or> p dvd n)"
    1.39 @@ -198,20 +198,20 @@
    1.40      { assume pa: "p dvd a"
    1.41        from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
    1.42        with p have "coprime b p"
    1.43 -        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    1.44 +        by (subst gcd.commute, intro prime_imp_coprime_nat)
    1.45        then have pnb: "coprime (p^n) b"
    1.46 -        by (subst gcd_commute_nat, rule coprime_exp_nat)
    1.47 -      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
    1.48 +        by (subst gcd.commute, rule coprime_exp_nat)
    1.49 +      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
    1.50      moreover
    1.51      { assume pb: "p dvd b"
    1.52        have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
    1.53        from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
    1.54          by auto
    1.55        with p have "coprime a p"
    1.56 -        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    1.57 +        by (subst gcd.commute, intro prime_imp_coprime_nat)
    1.58        then have pna: "coprime (p^n) a"
    1.59 -        by (subst gcd_commute_nat, rule coprime_exp_nat)
    1.60 -      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
    1.61 +        by (subst gcd.commute, rule coprime_exp_nat)
    1.62 +      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
    1.63      ultimately have ?thesis by blast }
    1.64    ultimately show ?thesis by blast
    1.65  qed