src/HOL/Number_Theory/Residues.thy
 author paulson Thu Jun 14 15:20:10 2018 +0100 (10 months ago) changeset 68447 0beb927eed89 parent 67341 df79ef3b3a41 child 68458 023b353911c5 permissions -rw-r--r--
 wenzelm@41959 ` 1` ```(* Title: HOL/Number_Theory/Residues.thy ``` nipkow@31719 ` 2` ``` Author: Jeremy Avigad ``` nipkow@31719 ` 3` wenzelm@41541 ` 4` ```An algebraic treatment of residue rings, and resulting proofs of ``` wenzelm@41959 ` 5` ```Euler's theorem and Wilson's theorem. ``` nipkow@31719 ` 6` ```*) ``` nipkow@31719 ` 7` wenzelm@60526 ` 8` ```section \Residue rings\ ``` nipkow@31719 ` 9` nipkow@31719 ` 10` ```theory Residues ``` haftmann@65416 ` 11` ```imports ``` haftmann@65416 ` 12` ``` Cong ``` wenzelm@66453 ` 13` ``` "HOL-Algebra.Multiplicative_Group" ``` haftmann@65465 ` 14` ``` Totient ``` nipkow@31719 ` 15` ```begin ``` nipkow@31719 ` 16` wenzelm@66305 ` 17` ```definition QuadRes :: "int \ int \ bool" ``` wenzelm@66305 ` 18` ``` where "QuadRes p a = (\y. ([y^2 = a] (mod p)))" ``` eberlm@64282 ` 19` wenzelm@66305 ` 20` ```definition Legendre :: "int \ int \ int" ``` wenzelm@66305 ` 21` ``` where "Legendre a p = ``` wenzelm@66305 ` 22` ``` (if ([a = 0] (mod p)) then 0 ``` wenzelm@66305 ` 23` ``` else if QuadRes p a then 1 ``` wenzelm@66305 ` 24` ``` else -1)" ``` wenzelm@66305 ` 25` eberlm@64282 ` 26` wenzelm@60527 ` 27` ```subsection \A locale for residue rings\ ``` nipkow@31719 ` 28` wenzelm@60527 ` 29` ```definition residue_ring :: "int \ int ring" ``` wenzelm@66305 ` 30` ``` where ``` wenzelm@66305 ` 31` ``` "residue_ring m = ``` wenzelm@66305 ` 32` ``` \carrier = {0..m - 1}, ``` wenzelm@66305 ` 33` ``` monoid.mult = \x y. (x * y) mod m, ``` wenzelm@66305 ` 34` ``` one = 1, ``` wenzelm@66305 ` 35` ``` zero = 0, ``` wenzelm@66305 ` 36` ``` add = \x y. (x + y) mod m\" ``` nipkow@31719 ` 37` nipkow@31719 ` 38` ```locale residues = ``` nipkow@31719 ` 39` ``` fixes m :: int and R (structure) ``` nipkow@31719 ` 40` ``` assumes m_gt_one: "m > 1" ``` wenzelm@60527 ` 41` ``` defines "R \ residue_ring m" ``` wenzelm@44872 ` 42` ```begin ``` nipkow@31719 ` 43` nipkow@31719 ` 44` ```lemma abelian_group: "abelian_group R" ``` lp15@65066 ` 45` ```proof - ``` lp15@65066 ` 46` ``` have "\y\{0..m - 1}. (x + y) mod m = 0" if "0 \ x" "x < m" for x ``` lp15@65066 ` 47` ``` proof (cases "x = 0") ``` lp15@65066 ` 48` ``` case True ``` lp15@65066 ` 49` ``` with m_gt_one show ?thesis by simp ``` lp15@65066 ` 50` ``` next ``` lp15@65066 ` 51` ``` case False ``` lp15@65066 ` 52` ``` then have "(x + (m - x)) mod m = 0" ``` lp15@65066 ` 53` ``` by simp ``` lp15@65066 ` 54` ``` with m_gt_one that show ?thesis ``` lp15@65066 ` 55` ``` by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le) ``` lp15@65066 ` 56` ``` qed ``` lp15@65066 ` 57` ``` with m_gt_one show ?thesis ``` lp15@65066 ` 58` ``` by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps intro!: abelian_groupI) ``` wenzelm@65899 ` 59` ```qed ``` nipkow@31719 ` 60` nipkow@31719 ` 61` ```lemma comm_monoid: "comm_monoid R" ``` lp15@65066 ` 62` ``` unfolding R_def residue_ring_def ``` nipkow@31719 ` 63` ``` apply (rule comm_monoidI) ``` lp15@65066 ` 64` ``` using m_gt_one apply auto ``` lp15@65066 ` 65` ``` apply (metis mod_mult_right_eq mult.assoc mult.commute) ``` lp15@65066 ` 66` ``` apply (metis mult.commute) ``` wenzelm@41541 ` 67` ``` done ``` nipkow@31719 ` 68` nipkow@31719 ` 69` ```lemma cring: "cring R" ``` lp15@65066 ` 70` ``` apply (intro cringI abelian_group comm_monoid) ``` lp15@65066 ` 71` ``` unfolding R_def residue_ring_def ``` lp15@65066 ` 72` ``` apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq) ``` wenzelm@41541 ` 73` ``` done ``` nipkow@31719 ` 74` nipkow@31719 ` 75` ```end ``` nipkow@31719 ` 76` nipkow@31719 ` 77` ```sublocale residues < cring ``` nipkow@31719 ` 78` ``` by (rule cring) ``` nipkow@31719 ` 79` nipkow@31719 ` 80` wenzelm@41541 ` 81` ```context residues ``` wenzelm@41541 ` 82` ```begin ``` nipkow@31719 ` 83` wenzelm@60527 ` 84` ```text \ ``` wenzelm@60527 ` 85` ``` These lemmas translate back and forth between internal and ``` wenzelm@60527 ` 86` ``` external concepts. ``` wenzelm@60527 ` 87` ```\ ``` nipkow@31719 ` 88` nipkow@31719 ` 89` ```lemma res_carrier_eq: "carrier R = {0..m - 1}" ``` wenzelm@66305 ` 90` ``` by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 91` nipkow@31719 ` 92` ```lemma res_add_eq: "x \ y = (x + y) mod m" ``` wenzelm@66305 ` 93` ``` by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 94` nipkow@31719 ` 95` ```lemma res_mult_eq: "x \ y = (x * y) mod m" ``` wenzelm@66305 ` 96` ``` by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 97` nipkow@31719 ` 98` ```lemma res_zero_eq: "\ = 0" ``` wenzelm@66305 ` 99` ``` by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 100` nipkow@31719 ` 101` ```lemma res_one_eq: "\ = 1" ``` wenzelm@66305 ` 102` ``` by (auto simp: R_def residue_ring_def units_of_def) ``` nipkow@31719 ` 103` wenzelm@60527 ` 104` ```lemma res_units_eq: "Units R = {x. 0 < x \ x < m \ coprime x m}" ``` lp15@65066 ` 105` ``` using m_gt_one ``` haftmann@67051 ` 106` ``` apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr) ``` nipkow@31952 ` 107` ``` apply (subst (asm) coprime_iff_invertible'_int) ``` haftmann@67051 ` 108` ``` apply (auto simp add: cong_def) ``` wenzelm@41541 ` 109` ``` done ``` nipkow@31719 ` 110` nipkow@31719 ` 111` ```lemma res_neg_eq: "\ x = (- x) mod m" ``` lp15@65066 ` 112` ``` using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def ``` lp15@65066 ` 113` ``` apply simp ``` nipkow@31719 ` 114` ``` apply (rule the_equality) ``` wenzelm@66305 ` 115` ``` apply (simp add: mod_add_right_eq) ``` wenzelm@66305 ` 116` ``` apply (simp add: add.commute mod_add_right_eq) ``` lp15@65066 ` 117` ``` apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial) ``` wenzelm@41541 ` 118` ``` done ``` nipkow@31719 ` 119` wenzelm@44872 ` 120` ```lemma finite [iff]: "finite (carrier R)" ``` haftmann@65416 ` 121` ``` by (simp add: res_carrier_eq) ``` nipkow@31719 ` 122` wenzelm@44872 ` 123` ```lemma finite_Units [iff]: "finite (Units R)" ``` haftmann@65416 ` 124` ``` by (simp add: finite_ring_finite_units) ``` nipkow@31719 ` 125` wenzelm@60527 ` 126` ```text \ ``` wenzelm@63167 ` 127` ``` The function \a \ a mod m\ maps the integers to the ``` wenzelm@60527 ` 128` ``` residue classes. The following lemmas show that this mapping ``` wenzelm@60527 ` 129` ``` respects addition and multiplication on the integers. ``` wenzelm@60527 ` 130` ```\ ``` nipkow@31719 ` 131` wenzelm@60527 ` 132` ```lemma mod_in_carrier [iff]: "a mod m \ carrier R" ``` wenzelm@60527 ` 133` ``` unfolding res_carrier_eq ``` wenzelm@60527 ` 134` ``` using insert m_gt_one by auto ``` nipkow@31719 ` 135` nipkow@31719 ` 136` ```lemma add_cong: "(x mod m) \ (y mod m) = (x + y) mod m" ``` wenzelm@66305 ` 137` ``` by (auto simp: R_def residue_ring_def mod_simps) ``` nipkow@31719 ` 138` nipkow@31719 ` 139` ```lemma mult_cong: "(x mod m) \ (y mod m) = (x * y) mod m" ``` wenzelm@66305 ` 140` ``` by (auto simp: R_def residue_ring_def mod_simps) ``` nipkow@31719 ` 141` nipkow@31719 ` 142` ```lemma zero_cong: "\ = 0" ``` wenzelm@66305 ` 143` ``` by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 144` nipkow@31719 ` 145` ```lemma one_cong: "\ = 1 mod m" ``` wenzelm@66305 ` 146` ``` using m_gt_one by (auto simp: R_def residue_ring_def) ``` nipkow@31719 ` 147` wenzelm@60527 ` 148` ```(* FIXME revise algebra library to use 1? *) ``` nipkow@67341 ` 149` ```lemma pow_cong: "(x mod m) [^] n = x^n mod m" ``` lp15@65066 ` 150` ``` using m_gt_one ``` nipkow@31719 ` 151` ``` apply (induct n) ``` wenzelm@41541 ` 152` ``` apply (auto simp add: nat_pow_def one_cong) ``` haftmann@57512 ` 153` ``` apply (metis mult.commute mult_cong) ``` wenzelm@41541 ` 154` ``` done ``` nipkow@31719 ` 155` nipkow@31719 ` 156` ```lemma neg_cong: "\ (x mod m) = (- x) mod m" ``` lp15@55352 ` 157` ``` by (metis mod_minus_eq res_neg_eq) ``` nipkow@31719 ` 158` wenzelm@60528 ` 159` ```lemma (in residues) prod_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 160` ``` by (induct set: finite) (auto simp: one_cong mult_cong) ``` nipkow@31719 ` 161` wenzelm@60528 ` 162` ```lemma (in residues) sum_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 163` ``` by (induct set: finite) (auto simp: zero_cong add_cong) ``` nipkow@31719 ` 164` haftmann@60688 ` 165` ```lemma mod_in_res_units [simp]: ``` haftmann@60688 ` 166` ``` assumes "1 < m" and "coprime a m" ``` haftmann@60688 ` 167` ``` shows "a mod m \ Units R" ``` haftmann@60688 ` 168` ```proof (cases "a mod m = 0") ``` wenzelm@66305 ` 169` ``` case True ``` wenzelm@66305 ` 170` ``` with assms show ?thesis ``` haftmann@60688 ` 171` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric]) ``` haftmann@60688 ` 172` ```next ``` haftmann@60688 ` 173` ``` case False ``` haftmann@60688 ` 174` ``` from assms have "0 < m" by simp ``` wenzelm@66305 ` 175` ``` then have "0 \ a mod m" by (rule pos_mod_sign [of m a]) ``` haftmann@60688 ` 176` ``` with False have "0 < a mod m" by simp ``` haftmann@60688 ` 177` ``` with assms show ?thesis ``` haftmann@60688 ` 178` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps) ``` haftmann@60688 ` 179` ```qed ``` nipkow@31719 ` 180` wenzelm@60528 ` 181` ```lemma res_eq_to_cong: "(a mod m) = (b mod m) \ [a = b] (mod m)" ``` haftmann@66888 ` 182` ``` by (auto simp: cong_def) ``` nipkow@31719 ` 183` nipkow@31719 ` 184` wenzelm@60528 ` 185` ```text \Simplifying with these will translate a ring equation in R to a congruence.\ ``` wenzelm@66305 ` 186` ```lemmas res_to_cong_simps = ``` wenzelm@66305 ` 187` ``` add_cong mult_cong pow_cong one_cong ``` wenzelm@66305 ` 188` ``` prod_cong sum_cong neg_cong res_eq_to_cong ``` nipkow@31719 ` 189` wenzelm@60527 ` 190` ```text \Other useful facts about the residue ring.\ ``` nipkow@31719 ` 191` ```lemma one_eq_neg_one: "\ = \ \ \ m = 2" ``` nipkow@31719 ` 192` ``` apply (simp add: res_one_eq res_neg_eq) ``` haftmann@57512 ` 193` ``` apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff ``` wenzelm@60528 ` 194` ``` zero_neq_one zmod_zminus1_eq_if) ``` wenzelm@41541 ` 195` ``` done ``` nipkow@31719 ` 196` nipkow@31719 ` 197` ```end ``` nipkow@31719 ` 198` nipkow@31719 ` 199` wenzelm@60527 ` 200` ```subsection \Prime residues\ ``` nipkow@31719 ` 201` nipkow@31719 ` 202` ```locale residues_prime = ``` eberlm@63534 ` 203` ``` fixes p :: nat and R (structure) ``` nipkow@31719 ` 204` ``` assumes p_prime [intro]: "prime p" ``` eberlm@63534 ` 205` ``` defines "R \ residue_ring (int p)" ``` nipkow@31719 ` 206` nipkow@31719 ` 207` ```sublocale residues_prime < residues p ``` lp15@65066 ` 208` ``` unfolding R_def residues_def ``` nipkow@31719 ` 209` ``` using p_prime apply auto ``` haftmann@62348 ` 210` ``` apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) ``` wenzelm@41541 ` 211` ``` done ``` nipkow@31719 ` 212` wenzelm@44872 ` 213` ```context residues_prime ``` wenzelm@44872 ` 214` ```begin ``` nipkow@31719 ` 215` haftmann@67051 ` 216` ```lemma p_coprime_left: ``` haftmann@67051 ` 217` ``` "coprime p a \ \ p dvd a" ``` haftmann@67051 ` 218` ``` using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor) ``` haftmann@67051 ` 219` haftmann@67051 ` 220` ```lemma p_coprime_right: ``` haftmann@67051 ` 221` ``` "coprime a p \ \ p dvd a" ``` haftmann@67051 ` 222` ``` using p_coprime_left [of a] by (simp add: ac_simps) ``` haftmann@67051 ` 223` haftmann@67051 ` 224` ```lemma p_coprime_left_int: ``` haftmann@67051 ` 225` ``` "coprime (int p) a \ \ int p dvd a" ``` haftmann@67051 ` 226` ``` using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor) ``` haftmann@67051 ` 227` haftmann@67051 ` 228` ```lemma p_coprime_right_int: ``` haftmann@67051 ` 229` ``` "coprime a (int p) \ \ int p dvd a" ``` haftmann@67051 ` 230` ``` using p_coprime_left_int [of a] by (simp add: ac_simps) ``` haftmann@67051 ` 231` nipkow@31719 ` 232` ```lemma is_field: "field R" ``` lp15@65066 ` 233` ```proof - ``` haftmann@66837 ` 234` ``` have "0 < x \ x < int p \ coprime (int p) x" for x ``` haftmann@66837 ` 235` ``` by (rule prime_imp_coprime) (auto simp add: zdvd_not_zless) ``` lp15@65066 ` 236` ``` then show ?thesis ``` haftmann@66837 ` 237` ``` by (intro cring.field_intro2 cring) ``` haftmann@66837 ` 238` ``` (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq ac_simps) ``` lp15@65066 ` 239` ```qed ``` nipkow@31719 ` 240` nipkow@31719 ` 241` ```lemma res_prime_units_eq: "Units R = {1..p - 1}" ``` nipkow@31719 ` 242` ``` apply (subst res_units_eq) ``` haftmann@67051 ` 243` ``` apply (auto simp add: p_coprime_right_int zdvd_not_zless) ``` wenzelm@41541 ` 244` ``` done ``` nipkow@31719 ` 245` nipkow@31719 ` 246` ```end ``` nipkow@31719 ` 247` nipkow@31719 ` 248` ```sublocale residues_prime < field ``` nipkow@31719 ` 249` ``` by (rule is_field) ``` nipkow@31719 ` 250` nipkow@31719 ` 251` wenzelm@60527 ` 252` ```section \Test cases: Euler's theorem and Wilson's theorem\ ``` nipkow@31719 ` 253` wenzelm@60527 ` 254` ```subsection \Euler's theorem\ ``` nipkow@31719 ` 255` haftmann@67051 ` 256` ```lemma (in residues) totatives_eq: ``` haftmann@67051 ` 257` ``` "totatives (nat m) = nat ` Units R" ``` lp15@55261 ` 258` ```proof - ``` haftmann@67051 ` 259` ``` from m_gt_one have "\m\ > 1" ``` haftmann@67051 ` 260` ``` by simp ``` haftmann@67051 ` 261` ``` then have "totatives (nat \m\) = nat ` abs ` Units R" ``` haftmann@67051 ` 262` ``` by (auto simp add: totatives_def res_units_eq image_iff le_less) ``` haftmann@67051 ` 263` ``` (use m_gt_one zless_nat_eq_int_zless in force) ``` haftmann@67051 ` 264` ``` moreover have "\m\ = m" "abs ` Units R = Units R" ``` haftmann@67051 ` 265` ``` using m_gt_one by (auto simp add: res_units_eq image_iff) ``` haftmann@67051 ` 266` ``` ultimately show ?thesis ``` haftmann@67051 ` 267` ``` by simp ``` haftmann@67051 ` 268` ```qed ``` haftmann@67051 ` 269` haftmann@67051 ` 270` ```lemma (in residues) totient_eq: ``` haftmann@67051 ` 271` ``` "totient (nat m) = card (Units R)" ``` haftmann@67051 ` 272` ```proof - ``` haftmann@65465 ` 273` ``` have *: "inj_on nat (Units R)" ``` haftmann@65465 ` 274` ``` by (rule inj_onI) (auto simp add: res_units_eq) ``` haftmann@67051 ` 275` ``` then show ?thesis ``` haftmann@67051 ` 276` ``` by (simp add: totient_def totatives_eq card_image) ``` lp15@55261 ` 277` ```qed ``` lp15@55261 ` 278` haftmann@65465 ` 279` ```lemma (in residues_prime) totient_eq: "totient p = p - 1" ``` haftmann@65465 ` 280` ``` using totient_eq by (simp add: res_prime_units_eq) ``` nipkow@31719 ` 281` haftmann@65465 ` 282` ```lemma (in residues) euler_theorem: ``` haftmann@65465 ` 283` ``` assumes "coprime a m" ``` haftmann@65465 ` 284` ``` shows "[a ^ totient (nat m) = 1] (mod m)" ``` haftmann@65416 ` 285` ```proof - ``` haftmann@65465 ` 286` ``` have "a ^ totient (nat m) mod m = 1 mod m" ``` haftmann@65465 ` 287` ``` by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one) ``` lp15@65066 ` 288` ``` then show ?thesis ``` lp15@65066 ` 289` ``` using res_eq_to_cong by blast ``` nipkow@31719 ` 290` ```qed ``` nipkow@31719 ` 291` nipkow@31719 ` 292` ```lemma euler_theorem: ``` haftmann@65465 ` 293` ``` fixes a m :: nat ``` haftmann@65465 ` 294` ``` assumes "coprime a m" ``` haftmann@65465 ` 295` ``` shows "[a ^ totient m = 1] (mod m)" ``` wenzelm@67091 ` 296` ```proof (cases "m = 0 \ m = 1") ``` wenzelm@60527 ` 297` ``` case True ``` wenzelm@44872 ` 298` ``` then show ?thesis by auto ``` nipkow@31719 ` 299` ```next ``` wenzelm@60527 ` 300` ``` case False ``` wenzelm@41541 ` 301` ``` with assms show ?thesis ``` haftmann@66954 ` 302` ``` using residues.euler_theorem [of "int m" "int a"] cong_int_iff ``` haftmann@66954 ` 303` ``` by (auto simp add: residues_def gcd_int_def) fastforce ``` nipkow@31719 ` 304` ```qed ``` nipkow@31719 ` 305` nipkow@31719 ` 306` ```lemma fermat_theorem: ``` haftmann@65465 ` 307` ``` fixes p a :: nat ``` haftmann@65465 ` 308` ``` assumes "prime p" and "\ p dvd a" ``` haftmann@65465 ` 309` ``` shows "[a ^ (p - 1) = 1] (mod p)" ``` nipkow@31719 ` 310` ```proof - ``` haftmann@65465 ` 311` ``` from assms prime_imp_coprime [of p a] have "coprime a p" ``` haftmann@65465 ` 312` ``` by (auto simp add: ac_simps) ``` haftmann@65465 ` 313` ``` then have "[a ^ totient p = 1] (mod p)" ``` haftmann@65465 ` 314` ``` by (rule euler_theorem) ``` haftmann@65465 ` 315` ``` also have "totient p = p - 1" ``` eberlm@65726 ` 316` ``` by (rule totient_prime) (rule assms) ``` haftmann@65465 ` 317` ``` finally show ?thesis . ``` nipkow@31719 ` 318` ```qed ``` nipkow@31719 ` 319` nipkow@31719 ` 320` wenzelm@60526 ` 321` ```subsection \Wilson's theorem\ ``` nipkow@31719 ` 322` wenzelm@60527 ` 323` ```lemma (in field) inv_pair_lemma: "x \ Units R \ y \ Units R \ ``` wenzelm@60527 ` 324` ``` {x, inv x} \ {y, inv y} \ {x, inv x} \ {y, inv y} = {}" ``` nipkow@31719 ` 325` ``` apply auto ``` lp15@55352 ` 326` ``` apply (metis Units_inv_inv)+ ``` wenzelm@41541 ` 327` ``` done ``` nipkow@31719 ` 328` nipkow@31719 ` 329` ```lemma (in residues_prime) wilson_theorem1: ``` nipkow@31719 ` 330` ``` assumes a: "p > 2" ``` lp15@59730 ` 331` ``` shows "[fact (p - 1) = (-1::int)] (mod p)" ``` nipkow@31719 ` 332` ```proof - ``` wenzelm@60527 ` 333` ``` let ?Inverse_Pairs = "{{x, inv x}| x. x \ Units R - {\, \ \}}" ``` wenzelm@60527 ` 334` ``` have UR: "Units R = {\, \ \} \ \?Inverse_Pairs" ``` nipkow@31719 ` 335` ``` by auto ``` wenzelm@60527 ` 336` ``` have "(\i\Units R. i) = (\i\{\, \ \}. i) \ (\i\\?Inverse_Pairs. i)" ``` nipkow@31732 ` 337` ``` apply (subst UR) ``` nipkow@31719 ` 338` ``` apply (subst finprod_Un_disjoint) ``` wenzelm@66305 ` 339` ``` apply (auto intro: funcsetI) ``` wenzelm@60527 ` 340` ``` using inv_one apply auto[1] ``` wenzelm@60527 ` 341` ``` using inv_eq_neg_one_eq apply auto ``` nipkow@31719 ` 342` ``` done ``` wenzelm@60527 ` 343` ``` also have "(\i\{\, \ \}. i) = \ \" ``` nipkow@31719 ` 344` ``` apply (subst finprod_insert) ``` wenzelm@66305 ` 345` ``` apply auto ``` nipkow@31719 ` 346` ``` apply (frule one_eq_neg_one) ``` wenzelm@60527 ` 347` ``` using a apply force ``` nipkow@31719 ` 348` ``` done ``` wenzelm@60527 ` 349` ``` also have "(\i\(\?Inverse_Pairs). i) = (\A\?Inverse_Pairs. (\y\A. y))" ``` wenzelm@60527 ` 350` ``` apply (subst finprod_Union_disjoint) ``` wenzelm@66305 ` 351` ``` apply auto ``` wenzelm@66305 ` 352` ``` apply (metis Units_inv_inv)+ ``` nipkow@31719 ` 353` ``` done ``` nipkow@31719 ` 354` ``` also have "\ = \" ``` lp15@68447 ` 355` ``` apply (rule finprod_one_eqI) ``` wenzelm@66305 ` 356` ``` apply auto ``` wenzelm@60527 ` 357` ``` apply (subst finprod_insert) ``` wenzelm@66305 ` 358` ``` apply auto ``` lp15@55352 ` 359` ``` apply (metis inv_eq_self) ``` nipkow@31719 ` 360` ``` done ``` wenzelm@60527 ` 361` ``` finally have "(\i\Units R. i) = \ \" ``` nipkow@31719 ` 362` ``` by simp ``` wenzelm@60527 ` 363` ``` also have "(\i\Units R. i) = (\i\Units R. i mod p)" ``` lp15@65066 ` 364` ``` by (rule finprod_cong') (auto simp: res_units_eq) ``` wenzelm@60527 ` 365` ``` also have "\ = (\i\Units R. i) mod p" ``` lp15@65066 ` 366` ``` by (rule prod_cong) auto ``` nipkow@31719 ` 367` ``` also have "\ = fact (p - 1) mod p" ``` nipkow@64272 ` 368` ``` apply (simp add: fact_prod) ``` lp15@65066 ` 369` ``` using assms ``` lp15@55242 ` 370` ``` apply (subst res_prime_units_eq) ``` nipkow@64272 ` 371` ``` apply (simp add: int_prod zmod_int prod_int_eq) ``` nipkow@31719 ` 372` ``` done ``` wenzelm@60527 ` 373` ``` finally have "fact (p - 1) mod p = \ \" . ``` wenzelm@60527 ` 374` ``` then show ?thesis ``` haftmann@66888 ` 375` ``` by (simp add: cong_def res_neg_eq res_one_eq zmod_int) ``` nipkow@31719 ` 376` ```qed ``` nipkow@31719 ` 377` lp15@55352 ` 378` ```lemma wilson_theorem: ``` wenzelm@60527 ` 379` ``` assumes "prime p" ``` wenzelm@60527 ` 380` ``` shows "[fact (p - 1) = - 1] (mod p)" ``` lp15@55352 ` 381` ```proof (cases "p = 2") ``` lp15@59667 ` 382` ``` case True ``` lp15@55352 ` 383` ``` then show ?thesis ``` haftmann@66888 ` 384` ``` by (simp add: cong_def fact_prod) ``` lp15@55352 ` 385` ```next ``` lp15@55352 ` 386` ``` case False ``` lp15@55352 ` 387` ``` then show ?thesis ``` lp15@55352 ` 388` ``` using assms prime_ge_2_nat ``` lp15@55352 ` 389` ``` by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) ``` lp15@55352 ` 390` ```qed ``` nipkow@31719 ` 391` wenzelm@66304 ` 392` ```text \ ``` haftmann@65416 ` 393` ``` This result can be transferred to the multiplicative group of ``` wenzelm@66305 ` 394` ``` \\/p\\ for \p\ prime.\ ``` haftmann@65416 ` 395` haftmann@65416 ` 396` ```lemma mod_nat_int_pow_eq: ``` haftmann@65416 ` 397` ``` fixes n :: nat and p a :: int ``` wenzelm@66305 ` 398` ``` shows "a \ 0 \ p \ 0 \ (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)" ``` haftmann@65416 ` 399` ``` by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric]) ``` haftmann@65416 ` 400` haftmann@65416 ` 401` ```theorem residue_prime_mult_group_has_gen : ``` haftmann@65416 ` 402` ``` fixes p :: nat ``` haftmann@65416 ` 403` ``` assumes prime_p : "prime p" ``` haftmann@65416 ` 404` ``` shows "\a \ {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \ UNIV}" ``` haftmann@65416 ` 405` ```proof - ``` wenzelm@66305 ` 406` ``` have "p \ 2" ``` wenzelm@66305 ` 407` ``` using prime_gt_1_nat[OF prime_p] by simp ``` wenzelm@66305 ` 408` ``` interpret R: residues_prime p "residue_ring p" ``` wenzelm@66305 ` 409` ``` by (simp add: residues_prime_def prime_p) ``` wenzelm@66305 ` 410` ``` have car: "carrier (residue_ring (int p)) - {\\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}" ``` haftmann@65416 ` 411` ``` by (auto simp add: R.zero_cong R.res_carrier_eq) ``` wenzelm@66305 ` 412` nipkow@67341 ` 413` ``` have "x [^]\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" ``` wenzelm@66305 ` 414` ``` if "x \ {1 .. int p - 1}" for x and i :: nat ``` wenzelm@66305 ` 415` ``` using that R.pow_cong[of x i] by auto ``` wenzelm@66305 ` 416` ``` moreover ``` wenzelm@66305 ` 417` ``` obtain a where a: "a \ {1 .. int p - 1}" ``` nipkow@67341 ` 418` ``` and a_gen: "{1 .. int p - 1} = {a[^]\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \ UNIV}" ``` wenzelm@66305 ` 419` ``` using field.finite_field_mult_group_has_gen[OF R.is_field] ``` haftmann@65416 ` 420` ``` by (auto simp add: car[symmetric] carrier_mult_of) ``` wenzelm@66305 ` 421` ``` moreover ``` wenzelm@66305 ` 422` ``` have "nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R") ``` haftmann@65416 ` 423` ``` proof ``` wenzelm@66305 ` 424` ``` have "n \ ?R" if "n \ ?L" for n ``` wenzelm@66305 ` 425` ``` using that \p\2\ by force ``` wenzelm@66305 ` 426` ``` then show "?L \ ?R" by blast ``` wenzelm@66305 ` 427` ``` have "n \ ?L" if "n \ ?R" for n ``` haftmann@66837 ` 428` ``` using that \p\2\ by (auto intro: rev_image_eqI [of "int n"]) ``` wenzelm@66305 ` 429` ``` then show "?R \ ?L" by blast ``` haftmann@65416 ` 430` ``` qed ``` wenzelm@66305 ` 431` ``` moreover ``` haftmann@65416 ` 432` ``` have "nat ` {a^i mod (int p) | i::nat. i \ UNIV} = {nat a^i mod p | i . i \ UNIV}" (is "?L = ?R") ``` haftmann@65416 ` 433` ``` proof ``` wenzelm@66305 ` 434` ``` have "x \ ?R" if "x \ ?L" for x ``` wenzelm@66305 ` 435` ``` proof - ``` wenzelm@66305 ` 436` ``` from that obtain i where i: "x = nat (a^i mod (int p))" ``` wenzelm@66305 ` 437` ``` by blast ``` wenzelm@66305 ` 438` ``` then have "x = nat a ^ i mod p" ``` wenzelm@66305 ` 439` ``` using mod_nat_int_pow_eq[of a "int p" i] a \p\2\ by auto ``` wenzelm@66305 ` 440` ``` with i show ?thesis by blast ``` wenzelm@66305 ` 441` ``` qed ``` wenzelm@66305 ` 442` ``` then show "?L \ ?R" by blast ``` wenzelm@66305 ` 443` ``` have "x \ ?L" if "x \ ?R" for x ``` wenzelm@66305 ` 444` ``` proof - ``` wenzelm@66305 ` 445` ``` from that obtain i where i: "x = nat a^i mod p" ``` wenzelm@66305 ` 446` ``` by blast ``` wenzelm@66305 ` 447` ``` with mod_nat_int_pow_eq[of a "int p" i] a \p\2\ show ?thesis ``` wenzelm@66305 ` 448` ``` by auto ``` wenzelm@66305 ` 449` ``` qed ``` wenzelm@66305 ` 450` ``` then show "?R \ ?L" by blast ``` haftmann@65416 ` 451` ``` qed ``` wenzelm@66305 ` 452` ``` ultimately have "{1 .. p - 1} = {nat a^i mod p | i. i \ UNIV}" ``` wenzelm@66305 ` 453` ``` by presburger ``` wenzelm@66305 ` 454` ``` moreover from a have "nat a \ {1 .. p - 1}" by force ``` haftmann@65416 ` 455` ``` ultimately show ?thesis .. ``` haftmann@65416 ` 456` ```qed ``` haftmann@65416 ` 457` nipkow@31719 ` 458` ```end ```