src/HOL/Number_Theory/Primes.thy
 changeset 62429 25271ff79171 parent 62410 2fc7a8d9c529 child 62481 b5d8e57826df
1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Feb 26 18:33:01 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Feb 26 22:15:09 2016 +0100
1.3 @@ -152,11 +152,11 @@
1.6  lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.7 -  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
1.8 +  by (metis coprime_exp gcd.commute prime_imp_coprime_nat)
1.10  lemma prime_imp_power_coprime_int:
1.11    fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.12 -  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
1.13 +  by (metis coprime_exp gcd.commute prime_imp_coprime_int)
1.15  lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.16    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
1.17 @@ -203,7 +203,7 @@
1.18        with p have "coprime b p"
1.19          by (subst gcd.commute, intro prime_imp_coprime_nat)
1.20        then have pnb: "coprime (p^n) b"
1.21 -        by (subst gcd.commute, rule coprime_exp_nat)
1.22 +        by (subst gcd.commute, rule coprime_exp)
1.23        from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
1.24      moreover
1.25      { assume pb: "p dvd b"
1.26 @@ -213,7 +213,7 @@
1.27        with p have "coprime a p"
1.28          by (subst gcd.commute, intro prime_imp_coprime_nat)
1.29        then have pna: "coprime (p^n) a"
1.30 -        by (subst gcd.commute, rule coprime_exp_nat)
1.31 +        by (subst gcd.commute, rule coprime_exp)
1.32        from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
1.33      ultimately have ?thesis by blast }
1.34    ultimately show ?thesis by blast
1.35 @@ -374,7 +374,7 @@
1.36  lemma bezout_gcd_nat:
1.37    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
1.38    using bezout_nat[of a b]