# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391377708 0
# Node ID ad3604df6bc6607a648df5efbd9ac4b80cf29ca0
# Parent  ada3ae6458d4d85ca86467aeeec4e3147ded8db8
new lemmas involving phi from Lehmer AFP entry

diff -r ada3ae6458d4 -r ad3604df6bc6 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 21:48:28 2014 +0000
@@ -289,6 +289,34 @@
 definition phi :: "int => nat"
   where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
 
+lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})"
+  apply (simp add: phi_def)
+  apply (rule bij_betw_same_card [of nat])
+  apply (auto simp add: inj_on_def bij_betw_def image_def)
+  apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
+  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)
+  done
+
+lemma prime_phi:
+  assumes  "2 \<le> p" "phi p = p - 1" shows "prime p"
+proof -
+  have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
+    using assms unfolding phi_def_nat
+    by (intro card_seteq) fastforce+
+  then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
+    by blast
+  { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
+    have "coprime x p" 
+      apply (rule cop)
+      using * apply auto
+      done
+    with `x dvd p` `1 < x` have "False" by auto }
+  then show ?thesis 
+    using `2 \<le> p` apply (simp add: prime_def)
+by (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_def)
 (* Auto hangs here. Once again, where is the simplification rule