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