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)