author Manuel Eberl Mon Feb 04 12:16:03 2019 +0100 (3 months ago) changeset 69785 9e326f6f8a24 parent 69784 24bbc4e30e5b child 69786 a5732629cc46
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
 CONTRIBUTORS file | annotate | diff | revisions NEWS file | annotate | diff | revisions src/HOL/Algebra/Multiplicative_Group.thy file | annotate | diff | revisions src/HOL/Computational_Algebra/Factorial_Ring.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Number_Theory/Number_Theory.thy file | annotate | diff | revisions src/HOL/Number_Theory/Pocklington.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residue_Primitive_Roots.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions src/HOL/Number_Theory/Totient.thy file | annotate | diff | revisions src/HOL/Number_Theory/document/root.bib file | annotate | diff | revisions src/HOL/Number_Theory/document/root.tex file | annotate | diff | revisions
     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"

     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.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.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.251 +  also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
8.252 +    using \<open>2 * k \<ge> Suc k\<close>
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.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.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