src/HOL/Number_Theory/Residues.thy
changeset 69785 9e326f6f8a24
parent 68458 023b353911c5
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -398,7 +398,7 @@
     1.4    shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
     1.5    by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
     1.6  
     1.7 -theorem residue_prime_mult_group_has_gen :
     1.8 +theorem residue_prime_mult_group_has_gen:
     1.9   fixes p :: nat
    1.10   assumes prime_p : "prime p"
    1.11   shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
    1.12 @@ -455,4 +455,52 @@
    1.13    ultimately show ?thesis ..
    1.14  qed
    1.15  
    1.16 +
    1.17 +subsection \<open>Upper bound for the number of $n$-th roots\<close>
    1.18 +
    1.19 +lemma roots_mod_prime_bound:
    1.20 +  fixes n c p :: nat
    1.21 +  assumes "prime p" "n > 0"
    1.22 +  defines "A \<equiv> {x\<in>{..<p}. [x ^ n = c] (mod p)}"
    1.23 +  shows   "card A \<le> n"
    1.24 +proof -
    1.25 +  define R where "R = residue_ring (int p)"
    1.26 +  term monom
    1.27 +  from assms(1) interpret residues_prime p R
    1.28 +    by unfold_locales (simp_all add: R_def)
    1.29 +  interpret R: UP_domain R "UP R" by (unfold_locales)
    1.30 +
    1.31 +  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"
    1.32 +  have in_carrier: "int (c mod p) \<in> carrier R"
    1.33 +    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)
    1.34 +  
    1.35 +  have "deg R ?f = n"
    1.36 +    using assms in_carrier by (simp add: R.deg_minus_eq)
    1.37 +  hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
    1.38 +  have roots_bound: "finite {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<and>
    1.39 +                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
    1.40 +                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
    1.41 +  have subs: "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<subseteq>
    1.42 +                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
    1.43 +    using in_carrier by (auto simp: R.evalRR_simps)
    1.44 +  then have "card {x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<le>
    1.45 +               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
    1.46 +    using finite by (intro card_mono) auto
    1.47 +  also have "\<dots> \<le> n"
    1.48 +    using \<open>deg R ?f = n\<close> roots_bound by linarith
    1.49 +  also {
    1.50 +    fix x assume "x \<in> carrier R"
    1.51 +    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
    1.52 +      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
    1.53 +  }
    1.54 +  hence "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} = {x \<in> carrier R. [x ^ n = int c] (mod p)}"
    1.55 +    by (fastforce simp: cong_def zmod_int)
    1.56 +  also have "bij_betw int A {x \<in> carrier R. [x ^ n = int c] (mod p)}"
    1.57 +    by (rule bij_betwI[of int _ _ nat])
    1.58 +       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
    1.59 +  from bij_betw_same_card[OF this] have "card {x \<in> carrier R. [x ^ n = int c] (mod p)} = card A" ..
    1.60 +  finally show ?thesis .
    1.61 +qed
    1.62 +
    1.63 +
    1.64  end