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