src/HOL/Number_Theory/Primes.thy
changeset 60688 01488b559910
parent 60526 fad653acf58f
child 60804 080a979a985b
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:40 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:41 2015 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
     1.6    apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
     1.7 -  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
     1.8 +  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
     1.9    done
    1.10  
    1.11  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    1.12 @@ -159,11 +159,11 @@
    1.13  
    1.14  
    1.15  lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
    1.16 -  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
    1.17 +  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
    1.18  
    1.19  lemma prime_imp_power_coprime_int:
    1.20    fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
    1.21 -  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
    1.22 +  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
    1.23  
    1.24  lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
    1.25    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
    1.26 @@ -375,7 +375,7 @@
    1.27  lemma bezout_gcd_nat:
    1.28    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
    1.29    using bezout_nat[of a b]
    1.30 -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
    1.31 +by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute
    1.32    gcd_nat.right_neutral mult_0)
    1.33  
    1.34  lemma gcd_bezout_sum_nat:
    1.35 @@ -423,7 +423,7 @@
    1.36    shows "\<exists>x y. a*x = Suc (p*y)"
    1.37  proof-
    1.38    have ap: "coprime a p"
    1.39 -    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
    1.40 +    by (metis gcd.commute p pa prime_imp_coprime_nat)
    1.41    from coprime_bezout_strong[OF ap] show ?thesis
    1.42      by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
    1.43  qed