src/HOL/Number_Theory/Residues.thy
changeset 55261 ad3604df6bc6
parent 55242 413ec965f95d
child 55262 16724746ad89
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 21:48:28 2014 +0000
     1.3 @@ -289,6 +289,34 @@
     1.4  definition phi :: "int => nat"
     1.5    where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
     1.6  
     1.7 +lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})"
     1.8 +  apply (simp add: phi_def)
     1.9 +  apply (rule bij_betw_same_card [of nat])
    1.10 +  apply (auto simp add: inj_on_def bij_betw_def image_def)
    1.11 +  apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
    1.12 +  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int transfer_int_nat_gcd(1) zless_int)
    1.13 +  done
    1.14 +
    1.15 +lemma prime_phi:
    1.16 +  assumes  "2 \<le> p" "phi p = p - 1" shows "prime p"
    1.17 +proof -
    1.18 +  have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
    1.19 +    using assms unfolding phi_def_nat
    1.20 +    by (intro card_seteq) fastforce+
    1.21 +  then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
    1.22 +    by blast
    1.23 +  { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
    1.24 +    have "coprime x p" 
    1.25 +      apply (rule cop)
    1.26 +      using * apply auto
    1.27 +      done
    1.28 +    with `x dvd p` `1 < x` have "False" by auto }
    1.29 +  then show ?thesis 
    1.30 +    using `2 \<le> p` apply (simp add: prime_def)
    1.31 +by (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
    1.32 +  not_numeral_le_zero one_dvd)
    1.33 +qed
    1.34 +
    1.35  lemma phi_zero [simp]: "phi 0 = 0"
    1.36    apply (subst phi_def)
    1.37  (* Auto hangs here. Once again, where is the simplification rule