src/HOL/Number_Theory/Pocklington.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58834 773b378d9313 child 60526 fad653acf58f permissions -rw-r--r--
```     1 (*  Title:      HOL/Number_Theory/Pocklington.thy
```
```     2     Author:     Amine Chaieb
```
```     3 *)
```
```     4
```
```     5 section {* Pocklington's Theorem for Primes *}
```
```     6
```
```     7 theory Pocklington
```
```     8 imports Residues
```
```     9 begin
```
```    10
```
```    11 subsection{*Lemmas about previously defined terms*}
```
```    12
```
```    13 lemma prime:
```
```    14   "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
```
```    15   (is "?lhs \<longleftrightarrow> ?rhs")
```
```    16 proof-
```
```    17   {assume "p=0 \<or> p=1" hence ?thesis
```
```    18     by (metis one_not_prime_nat zero_not_prime_nat)}
```
```    19   moreover
```
```    20   {assume p0: "p\<noteq>0" "p\<noteq>1"
```
```    21     {assume H: "?lhs"
```
```    22       {fix m assume m: "m > 0" "m < p"
```
```    23         {assume "m=1" hence "coprime p m" by simp}
```
```    24         moreover
```
```    25         {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
```
```    26           have "coprime p m" by simp}
```
```    27         ultimately have "coprime p m"
```
```    28           by (metis H prime_imp_coprime_nat)}
```
```    29       hence ?rhs using p0 by auto}
```
```    30     moreover
```
```    31     { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
```
```    32       obtain q where q: "prime q" "q dvd p"
```
```    33         by (metis p0(2) prime_factor_nat)
```
```    34       have q0: "q > 0"
```
```    35         by (metis prime_gt_0_nat q(1))
```
```    36       from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
```
```    37       {assume "q = p" hence ?lhs using q(1) by blast}
```
```    38       moreover
```
```    39       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
```
```    40         from H qplt q0 have "coprime p q" by arith
```
```    41        hence ?lhs using q
```
```    42          by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}
```
```    43       ultimately have ?lhs by blast}
```
```    44     ultimately have ?thesis by blast}
```
```    45   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
```
```    46 qed
```
```    47
```
```    48 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
```
```    49 proof-
```
```    50   have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
```
```    51   thus ?thesis by simp
```
```    52 qed
```
```    53
```
```    54
```
```    55 subsection{*Some basic theorems about solving congruences*}
```
```    56
```
```    57 lemma cong_solve:
```
```    58   fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
```
```    59 proof-
```
```    60   {assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)}
```
```    61   moreover
```
```    62   {assume az: "a\<noteq>0"
```
```    63   from bezout_add_strong_nat[OF az, of n]
```
```    64   obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
```
```    65   from dxy(1,2) have d1: "d = 1"
```
```    66     by (metis assms coprime_nat)
```
```    67   hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
```
```    68   hence "a*(x*b) = n*(y*b) + b"
```
```    69     by (auto simp add: algebra_simps)
```
```    70   hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
```
```    71   hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
```
```    72   hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .
```
```    73   hence ?thesis by blast}
```
```    74 ultimately  show ?thesis by blast
```
```    75 qed
```
```    76
```
```    77 lemma cong_solve_unique:
```
```    78   fixes n::nat assumes an: "coprime a n" and nz: "n \<noteq> 0"
```
```    79   shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
```
```    80 proof-
```
```    81   let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
```
```    82   from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
```
```    83   let ?x = "x mod n"
```
```    84   from x have th: "[a * ?x = b] (mod n)"
```
```    85     by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
```
```    86   from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
```
```    87   {fix y assume Py: "y < n" "[a * y = b] (mod n)"
```
```    88     from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def)
```
```    89     hence "[y = ?x] (mod n)"
```
```    90       by (metis an cong_mult_lcancel_nat)
```
```    91     with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
```
```    92     have "y = ?x" by (simp add: cong_nat_def)}
```
```    93   with Px show ?thesis by blast
```
```    94 qed
```
```    95
```
```    96 lemma cong_solve_unique_nontrivial:
```
```    97   assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
```
```    98   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
```
```    99 proof-
```
```   100   from pa have ap: "coprime a p"
```
```   101     by (metis gcd_nat.commute)
```
```   102   have px:"coprime x p"
```
```   103     by (metis gcd_nat.commute p prime x0 xp)
```
```   104   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
```
```   105     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
```
```   106   {assume y0: "y = 0"
```
```   107     with y(2) have th: "p dvd a"
```
```   108       by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right)
```
```   109     have False
```
```   110       by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
```
```   111   with y show ?thesis unfolding Ex1_def using neq0_conv by blast
```
```   112 qed
```
```   113
```
```   114 lemma cong_unique_inverse_prime:
```
```   115   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
```
```   116   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
```
```   117 by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms)
```
```   118
```
```   119 lemma chinese_remainder_coprime_unique:
```
```   120   fixes a::nat
```
```   121   assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
```
```   122   and ma: "coprime m a" and nb: "coprime n b"
```
```   123   shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   124 proof-
```
```   125   let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   126   from binary_chinese_remainder_unique_nat[OF ab az bz]
```
```   127   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
```
```   128     "\<forall>y. ?P y \<longrightarrow> y = x" by blast
```
```   129   from ma nb x
```
```   130   have "coprime x a" "coprime x b"
```
```   131     by (metis cong_gcd_eq_nat)+
```
```   132   then have "coprime x (a*b)"
```
```   133     by (metis coprime_mul_eq_nat)
```
```   134   with x show ?thesis by blast
```
```   135 qed
```
```   136
```
```   137
```
```   138 subsection{*Lucas's theorem*}
```
```   139
```
```   140 lemma phi_limit_strong: "phi(n) \<le> n - 1"
```
```   141 proof -
```
```   142   have "phi n = card {x. 0 < x \<and> x < int n \<and> coprime x (int n)}"
```
```   143     by (simp add: phi_def)
```
```   144   also have "... \<le> card {0 <..< int n}"
```
```   145     by (rule card_mono) auto
```
```   146   also have "... = card {0 <..< n}"
```
```   147     by (simp add: transfer_nat_int_set_functions)
```
```   148   also have "... \<le> n - 1"
```
```   149     by (metis card_greaterThanLessThan le_refl One_nat_def)
```
```   150   finally show ?thesis .
```
```   151 qed
```
```   152
```
```   153 lemma phi_lowerbound_1: assumes n: "n \<ge> 2"
```
```   154   shows "phi n \<ge> 1"
```
```   155 proof -
```
```   156   have "1 \<le> card {0::int <.. 1}"
```
```   157     by auto
```
```   158   also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
```
```   159     apply (rule card_mono) using assms
```
```   160     by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
```
```   161   also have "... = phi n"
```
```   162     by (simp add: phi_def)
```
```   163   finally show ?thesis .
```
```   164 qed
```
```   165
```
```   166 lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2"
```
```   167   shows "phi(int n) \<ge> 1"
```
```   168 by (metis n nat_le_iff nat_numeral phi_lowerbound_1)
```
```   169
```
```   170 lemma euler_theorem_nat:
```
```   171   fixes m::nat
```
```   172   assumes "coprime a m"
```
```   173   shows "[a ^ phi m = 1] (mod m)"
```
```   174 by (metis assms le0 euler_theorem [transferred])
```
```   175
```
```   176 lemma lucas_coprime_lemma:
```
```   177   fixes n::nat
```
```   178   assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
```
```   179   shows "coprime a n"
```
```   180 proof-
```
```   181   {assume "n=1" hence ?thesis by simp}
```
```   182   moreover
```
```   183   {assume "n = 0" hence ?thesis using am m
```
```   184      by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)}
```
```   185   moreover
```
```   186   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   187     from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
```
```   188     {fix d
```
```   189       assume d: "d dvd a" "d dvd n"
```
```   190       from n have n1: "1 < n" by arith
```
```   191       from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp
```
```   192       from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
```
```   193       from dvd_mod_iff[OF d(2), of "a^m"] dam am1
```
```   194       have "d = 1" by simp }
```
```   195     hence ?thesis by auto
```
```   196   }
```
```   197   ultimately show ?thesis by blast
```
```   198 qed
```
```   199
```
```   200 lemma lucas_weak:
```
```   201   fixes n::nat
```
```   202   assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)"
```
```   203   and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)"
```
```   204   shows "prime n"
```
```   205 proof-
```
```   206   from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+
```
```   207   from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" .
```
```   208   from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)"
```
```   209     by auto
```
```   210   {assume "phi n \<noteq> n - 1"
```
```   211     with phi_limit_strong phi_lowerbound_1_nat [OF n]
```
```   212     have c:"phi n > 0 \<and> phi n < n - 1"
```
```   213       by (metis gr0I leD less_linear not_one_le_zero)
```
```   214     from nm[rule_format, OF c] afn have False ..}
```
```   215   hence "phi n = n - 1" by blast
```
```   216   with prime_phi phi_prime n1(1,2) show ?thesis
```
```   217     by auto
```
```   218 qed
```
```   219
```
```   220 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
```
```   221   by (metis ex_least_nat_le not_less0)
```
```   222
```
```   223 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
```
```   224   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   225 proof-
```
```   226   {assume ?rhs hence ?lhs by blast}
```
```   227   moreover
```
```   228   { assume H: ?lhs then obtain n where n: "P n" by blast
```
```   229     let ?x = "Least P"
```
```   230     {fix m assume m: "m < ?x"
```
```   231       from not_less_Least[OF m] have "\<not> P m" .}
```
```   232     with LeastI_ex[OF H] have ?rhs by blast}
```
```   233   ultimately show ?thesis by blast
```
```   234 qed
```
```   235
```
```   236 theorem lucas:
```
```   237   assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
```
```   238   and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
```
```   239   shows "prime n"
```
```   240 proof-
```
```   241   from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
```
```   242   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
```
```   243   from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
```
```   244   have an: "coprime a n" "coprime (a^(n - 1)) n"
```
```   245     by (auto simp add: coprime_exp_nat gcd_nat.commute)
```
```   246   {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
```
```   247     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
```
```   248       m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
```
```   249     {assume nm1: "(n - 1) mod m > 0"
```
```   250       from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
```
```   251       let ?y = "a^ ((n - 1) div m * m)"
```
```   252       note mdeq = mod_div_equality[of "(n - 1)" m]
```
```   253       have yn: "coprime ?y n"
```
```   254         by (metis an(1) coprime_exp_nat gcd_nat.commute)
```
```   255       have "?y mod n = (a^m)^((n - 1) div m) mod n"
```
```   256         by (simp add: algebra_simps power_mult)
```
```   257       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
```
```   258         using power_mod[of "a^m" n "(n - 1) div m"] by simp
```
```   259       also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
```
```   260         by (metis power_one)
```
```   261       finally have th3: "?y mod n = 1"  .
```
```   262       have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
```
```   263         using an1[unfolded cong_nat_def onen] onen
```
```   264           mod_div_equality[of "(n - 1)" m, symmetric]
```
```   265         by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
```
```   266       have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
```
```   267         by (metis cong_mult_rcancel_nat mult.commute th2 yn)
```
```   268       from m(4)[rule_format, OF th0] nm1
```
```   269         less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
```
```   270       have False by blast }
```
```   271     hence "(n - 1) mod m = 0" by auto
```
```   272     then have mn: "m dvd n - 1" by presburger
```
```   273     then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
```
```   274     from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
```
```   275     obtain p where p: "prime p" "p dvd r"
```
```   276       by (metis prime_factor_nat r01(2))
```
```   277     hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
```
```   278     have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
```
```   279       by (simp add: power_mult)
```
```   280     also have "\<dots> = (a^(m*(r div p))) mod n"
```
```   281       using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0]
```
```   282       by simp
```
```   283     also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
```
```   284     also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..
```
```   285     also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)
```
```   286     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
```
```   287       using onen by (simp add: cong_nat_def)
```
```   288     with pn th have False by blast}
```
```   289   hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
```
```   290   from lucas_weak[OF n2 an1 th] show ?thesis .
```
```   291 qed
```
```   292
```
```   293
```
```   294 subsection{*Definition of the order of a number mod n (0 in non-coprime case)*}
```
```   295
```
```   296 definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
```
```   297
```
```   298 (* This has the expected properties.                                         *)
```
```   299
```
```   300 lemma coprime_ord:
```
```   301   fixes n::nat
```
```   302   assumes "coprime n a"
```
```   303   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))"
```
```   304 proof-
```
```   305   let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
```
```   306   from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast
```
```   307   from assms have o: "ord n a = Least ?P" by (simp add: ord_def)
```
```   308   {assume "n=0 \<or> n=1" with assms have "\<exists>m>0. ?P m"
```
```   309       by auto}
```
```   310   moreover
```
```   311   {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
```
```   312     from assms have na': "coprime a n"
```
```   313       by (metis gcd_nat.commute)
```
```   314     from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na']
```
```   315     have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) }
```
```   316   ultimately have ex: "\<exists>m>0. ?P m" by blast
```
```   317   from nat_exists_least_iff'[of ?P] ex assms show ?thesis
```
```   318     unfolding o[symmetric] by auto
```
```   319 qed
```
```   320
```
```   321 (* With the special value 0 for non-coprime case, it's more convenient.      *)
```
```   322 lemma ord_works:
```
```   323   fixes n::nat
```
```   324   shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
```
```   325 apply (cases "coprime n a")
```
```   326 using coprime_ord[of n a]
```
```   327 by (auto simp add: ord_def cong_nat_def)
```
```   328
```
```   329 lemma ord:
```
```   330   fixes n::nat
```
```   331   shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast
```
```   332
```
```   333 lemma ord_minimal:
```
```   334   fixes n::nat
```
```   335   shows "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
```
```   336   using ord_works by blast
```
```   337
```
```   338 lemma ord_eq_0:
```
```   339   fixes n::nat
```
```   340   shows "ord n a = 0 \<longleftrightarrow> ~coprime n a"
```
```   341 by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
```
```   342
```
```   343 lemma divides_rexp:
```
```   344   "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))"
```
```   345   by (simp add: dvd_mult2[of x y])
```
```   346
```
```   347 lemma ord_divides:
```
```   348   fixes n::nat
```
```   349   shows "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   350 proof
```
```   351   assume rh: ?rhs
```
```   352   then obtain k where "d = ord n a * k" unfolding dvd_def by blast
```
```   353   hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
```
```   354     by (simp add : cong_nat_def power_mult power_mod)
```
```   355   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
```
```   356     using ord[of a n, unfolded cong_nat_def]
```
```   357     by (simp add: cong_nat_def power_mod)
```
```   358   finally  show ?lhs .
```
```   359 next
```
```   360   assume lh: ?lhs
```
```   361   { assume H: "\<not> coprime n a"
```
```   362     hence o: "ord n a = 0" by (simp add: ord_def)
```
```   363     {assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)}
```
```   364     moreover
```
```   365     {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
```
```   366       from H
```
```   367       obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
```
```   368       from lh
```
```   369       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
```
```   370         by (metis H d0 gcd_nat.commute lucas_coprime_lemma)
```
```   371       hence "a ^ d + n * q1 - n * q2 = 1" by simp
```
```   372       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
```
```   373       have "p dvd 1"
```
```   374         by metis
```
```   375       with p(3) have False by simp
```
```   376       hence ?rhs ..}
```
```   377     ultimately have ?rhs by blast}
```
```   378   moreover
```
```   379   {assume H: "coprime n a"
```
```   380     let ?o = "ord n a"
```
```   381     let ?q = "d div ord n a"
```
```   382     let ?r = "d mod ord n a"
```
```   383     have eqo: "[(a^?o)^?q = 1] (mod n)"
```
```   384       by (metis cong_exp_nat ord power_one)
```
```   385     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
```
```   386     hence op: "?o > 0" by simp
```
```   387     from mod_div_equality[of d "ord n a"] lh
```
```   388     have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute)
```
```   389     hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
```
```   390       by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
```
```   391     hence th: "[a^?r = 1] (mod n)"
```
```   392       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
```
```   393       apply (simp add: cong_nat_def del: One_nat_def)
```
```   394       by (simp add: mod_mult_left_eq[symmetric])
```
```   395     {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
```
```   396     moreover
```
```   397     {assume r: "?r \<noteq> 0"
```
```   398       with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
```
```   399       from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
```
```   400       have ?rhs by blast}
```
```   401     ultimately have ?rhs by blast}
```
```   402   ultimately  show ?rhs by blast
```
```   403 qed
```
```   404
```
```   405 lemma order_divides_phi:
```
```   406   fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n"
```
```   407   by (metis ord_divides euler_theorem_nat gcd_nat.commute)
```
```   408
```
```   409 lemma order_divides_expdiff:
```
```   410   fixes n::nat and a::nat assumes na: "coprime n a"
```
```   411   shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   412 proof-
```
```   413   {fix n::nat and a::nat and d::nat and e::nat
```
```   414     assume na: "coprime n a" and ed: "(e::nat) \<le> d"
```
```   415     hence "\<exists>c. d = e + c" by presburger
```
```   416     then obtain c where c: "d = e + c" by presburger
```
```   417     from na have an: "coprime a n"
```
```   418       by (metis gcd_nat.commute)
```
```   419     have aen: "coprime (a^e) n"
```
```   420       by (metis coprime_exp_nat gcd_nat.commute na)
```
```   421     have acn: "coprime (a^c) n"
```
```   422       by (metis coprime_exp_nat gcd_nat.commute na)
```
```   423     have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
```
```   424       using c by simp
```
```   425     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
```
```   426     also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
```
```   427       using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp
```
```   428     also  have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
```
```   429     also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
```
```   430       using cong_add_lcancel_nat
```
```   431       by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
```
```   432     finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   433       using c by simp }
```
```   434   note th = this
```
```   435   have "e \<le> d \<or> d \<le> e" by arith
```
```   436   moreover
```
```   437   {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
```
```   438   moreover
```
```   439   {assume de: "d \<le> e"
```
```   440     from th[OF na de] have ?thesis
```
```   441     by (metis cong_sym_nat)}
```
```   442   ultimately show ?thesis by blast
```
```   443 qed
```
```   444
```
```   445 subsection{*Another trivial primality characterization*}
```
```   446
```
```   447 lemma prime_prime_factor:
```
```   448   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
```
```   449   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   450 proof (cases "n=0 \<or> n=1")
```
```   451   case True
```
```   452   then show ?thesis
```
```   453      by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
```
```   454 next
```
```   455   case False
```
```   456   show ?thesis
```
```   457   proof
```
```   458     assume "prime n"
```
```   459     then show ?rhs
```
```   460       by (metis one_not_prime_nat prime_nat_def)
```
```   461   next
```
```   462     assume ?rhs
```
```   463     with False show "prime n"
```
```   464       by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)
```
```   465   qed
```
```   466 qed
```
```   467
```
```   468 lemma prime_divisor_sqrt:
```
```   469   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
```
```   470 proof -
```
```   471   {assume "n=0 \<or> n=1" hence ?thesis
```
```   472     by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)}
```
```   473   moreover
```
```   474   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   475     hence np: "n > 1" by arith
```
```   476     {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
```
```   477       from H d have d1n: "d = 1 \<or> d=n" by blast
```
```   478       {assume dn: "d=n"
```
```   479         have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
```
```   480         with dn d(2) have "d=1" by simp}
```
```   481       with d1n have "d = 1" by blast  }
```
```   482     moreover
```
```   483     {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
```
```   484       from d n have "d \<noteq> 0"
```
```   485         by (metis dvd_0_left_iff)
```
```   486       hence dp: "d > 0" by simp
```
```   487       from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
```
```   488       from n dp e have ep:"e > 0" by simp
```
```   489       have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
```
```   490         by (auto simp add: e power2_eq_square mult_le_cancel_left)
```
```   491       moreover
```
```   492       {assume h: "d\<^sup>2 \<le> n"
```
```   493         from H[rule_format, of d] h d have "d = 1" by blast}
```
```   494       moreover
```
```   495       {assume h: "e\<^sup>2 \<le> n"
```
```   496         from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute)
```
```   497         with H[rule_format, of e] h have "e=1" by simp
```
```   498         with e have "d = n" by simp}
```
```   499       ultimately have "d=1 \<or> d=n"  by blast}
```
```   500     ultimately have ?thesis unfolding prime_def using np n(2) by blast}
```
```   501   ultimately show ?thesis by auto
```
```   502 qed
```
```   503
```
```   504 lemma prime_prime_factor_sqrt:
```
```   505   "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
```
```   506   (is "?lhs \<longleftrightarrow>?rhs")
```
```   507 proof-
```
```   508   {assume "n=0 \<or> n=1"
```
```   509    hence ?thesis
```
```   510      by (metis one_not_prime_nat zero_not_prime_nat)}
```
```   511   moreover
```
```   512   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   513     {assume H: ?lhs
```
```   514       from H[unfolded prime_divisor_sqrt] n
```
```   515       have ?rhs
```
```   516         by (metis prime_prime_factor) }
```
```   517     moreover
```
```   518     {assume H: ?rhs
```
```   519       {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
```
```   520         then obtain p where p: "prime p" "p dvd d"
```
```   521           by (metis prime_factor_nat)
```
```   522         from d(1) n have dp: "d > 0"
```
```   523           by (metis dvd_0_left neq0_conv)
```
```   524         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
```
```   525         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
```
```   526         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
```
```   527       with n prime_divisor_sqrt  have ?lhs by auto}
```
```   528     ultimately have ?thesis by blast }
```
```   529   ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
```
```   530 qed
```
```   531
```
```   532
```
```   533 subsection{*Pocklington theorem*}
```
```   534
```
```   535 lemma pocklington_lemma:
```
```   536   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
```
```   537   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
```
```   538   and pp: "prime p" and pn: "p dvd n"
```
```   539   shows "[p = 1] (mod q)"
```
```   540 proof -
```
```   541   have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by auto
```
```   542   obtain k where k: "a ^ (q * r) - 1 = n*k"
```
```   543     by (metis an cong_to_1_nat dvd_def nqr)
```
```   544   from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
```
```   545   {assume a0: "a = 0"
```
```   546     hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
```
```   547     with n an mod_less[of 1 n]  have False by (simp add: power_0_left cong_nat_def)}
```
```   548   hence a0: "a\<noteq>0" ..
```
```   549   from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
```
```   550   hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
```
```   551   with k l have "a ^ (q * r) = p*l*k + 1" by simp
```
```   552   hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
```
```   553   hence odq: "ord p (a^r) dvd q"
```
```   554     unfolding ord_divides[symmetric] power_mult[symmetric]
```
```   555     by (metis an cong_dvd_modulus_nat mult.commute nqr pn)
```
```   556   from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
```
```   557   {assume d1: "d \<noteq> 1"
```
```   558     obtain P where P: "prime P" "P dvd d"
```
```   559       by (metis d1 prime_factor_nat)
```
```   560     from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
```
```   561     from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
```
```   562     from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
```
```   563     have P0: "P \<noteq> 0" using P(1)
```
```   564       by (metis zero_not_prime_nat)
```
```   565     from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
```
```   566     from d s t P0  have s': "ord p (a^r) * t = s"
```
```   567       by (metis mult.commute mult_cancel1 mult.assoc)
```
```   568     have "ord p (a^r) * t*r = r * ord p (a^r) * t"
```
```   569       by (metis mult.assoc mult.commute)
```
```   570     hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
```
```   571       by (simp only: power_mult)
```
```   572     then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
```
```   573       by (metis cong_exp_nat ord power_one)
```
```   574     have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
```
```   575       by (metis cong_to_1_nat exps th)
```
```   576     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
```
```   577     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
```
```   578     with p01 pn pd0 coprime_common_divisor_nat have False
```
```   579       by auto}
```
```   580   hence d1: "d = 1" by blast
```
```   581   hence o: "ord p (a^r) = q" using d by simp
```
```   582   from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
```
```   583   {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
```
```   584     from pp[unfolded prime_def] d have dp: "d = p" by blast
```
```   585     from n have "n \<noteq> 0" by simp
```
```   586     then have False using d
```
```   587       by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat
```
```   588            gcd_lcm_complete_lattice_nat.top_greatest pn)}
```
```   589   hence cpa: "coprime p a" by auto
```
```   590   have arp: "coprime (a^r) p"
```
```   591     by (metis coprime_exp_nat cpa gcd_nat.commute)
```
```   592   from euler_theorem_nat[OF arp, simplified ord_divides] o phip
```
```   593   have "q dvd (p - 1)" by simp
```
```   594   then obtain d where d:"p - 1 = q * d"
```
```   595     unfolding dvd_def by blast
```
```   596   have p0:"p \<noteq> 0"
```
```   597     by (metis p01(1))
```
```   598   from p0 d have "p + q * 0 = 1 + q * d" by simp
```
```   599   then show ?thesis
```
```   600     by (metis cong_iff_lin_nat mult.commute)
```
```   601 qed
```
```   602
```
```   603 theorem pocklington:
```
```   604   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
```
```   605   and an: "[a^ (n - 1) = 1] (mod n)"
```
```   606   and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
```
```   607   shows "prime n"
```
```   608 unfolding prime_prime_factor_sqrt[of n]
```
```   609 proof-
```
```   610   let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
```
```   611   from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
```
```   612   {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
```
```   613     from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
```
```   614     hence pq: "p \<le> q"
```
```   615       by (metis le0 power_le_imp_le_base)
```
```   616     from pocklington_lemma[OF n nqr an aq p(1,2)]
```
```   617     have th: "q dvd p - 1"
```
```   618       by (metis cong_to_1_nat)
```
```   619     have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
```
```   620     with pq p have False
```
```   621       by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq
```
```   622             prime_gt_0_nat th) }
```
```   623   with n01 show ?ths by blast
```
```   624 qed
```
```   625
```
```   626 (* Variant for application, to separate the exponentiation.                  *)
```
```   627 lemma pocklington_alt:
```
```   628   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
```
```   629   and an: "[a^ (n - 1) = 1] (mod n)"
```
```   630   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)"
```
```   631   shows "prime n"
```
```   632 proof-
```
```   633   {fix p assume p: "prime p" "p dvd q"
```
```   634     from aq[rule_format] p obtain b where
```
```   635       b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
```
```   636     {assume a0: "a=0"
```
```   637       from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
```
```   638       hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])}
```
```   639     hence a0: "a\<noteq> 0" ..
```
```   640     hence a1: "a \<ge> 1" by arith
```
```   641     from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
```
```   642     {assume b0: "b = 0"
```
```   643       from p(2) nqr have "(n - 1) mod p = 0"
```
```   644         by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
```
```   645       with mod_div_equality[of "n - 1" p]
```
```   646       have "(n - 1) div p * p= n - 1" by auto
```
```   647       hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
```
```   648         by (simp only: power_mult[symmetric])
```
```   649       have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
```
```   650       then have pS: "Suc (p - 1) = p" by arith
```
```   651       from b have d: "n dvd a^((n - 1) div p)" unfolding b0
```
```   652         by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left
```
```   653                    gcd_lcm_complete_lattice_nat.inf_top_left)
```
```   654       from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
```
```   655       have False
```
```   656         by simp}
```
```   657     then have b0: "b \<noteq> 0" ..
```
```   658     hence b1: "b \<ge> 1" by arith
```
```   659     from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]]
```
```   660          ath b1 b nqr
```
```   661     have "coprime (a ^ ((n - 1) div p) - 1) n"
```
```   662       by simp}
```
```   663   hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
```
```   664     by blast
```
```   665   from pocklington[OF n nqr sqr an th] show ?thesis .
```
```   666 qed
```
```   667
```
```   668
```
```   669 subsection{*Prime factorizations*}
```
```   670
```
```   671 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
```
```   672
```
```   673 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
```
```   674
```
```   675 lemma primefact: assumes n: "n \<noteq> 0"
```
```   676   shows "\<exists>ps. primefact ps n"
```
```   677 using n
```
```   678 proof(induct n rule: nat_less_induct)
```
```   679   fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
```
```   680   let ?ths = "\<exists>ps. primefact ps n"
```
```   681   {assume "n = 1"
```
```   682     hence "primefact [] n" by (simp add: primefact_def)
```
```   683     hence ?ths by blast }
```
```   684   moreover
```
```   685   {assume n1: "n \<noteq> 1"
```
```   686     with n have n2: "n \<ge> 2" by arith
```
```   687     obtain p where p: "prime p" "p dvd n"
```
```   688       by (metis n1 prime_factor_nat)
```
```   689     from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
```
```   690     from n m have m0: "m > 0" "m\<noteq>0" by auto
```
```   691     have "1 < p"
```
```   692       by (metis p(1) prime_nat_def)
```
```   693     with m0 m have mn: "m < n" by auto
```
```   694     from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
```
```   695     from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
```
```   696     hence ?ths by blast}
```
```   697   ultimately show ?ths by blast
```
```   698 qed
```
```   699
```
```   700 lemma primefact_contains:
```
```   701   assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
```
```   702   shows "p \<in> set ps"
```
```   703   using pf p pn
```
```   704 proof(induct ps arbitrary: p n)
```
```   705   case Nil thus ?case by (auto simp add: primefact_def)
```
```   706 next
```
```   707   case (Cons q qs p n)
```
```   708   from Cons.prems[unfolded primefact_def]
```
```   709   have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"  and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all
```
```   710   {assume "p dvd q"
```
```   711     with p(1) q(1) have "p = q" unfolding prime_def by auto
```
```   712     hence ?case by simp}
```
```   713   moreover
```
```   714   { assume h: "p dvd foldr op * qs 1"
```
```   715     from q(3) have pqs: "primefact qs (foldr op * qs 1)"
```
```   716       by (simp add: primefact_def)
```
```   717     from Cons.hyps[OF pqs p(1) h] have ?case by simp}
```
```   718   ultimately show ?case
```
```   719     by (metis p prime_dvd_mult_eq_nat)
```
```   720 qed
```
```   721
```
```   722 lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
```
```   723   by (auto simp add: primefact_def list_all_iff)
```
```   724
```
```   725 (* Variant of Lucas theorem.                                                 *)
```
```   726
```
```   727 lemma lucas_primefact:
```
```   728   assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
```
```   729   and psn: "foldr op * ps 1 = n - 1"
```
```   730   and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
```
```   731   shows "prime n"
```
```   732 proof-
```
```   733   {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
```
```   734     from psn psp have psn1: "primefact ps (n - 1)"
```
```   735       by (auto simp add: list_all_iff primefact_variant)
```
```   736     from p(3) primefact_contains[OF psn1 p(1,2)] psp
```
```   737     have False by (induct ps, auto)}
```
```   738   with lucas[OF n an] show ?thesis by blast
```
```   739 qed
```
```   740
```
```   741 (* Variant of Pocklington theorem.                                           *)
```
```   742
```
```   743 lemma pocklington_primefact:
```
```   744   assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
```
```   745   and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
```
```   746   and bqn: "(b^q) mod n = 1"
```
```   747   and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
```
```   748   shows "prime n"
```
```   749 proof-
```
```   750   from bqn psp qrn
```
```   751   have bqn: "a ^ (n - 1) mod n = 1"
```
```   752     and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"
```
```   753     unfolding arnb[symmetric] power_mod
```
```   754     by (simp_all add: power_mult[symmetric] algebra_simps)
```
```   755   from n  have n0: "n > 0" by arith
```
```   756   from mod_div_equality[of "a^(n - 1)" n]
```
```   757     mod_less_divisor[OF n0, of "a^(n - 1)"]
```
```   758   have an1: "[a ^ (n - 1) = 1] (mod n)"
```
```   759     by (metis bqn cong_nat_def mod_mod_trivial)
```
```   760   {fix p assume p: "prime p" "p dvd q"
```
```   761     from psp psq have pfpsq: "primefact ps q"
```
```   762       by (auto simp add: primefact_variant list_all_iff)
```
```   763     from psp primefact_contains[OF pfpsq p]
```
```   764     have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
```
```   765       by (simp add: list_all_iff)
```
```   766     from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)"
```
```   767       by auto
```
```   768     from div_mult1_eq[of r q p] p(2)
```
```   769     have eq1: "r* (q div p) = (n - 1) div p"
```
```   770       unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute)
```
```   771     have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
```
```   772     {assume "a ^ ((n - 1) div p) mod n = 0"
```
```   773       then obtain s where s: "a ^ ((n - 1) div p) = n*s"
```
```   774         unfolding mod_eq_0_iff by blast
```
```   775       hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
```
```   776       from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
```
```   777       from dvd_trans[OF p(2) qn1]
```
```   778       have npp: "(n - 1) div p * p = n - 1" by simp
```
```   779       with eq0 have "a^ (n - 1) = (n*s)^p"
```
```   780         by (simp add: power_mult[symmetric])
```
```   781       hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
```
```   782       also have "\<dots> = 0" by (simp add: mult.assoc)
```
```   783       finally have False by simp }
```
```   784       then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
```
```   785     have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
```
```   786       unfolding cong_nat_def by simp
```
```   787     from  th1   ath[OF mod_less_eq_dividend th11]
```
```   788     have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
```
```   789       by (metis cong_diff_nat cong_refl_nat)
```
```   790     have "coprime (a ^ ((n - 1) div p) - 1) n"
```
```   791       by (metis cong_imp_coprime_nat eq1 p' th) }
```
```   792   with pocklington[OF n qrn[symmetric] nq2 an1]
```
```   793   show ?thesis by blast
```
```   794 qed
```
```   795
```
```   796 end
```