More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
authorManuel Eberl <eberlm@in.tum.de>
Mon Feb 04 12:16:03 2019 +0100 (3 months ago)
changeset 697859e326f6f8a24
parent 69784 24bbc4e30e5b
child 69786 a5732629cc46
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
CONTRIBUTORS
NEWS
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Number_Theory/Number_Theory.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Residue_Primitive_Roots.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/Totient.thy
src/HOL/Number_Theory/document/root.bib
src/HOL/Number_Theory/document/root.tex
     1.1 --- a/CONTRIBUTORS	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* February 2019: Manuel Eberl
     1.8 +  Carmichael's function, primitive roots in residue rings, more properties
     1.9 +  of the order in residue rings.
    1.10 +
    1.11  * January 2019: Andreas Lochbihler
    1.12    New implementation for case_of_simps based on Code_Lazy's
    1.13    pattern matching elimination algorithm.
     2.1 --- a/NEWS	Sat Feb 02 15:52:14 2019 +0100
     2.2 +++ b/NEWS	Mon Feb 04 12:16:03 2019 +0100
     2.3 @@ -87,6 +87,9 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* more material on residue rings in HOL-Number_Theory:
     2.8 +Carmichael's function, primitive roots, more properties for "ord"
     2.9 +
    2.10  * the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
    2.11  (not the corresponding binding operators) now have the same precedence
    2.12  as any other prefix function symbol.
     3.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Feb 02 15:52:14 2019 +0100
     3.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Mon Feb 04 12:16:03 2019 +0100
     3.3 @@ -136,7 +136,9 @@
     3.4   shows "n > 0 \<and> n \<le> p"
     3.5   using assms by (simp add: dvd_pos_nat dvd_imp_le)
     3.6  
     3.7 -(* Deviates from the definition given in the library in number theory *)
     3.8 +(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
     3.9 +   HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
    3.10 +   dependency. *)
    3.11  definition phi' :: "nat => nat"
    3.12    where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
    3.13  
     4.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Feb 02 15:52:14 2019 +0100
     4.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Feb 04 12:16:03 2019 +0100
     4.3 @@ -1290,6 +1290,11 @@
     4.4    with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
     4.5  qed (rule prime_factorization_cong)
     4.6  
     4.7 +lemma prime_factorization_eqI:
     4.8 +  assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n"
     4.9 +  shows   "prime_factorization n = P"
    4.10 +  using prime_factorization_prod_mset_primes[of P] assms by simp
    4.11 +
    4.12  lemma prime_factorization_mult:
    4.13    assumes "x \<noteq> 0" "y \<noteq> 0"
    4.14    shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
    4.15 @@ -1543,6 +1548,40 @@
    4.16    with \<open>m \<le> n\<close> show thesis ..
    4.17  qed
    4.18  
    4.19 +lemma divide_out_primepow_ex:
    4.20 +  assumes "n \<noteq> 0" "\<exists>p\<in>prime_factors n. P p"
    4.21 +  obtains p k n' where "P p" "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
    4.22 +proof -
    4.23 +  from assms obtain p where p: "P p" "prime p" "p dvd n"
    4.24 +    by auto
    4.25 +  define k where "k = multiplicity p n"
    4.26 +  define n' where "n' = n div p ^ k"
    4.27 +  have n': "n = p ^ k * n'" "\<not>p dvd n'"
    4.28 +    using assms p multiplicity_decompose[of n p]
    4.29 +    by (auto simp: n'_def k_def multiplicity_dvd)
    4.30 +  from n' p have "k > 0" by (intro Nat.gr0I) auto
    4.31 +  with n' p that[of p n' k] show ?thesis by auto
    4.32 +qed
    4.33 +
    4.34 +lemma divide_out_primepow:
    4.35 +  assumes "n \<noteq> 0" "\<not>is_unit n"
    4.36 +  obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
    4.37 +  using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms
    4.38 +        prime_factorsI by metis
    4.39 +  
    4.40 +lemma Ex_other_prime_factor:
    4.41 +  assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
    4.42 +  shows   "\<exists>q\<in>prime_factors n. q \<noteq> p"
    4.43 +proof (rule ccontr)
    4.44 +  assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
    4.45 +  have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
    4.46 +    using assms(1) by (intro prod_prime_factors [symmetric]) auto
    4.47 +  also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
    4.48 +    using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
    4.49 +  finally have "normalize n = p ^ multiplicity p n" by auto
    4.50 +  with assms show False by auto
    4.51 +qed
    4.52 +
    4.53  
    4.54  subsection \<open>GCD and LCM computation with unique factorizations\<close>
    4.55  
     5.1 --- a/src/HOL/Divides.thy	Sat Feb 02 15:52:14 2019 +0100
     5.2 +++ b/src/HOL/Divides.thy	Mon Feb 04 12:16:03 2019 +0100
     5.3 @@ -881,6 +881,21 @@
     5.4      by (simp_all add: div mod)
     5.5  qed
     5.6  
     5.7 +lemma mod_double_modulus:
     5.8 +  assumes "m > 0" "x \<ge> 0"
     5.9 +  shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
    5.10 +proof (cases "x mod (2 * m) < m")
    5.11 +  case True
    5.12 +  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
    5.13 +next
    5.14 +  case False
    5.15 +  hence *: "x mod (2 * m) - m = x mod m"
    5.16 +    using assms by (intro divmod_digit_1) auto
    5.17 +  hence "x mod (2 * m) = x mod m + m"
    5.18 +    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
    5.19 +  thus ?thesis by simp
    5.20 +qed
    5.21 +
    5.22  lemma fst_divmod:
    5.23    "fst (divmod m n) = numeral m div numeral n"
    5.24    by (simp add: divmod_def)
     6.1 --- a/src/HOL/GCD.thy	Sat Feb 02 15:52:14 2019 +0100
     6.2 +++ b/src/HOL/GCD.thy	Mon Feb 04 12:16:03 2019 +0100
     6.3 @@ -682,6 +682,12 @@
     6.4      by simp
     6.5  qed
     6.6  
     6.7 +lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
     6.8 +  by (simp add: gcd_dvdI1 gcd_dvdI2)
     6.9 +
    6.10 +lemma lcm_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> lcm a b dvd lcm c d"
    6.11 +  by (simp add: dvd_lcmI1 dvd_lcmI2)
    6.12 +
    6.13  lemma dvd_productE:
    6.14    assumes "p dvd a * b"
    6.15    obtains x y where "p = x * y" "x dvd a" "y dvd b"
    6.16 @@ -1081,6 +1087,29 @@
    6.17  lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
    6.18    by simp
    6.19  
    6.20 +lemma Gcd_mono:
    6.21 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
    6.22 +  shows   "(GCD x\<in>A. f x) dvd (GCD x\<in>A. g x)"
    6.23 +proof (intro Gcd_greatest, safe)
    6.24 +  fix x assume "x \<in> A"
    6.25 +  hence "(GCD x\<in>A. f x) dvd f x"
    6.26 +    by (intro Gcd_dvd) auto
    6.27 +  also have "f x dvd g x"
    6.28 +    using \<open>x \<in> A\<close> assms by blast
    6.29 +  finally show "(GCD x\<in>A. f x) dvd \<dots>" .
    6.30 +qed
    6.31 +
    6.32 +lemma Lcm_mono:
    6.33 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
    6.34 +  shows   "(LCM x\<in>A. f x) dvd (LCM x\<in>A. g x)"
    6.35 +proof (intro Lcm_least, safe)
    6.36 +  fix x assume "x \<in> A"
    6.37 +  hence "f x dvd g x" by (rule assms)
    6.38 +  also have "g x dvd (LCM x\<in>A. g x)"
    6.39 +    using \<open>x \<in> A\<close> by (intro dvd_Lcm) auto
    6.40 +  finally show "f x dvd \<dots>" .
    6.41 +qed
    6.42 +
    6.43  end
    6.44  
    6.45  
     7.1 --- a/src/HOL/Number_Theory/Number_Theory.thy	Sat Feb 02 15:52:14 2019 +0100
     7.2 +++ b/src/HOL/Number_Theory/Number_Theory.thy	Mon Feb 04 12:16:03 2019 +0100
     7.3 @@ -2,7 +2,14 @@
     7.4  section \<open>Comprehensive number theory\<close>
     7.5  
     7.6  theory Number_Theory
     7.7 -imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers
     7.8 +imports
     7.9 +  Fib
    7.10 +  Residues
    7.11 +  Eratosthenes
    7.12 +  Quadratic_Reciprocity
    7.13 +  Pocklington
    7.14 +  Prime_Powers
    7.15 +  Residue_Primitive_Roots
    7.16  begin
    7.17  
    7.18  end
     8.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Feb 02 15:52:14 2019 +0100
     8.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Feb 04 12:16:03 2019 +0100
     8.3 @@ -1,5 +1,5 @@
     8.4  (*  Title:      HOL/Number_Theory/Pocklington.thy
     8.5 -    Author:     Amine Chaieb
     8.6 +    Author:     Amine Chaieb, Manuel Eberl
     8.7  *)
     8.8  
     8.9  section \<open>Pocklington's Theorem for Primes\<close>
    8.10 @@ -270,7 +270,7 @@
    8.11  qed
    8.12  
    8.13  
    8.14 -subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
    8.15 +subsection \<open>Definition of the order of a number mod \<open>n\<close>\<close>
    8.16  
    8.17  definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
    8.18  
    8.19 @@ -439,6 +439,425 @@
    8.20    qed
    8.21  qed
    8.22  
    8.23 +lemma ord_not_coprime [simp]: "\<not>coprime n a \<Longrightarrow> ord n a = 0"
    8.24 +  by (simp add: ord_def)
    8.25 +
    8.26 +lemma ord_1 [simp]: "ord 1 n = 1"
    8.27 +proof -
    8.28 +  have "(LEAST k. k > 0) = (1 :: nat)"
    8.29 +    by (rule Least_equality) auto
    8.30 +  thus ?thesis by (simp add: ord_def)
    8.31 +qed
    8.32 +
    8.33 +lemma ord_1_right [simp]: "ord (n::nat) 1 = 1"
    8.34 +  using ord_divides[of 1 1 n] by simp
    8.35 +
    8.36 +lemma ord_Suc_0_right [simp]: "ord (n::nat) (Suc 0) = 1"
    8.37 +  using ord_divides[of 1 1 n] by simp
    8.38 +
    8.39 +lemma ord_0_nat [simp]: "ord 0 (n :: nat) = (if n = 1 then 1 else 0)"
    8.40 +proof -
    8.41 +  have "(LEAST k. k > 0) = (1 :: nat)"
    8.42 +    by (rule Least_equality) auto
    8.43 +  thus ?thesis by (auto simp: ord_def)
    8.44 +qed
    8.45 +
    8.46 +lemma ord_0_right_nat [simp]: "ord (n :: nat) 0 = (if n = 1 then 1 else 0)"
    8.47 +proof -
    8.48 +  have "(LEAST k. k > 0) = (1 :: nat)"
    8.49 +    by (rule Least_equality) auto
    8.50 +  thus ?thesis by (auto simp: ord_def)
    8.51 +qed
    8.52 +
    8.53 +lemma ord_divides': "[a ^ d = Suc 0] (mod n) = (ord n a dvd d)"
    8.54 +  using ord_divides[of a d n] by simp
    8.55 +
    8.56 +lemma ord_Suc_0 [simp]: "ord (Suc 0) n = 1"
    8.57 +  using ord_1[where 'a = nat] by (simp del: ord_1)
    8.58 +
    8.59 +lemma ord_mod [simp]: "ord n (k mod n) = ord n k"
    8.60 +  by (cases "n = 0") (auto simp add: ord_def cong_def power_mod)
    8.61 +
    8.62 +lemma ord_gt_0_iff [simp]: "ord (n::nat) x > 0 \<longleftrightarrow> coprime n x"
    8.63 +  using ord_eq_0[of n x] by auto
    8.64 +
    8.65 +lemma ord_eq_Suc_0_iff: "ord n (x::nat) = Suc 0 \<longleftrightarrow> [x = 1] (mod n)"
    8.66 +  using ord_divides[of x 1 n] by (auto simp: ord_divides')
    8.67 +
    8.68 +lemma ord_cong:
    8.69 +  assumes "[k1 = k2] (mod n)"
    8.70 +  shows   "ord n k1 = ord n k2"
    8.71 +proof -
    8.72 +  have "ord n (k1 mod n) = ord n (k2 mod n)"
    8.73 +    by (simp only: assms[unfolded cong_def])
    8.74 +  thus ?thesis by simp
    8.75 +qed
    8.76 +
    8.77 +lemma ord_nat_code [code_unfold]:
    8.78 +  "ord n a =
    8.79 +     (if n = 0 then if a = 1 then 1 else 0 else
    8.80 +        if coprime n a then Min (Set.filter (\<lambda>k. [a ^ k = 1] (mod n)) {0<..n}) else 0)"
    8.81 +proof (cases "coprime n a \<and> n > 0")
    8.82 +  case True
    8.83 +  define A where "A = {k\<in>{0<..n}. [a ^ k = 1] (mod n)}"
    8.84 +  define k where "k = (LEAST k. k > 0 \<and> [a ^ k = 1] (mod n))"
    8.85 +  have totient: "totient n \<in> A"
    8.86 +    using euler_theorem[of a n] True
    8.87 +    by (auto simp: A_def coprime_commute intro!: Nat.gr0I totient_le)
    8.88 +  moreover have "finite A" by (auto simp: A_def)
    8.89 +  ultimately have *: "Min A \<in> A" and "\<forall>y. y \<in> A \<longrightarrow> Min A \<le> y"
    8.90 +    by (auto intro: Min_in)
    8.91 +
    8.92 +  have "k > 0 \<and> [a ^ k = 1] (mod n)"
    8.93 +    unfolding k_def by (rule LeastI[of _ "totient n"]) (use totient in \<open>auto simp: A_def\<close>)
    8.94 +  moreover have "k \<le> totient n"
    8.95 +    unfolding k_def by (intro Least_le) (use totient in \<open>auto simp: A_def\<close>)
    8.96 +  ultimately have "k \<in> A" using totient_le[of n] by (auto simp: A_def)
    8.97 +  hence "Min A \<le> k" by (intro Min_le) (auto simp: \<open>finite A\<close>)
    8.98 +  moreover from * have "k \<le> Min A"
    8.99 +    unfolding k_def by (intro Least_le) (auto simp: A_def)
   8.100 +  ultimately show ?thesis using True by (simp add: ord_def k_def A_def Set.filter_def)
   8.101 +qed auto
   8.102 +
   8.103 +theorem ord_modulus_mult_coprime:
   8.104 +  fixes x :: nat
   8.105 +  assumes "coprime m n"
   8.106 +  shows   "ord (m * n) x = lcm (ord m x) (ord n x)"
   8.107 +proof (intro dvd_antisym)
   8.108 +  have "[x ^ lcm (ord m x) (ord n x) = 1] (mod (m * n))"
   8.109 +    using assms by (intro coprime_cong_mult_nat assms) (auto simp: ord_divides')
   8.110 +  thus "ord (m * n) x dvd lcm (ord m x) (ord n x)"
   8.111 +    by (simp add: ord_divides')
   8.112 +next
   8.113 +  show "lcm (ord m x) (ord n x) dvd ord (m * n) x"
   8.114 +  proof (intro lcm_least)
   8.115 +    show "ord m x dvd ord (m * n) x"
   8.116 +      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 m n] assms
   8.117 +      by (simp add: ord_divides')
   8.118 +    show "ord n x dvd ord (m * n) x"
   8.119 +      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 n m] assms
   8.120 +      by (simp add: ord_divides' mult.commute)
   8.121 +  qed
   8.122 +qed
   8.123 +
   8.124 +corollary ord_modulus_prod_coprime:
   8.125 +  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
   8.126 +  shows   "ord (\<Prod>i\<in>A. f i :: nat) x = (LCM i\<in>A. ord (f i) x)"
   8.127 +  using assms by (induction A rule: finite_induct)
   8.128 +                 (simp, simp, subst ord_modulus_mult_coprime, auto intro!: prod_coprime_right)
   8.129 +
   8.130 +lemma ord_power_aux:
   8.131 +  fixes m x k a :: nat
   8.132 +  defines "l \<equiv> ord m a"
   8.133 +  shows   "ord m (a ^ k) * gcd k l = l"
   8.134 +proof (rule dvd_antisym)
   8.135 +  have "[a ^ lcm k l = 1] (mod m)"
   8.136 +    unfolding ord_divides by (simp add: l_def)
   8.137 +  also have "lcm k l = k * (l div gcd k l)"
   8.138 +    by (simp add: lcm_nat_def div_mult_swap)
   8.139 +  finally have "ord m (a ^ k) dvd l div gcd k l"
   8.140 +    unfolding ord_divides [symmetric] by (simp add: power_mult [symmetric])
   8.141 +  thus "ord m (a ^ k) * gcd k l dvd l"
   8.142 +    by (cases "l = 0") (auto simp: dvd_div_iff_mult)
   8.143 +
   8.144 +  have "[(a ^ k) ^ ord m (a ^ k) = 1] (mod m)"
   8.145 +    by (rule ord)
   8.146 +  also have "(a ^ k) ^ ord m (a ^ k) = a ^ (k * ord m (a ^ k))"
   8.147 +    by (simp add: power_mult)
   8.148 +  finally have "ord m a dvd k * ord m (a ^ k)"
   8.149 +    by (simp add: ord_divides')
   8.150 +  hence "l dvd gcd (k * ord m (a ^ k)) (l * ord m (a ^ k))"
   8.151 +    by (intro gcd_greatest dvd_triv_left) (auto simp: l_def ord_divides')
   8.152 +  also have "gcd (k * ord m (a ^ k)) (l * ord m (a ^ k)) = ord m (a ^ k) * gcd k l"
   8.153 +    by (subst gcd_mult_distrib_nat) (auto simp: mult_ac)
   8.154 +  finally show "l dvd ord m (a ^ k) * gcd k l" .
   8.155 +qed
   8.156 +
   8.157 +theorem ord_power: "coprime m a \<Longrightarrow> ord m (a ^ k :: nat) = ord m a div gcd k (ord m a)"
   8.158 +  using ord_power_aux[of m a k] by (metis div_mult_self_is_m gcd_pos_nat ord_eq_0)
   8.159 +
   8.160 +lemma inj_power_mod:
   8.161 +  assumes "coprime n (a :: nat)"
   8.162 +  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<ord n a}"
   8.163 +proof
   8.164 +  fix k l assume *: "k \<in> {..<ord n a}" "l \<in> {..<ord n a}" "a ^ k mod n = a ^ l mod n"
   8.165 +  have "k = l" if "k < l" "l < ord n a" "[a ^ k = a ^ l] (mod n)" for k l
   8.166 +  proof -
   8.167 +    have "l = k + (l - k)" using that by simp
   8.168 +    also have "a ^ \<dots> = a ^ k * a ^ (l - k)"
   8.169 +      by (simp add: power_add)
   8.170 +    also have "[\<dots> = a ^ l * a ^ (l - k)] (mod n)"
   8.171 +      using that by (intro cong_mult) auto
   8.172 +    finally have "[a ^ l * a ^ (l - k) = a ^ l * 1] (mod n)"
   8.173 +      by (simp add: cong_sym_eq)
   8.174 +    with assms have "[a ^ (l - k) = 1] (mod n)"
   8.175 +      by (subst (asm) cong_mult_lcancel_nat) (auto simp: coprime_commute)
   8.176 +    hence "ord n a dvd l - k"
   8.177 +      by (simp add: ord_divides')
   8.178 +    from dvd_imp_le[OF this] and \<open>l < ord n a\<close> have "l - k = 0"
   8.179 +      by (cases "l - k = 0") auto
   8.180 +    with \<open>k < l\<close> show "k = l" by simp
   8.181 +  qed
   8.182 +  from this[of k l] and this[of l k] and * show "k = l"
   8.183 +    by (cases k l rule: linorder_cases) (auto simp: cong_def)
   8.184 +qed
   8.185 +
   8.186 +lemma ord_eq_2_iff: "ord n (x :: nat) = 2 \<longleftrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
   8.187 +proof
   8.188 +  assume x: "[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
   8.189 +  hence "coprime n x"
   8.190 +    by (metis coprime_commute lucas_coprime_lemma zero_neq_numeral)
   8.191 +  with x have "ord n x dvd 2" "ord n x \<noteq> 1" "ord n x > 0"
   8.192 +    by (auto simp: ord_divides' ord_eq_Suc_0_iff)
   8.193 +  thus "ord n x = 2" by (auto dest!: dvd_imp_le simp del: ord_gt_0_iff)
   8.194 +qed (use ord_divides[of _ 2] ord_divides[of _ 1] in auto)
   8.195 +
   8.196 +lemma square_mod_8_eq_1_iff: "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> odd (x :: nat)"
   8.197 +proof -
   8.198 +  have "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> ((x mod 8)\<^sup>2 mod 8 = 1)"
   8.199 +    by (simp add: power_mod cong_def)
   8.200 +  also have "\<dots> \<longleftrightarrow> x mod 8 \<in> {1, 3, 5, 7}"
   8.201 +  proof
   8.202 +    assume x: "(x mod 8)\<^sup>2 mod 8 = 1"
   8.203 +    have "x mod 8 \<in> {..<8}" by simp
   8.204 +    also have "{..<8} = {0, 1, 2, 3, 4, 5, 6, 7::nat}"
   8.205 +      by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
   8.206 +    finally have x_cases: "x mod 8 \<in> {0, 1, 2, 3, 4, 5, 6, 7}" .
   8.207 +    from x have "x mod 8 \<notin> {0, 2, 4, 6}"
   8.208 +      using x by (auto intro: Nat.gr0I)
   8.209 +    with x_cases show "x mod 8 \<in> {1, 3, 5, 7}" by simp
   8.210 +  qed auto
   8.211 +  also have "\<dots> \<longleftrightarrow> odd (x mod 8)"
   8.212 +    by (auto elim!: oddE)
   8.213 +  also have "\<dots> \<longleftrightarrow> odd x"
   8.214 +    by presburger
   8.215 +  finally show ?thesis .
   8.216 +qed
   8.217 +
   8.218 +lemma ord_twopow_aux:
   8.219 +  assumes "k \<ge> 3" and "odd (x :: nat)"
   8.220 +  shows   "[x ^ (2 ^ (k - 2)) = 1] (mod (2 ^ k))"
   8.221 +  using assms(1)
   8.222 +proof (induction k rule: dec_induct)
   8.223 +  case base
   8.224 +  from assms have "[x\<^sup>2 = 1] (mod 8)"
   8.225 +    by (subst square_mod_8_eq_1_iff) auto
   8.226 +  thus ?case by simp
   8.227 +next
   8.228 +  case (step k)
   8.229 +  define k' where "k' = k - 2"
   8.230 +  have k: "k = Suc (Suc k')"
   8.231 +    using \<open>k \<ge> 3\<close> by (simp add: k'_def)
   8.232 +  from \<open>k \<ge> 3\<close> have "2 * k \<ge> Suc k" by presburger
   8.233 +
   8.234 +  from \<open>odd x\<close> have "x > 0" by (intro Nat.gr0I) auto
   8.235 +  from step.IH have "2 ^ k dvd (x ^ (2 ^ (k - 2)) - 1)"
   8.236 +    by (rule cong_to_1_nat)
   8.237 +  then obtain t where "x ^ (2 ^ (k - 2)) - 1 = t * 2 ^ k"
   8.238 +    by auto
   8.239 +  hence "x ^ (2 ^ (k - 2)) = t * 2 ^ k + 1"
   8.240 +    by (metis \<open>0 < x\<close> add.commute add_diff_inverse_nat less_one neq0_conv power_eq_0_iff)
   8.241 +  hence "(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2"
   8.242 +    by (rule arg_cong)
   8.243 +  hence "[(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2] (mod (2 ^ Suc k))"
   8.244 +    by simp
   8.245 +  also have "(x ^ (2 ^ (k - 2))) ^ 2 = x ^ (2 ^ (k - 1))"
   8.246 +    by (simp_all add: power_even_eq[symmetric] power_mult k )
   8.247 +  also have "(t * 2 ^ k + 1) ^ 2 = t\<^sup>2 * 2 ^ (2 * k) + t * 2 ^ Suc k + 1"
   8.248 +    by (subst power2_eq_square)
   8.249 +       (auto simp: algebra_simps k power2_eq_square[of t]
   8.250 +                   power_even_eq[symmetric] power_add [symmetric])
   8.251 +  also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
   8.252 +    using \<open>2 * k \<ge> Suc k\<close>
   8.253 +    by (intro cong_add)
   8.254 +       (auto simp: cong_0_iff intro: dvd_mult[OF le_imp_power_dvd] simp del: power_Suc)
   8.255 +  finally show ?case by simp
   8.256 +qed
   8.257 +
   8.258 +lemma ord_twopow_3_5:
   8.259 +  assumes "k \<ge> 3" "x mod 8 \<in> {3, 5 :: nat}"
   8.260 +  shows   "ord (2 ^ k) x = 2 ^ (k - 2)"
   8.261 +  using assms(1)
   8.262 +proof (induction k rule: less_induct)
   8.263 +  have "x mod 8 = 3 \<or> x mod 8 = 5" using assms by auto
   8.264 +  hence "odd x" by presburger
   8.265 +  case (less k)
   8.266 +  from \<open>k \<ge> 3\<close> consider "k = 3" | "k = 4" | "k \<ge> 5" by force
   8.267 +  thus ?case
   8.268 +  proof cases
   8.269 +    case 1
   8.270 +    thus ?thesis using assms
   8.271 +      by (auto simp: ord_eq_2_iff cong_def simp flip: power_mod[of x])
   8.272 +  next
   8.273 +    case 2
   8.274 +    from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
   8.275 +    hence x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
   8.276 +      using mod_double_modulus[of 8 x] by auto
   8.277 +    hence "[x ^ 4 = 1] (mod 16)" using assms
   8.278 +      by (auto simp: cong_def simp flip: power_mod[of x])
   8.279 +    hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
   8.280 +    then obtain l where l: "ord 16 x = 2 ^ l" "l \<le> 2"
   8.281 +      by (subst (asm) divides_primepow_nat) auto
   8.282 +
   8.283 +    have "[x ^ 2 \<noteq> 1] (mod 16)"
   8.284 +      using x' by (auto simp: cong_def simp flip: power_mod[of x])
   8.285 +    hence "\<not>ord 16 x dvd 2" by (simp add: ord_divides')
   8.286 +    with l have "l = 2"
   8.287 +      using le_imp_power_dvd[of l 1 2] by (cases "l \<le> 1") auto
   8.288 +    with l show ?thesis by (simp add: \<open>k = 4\<close>)
   8.289 +  next
   8.290 +    case 3
   8.291 +    define k' where "k' = k - 2"
   8.292 +    have k': "k' \<ge> 2" and [simp]: "k = Suc (Suc k')"
   8.293 +      using 3 by (simp_all add: k'_def)
   8.294 +    have IH: "ord (2 ^ k') x = 2 ^ (k' - 2)" "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
   8.295 +      using less.IH[of k'] less.IH[of "Suc k'"] 3 by simp_all
   8.296 +    from IH have cong: "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ k'))"
   8.297 +      by (simp_all add: ord_divides')
   8.298 +    have notcong: "[x ^ (2 ^ (k' - 2)) \<noteq> 1] (mod (2 ^ Suc k'))"
   8.299 +    proof
   8.300 +      assume "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ Suc k'))"
   8.301 +      hence "ord (2 ^ Suc k') x dvd 2 ^ (k' - 2)"
   8.302 +        by (simp add: ord_divides')
   8.303 +      also have "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
   8.304 +        using IH by simp
   8.305 +      finally have "k' - 1 \<le> k' - 2"
   8.306 +        by (rule power_dvd_imp_le) auto
   8.307 +      with \<open>k' \<ge> 2\<close> show False by simp
   8.308 +    qed
   8.309 +
   8.310 +    have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
   8.311 +      using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
   8.312 +    with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
   8.313 +      using mod_double_modulus[of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
   8.314 +
   8.315 +    hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
   8.316 +           x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
   8.317 +      using mod_double_modulus[of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
   8.318 +    hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   8.319 +    proof
   8.320 +      assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
   8.321 +      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
   8.322 +        by simp
   8.323 +      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'] (mod 2 ^ k)"
   8.324 +        by (subst *) auto
   8.325 +      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
   8.326 +        by (rule cong_pow)
   8.327 +      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
   8.328 +        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
   8.329 +      also have "Suc (k' - 2) = k' - 1"
   8.330 +        using k' by simp
   8.331 +      also have "(1 + 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ (2 * k')"
   8.332 +        by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
   8.333 +      also have "(2 ^ k :: nat) dvd 2 ^ (2 * k')"
   8.334 +        using k' by (intro le_imp_power_dvd) auto
   8.335 +      hence "[1 + 2 ^ (k - 1) + 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + (0 :: nat)] (mod 2 ^ k)"
   8.336 +        by (intro cong_add) (auto simp: cong_0_iff)
   8.337 +      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   8.338 +        by simp
   8.339 +    next
   8.340 +      assume *: "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
   8.341 +      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
   8.342 +        by simp
   8.343 +      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 3 * 2 ^ k'] (mod 2 ^ k)"
   8.344 +        by (subst *) auto
   8.345 +      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
   8.346 +        by (rule cong_pow)
   8.347 +      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
   8.348 +        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
   8.349 +      also have "Suc (k' - 2) = k' - 1"
   8.350 +        using k' by simp
   8.351 +      also have "(1 + 3 * 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k')"
   8.352 +        by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
   8.353 +      also have "(2 ^ k :: nat) dvd 9 * 2 ^ (2 * k')"
   8.354 +        using k' by (intro dvd_mult le_imp_power_dvd) auto
   8.355 +      hence "[1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + 0 + (0 :: nat)]
   8.356 +               (mod 2 ^ k)"
   8.357 +        by (intro cong_add) (auto simp: cong_0_iff)
   8.358 +      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
   8.359 +        by simp
   8.360 +    qed
   8.361 +
   8.362 +    have notcong': "[x ^ 2 ^ (k - 3) \<noteq> 1] (mod 2 ^ k)"
   8.363 +    proof
   8.364 +      assume "[x ^ 2 ^ (k - 3) = 1] (mod 2 ^ k)"
   8.365 +      hence "[x ^ 2 ^ (k' - 1) - x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1) - 1] (mod 2 ^ k)"
   8.366 +        by (intro cong_diff_nat eq) auto
   8.367 +      hence "[2 ^ (k - 1) = (0 :: nat)] (mod 2 ^ k)"
   8.368 +        by (simp add: cong_sym_eq)
   8.369 +      hence "2 ^ k dvd 2 ^ (k - 1)"
   8.370 +        by (simp add: cong_0_iff)
   8.371 +      hence "k \<le> k - 1"
   8.372 +        by (rule power_dvd_imp_le) auto
   8.373 +      thus False by simp
   8.374 +    qed
   8.375 +
   8.376 +    have "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
   8.377 +      using ord_twopow_aux[of k x] \<open>odd x\<close> \<open>k \<ge> 3\<close> by simp
   8.378 +    hence "ord (2 ^ k) x dvd 2 ^ (k - 2)"
   8.379 +      by (simp add: ord_divides')
   8.380 +    then obtain l where l: "l \<le> k - 2" "ord (2 ^ k) x = 2 ^ l"
   8.381 +      using divides_primepow_nat[of 2 "ord (2 ^ k) x" "k - 2"] by auto
   8.382 +
   8.383 +    from notcong' have "\<not>ord (2 ^ k) x dvd 2 ^ (k - 3)"
   8.384 +      by (simp add: ord_divides')
   8.385 +    with l have "l = k - 2"
   8.386 +      using le_imp_power_dvd[of l "k - 3" 2] by (cases "l \<le> k - 3") auto
   8.387 +    with l show ?thesis by simp
   8.388 +  qed
   8.389 +qed
   8.390 +
   8.391 +lemma ord_4_3 [simp]: "ord 4 (3::nat) = 2"
   8.392 +proof -
   8.393 +  have "[3 ^ 2 = (1 :: nat)] (mod 4)"
   8.394 +    by (simp add: cong_def)
   8.395 +  hence "ord 4 (3::nat) dvd 2"
   8.396 +    by (subst (asm) ord_divides) auto
   8.397 +  hence "ord 4 (3::nat) \<le> 2"
   8.398 +    by (intro dvd_imp_le) auto
   8.399 +  moreover have "ord 4 (3::nat) \<noteq> 1"
   8.400 +    by (auto simp: ord_eq_Suc_0_iff cong_def)
   8.401 +  moreover have "ord 4 (3::nat) \<noteq> 0"
   8.402 +    by (auto simp: gcd_non_0_nat coprime_iff_gcd_eq_1)
   8.403 +  ultimately show "ord 4 (3 :: nat) = 2"
   8.404 +    by linarith
   8.405 +qed
   8.406 +
   8.407 +lemma elements_with_ord_1: "n > 0 \<Longrightarrow> {x\<in>totatives n. ord n x = Suc 0} = {1}"
   8.408 +  by (auto simp: ord_eq_Suc_0_iff cong_def totatives_less)
   8.409 +
   8.410 +lemma residue_prime_has_primroot:
   8.411 +  fixes p :: nat
   8.412 +  assumes "prime p"
   8.413 +  shows "\<exists>a\<in>totatives p. ord p a = p - 1"
   8.414 +proof -
   8.415 +  from residue_prime_mult_group_has_gen[OF assms]
   8.416 +    obtain a where a: "a \<in> {1..p-1}" "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by blast
   8.417 +  from a have "coprime p a"
   8.418 +    using a assms by (intro prime_imp_coprime) (auto dest: dvd_imp_le)
   8.419 +  with a(1) have "a \<in> totatives p" by (auto simp: totatives_def coprime_commute)
   8.420 +
   8.421 +  have "p - 1 = card {1..p-1}" by simp
   8.422 +  also have "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by fact
   8.423 +  also have "{a ^ i mod p |i. i \<in> UNIV} = (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
   8.424 +  proof (intro equalityI subsetI)
   8.425 +    fix x assume "x \<in> {a ^ i mod p |i. i \<in> UNIV}"
   8.426 +    then obtain i where [simp]: "x = a ^ i mod p" by auto
   8.427 +
   8.428 +    have "[a ^ i = a ^ (i mod ord p a)] (mod p)"
   8.429 +      using \<open>coprime p a\<close> by (subst order_divides_expdiff) auto
   8.430 +    hence "\<exists>j. a ^ i mod p = a ^ j mod p \<and> j < ord p a"
   8.431 +      using \<open>coprime p a\<close> by (intro exI[of _ "i mod ord p a"]) (auto simp: cong_def)
   8.432 +    thus "x \<in> (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
   8.433 +      by auto
   8.434 +  qed auto
   8.435 +  also have "card \<dots> = ord p a"
   8.436 +    using inj_power_mod[OF \<open>coprime p a\<close>] by (subst card_image) auto
   8.437 +  finally show ?thesis using \<open>a \<in> totatives p\<close>
   8.438 +    by auto
   8.439 +qed
   8.440 +
   8.441 +
   8.442  
   8.443  subsection \<open>Another trivial primality characterization\<close>
   8.444  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Mon Feb 04 12:16:03 2019 +0100
     9.3 @@ -0,0 +1,1152 @@
     9.4 +(*
     9.5 +  File:      HOL/Number_Theory/Residue_Primitive_Roots.thy
     9.6 +  Author:    Manuel Eberl
     9.7 +
     9.8 +  Primitive roots in residue rings: Definition and existence criteria
     9.9 +*)
    9.10 +section \<open>Primitive roots in residue rings and Carmichael's function\<close>
    9.11 +theory Residue_Primitive_Roots
    9.12 +  imports Pocklington
    9.13 +begin
    9.14 +
    9.15 +text \<open>
    9.16 +  This theory develops the notions of primitive roots (generators) in residue rings. It also
    9.17 +  provides a definition and all the basic properties of Carmichael's function $\lambda(n)$, which
    9.18 +  is strongly related to this. The proofs mostly follow Apostol's presentation
    9.19 +\<close>
    9.20 +
    9.21 +subsection \<open>Primitive roots in residue rings\<close>
    9.22 +
    9.23 +text \<open>
    9.24 +  A primitive root of a residue ring modulo \<open>n\<close> is an element \<open>g\<close> that \<^emph>\<open>generates\<close> the
    9.25 +  ring, i.\,e.\ such that for each \<open>x\<close> coprime to \<open>n\<close> there exists an \<open>i\<close> such that $x = g^i$.
    9.26 +  A simpler definition is that \<open>g\<close> must have the same order as the cardinality of the
    9.27 +  multiplicative group, which is $\varphi(n)$.
    9.28 +
    9.29 +  Note that for convenience, this definition does \<^emph>\<open>not\<close> demand \<open>g < n\<close>.
    9.30 +\<close>
    9.31 +inductive residue_primroot :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    9.32 +  "n > 0 \<Longrightarrow> coprime n g \<Longrightarrow> ord n g = totient n \<Longrightarrow> residue_primroot n g"
    9.33 +
    9.34 +lemma residue_primroot_def [code]:
    9.35 +  "residue_primroot n x \<longleftrightarrow> n > 0 \<and> coprime n x \<and> ord n x = totient n"
    9.36 +  by (simp add: residue_primroot.simps)
    9.37 +
    9.38 +lemma not_residue_primroot_0 [simp]: "~residue_primroot 0 x"
    9.39 +  by (auto simp: residue_primroot_def)
    9.40 +
    9.41 +lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
    9.42 +  by (cases "n = 0") (simp_all add: residue_primroot_def)
    9.43 +
    9.44 +lemma residue_primroot_cong:
    9.45 +  assumes "[x = x'] (mod n)"
    9.46 +  shows   "residue_primroot n x = residue_primroot n x'"
    9.47 +proof -
    9.48 +  have "residue_primroot n x = residue_primroot n (x mod n)"
    9.49 +    by simp
    9.50 +  also have "x mod n = x' mod n"
    9.51 +    using assms by (simp add: cong_def)
    9.52 +  also have "residue_primroot n (x' mod n) = residue_primroot n x'"
    9.53 +    by simp
    9.54 +  finally show ?thesis .
    9.55 +qed
    9.56 +
    9.57 +lemma not_residue_primroot_0_right [simp]: "residue_primroot n 0 \<longleftrightarrow> n = 1"
    9.58 +  by (auto simp: residue_primroot_def)
    9.59 +
    9.60 +lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
    9.61 +proof
    9.62 +  assume *: "residue_primroot n (Suc 0)"
    9.63 +  with totient_gt_1[of n] have "n \<le> 2" by (cases "n \<le> 2") (auto simp: residue_primroot_def)
    9.64 +  hence "n \<in> {0, 1, 2}" by auto
    9.65 +  thus "n \<in> {1, 2}" using * by (auto simp: residue_primroot_def)
    9.66 +qed (auto simp: residue_primroot_def)
    9.67 +
    9.68 +
    9.69 +subsection \<open>Primitive roots modulo a prime\<close>
    9.70 +
    9.71 +text \<open>
    9.72 +  For prime \<open>p\<close>, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$
    9.73 +  whose order is precisely \<open>d\<close> for each \<open>d\<close>.
    9.74 +\<close>
    9.75 +context
    9.76 +  fixes n :: nat and \<psi>
    9.77 +  assumes n: "n > 1"
    9.78 +  defines "\<psi> \<equiv> (\<lambda>d. card {x\<in>totatives n. ord n x = d})"
    9.79 +begin
    9.80 +
    9.81 +lemma elements_with_ord_restrict_totatives:
    9.82 +  "d > 0 \<Longrightarrow> {x\<in>{..<n}. ord n x = d} = {x\<in>totatives n. ord n x = d}"
    9.83 +  using n by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I le_neq_trans)
    9.84 +
    9.85 +lemma prime_elements_with_ord:
    9.86 +  assumes "\<psi> d \<noteq> 0" and "prime n"
    9.87 +      and a: "a \<in> totatives n" "ord n a = d" "a \<noteq> 1"
    9.88 +  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    9.89 +    and   "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}"
    9.90 +    and   "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
    9.91 +proof -
    9.92 +  show inj: "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    9.93 +    using inj_power_mod[of n a] a by (auto simp: totatives_def coprime_commute)
    9.94 +  from a have "d > 0" by (auto simp: totatives_def coprime_commute)
    9.95 +  moreover have "d \<noteq> 1" using a n
    9.96 +    by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def)
    9.97 +  ultimately have d: "d > 1" by simp
    9.98 +
    9.99 +  have *: "(\<lambda>k. a ^ k mod n) ` {..<d} = {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
   9.100 +  proof (rule card_seteq)
   9.101 +    have "card {x\<in>{..<n}. [x ^ d = 1] (mod n)} \<le> d"
   9.102 +      using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute)
   9.103 +    also have "\<dots> = card ((\<lambda>k. a ^ k mod n) ` {..<d})"
   9.104 +      using inj by (subst card_image) auto
   9.105 +    finally show "card {x \<in> {..<n}. [x ^ d = 1] (mod n)} \<le> \<dots>" .
   9.106 +  next
   9.107 +    show "(\<lambda>k. a ^ k mod n) ` {..<d} \<subseteq> {x \<in> {..<n}. [x ^ d = 1] (mod n)}"
   9.108 +    proof safe
   9.109 +      fix k assume "k < d"
   9.110 +      have "[(a ^ d) ^ k = 1 ^ k] (mod n)"
   9.111 +        by (intro cong_pow) (use a in \<open>auto simp: ord_divides'\<close>)
   9.112 +      thus "[(a ^ k mod n) ^ d = 1] (mod n)"
   9.113 +        by (simp add: power_mult [symmetric] cong_def power_mod mult.commute)
   9.114 +    qed (use \<open>prime n\<close> in \<open>auto dest: prime_gt_1_nat\<close>)
   9.115 +  qed auto
   9.116 +  thus "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}" ..
   9.117 +
   9.118 +  show "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
   9.119 +    unfolding bij_betw_def
   9.120 +  proof (intro conjI inj_on_subset[OF inj] equalityI subsetI)
   9.121 +    fix b assume "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d"
   9.122 +    then obtain k where "b = a ^ k mod n" "k \<in> totatives d" by auto
   9.123 +    thus "b \<in> {b \<in> {..<n}. ord n b = d}"
   9.124 +      using n a by (simp add: ord_power totatives_def coprime_commute)
   9.125 +  next
   9.126 +    fix b assume "b \<in> {x \<in> {..<n}. ord n x = d}"
   9.127 +    hence b: "ord n b = d" "b < n" by auto
   9.128 +    with d have "coprime n b" using ord_eq_0[of n b] by auto
   9.129 +    from b have "b \<in> {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
   9.130 +      by (auto simp: ord_divides')
   9.131 +    with * obtain k where k: "k < d" "b = a ^ k mod n"
   9.132 +      by blast
   9.133 +    with b(2) n a d have "d div gcd k d = ord n b"
   9.134 +      using \<open>coprime n b\<close> by (auto simp: ord_power)
   9.135 +    also have "ord n b = d" by (simp add: b)
   9.136 +    finally have "coprime k d"
   9.137 +      unfolding coprime_iff_gcd_eq_1 using d a by (subst (asm) div_eq_dividend_iff) auto
   9.138 +    with k b d have "k \<in> totatives d" by (auto simp: totatives_def intro!: Nat.gr0I)
   9.139 +    with k show "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d" by blast
   9.140 +  qed (use d n in \<open>auto simp: totatives_less\<close>)
   9.141 +qed
   9.142 +
   9.143 +lemma prime_card_elements_with_ord:
   9.144 +  assumes "\<psi> d \<noteq> 0" and "prime n"
   9.145 +  shows   "\<psi> d = totient d"
   9.146 +proof (cases "d = 1")
   9.147 +  case True
   9.148 +  have "\<psi> 1 = 1"
   9.149 +    using elements_with_ord_1[of n] n by (simp add: \<psi>_def)
   9.150 +  thus ?thesis using True by simp
   9.151 +next
   9.152 +  case False
   9.153 +  from assms obtain a where a: "a \<in> totatives n" "ord n a = d"
   9.154 +    by (auto simp: \<psi>_def)
   9.155 +  from a have "d > 0" by (auto intro!: Nat.gr0I simp: ord_eq_0 totatives_def coprime_commute)
   9.156 +  from a and False have "a \<noteq> 1" by auto
   9.157 +  from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "\<psi> d = totient d"
   9.158 +    using elements_with_ord_restrict_totatives[of d] False a \<open>d > 0\<close>
   9.159 +    by (simp add: \<psi>_def totient_def)
   9.160 +qed
   9.161 +
   9.162 +lemma prime_sum_card_elements_with_ord_eq_totient:
   9.163 +  "(\<Sum>d | d dvd totient n. \<psi> d) = totient n"
   9.164 +proof -
   9.165 +  have "totient n = card (totatives n)"
   9.166 +    by (simp add: totient_def)
   9.167 +  also have "totatives n = (\<Union>d\<in>{d. d dvd totient n}. {x\<in>totatives n. ord n x = d})"
   9.168 +    by (force simp: order_divides_totient totatives_def coprime_commute)
   9.169 +  also have "card \<dots> = (\<Sum>d | d dvd totient n. \<psi> d)"
   9.170 +    unfolding \<psi>_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat)
   9.171 +  finally show ?thesis ..
   9.172 +qed
   9.173 +
   9.174 +text \<open>
   9.175 +  We can now show that the number of elements of order \<open>d\<close> is $\varphi(d)$ if $d\mid p - 1$
   9.176 +  and 0 otherwise.
   9.177 +\<close>
   9.178 +theorem prime_card_elements_with_ord_eq_totient:
   9.179 +  assumes "prime n"
   9.180 +  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
   9.181 +proof (cases "d dvd totient n")
   9.182 +  case False
   9.183 +  thus ?thesis using order_divides_totient[of n] assms
   9.184 +    by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
   9.185 +next
   9.186 +  case True
   9.187 +  have "\<psi> d = totient d"
   9.188 +  proof (rule ccontr)
   9.189 +    assume neq: "\<psi> d \<noteq> totient d"
   9.190 +    have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
   9.191 +      using prime_card_elements_with_ord[of d] assms by (cases "\<psi> d = 0") auto
   9.192 +    from neq and le[of d] and True have less: "\<psi> d < totient d" by auto
   9.193 +  
   9.194 +    have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
   9.195 +      using prime_sum_card_elements_with_ord_eq_totient ..
   9.196 +    also have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
   9.197 +      by (rule sum_strict_mono_ex1)
   9.198 +         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
   9.199 +    also have "\<dots> = totient n"
   9.200 +      using totient_divisor_sum .
   9.201 +    finally show False by simp
   9.202 +  qed
   9.203 +  with True show ?thesis using assms by (simp add: totient_prime)
   9.204 +qed
   9.205 +
   9.206 +text \<open>
   9.207 +  As a corollary, we get that the number of primitive roots modulo a prime \<open>p\<close> is
   9.208 +  $\varphi(p - 1)$. Since this number is positive, we also get that there \<^emph>\<open>is\<close> at least
   9.209 +  one primitive root modulo \<open>p\<close>.
   9.210 +\<close>
   9.211 +lemma
   9.212 +  assumes "prime n"
   9.213 +  shows   prime_card_primitive_roots:  "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
   9.214 +                                       "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
   9.215 +  and     prime_primitive_root_exists: "\<exists>x. residue_primroot n x"
   9.216 +proof -
   9.217 +  show *: "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
   9.218 +    using prime_card_elements_with_ord_eq_totient[of "n - 1"] assms
   9.219 +    by (auto simp: totient_prime \<psi>_def)
   9.220 +  thus "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
   9.221 +    using assms n elements_with_ord_restrict_totatives[of "n - 1"] by simp
   9.222 +  
   9.223 +  note *
   9.224 +  also have "totient (n - 1) > 0" using n by auto
   9.225 +  finally show "\<exists>x. residue_primroot n x" using assms prime_gt_1_nat[of n]
   9.226 +    by (subst (asm) card_gt_0_iff)
   9.227 +       (auto simp: residue_primroot_def totient_prime totatives_def coprime_commute)
   9.228 +qed
   9.229 +
   9.230 +end
   9.231 +
   9.232 +
   9.233 +subsection \<open>Primitive roots modulo powers of an odd prime\<close>
   9.234 +
   9.235 +text \<open>
   9.236 +  Any primitive root \<open>g\<close> modulo an odd prime \<open>p\<close> is also a primitive root modulo $p^k$ for all
   9.237 +  $k > 0$ if $[g^{p - 1} \neq 1]\ (\text{mod}\ p^2)$. To show this, we first need the
   9.238 +  following lemma.
   9.239 +\<close>
   9.240 +lemma residue_primroot_power_prime_power_neq_1:
   9.241 +  assumes "k \<ge> 2"
   9.242 +  assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.243 +  shows   "[g ^ totient (p ^ (k - 1)) \<noteq> 1] (mod (p ^ k))"
   9.244 +  using assms(1)
   9.245 +proof (induction k rule: dec_induct)
   9.246 +  case base
   9.247 +  thus ?case using assms by (simp add: totient_prime)
   9.248 +next
   9.249 +  case (step k)
   9.250 +  from p have "p > 2"
   9.251 +    using prime_gt_1_nat[of p] by (cases "p = 2") auto
   9.252 +  from assms have g: "g > 0" by (auto intro!: Nat.gr0I)
   9.253 +  have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ (k - 1))"
   9.254 +    using assms by (intro euler_theorem)
   9.255 +                   (auto simp: residue_primroot_def totatives_def coprime_commute)
   9.256 +  from cong_to_1_nat[OF this]
   9.257 +    obtain t where *: "g ^ totient (p ^ (k - 1)) - 1 = p ^ (k - 1) * t" by auto
   9.258 +  have t: "g ^ totient (p ^ (k - 1)) = p ^ (k - 1) * t + 1"
   9.259 +    using g by (subst * [symmetric]) auto 
   9.260 +
   9.261 +  have "\<not>p dvd t"
   9.262 +  proof
   9.263 +    assume "p dvd t"
   9.264 +    then obtain q where [simp]: "t = p * q" by auto
   9.265 +    from t have "g ^ totient (p ^ (k - 1)) = p ^ k * q + 1"
   9.266 +      using \<open>k \<ge> 2\<close> by (cases k) auto
   9.267 +    hence "[g ^ totient (p ^ (k - 1)) = p ^ k * q + 1] (mod p ^ k)"
   9.268 +      by simp
   9.269 +    also have "[p ^ k * q + 1 = 0 * q + 1] (mod p ^ k)"
   9.270 +      by (intro cong_add cong_mult) (auto simp: cong_0_iff)
   9.271 +    finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ k)"
   9.272 +      by simp
   9.273 +    with step.IH show False by contradiction
   9.274 +  qed
   9.275 +
   9.276 +  from t have "(g ^ totient (p ^ (k - 1))) ^ p = (p ^ (k - 1) * t + 1) ^ p"
   9.277 +    by (rule arg_cong)
   9.278 +  also have "(g ^ totient (p ^ (k - 1))) ^ p = g ^ (p * totient (p ^ (k - 1)))"
   9.279 +    by (simp add: power_mult [symmetric] mult.commute)
   9.280 +  also have "p * totient (p ^ (k - 1)) = totient (p ^ k)"
   9.281 +    using p \<open>k \<ge> 2\<close> by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc)
   9.282 +  also have "(p ^ (k - 1) * t + 1) ^ p = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))"
   9.283 +    by (subst binomial) (simp_all add: mult_ac power_mult_distrib power_mult [symmetric])
   9.284 +  finally have "[g ^ totient (p ^ k) = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))]
   9.285 +                  (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp
   9.286 +
   9.287 +  also have "[?rhs = (\<Sum>i\<le>p. if i \<le> 1 then (p choose i) * t ^ i * p ^ (i * (k - 1)) else 0)]
   9.288 +               (mod (p ^ Suc k))" (is "[sum ?f _ = sum ?g _] (mod _)")
   9.289 +  proof (intro cong_sum)
   9.290 +    fix i assume i: "i \<in> {..p}"
   9.291 +    consider "i \<le> 1" | "i = 2" | "i > 2" by force
   9.292 +    thus "[?f i = ?g i] (mod (p ^ Suc k))"
   9.293 +    proof cases
   9.294 +      assume i: "i > 2"
   9.295 +      have "Suc k \<le> 3 * (k - 1)"
   9.296 +        using \<open>k \<ge> 2\<close> by (simp add: algebra_simps)
   9.297 +      also have "3 * (k - 1) \<le> i * (k - 1)"
   9.298 +        using i by (intro mult_right_mono) auto
   9.299 +      finally have "p ^ Suc k dvd ?f i"
   9.300 +        by (intro dvd_mult le_imp_power_dvd)
   9.301 +      thus "[?f i = ?g i] (mod (p ^ Suc k))"
   9.302 +        by (simp add: cong_0_iff)
   9.303 +    next
   9.304 +      assume [simp]: "i = 2"
   9.305 +      have "?f i = p * (p - 1) div 2 * t\<^sup>2 * p ^ (2 * (k - 1))"
   9.306 +        using choose_two[of p] by simp
   9.307 +      also have "p * (p - 1) div 2 = (p - 1) div 2 * p"
   9.308 +        using \<open>odd p\<close> by (auto elim!: oddE)
   9.309 +      also have "\<dots> * t\<^sup>2 * p ^ (2 * (k - 1)) = (p - 1) div 2 * t\<^sup>2 * (p * p ^ (2 * (k - 1)))"
   9.310 +        by (simp add: algebra_simps)
   9.311 +      also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)"
   9.312 +        using \<open>k \<ge> 2\<close> by (cases k) auto
   9.313 +      also have "p ^ Suc k dvd (p - 1) div 2 * t\<^sup>2 * p ^ (2 * k - 1)"
   9.314 +        using \<open>k \<ge> 2\<close> by (intro dvd_mult le_imp_power_dvd) auto
   9.315 +      finally show "[?f i = ?g i] (mod (p ^ Suc k))"
   9.316 +        by (simp add: cong_0_iff)
   9.317 +    qed auto
   9.318 +  qed
   9.319 +  also have "(\<Sum>i\<le>p. ?g i) = (\<Sum>i\<le>1. ?f i)"
   9.320 +    using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto
   9.321 +  also have "\<dots> = 1 + t * p ^ k"
   9.322 +    using choose_two[of p] \<open>k \<ge> 2\<close> by (cases k) simp_all
   9.323 +  finally have eq: "[g ^ totient (p ^ k) = 1 + t * p ^ k] (mod p ^ Suc k)" .
   9.324 +
   9.325 +  have "[g ^ totient (p ^ k) \<noteq> 1] (mod p ^ Suc k)"
   9.326 +  proof
   9.327 +    assume "[g ^ totient (p ^ k) = 1] (mod p ^ Suc k)"
   9.328 +    hence "[g ^ totient (p ^ k) - g ^ totient (p ^ k) = 1 + t * p ^ k - 1] (mod p ^ Suc k)"
   9.329 +      by (intro cong_diff_nat eq) auto
   9.330 +    hence "[t * p ^ k = 0] (mod p ^ Suc k)"
   9.331 +      by (simp add: cong_sym_eq)
   9.332 +    hence "p * p ^ k dvd t * p ^ k"
   9.333 +      by (simp add: cong_0_iff)
   9.334 +    hence "p dvd t" using \<open>p > 2\<close> by simp
   9.335 +    with \<open>\<not>p dvd t\<close> show False by contradiction
   9.336 +  qed
   9.337 +  thus ?case by simp
   9.338 +qed
   9.339 +
   9.340 +text \<open>
   9.341 +  We can now show that primitive roots modulo \<open>p\<close> with the above condition are
   9.342 +  indeed also primitive roots modulo $p^k$.
   9.343 +\<close>
   9.344 +proposition residue_primroot_prime_lift_iff:
   9.345 +  assumes p: "prime p" "odd p" and "residue_primroot p g"
   9.346 +  shows   "(\<forall>k>0. residue_primroot (p ^ k) g) \<longleftrightarrow> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.347 +proof -
   9.348 +  from assms have g: "coprime p g" "ord p g = p - 1"
   9.349 +    by (auto simp: residue_primroot_def totient_prime)
   9.350 +  show ?thesis
   9.351 +  proof
   9.352 +    assume "\<forall>k>0. residue_primroot (p ^ k) g"
   9.353 +    hence "residue_primroot (p\<^sup>2) g" by auto
   9.354 +    hence "ord (p\<^sup>2) g = totient (p\<^sup>2)"
   9.355 +      by (simp_all add: residue_primroot_def)
   9.356 +    thus "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.357 +      using g assms prime_gt_1_nat[of p]
   9.358 +      by (auto simp: ord_divides' totient_prime_power)
   9.359 +  next
   9.360 +    assume g': "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.361 +
   9.362 +    have "residue_primroot (p ^ k) g" if "k > 0" for k
   9.363 +    proof (cases "k = 1")
   9.364 +      case False
   9.365 +      with that have k: "k > 1" by simp
   9.366 +      from g have coprime: "coprime (p ^ k) g"
   9.367 +        by (auto simp: totatives_def coprime_commute)
   9.368 +
   9.369 +      define t where "t = ord (p ^ k) g"
   9.370 +      have "[g ^ t = 1] (mod (p ^ k))"
   9.371 +        by (simp add: t_def ord_divides')
   9.372 +      also have "p ^ k = p * p ^ (k - 1)"
   9.373 +        using k by (cases k) auto
   9.374 +      finally have "[g ^ t = 1] (mod p)"
   9.375 +        by (rule cong_modulus_mult_nat)
   9.376 +      hence "totient p dvd t"
   9.377 +        using g p by (simp add: ord_divides' totient_prime)
   9.378 +      then obtain q where t: "t = totient p * q" by auto
   9.379 +
   9.380 +      have "t dvd totient (p ^ k)"
   9.381 +        using coprime by (simp add: t_def order_divides_totient)
   9.382 +      with t p k have "q dvd p ^ (k - 1)" using prime_gt_1_nat[of p]
   9.383 +        by (auto simp: totient_prime totient_prime_power)
   9.384 +      then obtain b where b: "b \<le> k - 1" "q = p ^ b"
   9.385 +        using divides_primepow_nat[of p q "k - 1"] p by auto
   9.386 +
   9.387 +      have "b = k - 1"
   9.388 +      proof (rule ccontr)
   9.389 +        assume "b \<noteq> k - 1"
   9.390 +        with b have "b < k - 1" by simp
   9.391 +        have "t = p ^ b * (p - 1)"
   9.392 +          using b p by (simp add: t totient_prime)
   9.393 +        also have "\<dots> dvd p ^ (k - 2) * (p - 1)"
   9.394 +          using \<open>b < k - 1\<close> by (intro mult_dvd_mono le_imp_power_dvd) auto
   9.395 +        also have "\<dots> = totient (p ^ (k - 1))"
   9.396 +          using k p by (simp add: totient_prime_power numeral_2_eq_2)
   9.397 +        finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod (p ^ k))"
   9.398 +          by (simp add: ord_divides' t_def)
   9.399 +        with residue_primroot_power_prime_power_neq_1[of k p g] p k assms g' show False
   9.400 +          by auto
   9.401 +      qed
   9.402 +      hence "t = totient (p ^ k)"
   9.403 +        using p k by (simp add: t b totient_prime totient_prime_power)
   9.404 +      thus "residue_primroot (p ^ k) g"
   9.405 +        using g one_less_power[of p k] prime_gt_1_nat[of p] p k
   9.406 +        by (simp add: residue_primroot_def t_def)
   9.407 +    qed (use assms in auto)
   9.408 +    thus "\<forall>k>0. residue_primroot (p ^ k) g" by blast
   9.409 +  qed
   9.410 +qed
   9.411 +
   9.412 +text \<open>
   9.413 +  If \<open>p\<close> is an odd prime, there is always a primitive root \<open>g\<close> modulo \<open>p\<close>, and if \<open>g\<close> does not
   9.414 +  fulfil the above assumption required for it to be liftable to $p^k$, we can use $g + p$, which
   9.415 +  is also a primitive root modulo \<open>p\<close> and \<^emph>\<open>does\<close> fulfil the assumption.
   9.416 +
   9.417 +  This shows that any modulus that is a power of an odd prime has a primitive root.
   9.418 +\<close>
   9.419 +theorem residue_primroot_odd_prime_power_exists:
   9.420 +  assumes p: "prime p" "odd p"
   9.421 +  obtains g where "\<forall>k>0. residue_primroot (p ^ k) g"
   9.422 +proof -
   9.423 +  obtain g where g: "residue_primroot p g"
   9.424 +    using prime_primitive_root_exists[of p] assms prime_gt_1_nat[of p] by auto
   9.425 +
   9.426 +  have "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.427 +  proof (cases "[g ^ (p - 1) = 1] (mod p\<^sup>2)")
   9.428 +    case True
   9.429 +    define g' where "g' = p + g"
   9.430 +    note g
   9.431 +    also have "residue_primroot p g \<longleftrightarrow> residue_primroot p g'"
   9.432 +      unfolding g'_def by (rule residue_primroot_cong) (auto simp: cong_def)
   9.433 +    finally have g': "residue_primroot p g'" .
   9.434 +
   9.435 +    have "[g' ^ (p - 1) = (\<Sum>k\<le>p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p\<^sup>2)"
   9.436 +      (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac)
   9.437 +    also have "[?rhs = (\<Sum>k\<le>p-1. if k \<le> 1 then ((p-1) choose k) *
   9.438 +                                   g ^ (p - Suc k) * p ^ k else 0)] (mod p\<^sup>2)"
   9.439 +      (is "[sum ?f _ = sum ?g _] (mod _)")
   9.440 +    proof (intro cong_sum)
   9.441 +      fix k assume "k \<in> {..p-1}"
   9.442 +      show "[?f k = ?g k] (mod p\<^sup>2)"
   9.443 +      proof (cases "k \<le> 1")
   9.444 +        case False
   9.445 +        have "p\<^sup>2 dvd ?f k"
   9.446 +          using False by (intro dvd_mult le_imp_power_dvd) auto
   9.447 +        thus ?thesis using False by (simp add: cong_0_iff)
   9.448 +      qed auto
   9.449 +    qed
   9.450 +    also have "sum ?g {..p-1} = sum ?f {0, 1}"
   9.451 +      using prime_gt_1_nat[of p] p by (intro sum.mono_neutral_cong_right) auto
   9.452 +    also have "\<dots> = g ^ (p - 1) + p * (p - 1) * g ^ (p - 2)"
   9.453 +      using p by (simp add: numeral_2_eq_2)
   9.454 +    also have "[g ^ (p - 1) + p * (p - 1) * g ^ (p - 2) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)"
   9.455 +      by (intro cong_add True) auto
   9.456 +    finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)" .
   9.457 +
   9.458 +    moreover have "[1 + p * (p - 1) * g ^ (p - 2) \<noteq> 1] (mod p\<^sup>2)"
   9.459 +    proof
   9.460 +      assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p\<^sup>2)"
   9.461 +      hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p\<^sup>2)"
   9.462 +        by (intro cong_diff_nat) auto
   9.463 +      hence "p * p dvd p * ((p - 1) * g ^ (p - 2))"
   9.464 +        by (auto simp: cong_0_iff power2_eq_square)
   9.465 +      hence "p dvd (p - 1) * g ^ (p - 2)"
   9.466 +        using p by simp
   9.467 +      hence "p dvd g ^ (p - 2)"
   9.468 +        using p dvd_imp_le[of p "p - Suc 0"] prime_gt_1_nat[of p]
   9.469 +        by (auto simp: prime_dvd_mult_iff)
   9.470 +      also have "\<dots> dvd g ^ (p - 1)"
   9.471 +        by (intro le_imp_power_dvd) auto
   9.472 +      finally have "[g ^ (p - 1) = 0] (mod p)"
   9.473 +        by (simp add: cong_0_iff)
   9.474 +      hence "[0 = g ^ (p - 1)] (mod p)"
   9.475 +        by (simp add: cong_sym_eq)
   9.476 +
   9.477 +      also from \<open>residue_primroot p g\<close> have "[g ^ (p - 1) = 1] (mod p)"
   9.478 +        using p by (auto simp: residue_primroot_def ord_divides' totient_prime)
   9.479 +      finally have "[0 = 1] (mod p)" .
   9.480 +      thus False using prime_gt_1_nat[of p] p by (simp add: cong_def)
   9.481 +    qed
   9.482 +
   9.483 +    ultimately have "[g' ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.484 +      by (simp add: cong_def)
   9.485 +    thus "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   9.486 +      using g' by blast    
   9.487 +  qed (use g in auto)
   9.488 +  thus ?thesis
   9.489 +    using residue_primroot_prime_lift_iff[OF assms] that by blast
   9.490 +qed
   9.491 +
   9.492 +
   9.493 +subsection \<open>Carmichael's function\<close>
   9.494 +
   9.495 +text \<open>
   9.496 +  Carmichael's function $\lambda(n)$ gives the LCM of the orders of all elements in the
   9.497 +  residue ring modulo $n$ -- or, equivalently, the maximum order, as we will show later.
   9.498 +  Algebraically speaking, it is the exponent of the multiplicative group
   9.499 +  $(\mathbb{Z}/n\mathbb{Z})^*$.
   9.500 +
   9.501 +  It is not to be confused with Liouville's function, which is also denoted by $\lambda(n)$.
   9.502 +\<close>
   9.503 +definition Carmichael where
   9.504 +  "Carmichael n = (LCM a \<in> totatives n. ord n a)"
   9.505 +
   9.506 +lemma Carmichael_0 [simp]: "Carmichael 0 = 1"
   9.507 +  by (simp add: Carmichael_def)
   9.508 +
   9.509 +lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
   9.510 +  by (simp add: Carmichael_def)
   9.511 +
   9.512 +lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
   9.513 +  by (simp add: Carmichael_def)
   9.514 +
   9.515 +lemma ord_dvd_Carmichael:
   9.516 +  assumes "n > 1" "coprime n k"
   9.517 +  shows   "ord n k dvd Carmichael n"
   9.518 +proof -
   9.519 +  have "k mod n \<in> totatives n"
   9.520 +    using assms by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
   9.521 +  hence "ord n (k mod n) dvd Carmichael n"
   9.522 +    by (simp add: Carmichael_def del: ord_mod)
   9.523 +  thus ?thesis by simp
   9.524 +qed
   9.525 +
   9.526 +lemma Carmichael_divides:
   9.527 +  assumes "Carmichael n dvd k" "coprime n a"
   9.528 +  shows   "[a ^ k = 1] (mod n)"
   9.529 +proof (cases "n < 2 \<or> a = 1")
   9.530 +  case False
   9.531 +  hence "ord n a dvd Carmichael n"
   9.532 +    using False assms by (intro ord_dvd_Carmichael) auto
   9.533 +  also have "\<dots> dvd k" by fact
   9.534 +  finally have "ord n a dvd k" .
   9.535 +  thus ?thesis using ord_divides by auto
   9.536 +next
   9.537 +  case True
   9.538 +  then consider "a = 1" | "n = 0" | "n = 1" by force
   9.539 +  thus ?thesis using assms by cases auto
   9.540 +qed
   9.541 +
   9.542 +lemma Carmichael_dvd_totient: "Carmichael n dvd totient n"
   9.543 +  unfolding Carmichael_def
   9.544 +proof (intro Lcm_least, safe)
   9.545 +  fix a assume "a \<in> totatives n"
   9.546 +  hence "[a ^ totient n = 1] (mod n)"
   9.547 +    by (intro euler_theorem) (auto simp: totatives_def)
   9.548 +  thus "ord n a dvd totient n"
   9.549 +    using ord_divides by blast
   9.550 +qed
   9.551 +
   9.552 +lemma Carmichael_dvd_mono_coprime:
   9.553 +  assumes "coprime m n" "m > 1" "n > 1"
   9.554 +  shows   "Carmichael m dvd Carmichael (m * n)"
   9.555 +  unfolding Carmichael_def[of m]
   9.556 +proof (intro Lcm_least, safe)
   9.557 +  fix x assume x: "x \<in> totatives m"
   9.558 +  from assms have "totatives n \<noteq> {}" by simp
   9.559 +  then obtain y where y: "y \<in> totatives n" by blast
   9.560 +
   9.561 +  from binary_chinese_remainder_nat[OF assms(1), of x y]
   9.562 +  obtain z where z: "[z = x] (mod m)" "[z = y] (mod n)" by blast
   9.563 +  have z': "coprime z n" "coprime z m"
   9.564 +    by (rule cong_imp_coprime; use x y z in \<open>force simp: totatives_def cong_sym_eq\<close>)+
   9.565 +
   9.566 +  from z have "ord m x = ord m z"
   9.567 +    by (intro ord_cong) (auto simp: cong_sym_eq)
   9.568 +  also have "ord m z dvd ord (m * n) z"
   9.569 +    using assms by (auto simp: ord_modulus_mult_coprime)
   9.570 +  also from z' assms have "\<dots> dvd Carmichael (m * n)"
   9.571 +    by (intro ord_dvd_Carmichael) (auto simp: coprime_commute intro!:one_less_mult)
   9.572 +  finally show "ord m x dvd Carmichael (m * n)" .
   9.573 +qed
   9.574 +
   9.575 +text \<open>
   9.576 +  $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but
   9.577 +  with LCM instead of multiplication:
   9.578 +\<close>
   9.579 +lemma Carmichael_mult_coprime:
   9.580 +  assumes "coprime m n"
   9.581 +  shows   "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)"
   9.582 +proof (cases "m \<le> 1 \<or> n \<le> 1")
   9.583 +  case True
   9.584 +  hence "m = 0 \<or> n = 0 \<or> m = 1 \<or> n = 1" by force
   9.585 +  thus ?thesis using assms by auto
   9.586 +next
   9.587 +  case False
   9.588 +  show ?thesis
   9.589 +  proof (rule dvd_antisym)
   9.590 +    show "Carmichael (m * n) dvd lcm (Carmichael m) (Carmichael n)"
   9.591 +      unfolding Carmichael_def[of "m * n"]
   9.592 +    proof (intro Lcm_least, safe)
   9.593 +      fix x assume x: "x \<in> totatives (m * n)"
   9.594 +      have "ord (m * n) x = lcm (ord m x) (ord n x)"
   9.595 +        using assms x by (subst ord_modulus_mult_coprime) (auto simp: coprime_commute totatives_def)
   9.596 +      also have "\<dots> dvd lcm (Carmichael m) (Carmichael n)"
   9.597 +        using False x
   9.598 +        by (intro lcm_mono ord_dvd_Carmichael) (auto simp: totatives_def coprime_commute)
   9.599 +      finally show "ord (m * n) x dvd \<dots>" .
   9.600 +    qed
   9.601 +  next
   9.602 +    show "lcm (Carmichael m) (Carmichael n) dvd Carmichael (m * n)"
   9.603 +      using Carmichael_dvd_mono_coprime[of m n]
   9.604 +            Carmichael_dvd_mono_coprime[of n m] assms False
   9.605 +      by (auto intro!: lcm_least simp: coprime_commute mult.commute)
   9.606 +  qed
   9.607 +qed
   9.608 +
   9.609 +lemma Carmichael_pos [simp, intro]: "Carmichael n > 0"
   9.610 +  by (auto simp: Carmichael_def ord_eq_0 totatives_def coprime_commute intro!: Nat.gr0I)
   9.611 +
   9.612 +lemma Carmichael_nonzero [simp]: "Carmichael n \<noteq> 0"
   9.613 +  by simp
   9.614 +
   9.615 +lemma power_Carmichael_eq_1:
   9.616 +  assumes "n > 1" "coprime n x"
   9.617 +  shows   "[x ^ Carmichael n = 1] (mod n)"
   9.618 +  using ord_dvd_Carmichael[of n x] assms
   9.619 +  by (auto simp: ord_divides')
   9.620 +
   9.621 +lemma Carmichael_2 [simp]: "Carmichael 2 = 1"
   9.622 +  using Carmichael_dvd_totient[of 2] by simp
   9.623 +
   9.624 +lemma Carmichael_4 [simp]: "Carmichael 4 = 2"
   9.625 +proof -
   9.626 +  have "Carmichael 4 dvd 2"
   9.627 +    using Carmichael_dvd_totient[of 4] by simp
   9.628 +  hence "Carmichael 4 \<le> 2" by (rule dvd_imp_le) auto
   9.629 +  moreover have "Carmichael 4 \<noteq> 1"
   9.630 +    using power_Carmichael_eq_1[of "4::nat" 3]
   9.631 +    unfolding coprime_iff_gcd_eq_1 by (auto simp: gcd_non_0_nat cong_def)
   9.632 +  ultimately show ?thesis
   9.633 +    using Carmichael_pos[of 4] by linarith
   9.634 +qed
   9.635 +
   9.636 +lemma residue_primroot_Carmichael:
   9.637 +  assumes "residue_primroot n g"
   9.638 +  shows   "Carmichael n = totient n"
   9.639 +proof (cases "n = 1")
   9.640 +  case False
   9.641 +  show ?thesis
   9.642 +  proof (intro dvd_antisym Carmichael_dvd_totient)
   9.643 +    have "ord n g dvd Carmichael n"
   9.644 +      using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
   9.645 +    thus "totient n dvd Carmichael n"
   9.646 +      using assms by (auto simp: residue_primroot_def)
   9.647 +  qed
   9.648 +qed auto
   9.649 +
   9.650 +lemma Carmichael_odd_prime_power:
   9.651 +  assumes "prime p" "odd p" "k > 0"
   9.652 +  shows   "Carmichael (p ^ k) = p ^ (k - 1) * (p - 1)"
   9.653 +proof -
   9.654 +  from assms obtain g where "residue_primroot (p ^ k) g"
   9.655 +    using residue_primroot_odd_prime_power_exists[of p] assms by metis
   9.656 +  hence "Carmichael (p ^ k) = totient (p ^ k)"
   9.657 +    by (intro residue_primroot_Carmichael[of "p ^ k" g]) auto
   9.658 +  with assms show ?thesis by (simp add: totient_prime_power)
   9.659 +qed
   9.660 +
   9.661 +lemma Carmichael_prime:
   9.662 +  assumes "prime p"
   9.663 +  shows   "Carmichael p = p - 1"
   9.664 +proof (cases "even p")
   9.665 +  case True
   9.666 +  with assms have "p = 2"
   9.667 +    using primes_dvd_imp_eq two_is_prime_nat by blast
   9.668 +  thus ?thesis by simp
   9.669 +next
   9.670 +  case False
   9.671 +  with Carmichael_odd_prime_power[of p 1] assms show ?thesis by simp
   9.672 +qed
   9.673 +  
   9.674 +lemma Carmichael_twopow_ge_8:
   9.675 +  assumes "k \<ge> 3"
   9.676 +  shows   "Carmichael (2 ^ k) = 2 ^ (k - 2)"
   9.677 +proof (intro dvd_antisym)
   9.678 +  have "2 ^ (k - 2) = ord (2 ^ k) (3 :: nat)"
   9.679 +    using ord_twopow_3_5[of k 3] assms by simp
   9.680 +  also have "\<dots> dvd Carmichael (2 ^ k)"
   9.681 +    using assms one_less_power[of "2::nat" k] by (intro ord_dvd_Carmichael) auto
   9.682 +  finally show "2 ^ (k - 2) dvd \<dots>" .
   9.683 +next
   9.684 +  show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)"
   9.685 +    unfolding Carmichael_def
   9.686 +  proof (intro Lcm_least, safe)
   9.687 +    fix x assume "x \<in> totatives (2 ^ k)"
   9.688 +    hence "odd x" by (auto simp: totatives_def)
   9.689 +    hence "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
   9.690 +      using assms ord_twopow_aux[of k x] by auto
   9.691 +    thus "ord (2 ^ k) x dvd 2 ^ (k - 2)"
   9.692 +      by (simp add: ord_divides')
   9.693 +  qed
   9.694 +qed
   9.695 +
   9.696 +lemma Carmichael_twopow:
   9.697 +  "Carmichael (2 ^ k) = (if k \<le> 2 then 2 ^ (k - 1) else 2 ^ (k - 2))"
   9.698 +proof -
   9.699 +  have "k = 0 \<or> k = 1 \<or> k = 2 \<or> k \<ge> 3" by linarith
   9.700 +  thus ?thesis by (auto simp: Carmichael_twopow_ge_8)
   9.701 +qed
   9.702 +
   9.703 +lemma Carmichael_prime_power:
   9.704 +  assumes "prime p" "k > 0"
   9.705 +  shows   "Carmichael (p ^ k) =
   9.706 +             (if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   9.707 +proof (cases "p = 2")
   9.708 +  case True
   9.709 +  thus ?thesis by (simp add: Carmichael_twopow)
   9.710 +next
   9.711 +  case False
   9.712 +  with assms have "odd p" "p > 2"
   9.713 +    using prime_odd_nat[of p] prime_gt_1_nat[of p] by auto
   9.714 +  thus ?thesis
   9.715 +    using assms Carmichael_odd_prime_power[of p k] by simp
   9.716 +qed
   9.717 +
   9.718 +lemma Carmichael_prod_coprime:
   9.719 +  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
   9.720 +  shows   "Carmichael (\<Prod>i\<in>A. f i) = (LCM i\<in>A. Carmichael (f i))"
   9.721 +  using assms by (induction A rule: finite_induct)
   9.722 +                 (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto)
   9.723 +
   9.724 +text \<open>
   9.725 +  Since $\lambda$ distributes over coprime factors and we know the value of $\lambda(p^k)$
   9.726 +  for prime $p$, we can now give a closed formula for $\lambda(n)$ in terms of the prime
   9.727 +  factorisation of $n$:
   9.728 +\<close>
   9.729 +theorem Carmichael_closed_formula:
   9.730 +  "Carmichael n =
   9.731 +     (LCM p\<in>prime_factors n. let k = multiplicity p n
   9.732 +                             in  if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   9.733 +  (is "_ = Lcm ?A")
   9.734 +proof (cases "n = 0")
   9.735 +  case False
   9.736 +  hence "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
   9.737 +    using prime_factorization_nat by blast
   9.738 +  also have "Carmichael \<dots> =
   9.739 +               (LCM p\<in>prime_factors n. Carmichael (p ^ multiplicity p n))"
   9.740 +    by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime)
   9.741 +  also have "(\<lambda>p. Carmichael (p ^ multiplicity p n)) ` prime_factors n = ?A"
   9.742 +    by (intro image_cong)
   9.743 +       (auto simp: Let_def Carmichael_prime_power prime_factors_multiplicity)
   9.744 +  finally show ?thesis .
   9.745 +qed auto
   9.746 +
   9.747 +corollary even_Carmichael:
   9.748 +  assumes "n > 2"
   9.749 +  shows   "even (Carmichael n)"
   9.750 +proof (cases "\<exists>k. n = 2 ^ k")
   9.751 +  case True
   9.752 +  then obtain k where [simp]: "n = 2 ^ k" by auto
   9.753 +  from assms have "k \<noteq> 0" "k \<noteq> 1" by (auto intro!: Nat.gr0I)
   9.754 +  hence "k \<ge> 2" by auto
   9.755 +  thus ?thesis by (auto simp: Carmichael_twopow)
   9.756 +next
   9.757 +  case False
   9.758 +  from assms have "n \<noteq> 0" by auto
   9.759 +  from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
   9.760 +    using assms Ex_other_prime_factor[of n 2] by auto
   9.761 +  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
   9.762 +  from p have coprime: "coprime (p ^ k) n'"
   9.763 +    using p prime_imp_coprime by auto
   9.764 +  have "odd p"
   9.765 +    using p primes_dvd_imp_eq[of 2 p] by auto
   9.766 +  have "even (Carmichael (p ^ k))"
   9.767 +    using p \<open>odd p\<close> by (auto simp: Carmichael_prime_power)
   9.768 +  with p coprime show ?thesis
   9.769 +    by (auto simp: Carmichael_mult_coprime intro!: dvd_lcmI1)
   9.770 +qed
   9.771 +
   9.772 +lemma eval_Carmichael:
   9.773 +  assumes "prime_factorization n = A"
   9.774 +  shows     "Carmichael n = (LCM p \<in> set_mset A.
   9.775 +               let k = count A p in if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   9.776 +  unfolding assms [symmetric] Carmichael_closed_formula
   9.777 +  by (intro arg_cong[where f = Lcm] image_cong) (auto simp: Let_def count_prime_factorization)
   9.778 +
   9.779 +text \<open>
   9.780 +  Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose
   9.781 +  order is $\lambda(n)$.
   9.782 +\<close>
   9.783 +theorem Carmichael_root_exists:
   9.784 +  assumes "n > (0::nat)"
   9.785 +  obtains g where "g \<in> totatives n" and "ord n g = Carmichael n"
   9.786 +proof (cases "n = 1")
   9.787 +  case True
   9.788 +  thus ?thesis by (intro that[of 1]) (auto simp: totatives_def)
   9.789 +next
   9.790 +  case False
   9.791 +  have primepow: "\<exists>g. coprime (p ^ k) g \<and> ord (p ^ k) g = Carmichael (p ^ k)"
   9.792 +    if pk: "prime p" "k > 0" for p k
   9.793 +  proof (cases "p = 2")
   9.794 +    case [simp]: True
   9.795 +    from \<open>k > 0\<close> consider "k = 1" | "k = 2" | "k \<ge> 3" by force
   9.796 +    thus ?thesis
   9.797 +    proof cases
   9.798 +      assume "k = 1"
   9.799 +      thus ?thesis by (intro exI[of _ 1]) auto
   9.800 +    next
   9.801 +      assume [simp]: "k = 2"
   9.802 +      have "coprime 4 (3::nat)"
   9.803 +        by (auto simp: coprime_iff_gcd_eq_1 gcd_non_0_nat)
   9.804 +      thus ?thesis by (intro exI[of _ 3]) auto
   9.805 +    next
   9.806 +      assume k: "k \<ge> 3"
   9.807 +      have "coprime (2 ^ k :: nat) 3" by auto
   9.808 +      thus ?thesis using k
   9.809 +        by (intro exI[of _ 3]) (auto simp: ord_twopow_3_5 Carmichael_twopow)
   9.810 +    qed
   9.811 +  next
   9.812 +    case False
   9.813 +    hence "odd p" using \<open>prime p\<close>
   9.814 +      using primes_dvd_imp_eq two_is_prime_nat by blast
   9.815 +    then obtain g where "residue_primroot (p ^ k) g"
   9.816 +      using residue_primroot_odd_prime_power_exists[of p] pk by metis
   9.817 +    thus ?thesis using False pk
   9.818 +      by (intro exI[of _ g])
   9.819 +         (auto simp: Carmichael_prime_power residue_primroot_def totient_prime_power)
   9.820 +  qed
   9.821 +
   9.822 +  define P where "P = prime_factors n"
   9.823 +  define k where "k = (\<lambda>p. multiplicity p n)"
   9.824 +  have "\<forall>p\<in>P. \<exists>g. coprime (p ^ k p) g \<and> ord (p ^ k p) g = Carmichael (p ^ k p)"
   9.825 +    using primepow by (auto simp: P_def k_def prime_factors_multiplicity)
   9.826 +  hence "\<exists>g. \<forall>p\<in>P. coprime (p ^ k p) (g p) \<and> ord (p ^ k p) (g p) = Carmichael (p ^ k p)"
   9.827 +    by (subst (asm) bchoice_iff)
   9.828 +  then obtain g where g: "\<And>p. p \<in> P \<Longrightarrow> coprime (p ^ k p) (g p)"
   9.829 +                         "\<And>p. p \<in> P \<Longrightarrow> ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis
   9.830 +  have "\<exists>x. \<forall>i\<in>P. [x = g i] (mod i ^ k i)"
   9.831 +    by (intro chinese_remainder_nat)
   9.832 +       (auto simp: P_def k_def in_prime_factors_iff primes_coprime)
   9.833 +  then obtain x where x: "\<And>p. p \<in> P \<Longrightarrow> [x = g p] (mod p ^ k p)" by metis
   9.834 +
   9.835 +  have "n = (\<Prod>p\<in>P. p ^ k p)"
   9.836 +    using assms unfolding P_def k_def by (rule prime_factorization_nat)
   9.837 +  also have "ord \<dots> x = (LCM p\<in>P. ord (p ^ k p) x)"
   9.838 +    by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime)
   9.839 +  also have "(\<lambda>p. ord (p ^ k p) x) ` P = (\<lambda>p. ord (p ^ k p) (g p)) ` P"
   9.840 +    by (intro image_cong ord_cong x) auto
   9.841 +  also have "\<dots> = (\<lambda>p. Carmichael (p ^ k p)) ` P"
   9.842 +    by (intro image_cong g) auto
   9.843 +  also have "Lcm \<dots> = Carmichael (\<Prod>p\<in>P. p ^ k p)"
   9.844 +    by (intro Carmichael_prod_coprime [symmetric])
   9.845 +       (auto simp: P_def in_prime_factors_iff primes_coprime)
   9.846 +  also have "(\<Prod>p\<in>P. p ^ k p) = n"
   9.847 +    using assms unfolding P_def k_def by (rule prime_factorization_nat [symmetric])
   9.848 +  finally have "ord n x = Carmichael n" .
   9.849 +  moreover from this have "coprime n x"
   9.850 +    by (cases "coprime n x") (auto split: if_splits)
   9.851 +  ultimately show ?thesis using assms False
   9.852 +    by (intro that[of "x mod n"])
   9.853 +       (auto simp: totatives_def coprime_commute coprime_absorb_left intro!: Nat.gr0I)
   9.854 +qed
   9.855 +
   9.856 +text \<open>
   9.857 +  This also means that the Carmichael number is not only the LCM of the orders
   9.858 +  of the elements of the residue ring, but indeed the maximum of the orders.
   9.859 +\<close>
   9.860 +lemma Carmichael_altdef:
   9.861 +  "Carmichael n = (if n = 0 then 1 else Max (ord n ` totatives n))"
   9.862 +proof (cases "n = 0")
   9.863 +  case False
   9.864 +  have "Carmichael n = Max (ord n ` totatives n)"
   9.865 +  proof (intro antisym Max.boundedI Max.coboundedI)
   9.866 +    fix k assume k: "k \<in> ord n ` totatives n"
   9.867 +    thus "k \<le> Carmichael n"
   9.868 +    proof (cases "n = 1")
   9.869 +      case False
   9.870 +      with \<open>n \<noteq> 0\<close> have "n > 1" by linarith
   9.871 +      thus ?thesis using k \<open>n \<noteq> 0\<close>
   9.872 +        by (intro dvd_imp_le)
   9.873 +           (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute)
   9.874 +    qed auto
   9.875 +  next
   9.876 +    obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
   9.877 +      using Carmichael_root_exists[of n] \<open>n \<noteq> 0\<close> by auto
   9.878 +    thus "Carmichael n \<in> ord n ` totatives n" by force
   9.879 +  qed (use \<open>n \<noteq> 0\<close> in auto)
   9.880 +  thus ?thesis using False by simp
   9.881 +qed auto
   9.882 +
   9.883 +
   9.884 +subsection \<open>Existence of primitive roots for general moduli\<close>
   9.885 +
   9.886 +text \<open>
   9.887 +  We now related Carmichael's function to the existence of primitive roots and, in the end,
   9.888 +  use this to show precisely which moduli have primitive roots and which do not.
   9.889 +
   9.890 +  The first criterion for the existence of a primitive root is this: A primitive root modulo $n$
   9.891 +  exists iff $\lambda(n) = \varphi(n)$.
   9.892 +\<close>
   9.893 +lemma Carmichael_eq_totient_imp_primroot:
   9.894 +  assumes "n > 0" and "Carmichael n = totient n"
   9.895 +  shows   "\<exists>g. residue_primroot n g"
   9.896 +proof -
   9.897 +  from \<open>n > 0\<close> obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
   9.898 +    using Carmichael_root_exists[of n] by metis
   9.899 +  with assms show ?thesis by (auto simp: residue_primroot_def totatives_def coprime_commute)
   9.900 +qed
   9.901 +
   9.902 +theorem residue_primroot_iff_Carmichael:
   9.903 +  "(\<exists>g. residue_primroot n g) \<longleftrightarrow> Carmichael n = totient n \<and> n > 0"
   9.904 +proof safe
   9.905 +  fix g assume g: "residue_primroot n g"
   9.906 +  thus "n > 0" by (auto simp: residue_primroot_def)
   9.907 +  have "coprime n g" by (rule ccontr) (use g in \<open>auto simp: residue_primroot_def\<close>)
   9.908 +
   9.909 +  show "Carmichael n = totient n"
   9.910 +  proof (cases "n = 1")
   9.911 +    case False
   9.912 +    with \<open>n > 0\<close> have "n > 1" by auto
   9.913 +    with \<open>coprime n g\<close> have "ord n g dvd Carmichael n"
   9.914 +      by (intro ord_dvd_Carmichael) auto
   9.915 +    thus ?thesis using g by (intro dvd_antisym Carmichael_dvd_totient)
   9.916 +                            (auto simp: residue_primroot_def)
   9.917 +  qed auto
   9.918 +qed (use Carmichael_eq_totient_imp_primroot[of n] in auto)
   9.919 +
   9.920 +text \<open>
   9.921 +  Any primitive root modulo $mn$ for coprime $m$, $n$ is also a primitive root modulo $m$ and $n$.
   9.922 +  The converse does not hold in general.
   9.923 +\<close>
   9.924 +lemma residue_primroot_modulus_mult_coprimeD:
   9.925 +  assumes "coprime m n" and "residue_primroot (m * n) g"
   9.926 +  shows   "residue_primroot m g" "residue_primroot n g"
   9.927 +proof -
   9.928 +  have *: "m > 0" "n > 0" "coprime m g" "coprime n g"
   9.929 +          "lcm (ord m g) (ord n g) = totient m * totient n"
   9.930 +    using assms
   9.931 +    by (auto simp: residue_primroot_def ord_modulus_mult_coprime totient_mult_coprime)
   9.932 +
   9.933 +  define a b where "a = totient m div ord m g" and "b = totient n div ord n g"
   9.934 +  have ab: "totient m = ord m g * a" "totient n = ord n g * b"
   9.935 +    using * by (auto simp: a_def b_def order_divides_totient)
   9.936 +
   9.937 +  have "a = 1" "b = 1" "coprime (ord m g) (ord n g)"
   9.938 +    unfolding coprime_iff_gcd_eq_1 using * by (auto simp: ab lcm_nat_def dvd_div_eq_mult ord_eq_0)
   9.939 +  with ab and * show "residue_primroot m g" "residue_primroot n g"
   9.940 +    by (auto simp: residue_primroot_def)
   9.941 +qed
   9.942 +
   9.943 +text \<open>
   9.944 +  If a primitive root modulo $mn$ exists for coprime $m, n$, then $\lambda(m)$ and $\lambda(n)$
   9.945 +  must also be coprime. This is helpful in establishing that there are no primitive roots
   9.946 +  modulo $mn$ by showing e.\,g.\ that $\lambda(m)$ and $\lambda(n)$ are both even.
   9.947 +\<close>
   9.948 +lemma residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime:
   9.949 +  assumes "coprime m n" and "residue_primroot (m * n) g"
   9.950 +  shows   "coprime (Carmichael m) (Carmichael n)"
   9.951 +proof -
   9.952 +  from residue_primroot_modulus_mult_coprimeD[OF assms]
   9.953 +    have *: "residue_primroot m g" "residue_primroot n g" by auto
   9.954 +  hence [simp]: "Carmichael m = totient m" "Carmichael n = totient n"
   9.955 +    by (simp_all add: residue_primroot_Carmichael)
   9.956 +  from * have mn: "m > 0" "n > 0" by (auto simp: residue_primroot_def)
   9.957 +  
   9.958 +  from assms have "Carmichael (m * n) = totient (m * n) \<and> n > 0"
   9.959 +    using residue_primroot_iff_Carmichael[of "m * n"] by auto
   9.960 +  with assms have "lcm (totient m) (totient n) = totient m * totient n"
   9.961 +    by (simp add: Carmichael_mult_coprime totient_mult_coprime)
   9.962 +  thus ?thesis unfolding coprime_iff_gcd_eq_1 using mn
   9.963 +    by (simp add: lcm_nat_def dvd_div_eq_mult)
   9.964 +qed
   9.965 +  
   9.966 +text \<open>
   9.967 +  The following moduli are precisely those that have primitive roots.
   9.968 +\<close>
   9.969 +definition cyclic_moduli :: "nat set" where
   9.970 +  "cyclic_moduli = {1, 2, 4} \<union> {p ^ k |p k. prime p \<and> odd p \<and> k > 0} \<union>
   9.971 +                     {2 * p ^ k |p k. prime p \<and> odd p \<and> k > 0}"
   9.972 +
   9.973 +theorem residue_primroot_iff_in_cyclic_moduli:
   9.974 +  "(\<exists>g. residue_primroot m g) \<longleftrightarrow> m \<in> cyclic_moduli"
   9.975 +proof -
   9.976 +  have "(\<exists>g. residue_primroot m g)" if "m \<in> cyclic_moduli"
   9.977 +  using that unfolding cyclic_moduli_def
   9.978 +  by (intro Carmichael_eq_totient_imp_primroot)
   9.979 +     (auto dest: prime_gt_0_nat simp: Carmichael_prime_power totient_prime_power
   9.980 +                 Carmichael_mult_coprime totient_mult_coprime)
   9.981 +
   9.982 +  moreover have "\<not>(\<exists>g. residue_primroot m g)" if "m \<notin> cyclic_moduli"
   9.983 +  proof (cases "m = 0")
   9.984 +    case False
   9.985 +    with that have [simp]: "m > 0" "m \<noteq> 1" by (auto simp: cyclic_moduli_def)
   9.986 +    show ?thesis
   9.987 +    proof (cases "\<exists>k. m = 2 ^ k")
   9.988 +      case True
   9.989 +      then obtain k where [simp]: "m = 2 ^ k" by auto
   9.990 +      with that have "k \<noteq> 0 \<and> k \<noteq> 1 \<and> k \<noteq> 2" by (auto simp: cyclic_moduli_def)
   9.991 +      hence "k \<ge> 3" by auto
   9.992 +      thus ?thesis by (subst residue_primroot_iff_Carmichael)
   9.993 +                      (auto simp: Carmichael_twopow totient_prime_power)
   9.994 +    next
   9.995 +      case False
   9.996 +      hence "\<exists>p\<in>prime_factors m. p \<noteq> 2"
   9.997 +        using Ex_other_prime_factor[of m 2] by auto
   9.998 +      from divide_out_primepow_ex[OF \<open>m \<noteq> 0\<close> this]
   9.999 +      obtain p k m' where p: "p \<noteq> 2" "prime p" "p dvd m" "\<not>p dvd m'" "0 < k" "m = p ^ k * m'"
  9.1000 +        by metis
  9.1001 +      have "odd p"
  9.1002 +        using p primes_dvd_imp_eq[of 2 p] by auto
  9.1003 +      from p have coprime: "coprime (p ^ k) m'"
  9.1004 +        using p prime_imp_coprime by auto
  9.1005 +      have "m \<in> cyclic_moduli" if "m' = 1"
  9.1006 +        using that p \<open>odd p\<close> by (auto simp: cyclic_moduli_def)
  9.1007 +      moreover have "m \<in> cyclic_moduli" if "m' = 2"
  9.1008 +      proof -
  9.1009 +        have "m = 2 * p ^ k" using p that by (simp add: mult.commute)
  9.1010 +        thus "m \<in> cyclic_moduli" using p \<open>odd p\<close>
  9.1011 +          unfolding cyclic_moduli_def by blast
  9.1012 +      qed
  9.1013 +      moreover have "m' \<noteq> 0" using p by (intro notI) auto
  9.1014 +      ultimately have "m' \<noteq> 0 \<and>m' \<noteq> 1 \<and> m' \<noteq> 2" using that by auto
  9.1015 +      hence "m' > 2" by linarith
  9.1016 +  
  9.1017 +      show ?thesis
  9.1018 +      proof
  9.1019 +        assume "\<exists>g. residue_primroot m g"
  9.1020 +        with coprime p have coprime': "coprime (p - 1) (Carmichael m')"
  9.1021 +          using residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime[OF coprime]
  9.1022 +          by (auto simp: Carmichael_prime_power)
  9.1023 +        moreover have "even (p - 1)" "even (Carmichael m')"
  9.1024 +          using \<open>m' > 2\<close> \<open>odd p\<close> by (auto intro!: even_Carmichael)
  9.1025 +        ultimately show False by force
  9.1026 +      qed
  9.1027 +    qed
  9.1028 +  qed auto
  9.1029 +
  9.1030 +  ultimately show ?thesis by metis
  9.1031 +qed
  9.1032 +
  9.1033 +lemma residue_primroot_is_generator:
  9.1034 +  assumes "m > 1" and "residue_primroot m g"
  9.1035 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) {..<totient m} (totatives m)"
  9.1036 +  unfolding bij_betw_def
  9.1037 +proof
  9.1038 +  from assms have [simp]: "ord m g = totient m"
  9.1039 +    by (simp add: residue_primroot_def)
  9.1040 +  from assms have "coprime m g" by (simp add: residue_primroot_def)
  9.1041 +  hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
  9.1042 +    by (intro inj_power_mod)
  9.1043 +  thus inj: "inj_on (\<lambda>i. g ^ i mod m) {..<totient m}"
  9.1044 +    by simp
  9.1045 +
  9.1046 +  show "(\<lambda>i. g ^ i mod m) ` {..<totient m} = totatives m"
  9.1047 +  proof (rule card_subset_eq)
  9.1048 +    show "card ((\<lambda>i. g ^ i mod m) ` {..<totient m}) = card (totatives m)"
  9.1049 +      using inj by (subst card_image) (auto simp: totient_def)
  9.1050 +    show "(\<lambda>i. g ^ i mod m) ` {..<totient m} \<subseteq> totatives m"
  9.1051 +      using \<open>m > 1\<close> \<open>coprime m g\<close> power_in_totatives[of m g] by blast
  9.1052 +  qed auto
  9.1053 +qed
  9.1054 +
  9.1055 +text \<open>
  9.1056 +  Given one primitive root \<open>g\<close>, all the primitive roots are powers $g^i$ for
  9.1057 +  $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$.
  9.1058 +\<close>
  9.1059 +theorem residue_primroot_bij_betw_primroots:
  9.1060 +  assumes "m > 1" and "residue_primroot m g"
  9.1061 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
  9.1062 +                                      {g\<in>totatives m. residue_primroot m g}"
  9.1063 +proof (cases "m = 2")
  9.1064 +  case [simp]: True
  9.1065 +  have [simp]: "totatives 2 = {1}"
  9.1066 +    by (auto simp: totatives_def elim!: oddE)
  9.1067 +  from assms have "odd g"
  9.1068 +    by (auto simp: residue_primroot_def)
  9.1069 +  hence pow_eq: "(\<lambda>i. g ^ i mod m) = (\<lambda>_. 1)"
  9.1070 +    by (auto simp: fun_eq_iff mod_2_eq_odd)
  9.1071 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
  9.1072 +    by (auto simp: residue_primroot_def)
  9.1073 +  thus ?thesis using pow_eq by (auto simp: bij_betw_def)
  9.1074 +next
  9.1075 +  case False
  9.1076 +  thus ?thesis unfolding bij_betw_def
  9.1077 +  proof safe
  9.1078 +    from assms False have "m > 2" by auto
  9.1079 +    from assms \<open>m > 2\<close> have "totient m > 1" by (intro totient_gt_1) auto
  9.1080 +    from assms have [simp]: "ord m g = totient m"
  9.1081 +      by (simp add: residue_primroot_def)
  9.1082 +    from assms have "coprime m g" by (simp add: residue_primroot_def)
  9.1083 +    hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
  9.1084 +      by (intro inj_power_mod)
  9.1085 +    thus "inj_on (\<lambda>i. g ^ i mod m) (totatives (totient m))"
  9.1086 +      by (rule inj_on_subset)
  9.1087 +         (use assms \<open>totient m > 1\<close> in \<open>auto simp: totatives_less residue_primroot_def\<close>)
  9.1088 +
  9.1089 +    {
  9.1090 +      fix i assume i: "i \<in> totatives (totient m)"
  9.1091 +      from \<open>coprime m g\<close> and \<open>m > 2\<close> show "g ^ i mod m \<in> totatives m"
  9.1092 +        by (intro power_in_totatives) auto
  9.1093 +      show "residue_primroot m (g ^ i mod m)"
  9.1094 +        using i \<open>m > 2\<close> \<open>coprime m g\<close>
  9.1095 +        by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def)
  9.1096 +    }
  9.1097 +    {
  9.1098 +      fix x assume x: "x \<in> totatives m" "residue_primroot m x"
  9.1099 +      then obtain i where i: "i < totient m" "x = (g ^ i mod m)"
  9.1100 +        using assms residue_primroot_is_generator[of m g] by (auto simp: bij_betw_def)
  9.1101 +      from i x \<open>m > 2\<close> have "i > 0" by (intro Nat.gr0I) (auto simp: residue_primroot_1_iff)
  9.1102 +      have "totient m div gcd i (totient m) = totient m"
  9.1103 +        using x i \<open>coprime m g\<close> by (auto simp add: residue_primroot_def ord_power)
  9.1104 +      hence "coprime i (totient m)"
  9.1105 +        unfolding coprime_iff_gcd_eq_1 using assms by (subst (asm) dvd_div_eq_mult) auto
  9.1106 +      with i \<open>i > 0\<close> have "i \<in> totatives (totient m)" by (auto simp: totatives_def)
  9.1107 +      thus "x \<in> (\<lambda>i. g ^ i mod m) ` totatives (totient m)" using i by auto
  9.1108 +    }
  9.1109 +  qed
  9.1110 +qed
  9.1111 +
  9.1112 +text \<open>
  9.1113 +  It follows from the above statement that any residue ring modulo \<open>n\<close> that \<^emph>\<open>has\<close> primitive roots
  9.1114 +  has exactly $\varphi(\varphi(n))$ of them.
  9.1115 +\<close>
  9.1116 +corollary card_residue_primroots:
  9.1117 +  assumes "\<exists>g. residue_primroot m g"
  9.1118 +  shows   "card {g\<in>totatives m. residue_primroot m g} = totient (totient m)"
  9.1119 +proof (cases "m = 1")
  9.1120 +  case [simp]: True
  9.1121 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
  9.1122 +    by (auto simp: residue_primroot_def)
  9.1123 +  thus ?thesis by simp
  9.1124 +next
  9.1125 +  case False
  9.1126 +  from assms obtain g where g: "residue_primroot m g" by auto
  9.1127 +  hence "m \<noteq> 0" by (intro notI) auto
  9.1128 +  with \<open>m \<noteq> 1\<close> have "m > 1" by linarith
  9.1129 +  from this g have "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
  9.1130 +                      {g\<in>totatives m. residue_primroot m g}"
  9.1131 +    by (rule residue_primroot_bij_betw_primroots)
  9.1132 +  hence "card (totatives (totient m)) = card {g\<in>totatives m. residue_primroot m g}"
  9.1133 +    by (rule bij_betw_same_card)
  9.1134 +  thus ?thesis by (simp add: totient_def)
  9.1135 +qed
  9.1136 +
  9.1137 +corollary card_residue_primroots':
  9.1138 +  "card {g\<in>totatives m. residue_primroot m g} =
  9.1139 +     (if m \<in> cyclic_moduli then totient (totient m) else 0)"
  9.1140 +  by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots)
  9.1141 +
  9.1142 +text \<open>
  9.1143 +  As an example, we evaluate $\lambda(122200)$ using the prime factorisation.
  9.1144 +\<close>
  9.1145 +lemma "Carmichael 122200 = 1380"
  9.1146 +proof -
  9.1147 +  have "prime_factorization (2^3 * 5^2 * 13 * 47) = {#2, 2, 2, 5, 5, 13, 47::nat#}"
  9.1148 +    by (intro prime_factorization_eqI) auto
  9.1149 +  from eval_Carmichael[OF this] show "Carmichael 122200 = 1380"
  9.1150 +    by (simp add: lcm_nat_def gcd_non_0_nat)
  9.1151 +qed
  9.1152 +
  9.1153 +(* TODO: definition of index ("discrete logarithm") *)
  9.1154 +
  9.1155 +end
  9.1156 \ No newline at end of file
    10.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 02 15:52:14 2019 +0100
    10.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 04 12:16:03 2019 +0100
    10.3 @@ -398,7 +398,7 @@
    10.4    shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
    10.5    by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
    10.6  
    10.7 -theorem residue_prime_mult_group_has_gen :
    10.8 +theorem residue_prime_mult_group_has_gen:
    10.9   fixes p :: nat
   10.10   assumes prime_p : "prime p"
   10.11   shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
   10.12 @@ -455,4 +455,52 @@
   10.13    ultimately show ?thesis ..
   10.14  qed
   10.15  
   10.16 +
   10.17 +subsection \<open>Upper bound for the number of $n$-th roots\<close>
   10.18 +
   10.19 +lemma roots_mod_prime_bound:
   10.20 +  fixes n c p :: nat
   10.21 +  assumes "prime p" "n > 0"
   10.22 +  defines "A \<equiv> {x\<in>{..<p}. [x ^ n = c] (mod p)}"
   10.23 +  shows   "card A \<le> n"
   10.24 +proof -
   10.25 +  define R where "R = residue_ring (int p)"
   10.26 +  term monom
   10.27 +  from assms(1) interpret residues_prime p R
   10.28 +    by unfold_locales (simp_all add: R_def)
   10.29 +  interpret R: UP_domain R "UP R" by (unfold_locales)
   10.30 +
   10.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"
   10.32 +  have in_carrier: "int (c mod p) \<in> carrier R"
   10.33 +    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)
   10.34 +  
   10.35 +  have "deg R ?f = n"
   10.36 +    using assms in_carrier by (simp add: R.deg_minus_eq)
   10.37 +  hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
   10.38 +  have roots_bound: "finite {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<and>
   10.39 +                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
   10.40 +                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
   10.41 +  have subs: "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<subseteq>
   10.42 +                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
   10.43 +    using in_carrier by (auto simp: R.evalRR_simps)
   10.44 +  then have "card {x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<le>
   10.45 +               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
   10.46 +    using finite by (intro card_mono) auto
   10.47 +  also have "\<dots> \<le> n"
   10.48 +    using \<open>deg R ?f = n\<close> roots_bound by linarith
   10.49 +  also {
   10.50 +    fix x assume "x \<in> carrier R"
   10.51 +    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
   10.52 +      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
   10.53 +  }
   10.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)}"
   10.55 +    by (fastforce simp: cong_def zmod_int)
   10.56 +  also have "bij_betw int A {x \<in> carrier R. [x ^ n = int c] (mod p)}"
   10.57 +    by (rule bij_betwI[of int _ _ nat])
   10.58 +       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
   10.59 +  from bij_betw_same_card[OF this] have "card {x \<in> carrier R. [x ^ n = int c] (mod p)} = card A" ..
   10.60 +  finally show ?thesis .
   10.61 +qed
   10.62 +
   10.63 +
   10.64  end
    11.1 --- a/src/HOL/Number_Theory/Totient.thy	Sat Feb 02 15:52:14 2019 +0100
    11.2 +++ b/src/HOL/Number_Theory/Totient.thy	Mon Feb 04 12:16:03 2019 +0100
    11.3 @@ -62,6 +62,21 @@
    11.4    shows "n - 1 \<in> totatives n"
    11.5    using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
    11.6  
    11.7 +lemma power_in_totatives:
    11.8 +  assumes "m > 1" "coprime m g"
    11.9 +  shows   "g ^ i mod m \<in> totatives m"
   11.10 +proof -
   11.11 +  have "\<not>m dvd g ^ i"
   11.12 +  proof
   11.13 +    assume "m dvd g ^ i"
   11.14 +    hence "\<not>coprime m (g ^ i)"
   11.15 +      using \<open>m > 1\<close> by (subst coprime_absorb_left) auto
   11.16 +    with \<open>coprime m g\<close> show False by simp
   11.17 +  qed
   11.18 +  with assms show ?thesis
   11.19 +    by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
   11.20 +qed
   11.21 +
   11.22  lemma totatives_prime_power_Suc:
   11.23    assumes "prime p"
   11.24    shows   "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m) ` {0<..p^n}"
   11.25 @@ -198,6 +213,18 @@
   11.26  lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0"
   11.27    by (auto intro: Nat.gr0I)
   11.28  
   11.29 +lemma totient_gt_1:
   11.30 +  assumes "n > 2"
   11.31 +  shows   "totient n > 1"
   11.32 +proof -
   11.33 +  have "{1, n - 1} \<subseteq> totatives n"
   11.34 +    using assms coprime_diff_one_left_nat[of n] by (auto simp: totatives_def)
   11.35 +  hence "card {1, n - 1} \<le> card (totatives n)"
   11.36 +    by (intro card_mono) auto
   11.37 +  thus ?thesis using assms
   11.38 +    by (simp add: totient_def)
   11.39 +qed
   11.40 +
   11.41  lemma card_gcd_eq_totient:
   11.42    "n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)"
   11.43    unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq])
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Number_Theory/document/root.bib	Mon Feb 04 12:16:03 2019 +0100
    12.3 @@ -0,0 +1,10 @@
    12.4 +@book{apostol1976analytic,
    12.5 +	series = "Undergraduate {T}exts in {M}athematics",
    12.6 +	title = "Introduction to {A}nalytic {N}umber {T}heory",
    12.7 +	year = 1976,
    12.8 +	author = "Tom M. Apostol",
    12.9 +	publisher = "Springer-Verlag",
   12.10 +	doi = "10.1007/978-1-4757-5579-4",
   12.11 +	isbn = "978-0-387-90163-3"
   12.12 +}
   12.13 +
    13.1 --- a/src/HOL/Number_Theory/document/root.tex	Sat Feb 02 15:52:14 2019 +0100
    13.2 +++ b/src/HOL/Number_Theory/document/root.tex	Mon Feb 04 12:16:03 2019 +0100
    13.3 @@ -26,5 +26,8 @@
    13.4  
    13.5  \input{session}
    13.6  
    13.7 +\bibliographystyle{abbrv}
    13.8 +\bibliography{root}
    13.9 +
   13.10  \end{document}
   13.11