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