src/HOL/Old_Number_Theory/Pocklington.thy
 author wenzelm Sat Oct 10 16:26:23 2015 +0200 (2015-10-10) changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 62481 b5d8e57826df permissions -rw-r--r--
isabelle update_cartouches;
```     1 (*  Title:      HOL/Old_Number_Theory/Pocklington.thy
```
```     2     Author:     Amine Chaieb
```
```     3 *)
```
```     4
```
```     5 section \<open>Pocklington's Theorem for Primes\<close>
```
```     6
```
```     7 theory Pocklington
```
```     8 imports Primes
```
```     9 begin
```
```    10
```
```    11 definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
```
```    12   where "[a = b] (mod p) == ((a mod p) = (b mod p))"
```
```    13
```
```    14 definition modneq:: "nat => nat => nat => bool"    ("(1[_ \<noteq> _] '(mod _'))")
```
```    15   where "[a \<noteq> b] (mod p) == ((a mod p) \<noteq> (b mod p))"
```
```    16
```
```    17 lemma modeq_trans:
```
```    18   "\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
```
```    19   by (simp add:modeq_def)
```
```    20
```
```    21 lemma modeq_sym[sym]:
```
```    22   "[a = b] (mod p) \<Longrightarrow> [b = a] (mod p)"
```
```    23   unfolding modeq_def by simp
```
```    24
```
```    25 lemma modneq_sym[sym]:
```
```    26   "[a \<noteq> b] (mod p) \<Longrightarrow> [b \<noteq> a] (mod p)"
```
```    27   by (simp add: modneq_def)
```
```    28
```
```    29 lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
```
```    30   shows "\<exists>q. x = y + n * q"
```
```    31 using xyn xy unfolding modeq_def using nat_mod_eq_lemma by blast
```
```    32
```
```    33 lemma nat_mod[algebra]: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
```
```    34 unfolding modeq_def nat_mod_eq_iff ..
```
```    35
```
```    36 (* Lemmas about previously defined terms.                                    *)
```
```    37
```
```    38 lemma prime: "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
```
```    39   (is "?lhs \<longleftrightarrow> ?rhs")
```
```    40 proof-
```
```    41   {assume "p=0 \<or> p=1" hence ?thesis using prime_0 prime_1 by (cases "p=0", simp_all)}
```
```    42   moreover
```
```    43   {assume p0: "p\<noteq>0" "p\<noteq>1"
```
```    44     {assume H: "?lhs"
```
```    45       {fix m assume m: "m > 0" "m < p"
```
```    46         {assume "m=1" hence "coprime p m" by simp}
```
```    47         moreover
```
```    48         {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
```
```    49           have "coprime p m" by simp}
```
```    50         ultimately have "coprime p m" using prime_coprime[OF H, of m] by blast}
```
```    51       hence ?rhs using p0 by auto}
```
```    52     moreover
```
```    53     { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
```
```    54       from prime_factor[OF p0(2)] obtain q where q: "prime q" "q dvd p" by blast
```
```    55       from prime_ge_2[OF q(1)] have q0: "q > 0" by arith
```
```    56       from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
```
```    57       {assume "q = p" hence ?lhs using q(1) by blast}
```
```    58       moreover
```
```    59       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
```
```    60         from H[rule_format, of q] qplt q0 have "coprime p q" by arith
```
```    61         with coprime_prime[of p q q] q have False by simp hence ?lhs by blast}
```
```    62       ultimately have ?lhs by blast}
```
```    63     ultimately have ?thesis by blast}
```
```    64   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
```
```    65 qed
```
```    66
```
```    67 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
```
```    68 proof-
```
```    69   have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
```
```    70   thus ?thesis by simp
```
```    71 qed
```
```    72
```
```    73 lemma coprime_mod: assumes n: "n \<noteq> 0" shows "coprime (a mod n) n \<longleftrightarrow> coprime a n"
```
```    74   using n dvd_mod_iff[of _ n a] by (auto simp add: coprime)
```
```    75
```
```    76 (* Congruences.                                                              *)
```
```    77
```
```    78 lemma cong_mod_01[simp,presburger]:
```
```    79   "[x = y] (mod 0) \<longleftrightarrow> x = y" "[x = y] (mod 1)" "[x = 0] (mod n) \<longleftrightarrow> n dvd x"
```
```    80   by (simp_all add: modeq_def, presburger)
```
```    81
```
```    82 lemma cong_sub_cases:
```
```    83   "[x = y] (mod n) \<longleftrightarrow> (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
```
```    84 apply (auto simp add: nat_mod)
```
```    85 apply (rule_tac x="q2" in exI)
```
```    86 apply (rule_tac x="q1" in exI, simp)
```
```    87 apply (rule_tac x="q2" in exI)
```
```    88 apply (rule_tac x="q1" in exI, simp)
```
```    89 apply (rule_tac x="q1" in exI)
```
```    90 apply (rule_tac x="q2" in exI, simp)
```
```    91 apply (rule_tac x="q1" in exI)
```
```    92 apply (rule_tac x="q2" in exI, simp)
```
```    93 done
```
```    94
```
```    95 lemma cong_mult_lcancel: assumes an: "coprime a n" and axy:"[a * x = a * y] (mod n)"
```
```    96   shows "[x = y] (mod n)"
```
```    97 proof-
```
```    98   {assume "a = 0" with an axy coprime_0'[of n] have ?thesis by (simp add: modeq_def) }
```
```    99   moreover
```
```   100   {assume az: "a\<noteq>0"
```
```   101     {assume xy: "x \<le> y" hence axy': "a*x \<le> a*y" by simp
```
```   102       with axy cong_sub_cases[of "a*x" "a*y" n]  have "[a*(y - x) = 0] (mod n)"
```
```   103         by (simp only: if_True diff_mult_distrib2)
```
```   104       hence th: "n dvd a*(y -x)" by simp
```
```   105       from coprime_divprod[OF th] an have "n dvd y - x"
```
```   106         by (simp add: coprime_commute)
```
```   107       hence ?thesis using xy cong_sub_cases[of x y n] by simp}
```
```   108     moreover
```
```   109     {assume H: "\<not>x \<le> y" hence xy: "y \<le> x"  by arith
```
```   110       from H az have axy': "\<not> a*x \<le> a*y" by auto
```
```   111       with axy H cong_sub_cases[of "a*x" "a*y" n]  have "[a*(x - y) = 0] (mod n)"
```
```   112         by (simp only: if_False diff_mult_distrib2)
```
```   113       hence th: "n dvd a*(x - y)" by simp
```
```   114       from coprime_divprod[OF th] an have "n dvd x - y"
```
```   115         by (simp add: coprime_commute)
```
```   116       hence ?thesis using xy cong_sub_cases[of x y n] by simp}
```
```   117     ultimately have ?thesis by blast}
```
```   118   ultimately show ?thesis by blast
```
```   119 qed
```
```   120
```
```   121 lemma cong_mult_rcancel: assumes an: "coprime a n" and axy:"[x*a = y*a] (mod n)"
```
```   122   shows "[x = y] (mod n)"
```
```   123   using cong_mult_lcancel[OF an axy[unfolded mult.commute[of _a]]] .
```
```   124
```
```   125 lemma cong_refl: "[x = x] (mod n)" by (simp add: modeq_def)
```
```   126
```
```   127 lemma eq_imp_cong: "a = b \<Longrightarrow> [a = b] (mod n)" by (simp add: cong_refl)
```
```   128
```
```   129 lemma cong_commute: "[x = y] (mod n) \<longleftrightarrow> [y = x] (mod n)"
```
```   130   by (auto simp add: modeq_def)
```
```   131
```
```   132 lemma cong_trans[trans]: "[x = y] (mod n) \<Longrightarrow> [y = z] (mod n) \<Longrightarrow> [x = z] (mod n)"
```
```   133   by (simp add: modeq_def)
```
```   134
```
```   135 lemma cong_add: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)"
```
```   136   shows "[x + y = x' + y'] (mod n)"
```
```   137 proof-
```
```   138   have "(x + y) mod n = (x mod n + y mod n) mod n"
```
```   139     by (simp add: mod_add_left_eq[of x y n] mod_add_right_eq[of "x mod n" y n])
```
```   140   also have "\<dots> = (x' mod n + y' mod n) mod n" using xx' yy' modeq_def by simp
```
```   141   also have "\<dots> = (x' + y') mod n"
```
```   142     by (simp add: mod_add_left_eq[of x' y' n] mod_add_right_eq[of "x' mod n" y' n])
```
```   143   finally show ?thesis unfolding modeq_def .
```
```   144 qed
```
```   145
```
```   146 lemma cong_mult: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)"
```
```   147   shows "[x * y = x' * y'] (mod n)"
```
```   148 proof-
```
```   149   have "(x * y) mod n = (x mod n) * (y mod n) mod n"
```
```   150     by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n])
```
```   151   also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp
```
```   152   also have "\<dots> = (x' * y') mod n"
```
```   153     by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n])
```
```   154   finally show ?thesis unfolding modeq_def .
```
```   155 qed
```
```   156
```
```   157 lemma cong_exp: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
```
```   158   by (induct k, auto simp add: cong_refl cong_mult)
```
```   159 lemma cong_sub: assumes xx': "[x = x'] (mod n)" and yy': "[y = y'] (mod n)"
```
```   160   and yx: "y <= x" and yx': "y' <= x'"
```
```   161   shows "[x - y = x' - y'] (mod n)"
```
```   162 proof-
```
```   163   { fix x a x' a' y b y' b'
```
```   164     have "(x::nat) + a = x' + a' \<Longrightarrow> y + b = y' + b' \<Longrightarrow> y <= x \<Longrightarrow> y' <= x'
```
```   165       \<Longrightarrow> (x - y) + (a + b') = (x' - y') + (a' + b)" by arith}
```
```   166   note th = this
```
```   167   from xx' yy' obtain q1 q2 q1' q2' where q12: "x + n*q1 = x'+n*q2"
```
```   168     and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
```
```   169   from th[OF q12 q12' yx yx']
```
```   170   have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
```
```   171     by (simp add: distrib_left)
```
```   172   thus ?thesis unfolding nat_mod by blast
```
```   173 qed
```
```   174
```
```   175 lemma cong_mult_lcancel_eq: assumes an: "coprime a n"
```
```   176   shows "[a * x = a * y] (mod n) \<longleftrightarrow> [x = y] (mod n)" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   177 proof
```
```   178   assume H: "?rhs" from cong_mult[OF cong_refl[of a n] H] show ?lhs .
```
```   179 next
```
```   180   assume H: "?lhs" hence H': "[x*a = y*a] (mod n)" by (simp add: mult.commute)
```
```   181   from cong_mult_rcancel[OF an H'] show ?rhs  .
```
```   182 qed
```
```   183
```
```   184 lemma cong_mult_rcancel_eq: assumes an: "coprime a n"
```
```   185   shows "[x * a = y * a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
```
```   186 using cong_mult_lcancel_eq[OF an, of x y] by (simp add: mult.commute)
```
```   187
```
```   188 lemma cong_add_lcancel_eq: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
```
```   189   by (simp add: nat_mod)
```
```   190
```
```   191 lemma cong_add_rcancel_eq: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
```
```   192   by (simp add: nat_mod)
```
```   193
```
```   194 lemma cong_add_rcancel: "[x + a = y + a] (mod n) \<Longrightarrow> [x = y] (mod n)"
```
```   195   by (simp add: nat_mod)
```
```   196
```
```   197 lemma cong_add_lcancel: "[a + x = a + y] (mod n) \<Longrightarrow> [x = y] (mod n)"
```
```   198   by (simp add: nat_mod)
```
```   199
```
```   200 lemma cong_add_lcancel_eq_0: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
```
```   201   by (simp add: nat_mod)
```
```   202
```
```   203 lemma cong_add_rcancel_eq_0: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
```
```   204   by (simp add: nat_mod)
```
```   205
```
```   206 lemma cong_imp_eq: assumes xn: "x < n" and yn: "y < n" and xy: "[x = y] (mod n)"
```
```   207   shows "x = y"
```
```   208   using xy[unfolded modeq_def mod_less[OF xn] mod_less[OF yn]] .
```
```   209
```
```   210 lemma cong_divides_modulus: "[x = y] (mod m) \<Longrightarrow> n dvd m ==> [x = y] (mod n)"
```
```   211   apply (auto simp add: nat_mod dvd_def)
```
```   212   apply (rule_tac x="k*q1" in exI)
```
```   213   apply (rule_tac x="k*q2" in exI)
```
```   214   by simp
```
```   215
```
```   216 lemma cong_0_divides: "[x = 0] (mod n) \<longleftrightarrow> n dvd x" by simp
```
```   217
```
```   218 lemma cong_1_divides:"[x = 1] (mod n) ==> n dvd x - 1"
```
```   219   apply (cases "x\<le>1", simp_all)
```
```   220   using cong_sub_cases[of x 1 n] by auto
```
```   221
```
```   222 lemma cong_divides: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
```
```   223 apply (auto simp add: nat_mod dvd_def)
```
```   224 apply (rule_tac x="k + q1 - q2" in exI, simp add: add_mult_distrib2 diff_mult_distrib2)
```
```   225 apply (rule_tac x="k + q2 - q1" in exI, simp add: add_mult_distrib2 diff_mult_distrib2)
```
```   226 done
```
```   227
```
```   228 lemma cong_coprime: assumes xy: "[x = y] (mod n)"
```
```   229   shows "coprime n x \<longleftrightarrow> coprime n y"
```
```   230 proof-
```
```   231   {assume "n=0" hence ?thesis using xy by simp}
```
```   232   moreover
```
```   233   {assume nz: "n \<noteq> 0"
```
```   234   have "coprime n x \<longleftrightarrow> coprime (x mod n) n"
```
```   235     by (simp add: coprime_mod[OF nz, of x] coprime_commute[of n x])
```
```   236   also have "\<dots> \<longleftrightarrow> coprime (y mod n) n" using xy[unfolded modeq_def] by simp
```
```   237   also have "\<dots> \<longleftrightarrow> coprime y n" by (simp add: coprime_mod[OF nz, of y])
```
```   238   finally have ?thesis by (simp add: coprime_commute) }
```
```   239 ultimately show ?thesis by blast
```
```   240 qed
```
```   241
```
```   242 lemma cong_mod: "~(n = 0) \<Longrightarrow> [a mod n = a] (mod n)" by (simp add: modeq_def)
```
```   243
```
```   244 lemma mod_mult_cong: "~(a = 0) \<Longrightarrow> ~(b = 0)
```
```   245   \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
```
```   246   by (simp add: modeq_def mod_mult2_eq mod_add_left_eq)
```
```   247
```
```   248 lemma cong_mod_mult: "[x = y] (mod n) \<Longrightarrow> m dvd n \<Longrightarrow> [x = y] (mod m)"
```
```   249   apply (auto simp add: nat_mod dvd_def)
```
```   250   apply (rule_tac x="k*q1" in exI)
```
```   251   apply (rule_tac x="k*q2" in exI, simp)
```
```   252   done
```
```   253
```
```   254 (* Some things when we know more about the order.                            *)
```
```   255
```
```   256 lemma cong_le: "y <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
```
```   257   using nat_mod_lemma[of x y n]
```
```   258   apply auto
```
```   259   apply (simp add: nat_mod)
```
```   260   apply (rule_tac x="q" in exI)
```
```   261   apply (rule_tac x="q + q" in exI)
```
```   262   by (auto simp: algebra_simps)
```
```   263
```
```   264 lemma cong_to_1: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
```
```   265 proof-
```
```   266   {assume "n = 0 \<or> n = 1\<or> a = 0 \<or> a = 1" hence ?thesis
```
```   267       apply (cases "n=0", simp_all add: cong_commute)
```
```   268       apply (cases "n=1", simp_all add: cong_commute modeq_def)
```
```   269       apply arith
```
```   270       apply (cases "a=1")
```
```   271       apply (simp_all add: modeq_def cong_commute)
```
```   272       done }
```
```   273   moreover
```
```   274   {assume n: "n\<noteq>0" "n\<noteq>1" and a:"a\<noteq>0" "a \<noteq> 1" hence a': "a \<ge> 1" by simp
```
```   275     hence ?thesis using cong_le[OF a', of n] by auto }
```
```   276   ultimately show ?thesis by auto
```
```   277 qed
```
```   278
```
```   279 (* Some basic theorems about solving congruences.                            *)
```
```   280
```
```   281
```
```   282 lemma cong_solve: assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
```
```   283 proof-
```
```   284   {assume "a=0" hence ?thesis using an by (simp add: modeq_def)}
```
```   285   moreover
```
```   286   {assume az: "a\<noteq>0"
```
```   287   from bezout_add_strong[OF az, of n]
```
```   288   obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
```
```   289   from an[unfolded coprime, rule_format, of d] dxy(1,2) have d1: "d = 1" by blast
```
```   290   hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
```
```   291   hence "a*(x*b) = n*(y*b) + b" by algebra
```
```   292   hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
```
```   293   hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
```
```   294   hence "[a*(x*b) = b] (mod n)" unfolding modeq_def .
```
```   295   hence ?thesis by blast}
```
```   296 ultimately  show ?thesis by blast
```
```   297 qed
```
```   298
```
```   299 lemma cong_solve_unique: assumes an: "coprime a n" and nz: "n \<noteq> 0"
```
```   300   shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
```
```   301 proof-
```
```   302   let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
```
```   303   from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
```
```   304   let ?x = "x mod n"
```
```   305   from x have th: "[a * ?x = b] (mod n)"
```
```   306     by (simp add: modeq_def mod_mult_right_eq[of a x n])
```
```   307   from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
```
```   308   {fix y assume Py: "y < n" "[a * y = b] (mod n)"
```
```   309     from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def)
```
```   310     hence "[y = ?x] (mod n)" by (simp add: cong_mult_lcancel_eq[OF an])
```
```   311     with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
```
```   312     have "y = ?x" by (simp add: modeq_def)}
```
```   313   with Px show ?thesis by blast
```
```   314 qed
```
```   315
```
```   316 lemma cong_solve_unique_nontrivial:
```
```   317   assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
```
```   318   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
```
```   319 proof-
```
```   320   from p have p1: "p > 1" using prime_ge_2[OF p] by arith
```
```   321   hence p01: "p \<noteq> 0" "p \<noteq> 1" by arith+
```
```   322   from pa have ap: "coprime a p" by (simp add: coprime_commute)
```
```   323   from prime_coprime[OF p, of x] dvd_imp_le[of p x] x0 xp have px:"coprime x p"
```
```   324     by (auto simp add: coprime_commute)
```
```   325   from cong_solve_unique[OF px p01(1)]
```
```   326   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y" by blast
```
```   327   {assume y0: "y = 0"
```
```   328     with y(2) have th: "p dvd a" by (simp add: cong_commute[of 0 a p])
```
```   329     with p coprime_prime[OF pa, of p] have False by simp}
```
```   330   with y show ?thesis unfolding Ex1_def using neq0_conv by blast
```
```   331 qed
```
```   332 lemma cong_unique_inverse_prime:
```
```   333   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
```
```   334   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
```
```   335   using cong_solve_unique_nontrivial[OF p coprime_1[of p] x0 xp] .
```
```   336
```
```   337 (* Forms of the Chinese remainder theorem.                                   *)
```
```   338
```
```   339 lemma cong_chinese:
```
```   340   assumes ab: "coprime a b" and  xya: "[x = y] (mod a)"
```
```   341   and xyb: "[x = y] (mod b)"
```
```   342   shows "[x = y] (mod a*b)"
```
```   343   using ab xya xyb
```
```   344   by (simp add: cong_sub_cases[of x y a] cong_sub_cases[of x y b]
```
```   345     cong_sub_cases[of x y "a*b"])
```
```   346 (cases "x \<le> y", simp_all add: divides_mul[of a _ b])
```
```   347
```
```   348 lemma chinese_remainder_unique:
```
```   349   assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b\<noteq>0"
```
```   350   shows "\<exists>!x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   351 proof-
```
```   352   from az bz have abpos: "a*b > 0" by simp
```
```   353   from chinese_remainder[OF ab az bz] obtain x q1 q2 where
```
```   354     xq12: "x = m + q1 * a" "x = n + q2 * b" by blast
```
```   355   let ?w = "x mod (a*b)"
```
```   356   have wab: "?w < a*b" by (simp add: mod_less_divisor[OF abpos])
```
```   357   from xq12(1) have "?w mod a = ((m + q1 * a) mod (a*b)) mod a" by simp
```
```   358   also have "\<dots> = m mod a" by (simp add: mod_mult2_eq)
```
```   359   finally have th1: "[?w = m] (mod a)" by (simp add: modeq_def)
```
```   360   from xq12(2) have "?w mod b = ((n + q2 * b) mod (a*b)) mod b" by simp
```
```   361   also have "\<dots> = ((n + q2 * b) mod (b*a)) mod b" by (simp add: mult.commute)
```
```   362   also have "\<dots> = n mod b" by (simp add: mod_mult2_eq)
```
```   363   finally have th2: "[?w = n] (mod b)" by (simp add: modeq_def)
```
```   364   {fix y assume H: "y < a*b" "[y = m] (mod a)" "[y = n] (mod b)"
```
```   365     with th1 th2 have H': "[y = ?w] (mod a)" "[y = ?w] (mod b)"
```
```   366       by (simp_all add: modeq_def)
```
```   367     from cong_chinese[OF ab H'] mod_less[OF H(1)] mod_less[OF wab]
```
```   368     have "y = ?w" by (simp add: modeq_def)}
```
```   369   with th1 th2 wab show ?thesis by blast
```
```   370 qed
```
```   371
```
```   372 lemma chinese_remainder_coprime_unique:
```
```   373   assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
```
```   374   and ma: "coprime m a" and nb: "coprime n b"
```
```   375   shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   376 proof-
```
```   377   let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
```
```   378   from chinese_remainder_unique[OF ab az bz]
```
```   379   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
```
```   380     "\<forall>y. ?P y \<longrightarrow> y = x" by blast
```
```   381   from ma nb cong_coprime[OF x(2)] cong_coprime[OF x(3)]
```
```   382   have "coprime x a" "coprime x b" by (simp_all add: coprime_commute)
```
```   383   with coprime_mul[of x a b] have "coprime x (a*b)" by simp
```
```   384   with x show ?thesis by blast
```
```   385 qed
```
```   386
```
```   387 (* Euler totient function.                                                   *)
```
```   388
```
```   389 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
```
```   390
```
```   391 lemma phi_0[simp]: "\<phi> 0 = 0"
```
```   392   unfolding phi_def by auto
```
```   393
```
```   394 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
```
```   395 proof-
```
```   396   have "{ m. 0 < m \<and> m <= n \<and> coprime m n } \<subseteq> {0..n}" by auto
```
```   397   thus ?thesis by (auto intro: finite_subset)
```
```   398 qed
```
```   399
```
```   400 declare coprime_1[presburger]
```
```   401 lemma phi_1[simp]: "\<phi> 1 = 1"
```
```   402 proof-
```
```   403   {fix m
```
```   404     have "0 < m \<and> m <= 1 \<and> coprime m 1 \<longleftrightarrow> m = 1" by presburger }
```
```   405   thus ?thesis by (simp add: phi_def)
```
```   406 qed
```
```   407
```
```   408 lemma [simp]: "\<phi> (Suc 0) = Suc 0" using phi_1 by simp
```
```   409
```
```   410 lemma phi_alt: "\<phi>(n) = card { m. coprime m n \<and> m < n}"
```
```   411 proof-
```
```   412   {assume "n=0 \<or> n=1" hence ?thesis by (cases "n=0", simp_all)}
```
```   413   moreover
```
```   414   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   415     {fix m
```
```   416       from n have "0 < m \<and> m <= n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n"
```
```   417         apply (cases "m = 0", simp_all)
```
```   418         apply (cases "m = 1", simp_all)
```
```   419         apply (cases "m = n", auto)
```
```   420         done }
```
```   421     hence ?thesis unfolding phi_def by simp}
```
```   422   ultimately show ?thesis by auto
```
```   423 qed
```
```   424
```
```   425 lemma phi_finite_lemma[simp]: "finite {m. coprime m n \<and>  m < n}" (is "finite ?S")
```
```   426   by (rule finite_subset[of "?S" "{0..n}"], auto)
```
```   427
```
```   428 lemma phi_another: assumes n: "n\<noteq>1"
```
```   429   shows "\<phi> n = card {m. 0 < m \<and> m < n \<and> coprime m n }"
```
```   430 proof-
```
```   431   {fix m
```
```   432     from n have "0 < m \<and> m < n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n"
```
```   433       by (cases "m=0", auto)}
```
```   434   thus ?thesis unfolding phi_alt by auto
```
```   435 qed
```
```   436
```
```   437 lemma phi_limit: "\<phi> n \<le> n"
```
```   438 proof-
```
```   439   have "{ m. coprime m n \<and> m < n} \<subseteq> {0 ..<n}" by auto
```
```   440   with card_mono[of "{0 ..<n}" "{ m. coprime m n \<and> m < n}"]
```
```   441   show ?thesis unfolding phi_alt by auto
```
```   442 qed
```
```   443
```
```   444 lemma stupid[simp]: "{m. (0::nat) < m \<and> m < n} = {1..<n}"
```
```   445   by auto
```
```   446
```
```   447 lemma phi_limit_strong: assumes n: "n\<noteq>1"
```
```   448   shows "\<phi>(n) \<le> n - 1"
```
```   449 proof-
```
```   450   show ?thesis
```
```   451     unfolding phi_another[OF n] finite_number_segment[of n, symmetric]
```
```   452     by (rule card_mono[of "{m. 0 < m \<and> m < n}" "{m. 0 < m \<and> m < n \<and> coprime m n}"], auto)
```
```   453 qed
```
```   454
```
```   455 lemma phi_lowerbound_1_strong: assumes n: "n \<ge> 1"
```
```   456   shows "\<phi>(n) \<ge> 1"
```
```   457 proof-
```
```   458   let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }"
```
```   459   from card_0_eq[of ?S] n have "\<phi> n \<noteq> 0" unfolding phi_alt
```
```   460     apply auto
```
```   461     apply (cases "n=1", simp_all)
```
```   462     apply (rule exI[where x=1], simp)
```
```   463     done
```
```   464   thus ?thesis by arith
```
```   465 qed
```
```   466
```
```   467 lemma phi_lowerbound_1: "2 <= n ==> 1 <= \<phi>(n)"
```
```   468   using phi_lowerbound_1_strong[of n] by auto
```
```   469
```
```   470 lemma phi_lowerbound_2: assumes n: "3 <= n" shows "2 <= \<phi> (n)"
```
```   471 proof-
```
```   472   let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }"
```
```   473   have inS: "{1, n - 1} \<subseteq> ?S" using n coprime_plus1[of "n - 1"]
```
```   474     by (auto simp add: coprime_commute)
```
```   475   from n have c2: "card {1, n - 1} = 2" by (auto simp add: card_insert_if)
```
```   476   from card_mono[of ?S "{1, n - 1}", simplified inS c2] show ?thesis
```
```   477     unfolding phi_def by auto
```
```   478 qed
```
```   479
```
```   480 lemma phi_prime: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1 \<longleftrightarrow> prime n"
```
```   481 proof-
```
```   482   {assume "n=0 \<or> n=1" hence ?thesis by (cases "n=1", simp_all)}
```
```   483   moreover
```
```   484   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   485     let ?S = "{m. 0 < m \<and> m < n}"
```
```   486     have fS: "finite ?S" by simp
```
```   487     let ?S' = "{m. 0 < m \<and> m < n \<and> coprime m n}"
```
```   488     have fS':"finite ?S'" apply (rule finite_subset[of ?S' ?S]) by auto
```
```   489     {assume H: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1"
```
```   490       hence ceq: "card ?S' = card ?S"
```
```   491       using n finite_number_segment[of n] phi_another[OF n(2)] by simp
```
```   492       {fix m assume m: "0 < m" "m < n" "\<not> coprime m n"
```
```   493         hence mS': "m \<notin> ?S'" by auto
```
```   494         have "insert m ?S' \<le> ?S" using m by auto
```
```   495         from m have "card (insert m ?S') \<le> card ?S"
```
```   496           by - (rule card_mono[of ?S "insert m ?S'"], auto)
```
```   497         hence False
```
```   498           unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq
```
```   499           by simp }
```
```   500       hence "\<forall>m. 0 <m \<and> m < n \<longrightarrow> coprime m n" by blast
```
```   501       hence "prime n" unfolding prime using n by (simp add: coprime_commute)}
```
```   502     moreover
```
```   503     {assume H: "prime n"
```
```   504       hence "?S = ?S'" unfolding prime using n
```
```   505         by (auto simp add: coprime_commute)
```
```   506       hence "card ?S = card ?S'" by simp
```
```   507       hence "\<phi> n = n - 1" unfolding phi_another[OF n(2)] by simp}
```
```   508     ultimately have ?thesis using n by blast}
```
```   509   ultimately show ?thesis by (cases "n=0") blast+
```
```   510 qed
```
```   511
```
```   512 (* Multiplicativity property.                                                *)
```
```   513
```
```   514 lemma phi_multiplicative: assumes ab: "coprime a b"
```
```   515   shows "\<phi> (a * b) = \<phi> a * \<phi> b"
```
```   516 proof-
```
```   517   {assume "a = 0 \<or> b = 0 \<or> a = 1 \<or> b = 1"
```
```   518     hence ?thesis
```
```   519       by (cases "a=0", simp, cases "b=0", simp, cases"a=1", simp_all) }
```
```   520   moreover
```
```   521   {assume a: "a\<noteq>0" "a\<noteq>1" and b: "b\<noteq>0" "b\<noteq>1"
```
```   522     hence ab0: "a*b \<noteq> 0" by simp
```
```   523     let ?S = "\<lambda>k. {m. coprime m k \<and> m < k}"
```
```   524     let ?f = "\<lambda>x. (x mod a, x mod b)"
```
```   525     have eq: "?f ` (?S (a*b)) = (?S a \<times> ?S b)"
```
```   526     proof-
```
```   527       {fix x assume x:"x \<in> ?S (a*b)"
```
```   528         hence x': "coprime x (a*b)" "x < a*b" by simp_all
```
```   529         hence xab: "coprime x a" "coprime x b" by (simp_all add: coprime_mul_eq)
```
```   530         from mod_less_divisor a b have xab':"x mod a < a" "x mod b < b" by auto
```
```   531         from xab xab' have "?f x \<in> (?S a \<times> ?S b)"
```
```   532           by (simp add: coprime_mod[OF a(1)] coprime_mod[OF b(1)])}
```
```   533       moreover
```
```   534       {fix x y assume x: "x \<in> ?S a" and y: "y \<in> ?S b"
```
```   535         hence x': "coprime x a" "x < a" and y': "coprime y b" "y < b" by simp_all
```
```   536         from chinese_remainder_coprime_unique[OF ab a(1) b(1) x'(1) y'(1)]
```
```   537         obtain z where z: "coprime z (a * b)" "z < a * b" "[z = x] (mod a)"
```
```   538           "[z = y] (mod b)" by blast
```
```   539         hence "(x,y) \<in> ?f ` (?S (a*b))"
```
```   540           using y'(2) mod_less_divisor[of b y] x'(2) mod_less_divisor[of a x]
```
```   541           by (auto simp add: image_iff modeq_def)}
```
```   542       ultimately show ?thesis by auto
```
```   543     qed
```
```   544     have finj: "inj_on ?f (?S (a*b))"
```
```   545       unfolding inj_on_def
```
```   546     proof(clarify)
```
```   547       fix x y assume H: "coprime x (a * b)" "x < a * b" "coprime y (a * b)"
```
```   548         "y < a * b" "x mod a = y mod a" "x mod b = y mod b"
```
```   549       hence cp: "coprime x a" "coprime x b" "coprime y a" "coprime y b"
```
```   550         by (simp_all add: coprime_mul_eq)
```
```   551       from chinese_remainder_coprime_unique[OF ab a(1) b(1) cp(3,4)] H
```
```   552       show "x = y" unfolding modeq_def by blast
```
```   553     qed
```
```   554     from card_image[OF finj, unfolded eq] have ?thesis
```
```   555       unfolding phi_alt by simp }
```
```   556   ultimately show ?thesis by auto
```
```   557 qed
```
```   558
```
```   559 (* Fermat's Little theorem / Fermat-Euler theorem.                           *)
```
```   560
```
```   561
```
```   562 lemma nproduct_mod:
```
```   563   assumes fS: "finite S" and n0: "n \<noteq> 0"
```
```   564   shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)"
```
```   565 proof-
```
```   566   have th1:"[1 = 1] (mod n)" by (simp add: modeq_def)
```
```   567   from cong_mult
```
```   568   have th3:"\<forall>x1 y1 x2 y2.
```
```   569     [x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)"
```
```   570     by blast
```
```   571   have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def)
```
```   572   from setprod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS)
```
```   573 qed
```
```   574
```
```   575 lemma nproduct_cmul:
```
```   576   assumes fS:"finite S"
```
```   577   shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
```
```   578 unfolding setprod.distrib setprod_constant[OF fS, of c] ..
```
```   579
```
```   580 lemma coprime_nproduct:
```
```   581   assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
```
```   582   shows "coprime n (setprod a S)"
```
```   583   using fS by (rule finite_subset_induct)
```
```   584     (insert Sn, auto simp add: coprime_mul)
```
```   585
```
```   586 lemma fermat_little: assumes an: "coprime a n"
```
```   587   shows "[a ^ (\<phi> n) = 1] (mod n)"
```
```   588 proof-
```
```   589   {assume "n=0" hence ?thesis by simp}
```
```   590   moreover
```
```   591   {assume "n=1" hence ?thesis by (simp add: modeq_def)}
```
```   592   moreover
```
```   593   {assume nz: "n \<noteq> 0" and n1: "n \<noteq> 1"
```
```   594     let ?S = "{m. coprime m n \<and> m < n}"
```
```   595     let ?P = "\<Prod> ?S"
```
```   596     have fS: "finite ?S" by simp
```
```   597     have cardfS: "\<phi> n = card ?S" unfolding phi_alt ..
```
```   598     {fix m assume m: "m \<in> ?S"
```
```   599       hence "coprime m n" by simp
```
```   600       with coprime_mul[of n a m] an have "coprime (a*m) n"
```
```   601         by (simp add: coprime_commute)}
```
```   602     hence Sn: "\<forall>m\<in> ?S. coprime (a*m) n " by blast
```
```   603     from coprime_nproduct[OF fS, of n "\<lambda>m. m"] have nP:"coprime ?P n"
```
```   604       by (simp add: coprime_commute)
```
```   605     have Paphi: "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
```
```   606     proof-
```
```   607       let ?h = "\<lambda>m. (a * m) mod n"
```
```   608
```
```   609       have eq0: "(\<Prod>i\<in>?S. ?h i) = (\<Prod>i\<in>?S. i)"
```
```   610       proof (rule setprod.reindex_bij_betw)
```
```   611         have "inj_on (\<lambda>i. ?h i) ?S"
```
```   612         proof (rule inj_onI)
```
```   613           fix x y assume "?h x = ?h y"
```
```   614           then have "[a * x = a * y] (mod n)"
```
```   615             by (simp add: modeq_def)
```
```   616           moreover assume "x \<in> ?S" "y \<in> ?S"
```
```   617           ultimately show "x = y"
```
```   618             by (auto intro: cong_imp_eq cong_mult_lcancel an)
```
```   619         qed
```
```   620         moreover have "?h ` ?S = ?S"
```
```   621         proof safe
```
```   622           fix y assume "coprime y n" then show "coprime (?h y) n"
```
```   623             by (metis an nz coprime_commute coprime_mod coprime_mul_eq)
```
```   624         next
```
```   625           fix y assume y: "coprime y n" "y < n"
```
```   626           from cong_solve_unique[OF an nz] obtain x where x: "x < n" "[a * x = y] (mod n)"
```
```   627             by blast
```
```   628           then show "y \<in> ?h ` ?S"
```
```   629             using cong_coprime[OF x(2)] coprime_mul_eq[of n a x] an y x
```
```   630             by (intro image_eqI[of _ _ x]) (auto simp add: coprime_commute modeq_def)
```
```   631         qed (insert nz, simp)
```
```   632         ultimately show "bij_betw ?h ?S ?S"
```
```   633           by (simp add: bij_betw_def)
```
```   634       qed
```
```   635       from nproduct_mod[OF fS nz, of "op * a"]
```
```   636       have "[(\<Prod>i\<in>?S. a * i) = (\<Prod>i\<in>?S. ?h i)] (mod n)"
```
```   637         by (simp add: cong_commute)
```
```   638       also have "[(\<Prod>i\<in>?S. ?h i) = ?P] (mod n)"
```
```   639         using eq0 fS an by (simp add: setprod_def modeq_def)
```
```   640       finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
```
```   641         unfolding cardfS mult.commute[of ?P "a^ (card ?S)"]
```
```   642           nproduct_cmul[OF fS, symmetric] mult_1_right by simp
```
```   643     qed
```
```   644     from cong_mult_lcancel[OF nP Paphi] have ?thesis . }
```
```   645   ultimately show ?thesis by blast
```
```   646 qed
```
```   647
```
```   648 lemma fermat_little_prime: assumes p: "prime p" and ap: "coprime a p"
```
```   649   shows "[a^ (p - 1) = 1] (mod p)"
```
```   650   using fermat_little[OF ap] p[unfolded phi_prime[symmetric]]
```
```   651 by simp
```
```   652
```
```   653
```
```   654 (* Lucas's theorem.                                                          *)
```
```   655
```
```   656 lemma lucas_coprime_lemma:
```
```   657   assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
```
```   658   shows "coprime a n"
```
```   659 proof-
```
```   660   {assume "n=1" hence ?thesis by simp}
```
```   661   moreover
```
```   662   {assume "n = 0" hence ?thesis using am m exp_eq_1[of a m] by simp}
```
```   663   moreover
```
```   664   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   665     from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
```
```   666     {fix d
```
```   667       assume d: "d dvd a" "d dvd n"
```
```   668       from n have n1: "1 < n" by arith
```
```   669       from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding modeq_def by simp
```
```   670       from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
```
```   671       from dvd_mod_iff[OF d(2), of "a^m"] dam am1
```
```   672       have "d = 1" by simp }
```
```   673     hence ?thesis unfolding coprime by auto
```
```   674   }
```
```   675   ultimately show ?thesis by blast
```
```   676 qed
```
```   677
```
```   678 lemma lucas_weak:
```
```   679   assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)"
```
```   680   and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)"
```
```   681   shows "prime n"
```
```   682 proof-
```
```   683   from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+
```
```   684   from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" .
```
```   685   from fermat_little[OF can] have afn: "[a ^ \<phi> n = 1] (mod n)" .
```
```   686   {assume "\<phi> n \<noteq> n - 1"
```
```   687     with phi_limit_strong[OF n1(1)] phi_lowerbound_1[OF n]
```
```   688     have c:"\<phi> n > 0 \<and> \<phi> n < n - 1" by arith
```
```   689     from nm[rule_format, OF c] afn have False ..}
```
```   690   hence "\<phi> n = n - 1" by blast
```
```   691   with phi_prime[of n] n1(1,2) show ?thesis by simp
```
```   692 qed
```
```   693
```
```   694 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
```
```   695   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   696 proof
```
```   697   assume ?rhs thus ?lhs by blast
```
```   698 next
```
```   699   assume H: ?lhs then obtain n where n: "P n" by blast
```
```   700   let ?x = "Least P"
```
```   701   {fix m assume m: "m < ?x"
```
```   702     from not_less_Least[OF m] have "\<not> P m" .}
```
```   703   with LeastI_ex[OF H] show ?rhs by blast
```
```   704 qed
```
```   705
```
```   706 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
```
```   707   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   708 proof-
```
```   709   {assume ?rhs hence ?lhs by blast}
```
```   710   moreover
```
```   711   { assume H: ?lhs then obtain n where n: "P n" by blast
```
```   712     let ?x = "Least P"
```
```   713     {fix m assume m: "m < ?x"
```
```   714       from not_less_Least[OF m] have "\<not> P m" .}
```
```   715     with LeastI_ex[OF H] have ?rhs by blast}
```
```   716   ultimately show ?thesis by blast
```
```   717 qed
```
```   718
```
```   719 lemma power_mod: "((x::nat) mod m)^n mod m = x^n mod m"
```
```   720 proof(induct n)
```
```   721   case 0 thus ?case by simp
```
```   722 next
```
```   723   case (Suc n)
```
```   724   have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m"
```
```   725     by (simp add: mod_mult_right_eq[symmetric])
```
```   726   also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp
```
```   727   also have "\<dots> = x^(Suc n) mod m"
```
```   728     by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric])
```
```   729   finally show ?case .
```
```   730 qed
```
```   731
```
```   732 lemma lucas:
```
```   733   assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
```
```   734   and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> \<not> [a^((n - 1) div p) = 1] (mod n)"
```
```   735   shows "prime n"
```
```   736 proof-
```
```   737   from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
```
```   738   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
```
```   739   from lucas_coprime_lemma[OF n01(3) an1] cong_coprime[OF an1]
```
```   740   have an: "coprime a n" "coprime (a^(n - 1)) n" by (simp_all add: coprime_commute)
```
```   741   {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
```
```   742     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
```
```   743       m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
```
```   744     {assume nm1: "(n - 1) mod m > 0"
```
```   745       from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
```
```   746       let ?y = "a^ ((n - 1) div m * m)"
```
```   747       note mdeq = mod_div_equality[of "(n - 1)" m]
```
```   748       from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]],
```
```   749         of "(n - 1) div m * m"]
```
```   750       have yn: "coprime ?y n" by (simp add: coprime_commute)
```
```   751       have "?y mod n = (a^m)^((n - 1) div m) mod n"
```
```   752         by (simp add: algebra_simps power_mult)
```
```   753       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
```
```   754         using power_mod[of "a^m" n "(n - 1) div m"] by simp
```
```   755       also have "\<dots> = 1" using m(3)[unfolded modeq_def onen] onen
```
```   756         by (simp add: power_Suc0)
```
```   757       finally have th3: "?y mod n = 1"  .
```
```   758       have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
```
```   759         using an1[unfolded modeq_def onen] onen
```
```   760           mod_div_equality[of "(n - 1)" m, symmetric]
```
```   761         by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def)
```
```   762       from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2]
```
```   763       have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"  .
```
```   764       from m(4)[rule_format, OF th0] nm1
```
```   765         less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
```
```   766       have False by blast }
```
```   767     hence "(n - 1) mod m = 0" by auto
```
```   768     then have mn: "m dvd n - 1" by presburger
```
```   769     then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
```
```   770     from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
```
```   771     from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast
```
```   772     hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
```
```   773     have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
```
```   774       by (simp add: power_mult)
```
```   775     also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
```
```   776     also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
```
```   777     also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..
```
```   778     also have "\<dots> = 1" using m(3) onen by (simp add: modeq_def power_Suc0)
```
```   779     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
```
```   780       using onen by (simp add: modeq_def)
```
```   781     with pn[rule_format, OF th] have False by blast}
```
```   782   hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
```
```   783   from lucas_weak[OF n2 an1 th] show ?thesis .
```
```   784 qed
```
```   785
```
```   786 (* Definition of the order of a number mod n (0 in non-coprime case).        *)
```
```   787
```
```   788 definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
```
```   789
```
```   790 (* This has the expected properties.                                         *)
```
```   791
```
```   792 lemma coprime_ord:
```
```   793   assumes na: "coprime n a"
```
```   794   shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))"
```
```   795 proof-
```
```   796   let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
```
```   797   from euclid[of a] obtain p where p: "prime p" "a < p" by blast
```
```   798   from na have o: "ord n a = Least ?P" by (simp add: ord_def)
```
```   799   {assume "n=0 \<or> n=1" with na have "\<exists>m>0. ?P m" apply auto apply (rule exI[where x=1]) by (simp  add: modeq_def)}
```
```   800   moreover
```
```   801   {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
```
```   802     from na have na': "coprime a n" by (simp add: coprime_commute)
```
```   803     from phi_lowerbound_1[OF n2] fermat_little[OF na']
```
```   804     have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="\<phi> n"], auto) }
```
```   805   ultimately have ex: "\<exists>m>0. ?P m" by blast
```
```   806   from nat_exists_least_iff'[of ?P] ex na show ?thesis
```
```   807     unfolding o[symmetric] by auto
```
```   808 qed
```
```   809 (* With the special value 0 for non-coprime case, it's more convenient.      *)
```
```   810 lemma ord_works:
```
```   811  "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
```
```   812 apply (cases "coprime n a")
```
```   813 using coprime_ord[of n a]
```
```   814 by (blast, simp add: ord_def modeq_def)
```
```   815
```
```   816 lemma ord: "[a^(ord n a) = 1] (mod n)" using ord_works by blast
```
```   817 lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
```
```   818   using ord_works by blast
```
```   819 lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> ~coprime n a"
```
```   820 by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
```
```   821
```
```   822 lemma ord_divides:
```
```   823  "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   824 proof
```
```   825   assume rh: ?rhs
```
```   826   then obtain k where "d = ord n a * k" unfolding dvd_def by blast
```
```   827   hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
```
```   828     by (simp add : modeq_def power_mult power_mod)
```
```   829   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
```
```   830     using ord[of a n, unfolded modeq_def]
```
```   831     by (simp add: modeq_def power_mod power_Suc0)
```
```   832   finally  show ?lhs .
```
```   833 next
```
```   834   assume lh: ?lhs
```
```   835   { assume H: "\<not> coprime n a"
```
```   836     hence o: "ord n a = 0" by (simp add: ord_def)
```
```   837     {assume d: "d=0" with o H have ?rhs by (simp add: modeq_def)}
```
```   838     moreover
```
```   839     {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
```
```   840       from H[unfolded coprime]
```
```   841       obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
```
```   842       from lh[unfolded nat_mod]
```
```   843       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
```
```   844       hence "a ^ d + n * q1 - n * q2 = 1" by simp
```
```   845       with dvd_diff_nat [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
```
```   846       with p(3) have False by simp
```
```   847       hence ?rhs ..}
```
```   848     ultimately have ?rhs by blast}
```
```   849   moreover
```
```   850   {assume H: "coprime n a"
```
```   851     let ?o = "ord n a"
```
```   852     let ?q = "d div ord n a"
```
```   853     let ?r = "d mod ord n a"
```
```   854     from cong_exp[OF ord[of a n], of ?q]
```
```   855     have eqo: "[(a^?o)^?q = 1] (mod n)"  by (simp add: modeq_def power_Suc0)
```
```   856     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
```
```   857     hence op: "?o > 0" by simp
```
```   858     from mod_div_equality[of d "ord n a"] lh
```
```   859     have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult.commute)
```
```   860     hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
```
```   861       by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
```
```   862     hence th: "[a^?r = 1] (mod n)"
```
```   863       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
```
```   864       apply (simp add: modeq_def del: One_nat_def)
```
```   865       by (simp add: mod_mult_left_eq[symmetric])
```
```   866     {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
```
```   867     moreover
```
```   868     {assume r: "?r \<noteq> 0"
```
```   869       with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
```
```   870       from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
```
```   871       have ?rhs by blast}
```
```   872     ultimately have ?rhs by blast}
```
```   873   ultimately  show ?rhs by blast
```
```   874 qed
```
```   875
```
```   876 lemma order_divides_phi: "coprime n a \<Longrightarrow> ord n a dvd \<phi> n"
```
```   877 using ord_divides fermat_little coprime_commute by simp
```
```   878 lemma order_divides_expdiff:
```
```   879   assumes na: "coprime n a"
```
```   880   shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   881 proof-
```
```   882   {fix n a d e
```
```   883     assume na: "coprime n a" and ed: "(e::nat) \<le> d"
```
```   884     hence "\<exists>c. d = e + c" by arith
```
```   885     then obtain c where c: "d = e + c" by arith
```
```   886     from na have an: "coprime a n" by (simp add: coprime_commute)
```
```   887     from coprime_exp[OF na, of e]
```
```   888     have aen: "coprime (a^e) n" by (simp add: coprime_commute)
```
```   889     from coprime_exp[OF na, of c]
```
```   890     have acn: "coprime (a^c) n" by (simp add: coprime_commute)
```
```   891     have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
```
```   892       using c by simp
```
```   893     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
```
```   894     also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
```
```   895       using cong_mult_lcancel_eq[OF aen, of "a^c" "a^0"] by simp
```
```   896     also  have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
```
```   897     also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
```
```   898       using cong_add_lcancel_eq[of e c 0 "ord n a", simplified cong_0_divides]
```
```   899       by simp
```
```   900     finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
```
```   901       using c by simp }
```
```   902   note th = this
```
```   903   have "e \<le> d \<or> d \<le> e" by arith
```
```   904   moreover
```
```   905   {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
```
```   906   moreover
```
```   907   {assume de: "d \<le> e"
```
```   908     from th[OF na de] have ?thesis by (simp add: cong_commute) }
```
```   909   ultimately show ?thesis by blast
```
```   910 qed
```
```   911
```
```   912 (* Another trivial primality characterization.                               *)
```
```   913
```
```   914 lemma prime_prime_factor:
```
```   915   "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
```
```   916 proof-
```
```   917   {assume n: "n=0 \<or> n=1" hence ?thesis using prime_0 two_is_prime by auto}
```
```   918   moreover
```
```   919   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   920     {assume pn: "prime n"
```
```   921
```
```   922       from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
```
```   923         using n
```
```   924         apply (cases "n = 0 \<or> n=1",simp)
```
```   925         by (clarsimp, erule_tac x="p" in allE, auto)}
```
```   926     moreover
```
```   927     {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
```
```   928       from n have n1: "n > 1" by arith
```
```   929       {fix m assume m: "m dvd n" "m\<noteq>1"
```
```   930         from prime_factor[OF m(2)] obtain p where
```
```   931           p: "prime p" "p dvd m" by blast
```
```   932         from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
```
```   933         with p(2) have "n dvd m"  by simp
```
```   934         hence "m=n"  using dvd_antisym[OF m(1)] by simp }
```
```   935       with n1 have "prime n"  unfolding prime_def by auto }
```
```   936     ultimately have ?thesis using n by blast}
```
```   937   ultimately       show ?thesis by auto
```
```   938 qed
```
```   939
```
```   940 lemma prime_divisor_sqrt:
```
```   941   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
```
```   942 proof-
```
```   943   {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1
```
```   944     by (auto simp add: nat_power_eq_0_iff)}
```
```   945   moreover
```
```   946   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   947     hence np: "n > 1" by arith
```
```   948     {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"
```
```   949       from H d have d1n: "d = 1 \<or> d=n" by blast
```
```   950       {assume dn: "d=n"
```
```   951         have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
```
```   952         with dn d(2) have "d=1" by simp}
```
```   953       with d1n have "d = 1" by blast  }
```
```   954     moreover
```
```   955     {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
```
```   956       from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp
```
```   957       hence dp: "d > 0" by simp
```
```   958       from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
```
```   959       from n dp e have ep:"e > 0" by simp
```
```   960       have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
```
```   961         by (auto simp add: e power2_eq_square mult_le_cancel_left)
```
```   962       moreover
```
```   963       {assume h: "d\<^sup>2 \<le> n"
```
```   964         from H[rule_format, of d] h d have "d = 1" by blast}
```
```   965       moreover
```
```   966       {assume h: "e\<^sup>2 \<le> n"
```
```   967         from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute)
```
```   968         with H[rule_format, of e] h have "e=1" by simp
```
```   969         with e have "d = n" by simp}
```
```   970       ultimately have "d=1 \<or> d=n"  by blast}
```
```   971     ultimately have ?thesis unfolding prime_def using np n(2) by blast}
```
```   972   ultimately show ?thesis by auto
```
```   973 qed
```
```   974 lemma prime_prime_factor_sqrt:
```
```   975   "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)"
```
```   976   (is "?lhs \<longleftrightarrow>?rhs")
```
```   977 proof-
```
```   978   {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto}
```
```   979   moreover
```
```   980   {assume n: "n\<noteq>0" "n\<noteq>1"
```
```   981     {assume H: ?lhs
```
```   982       from H[unfolded prime_divisor_sqrt] n
```
```   983       have ?rhs
```
```   984         apply clarsimp
```
```   985         apply (erule_tac x="p" in allE)
```
```   986         apply simp
```
```   987         done
```
```   988     }
```
```   989     moreover
```
```   990     {assume H: ?rhs
```
```   991       {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
```
```   992         from prime_factor[OF d(3)]
```
```   993         obtain p where p: "prime p" "p dvd d" by blast
```
```   994         from n have np: "n > 0" by arith
```
```   995         from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
```
```   996         hence dp: "d > 0" by arith
```
```   997         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
```
```   998         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
```
```   999         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
```
```  1000       with n prime_divisor_sqrt  have ?lhs by auto}
```
```  1001     ultimately have ?thesis by blast }
```
```  1002   ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
```
```  1003 qed
```
```  1004 (* Pocklington theorem. *)
```
```  1005
```
```  1006 lemma pocklington_lemma:
```
```  1007   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
```
```  1008   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
```
```  1009   and pp: "prime p" and pn: "p dvd n"
```
```  1010   shows "[p = 1] (mod q)"
```
```  1011 proof-
```
```  1012   from pp prime_0 prime_1 have p01: "p \<noteq> 0" "p \<noteq> 1" by - (rule ccontr, simp)+
```
```  1013   from cong_1_divides[OF an, unfolded nqr, unfolded dvd_def]
```
```  1014   obtain k where k: "a ^ (q * r) - 1 = n*k" by blast
```
```  1015   from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
```
```  1016   {assume a0: "a = 0"
```
```  1017     hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
```
```  1018     with n an mod_less[of 1 n]  have False by (simp add: power_0_left modeq_def)}
```
```  1019   hence a0: "a\<noteq>0" ..
```
```  1020   from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
```
```  1021   hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
```
```  1022   with k l have "a ^ (q * r) = p*l*k + 1" by simp
```
```  1023   hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
```
```  1024   hence odq: "ord p (a^r) dvd q"
```
```  1025     unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod  by blast
```
```  1026   from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
```
```  1027   {assume d1: "d \<noteq> 1"
```
```  1028     from prime_factor[OF d1] obtain P where P: "prime P" "P dvd d" by blast
```
```  1029     from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
```
```  1030     from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
```
```  1031     from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
```
```  1032     have P0: "P \<noteq> 0" using P(1) prime_0 by - (rule ccontr, simp)
```
```  1033     from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
```
```  1034     from d s t P0  have s': "ord p (a^r) * t = s" by algebra
```
```  1035     have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra
```
```  1036     hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
```
```  1037       by (simp only: power_mult)
```
```  1038     have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)"
```
```  1039       by (rule cong_exp, rule ord)
```
```  1040     then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
```
```  1041       by (simp add: power_Suc0)
```
```  1042     from cong_1_divides[OF th] exps have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" by simp
```
```  1043     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
```
```  1044     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
```
```  1045     with p01 pn pd0 have False unfolding coprime by auto}
```
```  1046   hence d1: "d = 1" by blast
```
```  1047   hence o: "ord p (a^r) = q" using d by simp
```
```  1048   from pp phi_prime[of p] have phip: " \<phi> p = p - 1" by simp
```
```  1049   {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
```
```  1050     from pp[unfolded prime_def] d have dp: "d = p" by blast
```
```  1051     from n have n12:"Suc (n - 2) = n - 1" by arith
```
```  1052     with divides_rexp[OF d(2)[unfolded dp], of "n - 2"]
```
```  1053     have th0: "p dvd a ^ (n - 1)" by simp
```
```  1054     from n have n0: "n \<noteq> 0" by simp
```
```  1055     from d(2) an n12[symmetric] have a0: "a \<noteq> 0"
```
```  1056       by - (rule ccontr, simp add: modeq_def)
```
```  1057     have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto
```
```  1058     from coprime_minus1[OF th1, unfolded coprime]
```
```  1059       dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp
```
```  1060     have False by auto}
```
```  1061   hence cpa: "coprime p a" using coprime by auto
```
```  1062   from coprime_exp[OF cpa, of r] coprime_commute
```
```  1063   have arp: "coprime (a^r) p" by blast
```
```  1064   from fermat_little[OF arp, simplified ord_divides] o phip
```
```  1065   have "q dvd (p - 1)" by simp
```
```  1066   then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast
```
```  1067   from prime_0 pp have p0:"p \<noteq> 0" by -  (rule ccontr, auto)
```
```  1068   from p0 d have "p + q * 0 = 1 + q * d" by simp
```
```  1069   with nat_mod[of p 1 q, symmetric]
```
```  1070   show ?thesis by blast
```
```  1071 qed
```
```  1072
```
```  1073 lemma pocklington:
```
```  1074   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
```
```  1075   and an: "[a^ (n - 1) = 1] (mod n)"
```
```  1076   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
```
```  1077   shows "prime n"
```
```  1078 unfolding prime_prime_factor_sqrt[of n]
```
```  1079 proof-
```
```  1080   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)"
```
```  1081   from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
```
```  1082   {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
```
```  1083     from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
```
```  1084     hence pq: "p \<le> q" unfolding exp_mono_le .
```
```  1085     from pocklington_lemma[OF n nqr an aq p(1,2)]  cong_1_divides
```
```  1086     have th: "q dvd p - 1" by blast
```
```  1087     have "p - 1 \<noteq> 0"using prime_ge_2[OF p(1)] by arith
```
```  1088     with divides_ge[OF th] pq have False by arith }
```
```  1089   with n01 show ?ths by blast
```
```  1090 qed
```
```  1091
```
```  1092 (* Variant for application, to separate the exponentiation.                  *)
```
```  1093 lemma pocklington_alt:
```
```  1094   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
```
```  1095   and an: "[a^ (n - 1) = 1] (mod n)"
```
```  1096   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)"
```
```  1097   shows "prime n"
```
```  1098 proof-
```
```  1099   {fix p assume p: "prime p" "p dvd q"
```
```  1100     from aq[rule_format] p obtain b where
```
```  1101       b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
```
```  1102     {assume a0: "a=0"
```
```  1103       from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
```
```  1104       hence False using n by (simp add: modeq_def dvd_eq_mod_eq_0[symmetric])}
```
```  1105     hence a0: "a\<noteq> 0" ..
```
```  1106     hence a1: "a \<ge> 1" by arith
```
```  1107     from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
```
```  1108     {assume b0: "b = 0"
```
```  1109       from p(2) nqr have "(n - 1) mod p = 0"
```
```  1110         apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp)
```
```  1111       with mod_div_equality[of "n - 1" p]
```
```  1112       have "(n - 1) div p * p= n - 1" by auto
```
```  1113       hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
```
```  1114         by (simp only: power_mult[symmetric])
```
```  1115       from prime_ge_2[OF p(1)] have pS: "Suc (p - 1) = p" by arith
```
```  1116       from b(1) have d: "n dvd a^((n - 1) div p)" unfolding b0 cong_0_divides .
```
```  1117       from divides_rexp[OF d, of "p - 1"] pS eq cong_divides[OF an] n
```
```  1118       have False by simp}
```
```  1119     then have b0: "b \<noteq> 0" ..
```
```  1120     hence b1: "b \<ge> 1" by arith
```
```  1121     from cong_coprime[OF cong_sub[OF b(1) cong_refl[of 1] ath b1]] b(2) nqr
```
```  1122     have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute)}
```
```  1123   hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
```
```  1124     by blast
```
```  1125   from pocklington[OF n nqr sqr an th] show ?thesis .
```
```  1126 qed
```
```  1127
```
```  1128 (* Prime factorizations.                                                     *)
```
```  1129
```
```  1130 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
```
```  1131
```
```  1132 lemma primefact: assumes n: "n \<noteq> 0"
```
```  1133   shows "\<exists>ps. primefact ps n"
```
```  1134 using n
```
```  1135 proof(induct n rule: nat_less_induct)
```
```  1136   fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
```
```  1137   let ?ths = "\<exists>ps. primefact ps n"
```
```  1138   {assume "n = 1"
```
```  1139     hence "primefact [] n" by (simp add: primefact_def)
```
```  1140     hence ?ths by blast }
```
```  1141   moreover
```
```  1142   {assume n1: "n \<noteq> 1"
```
```  1143     with n have n2: "n \<ge> 2" by arith
```
```  1144     from prime_factor[OF n1] obtain p where p: "prime p" "p dvd n" by blast
```
```  1145     from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
```
```  1146     from n m have m0: "m > 0" "m\<noteq>0" by auto
```
```  1147     from prime_ge_2[OF p(1)] have "1 < p" by arith
```
```  1148     with m0 m have mn: "m < n" by auto
```
```  1149     from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
```
```  1150     from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
```
```  1151     hence ?ths by blast}
```
```  1152   ultimately show ?ths by blast
```
```  1153 qed
```
```  1154
```
```  1155 lemma primefact_contains:
```
```  1156   assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
```
```  1157   shows "p \<in> set ps"
```
```  1158   using pf p pn
```
```  1159 proof(induct ps arbitrary: p n)
```
```  1160   case Nil thus ?case by (auto simp add: primefact_def)
```
```  1161 next
```
```  1162   case (Cons q qs p n)
```
```  1163   from Cons.prems[unfolded primefact_def]
```
```  1164   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
```
```  1165   {assume "p dvd q"
```
```  1166     with p(1) q(1) have "p = q" unfolding prime_def by auto
```
```  1167     hence ?case by simp}
```
```  1168   moreover
```
```  1169   { assume h: "p dvd foldr op * qs 1"
```
```  1170     from q(3) have pqs: "primefact qs (foldr op * qs 1)"
```
```  1171       by (simp add: primefact_def)
```
```  1172     from Cons.hyps[OF pqs p(1) h] have ?case by simp}
```
```  1173   ultimately show ?case using prime_divprod[OF p] by blast
```
```  1174 qed
```
```  1175
```
```  1176 lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
```
```  1177   by (auto simp add: primefact_def list_all_iff)
```
```  1178
```
```  1179 (* Variant of Lucas theorem.                                                 *)
```
```  1180
```
```  1181 lemma lucas_primefact:
```
```  1182   assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
```
```  1183   and psn: "foldr op * ps 1 = n - 1"
```
```  1184   and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
```
```  1185   shows "prime n"
```
```  1186 proof-
```
```  1187   {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
```
```  1188     from psn psp have psn1: "primefact ps (n - 1)"
```
```  1189       by (auto simp add: list_all_iff primefact_variant)
```
```  1190     from p(3) primefact_contains[OF psn1 p(1,2)] psp
```
```  1191     have False by (induct ps, auto)}
```
```  1192   with lucas[OF n an] show ?thesis by blast
```
```  1193 qed
```
```  1194
```
```  1195 (* Variant of Pocklington theorem.                                           *)
```
```  1196
```
```  1197 lemma mod_le: assumes n: "n \<noteq> (0::nat)" shows "m mod n \<le> m"
```
```  1198 proof-
```
```  1199     from mod_div_equality[of m n]
```
```  1200     have "\<exists>x. x + m mod n = m" by blast
```
```  1201     then show ?thesis by auto
```
```  1202 qed
```
```  1203
```
```  1204
```
```  1205 lemma pocklington_primefact:
```
```  1206   assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
```
```  1207   and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
```
```  1208   and bqn: "(b^q) mod n = 1"
```
```  1209   and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
```
```  1210   shows "prime n"
```
```  1211 proof-
```
```  1212   from bqn psp qrn
```
```  1213   have bqn: "a ^ (n - 1) mod n = 1"
```
```  1214     and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  unfolding arnb[symmetric] power_mod
```
```  1215     by (simp_all add: power_mult[symmetric] algebra_simps)
```
```  1216   from n  have n0: "n > 0" by arith
```
```  1217   from mod_div_equality[of "a^(n - 1)" n]
```
```  1218     mod_less_divisor[OF n0, of "a^(n - 1)"]
```
```  1219   have an1: "[a ^ (n - 1) = 1] (mod n)"
```
```  1220     unfolding nat_mod bqn
```
```  1221     apply -
```
```  1222     apply (rule exI[where x="0"])
```
```  1223     apply (rule exI[where x="a^(n - 1) div n"])
```
```  1224     by (simp add: algebra_simps)
```
```  1225   {fix p assume p: "prime p" "p dvd q"
```
```  1226     from psp psq have pfpsq: "primefact ps q"
```
```  1227       by (auto simp add: primefact_variant list_all_iff)
```
```  1228     from psp primefact_contains[OF pfpsq p]
```
```  1229     have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
```
```  1230       by (simp add: list_all_iff)
```
```  1231     from prime_ge_2[OF p(1)] have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" by arith+
```
```  1232     from div_mult1_eq[of r q p] p(2)
```
```  1233     have eq1: "r* (q div p) = (n - 1) div p"
```
```  1234       unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute)
```
```  1235     have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
```
```  1236     from n0 have n00: "n \<noteq> 0" by arith
```
```  1237     from mod_le[OF n00]
```
```  1238     have th10: "a ^ ((n - 1) div p) mod n \<le> a ^ ((n - 1) div p)" .
```
```  1239     {assume "a ^ ((n - 1) div p) mod n = 0"
```
```  1240       then obtain s where s: "a ^ ((n - 1) div p) = n*s"
```
```  1241         unfolding mod_eq_0_iff by blast
```
```  1242       hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
```
```  1243       from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
```
```  1244       from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
```
```  1245       have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
```
```  1246       with eq0 have "a^ (n - 1) = (n*s)^p"
```
```  1247         by (simp add: power_mult[symmetric])
```
```  1248       hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
```
```  1249       also have "\<dots> = 0" by (simp add: mult.assoc)
```
```  1250       finally have False by simp }
```
```  1251       then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
```
```  1252     have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
```
```  1253       unfolding modeq_def by simp
```
```  1254     from cong_sub[OF th1 cong_refl[of 1]]  ath[OF th10 th11]
```
```  1255     have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
```
```  1256       by blast
```
```  1257     from cong_coprime[OF th] p'[unfolded eq1]
```
```  1258     have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute) }
```
```  1259   with pocklington[OF n qrn[symmetric] nq2 an1]
```
```  1260   show ?thesis by blast
```
```  1261 qed
```
```  1262
```
```  1263 end
```