src/HOL/Number_Theory/Pocklington.thy
 author Manuel Eberl Mon Feb 04 12:16:03 2019 +0100 (4 months ago) changeset 69785 9e326f6f8a24 parent 69064 5840724b1d71 permissions -rw-r--r--
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
```     1 (*  Title:      HOL/Number_Theory/Pocklington.thy
```
```     2     Author:     Amine Chaieb, Manuel Eberl
```
```     3 *)
```
```     4
```
```     5 section \<open>Pocklington's Theorem for Primes\<close>
```
```     6
```
```     7 theory Pocklington
```
```     8 imports Residues
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Lemmas about previously defined terms\<close>
```
```    12
```
```    13 lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
```
```    14   apply (auto simp add: prime_nat_iff)
```
```    15    apply (rule coprimeI)
```
```    16    apply (auto dest: nat_dvd_not_less simp add: ac_simps)
```
```    17   apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
```
```    18   done
```
```    19
```
```    20 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
```
```    21 proof -
```
```    22   have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
```
```    23   then show ?thesis by simp
```
```    24 qed
```
```    25
```
```    26
```
```    27 subsection \<open>Some basic theorems about solving congruences\<close>
```
```    28
```
```    29 lemma cong_solve:
```
```    30   fixes n :: nat
```
```    31   assumes an: "coprime a n"
```
```    32   shows "\<exists>x. [a * x = b] (mod n)"
```
```    33 proof (cases "a = 0")
```
```    34   case True
```
```    35   with an show ?thesis
```
```    36     by (simp add: cong_def)
```
```    37 next
```
```    38   case False
```
```    39   from bezout_add_strong_nat [OF this]
```
```    40   obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
```
```    41   from dxy(1,2) have d1: "d = 1"
```
```    42     using assms coprime_common_divisor [of a n d] by simp
```
```    43   with dxy(3) have "a * x * b = (n * y + 1) * b"
```
```    44     by simp
```
```    45   then have "a * (x * b) = n * (y * b) + b"
```
```    46     by (auto simp: algebra_simps)
```
```    47   then have "a * (x * b) mod n = (n * (y * b) + b) mod n"
```
```    48     by simp
```
```    49   then have "a * (x * b) mod n = b mod n"
```
```    50     by (simp add: mod_add_left_eq)
```
```    51   then have "[a * (x * b) = b] (mod n)"
```
```    52     by (simp only: cong_def)
```
```    53   then show ?thesis by blast
```
```    54 qed
```
```    55
```
```    56 lemma cong_solve_unique:
```
```    57   fixes n :: nat
```
```    58   assumes an: "coprime a n" and nz: "n \<noteq> 0"
```
```    59   shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
```
```    60 proof -
```
```    61   from cong_solve[OF an] obtain x where x: "[a * x = b] (mod n)"
```
```    62     by blast
```
```    63   let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
```
```    64   let ?x = "x mod n"
```
```    65   from x have *: "[a * ?x = b] (mod n)"
```
```    66     by (simp add: cong_def mod_mult_right_eq[of a x n])
```
```    67   from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp
```
```    68   have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y
```
```    69   proof -
```
```    70     from Py(2) * have "[a * y = a * ?x] (mod n)"
```
```    71       by (simp add: cong_def)
```
```    72     then have "[y = ?x] (mod n)"
```
```    73       by (metis an cong_mult_lcancel_nat)
```
```    74     with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
```
```    75     show ?thesis
```
```    76       by (simp add: cong_def)
```
```    77   qed
```
```    78   with Px show ?thesis by blast
```
```    79 qed
```
```    80
```
```    81 lemma cong_solve_unique_nontrivial:
```
```    82   fixes p :: nat
```
```    83   assumes p: "prime p"
```
```    84     and pa: "coprime p a"
```
```    85     and x0: "0 < x"
```
```    86     and xp: "x < p"
```
```    87   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
```
```    88 proof -
```
```    89   from pa have ap: "coprime a p"
```
```    90     by (simp add: ac_simps)
```
```    91   from x0 xp p have px: "coprime x p"
```
```    92     by (auto simp add: prime_nat_iff'' ac_simps)
```
```    93   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
```
```    94     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
```
```    95   have "y \<noteq> 0"
```
```    96   proof
```
```    97     assume "y = 0"
```
```    98     with y(2) have "p dvd a"
```
```    99       using cong_dvd_iff by auto
```
```   100     with not_prime_1 p pa show False
```
```   101       by (auto simp add: gcd_nat.order_iff)
```
```   102   qed
```
```   103   with y show ?thesis
```
```   104     by blast
```
```   105 qed
```
```   106
```
```   107 lemma cong_unique_inverse_prime:
```
```   108   fixes p :: nat
```
```   109   assumes "prime p" and "0 < x" and "x < p"
```
```   110   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
```
```   111   by (rule cong_solve_unique_nontrivial) (use assms in simp_all)
```
```   112
```
```   113 lemma chinese_remainder_coprime_unique:
```
```   114   fixes a :: nat
```
```   115   assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
```
```   116     and ma: "coprime m a" and nb: "coprime n b"
```
```   117   shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   118 proof -
```
```   119   let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   120   from binary_chinese_remainder_unique_nat[OF ab az bz]
```
```   121   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
```
```   122     by blast
```
```   123   from ma nb x have "coprime x a" "coprime x b"
```
```   124     using cong_imp_coprime cong_sym by blast+
```
```   125   then have "coprime x (a*b)"
```
```   126     by simp
```
```   127   with x show ?thesis
```
```   128     by blast
```
```   129 qed
```
```   130
```
```   131
```
```   132 subsection \<open>Lucas's theorem\<close>
```
```   133
```
```   134 lemma lucas_coprime_lemma:
```
```   135   fixes n :: nat
```
```   136   assumes m: "m \<noteq> 0" and am: "[a^m = 1] (mod n)"
```
```   137   shows "coprime a n"
```
```   138 proof -
```
```   139   consider "n = 1" | "n = 0" | "n > 1" by arith
```
```   140   then show ?thesis
```
```   141   proof cases
```
```   142     case 1
```
```   143     then show ?thesis by simp
```
```   144   next
```
```   145     case 2
```
```   146     with am m show ?thesis
```
```   147       by simp
```
```   148   next
```
```   149     case 3
```
```   150     from m obtain m' where m': "m = Suc m'" by (cases m) blast+
```
```   151     have "d = 1" if d: "d dvd a" "d dvd n" for d
```
```   152     proof -
```
```   153       from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1"
```
```   154         by (simp add: cong_def)
```
```   155       from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m"
```
```   156         by (simp add: m')
```
```   157       from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
```
```   158         by simp
```
```   159     qed
```
```   160     then show ?thesis
```
```   161       by (auto intro: coprimeI)
```
```   162   qed
```
```   163 qed
```
```   164
```
```   165 lemma lucas_weak:
```
```   166   fixes n :: nat
```
```   167   assumes n: "n \<ge> 2"
```
```   168     and an: "[a ^ (n - 1) = 1] (mod n)"
```
```   169     and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
```
```   170   shows "prime n"
```
```   171 proof (rule totient_imp_prime)
```
```   172   show "totient n = n - 1"
```
```   173   proof (rule ccontr)
```
```   174     have "[a ^ totient n = 1] (mod n)"
```
```   175       by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"]) (use n an in auto)
```
```   176     moreover assume "totient n \<noteq> n - 1"
```
```   177     then have "totient n > 0" "totient n < n - 1"
```
```   178       using \<open>n \<ge> 2\<close> and totient_less[of n] by simp_all
```
```   179     ultimately show False
```
```   180       using nm by auto
```
```   181   qed
```
```   182 qed (use n in auto)
```
```   183
```
```   184 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
```
```   185   by (metis ex_least_nat_le not_less0)
```
```   186
```
```   187 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
```
```   188   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   189 proof
```
```   190   show ?lhs if ?rhs
```
```   191     using that by blast
```
```   192   show ?rhs if ?lhs
```
```   193   proof -
```
```   194     from \<open>?lhs\<close> obtain n where n: "P n" by blast
```
```   195     let ?x = "Least P"
```
```   196     have "\<not> P m" if "m < ?x" for m
```
```   197       by (rule not_less_Least[OF that])
```
```   198     with LeastI_ex[OF \<open>?lhs\<close>] show ?thesis
```
```   199       by blast
```
```   200   qed
```
```   201 qed
```
```   202
```
```   203 theorem lucas:
```
```   204   assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
```
```   205     and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
```
```   206   shows "prime n"
```
```   207 proof-
```
```   208   from n2 have n01: "n \<noteq> 0" "n \<noteq> 1" "n - 1 \<noteq> 0"
```
```   209     by arith+
```
```   210   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
```
```   211     by simp
```
```   212   from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime an1
```
```   213   have an: "coprime a n" "coprime (a ^ (n - 1)) n"
```
```   214     using \<open>n \<ge> 2\<close> by simp_all
```
```   215   have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "\<exists>m. ?P m")
```
```   216   proof -
```
```   217     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
```
```   218       m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k"
```
```   219       by blast
```
```   220     have False if nm1: "(n - 1) mod m > 0"
```
```   221     proof -
```
```   222       from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
```
```   223       let ?y = "a^ ((n - 1) div m * m)"
```
```   224       note mdeq = div_mult_mod_eq[of "(n - 1)" m]
```
```   225       have yn: "coprime ?y n"
```
```   226         using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
```
```   227       have "?y mod n = (a^m)^((n - 1) div m) mod n"
```
```   228         by (simp add: algebra_simps power_mult)
```
```   229       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
```
```   230         using power_mod[of "a^m" n "(n - 1) div m"] by simp
```
```   231       also have "\<dots> = 1" using m(3)[unfolded cong_def onen] onen
```
```   232         by (metis power_one)
```
```   233       finally have *: "?y mod n = 1"  .
```
```   234       have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
```
```   235         using an1[unfolded cong_def onen] onen
```
```   236           div_mult_mod_eq[of "(n - 1)" m, symmetric]
```
```   237         by (simp add:power_add[symmetric] cong_def * del: One_nat_def)
```
```   238       have "[a ^ ((n - 1) mod m) = 1] (mod n)"
```
```   239         by (metis cong_mult_rcancel_nat mult.commute ** yn)
```
```   240       with m(4)[rule_format, OF th0] nm1
```
```   241         less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] show ?thesis
```
```   242         by blast
```
```   243     qed
```
```   244     then have "(n - 1) mod m = 0" by auto
```
```   245     then have mn: "m dvd n - 1" by presburger
```
```   246     then obtain r where r: "n - 1 = m * r"
```
```   247       unfolding dvd_def by blast
```
```   248     from n01 r m(2) have r01: "r \<noteq> 0" "r \<noteq> 1" by auto
```
```   249     obtain p where p: "prime p" "p dvd r"
```
```   250       by (metis prime_factor_nat r01(2))
```
```   251     then have th: "prime p \<and> p dvd n - 1"
```
```   252       unfolding r by (auto intro: dvd_mult)
```
```   253     from r have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n"
```
```   254       by (simp add: power_mult)
```
```   255     also have "\<dots> = (a^(m*(r div p))) mod n"
```
```   256       using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
```
```   257     also have "\<dots> = ((a^m)^(r div p)) mod n"
```
```   258       by (simp add: power_mult)
```
```   259     also have "\<dots> = ((a^m mod n)^(r div p)) mod n"
```
```   260       using power_mod ..
```
```   261     also from m(3) onen have "\<dots> = 1"
```
```   262       by (simp add: cong_def)
```
```   263     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
```
```   264       using onen by (simp add: cong_def)
```
```   265     with pn th show ?thesis by blast
```
```   266   qed
```
```   267   then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
```
```   268     by blast
```
```   269   then show ?thesis by (rule lucas_weak[OF n2 an1])
```
```   270 qed
```
```   271
```
```   272
```
```   273 subsection \<open>Definition of the order of a number mod \<open>n\<close>\<close>
```
```   274
```
```   275 definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
```
```   276
```
```   277 text \<open>This has the expected properties.\<close>
```
```   278
```
```   279 lemma coprime_ord:
```
```   280   fixes n::nat
```
```   281   assumes "coprime n a"
```
```   282   shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> [a^ m \<noteq> 1] (mod n))"
```
```   283 proof-
```
```   284   let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
```
```   285   from bigger_prime[of a] obtain p where p: "prime p" "a < p"
```
```   286     by blast
```
```   287   from assms have o: "ord n a = Least ?P"
```
```   288     by (simp add: ord_def)
```
```   289   have ex: "\<exists>m>0. ?P m"
```
```   290   proof (cases "n \<ge> 2")
```
```   291     case True
```
```   292     moreover from assms have "coprime a n"
```
```   293       by (simp add: ac_simps)
```
```   294     then have "[a ^ totient n = 1] (mod n)"
```
```   295       by (rule euler_theorem)
```
```   296     ultimately show ?thesis
```
```   297       by (auto intro: exI [where x = "totient n"])
```
```   298   next
```
```   299     case False
```
```   300     then have "n = 0 \<or> n = 1"
```
```   301       by auto
```
```   302     with assms show ?thesis
```
```   303       by auto
```
```   304   qed
```
```   305   from nat_exists_least_iff'[of ?P] ex assms show ?thesis
```
```   306     unfolding o[symmetric] by auto
```
```   307 qed
```
```   308
```
```   309 text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close>
```
```   310 lemma ord_works: "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))"
```
```   311   for n :: nat
```
```   312   by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_def\<close>)
```
```   313
```
```   314 lemma ord: "[a^(ord n a) = 1] (mod n)"
```
```   315   for n :: nat
```
```   316   using ord_works by blast
```
```   317
```
```   318 lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> \<not> [a^m = 1] (mod n)"
```
```   319   for n :: nat
```
```   320   using ord_works by blast
```
```   321
```
```   322 lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> \<not> coprime n a"
```
```   323   for n :: nat
```
```   324   by (cases "coprime n a") (simp add: coprime_ord, simp add: ord_def)
```
```   325
```
```   326 lemma divides_rexp: "x dvd y \<Longrightarrow> x dvd (y ^ Suc n)"
```
```   327   for x y :: nat
```
```   328   by (simp add: dvd_mult2[of x y])
```
```   329
```
```   330 lemma ord_divides:"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d"
```
```   331   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   332   for n :: nat
```
```   333 proof
```
```   334   assume ?rhs
```
```   335   then obtain k where "d = ord n a * k"
```
```   336     unfolding dvd_def by blast
```
```   337   then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
```
```   338     by (simp add : cong_def power_mult power_mod)
```
```   339   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
```
```   340     using ord[of a n, unfolded cong_def]
```
```   341     by (simp add: cong_def power_mod)
```
```   342   finally show ?lhs .
```
```   343 next
```
```   344   assume ?lhs
```
```   345   show ?rhs
```
```   346   proof (cases "coprime n a")
```
```   347     case prem: False
```
```   348     then have o: "ord n a = 0" by (simp add: ord_def)
```
```   349     show ?thesis
```
```   350     proof (cases d)
```
```   351       case 0
```
```   352       with o prem show ?thesis by (simp add: cong_def)
```
```   353     next
```
```   354       case (Suc d')
```
```   355       then have d0: "d \<noteq> 0" by simp
```
```   356       from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
```
```   357         by (auto elim: not_coprimeE)
```
```   358       from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
```
```   359         using prem d0 lucas_coprime_lemma
```
```   360         by (auto elim: not_coprimeE simp add: ac_simps)
```
```   361       then have "a ^ d + n * q1 - n * q2 = 1" by simp
```
```   362       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
```
```   363         by metis
```
```   364       with p(3) have False by simp
```
```   365       then show ?thesis ..
```
```   366     qed
```
```   367   next
```
```   368     case H: True
```
```   369     let ?o = "ord n a"
```
```   370     let ?q = "d div ord n a"
```
```   371     let ?r = "d mod ord n a"
```
```   372     have eqo: "[(a^?o)^?q = 1] (mod n)"
```
```   373       using cong_pow ord_works by fastforce
```
```   374     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
```
```   375     then have opos: "?o > 0" by simp
```
```   376     from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close>
```
```   377     have "[a^(?o*?q + ?r) = 1] (mod n)"
```
```   378       by (simp add: cong_def mult.commute)
```
```   379     then have "[(a^?o)^?q * (a^?r) = 1] (mod n)"
```
```   380       by (simp add: cong_def power_mult[symmetric] power_add[symmetric])
```
```   381     then have th: "[a^?r = 1] (mod n)"
```
```   382       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
```
```   383       by (simp add: cong_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
```
```   384     show ?thesis
```
```   385     proof (cases "?r = 0")
```
```   386       case True
```
```   387       then show ?thesis by (simp add: dvd_eq_mod_eq_0)
```
```   388     next
```
```   389       case False
```
```   390       with mod_less_divisor[OF opos, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
```
```   391       from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
```
```   392       show ?thesis by blast
```
```   393     qed
```
```   394   qed
```
```   395 qed
```
```   396
```
```   397 lemma order_divides_totient:
```
```   398   "ord n a dvd totient n" if "coprime n a"
```
```   399   using that euler_theorem [of a n]
```
```   400   by (simp add: ord_divides [symmetric] ac_simps)
```
```   401
```
```   402 lemma order_divides_expdiff:
```
```   403   fixes n::nat and a::nat assumes na: "coprime n a"
```
```   404   shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   405 proof -
```
```   406   have th: "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   407     if na: "coprime n a" and ed: "(e::nat) \<le> d"
```
```   408     for n a d e :: nat
```
```   409   proof -
```
```   410     from na ed have "\<exists>c. d = e + c" by presburger
```
```   411     then obtain c where c: "d = e + c" ..
```
```   412     from na have an: "coprime a n"
```
```   413       by (simp add: ac_simps)
```
```   414     then have aen: "coprime (a ^ e) n"
```
```   415       by (cases "e > 0") simp_all
```
```   416     from an have acn: "coprime (a ^ c) n"
```
```   417       by (cases "c > 0") simp_all
```
```   418     from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
```
```   419       by simp
```
```   420     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
```
```   421     also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
```
```   422       using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp
```
```   423     also have "\<dots> \<longleftrightarrow> ord n a dvd c"
```
```   424       by (simp only: ord_divides)
```
```   425     also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
```
```   426       by (auto simp add: cong_altdef_nat)
```
```   427     finally show ?thesis
```
```   428       using c by simp
```
```   429   qed
```
```   430   consider "e \<le> d" | "d \<le> e" by arith
```
```   431   then show ?thesis
```
```   432   proof cases
```
```   433     case 1
```
```   434     with na show ?thesis by (rule th)
```
```   435   next
```
```   436     case 2
```
```   437     from th[OF na this] show ?thesis
```
```   438       by (metis cong_sym)
```
```   439   qed
```
```   440 qed
```
```   441
```
```   442 lemma ord_not_coprime [simp]: "\<not>coprime n a \<Longrightarrow> ord n a = 0"
```
```   443   by (simp add: ord_def)
```
```   444
```
```   445 lemma ord_1 [simp]: "ord 1 n = 1"
```
```   446 proof -
```
```   447   have "(LEAST k. k > 0) = (1 :: nat)"
```
```   448     by (rule Least_equality) auto
```
```   449   thus ?thesis by (simp add: ord_def)
```
```   450 qed
```
```   451
```
```   452 lemma ord_1_right [simp]: "ord (n::nat) 1 = 1"
```
```   453   using ord_divides[of 1 1 n] by simp
```
```   454
```
```   455 lemma ord_Suc_0_right [simp]: "ord (n::nat) (Suc 0) = 1"
```
```   456   using ord_divides[of 1 1 n] by simp
```
```   457
```
```   458 lemma ord_0_nat [simp]: "ord 0 (n :: nat) = (if n = 1 then 1 else 0)"
```
```   459 proof -
```
```   460   have "(LEAST k. k > 0) = (1 :: nat)"
```
```   461     by (rule Least_equality) auto
```
```   462   thus ?thesis by (auto simp: ord_def)
```
```   463 qed
```
```   464
```
```   465 lemma ord_0_right_nat [simp]: "ord (n :: nat) 0 = (if n = 1 then 1 else 0)"
```
```   466 proof -
```
```   467   have "(LEAST k. k > 0) = (1 :: nat)"
```
```   468     by (rule Least_equality) auto
```
```   469   thus ?thesis by (auto simp: ord_def)
```
```   470 qed
```
```   471
```
```   472 lemma ord_divides': "[a ^ d = Suc 0] (mod n) = (ord n a dvd d)"
```
```   473   using ord_divides[of a d n] by simp
```
```   474
```
```   475 lemma ord_Suc_0 [simp]: "ord (Suc 0) n = 1"
```
```   476   using ord_1[where 'a = nat] by (simp del: ord_1)
```
```   477
```
```   478 lemma ord_mod [simp]: "ord n (k mod n) = ord n k"
```
```   479   by (cases "n = 0") (auto simp add: ord_def cong_def power_mod)
```
```   480
```
```   481 lemma ord_gt_0_iff [simp]: "ord (n::nat) x > 0 \<longleftrightarrow> coprime n x"
```
```   482   using ord_eq_0[of n x] by auto
```
```   483
```
```   484 lemma ord_eq_Suc_0_iff: "ord n (x::nat) = Suc 0 \<longleftrightarrow> [x = 1] (mod n)"
```
```   485   using ord_divides[of x 1 n] by (auto simp: ord_divides')
```
```   486
```
```   487 lemma ord_cong:
```
```   488   assumes "[k1 = k2] (mod n)"
```
```   489   shows   "ord n k1 = ord n k2"
```
```   490 proof -
```
```   491   have "ord n (k1 mod n) = ord n (k2 mod n)"
```
```   492     by (simp only: assms[unfolded cong_def])
```
```   493   thus ?thesis by simp
```
```   494 qed
```
```   495
```
```   496 lemma ord_nat_code [code_unfold]:
```
```   497   "ord n a =
```
```   498      (if n = 0 then if a = 1 then 1 else 0 else
```
```   499         if coprime n a then Min (Set.filter (\<lambda>k. [a ^ k = 1] (mod n)) {0<..n}) else 0)"
```
```   500 proof (cases "coprime n a \<and> n > 0")
```
```   501   case True
```
```   502   define A where "A = {k\<in>{0<..n}. [a ^ k = 1] (mod n)}"
```
```   503   define k where "k = (LEAST k. k > 0 \<and> [a ^ k = 1] (mod n))"
```
```   504   have totient: "totient n \<in> A"
```
```   505     using euler_theorem[of a n] True
```
```   506     by (auto simp: A_def coprime_commute intro!: Nat.gr0I totient_le)
```
```   507   moreover have "finite A" by (auto simp: A_def)
```
```   508   ultimately have *: "Min A \<in> A" and "\<forall>y. y \<in> A \<longrightarrow> Min A \<le> y"
```
```   509     by (auto intro: Min_in)
```
```   510
```
```   511   have "k > 0 \<and> [a ^ k = 1] (mod n)"
```
```   512     unfolding k_def by (rule LeastI[of _ "totient n"]) (use totient in \<open>auto simp: A_def\<close>)
```
```   513   moreover have "k \<le> totient n"
```
```   514     unfolding k_def by (intro Least_le) (use totient in \<open>auto simp: A_def\<close>)
```
```   515   ultimately have "k \<in> A" using totient_le[of n] by (auto simp: A_def)
```
```   516   hence "Min A \<le> k" by (intro Min_le) (auto simp: \<open>finite A\<close>)
```
```   517   moreover from * have "k \<le> Min A"
```
```   518     unfolding k_def by (intro Least_le) (auto simp: A_def)
```
```   519   ultimately show ?thesis using True by (simp add: ord_def k_def A_def Set.filter_def)
```
```   520 qed auto
```
```   521
```
```   522 theorem ord_modulus_mult_coprime:
```
```   523   fixes x :: nat
```
```   524   assumes "coprime m n"
```
```   525   shows   "ord (m * n) x = lcm (ord m x) (ord n x)"
```
```   526 proof (intro dvd_antisym)
```
```   527   have "[x ^ lcm (ord m x) (ord n x) = 1] (mod (m * n))"
```
```   528     using assms by (intro coprime_cong_mult_nat assms) (auto simp: ord_divides')
```
```   529   thus "ord (m * n) x dvd lcm (ord m x) (ord n x)"
```
```   530     by (simp add: ord_divides')
```
```   531 next
```
```   532   show "lcm (ord m x) (ord n x) dvd ord (m * n) x"
```
```   533   proof (intro lcm_least)
```
```   534     show "ord m x dvd ord (m * n) x"
```
```   535       using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 m n] assms
```
```   536       by (simp add: ord_divides')
```
```   537     show "ord n x dvd ord (m * n) x"
```
```   538       using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 n m] assms
```
```   539       by (simp add: ord_divides' mult.commute)
```
```   540   qed
```
```   541 qed
```
```   542
```
```   543 corollary ord_modulus_prod_coprime:
```
```   544   assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
```
```   545   shows   "ord (\<Prod>i\<in>A. f i :: nat) x = (LCM i\<in>A. ord (f i) x)"
```
```   546   using assms by (induction A rule: finite_induct)
```
```   547                  (simp, simp, subst ord_modulus_mult_coprime, auto intro!: prod_coprime_right)
```
```   548
```
```   549 lemma ord_power_aux:
```
```   550   fixes m x k a :: nat
```
```   551   defines "l \<equiv> ord m a"
```
```   552   shows   "ord m (a ^ k) * gcd k l = l"
```
```   553 proof (rule dvd_antisym)
```
```   554   have "[a ^ lcm k l = 1] (mod m)"
```
```   555     unfolding ord_divides by (simp add: l_def)
```
```   556   also have "lcm k l = k * (l div gcd k l)"
```
```   557     by (simp add: lcm_nat_def div_mult_swap)
```
```   558   finally have "ord m (a ^ k) dvd l div gcd k l"
```
```   559     unfolding ord_divides [symmetric] by (simp add: power_mult [symmetric])
```
```   560   thus "ord m (a ^ k) * gcd k l dvd l"
```
```   561     by (cases "l = 0") (auto simp: dvd_div_iff_mult)
```
```   562
```
```   563   have "[(a ^ k) ^ ord m (a ^ k) = 1] (mod m)"
```
```   564     by (rule ord)
```
```   565   also have "(a ^ k) ^ ord m (a ^ k) = a ^ (k * ord m (a ^ k))"
```
```   566     by (simp add: power_mult)
```
```   567   finally have "ord m a dvd k * ord m (a ^ k)"
```
```   568     by (simp add: ord_divides')
```
```   569   hence "l dvd gcd (k * ord m (a ^ k)) (l * ord m (a ^ k))"
```
```   570     by (intro gcd_greatest dvd_triv_left) (auto simp: l_def ord_divides')
```
```   571   also have "gcd (k * ord m (a ^ k)) (l * ord m (a ^ k)) = ord m (a ^ k) * gcd k l"
```
```   572     by (subst gcd_mult_distrib_nat) (auto simp: mult_ac)
```
```   573   finally show "l dvd ord m (a ^ k) * gcd k l" .
```
```   574 qed
```
```   575
```
```   576 theorem ord_power: "coprime m a \<Longrightarrow> ord m (a ^ k :: nat) = ord m a div gcd k (ord m a)"
```
```   577   using ord_power_aux[of m a k] by (metis div_mult_self_is_m gcd_pos_nat ord_eq_0)
```
```   578
```
```   579 lemma inj_power_mod:
```
```   580   assumes "coprime n (a :: nat)"
```
```   581   shows   "inj_on (\<lambda>k. a ^ k mod n) {..<ord n a}"
```
```   582 proof
```
```   583   fix k l assume *: "k \<in> {..<ord n a}" "l \<in> {..<ord n a}" "a ^ k mod n = a ^ l mod n"
```
```   584   have "k = l" if "k < l" "l < ord n a" "[a ^ k = a ^ l] (mod n)" for k l
```
```   585   proof -
```
```   586     have "l = k + (l - k)" using that by simp
```
```   587     also have "a ^ \<dots> = a ^ k * a ^ (l - k)"
```
```   588       by (simp add: power_add)
```
```   589     also have "[\<dots> = a ^ l * a ^ (l - k)] (mod n)"
```
```   590       using that by (intro cong_mult) auto
```
```   591     finally have "[a ^ l * a ^ (l - k) = a ^ l * 1] (mod n)"
```
```   592       by (simp add: cong_sym_eq)
```
```   593     with assms have "[a ^ (l - k) = 1] (mod n)"
```
```   594       by (subst (asm) cong_mult_lcancel_nat) (auto simp: coprime_commute)
```
```   595     hence "ord n a dvd l - k"
```
```   596       by (simp add: ord_divides')
```
```   597     from dvd_imp_le[OF this] and \<open>l < ord n a\<close> have "l - k = 0"
```
```   598       by (cases "l - k = 0") auto
```
```   599     with \<open>k < l\<close> show "k = l" by simp
```
```   600   qed
```
```   601   from this[of k l] and this[of l k] and * show "k = l"
```
```   602     by (cases k l rule: linorder_cases) (auto simp: cong_def)
```
```   603 qed
```
```   604
```
```   605 lemma ord_eq_2_iff: "ord n (x :: nat) = 2 \<longleftrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
```
```   606 proof
```
```   607   assume x: "[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
```
```   608   hence "coprime n x"
```
```   609     by (metis coprime_commute lucas_coprime_lemma zero_neq_numeral)
```
```   610   with x have "ord n x dvd 2" "ord n x \<noteq> 1" "ord n x > 0"
```
```   611     by (auto simp: ord_divides' ord_eq_Suc_0_iff)
```
```   612   thus "ord n x = 2" by (auto dest!: dvd_imp_le simp del: ord_gt_0_iff)
```
```   613 qed (use ord_divides[of _ 2] ord_divides[of _ 1] in auto)
```
```   614
```
```   615 lemma square_mod_8_eq_1_iff: "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> odd (x :: nat)"
```
```   616 proof -
```
```   617   have "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> ((x mod 8)\<^sup>2 mod 8 = 1)"
```
```   618     by (simp add: power_mod cong_def)
```
```   619   also have "\<dots> \<longleftrightarrow> x mod 8 \<in> {1, 3, 5, 7}"
```
```   620   proof
```
```   621     assume x: "(x mod 8)\<^sup>2 mod 8 = 1"
```
```   622     have "x mod 8 \<in> {..<8}" by simp
```
```   623     also have "{..<8} = {0, 1, 2, 3, 4, 5, 6, 7::nat}"
```
```   624       by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
```
```   625     finally have x_cases: "x mod 8 \<in> {0, 1, 2, 3, 4, 5, 6, 7}" .
```
```   626     from x have "x mod 8 \<notin> {0, 2, 4, 6}"
```
```   627       using x by (auto intro: Nat.gr0I)
```
```   628     with x_cases show "x mod 8 \<in> {1, 3, 5, 7}" by simp
```
```   629   qed auto
```
```   630   also have "\<dots> \<longleftrightarrow> odd (x mod 8)"
```
```   631     by (auto elim!: oddE)
```
```   632   also have "\<dots> \<longleftrightarrow> odd x"
```
```   633     by presburger
```
```   634   finally show ?thesis .
```
```   635 qed
```
```   636
```
```   637 lemma ord_twopow_aux:
```
```   638   assumes "k \<ge> 3" and "odd (x :: nat)"
```
```   639   shows   "[x ^ (2 ^ (k - 2)) = 1] (mod (2 ^ k))"
```
```   640   using assms(1)
```
```   641 proof (induction k rule: dec_induct)
```
```   642   case base
```
```   643   from assms have "[x\<^sup>2 = 1] (mod 8)"
```
```   644     by (subst square_mod_8_eq_1_iff) auto
```
```   645   thus ?case by simp
```
```   646 next
```
```   647   case (step k)
```
```   648   define k' where "k' = k - 2"
```
```   649   have k: "k = Suc (Suc k')"
```
```   650     using \<open>k \<ge> 3\<close> by (simp add: k'_def)
```
```   651   from \<open>k \<ge> 3\<close> have "2 * k \<ge> Suc k" by presburger
```
```   652
```
```   653   from \<open>odd x\<close> have "x > 0" by (intro Nat.gr0I) auto
```
```   654   from step.IH have "2 ^ k dvd (x ^ (2 ^ (k - 2)) - 1)"
```
```   655     by (rule cong_to_1_nat)
```
```   656   then obtain t where "x ^ (2 ^ (k - 2)) - 1 = t * 2 ^ k"
```
```   657     by auto
```
```   658   hence "x ^ (2 ^ (k - 2)) = t * 2 ^ k + 1"
```
```   659     by (metis \<open>0 < x\<close> add.commute add_diff_inverse_nat less_one neq0_conv power_eq_0_iff)
```
```   660   hence "(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2"
```
```   661     by (rule arg_cong)
```
```   662   hence "[(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2] (mod (2 ^ Suc k))"
```
```   663     by simp
```
```   664   also have "(x ^ (2 ^ (k - 2))) ^ 2 = x ^ (2 ^ (k - 1))"
```
```   665     by (simp_all add: power_even_eq[symmetric] power_mult k )
```
```   666   also have "(t * 2 ^ k + 1) ^ 2 = t\<^sup>2 * 2 ^ (2 * k) + t * 2 ^ Suc k + 1"
```
```   667     by (subst power2_eq_square)
```
```   668        (auto simp: algebra_simps k power2_eq_square[of t]
```
```   669                    power_even_eq[symmetric] power_add [symmetric])
```
```   670   also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
```
```   671     using \<open>2 * k \<ge> Suc k\<close>
```
```   672     by (intro cong_add)
```
```   673        (auto simp: cong_0_iff intro: dvd_mult[OF le_imp_power_dvd] simp del: power_Suc)
```
```   674   finally show ?case by simp
```
```   675 qed
```
```   676
```
```   677 lemma ord_twopow_3_5:
```
```   678   assumes "k \<ge> 3" "x mod 8 \<in> {3, 5 :: nat}"
```
```   679   shows   "ord (2 ^ k) x = 2 ^ (k - 2)"
```
```   680   using assms(1)
```
```   681 proof (induction k rule: less_induct)
```
```   682   have "x mod 8 = 3 \<or> x mod 8 = 5" using assms by auto
```
```   683   hence "odd x" by presburger
```
```   684   case (less k)
```
```   685   from \<open>k \<ge> 3\<close> consider "k = 3" | "k = 4" | "k \<ge> 5" by force
```
```   686   thus ?case
```
```   687   proof cases
```
```   688     case 1
```
```   689     thus ?thesis using assms
```
```   690       by (auto simp: ord_eq_2_iff cong_def simp flip: power_mod[of x])
```
```   691   next
```
```   692     case 2
```
```   693     from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
```
```   694     hence x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
```
```   695       using mod_double_modulus[of 8 x] by auto
```
```   696     hence "[x ^ 4 = 1] (mod 16)" using assms
```
```   697       by (auto simp: cong_def simp flip: power_mod[of x])
```
```   698     hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
```
```   699     then obtain l where l: "ord 16 x = 2 ^ l" "l \<le> 2"
```
```   700       by (subst (asm) divides_primepow_nat) auto
```
```   701
```
```   702     have "[x ^ 2 \<noteq> 1] (mod 16)"
```
```   703       using x' by (auto simp: cong_def simp flip: power_mod[of x])
```
```   704     hence "\<not>ord 16 x dvd 2" by (simp add: ord_divides')
```
```   705     with l have "l = 2"
```
```   706       using le_imp_power_dvd[of l 1 2] by (cases "l \<le> 1") auto
```
```   707     with l show ?thesis by (simp add: \<open>k = 4\<close>)
```
```   708   next
```
```   709     case 3
```
```   710     define k' where "k' = k - 2"
```
```   711     have k': "k' \<ge> 2" and [simp]: "k = Suc (Suc k')"
```
```   712       using 3 by (simp_all add: k'_def)
```
```   713     have IH: "ord (2 ^ k') x = 2 ^ (k' - 2)" "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
```
```   714       using less.IH[of k'] less.IH[of "Suc k'"] 3 by simp_all
```
```   715     from IH have cong: "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ k'))"
```
```   716       by (simp_all add: ord_divides')
```
```   717     have notcong: "[x ^ (2 ^ (k' - 2)) \<noteq> 1] (mod (2 ^ Suc k'))"
```
```   718     proof
```
```   719       assume "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ Suc k'))"
```
```   720       hence "ord (2 ^ Suc k') x dvd 2 ^ (k' - 2)"
```
```   721         by (simp add: ord_divides')
```
```   722       also have "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
```
```   723         using IH by simp
```
```   724       finally have "k' - 1 \<le> k' - 2"
```
```   725         by (rule power_dvd_imp_le) auto
```
```   726       with \<open>k' \<ge> 2\<close> show False by simp
```
```   727     qed
```
```   728
```
```   729     have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
```
```   730       using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
```
```   731     with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
```
```   732       using mod_double_modulus[of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
```
```   733
```
```   734     hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
```
```   735            x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
```
```   736       using mod_double_modulus[of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
```
```   737     hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
```
```   738     proof
```
```   739       assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
```
```   740       have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
```
```   741         by simp
```
```   742       also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'] (mod 2 ^ k)"
```
```   743         by (subst *) auto
```
```   744       finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
```
```   745         by (rule cong_pow)
```
```   746       hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
```
```   747         by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
```
```   748       also have "Suc (k' - 2) = k' - 1"
```
```   749         using k' by simp
```
```   750       also have "(1 + 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ (2 * k')"
```
```   751         by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
```
```   752       also have "(2 ^ k :: nat) dvd 2 ^ (2 * k')"
```
```   753         using k' by (intro le_imp_power_dvd) auto
```
```   754       hence "[1 + 2 ^ (k - 1) + 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + (0 :: nat)] (mod 2 ^ k)"
```
```   755         by (intro cong_add) (auto simp: cong_0_iff)
```
```   756       finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
```
```   757         by simp
```
```   758     next
```
```   759       assume *: "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
```
```   760       have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
```
```   761         by simp
```
```   762       also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 3 * 2 ^ k'] (mod 2 ^ k)"
```
```   763         by (subst *) auto
```
```   764       finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
```
```   765         by (rule cong_pow)
```
```   766       hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
```
```   767         by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
```
```   768       also have "Suc (k' - 2) = k' - 1"
```
```   769         using k' by simp
```
```   770       also have "(1 + 3 * 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k')"
```
```   771         by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
```
```   772       also have "(2 ^ k :: nat) dvd 9 * 2 ^ (2 * k')"
```
```   773         using k' by (intro dvd_mult le_imp_power_dvd) auto
```
```   774       hence "[1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + 0 + (0 :: nat)]
```
```   775                (mod 2 ^ k)"
```
```   776         by (intro cong_add) (auto simp: cong_0_iff)
```
```   777       finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
```
```   778         by simp
```
```   779     qed
```
```   780
```
```   781     have notcong': "[x ^ 2 ^ (k - 3) \<noteq> 1] (mod 2 ^ k)"
```
```   782     proof
```
```   783       assume "[x ^ 2 ^ (k - 3) = 1] (mod 2 ^ k)"
```
```   784       hence "[x ^ 2 ^ (k' - 1) - x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1) - 1] (mod 2 ^ k)"
```
```   785         by (intro cong_diff_nat eq) auto
```
```   786       hence "[2 ^ (k - 1) = (0 :: nat)] (mod 2 ^ k)"
```
```   787         by (simp add: cong_sym_eq)
```
```   788       hence "2 ^ k dvd 2 ^ (k - 1)"
```
```   789         by (simp add: cong_0_iff)
```
```   790       hence "k \<le> k - 1"
```
```   791         by (rule power_dvd_imp_le) auto
```
```   792       thus False by simp
```
```   793     qed
```
```   794
```
```   795     have "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
```
```   796       using ord_twopow_aux[of k x] \<open>odd x\<close> \<open>k \<ge> 3\<close> by simp
```
```   797     hence "ord (2 ^ k) x dvd 2 ^ (k - 2)"
```
```   798       by (simp add: ord_divides')
```
```   799     then obtain l where l: "l \<le> k - 2" "ord (2 ^ k) x = 2 ^ l"
```
```   800       using divides_primepow_nat[of 2 "ord (2 ^ k) x" "k - 2"] by auto
```
```   801
```
```   802     from notcong' have "\<not>ord (2 ^ k) x dvd 2 ^ (k - 3)"
```
```   803       by (simp add: ord_divides')
```
```   804     with l have "l = k - 2"
```
```   805       using le_imp_power_dvd[of l "k - 3" 2] by (cases "l \<le> k - 3") auto
```
```   806     with l show ?thesis by simp
```
```   807   qed
```
```   808 qed
```
```   809
```
```   810 lemma ord_4_3 [simp]: "ord 4 (3::nat) = 2"
```
```   811 proof -
```
```   812   have "[3 ^ 2 = (1 :: nat)] (mod 4)"
```
```   813     by (simp add: cong_def)
```
```   814   hence "ord 4 (3::nat) dvd 2"
```
```   815     by (subst (asm) ord_divides) auto
```
```   816   hence "ord 4 (3::nat) \<le> 2"
```
```   817     by (intro dvd_imp_le) auto
```
```   818   moreover have "ord 4 (3::nat) \<noteq> 1"
```
```   819     by (auto simp: ord_eq_Suc_0_iff cong_def)
```
```   820   moreover have "ord 4 (3::nat) \<noteq> 0"
```
```   821     by (auto simp: gcd_non_0_nat coprime_iff_gcd_eq_1)
```
```   822   ultimately show "ord 4 (3 :: nat) = 2"
```
```   823     by linarith
```
```   824 qed
```
```   825
```
```   826 lemma elements_with_ord_1: "n > 0 \<Longrightarrow> {x\<in>totatives n. ord n x = Suc 0} = {1}"
```
```   827   by (auto simp: ord_eq_Suc_0_iff cong_def totatives_less)
```
```   828
```
```   829 lemma residue_prime_has_primroot:
```
```   830   fixes p :: nat
```
```   831   assumes "prime p"
```
```   832   shows "\<exists>a\<in>totatives p. ord p a = p - 1"
```
```   833 proof -
```
```   834   from residue_prime_mult_group_has_gen[OF assms]
```
```   835     obtain a where a: "a \<in> {1..p-1}" "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by blast
```
```   836   from a have "coprime p a"
```
```   837     using a assms by (intro prime_imp_coprime) (auto dest: dvd_imp_le)
```
```   838   with a(1) have "a \<in> totatives p" by (auto simp: totatives_def coprime_commute)
```
```   839
```
```   840   have "p - 1 = card {1..p-1}" by simp
```
```   841   also have "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by fact
```
```   842   also have "{a ^ i mod p |i. i \<in> UNIV} = (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
```
```   843   proof (intro equalityI subsetI)
```
```   844     fix x assume "x \<in> {a ^ i mod p |i. i \<in> UNIV}"
```
```   845     then obtain i where [simp]: "x = a ^ i mod p" by auto
```
```   846
```
```   847     have "[a ^ i = a ^ (i mod ord p a)] (mod p)"
```
```   848       using \<open>coprime p a\<close> by (subst order_divides_expdiff) auto
```
```   849     hence "\<exists>j. a ^ i mod p = a ^ j mod p \<and> j < ord p a"
```
```   850       using \<open>coprime p a\<close> by (intro exI[of _ "i mod ord p a"]) (auto simp: cong_def)
```
```   851     thus "x \<in> (\<lambda>i. a ^ i mod p) ` {..<ord p a}"
```
```   852       by auto
```
```   853   qed auto
```
```   854   also have "card \<dots> = ord p a"
```
```   855     using inj_power_mod[OF \<open>coprime p a\<close>] by (subst card_image) auto
```
```   856   finally show ?thesis using \<open>a \<in> totatives p\<close>
```
```   857     by auto
```
```   858 qed
```
```   859
```
```   860
```
```   861
```
```   862 subsection \<open>Another trivial primality characterization\<close>
```
```   863
```
```   864 lemma prime_prime_factor: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
```
```   865   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   866   for n :: nat
```
```   867 proof (cases "n = 0 \<or> n = 1")
```
```   868   case True
```
```   869   then show ?thesis
```
```   870      by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0)
```
```   871 next
```
```   872   case False
```
```   873   show ?thesis
```
```   874   proof
```
```   875     assume "prime n"
```
```   876     then show ?rhs
```
```   877       by (metis not_prime_1 prime_nat_iff)
```
```   878   next
```
```   879     assume ?rhs
```
```   880     with False show "prime n"
```
```   881       by (auto simp: prime_nat_iff) (metis One_nat_def prime_factor_nat prime_nat_iff)
```
```   882   qed
```
```   883 qed
```
```   884
```
```   885 lemma prime_divisor_sqrt: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
```
```   886   for n :: nat
```
```   887 proof -
```
```   888   consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1" by blast
```
```   889   then show ?thesis
```
```   890   proof cases
```
```   891     case 1
```
```   892     then show ?thesis by simp
```
```   893   next
```
```   894     case 2
```
```   895     then show ?thesis by simp
```
```   896   next
```
```   897     case n: 3
```
```   898     then have np: "n > 1" by arith
```
```   899     {
```
```   900       fix d
```
```   901       assume d: "d dvd n" "d\<^sup>2 \<le> n"
```
```   902         and H: "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
```
```   903       from H d have d1n: "d = 1 \<or> d = n" by blast
```
```   904       then have "d = 1"
```
```   905       proof
```
```   906         assume dn: "d = n"
```
```   907         from n have "n\<^sup>2 > n * 1"
```
```   908           by (simp add: power2_eq_square)
```
```   909         with dn d(2) show ?thesis by simp
```
```   910       qed
```
```   911     }
```
```   912     moreover
```
```   913     {
```
```   914       fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
```
```   915       from d n have "d \<noteq> 0"
```
```   916         by (metis dvd_0_left_iff)
```
```   917       then have dp: "d > 0" by simp
```
```   918       from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
```
```   919       from n dp e have ep:"e > 0" by simp
```
```   920       from dp ep have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n"
```
```   921         by (auto simp add: e power2_eq_square mult_le_cancel_left)
```
```   922       then have "d = 1 \<or> d = n"
```
```   923       proof
```
```   924         assume "d\<^sup>2 \<le> n"
```
```   925         with H[rule_format, of d] d have "d = 1" by blast
```
```   926         then show ?thesis ..
```
```   927       next
```
```   928         assume h: "e\<^sup>2 \<le> n"
```
```   929         from e have "e dvd n" by (simp add: dvd_def mult.commute)
```
```   930         with H[rule_format, of e] h have "e = 1" by simp
```
```   931         with e have "d = n" by simp
```
```   932         then show ?thesis ..
```
```   933       qed
```
```   934     }
```
```   935     ultimately show ?thesis
```
```   936       unfolding prime_nat_iff using np n(2) by blast
```
```   937   qed
```
```   938 qed
```
```   939
```
```   940 lemma prime_prime_factor_sqrt:
```
```   941   "prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
```
```   942   (is "?lhs \<longleftrightarrow>?rhs")
```
```   943 proof -
```
```   944   consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1"
```
```   945     by blast
```
```   946   then show ?thesis
```
```   947   proof cases
```
```   948     case 1
```
```   949     then show ?thesis by (metis not_prime_0)
```
```   950   next
```
```   951     case 2
```
```   952     then show ?thesis by (metis not_prime_1)
```
```   953   next
```
```   954     case n: 3
```
```   955     show ?thesis
```
```   956     proof
```
```   957       assume ?lhs
```
```   958       from this[unfolded prime_divisor_sqrt] n show ?rhs
```
```   959         by (metis prime_prime_factor)
```
```   960     next
```
```   961       assume ?rhs
```
```   962       {
```
```   963         fix d
```
```   964         assume d: "d dvd n" "d\<^sup>2 \<le> n" "d \<noteq> 1"
```
```   965         then obtain p where p: "prime p" "p dvd d"
```
```   966           by (metis prime_factor_nat)
```
```   967         from d(1) n have dp: "d > 0"
```
```   968           by (metis dvd_0_left neq0_conv)
```
```   969         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
```
```   970         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
```
```   971         with \<open>?rhs\<close> n p(1) dvd_trans[OF p(2) d(1)] have False
```
```   972           by blast
```
```   973       }
```
```   974       with n prime_divisor_sqrt show ?lhs by auto
```
```   975     qed
```
```   976   qed
```
```   977 qed
```
```   978
```
```   979
```
```   980 subsection \<open>Pocklington theorem\<close>
```
```   981
```
```   982 lemma pocklington_lemma:
```
```   983   fixes p :: nat
```
```   984   assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r"
```
```   985     and an: "[a^ (n - 1) = 1] (mod n)"
```
```   986     and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n"
```
```   987     and pp: "prime p" and pn: "p dvd n"
```
```   988   shows "[p = 1] (mod q)"
```
```   989 proof -
```
```   990   have p01: "p \<noteq> 0" "p \<noteq> 1"
```
```   991     using pp by (auto intro: prime_gt_0_nat)
```
```   992   obtain k where k: "a ^ (q * r) - 1 = n * k"
```
```   993     by (metis an cong_to_1_nat dvd_def nqr)
```
```   994   from pn[unfolded dvd_def] obtain l where l: "n = p * l"
```
```   995     by blast
```
```   996   have a0: "a \<noteq> 0"
```
```   997   proof
```
```   998     assume "a = 0"
```
```   999     with n have "a^ (n - 1) = 0"
```
```  1000       by (simp add: power_0_left)
```
```  1001     with n an mod_less[of 1 n] show False
```
```  1002       by (simp add: power_0_left cong_def)
```
```  1003   qed
```
```  1004   with n nqr have aqr0: "a ^ (q * r) \<noteq> 0"
```
```  1005     by simp
```
```  1006   then have "(a ^ (q * r) - 1) + 1  = a ^ (q * r)"
```
```  1007     by simp
```
```  1008   with k l have "a ^ (q * r) = p * l * k + 1"
```
```  1009     by simp
```
```  1010   then have "a ^ (r * q) + p * 0 = 1 + p * (l * k)"
```
```  1011     by (simp add: ac_simps)
```
```  1012   then have odq: "ord p (a^r) dvd q"
```
```  1013     unfolding ord_divides[symmetric] power_mult[symmetric]
```
```  1014     by (metis an cong_dvd_modulus_nat mult.commute nqr pn)
```
```  1015   from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d"
```
```  1016     by blast
```
```  1017   have d1: "d = 1"
```
```  1018   proof (rule ccontr)
```
```  1019     assume d1: "d \<noteq> 1"
```
```  1020     obtain P where P: "prime P" "P dvd d"
```
```  1021       by (metis d1 prime_factor_nat)
```
```  1022     from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
```
```  1023     from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
```
```  1024     from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
```
```  1025     from P(1) have P0: "P \<noteq> 0"
```
```  1026       by (metis not_prime_0)
```
```  1027     from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
```
```  1028     from d s t P0  have s': "ord p (a^r) * t = s"
```
```  1029       by (metis mult.commute mult_cancel1 mult.assoc)
```
```  1030     have "ord p (a^r) * t*r = r * ord p (a^r) * t"
```
```  1031       by (metis mult.assoc mult.commute)
```
```  1032     then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
```
```  1033       by (simp only: power_mult)
```
```  1034     then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
```
```  1035       by (metis cong_pow ord power_one)
```
```  1036     then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
```
```  1037       by (metis cong_to_1_nat exps)
```
```  1038     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
```
```  1039       using P0 by simp
```
```  1040     with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
```
```  1041       by simp
```
```  1042     with p01 pn pd0 coprime_common_divisor [of _ n p] show False
```
```  1043       by auto
```
```  1044   qed
```
```  1045   with d have o: "ord p (a^r) = q" by simp
```
```  1046   from pp totient_prime [of p] have totient_eq: "totient p = p - 1"
```
```  1047     by simp
```
```  1048   {
```
```  1049     fix d
```
```  1050     assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
```
```  1051     from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
```
```  1052     from n have "n \<noteq> 0" by simp
```
```  1053     then have False using d dp pn an
```
```  1054       by auto (metis One_nat_def Suc_lessI
```
```  1055         \<open>1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)\<close> \<open>a ^ (q * r) = p * l * k + 1\<close> add_diff_cancel_left' dvd_diff_nat dvd_power dvd_triv_left gcd_nat.trans nat_dvd_not_less nqr zero_less_diff zero_less_one)
```
```  1056   }
```
```  1057   then have cpa: "coprime p a"
```
```  1058     by (auto intro: coprimeI)
```
```  1059   then have arp: "coprime (a ^ r) p"
```
```  1060     by (cases "r > 0") (simp_all add: ac_simps)
```
```  1061   from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
```
```  1062     by simp
```
```  1063   then obtain d where d:"p - 1 = q * d"
```
```  1064     unfolding dvd_def by blast
```
```  1065   have "p \<noteq> 0"
```
```  1066     by (metis p01(1))
```
```  1067   with d have "p + q * 0 = 1 + q * d" by simp
```
```  1068   then show ?thesis
```
```  1069     by (metis cong_iff_lin_nat mult.commute)
```
```  1070 qed
```
```  1071
```
```  1072 theorem pocklington:
```
```  1073   assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
```
```  1074     and an: "[a^ (n - 1) = 1] (mod n)"
```
```  1075     and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
```
```  1076   shows "prime n"
```
```  1077   unfolding prime_prime_factor_sqrt[of n]
```
```  1078 proof -
```
```  1079   let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
```
```  1080   from n have n01: "n \<noteq> 0" "n \<noteq> 1" by arith+
```
```  1081   {
```
```  1082     fix p
```
```  1083     assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
```
```  1084     from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)"
```
```  1085       by (simp add: power2_eq_square)
```
```  1086     then have pq: "p \<le> q"
```
```  1087       by (metis le0 power_le_imp_le_base)
```
```  1088     from pocklington_lemma[OF n nqr an aq p(1,2)] have *: "q dvd p - 1"
```
```  1089       by (metis cong_to_1_nat)
```
```  1090     have "p - 1 \<noteq> 0"
```
```  1091       using prime_ge_2_nat [OF p(1)] by arith
```
```  1092     with pq * have False
```
```  1093       by (simp add: nat_dvd_not_less)
```
```  1094   }
```
```  1095   with n01 show ?ths by blast
```
```  1096 qed
```
```  1097
```
```  1098 text \<open>Variant for application, to separate the exponentiation.\<close>
```
```  1099 lemma pocklington_alt:
```
```  1100   assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2"
```
```  1101     and an: "[a^ (n - 1) = 1] (mod n)"
```
```  1102     and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)"
```
```  1103   shows "prime n"
```
```  1104 proof -
```
```  1105   {
```
```  1106     fix p
```
```  1107     assume p: "prime p" "p dvd q"
```
```  1108     from aq[rule_format] p obtain b where b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n"
```
```  1109       by blast
```
```  1110     have a0: "a \<noteq> 0"
```
```  1111     proof
```
```  1112       assume a0: "a = 0"
```
```  1113       from n an have "[0 = 1] (mod n)"
```
```  1114         unfolding a0 power_0_left by auto
```
```  1115       then show False
```
```  1116         using n by (simp add: cong_def dvd_eq_mod_eq_0[symmetric])
```
```  1117     qed
```
```  1118     then have a1: "a \<ge> 1" by arith
```
```  1119     from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
```
```  1120     have b0: "b \<noteq> 0"
```
```  1121     proof
```
```  1122       assume b0: "b = 0"
```
```  1123       from p(2) nqr have "(n - 1) mod p = 0"
```
```  1124         by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
```
```  1125       with div_mult_mod_eq[of "n - 1" p]
```
```  1126       have "(n - 1) div p * p= n - 1" by auto
```
```  1127       then have eq: "(a^((n - 1) div p))^p = a^(n - 1)"
```
```  1128         by (simp only: power_mult[symmetric])
```
```  1129       have "p - 1 \<noteq> 0"
```
```  1130         using prime_ge_2_nat [OF p(1)] by arith
```
```  1131       then have pS: "Suc (p - 1) = p" by arith
```
```  1132       from b have d: "n dvd a^((n - 1) div p)"
```
```  1133         unfolding b0 by auto
```
```  1134       from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_iff [OF an] n show False
```
```  1135         by simp
```
```  1136     qed
```
```  1137     then have b1: "b \<ge> 1" by arith
```
```  1138     from cong_imp_coprime[OF Cong.cong_diff_nat[OF cong_sym [OF b(1)] cong_refl [of 1] b1]]
```
```  1139       ath b1 b nqr
```
```  1140     have "coprime (a ^ ((n - 1) div p) - 1) n"
```
```  1141       by simp
```
```  1142   }
```
```  1143   then have "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
```
```  1144     by blast
```
```  1145   then show ?thesis by (rule pocklington[OF n nqr sqr an])
```
```  1146 qed
```
```  1147
```
```  1148
```
```  1149 subsection \<open>Prime factorizations\<close>
```
```  1150
```
```  1151 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
```
```  1152
```
```  1153 definition "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
```
```  1154
```
```  1155 lemma primefact:
```
```  1156   fixes n :: nat
```
```  1157   assumes n: "n \<noteq> 0"
```
```  1158   shows "\<exists>ps. primefact ps n"
```
```  1159 proof -
```
```  1160   obtain xs where xs: "mset xs = prime_factorization n"
```
```  1161     using ex_mset [of "prime_factorization n"] by blast
```
```  1162   from assms have "n = prod_mset (prime_factorization n)"
```
```  1163     by (simp add: prod_mset_prime_factorization)
```
```  1164   also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
```
```  1165   also have "\<dots> = foldr (*) xs 1" by (induct xs) simp_all
```
```  1166   finally have "foldr (*) xs 1 = n" ..
```
```  1167   moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
```
```  1168   ultimately have "primefact xs n" by (auto simp: primefact_def)
```
```  1169   then show ?thesis ..
```
```  1170 qed
```
```  1171
```
```  1172 lemma primefact_contains:
```
```  1173   fixes p :: nat
```
```  1174   assumes pf: "primefact ps n"
```
```  1175     and p: "prime p"
```
```  1176     and pn: "p dvd n"
```
```  1177   shows "p \<in> set ps"
```
```  1178   using pf p pn
```
```  1179 proof (induct ps arbitrary: p n)
```
```  1180   case Nil
```
```  1181   then show ?case by (auto simp: primefact_def)
```
```  1182 next
```
```  1183   case (Cons q qs)
```
```  1184   from Cons.prems[unfolded primefact_def]
```
```  1185   have q: "prime q" "q * foldr (*) qs 1 = n" "\<forall>p \<in>set qs. prime p"
```
```  1186     and p: "prime p" "p dvd q * foldr (*) qs 1"
```
```  1187     by simp_all
```
```  1188   consider "p dvd q" | "p dvd foldr (*) qs 1"
```
```  1189     by (metis p prime_dvd_mult_eq_nat)
```
```  1190   then show ?case
```
```  1191   proof cases
```
```  1192     case 1
```
```  1193     with p(1) q(1) have "p = q"
```
```  1194       unfolding prime_nat_iff by auto
```
```  1195     then show ?thesis by simp
```
```  1196   next
```
```  1197     case prem: 2
```
```  1198     from q(3) have pqs: "primefact qs (foldr (*) qs 1)"
```
```  1199       by (simp add: primefact_def)
```
```  1200     from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
```
```  1201   qed
```
```  1202 qed
```
```  1203
```
```  1204 lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> list_all prime ps"
```
```  1205   by (auto simp add: primefact_def list_all_iff)
```
```  1206
```
```  1207 text \<open>Variant of Lucas theorem.\<close>
```
```  1208 lemma lucas_primefact:
```
```  1209   assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
```
```  1210     and psn: "foldr (*) ps 1 = n - 1"
```
```  1211     and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
```
```  1212   shows "prime n"
```
```  1213 proof -
```
```  1214   {
```
```  1215     fix p
```
```  1216     assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
```
```  1217     from psn psp have psn1: "primefact ps (n - 1)"
```
```  1218       by (auto simp add: list_all_iff primefact_variant)
```
```  1219     from p(3) primefact_contains[OF psn1 p(1,2)] psp
```
```  1220     have False by (induct ps) auto
```
```  1221   }
```
```  1222   with lucas[OF n an] show ?thesis by blast
```
```  1223 qed
```
```  1224
```
```  1225 text \<open>Variant of Pocklington theorem.\<close>
```
```  1226 lemma pocklington_primefact:
```
```  1227   assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
```
```  1228     and arnb: "(a^r) mod n = b" and psq: "foldr (*) ps 1 = q"
```
```  1229     and bqn: "(b^q) mod n = 1"
```
```  1230     and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
```
```  1231   shows "prime n"
```
```  1232 proof -
```
```  1233   from bqn psp qrn
```
```  1234   have bqn: "a ^ (n - 1) mod n = 1"
```
```  1235     and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"
```
```  1236     unfolding arnb[symmetric] power_mod
```
```  1237     by (simp_all add: power_mult[symmetric] algebra_simps)
```
```  1238   from n have n0: "n > 0" by arith
```
```  1239   from div_mult_mod_eq[of "a^(n - 1)" n]
```
```  1240     mod_less_divisor[OF n0, of "a^(n - 1)"]
```
```  1241   have an1: "[a ^ (n - 1) = 1] (mod n)"
```
```  1242     by (metis bqn cong_def mod_mod_trivial)
```
```  1243   have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p
```
```  1244   proof -
```
```  1245     from psp psq have pfpsq: "primefact ps q"
```
```  1246       by (auto simp add: primefact_variant list_all_iff)
```
```  1247     from psp primefact_contains[OF pfpsq p]
```
```  1248     have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
```
```  1249       by (simp add: list_all_iff)
```
```  1250     from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p = Suc (p - 1)"
```
```  1251       by auto
```
```  1252     from div_mult1_eq[of r q p] p(2)
```
```  1253     have eq1: "r* (q div p) = (n - 1) div p"
```
```  1254       unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute)
```
```  1255     have ath: "a \<le> b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> 1 \<le> a \<and> 1 \<le> b" for a b :: nat
```
```  1256       by arith
```
```  1257     {
```
```  1258       assume "a ^ ((n - 1) div p) mod n = 0"
```
```  1259       then obtain s where s: "a ^ ((n - 1) div p) = n * s"
```
```  1260         by blast
```
```  1261       then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
```
```  1262       from qrn[symmetric] have qn1: "q dvd n - 1"
```
```  1263         by (auto simp: dvd_def)
```
```  1264       from dvd_trans[OF p(2) qn1] have npp: "(n - 1) div p * p = n - 1"
```
```  1265         by simp
```
```  1266       with eq0 have "a ^ (n - 1) = (n * s) ^ p"
```
```  1267         by (simp add: power_mult[symmetric])
```
```  1268       with bqn p01 have "1 = (n * s)^(Suc (p - 1)) mod n"
```
```  1269         by simp
```
```  1270       also have "\<dots> = 0" by (simp add: mult.assoc)
```
```  1271       finally have False by simp
```
```  1272     }
```
```  1273     then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
```
```  1274     have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
```
```  1275       by (simp add: cong_def)
```
```  1276     with ath[OF mod_less_eq_dividend *]
```
```  1277     have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
```
```  1278       by (simp add: cong_diff_nat)
```
```  1279     then show ?thesis
```
```  1280       by (metis cong_imp_coprime eq1 p')
```
```  1281   qed
```
```  1282   with pocklington[OF n qrn[symmetric] nq2 an1] show ?thesis
```
```  1283     by blast
```
```  1284 qed
```
```  1285
```
```  1286 end
```