src/HOL/Number_Theory/Residues.thy

--- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -398,7 +398,7 @@
   shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   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 :
+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}"
@@ -455,4 +455,52 @@
   ultimately show ?thesis ..
 qed
 
+
+subsection \<open>Upper bound for the number of $n$-th roots\<close>
+
+lemma roots_mod_prime_bound:
+  fixes n c p :: nat
+  assumes "prime p" "n > 0"
+  defines "A \<equiv> {x\<in>{..<p}. [x ^ n = c] (mod p)}"
+  shows   "card A \<le> n"
+proof -
+  define R where "R = residue_ring (int p)"
+  term monom
+  from assms(1) interpret residues_prime p R
+    by unfold_locales (simp_all add: R_def)
+  interpret R: UP_domain R "UP R" by (unfold_locales)
+
+  let ?f = "UnivPoly.monom (UP R) \<one>\<^bsub>R\<^esub> n \<ominus>\<^bsub>(UP R)\<^esub> UnivPoly.monom (UP R) (int (c mod p)) 0"
+  have in_carrier: "int (c mod p) \<in> carrier R"
+    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)
+  
+  have "deg R ?f = n"
+    using assms in_carrier by (simp add: R.deg_minus_eq)
+  hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
+  have roots_bound: "finite {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<and>
+                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
+                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
+  have subs: "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<subseteq>
+                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
+    using in_carrier by (auto simp: R.evalRR_simps)
+  then have "card {x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<le>
+               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
+    using finite by (intro card_mono) auto
+  also have "\<dots> \<le> n"
+    using \<open>deg R ?f = n\<close> roots_bound by linarith
+  also {
+    fix x assume "x \<in> carrier R"
+    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
+      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
+  }
+  hence "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} = {x \<in> carrier R. [x ^ n = int c] (mod p)}"
+    by (fastforce simp: cong_def zmod_int)
+  also have "bij_betw int A {x \<in> carrier R. [x ^ n = int c] (mod p)}"
+    by (rule bij_betwI[of int _ _ nat])
+       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
+  from bij_betw_same_card[OF this] have "card {x \<in> carrier R. [x ^ n = int c] (mod p)} = card A" ..
+  finally show ?thesis .
+qed
+
+
 end