src/HOL/Number_Theory/Pocklington.thy
changeset 69785 9e326f6f8a24
parent 69064 5840724b1d71
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Number_Theory/Pocklington.thy
     1.5 -    Author:     Amine Chaieb
     1.6 +    Author:     Amine Chaieb, Manuel Eberl
     1.7  *)
     1.8  
     1.9  section \<open>Pocklington's Theorem for Primes\<close>
    1.10 @@ -270,7 +270,7 @@
    1.11  qed
    1.12  
    1.13  
    1.14 -subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
    1.15 +subsection \<open>Definition of the order of a number mod \<open>n\<close>\<close>
    1.16  
    1.17  definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
    1.18  
    1.19 @@ -439,6 +439,425 @@
    1.20    qed
    1.21  qed
    1.22  
    1.23 +lemma ord_not_coprime [simp]: "\<not>coprime n a \<Longrightarrow> ord n a = 0"
    1.24 +  by (simp add: ord_def)
    1.25 +
    1.26 +lemma ord_1 [simp]: "ord 1 n = 1"
    1.27 +proof -
    1.28 +  have "(LEAST k. k > 0) = (1 :: nat)"
    1.29 +    by (rule Least_equality) auto
    1.30 +  thus ?thesis by (simp add: ord_def)
    1.31 +qed
    1.32 +
    1.33 +lemma ord_1_right [simp]: "ord (n::nat) 1 = 1"
    1.34 +  using ord_divides[of 1 1 n] by simp
    1.35 +
    1.36 +lemma ord_Suc_0_right [simp]: "ord (n::nat) (Suc 0) = 1"
    1.37 +  using ord_divides[of 1 1 n] by simp
    1.38 +
    1.39 +lemma ord_0_nat [simp]: "ord 0 (n :: nat) = (if n = 1 then 1 else 0)"
    1.40 +proof -
    1.41 +  have "(LEAST k. k > 0) = (1 :: nat)"
    1.42 +    by (rule Least_equality) auto
    1.43 +  thus ?thesis by (auto simp: ord_def)
    1.44 +qed
    1.45 +
    1.46 +lemma ord_0_right_nat [simp]: "ord (n :: nat) 0 = (if n = 1 then 1 else 0)"
    1.47 +proof -
    1.48 +  have "(LEAST k. k > 0) = (1 :: nat)"
    1.49 +    by (rule Least_equality) auto
    1.50 +  thus ?thesis by (auto simp: ord_def)
    1.51 +qed
    1.52 +
    1.53 +lemma ord_divides': "[a ^ d = Suc 0] (mod n) = (ord n a dvd d)"
    1.54 +  using ord_divides[of a d n] by simp
    1.55 +
    1.56 +lemma ord_Suc_0 [simp]: "ord (Suc 0) n = 1"
    1.57 +  using ord_1[where 'a = nat] by (simp del: ord_1)
    1.58 +
    1.59 +lemma ord_mod [simp]: "ord n (k mod n) = ord n k"
    1.60 +  by (cases "n = 0") (auto simp add: ord_def cong_def power_mod)
    1.61 +
    1.62 +lemma ord_gt_0_iff [simp]: "ord (n::nat) x > 0 \<longleftrightarrow> coprime n x"
    1.63 +  using ord_eq_0[of n x] by auto
    1.64 +
    1.65 +lemma ord_eq_Suc_0_iff: "ord n (x::nat) = Suc 0 \<longleftrightarrow> [x = 1] (mod n)"
    1.66 +  using ord_divides[of x 1 n] by (auto simp: ord_divides')
    1.67 +
    1.68 +lemma ord_cong:
    1.69 +  assumes "[k1 = k2] (mod n)"
    1.70 +  shows   "ord n k1 = ord n k2"
    1.71 +proof -
    1.72 +  have "ord n (k1 mod n) = ord n (k2 mod n)"
    1.73 +    by (simp only: assms[unfolded cong_def])
    1.74 +  thus ?thesis by simp
    1.75 +qed
    1.76 +
    1.77 +lemma ord_nat_code [code_unfold]:
    1.78 +  "ord n a =
    1.79 +     (if n = 0 then if a = 1 then 1 else 0 else
    1.80 +        if coprime n a then Min (Set.filter (\<lambda>k. [a ^ k = 1] (mod n)) {0<..n}) else 0)"
    1.81 +proof (cases "coprime n a \<and> n > 0")
    1.82 +  case True
    1.83 +  define A where "A = {k\<in>{0<..n}. [a ^ k = 1] (mod n)}"
    1.84 +  define k where "k = (LEAST k. k > 0 \<and> [a ^ k = 1] (mod n))"
    1.85 +  have totient: "totient n \<in> A"
    1.86 +    using euler_theorem[of a n] True
    1.87 +    by (auto simp: A_def coprime_commute intro!: Nat.gr0I totient_le)
    1.88 +  moreover have "finite A" by (auto simp: A_def)
    1.89 +  ultimately have *: "Min A \<in> A" and "\<forall>y. y \<in> A \<longrightarrow> Min A \<le> y"
    1.90 +    by (auto intro: Min_in)
    1.91 +
    1.92 +  have "k > 0 \<and> [a ^ k = 1] (mod n)"
    1.93 +    unfolding k_def by (rule LeastI[of _ "totient n"]) (use totient in \<open>auto simp: A_def\<close>)
    1.94 +  moreover have "k \<le> totient n"
    1.95 +    unfolding k_def by (intro Least_le) (use totient in \<open>auto simp: A_def\<close>)
    1.96 +  ultimately have "k \<in> A" using totient_le[of n] by (auto simp: A_def)
    1.97 +  hence "Min A \<le> k" by (intro Min_le) (auto simp: \<open>finite A\<close>)
    1.98 +  moreover from * have "k \<le> Min A"
    1.99 +    unfolding k_def by (intro Least_le) (auto simp: A_def)
   1.100 +  ultimately show ?thesis using True by (simp add: ord_def k_def A_def Set.filter_def)
   1.101 +qed auto
   1.102 +
   1.103 +theorem ord_modulus_mult_coprime:
   1.104 +  fixes x :: nat
   1.105 +  assumes "coprime m n"
   1.106 +  shows   "ord (m * n) x = lcm (ord m x) (ord n x)"
   1.107 +proof (intro dvd_antisym)
   1.108 +  have "[x ^ lcm (ord m x) (ord n x) = 1] (mod (m * n))"
   1.109 +    using assms by (intro coprime_cong_mult_nat assms) (auto simp: ord_divides')
   1.110 +  thus "ord (m * n) x dvd lcm (ord m x) (ord n x)"
   1.111 +    by (simp add: ord_divides')
   1.112 +next
   1.113 +  show "lcm (ord m x) (ord n x) dvd ord (m * n) x"
   1.114 +  proof (intro lcm_least)
   1.115 +    show "ord m x dvd ord (m * n) x"
   1.116 +      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 m n] assms
   1.117 +      by (simp add: ord_divides')
   1.118 +    show "ord n x dvd ord (m * n) x"
   1.119 +      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 n m] assms
   1.120 +      by (simp add: ord_divides' mult.commute)
   1.121 +  qed
   1.122 +qed
   1.123 +
   1.124 +corollary ord_modulus_prod_coprime:
   1.125 +  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
   1.126 +  shows   "ord (\<Prod>i\<in>A. f i :: nat) x = (LCM i\<in>A. ord (f i) x)"
   1.127 +  using assms by (induction A rule: finite_induct)
   1.128 +                 (simp, simp, subst ord_modulus_mult_coprime, auto intro!: prod_coprime_right)
   1.129 +
   1.130 +lemma ord_power_aux:
   1.131 +  fixes m x k a :: nat
   1.132 +  defines "l \<equiv> ord m a"
   1.133 +  shows   "ord m (a ^ k) * gcd k l = l"
   1.134 +proof (rule dvd_antisym)
   1.135 +  have "[a ^ lcm k l = 1] (mod m)"
   1.136 +    unfolding ord_divides by (simp add: l_def)
   1.137 +  also have "lcm k l = k * (l div gcd k l)"
   1.138 +    by (simp add: lcm_nat_def div_mult_swap)
   1.139 +  finally have "ord m (a ^ k) dvd l div gcd k l"
   1.140 +    unfolding ord_divides [symmetric] by (simp add: power_mult [symmetric])
   1.141 +  thus "ord m (a ^ k) * gcd k l dvd l"
   1.142 +    by (cases "l = 0") (auto simp: dvd_div_iff_mult)
   1.143 +
   1.144 +  have "[(a ^ k) ^ ord m (a ^ k) = 1] (mod m)"
   1.145 +    by (rule ord)
   1.146 +  also have "(a ^ k) ^ ord m (a ^ k) = a ^ (k * ord m (a ^ k))"
   1.147 +    by (simp add: power_mult)
   1.148 +  finally have "ord m a dvd k * ord m (a ^ k)"
   1.149 +    by (simp add: ord_divides')
   1.150 +  hence "l dvd gcd (k * ord m (a ^ k)) (l * ord m (a ^ k))"
   1.151 +    by (intro gcd_greatest dvd_triv_left) (auto simp: l_def ord_divides')
   1.152 +  also have "gcd (k * ord m (a ^ k)) (l * ord m (a ^ k)) = ord m (a ^ k) * gcd k l"
   1.153 +    by (subst gcd_mult_distrib_nat) (auto simp: mult_ac)
   1.154 +  finally show "l dvd ord m (a ^ k) * gcd k l" .
   1.155 +qed
   1.156 +
   1.157 +theorem ord_power: "coprime m a \<Longrightarrow> ord m (a ^ k :: nat) = ord m a div gcd k (ord m a)"
   1.158 +  using ord_power_aux[of m a k] by (metis div_mult_self_is_m gcd_pos_nat ord_eq_0)
   1.159 +
   1.160 +lemma inj_power_mod:
   1.161 +  assumes "coprime n (a :: nat)"
   1.162 +  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<ord n a}"
   1.163 +proof
   1.164 +  fix k l assume *: "k \<in> {..<ord n a}" "l \<in> {..<ord n a}" "a ^ k mod n = a ^ l mod n"
   1.165 +  have "k = l" if "k < l" "l < ord n a" "[a ^ k = a ^ l] (mod n)" for k l
   1.166 +  proof -
   1.167 +    have "l = k + (l - k)" using that by simp
   1.168 +    also have "a ^ \<dots> = a ^ k * a ^ (l - k)"
   1.169 +      by (simp add: power_add)
   1.170 +    also have "[\<dots> = a ^ l * a ^ (l - k)] (mod n)"
   1.171 +      using that by (intro cong_mult) auto
   1.172 +    finally have "[a ^ l * a ^ (l - k) = a ^ l * 1] (mod n)"
   1.173 +      by (simp add: cong_sym_eq)
   1.174 +    with assms have "[a ^ (l - k) = 1] (mod n)"
   1.175 +      by (subst (asm) cong_mult_lcancel_nat) (auto simp: coprime_commute)
   1.176 +    hence "ord n a dvd l - k"
   1.177 +      by (simp add: ord_divides')
   1.178 +    from dvd_imp_le[OF this] and \<open>l < ord n a\<close> have "l - k = 0"
   1.179 +      by (cases "l - k = 0") auto
   1.180 +    with \<open>k < l\<close> show "k = l" by simp
   1.181 +  qed
   1.182 +  from this[of k l] and this[of l k] and * show "k = l"
   1.183 +    by (cases k l rule: linorder_cases) (auto simp: cong_def)
   1.184 +qed
   1.185 +
   1.186 +lemma ord_eq_2_iff: "ord n (x :: nat) = 2 \<longleftrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
   1.187 +proof
   1.188 +  assume x: "[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
   1.189 +  hence "coprime n x"
   1.190 +    by (metis coprime_commute lucas_coprime_lemma zero_neq_numeral)
   1.191 +  with x have "ord n x dvd 2" "ord n x \<noteq> 1" "ord n x > 0"
   1.192 +    by (auto simp: ord_divides' ord_eq_Suc_0_iff)
   1.193 +  thus "ord n x = 2" by (auto dest!: dvd_imp_le simp del: ord_gt_0_iff)
   1.194 +qed (use ord_divides[of _ 2] ord_divides[of _ 1] in auto)
   1.195 +
   1.196 +lemma square_mod_8_eq_1_iff: "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> odd (x :: nat)"
   1.197 +proof -
   1.198 +  have "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> ((x mod 8)\<^sup>2 mod 8 = 1)"
   1.199 +    by (simp add: power_mod cong_def)
   1.200 +  also have "\<dots> \<longleftrightarrow> x mod 8 \<in> {1, 3, 5, 7}"
   1.201 +  proof
   1.202 +    assume x: "(x mod 8)\<^sup>2 mod 8 = 1"
   1.203 +    have "x mod 8 \<in> {..<8}" by simp
   1.204 +    also have "{..<8} = {0, 1, 2, 3, 4, 5, 6, 7::nat}"
   1.205 +      by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
   1.206 +    finally have x_cases: "x mod 8 \<in> {0, 1, 2, 3, 4, 5, 6, 7}" .
   1.207 +    from x have "x mod 8 \<notin> {0, 2, 4, 6}"
   1.208 +      using x by (auto intro: Nat.gr0I)
   1.209 +    with x_cases show "x mod 8 \<in> {1, 3, 5, 7}" by simp
   1.210 +  qed auto
   1.211 +  also have "\<dots> \<longleftrightarrow> odd (x mod 8)"
   1.212 +    by (auto elim!: oddE)
   1.213 +  also have "\<dots> \<longleftrightarrow> odd x"
   1.214 +    by presburger
   1.215 +  finally show ?thesis .
   1.216 +qed
   1.217 +
   1.218 +lemma ord_twopow_aux:
   1.219 +  assumes "k \<ge> 3" and "odd (x :: nat)"
   1.220 +  shows   "[x ^ (2 ^ (k - 2)) = 1] (mod (2 ^ k))"
   1.221 +  using assms(1)
   1.222 +proof (induction k rule: dec_induct)
   1.223 +  case base
   1.224 +  from assms have "[x\<^sup>2 = 1] (mod 8)"
   1.225 +    by (subst square_mod_8_eq_1_iff) auto
   1.226 +  thus ?case by simp
   1.227 +next
   1.228 +  case (step k)
   1.229 +  define k' where "k' = k - 2"
   1.230 +  have k: "k = Suc (Suc k')"
   1.231 +    using \<open>k \<ge> 3\<close> by (simp add: k'_def)
   1.232 +  from \<open>k \<ge> 3\<close> have "2 * k \<ge> Suc k" by presburger
   1.233 +
   1.234 +  from \<open>odd x\<close> have "x > 0" by (intro Nat.gr0I) auto
   1.235 +  from step.IH have "2 ^ k dvd (x ^ (2 ^ (k - 2)) - 1)"
   1.236 +    by (rule cong_to_1_nat)
   1.237 +  then obtain t where "x ^ (2 ^ (k - 2)) - 1 = t * 2 ^ k"
   1.238 +    by auto
   1.239 +  hence "x ^ (2 ^ (k - 2)) = t * 2 ^ k + 1"
   1.240 +    by (metis \<open>0 < x\<close> add.commute add_diff_inverse_nat less_one neq0_conv power_eq_0_iff)
   1.241 +  hence "(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2"
   1.242 +    by (rule arg_cong)
   1.243 +  hence "[(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2] (mod (2 ^ Suc k))"
   1.244 +    by simp
   1.245 +  also have "(x ^ (2 ^ (k - 2))) ^ 2 = x ^ (2 ^ (k - 1))"
   1.246 +    by (simp_all add: power_even_eq[symmetric] power_mult k )
   1.247 +  also have "(t * 2 ^ k + 1) ^ 2 = t\<^sup>2 * 2 ^ (2 * k) + t * 2 ^ Suc k + 1"
   1.248 +    by (subst power2_eq_square)
   1.249 +       (auto simp: algebra_simps k power2_eq_square[of t]
   1.250 +                   power_even_eq[symmetric] power_add [symmetric])
   1.251 +  also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
   1.252 +    using \<open>2 * k \<ge> Suc k\<close>
   1.253 +    by (intro cong_add)
   1.254 +       (auto simp: cong_0_iff intro: dvd_mult[OF le_imp_power_dvd] simp del: power_Suc)
   1.255 +  finally show ?case by simp
   1.256 +qed
   1.257 +
   1.258 +lemma ord_twopow_3_5:
   1.259 +  assumes "k \<ge> 3" "x mod 8 \<in> {3, 5 :: nat}"
   1.260 +  shows   "ord (2 ^ k) x = 2 ^ (k - 2)"
   1.261 +  using assms(1)
   1.262 +proof (induction k rule: less_induct)
   1.263 +  have "x mod 8 = 3 \<or> x mod 8 = 5" using assms by auto
   1.264 +  hence "odd x" by presburger
   1.265 +  case (less k)
   1.266 +  from \<open>k \<ge> 3\<close> consider "k = 3" | "k = 4" | "k \<ge> 5" by force
   1.267 +  thus ?case
   1.268 +  proof cases
   1.269 +    case 1
   1.270 +    thus ?thesis using assms
   1.271 +      by (auto simp: ord_eq_2_iff cong_def simp flip: power_mod[of x])
   1.272 +  next
   1.273 +    case 2
   1.274 +    from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
   1.275 +    hence x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
   1.276 +      using mod_double_modulus[of 8 x] by auto
   1.277 +    hence "[x ^ 4 = 1] (mod 16)" using assms
   1.278 +      by (auto simp: cong_def simp flip: power_mod[of x])
   1.279 +    hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
   1.280 +    then obtain l where l: "ord 16 x = 2 ^ l" "l \<le> 2"
   1.281 +      by (subst (asm) divides_primepow_nat) auto
   1.282 +
   1.283 +    have "[x ^ 2 \<noteq> 1] (mod 16)"
   1.284 +      using x' by (auto simp: cong_def simp flip: power_mod[of x])
   1.285 +    hence "\<not>ord 16 x dvd 2" by (simp add: ord_divides')
   1.286 +    with l have "l = 2"
   1.287 +      using le_imp_power_dvd[of l 1 2] by (cases "l \<le> 1") auto
   1.288 +    with l show ?thesis by (simp add: \<open>k = 4\<close>)
   1.289 +  next
   1.290 +    case 3
   1.291 +    define k' where "k' = k - 2"
   1.292 +    have k': "k' \<ge> 2" and [simp]: "k = Suc (Suc k')"
   1.293 +      using 3 by (simp_all add: k'_def)
   1.294 +    have IH: "ord (2 ^ k') x = 2 ^ (k' - 2)" "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
   1.295 +      using less.IH[of k'] less.IH[of "Suc k'"] 3 by simp_all
   1.296 +    from IH have cong: "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ k'))"
   1.297 +      by (simp_all add: ord_divides')
   1.298 +    have notcong: "[x ^ (2 ^ (k' - 2)) \<noteq> 1] (mod (2 ^ Suc k'))"
   1.299 +    proof
   1.300 +      assume "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ Suc k'))"
   1.301 +      hence "ord (2 ^ Suc k') x dvd 2 ^ (k' - 2)"
   1.302 +        by (simp add: ord_divides')
   1.303 +      also have "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
   1.304 +        using IH by simp
   1.305 +      finally have "k' - 1 \<le> k' - 2"
   1.306 +        by (rule power_dvd_imp_le) auto
   1.307 +      with \<open>k' \<ge> 2\<close> show False by simp
   1.308 +    qed
   1.309 +
   1.310 +    have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
   1.311 +      using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
   1.312 +    with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
   1.313 +      using mod_double_modulus[of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
   1.314 +
   1.315 +    hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
   1.316 +           x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
   1.317 +      using mod_double_modulus[of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
   1.318 +    hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   1.319 +    proof
   1.320 +      assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
   1.321 +      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
   1.322 +        by simp
   1.323 +      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'] (mod 2 ^ k)"
   1.324 +        by (subst *) auto
   1.325 +      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
   1.326 +        by (rule cong_pow)
   1.327 +      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
   1.328 +        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
   1.329 +      also have "Suc (k' - 2) = k' - 1"
   1.330 +        using k' by simp
   1.331 +      also have "(1 + 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ (2 * k')"
   1.332 +        by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
   1.333 +      also have "(2 ^ k :: nat) dvd 2 ^ (2 * k')"
   1.334 +        using k' by (intro le_imp_power_dvd) auto
   1.335 +      hence "[1 + 2 ^ (k - 1) + 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + (0 :: nat)] (mod 2 ^ k)"
   1.336 +        by (intro cong_add) (auto simp: cong_0_iff)
   1.337 +      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   1.338 +        by simp
   1.339 +    next
   1.340 +      assume *: "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
   1.341 +      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
   1.342 +        by simp
   1.343 +      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 3 * 2 ^ k'] (mod 2 ^ k)"
   1.344 +        by (subst *) auto
   1.345 +      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
   1.346 +        by (rule cong_pow)
   1.347 +      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
   1.348 +        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
   1.349 +      also have "Suc (k' - 2) = k' - 1"
   1.350 +        using k' by simp
   1.351 +      also have "(1 + 3 * 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k')"
   1.352 +        by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
   1.353 +      also have "(2 ^ k :: nat) dvd 9 * 2 ^ (2 * k')"
   1.354 +        using k' by (intro dvd_mult le_imp_power_dvd) auto
   1.355 +      hence "[1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + 0 + (0 :: nat)]
   1.356 +               (mod 2 ^ k)"
   1.357 +        by (intro cong_add) (auto simp: cong_0_iff)
   1.358 +      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   1.359 +        by simp
   1.360 +    qed
   1.361 +
   1.362 +    have notcong': "[x ^ 2 ^ (k - 3) \<noteq> 1] (mod 2 ^ k)"
   1.363 +    proof
   1.364 +      assume "[x ^ 2 ^ (k - 3) = 1] (mod 2 ^ k)"
   1.365 +      hence "[x ^ 2 ^ (k' - 1) - x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1) - 1] (mod 2 ^ k)"
   1.366 +        by (intro cong_diff_nat eq) auto
   1.367 +      hence "[2 ^ (k - 1) = (0 :: nat)] (mod 2 ^ k)"
   1.368 +        by (simp add: cong_sym_eq)
   1.369 +      hence "2 ^ k dvd 2 ^ (k - 1)"
   1.370 +        by (simp add: cong_0_iff)
   1.371 +      hence "k \<le> k - 1"
   1.372 +        by (rule power_dvd_imp_le) auto
   1.373 +      thus False by simp
   1.374 +    qed
   1.375 +
   1.376 +    have "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
   1.377 +      using ord_twopow_aux[of k x] \<open>odd x\<close> \<open>k \<ge> 3\<close> by simp
   1.378 +    hence "ord (2 ^ k) x dvd 2 ^ (k - 2)"
   1.379 +      by (simp add: ord_divides')
   1.380 +    then obtain l where l: "l \<le> k - 2" "ord (2 ^ k) x = 2 ^ l"
   1.381 +      using divides_primepow_nat[of 2 "ord (2 ^ k) x" "k - 2"] by auto
   1.382 +
   1.383 +    from notcong' have "\<not>ord (2 ^ k) x dvd 2 ^ (k - 3)"
   1.384 +      by (simp add: ord_divides')
   1.385 +    with l have "l = k - 2"
   1.386 +      using le_imp_power_dvd[of l "k - 3" 2] by (cases "l \<le> k - 3") auto
   1.387 +    with l show ?thesis by simp
   1.388 +  qed
   1.389 +qed
   1.390 +
   1.391 +lemma ord_4_3 [simp]: "ord 4 (3::nat) = 2"
   1.392 +proof -
   1.393 +  have "[3 ^ 2 = (1 :: nat)] (mod 4)"
   1.394 +    by (simp add: cong_def)
   1.395 +  hence "ord 4 (3::nat) dvd 2"
   1.396 +    by (subst (asm) ord_divides) auto
   1.397 +  hence "ord 4 (3::nat) \<le> 2"
   1.398 +    by (intro dvd_imp_le) auto
   1.399 +  moreover have "ord 4 (3::nat) \<noteq> 1"
   1.400 +    by (auto simp: ord_eq_Suc_0_iff cong_def)
   1.401 +  moreover have "ord 4 (3::nat) \<noteq> 0"
   1.402 +    by (auto simp: gcd_non_0_nat coprime_iff_gcd_eq_1)
   1.403 +  ultimately show "ord 4 (3 :: nat) = 2"
   1.404 +    by linarith
   1.405 +qed
   1.406 +
   1.407 +lemma elements_with_ord_1: "n > 0 \<Longrightarrow> {x\<in>totatives n. ord n x = Suc 0} = {1}"
   1.408 +  by (auto simp: ord_eq_Suc_0_iff cong_def totatives_less)
   1.409 +
   1.410 +lemma residue_prime_has_primroot:
   1.411 +  fixes p :: nat
   1.412 +  assumes "prime p"
   1.413 +  shows "\<exists>a\<in>totatives p. ord p a = p - 1"
   1.414 +proof -
   1.415 +  from residue_prime_mult_group_has_gen[OF assms]
   1.416 +    obtain a where a: "a \<in> {1..p-1}" "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by blast
   1.417 +  from a have "coprime p a"
   1.418 +    using a assms by (intro prime_imp_coprime) (auto dest: dvd_imp_le)
   1.419 +  with a(1) have "a \<in> totatives p" by (auto simp: totatives_def coprime_commute)
   1.420 +
   1.421 +  have "p - 1 = card {1..p-1}" by simp
   1.422 +  also have "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by fact
   1.423 +  also have "{a ^ i mod p |i. i \<in> UNIV} = (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
   1.424 +  proof (intro equalityI subsetI)
   1.425 +    fix x assume "x \<in> {a ^ i mod p |i. i \<in> UNIV}"
   1.426 +    then obtain i where [simp]: "x = a ^ i mod p" by auto
   1.427 +
   1.428 +    have "[a ^ i = a ^ (i mod ord p a)] (mod p)"
   1.429 +      using \<open>coprime p a\<close> by (subst order_divides_expdiff) auto
   1.430 +    hence "\<exists>j. a ^ i mod p = a ^ j mod p \<and> j < ord p a"
   1.431 +      using \<open>coprime p a\<close> by (intro exI[of _ "i mod ord p a"]) (auto simp: cong_def)
   1.432 +    thus "x \<in> (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
   1.433 +      by auto
   1.434 +  qed auto
   1.435 +  also have "card \<dots> = ord p a"
   1.436 +    using inj_power_mod[OF \<open>coprime p a\<close>] by (subst card_image) auto
   1.437 +  finally show ?thesis using \<open>a \<in> totatives p\<close>
   1.438 +    by auto
   1.439 +qed
   1.440 +
   1.441 +
   1.442  
   1.443  subsection \<open>Another trivial primality characterization\<close>
   1.444