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
```