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