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