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