src/HOL/Number_Theory/Residues.thy
```     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
```