src/HOL/Number_Theory/Residues.thy

 
 
 subsection \<open>Prime residues\<close>
 
 locale residues_prime =
-  fixes p and R (structure)
+  fixes p :: nat and R (structure)
   assumes p_prime [intro]: "prime p"
-  defines "R \<equiv> residue_ring p"
+  defines "R \<equiv> residue_ring (int p)"
 
 sublocale residues_prime < residues p
   apply (unfold R_def residues_def)
   using p_prime apply auto
   apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)

   apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
   apply (rule classical)
   apply (erule notE)
   apply (subst gcd.commute)
   apply (rule prime_imp_coprime_int)
-  apply (rule p_prime)
+  apply (simp add: p_prime)
   apply (rule notI)
   apply (frule zdvd_imp_le)
   apply auto
   done
 

     with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
       by auto
   qed
   then show ?thesis
     using \<open>2 \<le> p\<close>
-    by (simp add: prime_def)
+    by (simp add: is_prime_nat_iff)
        (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
               not_numeral_le_zero one_dvd)
 qed
 
 lemma phi_zero [simp]: "phi 0 = 0"

   apply (subst phi_eq)
   apply (subst res_prime_units_eq)
   apply auto
   done
 
-lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
+lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
   apply (rule residues_prime.phi_prime)
+  apply simp
   apply (erule residues_prime.intro)
   done
 
 lemma fermat_theorem:
   fixes a :: int
-  assumes "prime p"
+  assumes "prime (int p)"
     and "\<not> p dvd a"
   shows "[a^(p - 1) = 1] (mod p)"
 proof -
   from assms have "[a ^ phi p = 1] (mod p)"
-    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
+    by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
+             simp: gcd.commute[of _ "int p"])
   also have "phi p = nat p - 1"
     by (rule phi_prime) (rule assms)
   finally show ?thesis
     by (metis nat_int)
 qed
 
 lemma fermat_theorem_nat:
-  assumes "prime p" and "\<not> p dvd a"
+  assumes "prime (int p)" and "\<not> p dvd a"
   shows "[a ^ (p - 1) = 1] (mod p)"
   using fermat_theorem [of p a] assms
   by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)