src/HOL/Number_Theory/Pocklington.thy
 author haftmann Wed Jul 08 14:01:41 2015 +0200 (2015-07-08) changeset 60688 01488b559910 parent 60526 fad653acf58f child 61762 d50b993b4fb9 permissions -rw-r--r--
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
 lp15@55321 ` 1` ```(* Title: HOL/Number_Theory/Pocklington.thy ``` lp15@55321 ` 2` ``` Author: Amine Chaieb ``` lp15@55321 ` 3` ```*) ``` lp15@55321 ` 4` wenzelm@60526 ` 5` ```section \Pocklington's Theorem for Primes\ ``` lp15@55321 ` 6` lp15@55321 ` 7` ```theory Pocklington ``` lp15@55321 ` 8` ```imports Residues ``` lp15@55321 ` 9` ```begin ``` lp15@55321 ` 10` wenzelm@60526 ` 11` ```subsection\Lemmas about previously defined terms\ ``` lp15@55321 ` 12` lp15@55321 ` 13` ```lemma prime: ``` lp15@55321 ` 14` ``` "prime p \ p \ 0 \ p\1 \ (\m. 0 < m \ m < p \ coprime p m)" ``` lp15@55321 ` 15` ``` (is "?lhs \ ?rhs") ``` lp15@55321 ` 16` ```proof- ``` lp15@55321 ` 17` ``` {assume "p=0 \ p=1" hence ?thesis ``` lp15@55321 ` 18` ``` by (metis one_not_prime_nat zero_not_prime_nat)} ``` lp15@55321 ` 19` ``` moreover ``` lp15@55321 ` 20` ``` {assume p0: "p\0" "p\1" ``` lp15@55321 ` 21` ``` {assume H: "?lhs" ``` lp15@55321 ` 22` ``` {fix m assume m: "m > 0" "m < p" ``` lp15@55321 ` 23` ``` {assume "m=1" hence "coprime p m" by simp} ``` lp15@55321 ` 24` ``` moreover ``` lp15@55321 ` 25` ``` {assume "p dvd m" hence "p \ m" using dvd_imp_le m by blast with m(2) ``` lp15@55321 ` 26` ``` have "coprime p m" by simp} ``` lp15@55321 ` 27` ``` ultimately have "coprime p m" ``` lp15@55321 ` 28` ``` by (metis H prime_imp_coprime_nat)} ``` lp15@55321 ` 29` ``` hence ?rhs using p0 by auto} ``` lp15@55321 ` 30` ``` moreover ``` lp15@55321 ` 31` ``` { assume H: "\m. 0 < m \ m < p \ coprime p m" ``` lp15@55321 ` 32` ``` obtain q where q: "prime q" "q dvd p" ``` lp15@55321 ` 33` ``` by (metis p0(2) prime_factor_nat) ``` lp15@55321 ` 34` ``` have q0: "q > 0" ``` lp15@55321 ` 35` ``` by (metis prime_gt_0_nat q(1)) ``` lp15@55321 ` 36` ``` from dvd_imp_le[OF q(2)] p0 have qp: "q \ p" by arith ``` lp15@55321 ` 37` ``` {assume "q = p" hence ?lhs using q(1) by blast} ``` lp15@55321 ` 38` ``` moreover ``` lp15@55321 ` 39` ``` {assume "q\p" with qp have qplt: "q < p" by arith ``` lp15@55337 ` 40` ``` from H qplt q0 have "coprime p q" by arith ``` lp15@55337 ` 41` ``` hence ?lhs using q ``` lp15@55337 ` 42` ``` by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)} ``` lp15@55321 ` 43` ``` ultimately have ?lhs by blast} ``` lp15@55321 ` 44` ``` ultimately have ?thesis by blast} ``` lp15@55321 ` 45` ``` ultimately show ?thesis by (cases"p=0 \ p=1", auto) ``` lp15@55321 ` 46` ```qed ``` lp15@55321 ` 47` lp15@55321 ` 48` ```lemma finite_number_segment: "card { m. 0 < m \ m < n } = n - 1" ``` lp15@55321 ` 49` ```proof- ``` lp15@55321 ` 50` ``` have "{ m. 0 < m \ m < n } = {1..Some basic theorems about solving congruences\ ``` lp15@55321 ` 56` lp15@55321 ` 57` ```lemma cong_solve: ``` lp15@55321 ` 58` ``` fixes n::nat assumes an: "coprime a n" shows "\x. [a * x = b] (mod n)" ``` lp15@55321 ` 59` ```proof- ``` lp15@55321 ` 60` ``` {assume "a=0" hence ?thesis using an by (simp add: cong_nat_def)} ``` lp15@55321 ` 61` ``` moreover ``` lp15@55321 ` 62` ``` {assume az: "a\0" ``` lp15@55321 ` 63` ``` from bezout_add_strong_nat[OF az, of n] ``` lp15@55321 ` 64` ``` obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast ``` lp15@55321 ` 65` ``` from dxy(1,2) have d1: "d = 1" ``` lp15@55321 ` 66` ``` by (metis assms coprime_nat) ``` lp15@55321 ` 67` ``` hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp ``` lp15@55337 ` 68` ``` hence "a*(x*b) = n*(y*b) + b" ``` lp15@55321 ` 69` ``` by (auto simp add: algebra_simps) ``` lp15@55321 ` 70` ``` hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp ``` lp15@55321 ` 71` ``` hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq) ``` lp15@55321 ` 72` ``` hence "[a*(x*b) = b] (mod n)" unfolding cong_nat_def . ``` lp15@55321 ` 73` ``` hence ?thesis by blast} ``` lp15@55321 ` 74` ```ultimately show ?thesis by blast ``` lp15@55321 ` 75` ```qed ``` lp15@55321 ` 76` lp15@55321 ` 77` ```lemma cong_solve_unique: ``` lp15@55321 ` 78` ``` fixes n::nat assumes an: "coprime a n" and nz: "n \ 0" ``` lp15@55321 ` 79` ``` shows "\!x. x < n \ [a * x = b] (mod n)" ``` lp15@55321 ` 80` ```proof- ``` lp15@55321 ` 81` ``` let ?P = "\x. x < n \ [a * x = b] (mod n)" ``` lp15@55321 ` 82` ``` from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast ``` lp15@55321 ` 83` ``` let ?x = "x mod n" ``` lp15@55321 ` 84` ``` from x have th: "[a * ?x = b] (mod n)" ``` lp15@55321 ` 85` ``` by (simp add: cong_nat_def mod_mult_right_eq[of a x n]) ``` lp15@55321 ` 86` ``` from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp ``` lp15@55321 ` 87` ``` {fix y assume Py: "y < n" "[a * y = b] (mod n)" ``` lp15@55321 ` 88` ``` from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: cong_nat_def) ``` lp15@55321 ` 89` ``` hence "[y = ?x] (mod n)" ``` lp15@55321 ` 90` ``` by (metis an cong_mult_lcancel_nat) ``` lp15@55321 ` 91` ``` with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz ``` lp15@55321 ` 92` ``` have "y = ?x" by (simp add: cong_nat_def)} ``` lp15@55321 ` 93` ``` with Px show ?thesis by blast ``` lp15@55321 ` 94` ```qed ``` lp15@55321 ` 95` lp15@55321 ` 96` ```lemma cong_solve_unique_nontrivial: ``` lp15@55321 ` 97` ``` assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p" ``` lp15@55321 ` 98` ``` shows "\!y. 0 < y \ y < p \ [x * y = a] (mod p)" ``` lp15@55321 ` 99` ```proof- ``` lp15@55321 ` 100` ``` from pa have ap: "coprime a p" ``` haftmann@60688 ` 101` ``` by (metis gcd.commute) ``` lp15@55321 ` 102` ``` have px:"coprime x p" ``` haftmann@60688 ` 103` ``` by (metis gcd.commute p prime x0 xp) ``` lp15@55321 ` 104` ``` obtain y where y: "y < p" "[x * y = a] (mod p)" "\z. z < p \ [x * z = a] (mod p) \ z = y" ``` lp15@55321 ` 105` ``` by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px) ``` lp15@55321 ` 106` ``` {assume y0: "y = 0" ``` lp15@55321 ` 107` ``` with y(2) have th: "p dvd a" ``` lp15@55321 ` 108` ``` by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right) ``` lp15@55321 ` 109` ``` have False ``` lp15@55321 ` 110` ``` by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)} ``` lp15@55321 ` 111` ``` with y show ?thesis unfolding Ex1_def using neq0_conv by blast ``` lp15@55321 ` 112` ```qed ``` lp15@55321 ` 113` lp15@55321 ` 114` ```lemma cong_unique_inverse_prime: ``` lp15@55321 ` 115` ``` assumes p: "prime p" and x0: "0 < x" and xp: "x < p" ``` lp15@55321 ` 116` ``` shows "\!y. 0 < y \ y < p \ [x * y = 1] (mod p)" ``` haftmann@60688 ` 117` ```by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd.commute assms) ``` lp15@55321 ` 118` lp15@55321 ` 119` ```lemma chinese_remainder_coprime_unique: ``` lp15@55321 ` 120` ``` fixes a::nat ``` lp15@55321 ` 121` ``` assumes ab: "coprime a b" and az: "a \ 0" and bz: "b \ 0" ``` lp15@55321 ` 122` ``` and ma: "coprime m a" and nb: "coprime n b" ``` lp15@55321 ` 123` ``` shows "\!x. coprime x (a * b) \ x < a * b \ [x = m] (mod a) \ [x = n] (mod b)" ``` lp15@55321 ` 124` ```proof- ``` lp15@55321 ` 125` ``` let ?P = "\x. x < a * b \ [x = m] (mod a) \ [x = n] (mod b)" ``` lp15@55321 ` 126` ``` from binary_chinese_remainder_unique_nat[OF ab az bz] ``` lp15@55321 ` 127` ``` obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" ``` lp15@55321 ` 128` ``` "\y. ?P y \ y = x" by blast ``` lp15@55321 ` 129` ``` from ma nb x ``` lp15@55321 ` 130` ``` have "coprime x a" "coprime x b" ``` lp15@55321 ` 131` ``` by (metis cong_gcd_eq_nat)+ ``` lp15@55321 ` 132` ``` then have "coprime x (a*b)" ``` lp15@55321 ` 133` ``` by (metis coprime_mul_eq_nat) ``` lp15@55321 ` 134` ``` with x show ?thesis by blast ``` lp15@55321 ` 135` ```qed ``` lp15@55321 ` 136` lp15@55321 ` 137` wenzelm@60526 ` 138` ```subsection\Lucas's theorem\ ``` lp15@55321 ` 139` lp15@55321 ` 140` ```lemma phi_limit_strong: "phi(n) \ n - 1" ``` lp15@55321 ` 141` ```proof - ``` lp15@55321 ` 142` ``` have "phi n = card {x. 0 < x \ x < int n \ coprime x (int n)}" ``` lp15@55321 ` 143` ``` by (simp add: phi_def) ``` lp15@55321 ` 144` ``` also have "... \ card {0 <..< int n}" ``` lp15@55321 ` 145` ``` by (rule card_mono) auto ``` lp15@55321 ` 146` ``` also have "... = card {0 <..< n}" ``` lp15@55321 ` 147` ``` by (simp add: transfer_nat_int_set_functions) ``` lp15@55321 ` 148` ``` also have "... \ n - 1" ``` lp15@55321 ` 149` ``` by (metis card_greaterThanLessThan le_refl One_nat_def) ``` lp15@55321 ` 150` ``` finally show ?thesis . ``` lp15@55321 ` 151` ```qed ``` lp15@55321 ` 152` lp15@55321 ` 153` ```lemma phi_lowerbound_1: assumes n: "n \ 2" ``` lp15@55321 ` 154` ``` shows "phi n \ 1" ``` lp15@55321 ` 155` ```proof - ``` lp15@55321 ` 156` ``` have "1 \ card {0::int <.. 1}" ``` lp15@55321 ` 157` ``` by auto ``` lp15@55321 ` 158` ``` also have "... \ card {x. 0 < x \ x < n \ coprime x n}" ``` lp15@55321 ` 159` ``` apply (rule card_mono) using assms ``` haftmann@60688 ` 160` ``` by auto (metis dual_order.antisym gcd_1_int gcd.commute int_one_le_iff_zero_less) ``` lp15@55321 ` 161` ``` also have "... = phi n" ``` lp15@55321 ` 162` ``` by (simp add: phi_def) ``` lp15@55321 ` 163` ``` finally show ?thesis . ``` lp15@55321 ` 164` ```qed ``` lp15@55321 ` 165` lp15@55321 ` 166` ```lemma phi_lowerbound_1_nat: assumes n: "n \ 2" ``` lp15@55321 ` 167` ``` shows "phi(int n) \ 1" ``` lp15@55321 ` 168` ```by (metis n nat_le_iff nat_numeral phi_lowerbound_1) ``` lp15@55321 ` 169` lp15@55321 ` 170` ```lemma euler_theorem_nat: ``` lp15@55321 ` 171` ``` fixes m::nat ``` lp15@55321 ` 172` ``` assumes "coprime a m" ``` lp15@55321 ` 173` ``` shows "[a ^ phi m = 1] (mod m)" ``` lp15@55321 ` 174` ```by (metis assms le0 euler_theorem [transferred]) ``` lp15@55321 ` 175` lp15@55321 ` 176` ```lemma lucas_coprime_lemma: ``` lp15@55321 ` 177` ``` fixes n::nat ``` lp15@55321 ` 178` ``` assumes m: "m\0" and am: "[a^m = 1] (mod n)" ``` lp15@55321 ` 179` ``` shows "coprime a n" ``` lp15@55321 ` 180` ```proof- ``` lp15@55321 ` 181` ``` {assume "n=1" hence ?thesis by simp} ``` lp15@55321 ` 182` ``` moreover ``` lp15@55321 ` 183` ``` {assume "n = 0" hence ?thesis using am m ``` lp15@55321 ` 184` ``` by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)} ``` lp15@55321 ` 185` ``` moreover ``` lp15@55321 ` 186` ``` {assume n: "n\0" "n\1" ``` lp15@55321 ` 187` ``` from m obtain m' where m': "m = Suc m'" by (cases m, blast+) ``` lp15@55321 ` 188` ``` {fix d ``` lp15@55321 ` 189` ``` assume d: "d dvd a" "d dvd n" ``` lp15@55321 ` 190` ``` from n have n1: "1 < n" by arith ``` lp15@55321 ` 191` ``` from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding cong_nat_def by simp ``` lp15@55321 ` 192` ``` from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m') ``` lp15@55321 ` 193` ``` from dvd_mod_iff[OF d(2), of "a^m"] dam am1 ``` lp15@55321 ` 194` ``` have "d = 1" by simp } ``` lp15@55321 ` 195` ``` hence ?thesis by auto ``` lp15@55321 ` 196` ``` } ``` lp15@55321 ` 197` ``` ultimately show ?thesis by blast ``` lp15@55321 ` 198` ```qed ``` lp15@55321 ` 199` lp15@55321 ` 200` ```lemma lucas_weak: ``` lp15@55321 ` 201` ``` fixes n::nat ``` lp15@55321 ` 202` ``` assumes n: "n \ 2" and an:"[a^(n - 1) = 1] (mod n)" ``` lp15@55321 ` 203` ``` and nm: "\m. 0 m < n - 1 \ \ [a^m = 1] (mod n)" ``` lp15@55321 ` 204` ``` shows "prime n" ``` lp15@55321 ` 205` ```proof- ``` lp15@55321 ` 206` ``` from n have n1: "n \ 1" "n\0" "n - 1 \ 0" "n - 1 > 0" "n - 1 < n" by arith+ ``` lp15@55321 ` 207` ``` from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" . ``` lp15@55321 ` 208` ``` from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)" ``` lp15@55321 ` 209` ``` by auto ``` lp15@55321 ` 210` ``` {assume "phi n \ n - 1" ``` lp15@55321 ` 211` ``` with phi_limit_strong phi_lowerbound_1_nat [OF n] ``` lp15@55321 ` 212` ``` have c:"phi n > 0 \ phi n < n - 1" ``` lp15@55321 ` 213` ``` by (metis gr0I leD less_linear not_one_le_zero) ``` lp15@55321 ` 214` ``` from nm[rule_format, OF c] afn have False ..} ``` lp15@55321 ` 215` ``` hence "phi n = n - 1" by blast ``` lp15@55321 ` 216` ``` with prime_phi phi_prime n1(1,2) show ?thesis ``` lp15@55321 ` 217` ``` by auto ``` lp15@55321 ` 218` ```qed ``` lp15@55321 ` 219` lp15@55321 ` 220` ```lemma nat_exists_least_iff: "(\(n::nat). P n) \ (\n. P n \ (\m < n. \ P m))" ``` lp15@55337 ` 221` ``` by (metis ex_least_nat_le not_less0) ``` lp15@55321 ` 222` lp15@55321 ` 223` ```lemma nat_exists_least_iff': "(\(n::nat). P n) \ (P (Least P) \ (\m < (Least P). \ P m))" ``` lp15@55321 ` 224` ``` (is "?lhs \ ?rhs") ``` lp15@55321 ` 225` ```proof- ``` lp15@55321 ` 226` ``` {assume ?rhs hence ?lhs by blast} ``` lp15@55321 ` 227` ``` moreover ``` lp15@55321 ` 228` ``` { assume H: ?lhs then obtain n where n: "P n" by blast ``` lp15@55321 ` 229` ``` let ?x = "Least P" ``` lp15@55321 ` 230` ``` {fix m assume m: "m < ?x" ``` lp15@55321 ` 231` ``` from not_less_Least[OF m] have "\ P m" .} ``` lp15@55321 ` 232` ``` with LeastI_ex[OF H] have ?rhs by blast} ``` lp15@55321 ` 233` ``` ultimately show ?thesis by blast ``` lp15@55321 ` 234` ```qed ``` lp15@55321 ` 235` lp15@55321 ` 236` ```theorem lucas: ``` lp15@55321 ` 237` ``` assumes n2: "n \ 2" and an1: "[a^(n - 1) = 1] (mod n)" ``` lp15@55321 ` 238` ``` and pn: "\p. prime p \ p dvd n - 1 \ [a^((n - 1) div p) \ 1] (mod n)" ``` lp15@55321 ` 239` ``` shows "prime n" ``` lp15@55321 ` 240` ```proof- ``` lp15@55321 ` 241` ``` from n2 have n01: "n\0" "n\1" "n - 1 \ 0" by arith+ ``` lp15@55321 ` 242` ``` from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp ``` lp15@55321 ` 243` ``` from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1 ``` lp15@55321 ` 244` ``` have an: "coprime a n" "coprime (a^(n - 1)) n" ``` haftmann@60688 ` 245` ``` by (auto simp add: coprime_exp_nat gcd.commute) ``` lp15@55321 ` 246` ``` {assume H0: "\m. 0 < m \ m < n - 1 \ [a ^ m = 1] (mod n)" (is "EX m. ?P m") ``` lp15@55321 ` 247` ``` from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where ``` lp15@55321 ` 248` ``` m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\k ?P k" by blast ``` lp15@55321 ` 249` ``` {assume nm1: "(n - 1) mod m > 0" ``` lp15@55321 ` 250` ``` from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast ``` lp15@55321 ` 251` ``` let ?y = "a^ ((n - 1) div m * m)" ``` lp15@55321 ` 252` ``` note mdeq = mod_div_equality[of "(n - 1)" m] ``` lp15@55321 ` 253` ``` have yn: "coprime ?y n" ``` haftmann@60688 ` 254` ``` by (metis an(1) coprime_exp_nat gcd.commute) ``` lp15@55321 ` 255` ``` have "?y mod n = (a^m)^((n - 1) div m) mod n" ``` lp15@55321 ` 256` ``` by (simp add: algebra_simps power_mult) ``` lp15@55321 ` 257` ``` also have "\ = (a^m mod n)^((n - 1) div m) mod n" ``` lp15@55321 ` 258` ``` using power_mod[of "a^m" n "(n - 1) div m"] by simp ``` lp15@55321 ` 259` ``` also have "\ = 1" using m(3)[unfolded cong_nat_def onen] onen ``` lp15@55321 ` 260` ``` by (metis power_one) ``` lp15@55321 ` 261` ``` finally have th3: "?y mod n = 1" . ``` lp15@55321 ` 262` ``` have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" ``` lp15@55321 ` 263` ``` using an1[unfolded cong_nat_def onen] onen ``` lp15@55321 ` 264` ``` mod_div_equality[of "(n - 1)" m, symmetric] ``` lp15@55321 ` 265` ``` by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def) ``` lp15@55321 ` 266` ``` have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" ``` haftmann@57512 ` 267` ``` by (metis cong_mult_rcancel_nat mult.commute th2 yn) ``` lp15@55321 ` 268` ``` from m(4)[rule_format, OF th0] nm1 ``` lp15@55321 ` 269` ``` less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1 ``` lp15@55321 ` 270` ``` have False by blast } ``` lp15@55321 ` 271` ``` hence "(n - 1) mod m = 0" by auto ``` lp15@55321 ` 272` ``` then have mn: "m dvd n - 1" by presburger ``` lp15@55321 ` 273` ``` then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast ``` lp15@55321 ` 274` ``` from n01 r m(2) have r01: "r\0" "r\1" by - (rule ccontr, simp)+ ``` lp15@55321 ` 275` ``` obtain p where p: "prime p" "p dvd r" ``` lp15@55321 ` 276` ``` by (metis prime_factor_nat r01(2)) ``` lp15@55321 ` 277` ``` hence th: "prime p \ p dvd n - 1" unfolding r by (auto intro: dvd_mult) ``` lp15@55321 ` 278` ``` have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r ``` lp15@55321 ` 279` ``` by (simp add: power_mult) ``` lp15@55337 ` 280` ``` also have "\ = (a^(m*(r div p))) mod n" ``` lp15@55337 ` 281` ``` using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] ``` lp15@55337 ` 282` ``` by simp ``` lp15@55321 ` 283` ``` also have "\ = ((a^m)^(r div p)) mod n" by (simp add: power_mult) ``` lp15@55337 ` 284` ``` also have "\ = ((a^m mod n)^(r div p)) mod n" using power_mod .. ``` lp15@55337 ` 285` ``` also have "\ = 1" using m(3) onen by (simp add: cong_nat_def) ``` lp15@55321 ` 286` ``` finally have "[(a ^ ((n - 1) div p))= 1] (mod n)" ``` lp15@55321 ` 287` ``` using onen by (simp add: cong_nat_def) ``` lp15@55337 ` 288` ``` with pn th have False by blast} ``` lp15@55321 ` 289` ``` hence th: "\m. 0 < m \ m < n - 1 \ \ [a ^ m = 1] (mod n)" by blast ``` lp15@55321 ` 290` ``` from lucas_weak[OF n2 an1 th] show ?thesis . ``` lp15@55321 ` 291` ```qed ``` lp15@55321 ` 292` lp15@55321 ` 293` wenzelm@60526 ` 294` ```subsection\Definition of the order of a number mod n (0 in non-coprime case)\ ``` lp15@55321 ` 295` lp15@55321 ` 296` ```definition "ord n a = (if coprime n a then Least (\d. d > 0 \ [a ^d = 1] (mod n)) else 0)" ``` lp15@55321 ` 297` lp15@55321 ` 298` ```(* This has the expected properties. *) ``` lp15@55321 ` 299` lp15@55321 ` 300` ```lemma coprime_ord: ``` lp15@55321 ` 301` ``` fixes n::nat ``` lp15@55321 ` 302` ``` assumes "coprime n a" ``` lp15@55321 ` 303` ``` shows "ord n a > 0 \ [a ^(ord n a) = 1] (mod n) \ (\m. 0 < m \ m < ord n a \ [a^ m \ 1] (mod n))" ``` lp15@55321 ` 304` ```proof- ``` lp15@55321 ` 305` ``` let ?P = "\d. 0 < d \ [a ^ d = 1] (mod n)" ``` lp15@55321 ` 306` ``` from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast ``` lp15@55321 ` 307` ``` from assms have o: "ord n a = Least ?P" by (simp add: ord_def) ``` lp15@55321 ` 308` ``` {assume "n=0 \ n=1" with assms have "\m>0. ?P m" ``` lp15@55321 ` 309` ``` by auto} ``` lp15@55321 ` 310` ``` moreover ``` lp15@55321 ` 311` ``` {assume "n\0 \ n\1" hence n2:"n \ 2" by arith ``` lp15@55321 ` 312` ``` from assms have na': "coprime a n" ``` haftmann@60688 ` 313` ``` by (metis gcd.commute) ``` lp15@55321 ` 314` ``` from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na'] ``` lp15@55321 ` 315` ``` have ex: "\m>0. ?P m" by - (rule exI[where x="phi n"], auto) } ``` lp15@55321 ` 316` ``` ultimately have ex: "\m>0. ?P m" by blast ``` lp15@55321 ` 317` ``` from nat_exists_least_iff'[of ?P] ex assms show ?thesis ``` lp15@55321 ` 318` ``` unfolding o[symmetric] by auto ``` lp15@55321 ` 319` ```qed ``` lp15@55321 ` 320` lp15@55321 ` 321` ```(* With the special value 0 for non-coprime case, it's more convenient. *) ``` lp15@55321 ` 322` ```lemma ord_works: ``` lp15@55321 ` 323` ``` fixes n::nat ``` lp15@55321 ` 324` ``` shows "[a ^ (ord n a) = 1] (mod n) \ (\m. 0 < m \ m < ord n a \ ~[a^ m = 1] (mod n))" ``` lp15@55321 ` 325` ```apply (cases "coprime n a") ``` lp15@55321 ` 326` ```using coprime_ord[of n a] ``` lp15@55337 ` 327` ```by (auto simp add: ord_def cong_nat_def) ``` lp15@55321 ` 328` lp15@55321 ` 329` ```lemma ord: ``` lp15@55321 ` 330` ``` fixes n::nat ``` lp15@55321 ` 331` ``` shows "[a^(ord n a) = 1] (mod n)" using ord_works by blast ``` lp15@55321 ` 332` lp15@55321 ` 333` ```lemma ord_minimal: ``` lp15@55321 ` 334` ``` fixes n::nat ``` lp15@55321 ` 335` ``` shows "0 < m \ m < ord n a \ ~[a^m = 1] (mod n)" ``` lp15@55321 ` 336` ``` using ord_works by blast ``` lp15@55321 ` 337` lp15@55321 ` 338` ```lemma ord_eq_0: ``` lp15@55321 ` 339` ``` fixes n::nat ``` lp15@55321 ` 340` ``` shows "ord n a = 0 \ ~coprime n a" ``` lp15@55321 ` 341` ```by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def) ``` lp15@55321 ` 342` lp15@55321 ` 343` ```lemma divides_rexp: ``` lp15@55321 ` 344` ``` "x dvd y \ (x::nat) dvd (y^(Suc n))" ``` lp15@55321 ` 345` ``` by (simp add: dvd_mult2[of x y]) ``` lp15@55321 ` 346` lp15@55321 ` 347` ```lemma ord_divides: ``` lp15@55321 ` 348` ``` fixes n::nat ``` lp15@55321 ` 349` ``` shows "[a ^ d = 1] (mod n) \ ord n a dvd d" (is "?lhs \ ?rhs") ``` lp15@55321 ` 350` ```proof ``` lp15@55321 ` 351` ``` assume rh: ?rhs ``` lp15@55321 ` 352` ``` then obtain k where "d = ord n a * k" unfolding dvd_def by blast ``` lp15@55321 ` 353` ``` hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)" ``` lp15@55321 ` 354` ``` by (simp add : cong_nat_def power_mult power_mod) ``` lp15@55321 ` 355` ``` also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)" ``` lp15@55321 ` 356` ``` using ord[of a n, unfolded cong_nat_def] ``` lp15@55321 ` 357` ``` by (simp add: cong_nat_def power_mod) ``` lp15@55321 ` 358` ``` finally show ?lhs . ``` lp15@55321 ` 359` ```next ``` lp15@55321 ` 360` ``` assume lh: ?lhs ``` lp15@55321 ` 361` ``` { assume H: "\ coprime n a" ``` lp15@55321 ` 362` ``` hence o: "ord n a = 0" by (simp add: ord_def) ``` lp15@55321 ` 363` ``` {assume d: "d=0" with o H have ?rhs by (simp add: cong_nat_def)} ``` lp15@55321 ` 364` ``` moreover ``` lp15@55321 ` 365` ``` {assume d0: "d\0" then obtain d' where d': "d = Suc d'" by (cases d, auto) ``` lp15@55321 ` 366` ``` from H ``` lp15@55321 ` 367` ``` obtain p where p: "p dvd n" "p dvd a" "p \ 1" by auto ``` lp15@55321 ` 368` ``` from lh ``` lp15@55321 ` 369` ``` obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" ``` haftmann@60688 ` 370` ``` by (metis H d0 gcd.commute lucas_coprime_lemma) ``` lp15@55321 ` 371` ``` hence "a ^ d + n * q1 - n * q2 = 1" by simp ``` lp15@55337 ` 372` ``` with dvd_diff_nat [OF dvd_add [OF divides_rexp]] dvd_mult2 d' p ``` lp15@55337 ` 373` ``` have "p dvd 1" ``` lp15@55337 ` 374` ``` by metis ``` lp15@55321 ` 375` ``` with p(3) have False by simp ``` lp15@55321 ` 376` ``` hence ?rhs ..} ``` lp15@55321 ` 377` ``` ultimately have ?rhs by blast} ``` lp15@55321 ` 378` ``` moreover ``` lp15@55321 ` 379` ``` {assume H: "coprime n a" ``` lp15@55321 ` 380` ``` let ?o = "ord n a" ``` lp15@55321 ` 381` ``` let ?q = "d div ord n a" ``` lp15@55321 ` 382` ``` let ?r = "d mod ord n a" ``` lp15@55321 ` 383` ``` have eqo: "[(a^?o)^?q = 1] (mod n)" ``` lp15@55321 ` 384` ``` by (metis cong_exp_nat ord power_one) ``` lp15@55321 ` 385` ``` from H have onz: "?o \ 0" by (simp add: ord_eq_0) ``` lp15@55321 ` 386` ``` hence op: "?o > 0" by simp ``` lp15@55321 ` 387` ``` from mod_div_equality[of d "ord n a"] lh ``` haftmann@57512 ` 388` ``` have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute) ``` lp15@55321 ` 389` ``` hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" ``` lp15@55321 ` 390` ``` by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric]) ``` lp15@55321 ` 391` ``` hence th: "[a^?r = 1] (mod n)" ``` lp15@55321 ` 392` ``` using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n] ``` lp15@55321 ` 393` ``` apply (simp add: cong_nat_def del: One_nat_def) ``` lp15@55321 ` 394` ``` by (simp add: mod_mult_left_eq[symmetric]) ``` lp15@55321 ` 395` ``` {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)} ``` lp15@55321 ` 396` ``` moreover ``` lp15@55321 ` 397` ``` {assume r: "?r \ 0" ``` lp15@55321 ` 398` ``` with mod_less_divisor[OF op, of d] have r0o:"?r >0 \ ?r < ?o" by simp ``` lp15@55321 ` 399` ``` from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th ``` lp15@55321 ` 400` ``` have ?rhs by blast} ``` lp15@55321 ` 401` ``` ultimately have ?rhs by blast} ``` lp15@55321 ` 402` ``` ultimately show ?rhs by blast ``` lp15@55321 ` 403` ```qed ``` lp15@55321 ` 404` lp15@55321 ` 405` ```lemma order_divides_phi: ``` lp15@55321 ` 406` ``` fixes n::nat shows "coprime n a \ ord n a dvd phi n" ``` haftmann@60688 ` 407` ``` by (metis ord_divides euler_theorem_nat gcd.commute) ``` lp15@55321 ` 408` lp15@55321 ` 409` ```lemma order_divides_expdiff: ``` lp15@55321 ` 410` ``` fixes n::nat and a::nat assumes na: "coprime n a" ``` lp15@55321 ` 411` ``` shows "[a^d = a^e] (mod n) \ [d = e] (mod (ord n a))" ``` lp15@55321 ` 412` ```proof- ``` lp15@55321 ` 413` ``` {fix n::nat and a::nat and d::nat and e::nat ``` lp15@55321 ` 414` ``` assume na: "coprime n a" and ed: "(e::nat) \ d" ``` lp15@55321 ` 415` ``` hence "\c. d = e + c" by presburger ``` lp15@55321 ` 416` ``` then obtain c where c: "d = e + c" by presburger ``` lp15@55321 ` 417` ``` from na have an: "coprime a n" ``` haftmann@60688 ` 418` ``` by (metis gcd.commute) ``` lp15@55321 ` 419` ``` have aen: "coprime (a^e) n" ``` haftmann@60688 ` 420` ``` by (metis coprime_exp_nat gcd.commute na) ``` lp15@55321 ` 421` ``` have acn: "coprime (a^c) n" ``` haftmann@60688 ` 422` ``` by (metis coprime_exp_nat gcd.commute na) ``` lp15@55321 ` 423` ``` have "[a^d = a^e] (mod n) \ [a^(e + c) = a^(e + 0)] (mod n)" ``` lp15@55321 ` 424` ``` using c by simp ``` lp15@55321 ` 425` ``` also have "\ \ [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add) ``` lp15@55321 ` 426` ``` also have "\ \ [a ^ c = 1] (mod n)" ``` lp15@55321 ` 427` ``` using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp ``` lp15@55321 ` 428` ``` also have "\ \ ord n a dvd c" by (simp only: ord_divides) ``` lp15@55321 ` 429` ``` also have "\ \ [e + c = e + 0] (mod ord n a)" ``` lp15@55321 ` 430` ``` using cong_add_lcancel_nat ``` lp15@55321 ` 431` ``` by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1) ``` lp15@55321 ` 432` ``` finally have "[a^d = a^e] (mod n) \ [d = e] (mod (ord n a))" ``` lp15@55321 ` 433` ``` using c by simp } ``` lp15@55321 ` 434` ``` note th = this ``` lp15@55321 ` 435` ``` have "e \ d \ d \ e" by arith ``` lp15@55321 ` 436` ``` moreover ``` lp15@55321 ` 437` ``` {assume ed: "e \ d" from th[OF na ed] have ?thesis .} ``` lp15@55321 ` 438` ``` moreover ``` lp15@55321 ` 439` ``` {assume de: "d \ e" ``` lp15@55321 ` 440` ``` from th[OF na de] have ?thesis ``` lp15@55321 ` 441` ``` by (metis cong_sym_nat)} ``` lp15@55321 ` 442` ``` ultimately show ?thesis by blast ``` lp15@55321 ` 443` ```qed ``` lp15@55321 ` 444` wenzelm@60526 ` 445` ```subsection\Another trivial primality characterization\ ``` lp15@55321 ` 446` lp15@55321 ` 447` ```lemma prime_prime_factor: ``` lp15@55337 ` 448` ``` "prime n \ n \ 1 \ (\p. prime p \ p dvd n \ p = n)" ``` lp15@55337 ` 449` ``` (is "?lhs \ ?rhs") ``` lp15@55337 ` 450` ```proof (cases "n=0 \ n=1") ``` lp15@55337 ` 451` ``` case True ``` lp15@55337 ` 452` ``` then show ?thesis ``` lp15@55337 ` 453` ``` by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) ``` lp15@55337 ` 454` ```next ``` lp15@55337 ` 455` ``` case False ``` lp15@55337 ` 456` ``` show ?thesis ``` lp15@55337 ` 457` ``` proof ``` lp15@55337 ` 458` ``` assume "prime n" ``` lp15@55337 ` 459` ``` then show ?rhs ``` lp15@55337 ` 460` ``` by (metis one_not_prime_nat prime_nat_def) ``` lp15@55337 ` 461` ``` next ``` lp15@55337 ` 462` ``` assume ?rhs ``` lp15@55337 ` 463` ``` with False show "prime n" ``` lp15@55337 ` 464` ``` by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def) ``` lp15@55337 ` 465` ``` qed ``` lp15@55321 ` 466` ```qed ``` lp15@55321 ` 467` lp15@55321 ` 468` ```lemma prime_divisor_sqrt: ``` lp15@55321 ` 469` ``` "prime n \ n \ 1 \ (\d. d dvd n \ d\<^sup>2 \ n \ d = 1)" ``` lp15@55321 ` 470` ```proof - ``` lp15@55321 ` 471` ``` {assume "n=0 \ n=1" hence ?thesis ``` lp15@55321 ` 472` ``` by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)} ``` lp15@55321 ` 473` ``` moreover ``` lp15@55321 ` 474` ``` {assume n: "n\0" "n\1" ``` lp15@55321 ` 475` ``` hence np: "n > 1" by arith ``` lp15@55321 ` 476` ``` {fix d assume d: "d dvd n" "d\<^sup>2 \ n" and H: "\m. m dvd n \ m=1 \ m=n" ``` lp15@55321 ` 477` ``` from H d have d1n: "d = 1 \ d=n" by blast ``` lp15@55321 ` 478` ``` {assume dn: "d=n" ``` lp15@55321 ` 479` ``` have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square) ``` lp15@55321 ` 480` ``` with dn d(2) have "d=1" by simp} ``` lp15@55321 ` 481` ``` with d1n have "d = 1" by blast } ``` lp15@55321 ` 482` ``` moreover ``` lp15@55321 ` 483` ``` {fix d assume d: "d dvd n" and H: "\d'. d' dvd n \ d'\<^sup>2 \ n \ d' = 1" ``` lp15@55321 ` 484` ``` from d n have "d \ 0" ``` lp15@55321 ` 485` ``` by (metis dvd_0_left_iff) ``` lp15@55321 ` 486` ``` hence dp: "d > 0" by simp ``` lp15@55321 ` 487` ``` from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast ``` lp15@55321 ` 488` ``` from n dp e have ep:"e > 0" by simp ``` lp15@55321 ` 489` ``` have "d\<^sup>2 \ n \ e\<^sup>2 \ n" using dp ep ``` lp15@55321 ` 490` ``` by (auto simp add: e power2_eq_square mult_le_cancel_left) ``` lp15@55321 ` 491` ``` moreover ``` lp15@55321 ` 492` ``` {assume h: "d\<^sup>2 \ n" ``` lp15@55321 ` 493` ``` from H[rule_format, of d] h d have "d = 1" by blast} ``` lp15@55321 ` 494` ``` moreover ``` lp15@55321 ` 495` ``` {assume h: "e\<^sup>2 \ n" ``` haftmann@57512 ` 496` ``` from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute) ``` lp15@55321 ` 497` ``` with H[rule_format, of e] h have "e=1" by simp ``` lp15@55321 ` 498` ``` with e have "d = n" by simp} ``` lp15@55321 ` 499` ``` ultimately have "d=1 \ d=n" by blast} ``` lp15@55321 ` 500` ``` ultimately have ?thesis unfolding prime_def using np n(2) by blast} ``` lp15@55321 ` 501` ``` ultimately show ?thesis by auto ``` lp15@55321 ` 502` ```qed ``` lp15@55321 ` 503` lp15@55321 ` 504` ```lemma prime_prime_factor_sqrt: ``` lp15@55321 ` 505` ``` "prime n \ n \ 0 \ n \ 1 \ \ (\p. prime p \ p dvd n \ p\<^sup>2 \ n)" ``` lp15@55321 ` 506` ``` (is "?lhs \?rhs") ``` lp15@55321 ` 507` ```proof- ``` lp15@55321 ` 508` ``` {assume "n=0 \ n=1" ``` lp15@55321 ` 509` ``` hence ?thesis ``` lp15@55321 ` 510` ``` by (metis one_not_prime_nat zero_not_prime_nat)} ``` lp15@55321 ` 511` ``` moreover ``` lp15@55321 ` 512` ``` {assume n: "n\0" "n\1" ``` lp15@55321 ` 513` ``` {assume H: ?lhs ``` lp15@55321 ` 514` ``` from H[unfolded prime_divisor_sqrt] n ``` lp15@55321 ` 515` ``` have ?rhs ``` lp15@55337 ` 516` ``` by (metis prime_prime_factor) } ``` lp15@55321 ` 517` ``` moreover ``` lp15@55321 ` 518` ``` {assume H: ?rhs ``` lp15@55321 ` 519` ``` {fix d assume d: "d dvd n" "d\<^sup>2 \ n" "d\1" ``` lp15@55321 ` 520` ``` then obtain p where p: "prime p" "p dvd d" ``` lp15@55321 ` 521` ``` by (metis prime_factor_nat) ``` lp15@55337 ` 522` ``` from d(1) n have dp: "d > 0" ``` lp15@55337 ` 523` ``` by (metis dvd_0_left neq0_conv) ``` lp15@55321 ` 524` ``` from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) ``` lp15@55321 ` 525` ``` have "p\<^sup>2 \ n" unfolding power2_eq_square by arith ``` lp15@55321 ` 526` ``` with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast} ``` lp15@55321 ` 527` ``` with n prime_divisor_sqrt have ?lhs by auto} ``` lp15@55321 ` 528` ``` ultimately have ?thesis by blast } ``` lp15@55321 ` 529` ``` ultimately show ?thesis by (cases "n=0 \ n=1", auto) ``` lp15@55321 ` 530` ```qed ``` lp15@55321 ` 531` lp15@55321 ` 532` wenzelm@60526 ` 533` ```subsection\Pocklington theorem\ ``` lp15@55321 ` 534` lp15@55321 ` 535` ```lemma pocklington_lemma: ``` lp15@55321 ` 536` ``` assumes n: "n \ 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)" ``` lp15@55321 ` 537` ``` and aq:"\p. prime p \ p dvd q \ coprime (a^ ((n - 1) div p) - 1) n" ``` lp15@55321 ` 538` ``` and pp: "prime p" and pn: "p dvd n" ``` lp15@55321 ` 539` ``` shows "[p = 1] (mod q)" ``` lp15@55321 ` 540` ```proof - ``` lp15@55321 ` 541` ``` have p01: "p \ 0" "p \ 1" using pp one_not_prime_nat zero_not_prime_nat by auto ``` lp15@55321 ` 542` ``` obtain k where k: "a ^ (q * r) - 1 = n*k" ``` lp15@55321 ` 543` ``` by (metis an cong_to_1_nat dvd_def nqr) ``` lp15@55321 ` 544` ``` from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast ``` lp15@55321 ` 545` ``` {assume a0: "a = 0" ``` lp15@55321 ` 546` ``` hence "a^ (n - 1) = 0" using n by (simp add: power_0_left) ``` lp15@55321 ` 547` ``` with n an mod_less[of 1 n] have False by (simp add: power_0_left cong_nat_def)} ``` lp15@55321 ` 548` ``` hence a0: "a\0" .. ``` lp15@55321 ` 549` ``` from n nqr have aqr0: "a ^ (q * r) \ 0" using a0 by simp ``` lp15@55321 ` 550` ``` hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp ``` lp15@55321 ` 551` ``` with k l have "a ^ (q * r) = p*l*k + 1" by simp ``` haftmann@57514 ` 552` ``` hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps) ``` lp15@55321 ` 553` ``` hence odq: "ord p (a^r) dvd q" ``` lp15@55321 ` 554` ``` unfolding ord_divides[symmetric] power_mult[symmetric] ``` haftmann@57512 ` 555` ``` by (metis an cong_dvd_modulus_nat mult.commute nqr pn) ``` lp15@55321 ` 556` ``` from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast ``` lp15@55321 ` 557` ``` {assume d1: "d \ 1" ``` lp15@55321 ` 558` ``` obtain P where P: "prime P" "P dvd d" ``` lp15@55321 ` 559` ``` by (metis d1 prime_factor_nat) ``` lp15@55321 ` 560` ``` from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp ``` lp15@55321 ` 561` ``` from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast ``` lp15@55321 ` 562` ``` from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast ``` lp15@55321 ` 563` ``` have P0: "P \ 0" using P(1) ``` lp15@55321 ` 564` ``` by (metis zero_not_prime_nat) ``` lp15@55321 ` 565` ``` from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast ``` lp15@55321 ` 566` ``` from d s t P0 have s': "ord p (a^r) * t = s" ``` haftmann@57512 ` 567` ``` by (metis mult.commute mult_cancel1 mult.assoc) ``` lp15@55321 ` 568` ``` have "ord p (a^r) * t*r = r * ord p (a^r) * t" ``` haftmann@57512 ` 569` ``` by (metis mult.assoc mult.commute) ``` lp15@55321 ` 570` ``` hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" ``` lp15@55321 ` 571` ``` by (simp only: power_mult) ``` lp15@55321 ` 572` ``` then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" ``` lp15@55337 ` 573` ``` by (metis cong_exp_nat ord power_one) ``` lp15@55321 ` 574` ``` have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" ``` lp15@55321 ` 575` ``` by (metis cong_to_1_nat exps th) ``` lp15@55321 ` 576` ``` from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp ``` lp15@55321 ` 577` ``` with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp ``` lp15@55321 ` 578` ``` with p01 pn pd0 coprime_common_divisor_nat have False ``` lp15@55321 ` 579` ``` by auto} ``` lp15@55321 ` 580` ``` hence d1: "d = 1" by blast ``` lp15@55321 ` 581` ``` hence o: "ord p (a^r) = q" using d by simp ``` lp15@55321 ` 582` ``` from pp phi_prime[of p] have phip: "phi p = p - 1" by simp ``` lp15@55321 ` 583` ``` {fix d assume d: "d dvd p" "d dvd a" "d \ 1" ``` lp15@55321 ` 584` ``` from pp[unfolded prime_def] d have dp: "d = p" by blast ``` lp15@55321 ` 585` ``` from n have "n \ 0" by simp ``` lp15@55321 ` 586` ``` then have False using d ``` lp15@55321 ` 587` ``` by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat ``` lp15@55321 ` 588` ``` gcd_lcm_complete_lattice_nat.top_greatest pn)} ``` lp15@55321 ` 589` ``` hence cpa: "coprime p a" by auto ``` lp15@55321 ` 590` ``` have arp: "coprime (a^r) p" ``` haftmann@60688 ` 591` ``` by (metis coprime_exp_nat cpa gcd.commute) ``` lp15@55321 ` 592` ``` from euler_theorem_nat[OF arp, simplified ord_divides] o phip ``` lp15@55321 ` 593` ``` have "q dvd (p - 1)" by simp ``` lp15@55337 ` 594` ``` then obtain d where d:"p - 1 = q * d" ``` lp15@55337 ` 595` ``` unfolding dvd_def by blast ``` lp15@55321 ` 596` ``` have p0:"p \ 0" ``` lp15@55321 ` 597` ``` by (metis p01(1)) ``` lp15@55321 ` 598` ``` from p0 d have "p + q * 0 = 1 + q * d" by simp ``` lp15@55321 ` 599` ``` then show ?thesis ``` haftmann@57512 ` 600` ``` by (metis cong_iff_lin_nat mult.commute) ``` lp15@55321 ` 601` ```qed ``` lp15@55321 ` 602` lp15@55321 ` 603` ```theorem pocklington: ``` lp15@55321 ` 604` ``` assumes n: "n \ 2" and nqr: "n - 1 = q*r" and sqr: "n \ q\<^sup>2" ``` lp15@55321 ` 605` ``` and an: "[a^ (n - 1) = 1] (mod n)" ``` lp15@55321 ` 606` ``` and aq: "\p. prime p \ p dvd q \ coprime (a^ ((n - 1) div p) - 1) n" ``` lp15@55321 ` 607` ``` shows "prime n" ``` lp15@55321 ` 608` ```unfolding prime_prime_factor_sqrt[of n] ``` lp15@55321 ` 609` ```proof- ``` lp15@55321 ` 610` ``` let ?ths = "n \ 0 \ n \ 1 \ \ (\p. prime p \ p dvd n \ p\<^sup>2 \ n)" ``` lp15@55321 ` 611` ``` from n have n01: "n\0" "n\1" by arith+ ``` lp15@55321 ` 612` ``` {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \ n" ``` lp15@55321 ` 613` ``` from p(3) sqr have "p^(Suc 1) \ q^(Suc 1)" by (simp add: power2_eq_square) ``` lp15@55321 ` 614` ``` hence pq: "p \ q" ``` lp15@55321 ` 615` ``` by (metis le0 power_le_imp_le_base) ``` lp15@55321 ` 616` ``` from pocklington_lemma[OF n nqr an aq p(1,2)] ``` lp15@55321 ` 617` ``` have th: "q dvd p - 1" ``` lp15@55321 ` 618` ``` by (metis cong_to_1_nat) ``` lp15@55321 ` 619` ``` have "p - 1 \ 0" using prime_ge_2_nat [OF p(1)] by arith ``` lp15@55321 ` 620` ``` with pq p have False ``` lp15@55321 ` 621` ``` by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq ``` lp15@55321 ` 622` ``` prime_gt_0_nat th) } ``` lp15@55321 ` 623` ``` with n01 show ?ths by blast ``` lp15@55321 ` 624` ```qed ``` lp15@55321 ` 625` lp15@55321 ` 626` ```(* Variant for application, to separate the exponentiation. *) ``` lp15@55321 ` 627` ```lemma pocklington_alt: ``` lp15@55321 ` 628` ``` assumes n: "n \ 2" and nqr: "n - 1 = q*r" and sqr: "n \ q\<^sup>2" ``` lp15@55321 ` 629` ``` and an: "[a^ (n - 1) = 1] (mod n)" ``` lp15@55321 ` 630` ``` and aq:"\p. prime p \ p dvd q \ (\b. [a^((n - 1) div p) = b] (mod n) \ coprime (b - 1) n)" ``` lp15@55321 ` 631` ``` shows "prime n" ``` lp15@55321 ` 632` ```proof- ``` lp15@55321 ` 633` ``` {fix p assume p: "prime p" "p dvd q" ``` lp15@55321 ` 634` ``` from aq[rule_format] p obtain b where ``` lp15@55321 ` 635` ``` b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast ``` lp15@55321 ` 636` ``` {assume a0: "a=0" ``` lp15@55321 ` 637` ``` from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto ``` lp15@55321 ` 638` ``` hence False using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])} ``` lp15@55321 ` 639` ``` hence a0: "a\ 0" .. ``` lp15@55321 ` 640` ``` hence a1: "a \ 1" by arith ``` lp15@55321 ` 641` ``` from one_le_power[OF a1] have ath: "1 \ a ^ ((n - 1) div p)" . ``` lp15@55321 ` 642` ``` {assume b0: "b = 0" ``` lp15@55321 ` 643` ``` from p(2) nqr have "(n - 1) mod p = 0" ``` lp15@55321 ` 644` ``` by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0) ``` lp15@55321 ` 645` ``` with mod_div_equality[of "n - 1" p] ``` lp15@55321 ` 646` ``` have "(n - 1) div p * p= n - 1" by auto ``` lp15@55321 ` 647` ``` hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" ``` lp15@55321 ` 648` ``` by (simp only: power_mult[symmetric]) ``` lp15@55321 ` 649` ``` have "p - 1 \ 0" using prime_ge_2_nat [OF p(1)] by arith ``` lp15@55321 ` 650` ``` then have pS: "Suc (p - 1) = p" by arith ``` lp15@55321 ` 651` ``` from b have d: "n dvd a^((n - 1) div p)" unfolding b0 ``` lp15@55321 ` 652` ``` by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left ``` lp15@55321 ` 653` ``` gcd_lcm_complete_lattice_nat.inf_top_left) ``` lp15@55321 ` 654` ``` from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n ``` lp15@55321 ` 655` ``` have False ``` lp15@55321 ` 656` ``` by simp} ``` lp15@55321 ` 657` ``` then have b0: "b \ 0" .. ``` lp15@55346 ` 658` ``` hence b1: "b \ 1" by arith ``` lp15@55346 ` 659` ``` from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] ``` lp15@55346 ` 660` ``` ath b1 b nqr ``` lp15@55321 ` 661` ``` have "coprime (a ^ ((n - 1) div p) - 1) n" ``` lp15@55321 ` 662` ``` by simp} ``` lp15@55321 ` 663` ``` hence th: "\p. prime p \ p dvd q \ coprime (a ^ ((n - 1) div p) - 1) n " ``` lp15@55321 ` 664` ``` by blast ``` lp15@55321 ` 665` ``` from pocklington[OF n nqr sqr an th] show ?thesis . ``` lp15@55321 ` 666` ```qed ``` lp15@55321 ` 667` lp15@55321 ` 668` wenzelm@60526 ` 669` ```subsection\Prime factorizations\ ``` lp15@55321 ` 670` wenzelm@55370 ` 671` ```(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *) ``` lp15@55321 ` 672` lp15@55321 ` 673` ```definition "primefact ps n = (foldr op * ps 1 = n \ (\p\ set ps. prime p))" ``` lp15@55321 ` 674` lp15@55321 ` 675` ```lemma primefact: assumes n: "n \ 0" ``` lp15@55321 ` 676` ``` shows "\ps. primefact ps n" ``` lp15@55321 ` 677` ```using n ``` lp15@55321 ` 678` ```proof(induct n rule: nat_less_induct) ``` lp15@55321 ` 679` ``` fix n assume H: "\m 0 \ (\ps. primefact ps m)" and n: "n\0" ``` lp15@55321 ` 680` ``` let ?ths = "\ps. primefact ps n" ``` lp15@55321 ` 681` ``` {assume "n = 1" ``` lp15@55321 ` 682` ``` hence "primefact [] n" by (simp add: primefact_def) ``` lp15@55321 ` 683` ``` hence ?ths by blast } ``` lp15@55321 ` 684` ``` moreover ``` lp15@55321 ` 685` ``` {assume n1: "n \ 1" ``` lp15@55321 ` 686` ``` with n have n2: "n \ 2" by arith ``` lp15@55321 ` 687` ``` obtain p where p: "prime p" "p dvd n" ``` lp15@55321 ` 688` ``` by (metis n1 prime_factor_nat) ``` lp15@55321 ` 689` ``` from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast ``` lp15@55321 ` 690` ``` from n m have m0: "m > 0" "m\0" by auto ``` lp15@55321 ` 691` ``` have "1 < p" ``` lp15@55321 ` 692` ``` by (metis p(1) prime_nat_def) ``` lp15@55321 ` 693` ``` with m0 m have mn: "m < n" by auto ``` lp15@55321 ` 694` ``` from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" .. ``` lp15@55321 ` 695` ``` from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def) ``` lp15@55321 ` 696` ``` hence ?ths by blast} ``` lp15@55321 ` 697` ``` ultimately show ?ths by blast ``` lp15@55321 ` 698` ```qed ``` lp15@55321 ` 699` lp15@55321 ` 700` ```lemma primefact_contains: ``` lp15@55321 ` 701` ``` assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n" ``` lp15@55321 ` 702` ``` shows "p \ set ps" ``` lp15@55321 ` 703` ``` using pf p pn ``` lp15@55321 ` 704` ```proof(induct ps arbitrary: p n) ``` lp15@55321 ` 705` ``` case Nil thus ?case by (auto simp add: primefact_def) ``` lp15@55321 ` 706` ```next ``` lp15@55321 ` 707` ``` case (Cons q qs p n) ``` lp15@55321 ` 708` ``` from Cons.prems[unfolded primefact_def] ``` lp15@55321 ` 709` ``` have q: "prime q" "q * foldr op * qs 1 = n" "\p \set qs. prime p" and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all ``` lp15@55321 ` 710` ``` {assume "p dvd q" ``` lp15@55321 ` 711` ``` with p(1) q(1) have "p = q" unfolding prime_def by auto ``` lp15@55321 ` 712` ``` hence ?case by simp} ``` lp15@55321 ` 713` ``` moreover ``` lp15@55321 ` 714` ``` { assume h: "p dvd foldr op * qs 1" ``` lp15@55321 ` 715` ``` from q(3) have pqs: "primefact qs (foldr op * qs 1)" ``` lp15@55321 ` 716` ``` by (simp add: primefact_def) ``` lp15@55321 ` 717` ``` from Cons.hyps[OF pqs p(1) h] have ?case by simp} ``` lp15@55321 ` 718` ``` ultimately show ?case ``` lp15@55321 ` 719` ``` by (metis p prime_dvd_mult_eq_nat) ``` lp15@55321 ` 720` ```qed ``` lp15@55321 ` 721` lp15@55321 ` 722` ```lemma primefact_variant: "primefact ps n \ foldr op * ps 1 = n \ list_all prime ps" ``` lp15@55321 ` 723` ``` by (auto simp add: primefact_def list_all_iff) ``` lp15@55321 ` 724` lp15@55321 ` 725` ```(* Variant of Lucas theorem. *) ``` lp15@55321 ` 726` lp15@55321 ` 727` ```lemma lucas_primefact: ``` lp15@55321 ` 728` ``` assumes n: "n \ 2" and an: "[a^(n - 1) = 1] (mod n)" ``` lp15@55321 ` 729` ``` and psn: "foldr op * ps 1 = n - 1" ``` lp15@55321 ` 730` ``` and psp: "list_all (\p. prime p \ \ [a^((n - 1) div p) = 1] (mod n)) ps" ``` lp15@55321 ` 731` ``` shows "prime n" ``` lp15@55321 ` 732` ```proof- ``` lp15@55321 ` 733` ``` {fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)" ``` lp15@55321 ` 734` ``` from psn psp have psn1: "primefact ps (n - 1)" ``` lp15@55321 ` 735` ``` by (auto simp add: list_all_iff primefact_variant) ``` lp15@55321 ` 736` ``` from p(3) primefact_contains[OF psn1 p(1,2)] psp ``` lp15@55321 ` 737` ``` have False by (induct ps, auto)} ``` lp15@55321 ` 738` ``` with lucas[OF n an] show ?thesis by blast ``` lp15@55321 ` 739` ```qed ``` lp15@55321 ` 740` lp15@55321 ` 741` ```(* Variant of Pocklington theorem. *) ``` lp15@55321 ` 742` lp15@55321 ` 743` ```lemma pocklington_primefact: ``` lp15@55321 ` 744` ``` assumes n: "n \ 2" and qrn: "q*r = n - 1" and nq2: "n \ q\<^sup>2" ``` lp15@55321 ` 745` ``` and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q" ``` lp15@55321 ` 746` ``` and bqn: "(b^q) mod n = 1" ``` lp15@55321 ` 747` ``` and psp: "list_all (\p. prime p \ coprime ((b^(q div p)) mod n - 1) n) ps" ``` lp15@55321 ` 748` ``` shows "prime n" ``` lp15@55321 ` 749` ```proof- ``` lp15@55321 ` 750` ``` from bqn psp qrn ``` lp15@55321 ` 751` ``` have bqn: "a ^ (n - 1) mod n = 1" ``` lp15@55337 ` 752` ``` and psp: "list_all (\p. prime p \ coprime (a^(r *(q div p)) mod n - 1) n) ps" ``` lp15@55337 ` 753` ``` unfolding arnb[symmetric] power_mod ``` lp15@55321 ` 754` ``` by (simp_all add: power_mult[symmetric] algebra_simps) ``` lp15@55321 ` 755` ``` from n have n0: "n > 0" by arith ``` lp15@55321 ` 756` ``` from mod_div_equality[of "a^(n - 1)" n] ``` lp15@55321 ` 757` ``` mod_less_divisor[OF n0, of "a^(n - 1)"] ``` lp15@55321 ` 758` ``` have an1: "[a ^ (n - 1) = 1] (mod n)" ``` lp15@55321 ` 759` ``` by (metis bqn cong_nat_def mod_mod_trivial) ``` lp15@55321 ` 760` ``` {fix p assume p: "prime p" "p dvd q" ``` lp15@55321 ` 761` ``` from psp psq have pfpsq: "primefact ps q" ``` lp15@55321 ` 762` ``` by (auto simp add: primefact_variant list_all_iff) ``` lp15@55321 ` 763` ``` from psp primefact_contains[OF pfpsq p] ``` lp15@55321 ` 764` ``` have p': "coprime (a ^ (r * (q div p)) mod n - 1) n" ``` lp15@55321 ` 765` ``` by (simp add: list_all_iff) ``` lp15@55321 ` 766` ``` from p prime_def have p01: "p \ 0" "p \ 1" "p =Suc(p - 1)" ``` lp15@55321 ` 767` ``` by auto ``` lp15@55321 ` 768` ``` from div_mult1_eq[of r q p] p(2) ``` lp15@55321 ` 769` ``` have eq1: "r* (q div p) = (n - 1) div p" ``` haftmann@57512 ` 770` ``` unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute) ``` lp15@55321 ` 771` ``` have ath: "\a (b::nat). a <= b \ a \ 0 ==> 1 <= a \ 1 <= b" by arith ``` lp15@55321 ` 772` ``` {assume "a ^ ((n - 1) div p) mod n = 0" ``` lp15@55321 ` 773` ``` then obtain s where s: "a ^ ((n - 1) div p) = n*s" ``` lp15@55321 ` 774` ``` unfolding mod_eq_0_iff by blast ``` lp15@55321 ` 775` ``` hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp ``` lp15@55321 ` 776` ``` from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto ``` haftmann@58834 ` 777` ``` from dvd_trans[OF p(2) qn1] ``` haftmann@58834 ` 778` ``` have npp: "(n - 1) div p * p = n - 1" by simp ``` lp15@55321 ` 779` ``` with eq0 have "a^ (n - 1) = (n*s)^p" ``` lp15@55321 ` 780` ``` by (simp add: power_mult[symmetric]) ``` lp15@55321 ` 781` ``` hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp ``` haftmann@57512 ` 782` ``` also have "\ = 0" by (simp add: mult.assoc) ``` lp15@55321 ` 783` ``` finally have False by simp } ``` lp15@55321 ` 784` ``` then have th11: "a ^ ((n - 1) div p) mod n \ 0" by auto ``` lp15@55321 ` 785` ``` have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)" ``` lp15@55321 ` 786` ``` unfolding cong_nat_def by simp ``` lp15@55321 ` 787` ``` from th1 ath[OF mod_less_eq_dividend th11] ``` lp15@55321 ` 788` ``` have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)" ``` lp15@55321 ` 789` ``` by (metis cong_diff_nat cong_refl_nat) ``` lp15@55321 ` 790` ``` have "coprime (a ^ ((n - 1) div p) - 1) n" ``` lp15@55321 ` 791` ``` by (metis cong_imp_coprime_nat eq1 p' th) } ``` lp15@55321 ` 792` ``` with pocklington[OF n qrn[symmetric] nq2 an1] ``` lp15@55321 ` 793` ``` show ?thesis by blast ``` lp15@55321 ` 794` ```qed ``` lp15@55321 ` 795` lp15@55321 ` 796` ```end ```