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.4  
     1.5  
     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.9  
    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.14  
    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]
    1.39 -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute
    1.40 +by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
    1.41    gcd_nat.right_neutral mult_0)
    1.42  
    1.43  lemma gcd_bezout_sum_nat: