src/HOL/Number_Theory/Residues.thy
 changeset 55242 413ec965f95d parent 55227 653de351d21c child 55261 ad3604df6bc6
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 01 22:02:20 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 19:15:25 2014 +0000
1.3 @@ -14,7 +14,6 @@
1.4    MiscAlgebra
1.5  begin
1.6
1.7 -
1.8  (*
1.9
1.10    A locale for residue rings
1.11 @@ -235,13 +234,14 @@
1.12  (* prime residues *)
1.13
1.14  locale residues_prime =
1.15 -  fixes p :: int and R (structure)
1.16 +  fixes p and R (structure)
1.17    assumes p_prime [intro]: "prime p"
1.18    defines "R == residue_ring p"
1.19
1.20  sublocale residues_prime < residues p
1.21    apply (unfold R_def residues_def)
1.22    using p_prime apply auto
1.23 +  apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
1.24    done
1.25
1.26  context residues_prime
1.27 @@ -357,26 +357,26 @@
1.28    done
1.29
1.30  lemma fermat_theorem:
1.31 +  fixes a::int
1.32    assumes "prime p" and "~ (p dvd a)"
1.33 -  shows "[a^(nat p - 1) = 1] (mod p)"
1.34 +  shows "[a^(p - 1) = 1] (mod p)"
1.35  proof -
1.36    from assms have "[a^phi p = 1] (mod p)"
1.37      apply (intro euler_theorem)
1.38 -    (* auto should get this next part. matching across
1.39 -       substitutions is needed. *)
1.40 -    apply (frule prime_gt_1_int, arith)
1.41 -    apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
1.42 +    apply (metis of_nat_0_le_iff)
1.43 +    apply (metis gcd_int.commute prime_imp_coprime_int)
1.44      done
1.45    also have "phi p = nat p - 1"
1.46      by (rule phi_prime, rule assms)
1.47 -  finally show ?thesis .
1.48 +  finally show ?thesis
1.49 +    by (metis nat_int)
1.50  qed
1.51
1.52  lemma fermat_theorem_nat:
1.53    assumes "prime p" and "~ (p dvd a)"
1.54    shows "[a^(p - 1) = 1] (mod p)"
1.55  using fermat_theorem [of p a] assms
1.56 -by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
1.57 +by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
1.58
1.59
1.60  subsection {* Wilson's theorem *}
1.61 @@ -445,18 +445,20 @@
1.62      apply auto
1.63      done
1.64    also have "\<dots> = fact (p - 1) mod p"
1.65 -    apply (subst fact_altdef_int)
1.66 -    apply (insert assms, force)
1.67 -    apply (subst res_prime_units_eq, rule refl)
1.68 +    apply (subst fact_altdef_nat)
1.69 +    apply (insert assms)
1.70 +    apply (subst res_prime_units_eq)
1.71 +    apply (simp add: int_setprod zmod_int setprod_int_eq)
1.72      done
1.73    finally have "fact (p - 1) mod p = \<ominus> \<one>".
1.74 -  then show ?thesis by (simp add: res_to_cong_simps)
1.75 +  then show ?thesis
1.76 +    by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
1.77  qed
1.78
1.79 -lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
1.80 -  apply (frule prime_gt_1_int)
1.81 +lemma wilson_theorem: "prime p \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
1.82 +  apply (frule prime_gt_1_nat)
1.83    apply (case_tac "p = 2")
1.84 -  apply (subst fact_altdef_int, simp)
1.85 +  apply (subst fact_altdef_nat, simp)
1.86    apply (subst cong_int_def)
1.87    apply simp
1.88    apply (rule residues_prime.wilson_theorem1)
```