Restoration of Pocklington.thy. Tidying.
authorpaulson <lp15@cam.ac.uk>
Tue Feb 04 21:28:38 2014 +0000 (2014-02-04)
changeset 55321eadea363deb6
parent 55320 8a6ee5c1f2e0
child 55322 3bf50e3cd727
Restoration of Pocklington.thy. Tidying.
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Tue Feb 04 21:01:35 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Feb 04 21:28:38 2014 +0000
     1.3 @@ -154,13 +154,12 @@
     1.4    unfolding cong_int_def  by (metis mod_diff_cong) 
     1.5  
     1.6  lemma cong_diff_aux_int:
     1.7 -  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
     1.8 -      [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
     1.9 +  "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
    1.10 +   (a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
    1.11    by (metis cong_diff_int tsub_eq)
    1.12  
    1.13  lemma cong_diff_nat:
    1.14 -  assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
    1.15 -    "[c = d] (mod m)"
    1.16 +  assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d" 
    1.17    shows "[a - c = b - d] (mod m)"
    1.18    using assms by (rule cong_diff_aux_int [transferred]);
    1.19  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Feb 04 21:28:38 2014 +0000
     2.3 @@ -0,0 +1,815 @@
     2.4 +(*  Title:      HOL/Number_Theory/Pocklington.thy
     2.5 +    Author:     Amine Chaieb
     2.6 +*)
     2.7 +
     2.8 +header {* Pocklington's Theorem for Primes *}
     2.9 +
    2.10 +theory Pocklington
    2.11 +imports Residues
    2.12 +begin
    2.13 +
    2.14 +subsection{*Lemmas about previously defined terms*}
    2.15 +
    2.16 +lemma prime: 
    2.17 +  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
    2.18 +  (is "?lhs \<longleftrightarrow> ?rhs")
    2.19 +proof-
    2.20 +  {assume "p=0 \<or> p=1" hence ?thesis
    2.21 +    by (metis one_not_prime_nat zero_not_prime_nat)}
    2.22 +  moreover
    2.23 +  {assume p0: "p\<noteq>0" "p\<noteq>1"
    2.24 +    {assume H: "?lhs"
    2.25 +      {fix m assume m: "m > 0" "m < p"
    2.26 +        {assume "m=1" hence "coprime p m" by simp}
    2.27 +        moreover
    2.28 +        {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
    2.29 +          have "coprime p m" by simp}
    2.30 +        ultimately have "coprime p m" 
    2.31 +          by (metis H prime_imp_coprime_nat)}
    2.32 +      hence ?rhs using p0 by auto}
    2.33 +    moreover
    2.34 +    { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
    2.35 +      obtain q where q: "prime q" "q dvd p"
    2.36 +        by (metis p0(2) prime_factor_nat) 
    2.37 +      have q0: "q > 0"
    2.38 +        by (metis prime_gt_0_nat q(1))
    2.39 +      from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
    2.40 +      {assume "q = p" hence ?lhs using q(1) by blast}
    2.41 +      moreover
    2.42 +      {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
    2.43 +        from H[rule_format, of q] qplt q0 have "coprime p q" by arith
    2.44 +       hence ?lhs
    2.45 +         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat q(1) q(2))}
    2.46 +      ultimately have ?lhs by blast}
    2.47 +    ultimately have ?thesis by blast}
    2.48 +  ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
    2.49 +qed
    2.50 +
    2.51 +lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
    2.52 +proof-
    2.53 +  have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto
    2.54 +  thus ?thesis by simp
    2.55 +qed
    2.56 +
    2.57 +
    2.58 +subsection{*Some basic theorems about solving congruences*}
    2.59 +
    2.60 +lemma cong_solve: 
    2.61 +  fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
    2.62 +proof-
    2.63 +  {assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)}
    2.64 +  moreover
    2.65 +  {assume az: "a\<noteq>0"
    2.66 +  from bezout_add_strong_nat[OF az, of n]
    2.67 +  obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast
    2.68 +  from dxy(1,2) have d1: "d = 1"
    2.69 +    by (metis assms coprime_nat) 
    2.70 +  hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
    2.71 +  hence "a*(x*b) = n*(y*b) + b"
    2.72 +    by (auto simp add: algebra_simps)
    2.73 +  hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
    2.74 +  hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
    2.75 +  hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def .
    2.76 +  hence ?thesis by blast}
    2.77 +ultimately  show ?thesis by blast
    2.78 +qed
    2.79 +
    2.80 +lemma cong_solve_unique: 
    2.81 +  fixes n::nat assumes an: "coprime a n" and nz: "n \<noteq> 0"
    2.82 +  shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)"
    2.83 +proof-
    2.84 +  let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
    2.85 +  from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
    2.86 +  let ?x = "x mod n"
    2.87 +  from x have th: "[a * ?x = b] (mod n)"
    2.88 +    by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
    2.89 +  from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
    2.90 +  {fix y assume Py: "y < n" "[a * y = b] (mod n)"
    2.91 +    from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def)
    2.92 +    hence "[y = ?x] (mod n)"
    2.93 +      by (metis an cong_mult_lcancel_nat) 
    2.94 +    with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
    2.95 +    have "y = ?x" by (simp add: cong_nat_def)}
    2.96 +  with Px show ?thesis by blast
    2.97 +qed
    2.98 +
    2.99 +lemma cong_solve_unique_nontrivial:
   2.100 +  assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
   2.101 +  shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
   2.102 +proof-
   2.103 +  from pa have ap: "coprime a p"
   2.104 +    by (metis gcd_nat.commute) 
   2.105 +  have px:"coprime x p"
   2.106 +    by (metis gcd_nat.commute p prime x0 xp)
   2.107 +  obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
   2.108 +    by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   2.109 +  {assume y0: "y = 0"
   2.110 +    with y(2) have th: "p dvd a"
   2.111 +      by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right) 
   2.112 +    have False
   2.113 +      by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
   2.114 +  with y show ?thesis unfolding Ex1_def using neq0_conv by blast
   2.115 +qed
   2.116 +
   2.117 +lemma cong_unique_inverse_prime:
   2.118 +  fixes p::nat 
   2.119 +  assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
   2.120 +  shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
   2.121 +by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
   2.122 +
   2.123 +lemma chinese_remainder_coprime_unique:
   2.124 +  fixes a::nat 
   2.125 +  assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0"
   2.126 +  and ma: "coprime m a" and nb: "coprime n b"
   2.127 +  shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
   2.128 +proof-
   2.129 +  let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)"
   2.130 +  from binary_chinese_remainder_unique_nat[OF ab az bz]
   2.131 +  obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)"
   2.132 +    "\<forall>y. ?P y \<longrightarrow> y = x" by blast
   2.133 +  from ma nb x
   2.134 +  have "coprime x a" "coprime x b"
   2.135 +    by (metis cong_gcd_eq_nat)+
   2.136 +  then have "coprime x (a*b)"
   2.137 +    by (metis coprime_mul_eq_nat)
   2.138 +  with x show ?thesis by blast
   2.139 +qed
   2.140 +
   2.141 +
   2.142 +subsection{*Lucas's theorem*}
   2.143 +
   2.144 +lemma phi_limit_strong: "phi(n) \<le> n - 1"
   2.145 +proof -
   2.146 +  have "phi n = card {x. 0 < x \<and> x < int n \<and> coprime x (int n)}"
   2.147 +    by (simp add: phi_def)
   2.148 +  also have "... \<le> card {0 <..< int n}"
   2.149 +    by (rule card_mono) auto
   2.150 +  also have "... = card {0 <..< n}"
   2.151 +    by (simp add: transfer_nat_int_set_functions)
   2.152 +  also have "... \<le> n - 1"
   2.153 +    by (metis card_greaterThanLessThan le_refl One_nat_def)
   2.154 +  finally show ?thesis .
   2.155 +qed
   2.156 +
   2.157 +lemma phi_lowerbound_1: assumes n: "n \<ge> 2"
   2.158 +  shows "phi n \<ge> 1"
   2.159 +proof -
   2.160 +  have "1 \<le> card {0::int <.. 1}"
   2.161 +    by auto
   2.162 +  also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
   2.163 +    apply (rule card_mono) using assms
   2.164 +    apply (auto simp add: )
   2.165 +    by (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
   2.166 +  also have "... = phi n"
   2.167 +    by (simp add: phi_def)
   2.168 +  finally show ?thesis .
   2.169 +qed
   2.170 +
   2.171 +lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2"
   2.172 +  shows "phi(int n) \<ge> 1"
   2.173 +by (metis n nat_le_iff nat_numeral phi_lowerbound_1)
   2.174 +
   2.175 +lemma euler_theorem_nat:
   2.176 +  fixes m::nat 
   2.177 +  assumes "coprime a m"
   2.178 +  shows "[a ^ phi m = 1] (mod m)"
   2.179 +by (metis assms le0 euler_theorem [transferred])
   2.180 +
   2.181 +lemma lucas_coprime_lemma:
   2.182 +  fixes n::nat 
   2.183 +  assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
   2.184 +  shows "coprime a n"
   2.185 +proof-
   2.186 +  {assume "n=1" hence ?thesis by simp}
   2.187 +  moreover
   2.188 +  {assume "n = 0" hence ?thesis using am m 
   2.189 +     by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)}
   2.190 +  moreover
   2.191 +  {assume n: "n\<noteq>0" "n\<noteq>1"
   2.192 +    from m obtain m' where m': "m = Suc m'" by (cases m, blast+)
   2.193 +    {fix d
   2.194 +      assume d: "d dvd a" "d dvd n"
   2.195 +      from n have n1: "1 < n" by arith
   2.196 +      from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp
   2.197 +      from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m')
   2.198 +      from dvd_mod_iff[OF d(2), of "a^m"] dam am1
   2.199 +      have "d = 1" by simp }
   2.200 +    hence ?thesis by auto
   2.201 +  }
   2.202 +  ultimately show ?thesis by blast
   2.203 +qed
   2.204 +
   2.205 +lemma lucas_weak:
   2.206 +  fixes n::nat 
   2.207 +  assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)"
   2.208 +  and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)"
   2.209 +  shows "prime n"
   2.210 +proof-
   2.211 +  from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+
   2.212 +  from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" .
   2.213 +  from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)"
   2.214 +    by auto 
   2.215 +  {assume "phi n \<noteq> n - 1"
   2.216 +    with phi_limit_strong phi_lowerbound_1_nat [OF n]
   2.217 +    have c:"phi n > 0 \<and> phi n < n - 1"
   2.218 +      by (metis gr0I leD less_linear not_one_le_zero)
   2.219 +    from nm[rule_format, OF c] afn have False ..}
   2.220 +  hence "phi n = n - 1" by blast
   2.221 +  with prime_phi phi_prime n1(1,2) show ?thesis
   2.222 +    by auto
   2.223 +qed
   2.224 +
   2.225 +lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
   2.226 +  (is "?lhs \<longleftrightarrow> ?rhs")
   2.227 +proof
   2.228 +  assume ?rhs thus ?lhs by blast
   2.229 +next
   2.230 +  assume H: ?lhs then obtain n where n: "P n" by blast
   2.231 +  let ?x = "Least P"
   2.232 +  {fix m assume m: "m < ?x"
   2.233 +    from not_less_Least[OF m] have "\<not> P m" .}
   2.234 +  with LeastI_ex[OF H] show ?rhs by blast
   2.235 +qed
   2.236 +
   2.237 +lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
   2.238 +  (is "?lhs \<longleftrightarrow> ?rhs")
   2.239 +proof-
   2.240 +  {assume ?rhs hence ?lhs by blast}
   2.241 +  moreover
   2.242 +  { assume H: ?lhs then obtain n where n: "P n" by blast
   2.243 +    let ?x = "Least P"
   2.244 +    {fix m assume m: "m < ?x"
   2.245 +      from not_less_Least[OF m] have "\<not> P m" .}
   2.246 +    with LeastI_ex[OF H] have ?rhs by blast}
   2.247 +  ultimately show ?thesis by blast
   2.248 +qed
   2.249 +
   2.250 +theorem lucas:
   2.251 +  assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
   2.252 +  and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
   2.253 +  shows "prime n"
   2.254 +proof-
   2.255 +  from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+
   2.256 +  from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
   2.257 +  from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
   2.258 +  have an: "coprime a n" "coprime (a^(n - 1)) n"
   2.259 +    by (auto simp add: coprime_exp_nat gcd_nat.commute)
   2.260 +  {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   2.261 +    from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
   2.262 +      m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
   2.263 +    {assume nm1: "(n - 1) mod m > 0"
   2.264 +      from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
   2.265 +      let ?y = "a^ ((n - 1) div m * m)"
   2.266 +      note mdeq = mod_div_equality[of "(n - 1)" m]
   2.267 +      have yn: "coprime ?y n"
   2.268 +        by (metis an(1) coprime_exp_nat gcd_nat.commute)
   2.269 +      have "?y mod n = (a^m)^((n - 1) div m) mod n"
   2.270 +        by (simp add: algebra_simps power_mult)
   2.271 +      also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
   2.272 +        using power_mod[of "a^m" n "(n - 1) div m"] by simp
   2.273 +      also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
   2.274 +        by (metis power_one)
   2.275 +      finally have th3: "?y mod n = 1"  .
   2.276 +      have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
   2.277 +        using an1[unfolded cong_nat_def onen] onen
   2.278 +          mod_div_equality[of "(n - 1)" m, symmetric]
   2.279 +        by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
   2.280 +      have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
   2.281 +        by (metis cong_mult_rcancel_nat nat_mult_commute th2 yn)
   2.282 +      from m(4)[rule_format, OF th0] nm1
   2.283 +        less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1
   2.284 +      have False by blast }
   2.285 +    hence "(n - 1) mod m = 0" by auto
   2.286 +    then have mn: "m dvd n - 1" by presburger
   2.287 +    then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast
   2.288 +    from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+
   2.289 +    obtain p where p: "prime p" "p dvd r"
   2.290 +      by (metis prime_factor_nat r01(2))
   2.291 +    hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
   2.292 +    have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
   2.293 +      by (simp add: power_mult)
   2.294 +    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
   2.295 +    also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
   2.296 +    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..
   2.297 +    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def power_Suc_0)
   2.298 +    finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
   2.299 +      using onen by (simp add: cong_nat_def)
   2.300 +    with pn[rule_format, OF th] have False by blast}
   2.301 +  hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
   2.302 +  from lucas_weak[OF n2 an1 th] show ?thesis .
   2.303 +qed
   2.304 +
   2.305 +
   2.306 +subsection{*Definition of the order of a number mod n (0 in non-coprime case)*}
   2.307 +
   2.308 +definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
   2.309 +
   2.310 +(* This has the expected properties.                                         *)
   2.311 +
   2.312 +lemma coprime_ord:
   2.313 +  fixes n::nat 
   2.314 +  assumes "coprime n a"
   2.315 +  shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> [a^ m \<noteq> 1] (mod n))"
   2.316 +proof-
   2.317 +  let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
   2.318 +  from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast
   2.319 +  from assms have o: "ord n a = Least ?P" by (simp add: ord_def)
   2.320 +  {assume "n=0 \<or> n=1" with assms have "\<exists>m>0. ?P m" 
   2.321 +      by auto}
   2.322 +  moreover
   2.323 +  {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
   2.324 +    from assms have na': "coprime a n"
   2.325 +      by (metis gcd_nat.commute)
   2.326 +    from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na']
   2.327 +    have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) }
   2.328 +  ultimately have ex: "\<exists>m>0. ?P m" by blast
   2.329 +  from nat_exists_least_iff'[of ?P] ex assms show ?thesis
   2.330 +    unfolding o[symmetric] by auto
   2.331 +qed
   2.332 +
   2.333 +(* With the special value 0 for non-coprime case, it's more convenient.      *)
   2.334 +lemma ord_works:
   2.335 +  fixes n::nat
   2.336 +  shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
   2.337 +apply (cases "coprime n a")
   2.338 +using coprime_ord[of n a]
   2.339 +by (blast, simp add: ord_def cong_nat_def)
   2.340 +
   2.341 +lemma ord:
   2.342 +  fixes n::nat
   2.343 +  shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast
   2.344 +
   2.345 +lemma ord_minimal:
   2.346 +  fixes n::nat
   2.347 +  shows "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
   2.348 +  using ord_works by blast
   2.349 +
   2.350 +lemma ord_eq_0:
   2.351 +  fixes n::nat
   2.352 +  shows "ord n a = 0 \<longleftrightarrow> ~coprime n a"
   2.353 +by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
   2.354 +
   2.355 +lemma divides_rexp: 
   2.356 +  "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" 
   2.357 +  by (simp add: dvd_mult2[of x y])
   2.358 +
   2.359 +lemma ord_divides:
   2.360 +  fixes n::nat
   2.361 +  shows "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
   2.362 +proof
   2.363 +  assume rh: ?rhs
   2.364 +  then obtain k where "d = ord n a * k" unfolding dvd_def by blast
   2.365 +  hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
   2.366 +    by (simp add : cong_nat_def power_mult power_mod)
   2.367 +  also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
   2.368 +    using ord[of a n, unfolded cong_nat_def]
   2.369 +    by (simp add: cong_nat_def power_mod)
   2.370 +  finally  show ?lhs .
   2.371 +next
   2.372 +  assume lh: ?lhs
   2.373 +  { assume H: "\<not> coprime n a"
   2.374 +    hence o: "ord n a = 0" by (simp add: ord_def)
   2.375 +    {assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)}
   2.376 +    moreover
   2.377 +    {assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto)
   2.378 +      from H
   2.379 +      obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
   2.380 +      from lh
   2.381 +      obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
   2.382 +        by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
   2.383 +      hence "a ^ d + n * q1 - n * q2 = 1" by simp
   2.384 +      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' 
   2.385 +      have "p dvd 1" by simp
   2.386 +      with p(3) have False by simp
   2.387 +      hence ?rhs ..}
   2.388 +    ultimately have ?rhs by blast}
   2.389 +  moreover
   2.390 +  {assume H: "coprime n a"
   2.391 +    let ?o = "ord n a"
   2.392 +    let ?q = "d div ord n a"
   2.393 +    let ?r = "d mod ord n a"
   2.394 +    have eqo: "[(a^?o)^?q = 1] (mod n)"
   2.395 +      by (metis cong_exp_nat ord power_one)
   2.396 +    from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
   2.397 +    hence op: "?o > 0" by simp
   2.398 +    from mod_div_equality[of d "ord n a"] lh
   2.399 +    have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult_commute)
   2.400 +    hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   2.401 +      by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
   2.402 +    hence th: "[a^?r = 1] (mod n)"
   2.403 +      using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
   2.404 +      apply (simp add: cong_nat_def del: One_nat_def)
   2.405 +      by (simp add: mod_mult_left_eq[symmetric])
   2.406 +    {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
   2.407 +    moreover
   2.408 +    {assume r: "?r \<noteq> 0"
   2.409 +      with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp
   2.410 +      from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th
   2.411 +      have ?rhs by blast}
   2.412 +    ultimately have ?rhs by blast}
   2.413 +  ultimately  show ?rhs by blast
   2.414 +qed
   2.415 +
   2.416 +lemma order_divides_phi: 
   2.417 +  fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n"
   2.418 +  by (metis ord_divides euler_theorem_nat gcd_nat.commute)
   2.419 +
   2.420 +lemma order_divides_expdiff:
   2.421 +  fixes n::nat and a::nat assumes na: "coprime n a"
   2.422 +  shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
   2.423 +proof-
   2.424 +  {fix n::nat and a::nat and d::nat and e::nat
   2.425 +    assume na: "coprime n a" and ed: "(e::nat) \<le> d"
   2.426 +    hence "\<exists>c. d = e + c" by presburger
   2.427 +    then obtain c where c: "d = e + c" by presburger
   2.428 +    from na have an: "coprime a n"
   2.429 +      by (metis gcd_nat.commute)
   2.430 +    have aen: "coprime (a^e) n"
   2.431 +      by (metis coprime_exp_nat gcd_nat.commute na)      
   2.432 +    have acn: "coprime (a^c) n"
   2.433 +      by (metis coprime_exp_nat gcd_nat.commute na) 
   2.434 +    have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
   2.435 +      using c by simp
   2.436 +    also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
   2.437 +    also have  "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)"
   2.438 +      using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp
   2.439 +    also  have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides)
   2.440 +    also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
   2.441 +      using cong_add_lcancel_nat 
   2.442 +      by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
   2.443 +    finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))"
   2.444 +      using c by simp }
   2.445 +  note th = this
   2.446 +  have "e \<le> d \<or> d \<le> e" by arith
   2.447 +  moreover
   2.448 +  {assume ed: "e \<le> d" from th[OF na ed] have ?thesis .}
   2.449 +  moreover
   2.450 +  {assume de: "d \<le> e"
   2.451 +    from th[OF na de] have ?thesis
   2.452 +    by (metis cong_sym_nat)}
   2.453 +  ultimately show ?thesis by blast
   2.454 +qed
   2.455 +
   2.456 +subsection{*Another trivial primality characterization*}
   2.457 +
   2.458 +lemma prime_prime_factor:
   2.459 +  "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
   2.460 +proof-
   2.461 +  {assume n: "n=0 \<or> n=1" 
   2.462 +   hence ?thesis
   2.463 +     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) }
   2.464 +  moreover
   2.465 +  {assume n: "n\<noteq>0" "n\<noteq>1"
   2.466 +    {assume pn: "prime n"
   2.467 +
   2.468 +      from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
   2.469 +        using n
   2.470 +        apply (cases "n = 0 \<or> n=1",simp)
   2.471 +        by (clarsimp, erule_tac x="p" in allE, auto)}
   2.472 +    moreover
   2.473 +    {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
   2.474 +      from n have n1: "n > 1" by arith
   2.475 +      {fix m assume m: "m dvd n" "m\<noteq>1"
   2.476 +       then obtain p where p: "prime p" "p dvd m"
   2.477 +         by (metis prime_factor_nat) 
   2.478 +       from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
   2.479 +       with p(2) have "n dvd m"  by simp
   2.480 +       hence "m=n"  using dvd_antisym[OF m(1)] by simp }
   2.481 +      with n1 have "prime n"  unfolding prime_def by auto }
   2.482 +    ultimately have ?thesis using n by blast}
   2.483 +  ultimately       show ?thesis by auto
   2.484 +qed
   2.485 +
   2.486 +lemma prime_divisor_sqrt:
   2.487 +  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
   2.488 +proof -
   2.489 +  {assume "n=0 \<or> n=1" hence ?thesis
   2.490 +    by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)}
   2.491 +  moreover
   2.492 +  {assume n: "n\<noteq>0" "n\<noteq>1"
   2.493 +    hence np: "n > 1" by arith
   2.494 +    {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"
   2.495 +      from H d have d1n: "d = 1 \<or> d=n" by blast
   2.496 +      {assume dn: "d=n"
   2.497 +        have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
   2.498 +        with dn d(2) have "d=1" by simp}
   2.499 +      with d1n have "d = 1" by blast  }
   2.500 +    moreover
   2.501 +    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
   2.502 +      from d n have "d \<noteq> 0"
   2.503 +        by (metis dvd_0_left_iff)
   2.504 +      hence dp: "d > 0" by simp
   2.505 +      from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
   2.506 +      from n dp e have ep:"e > 0" by simp
   2.507 +      have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
   2.508 +        by (auto simp add: e power2_eq_square mult_le_cancel_left)
   2.509 +      moreover
   2.510 +      {assume h: "d\<^sup>2 \<le> n"
   2.511 +        from H[rule_format, of d] h d have "d = 1" by blast}
   2.512 +      moreover
   2.513 +      {assume h: "e\<^sup>2 \<le> n"
   2.514 +        from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute)
   2.515 +        with H[rule_format, of e] h have "e=1" by simp
   2.516 +        with e have "d = n" by simp}
   2.517 +      ultimately have "d=1 \<or> d=n"  by blast}
   2.518 +    ultimately have ?thesis unfolding prime_def using np n(2) by blast}
   2.519 +  ultimately show ?thesis by auto
   2.520 +qed
   2.521 +
   2.522 +lemma prime_prime_factor_sqrt:
   2.523 +  "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)"
   2.524 +  (is "?lhs \<longleftrightarrow>?rhs")
   2.525 +proof-
   2.526 +  {assume "n=0 \<or> n=1" 
   2.527 +   hence ?thesis
   2.528 +     by (metis one_not_prime_nat zero_not_prime_nat)}
   2.529 +  moreover
   2.530 +  {assume n: "n\<noteq>0" "n\<noteq>1"
   2.531 +    {assume H: ?lhs
   2.532 +      from H[unfolded prime_divisor_sqrt] n
   2.533 +      have ?rhs
   2.534 +        apply clarsimp
   2.535 +        apply (erule_tac x="p" in allE)
   2.536 +        apply simp
   2.537 +        done
   2.538 +    }
   2.539 +    moreover
   2.540 +    {assume H: ?rhs
   2.541 +      {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
   2.542 +        then obtain p where p: "prime p" "p dvd d"
   2.543 +          by (metis prime_factor_nat) 
   2.544 +        from n have np: "n > 0" by arith
   2.545 +        from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
   2.546 +        hence dp: "d > 0" by arith
   2.547 +        from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
   2.548 +        have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
   2.549 +        with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
   2.550 +      with n prime_divisor_sqrt  have ?lhs by auto}
   2.551 +    ultimately have ?thesis by blast }
   2.552 +  ultimately show ?thesis by (cases "n=0 \<or> n=1", auto)
   2.553 +qed
   2.554 +
   2.555 +
   2.556 +subsection{*Pocklington theorem*}
   2.557 +
   2.558 +lemma pocklington_lemma:
   2.559 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
   2.560 +  and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   2.561 +  and pp: "prime p" and pn: "p dvd n"
   2.562 +  shows "[p = 1] (mod q)"
   2.563 +proof -
   2.564 +  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by auto
   2.565 +  obtain k where k: "a ^ (q * r) - 1 = n*k"
   2.566 +    by (metis an cong_to_1_nat dvd_def nqr)
   2.567 +  from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
   2.568 +  {assume a0: "a = 0"
   2.569 +    hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
   2.570 +    with n an mod_less[of 1 n]  have False by (simp add: power_0_left cong_nat_def)}
   2.571 +  hence a0: "a\<noteq>0" ..
   2.572 +  from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
   2.573 +  hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
   2.574 +  with k l have "a ^ (q * r) = p*l*k + 1" by simp
   2.575 +  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
   2.576 +  hence odq: "ord p (a^r) dvd q"
   2.577 +    unfolding ord_divides[symmetric] power_mult[symmetric]
   2.578 +    by (metis an cong_dvd_modulus_nat mult_commute nqr pn) 
   2.579 +  from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
   2.580 +  {assume d1: "d \<noteq> 1"
   2.581 +    obtain P where P: "prime P" "P dvd d"
   2.582 +      by (metis d1 prime_factor_nat) 
   2.583 +    from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp
   2.584 +    from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
   2.585 +    from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
   2.586 +    have P0: "P \<noteq> 0" using P(1)
   2.587 +      by (metis zero_not_prime_nat) 
   2.588 +    from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
   2.589 +    from d s t P0  have s': "ord p (a^r) * t = s"
   2.590 +      by (metis mult_commute mult_cancel1 nat_mult_assoc) 
   2.591 +    have "ord p (a^r) * t*r = r * ord p (a^r) * t"
   2.592 +      by (metis mult_assoc mult_commute)
   2.593 +    hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
   2.594 +      by (simp only: power_mult)
   2.595 +    have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)"
   2.596 +      by (metis cong_exp_nat ord)
   2.597 +    then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
   2.598 +      by simp
   2.599 +    have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
   2.600 +      by (metis cong_to_1_nat exps th)
   2.601 +    from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
   2.602 +    with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
   2.603 +    with p01 pn pd0 coprime_common_divisor_nat have False 
   2.604 +      by auto}
   2.605 +  hence d1: "d = 1" by blast
   2.606 +  hence o: "ord p (a^r) = q" using d by simp
   2.607 +  from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
   2.608 +  {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
   2.609 +    from pp[unfolded prime_def] d have dp: "d = p" by blast
   2.610 +    from n have "n \<noteq> 0" by simp
   2.611 +    then have False using d
   2.612 +      by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat 
   2.613 +           gcd_lcm_complete_lattice_nat.top_greatest pn)} 
   2.614 +  hence cpa: "coprime p a" by auto
   2.615 +  have arp: "coprime (a^r) p"
   2.616 +    by (metis coprime_exp_nat cpa gcd_nat.commute) 
   2.617 +  from euler_theorem_nat[OF arp, simplified ord_divides] o phip
   2.618 +  have "q dvd (p - 1)" by simp
   2.619 +  then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast
   2.620 +  have p0:"p \<noteq> 0"
   2.621 +    by (metis p01(1)) 
   2.622 +  from p0 d have "p + q * 0 = 1 + q * d" by simp
   2.623 +  then show ?thesis
   2.624 +    by (metis cong_iff_lin_nat mult_commute)
   2.625 +qed
   2.626 +
   2.627 +theorem pocklington:
   2.628 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   2.629 +  and an: "[a^ (n - 1) = 1] (mod n)"
   2.630 +  and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   2.631 +  shows "prime n"
   2.632 +unfolding prime_prime_factor_sqrt[of n]
   2.633 +proof-
   2.634 +  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)"
   2.635 +  from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
   2.636 +  {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
   2.637 +    from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
   2.638 +    hence pq: "p \<le> q"
   2.639 +      by (metis le0 power_le_imp_le_base) 
   2.640 +    from pocklington_lemma[OF n nqr an aq p(1,2)] 
   2.641 +    have th: "q dvd p - 1"
   2.642 +      by (metis cong_to_1_nat) 
   2.643 +    have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
   2.644 +    with pq p have False
   2.645 +      by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq
   2.646 +            prime_gt_0_nat th) }
   2.647 +  with n01 show ?ths by blast
   2.648 +qed
   2.649 +
   2.650 +(* Variant for application, to separate the exponentiation.                  *)
   2.651 +lemma pocklington_alt:
   2.652 +  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   2.653 +  and an: "[a^ (n - 1) = 1] (mod n)"
   2.654 +  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)"
   2.655 +  shows "prime n"
   2.656 +proof-
   2.657 +  {fix p assume p: "prime p" "p dvd q"
   2.658 +    from aq[rule_format] p obtain b where
   2.659 +      b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast
   2.660 +    {assume a0: "a=0"
   2.661 +      from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto
   2.662 +      hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])}
   2.663 +    hence a0: "a\<noteq> 0" ..
   2.664 +    hence a1: "a \<ge> 1" by arith
   2.665 +    from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
   2.666 +    {assume b0: "b = 0"
   2.667 +      from p(2) nqr have "(n - 1) mod p = 0"
   2.668 +        by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
   2.669 +      with mod_div_equality[of "n - 1" p]
   2.670 +      have "(n - 1) div p * p= n - 1" by auto
   2.671 +      hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
   2.672 +        by (simp only: power_mult[symmetric])
   2.673 +      have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
   2.674 +      then have pS: "Suc (p - 1) = p" by arith
   2.675 +      from b have d: "n dvd a^((n - 1) div p)" unfolding b0
   2.676 +        by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left 
   2.677 +                   gcd_lcm_complete_lattice_nat.inf_top_left) 
   2.678 +      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
   2.679 +      have False
   2.680 +        by simp}
   2.681 +    then have b0: "b \<noteq> 0" ..
   2.682 +    hence b1: "b \<ge> 1" by arith thm Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1]]
   2.683 +    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] ath b1 b(2) nqr
   2.684 +    have "coprime (a ^ ((n - 1) div p) - 1) n"
   2.685 +      by simp}
   2.686 +  hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
   2.687 +    by blast
   2.688 +  from pocklington[OF n nqr sqr an th] show ?thesis .
   2.689 +qed
   2.690 +
   2.691 +
   2.692 +subsection{*Prime factorizations*}
   2.693 +
   2.694 +text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
   2.695 +
   2.696 +definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
   2.697 +
   2.698 +lemma primefact: assumes n: "n \<noteq> 0"
   2.699 +  shows "\<exists>ps. primefact ps n"
   2.700 +using n
   2.701 +proof(induct n rule: nat_less_induct)
   2.702 +  fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
   2.703 +  let ?ths = "\<exists>ps. primefact ps n"
   2.704 +  {assume "n = 1"
   2.705 +    hence "primefact [] n" by (simp add: primefact_def)
   2.706 +    hence ?ths by blast }
   2.707 +  moreover
   2.708 +  {assume n1: "n \<noteq> 1"
   2.709 +    with n have n2: "n \<ge> 2" by arith
   2.710 +    obtain p where p: "prime p" "p dvd n"
   2.711 +      by (metis n1 prime_factor_nat) 
   2.712 +    from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
   2.713 +    from n m have m0: "m > 0" "m\<noteq>0" by auto
   2.714 +    have "1 < p"
   2.715 +      by (metis p(1) prime_nat_def)
   2.716 +    with m0 m have mn: "m < n" by auto
   2.717 +    from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
   2.718 +    from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
   2.719 +    hence ?ths by blast}
   2.720 +  ultimately show ?ths by blast
   2.721 +qed
   2.722 +
   2.723 +lemma primefact_contains:
   2.724 +  assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
   2.725 +  shows "p \<in> set ps"
   2.726 +  using pf p pn
   2.727 +proof(induct ps arbitrary: p n)
   2.728 +  case Nil thus ?case by (auto simp add: primefact_def)
   2.729 +next
   2.730 +  case (Cons q qs p n)
   2.731 +  from Cons.prems[unfolded primefact_def]
   2.732 +  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
   2.733 +  {assume "p dvd q"
   2.734 +    with p(1) q(1) have "p = q" unfolding prime_def by auto
   2.735 +    hence ?case by simp}
   2.736 +  moreover
   2.737 +  { assume h: "p dvd foldr op * qs 1"
   2.738 +    from q(3) have pqs: "primefact qs (foldr op * qs 1)"
   2.739 +      by (simp add: primefact_def)
   2.740 +    from Cons.hyps[OF pqs p(1) h] have ?case by simp}
   2.741 +  ultimately show ?case
   2.742 +    by (metis p prime_dvd_mult_eq_nat) 
   2.743 +qed
   2.744 +
   2.745 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
   2.746 +  by (auto simp add: primefact_def list_all_iff)
   2.747 +
   2.748 +(* Variant of Lucas theorem.                                                 *)
   2.749 +
   2.750 +lemma lucas_primefact:
   2.751 +  assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
   2.752 +  and psn: "foldr op * ps 1 = n - 1"
   2.753 +  and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
   2.754 +  shows "prime n"
   2.755 +proof-
   2.756 +  {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)"
   2.757 +    from psn psp have psn1: "primefact ps (n - 1)"
   2.758 +      by (auto simp add: list_all_iff primefact_variant)
   2.759 +    from p(3) primefact_contains[OF psn1 p(1,2)] psp
   2.760 +    have False by (induct ps, auto)}
   2.761 +  with lucas[OF n an] show ?thesis by blast
   2.762 +qed
   2.763 +
   2.764 +(* Variant of Pocklington theorem.                                           *)
   2.765 +
   2.766 +lemma pocklington_primefact:
   2.767 +  assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
   2.768 +  and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
   2.769 +  and bqn: "(b^q) mod n = 1"
   2.770 +  and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
   2.771 +  shows "prime n"
   2.772 +proof-
   2.773 +  from bqn psp qrn
   2.774 +  have bqn: "a ^ (n - 1) mod n = 1"
   2.775 +    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
   2.776 +    by (simp_all add: power_mult[symmetric] algebra_simps)
   2.777 +  from n  have n0: "n > 0" by arith
   2.778 +  from mod_div_equality[of "a^(n - 1)" n]
   2.779 +    mod_less_divisor[OF n0, of "a^(n - 1)"]
   2.780 +  have an1: "[a ^ (n - 1) = 1] (mod n)"
   2.781 +    by (metis bqn cong_nat_def mod_mod_trivial)
   2.782 +  {fix p assume p: "prime p" "p dvd q"
   2.783 +    from psp psq have pfpsq: "primefact ps q"
   2.784 +      by (auto simp add: primefact_variant list_all_iff)
   2.785 +    from psp primefact_contains[OF pfpsq p]
   2.786 +    have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
   2.787 +      by (simp add: list_all_iff)
   2.788 +    from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
   2.789 +      by auto
   2.790 +    from div_mult1_eq[of r q p] p(2)
   2.791 +    have eq1: "r* (q div p) = (n - 1) div p"
   2.792 +      unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult_commute)
   2.793 +    have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith
   2.794 +    {assume "a ^ ((n - 1) div p) mod n = 0"
   2.795 +      then obtain s where s: "a ^ ((n - 1) div p) = n*s"
   2.796 +        unfolding mod_eq_0_iff by blast
   2.797 +      hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
   2.798 +      from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
   2.799 +      from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
   2.800 +      have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
   2.801 +      with eq0 have "a^ (n - 1) = (n*s)^p"
   2.802 +        by (simp add: power_mult[symmetric])
   2.803 +      hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
   2.804 +      also have "\<dots> = 0" by (simp add: mult_assoc)
   2.805 +      finally have False by simp }
   2.806 +      then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
   2.807 +    have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
   2.808 +      unfolding cong_nat_def by simp
   2.809 +    from  th1   ath[OF mod_less_eq_dividend th11]
   2.810 +    have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
   2.811 +      by (metis cong_diff_nat cong_refl_nat)
   2.812 +    have "coprime (a ^ ((n - 1) div p) - 1) n"
   2.813 +      by (metis cong_imp_coprime_nat eq1 p' th) }
   2.814 +  with pocklington[OF n qrn[symmetric] nq2 an1]
   2.815 +  show ?thesis by blast
   2.816 +qed
   2.817 +
   2.818 +end
     3.1 --- a/src/HOL/ROOT	Tue Feb 04 21:01:35 2014 +0100
     3.2 +++ b/src/HOL/ROOT	Tue Feb 04 21:28:38 2014 +0000
     3.3 @@ -171,8 +171,19 @@
     3.4    theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
     3.5  
     3.6  session "HOL-Number_Theory" in Number_Theory = HOL +
     3.7 -  options [document = false]
     3.8 -  theories Number_Theory
     3.9 +  description {*
    3.10 +    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    3.11 +    Theorem, Wilson's Theorem, Quadratic Reciprocity.
    3.12 +  *}
    3.13 +  options [document_graph]
    3.14 +  theories [document = false]
    3.15 +    "~~/src/HOL/Library/FuncSet"
    3.16 +    "~~/src/HOL/Library/Multiset"
    3.17 +    "~~/src/HOL/Algebra/Ring"
    3.18 +    "~~/src/HOL/Algebra/FiniteProduct"
    3.19 +  theories
    3.20 +    Pocklington
    3.21 +    Number_Theory
    3.22  
    3.23  session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
    3.24    description {*