src/HOL/Number_Theory/Residues.thy
changeset 63534 523b488b15c9
parent 63417 c184ec919c70
child 63537 831816778409
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 20 14:52:09 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jul 21 10:06:04 2016 +0200
     1.3 @@ -202,9 +202,9 @@
     1.4  subsection \<open>Prime residues\<close>
     1.5  
     1.6  locale residues_prime =
     1.7 -  fixes p and R (structure)
     1.8 +  fixes p :: nat and R (structure)
     1.9    assumes p_prime [intro]: "prime p"
    1.10 -  defines "R \<equiv> residue_ring p"
    1.11 +  defines "R \<equiv> residue_ring (int p)"
    1.12  
    1.13  sublocale residues_prime < residues p
    1.14    apply (unfold R_def residues_def)
    1.15 @@ -223,7 +223,7 @@
    1.16    apply (erule notE)
    1.17    apply (subst gcd.commute)
    1.18    apply (rule prime_imp_coprime_int)
    1.19 -  apply (rule p_prime)
    1.20 +  apply (simp add: p_prime)
    1.21    apply (rule notI)
    1.22    apply (frule zdvd_imp_le)
    1.23    apply auto
    1.24 @@ -280,7 +280,7 @@
    1.25    qed
    1.26    then show ?thesis
    1.27      using \<open>2 \<le> p\<close>
    1.28 -    by (simp add: prime_def)
    1.29 +    by (simp add: is_prime_nat_iff)
    1.30         (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
    1.31                not_numeral_le_zero one_dvd)
    1.32  qed
    1.33 @@ -347,19 +347,21 @@
    1.34    apply auto
    1.35    done
    1.36  
    1.37 -lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
    1.38 +lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
    1.39    apply (rule residues_prime.phi_prime)
    1.40 +  apply simp
    1.41    apply (erule residues_prime.intro)
    1.42    done
    1.43  
    1.44  lemma fermat_theorem:
    1.45    fixes a :: int
    1.46 -  assumes "prime p"
    1.47 +  assumes "prime (int p)"
    1.48      and "\<not> p dvd a"
    1.49    shows "[a^(p - 1) = 1] (mod p)"
    1.50  proof -
    1.51    from assms have "[a ^ phi p = 1] (mod p)"
    1.52 -    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
    1.53 +    by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
    1.54 +             simp: gcd.commute[of _ "int p"])
    1.55    also have "phi p = nat p - 1"
    1.56      by (rule phi_prime) (rule assms)
    1.57    finally show ?thesis
    1.58 @@ -367,7 +369,7 @@
    1.59  qed
    1.60  
    1.61  lemma fermat_theorem_nat:
    1.62 -  assumes "prime p" and "\<not> p dvd a"
    1.63 +  assumes "prime (int p)" and "\<not> p dvd a"
    1.64    shows "[a ^ (p - 1) = 1] (mod p)"
    1.65    using fermat_theorem [of p a] assms
    1.66    by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)