src/HOL/Number_Theory/Residues.thy

 *)
 
 section \<open>Residue rings\<close>
 
 theory Residues
-imports Cong MiscAlgebra
+imports
+  Cong
+  "~~/src/HOL/Algebra/More_Group"
+  "~~/src/HOL/Algebra/More_Ring"
+  "~~/src/HOL/Algebra/More_Finite_Product"
+  "~~/src/HOL/Algebra/Multiplicative_Group"
 begin
 
 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
   "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
 

   apply (simp add: add.commute mod_add_right_eq)
   apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
   done
 
 lemma finite [iff]: "finite (carrier R)"
-  by (subst res_carrier_eq) auto
+  by (simp add: res_carrier_eq)
 
 lemma finite_Units [iff]: "finite (Units R)"
-  by (subst res_units_eq) auto
+  by (simp add: finite_ring_finite_units)
 
 text \<open>
   The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
   residue classes. The following lemmas show that this mapping
   respects addition and multiplication on the integers.

   unfolding phi_def by (auto simp add: card_eq_0_iff)
 
 lemma phi_one [simp]: "phi 1 = 0"
   by (auto simp add: phi_def card_eq_0_iff)
 
+lemma phi_leq: "phi x \<le> nat x - 1"
+proof -
+  have "phi x \<le> card {1..x - 1}"
+    unfolding phi_def by (rule card_mono) auto
+  then show ?thesis by simp
+qed
+
+lemma phi_nonzero:
+  "phi x > 0" if "2 \<le> x"
+proof -
+  have "finite {y. 0 < y \<and> y < x}"
+    by simp
+  then have "finite {y. 0 < y \<and> y < x \<and> coprime y x}"
+    by (auto intro: rev_finite_subset)
+  moreover have "1 \<in> {y. 0 < y \<and> y < x \<and> coprime y x}"
+    using that by simp
+  ultimately have "card {y. 0 < y \<and> y < x \<and> coprime y x} \<noteq> 0"
+    by auto
+  then show ?thesis
+    by (simp add: phi_def)
+qed
+
 lemma (in residues) phi_eq: "phi m = card (Units R)"
   by (simp add: phi_def res_units_eq)
 
 lemma (in residues) euler_theorem1:
   assumes a: "gcd a m = 1"

   then show ?thesis
     using assms prime_ge_2_nat
     by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
 qed
 
+text {*
+  This result can be transferred to the multiplicative group of
+  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
+
+lemma mod_nat_int_pow_eq:
+  fixes n :: nat and p a :: int
+  assumes "a \<ge> 0" "p \<ge> 0"
+  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
+  using assms
+  by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
+
+theorem residue_prime_mult_group_has_gen :
+ fixes p :: nat
+ assumes prime_p : "prime p"
+ shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
+proof -
+  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
+  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
+    by (simp add: prime_p)
+  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
+    by (auto simp add: R.zero_cong R.res_carrier_eq)
+  obtain a where a:"a \<in> {1 .. int p - 1}"
+         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
+    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
+    by (auto simp add: car[symmetric] carrier_mult_of)
+  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
+    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
+  note * = this
+  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
+  proof
+    { fix n assume n: "n \<in> ?L"
+      then have "n \<in> ?R" using `p\<ge>2` by force
+    } thus "?L \<subseteq> ?R" by blast
+    { fix n assume n: "n \<in> ?R"
+      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
+    } thus "?R \<subseteq> ?L" by blast
+  qed
+  have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
+  proof
+    { fix x assume x: "x \<in> ?L"
+      then obtain i where i:"x = nat (a^i mod (int p))" by blast
+      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
+      hence "x \<in> ?R" using i by blast
+    } thus "?L \<subseteq> ?R" by blast
+    { fix x assume x: "x \<in> ?R"
+      then obtain i where i:"x = nat a^i mod p" by blast
+      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
+    } thus "?R \<subseteq> ?L" by blast
+  qed
+  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
+    using * a a_gen ** by presburger
+  moreover
+  have "nat a \<in> {1 .. p - 1}" using a by force
+  ultimately show ?thesis ..
+qed
+
 end