src/HOL/Number_Theory/Residues.thy
 author eberlm Mon Oct 17 15:20:06 2016 +0200 (2016-10-17) changeset 64282 261d42f0bfac parent 64272 f76b6dda2e56 child 64593 50c715579715 permissions -rw-r--r--
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
 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 ``` eberlm@63537 ` 11` ```imports Cong MiscAlgebra ``` nipkow@31719 ` 12` ```begin ``` nipkow@31719 ` 13` eberlm@64282 ` 14` ```definition QuadRes :: "int \ int \ bool" where ``` eberlm@64282 ` 15` ``` "QuadRes p a = (\y. ([y^2 = a] (mod p)))" ``` eberlm@64282 ` 16` eberlm@64282 ` 17` ```definition Legendre :: "int \ int \ int" where ``` eberlm@64282 ` 18` ``` "Legendre a p = (if ([a = 0] (mod p)) then 0 ``` eberlm@64282 ` 19` ``` else if QuadRes p a then 1 ``` eberlm@64282 ` 20` ``` else -1)" ``` eberlm@64282 ` 21` wenzelm@60527 ` 22` ```subsection \A locale for residue rings\ ``` nipkow@31719 ` 23` wenzelm@60527 ` 24` ```definition residue_ring :: "int \ int ring" ``` wenzelm@60528 ` 25` ```where ``` wenzelm@60527 ` 26` ``` "residue_ring m = ``` wenzelm@60527 ` 27` ``` \carrier = {0..m - 1}, ``` wenzelm@60527 ` 28` ``` mult = \x y. (x * y) mod m, ``` wenzelm@60527 ` 29` ``` one = 1, ``` wenzelm@60527 ` 30` ``` zero = 0, ``` wenzelm@60527 ` 31` ``` add = \x y. (x + y) mod m\" ``` nipkow@31719 ` 32` nipkow@31719 ` 33` ```locale residues = ``` nipkow@31719 ` 34` ``` fixes m :: int and R (structure) ``` nipkow@31719 ` 35` ``` assumes m_gt_one: "m > 1" ``` wenzelm@60527 ` 36` ``` defines "R \ residue_ring m" ``` wenzelm@44872 ` 37` ```begin ``` nipkow@31719 ` 38` nipkow@31719 ` 39` ```lemma abelian_group: "abelian_group R" ``` nipkow@31719 ` 40` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 41` ``` apply (rule abelian_groupI) ``` nipkow@31719 ` 42` ``` apply (unfold R_def residue_ring_def) ``` haftmann@57514 ` 43` ``` apply (auto simp add: mod_add_right_eq [symmetric] ac_simps) ``` nipkow@31719 ` 44` ``` apply (case_tac "x = 0") ``` nipkow@31719 ` 45` ``` apply force ``` nipkow@31719 ` 46` ``` apply (subgoal_tac "(x + (m - x)) mod m = 0") ``` nipkow@31719 ` 47` ``` apply (erule bexI) ``` nipkow@31719 ` 48` ``` apply auto ``` wenzelm@41541 ` 49` ``` done ``` nipkow@31719 ` 50` nipkow@31719 ` 51` ```lemma comm_monoid: "comm_monoid R" ``` nipkow@31719 ` 52` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 53` ``` apply (unfold R_def residue_ring_def) ``` nipkow@31719 ` 54` ``` apply (rule comm_monoidI) ``` nipkow@31719 ` 55` ``` apply auto ``` nipkow@31719 ` 56` ``` apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") ``` nipkow@31719 ` 57` ``` apply (erule ssubst) ``` huffman@47163 ` 58` ``` apply (subst mod_mult_right_eq [symmetric])+ ``` haftmann@57514 ` 59` ``` apply (simp_all only: ac_simps) ``` wenzelm@41541 ` 60` ``` done ``` nipkow@31719 ` 61` nipkow@31719 ` 62` ```lemma cring: "cring R" ``` nipkow@31719 ` 63` ``` apply (rule cringI) ``` nipkow@31719 ` 64` ``` apply (rule abelian_group) ``` nipkow@31719 ` 65` ``` apply (rule comm_monoid) ``` nipkow@31719 ` 66` ``` apply (unfold R_def residue_ring_def, auto) ``` nipkow@31719 ` 67` ``` apply (subst mod_add_eq [symmetric]) ``` haftmann@57512 ` 68` ``` apply (subst mult.commute) ``` huffman@47163 ` 69` ``` apply (subst mod_mult_right_eq [symmetric]) ``` haftmann@36350 ` 70` ``` apply (simp add: field_simps) ``` wenzelm@41541 ` 71` ``` done ``` nipkow@31719 ` 72` nipkow@31719 ` 73` ```end ``` nipkow@31719 ` 74` nipkow@31719 ` 75` ```sublocale residues < cring ``` nipkow@31719 ` 76` ``` by (rule cring) ``` nipkow@31719 ` 77` nipkow@31719 ` 78` wenzelm@41541 ` 79` ```context residues ``` wenzelm@41541 ` 80` ```begin ``` nipkow@31719 ` 81` wenzelm@60527 ` 82` ```text \ ``` wenzelm@60527 ` 83` ``` These lemmas translate back and forth between internal and ``` wenzelm@60527 ` 84` ``` external concepts. ``` wenzelm@60527 ` 85` ```\ ``` nipkow@31719 ` 86` nipkow@31719 ` 87` ```lemma res_carrier_eq: "carrier R = {0..m - 1}" ``` wenzelm@44872 ` 88` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 89` nipkow@31719 ` 90` ```lemma res_add_eq: "x \ y = (x + y) mod m" ``` wenzelm@44872 ` 91` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 92` nipkow@31719 ` 93` ```lemma res_mult_eq: "x \ y = (x * y) mod m" ``` wenzelm@44872 ` 94` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 95` nipkow@31719 ` 96` ```lemma res_zero_eq: "\ = 0" ``` wenzelm@44872 ` 97` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 98` nipkow@31719 ` 99` ```lemma res_one_eq: "\ = 1" ``` wenzelm@44872 ` 100` ``` unfolding R_def residue_ring_def units_of_def by auto ``` nipkow@31719 ` 101` wenzelm@60527 ` 102` ```lemma res_units_eq: "Units R = {x. 0 < x \ x < m \ coprime x m}" ``` nipkow@31719 ` 103` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 104` ``` apply (unfold Units_def R_def residue_ring_def) ``` nipkow@31719 ` 105` ``` apply auto ``` wenzelm@60527 ` 106` ``` apply (subgoal_tac "x \ 0") ``` nipkow@31719 ` 107` ``` apply auto ``` lp15@55352 ` 108` ``` apply (metis invertible_coprime_int) ``` nipkow@31952 ` 109` ``` apply (subst (asm) coprime_iff_invertible'_int) ``` haftmann@57512 ` 110` ``` apply (auto simp add: cong_int_def mult.commute) ``` wenzelm@41541 ` 111` ``` done ``` nipkow@31719 ` 112` nipkow@31719 ` 113` ```lemma res_neg_eq: "\ x = (- x) mod m" ``` nipkow@31719 ` 114` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 115` ``` apply (unfold R_def a_inv_def m_inv_def residue_ring_def) ``` nipkow@31719 ` 116` ``` apply auto ``` nipkow@31719 ` 117` ``` apply (rule the_equality) ``` nipkow@31719 ` 118` ``` apply auto ``` nipkow@31719 ` 119` ``` apply (subst mod_add_right_eq [symmetric]) ``` nipkow@31719 ` 120` ``` apply auto ``` nipkow@31719 ` 121` ``` apply (subst mod_add_left_eq [symmetric]) ``` nipkow@31719 ` 122` ``` apply auto ``` nipkow@31719 ` 123` ``` apply (subgoal_tac "y mod m = - x mod m") ``` nipkow@31719 ` 124` ``` apply simp ``` haftmann@57512 ` 125` ``` apply (metis minus_add_cancel mod_mult_self1 mult.commute) ``` wenzelm@41541 ` 126` ``` done ``` nipkow@31719 ` 127` wenzelm@44872 ` 128` ```lemma finite [iff]: "finite (carrier R)" ``` wenzelm@60527 ` 129` ``` by (subst res_carrier_eq) auto ``` nipkow@31719 ` 130` wenzelm@44872 ` 131` ```lemma finite_Units [iff]: "finite (Units R)" ``` bulwahn@50027 ` 132` ``` by (subst res_units_eq) auto ``` nipkow@31719 ` 133` wenzelm@60527 ` 134` ```text \ ``` wenzelm@63167 ` 135` ``` The function \a \ a mod m\ maps the integers to the ``` wenzelm@60527 ` 136` ``` residue classes. The following lemmas show that this mapping ``` wenzelm@60527 ` 137` ``` respects addition and multiplication on the integers. ``` wenzelm@60527 ` 138` ```\ ``` nipkow@31719 ` 139` wenzelm@60527 ` 140` ```lemma mod_in_carrier [iff]: "a mod m \ carrier R" ``` wenzelm@60527 ` 141` ``` unfolding res_carrier_eq ``` wenzelm@60527 ` 142` ``` using insert m_gt_one by auto ``` nipkow@31719 ` 143` nipkow@31719 ` 144` ```lemma add_cong: "(x mod m) \ (y mod m) = (x + y) mod m" ``` wenzelm@44872 ` 145` ``` unfolding R_def residue_ring_def ``` wenzelm@44872 ` 146` ``` apply auto ``` wenzelm@44872 ` 147` ``` apply presburger ``` wenzelm@44872 ` 148` ``` done ``` nipkow@31719 ` 149` nipkow@31719 ` 150` ```lemma mult_cong: "(x mod m) \ (y mod m) = (x * y) mod m" ``` lp15@55352 ` 151` ``` unfolding R_def residue_ring_def ``` lp15@55352 ` 152` ``` by auto (metis mod_mult_eq) ``` nipkow@31719 ` 153` nipkow@31719 ` 154` ```lemma zero_cong: "\ = 0" ``` wenzelm@44872 ` 155` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 156` nipkow@31719 ` 157` ```lemma one_cong: "\ = 1 mod m" ``` wenzelm@44872 ` 158` ``` using m_gt_one unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 159` wenzelm@60527 ` 160` ```(* FIXME revise algebra library to use 1? *) ``` nipkow@31719 ` 161` ```lemma pow_cong: "(x mod m) (^) n = x^n mod m" ``` nipkow@31719 ` 162` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 163` ``` apply (induct n) ``` wenzelm@41541 ` 164` ``` apply (auto simp add: nat_pow_def one_cong) ``` haftmann@57512 ` 165` ``` apply (metis mult.commute mult_cong) ``` wenzelm@41541 ` 166` ``` done ``` nipkow@31719 ` 167` nipkow@31719 ` 168` ```lemma neg_cong: "\ (x mod m) = (- x) mod m" ``` lp15@55352 ` 169` ``` by (metis mod_minus_eq res_neg_eq) ``` nipkow@31719 ` 170` wenzelm@60528 ` 171` ```lemma (in residues) prod_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 172` ``` by (induct set: finite) (auto simp: one_cong mult_cong) ``` nipkow@31719 ` 173` wenzelm@60528 ` 174` ```lemma (in residues) sum_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 175` ``` by (induct set: finite) (auto simp: zero_cong add_cong) ``` nipkow@31719 ` 176` haftmann@60688 ` 177` ```lemma mod_in_res_units [simp]: ``` haftmann@60688 ` 178` ``` assumes "1 < m" and "coprime a m" ``` haftmann@60688 ` 179` ``` shows "a mod m \ Units R" ``` haftmann@60688 ` 180` ```proof (cases "a mod m = 0") ``` haftmann@60688 ` 181` ``` case True with assms show ?thesis ``` haftmann@60688 ` 182` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric]) ``` haftmann@60688 ` 183` ```next ``` haftmann@60688 ` 184` ``` case False ``` haftmann@60688 ` 185` ``` from assms have "0 < m" by simp ``` haftmann@60688 ` 186` ``` with pos_mod_sign [of m a] have "0 \ a mod m" . ``` haftmann@60688 ` 187` ``` with False have "0 < a mod m" by simp ``` haftmann@60688 ` 188` ``` with assms show ?thesis ``` haftmann@60688 ` 189` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps) ``` haftmann@60688 ` 190` ```qed ``` nipkow@31719 ` 191` wenzelm@60528 ` 192` ```lemma res_eq_to_cong: "(a mod m) = (b mod m) \ [a = b] (mod m)" ``` nipkow@31719 ` 193` ``` unfolding cong_int_def by auto ``` nipkow@31719 ` 194` nipkow@31719 ` 195` wenzelm@60528 ` 196` ```text \Simplifying with these will translate a ring equation in R to a congruence.\ ``` nipkow@31719 ` 197` ```lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong ``` nipkow@31719 ` 198` ``` prod_cong sum_cong neg_cong res_eq_to_cong ``` nipkow@31719 ` 199` wenzelm@60527 ` 200` ```text \Other useful facts about the residue ring.\ ``` nipkow@31719 ` 201` ```lemma one_eq_neg_one: "\ = \ \ \ m = 2" ``` nipkow@31719 ` 202` ``` apply (simp add: res_one_eq res_neg_eq) ``` haftmann@57512 ` 203` ``` apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff ``` wenzelm@60528 ` 204` ``` zero_neq_one zmod_zminus1_eq_if) ``` wenzelm@41541 ` 205` ``` done ``` nipkow@31719 ` 206` nipkow@31719 ` 207` ```end ``` nipkow@31719 ` 208` nipkow@31719 ` 209` wenzelm@60527 ` 210` ```subsection \Prime residues\ ``` nipkow@31719 ` 211` nipkow@31719 ` 212` ```locale residues_prime = ``` eberlm@63534 ` 213` ``` fixes p :: nat and R (structure) ``` nipkow@31719 ` 214` ``` assumes p_prime [intro]: "prime p" ``` eberlm@63534 ` 215` ``` defines "R \ residue_ring (int p)" ``` nipkow@31719 ` 216` nipkow@31719 ` 217` ```sublocale residues_prime < residues p ``` nipkow@31719 ` 218` ``` apply (unfold R_def residues_def) ``` nipkow@31719 ` 219` ``` using p_prime apply auto ``` haftmann@62348 ` 220` ``` apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) ``` wenzelm@41541 ` 221` ``` done ``` nipkow@31719 ` 222` wenzelm@44872 ` 223` ```context residues_prime ``` wenzelm@44872 ` 224` ```begin ``` nipkow@31719 ` 225` nipkow@31719 ` 226` ```lemma is_field: "field R" ``` nipkow@31719 ` 227` ``` apply (rule cring.field_intro2) ``` nipkow@31719 ` 228` ``` apply (rule cring) ``` wenzelm@44872 ` 229` ``` apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) ``` nipkow@31719 ` 230` ``` apply (rule classical) ``` nipkow@31719 ` 231` ``` apply (erule notE) ``` haftmann@62348 ` 232` ``` apply (subst gcd.commute) ``` nipkow@31952 ` 233` ``` apply (rule prime_imp_coprime_int) ``` eberlm@63534 ` 234` ``` apply (simp add: p_prime) ``` nipkow@31719 ` 235` ``` apply (rule notI) ``` nipkow@31719 ` 236` ``` apply (frule zdvd_imp_le) ``` nipkow@31719 ` 237` ``` apply auto ``` wenzelm@41541 ` 238` ``` done ``` nipkow@31719 ` 239` nipkow@31719 ` 240` ```lemma res_prime_units_eq: "Units R = {1..p - 1}" ``` nipkow@31719 ` 241` ``` apply (subst res_units_eq) ``` nipkow@31719 ` 242` ``` apply auto ``` haftmann@62348 ` 243` ``` apply (subst gcd.commute) ``` lp15@55352 ` 244` ``` apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) ``` wenzelm@41541 ` 245` ``` done ``` nipkow@31719 ` 246` nipkow@31719 ` 247` ```end ``` nipkow@31719 ` 248` nipkow@31719 ` 249` ```sublocale residues_prime < field ``` nipkow@31719 ` 250` ``` by (rule is_field) ``` nipkow@31719 ` 251` nipkow@31719 ` 252` wenzelm@60527 ` 253` ```section \Test cases: Euler's theorem and Wilson's theorem\ ``` nipkow@31719 ` 254` wenzelm@60527 ` 255` ```subsection \Euler's theorem\ ``` nipkow@31719 ` 256` wenzelm@60527 ` 257` ```text \The definition of the phi function.\ ``` nipkow@31719 ` 258` wenzelm@60527 ` 259` ```definition phi :: "int \ nat" ``` wenzelm@60527 ` 260` ``` where "phi m = card {x. 0 < x \ x < m \ gcd x m = 1}" ``` nipkow@31719 ` 261` wenzelm@60527 ` 262` ```lemma phi_def_nat: "phi m = card {x. 0 < x \ x < nat m \ gcd x (nat m) = 1}" ``` lp15@55261 ` 263` ``` apply (simp add: phi_def) ``` lp15@55261 ` 264` ``` apply (rule bij_betw_same_card [of nat]) ``` lp15@55261 ` 265` ``` apply (auto simp add: inj_on_def bij_betw_def image_def) ``` lp15@55261 ` 266` ``` apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) ``` haftmann@62348 ` 267` ``` apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int ``` haftmann@62348 ` 268` ``` transfer_int_nat_gcd(1) of_nat_less_iff) ``` lp15@55261 ` 269` ``` done ``` lp15@55261 ` 270` lp15@55261 ` 271` ```lemma prime_phi: ``` wenzelm@60527 ` 272` ``` assumes "2 \ p" "phi p = p - 1" ``` wenzelm@60527 ` 273` ``` shows "prime p" ``` lp15@55261 ` 274` ```proof - ``` wenzelm@60528 ` 275` ``` have *: "{x. 0 < x \ x < p \ coprime x p} = {1..p - 1}" ``` lp15@55261 ` 276` ``` using assms unfolding phi_def_nat ``` lp15@55261 ` 277` ``` by (intro card_seteq) fastforce+ ``` wenzelm@60528 ` 278` ``` have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat ``` wenzelm@60527 ` 279` ``` proof - ``` wenzelm@60528 ` 280` ``` from * have cop: "x \ {1..p - 1} \ coprime x p" ``` wenzelm@60528 ` 281` ``` by blast ``` lp15@59667 ` 282` ``` have "coprime x p" ``` lp15@55261 ` 283` ``` apply (rule cop) ``` wenzelm@60528 ` 284` ``` using ** apply auto ``` lp15@55261 ` 285` ``` done ``` wenzelm@60527 ` 286` ``` with \x dvd p\ \1 < x\ show ?thesis ``` wenzelm@60527 ` 287` ``` by auto ``` wenzelm@60527 ` 288` ``` qed ``` lp15@59667 ` 289` ``` then show ?thesis ``` wenzelm@60526 ` 290` ``` using \2 \ p\ ``` eberlm@63633 ` 291` ``` by (simp add: prime_nat_iff) ``` lp15@59667 ` 292` ``` (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 ``` lp15@55352 ` 293` ``` not_numeral_le_zero one_dvd) ``` lp15@55261 ` 294` ```qed ``` lp15@55261 ` 295` nipkow@31719 ` 296` ```lemma phi_zero [simp]: "phi 0 = 0" ``` wenzelm@60527 ` 297` ``` unfolding phi_def ``` wenzelm@44872 ` 298` ```(* Auto hangs here. Once again, where is the simplification rule ``` wenzelm@60527 ` 299` ``` 1 \ Suc 0 coming from? *) ``` nipkow@31719 ` 300` ``` apply (auto simp add: card_eq_0_iff) ``` nipkow@31719 ` 301` ```(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) ``` wenzelm@41541 ` 302` ``` done ``` nipkow@31719 ` 303` nipkow@31719 ` 304` ```lemma phi_one [simp]: "phi 1 = 0" ``` wenzelm@44872 ` 305` ``` by (auto simp add: phi_def card_eq_0_iff) ``` nipkow@31719 ` 306` wenzelm@60527 ` 307` ```lemma (in residues) phi_eq: "phi m = card (Units R)" ``` nipkow@31719 ` 308` ``` by (simp add: phi_def res_units_eq) ``` nipkow@31719 ` 309` wenzelm@44872 ` 310` ```lemma (in residues) euler_theorem1: ``` nipkow@31719 ` 311` ``` assumes a: "gcd a m = 1" ``` nipkow@31719 ` 312` ``` shows "[a^phi m = 1] (mod m)" ``` nipkow@31719 ` 313` ```proof - ``` wenzelm@60527 ` 314` ``` from a m_gt_one have [simp]: "a mod m \ Units R" ``` nipkow@31719 ` 315` ``` by (intro mod_in_res_units) ``` nipkow@31719 ` 316` ``` from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" ``` nipkow@31719 ` 317` ``` by simp ``` wenzelm@44872 ` 318` ``` also have "\ = \" ``` wenzelm@60527 ` 319` ``` by (intro units_power_order_eq_one) auto ``` nipkow@31719 ` 320` ``` finally show ?thesis ``` nipkow@31719 ` 321` ``` by (simp add: res_to_cong_simps) ``` nipkow@31719 ` 322` ```qed ``` nipkow@31719 ` 323` nipkow@31719 ` 324` ```(* In fact, there is a two line proof! ``` nipkow@31719 ` 325` wenzelm@44872 ` 326` ```lemma (in residues) euler_theorem1: ``` nipkow@31719 ` 327` ``` assumes a: "gcd a m = 1" ``` nipkow@31719 ` 328` ``` shows "[a^phi m = 1] (mod m)" ``` nipkow@31719 ` 329` ```proof - ``` nipkow@31719 ` 330` ``` have "(a mod m) (^) (phi m) = \" ``` nipkow@31719 ` 331` ``` by (simp add: phi_eq units_power_order_eq_one a m_gt_one) ``` wenzelm@44872 ` 332` ``` then show ?thesis ``` nipkow@31719 ` 333` ``` by (simp add: res_to_cong_simps) ``` nipkow@31719 ` 334` ```qed ``` nipkow@31719 ` 335` nipkow@31719 ` 336` ```*) ``` nipkow@31719 ` 337` wenzelm@63167 ` 338` ```text \Outside the locale, we can relax the restriction \m > 1\.\ ``` nipkow@31719 ` 339` ```lemma euler_theorem: ``` wenzelm@60527 ` 340` ``` assumes "m \ 0" ``` wenzelm@60527 ` 341` ``` and "gcd a m = 1" ``` nipkow@31719 ` 342` ``` shows "[a^phi m = 1] (mod m)" ``` wenzelm@60527 ` 343` ```proof (cases "m = 0 | m = 1") ``` wenzelm@60527 ` 344` ``` case True ``` wenzelm@44872 ` 345` ``` then show ?thesis by auto ``` nipkow@31719 ` 346` ```next ``` wenzelm@60527 ` 347` ``` case False ``` wenzelm@41541 ` 348` ``` with assms show ?thesis ``` nipkow@31719 ` 349` ``` by (intro residues.euler_theorem1, unfold residues_def, auto) ``` nipkow@31719 ` 350` ```qed ``` nipkow@31719 ` 351` wenzelm@60527 ` 352` ```lemma (in residues_prime) phi_prime: "phi p = nat p - 1" ``` nipkow@31719 ` 353` ``` apply (subst phi_eq) ``` nipkow@31719 ` 354` ``` apply (subst res_prime_units_eq) ``` nipkow@31719 ` 355` ``` apply auto ``` wenzelm@41541 ` 356` ``` done ``` nipkow@31719 ` 357` eberlm@63534 ` 358` ```lemma phi_prime: "prime (int p) \ phi p = nat p - 1" ``` nipkow@31719 ` 359` ``` apply (rule residues_prime.phi_prime) ``` eberlm@63534 ` 360` ``` apply simp ``` nipkow@31719 ` 361` ``` apply (erule residues_prime.intro) ``` wenzelm@41541 ` 362` ``` done ``` nipkow@31719 ` 363` nipkow@31719 ` 364` ```lemma fermat_theorem: ``` wenzelm@60527 ` 365` ``` fixes a :: int ``` eberlm@63534 ` 366` ``` assumes "prime (int p)" ``` wenzelm@60527 ` 367` ``` and "\ p dvd a" ``` lp15@55242 ` 368` ``` shows "[a^(p - 1) = 1] (mod p)" ``` nipkow@31719 ` 369` ```proof - ``` wenzelm@60527 ` 370` ``` from assms have "[a ^ phi p = 1] (mod p)" ``` eberlm@63534 ` 371` ``` by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p] ``` eberlm@63534 ` 372` ``` simp: gcd.commute[of _ "int p"]) ``` nipkow@31719 ` 373` ``` also have "phi p = nat p - 1" ``` wenzelm@60527 ` 374` ``` by (rule phi_prime) (rule assms) ``` lp15@55242 ` 375` ``` finally show ?thesis ``` lp15@59667 ` 376` ``` by (metis nat_int) ``` nipkow@31719 ` 377` ```qed ``` nipkow@31719 ` 378` lp15@55227 ` 379` ```lemma fermat_theorem_nat: ``` eberlm@63534 ` 380` ``` assumes "prime (int p)" and "\ p dvd a" ``` wenzelm@60527 ` 381` ``` shows "[a ^ (p - 1) = 1] (mod p)" ``` wenzelm@60527 ` 382` ``` using fermat_theorem [of p a] assms ``` haftmann@62348 ` 383` ``` by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int) ``` lp15@55227 ` 384` nipkow@31719 ` 385` wenzelm@60526 ` 386` ```subsection \Wilson's theorem\ ``` nipkow@31719 ` 387` wenzelm@60527 ` 388` ```lemma (in field) inv_pair_lemma: "x \ Units R \ y \ Units R \ ``` wenzelm@60527 ` 389` ``` {x, inv x} \ {y, inv y} \ {x, inv x} \ {y, inv y} = {}" ``` nipkow@31719 ` 390` ``` apply auto ``` lp15@55352 ` 391` ``` apply (metis Units_inv_inv)+ ``` wenzelm@41541 ` 392` ``` done ``` nipkow@31719 ` 393` nipkow@31719 ` 394` ```lemma (in residues_prime) wilson_theorem1: ``` nipkow@31719 ` 395` ``` assumes a: "p > 2" ``` lp15@59730 ` 396` ``` shows "[fact (p - 1) = (-1::int)] (mod p)" ``` nipkow@31719 ` 397` ```proof - ``` wenzelm@60527 ` 398` ``` let ?Inverse_Pairs = "{{x, inv x}| x. x \ Units R - {\, \ \}}" ``` wenzelm@60527 ` 399` ``` have UR: "Units R = {\, \ \} \ \?Inverse_Pairs" ``` nipkow@31719 ` 400` ``` by auto ``` wenzelm@60527 ` 401` ``` have "(\i\Units R. i) = (\i\{\, \ \}. i) \ (\i\\?Inverse_Pairs. i)" ``` nipkow@31732 ` 402` ``` apply (subst UR) ``` nipkow@31719 ` 403` ``` apply (subst finprod_Un_disjoint) ``` lp15@55352 ` 404` ``` apply (auto intro: funcsetI) ``` wenzelm@60527 ` 405` ``` using inv_one apply auto[1] ``` wenzelm@60527 ` 406` ``` using inv_eq_neg_one_eq apply auto ``` nipkow@31719 ` 407` ``` done ``` wenzelm@60527 ` 408` ``` also have "(\i\{\, \ \}. i) = \ \" ``` nipkow@31719 ` 409` ``` apply (subst finprod_insert) ``` nipkow@31719 ` 410` ``` apply auto ``` nipkow@31719 ` 411` ``` apply (frule one_eq_neg_one) ``` wenzelm@60527 ` 412` ``` using a apply force ``` nipkow@31719 ` 413` ``` done ``` wenzelm@60527 ` 414` ``` also have "(\i\(\?Inverse_Pairs). i) = (\A\?Inverse_Pairs. (\y\A. y))" ``` wenzelm@60527 ` 415` ``` apply (subst finprod_Union_disjoint) ``` wenzelm@60527 ` 416` ``` apply auto ``` lp15@55352 ` 417` ``` apply (metis Units_inv_inv)+ ``` nipkow@31719 ` 418` ``` done ``` nipkow@31719 ` 419` ``` also have "\ = \" ``` wenzelm@60527 ` 420` ``` apply (rule finprod_one) ``` wenzelm@60527 ` 421` ``` apply auto ``` wenzelm@60527 ` 422` ``` apply (subst finprod_insert) ``` wenzelm@60527 ` 423` ``` apply auto ``` lp15@55352 ` 424` ``` apply (metis inv_eq_self) ``` nipkow@31719 ` 425` ``` done ``` wenzelm@60527 ` 426` ``` finally have "(\i\Units R. i) = \ \" ``` nipkow@31719 ` 427` ``` by simp ``` wenzelm@60527 ` 428` ``` also have "(\i\Units R. i) = (\i\Units R. i mod p)" ``` nipkow@31719 ` 429` ``` apply (rule finprod_cong') ``` wenzelm@60527 ` 430` ``` apply auto ``` nipkow@31719 ` 431` ``` apply (subst (asm) res_prime_units_eq) ``` nipkow@31719 ` 432` ``` apply auto ``` nipkow@31719 ` 433` ``` done ``` wenzelm@60527 ` 434` ``` also have "\ = (\i\Units R. i) mod p" ``` nipkow@31719 ` 435` ``` apply (rule prod_cong) ``` nipkow@31719 ` 436` ``` apply auto ``` nipkow@31719 ` 437` ``` done ``` nipkow@31719 ` 438` ``` also have "\ = fact (p - 1) mod p" ``` nipkow@64272 ` 439` ``` apply (simp add: fact_prod) ``` lp15@55242 ` 440` ``` apply (insert assms) ``` lp15@55242 ` 441` ``` apply (subst res_prime_units_eq) ``` nipkow@64272 ` 442` ``` apply (simp add: int_prod zmod_int prod_int_eq) ``` nipkow@31719 ` 443` ``` done ``` wenzelm@60527 ` 444` ``` finally have "fact (p - 1) mod p = \ \" . ``` wenzelm@60527 ` 445` ``` then show ?thesis ``` wenzelm@60528 ` 446` ``` by (metis of_nat_fact Divides.transfer_int_nat_functions(2) ``` wenzelm@60528 ` 447` ``` cong_int_def res_neg_eq res_one_eq) ``` nipkow@31719 ` 448` ```qed ``` nipkow@31719 ` 449` lp15@55352 ` 450` ```lemma wilson_theorem: ``` wenzelm@60527 ` 451` ``` assumes "prime p" ``` wenzelm@60527 ` 452` ``` shows "[fact (p - 1) = - 1] (mod p)" ``` lp15@55352 ` 453` ```proof (cases "p = 2") ``` lp15@59667 ` 454` ``` case True ``` lp15@55352 ` 455` ``` then show ?thesis ``` nipkow@64272 ` 456` ``` by (simp add: cong_int_def fact_prod) ``` lp15@55352 ` 457` ```next ``` lp15@55352 ` 458` ``` case False ``` lp15@55352 ` 459` ``` then show ?thesis ``` lp15@55352 ` 460` ``` using assms prime_ge_2_nat ``` lp15@55352 ` 461` ``` by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) ``` lp15@55352 ` 462` ```qed ``` nipkow@31719 ` 463` nipkow@31719 ` 464` ```end ```