src/HOL/Number_Theory/Residues.thy
 author haftmann Sat Dec 17 15:22:14 2016 +0100 (2016-12-17) changeset 64593 50c715579715 parent 64282 261d42f0bfac child 65066 c64d778a593a permissions -rw-r--r--
reoriented congruence rules in non-explosive direction
 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@64593 ` 43` ``` apply (auto simp add: mod_add_right_eq 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) ``` haftmann@64593 ` 58` ``` apply (subst mod_mult_right_eq)+ ``` 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) ``` haftmann@64593 ` 67` ``` apply (subst mod_add_eq) ``` haftmann@57512 ` 68` ``` apply (subst mult.commute) ``` haftmann@64593 ` 69` ``` apply (subst mod_mult_right_eq) ``` 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 ``` haftmann@64593 ` 119` ``` apply (subst mod_add_right_eq) ``` nipkow@31719 ` 120` ``` apply auto ``` haftmann@64593 ` 121` ``` apply (subst mod_add_left_eq) ``` 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 ``` haftmann@64593 ` 146` ``` by (auto simp add: mod_simps) ``` nipkow@31719 ` 147` nipkow@31719 ` 148` ```lemma mult_cong: "(x mod m) \ (y mod m) = (x * y) mod m" ``` lp15@55352 ` 149` ``` unfolding R_def residue_ring_def ``` haftmann@64593 ` 150` ``` by (auto simp add: mod_simps) ``` nipkow@31719 ` 151` nipkow@31719 ` 152` ```lemma zero_cong: "\ = 0" ``` wenzelm@44872 ` 153` ``` unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 154` nipkow@31719 ` 155` ```lemma one_cong: "\ = 1 mod m" ``` wenzelm@44872 ` 156` ``` using m_gt_one unfolding R_def residue_ring_def by auto ``` nipkow@31719 ` 157` wenzelm@60527 ` 158` ```(* FIXME revise algebra library to use 1? *) ``` nipkow@31719 ` 159` ```lemma pow_cong: "(x mod m) (^) n = x^n mod m" ``` nipkow@31719 ` 160` ``` apply (insert m_gt_one) ``` nipkow@31719 ` 161` ``` apply (induct n) ``` wenzelm@41541 ` 162` ``` apply (auto simp add: nat_pow_def one_cong) ``` haftmann@57512 ` 163` ``` apply (metis mult.commute mult_cong) ``` wenzelm@41541 ` 164` ``` done ``` nipkow@31719 ` 165` nipkow@31719 ` 166` ```lemma neg_cong: "\ (x mod m) = (- x) mod m" ``` lp15@55352 ` 167` ``` by (metis mod_minus_eq res_neg_eq) ``` nipkow@31719 ` 168` wenzelm@60528 ` 169` ```lemma (in residues) prod_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 170` ``` by (induct set: finite) (auto simp: one_cong mult_cong) ``` nipkow@31719 ` 171` wenzelm@60528 ` 172` ```lemma (in residues) sum_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m" ``` lp15@55352 ` 173` ``` by (induct set: finite) (auto simp: zero_cong add_cong) ``` nipkow@31719 ` 174` haftmann@60688 ` 175` ```lemma mod_in_res_units [simp]: ``` haftmann@60688 ` 176` ``` assumes "1 < m" and "coprime a m" ``` haftmann@60688 ` 177` ``` shows "a mod m \ Units R" ``` haftmann@60688 ` 178` ```proof (cases "a mod m = 0") ``` haftmann@60688 ` 179` ``` case True with assms show ?thesis ``` haftmann@60688 ` 180` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric]) ``` haftmann@60688 ` 181` ```next ``` haftmann@60688 ` 182` ``` case False ``` haftmann@60688 ` 183` ``` from assms have "0 < m" by simp ``` haftmann@60688 ` 184` ``` with pos_mod_sign [of m a] have "0 \ a mod m" . ``` haftmann@60688 ` 185` ``` with False have "0 < a mod m" by simp ``` haftmann@60688 ` 186` ``` with assms show ?thesis ``` haftmann@60688 ` 187` ``` by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps) ``` haftmann@60688 ` 188` ```qed ``` nipkow@31719 ` 189` wenzelm@60528 ` 190` ```lemma res_eq_to_cong: "(a mod m) = (b mod m) \ [a = b] (mod m)" ``` nipkow@31719 ` 191` ``` unfolding cong_int_def by auto ``` nipkow@31719 ` 192` nipkow@31719 ` 193` wenzelm@60528 ` 194` ```text \Simplifying with these will translate a ring equation in R to a congruence.\ ``` nipkow@31719 ` 195` ```lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong ``` nipkow@31719 ` 196` ``` prod_cong sum_cong neg_cong res_eq_to_cong ``` nipkow@31719 ` 197` wenzelm@60527 ` 198` ```text \Other useful facts about the residue ring.\ ``` nipkow@31719 ` 199` ```lemma one_eq_neg_one: "\ = \ \ \ m = 2" ``` nipkow@31719 ` 200` ``` apply (simp add: res_one_eq res_neg_eq) ``` haftmann@57512 ` 201` ``` apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff ``` wenzelm@60528 ` 202` ``` zero_neq_one zmod_zminus1_eq_if) ``` wenzelm@41541 ` 203` ``` done ``` nipkow@31719 ` 204` nipkow@31719 ` 205` ```end ``` nipkow@31719 ` 206` nipkow@31719 ` 207` wenzelm@60527 ` 208` ```subsection \Prime residues\ ``` nipkow@31719 ` 209` nipkow@31719 ` 210` ```locale residues_prime = ``` eberlm@63534 ` 211` ``` fixes p :: nat and R (structure) ``` nipkow@31719 ` 212` ``` assumes p_prime [intro]: "prime p" ``` eberlm@63534 ` 213` ``` defines "R \ residue_ring (int p)" ``` nipkow@31719 ` 214` nipkow@31719 ` 215` ```sublocale residues_prime < residues p ``` nipkow@31719 ` 216` ``` apply (unfold R_def residues_def) ``` nipkow@31719 ` 217` ``` using p_prime apply auto ``` haftmann@62348 ` 218` ``` apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) ``` wenzelm@41541 ` 219` ``` done ``` nipkow@31719 ` 220` wenzelm@44872 ` 221` ```context residues_prime ``` wenzelm@44872 ` 222` ```begin ``` nipkow@31719 ` 223` nipkow@31719 ` 224` ```lemma is_field: "field R" ``` nipkow@31719 ` 225` ``` apply (rule cring.field_intro2) ``` nipkow@31719 ` 226` ``` apply (rule cring) ``` wenzelm@44872 ` 227` ``` apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) ``` nipkow@31719 ` 228` ``` apply (rule classical) ``` nipkow@31719 ` 229` ``` apply (erule notE) ``` haftmann@62348 ` 230` ``` apply (subst gcd.commute) ``` nipkow@31952 ` 231` ``` apply (rule prime_imp_coprime_int) ``` eberlm@63534 ` 232` ``` apply (simp add: p_prime) ``` nipkow@31719 ` 233` ``` apply (rule notI) ``` nipkow@31719 ` 234` ``` apply (frule zdvd_imp_le) ``` nipkow@31719 ` 235` ``` apply auto ``` wenzelm@41541 ` 236` ``` done ``` nipkow@31719 ` 237` nipkow@31719 ` 238` ```lemma res_prime_units_eq: "Units R = {1..p - 1}" ``` nipkow@31719 ` 239` ``` apply (subst res_units_eq) ``` nipkow@31719 ` 240` ``` apply auto ``` haftmann@62348 ` 241` ``` apply (subst gcd.commute) ``` lp15@55352 ` 242` ``` apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) ``` wenzelm@41541 ` 243` ``` done ``` nipkow@31719 ` 244` nipkow@31719 ` 245` ```end ``` nipkow@31719 ` 246` nipkow@31719 ` 247` ```sublocale residues_prime < field ``` nipkow@31719 ` 248` ``` by (rule is_field) ``` nipkow@31719 ` 249` nipkow@31719 ` 250` wenzelm@60527 ` 251` ```section \Test cases: Euler's theorem and Wilson's theorem\ ``` nipkow@31719 ` 252` wenzelm@60527 ` 253` ```subsection \Euler's theorem\ ``` nipkow@31719 ` 254` wenzelm@60527 ` 255` ```text \The definition of the phi function.\ ``` nipkow@31719 ` 256` wenzelm@60527 ` 257` ```definition phi :: "int \ nat" ``` wenzelm@60527 ` 258` ``` where "phi m = card {x. 0 < x \ x < m \ gcd x m = 1}" ``` nipkow@31719 ` 259` wenzelm@60527 ` 260` ```lemma phi_def_nat: "phi m = card {x. 0 < x \ x < nat m \ gcd x (nat m) = 1}" ``` lp15@55261 ` 261` ``` apply (simp add: phi_def) ``` lp15@55261 ` 262` ``` apply (rule bij_betw_same_card [of nat]) ``` lp15@55261 ` 263` ``` apply (auto simp add: inj_on_def bij_betw_def image_def) ``` lp15@55261 ` 264` ``` apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) ``` haftmann@62348 ` 265` ``` apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int ``` haftmann@62348 ` 266` ``` transfer_int_nat_gcd(1) of_nat_less_iff) ``` lp15@55261 ` 267` ``` done ``` lp15@55261 ` 268` lp15@55261 ` 269` ```lemma prime_phi: ``` wenzelm@60527 ` 270` ``` assumes "2 \ p" "phi p = p - 1" ``` wenzelm@60527 ` 271` ``` shows "prime p" ``` lp15@55261 ` 272` ```proof - ``` wenzelm@60528 ` 273` ``` have *: "{x. 0 < x \ x < p \ coprime x p} = {1..p - 1}" ``` lp15@55261 ` 274` ``` using assms unfolding phi_def_nat ``` lp15@55261 ` 275` ``` by (intro card_seteq) fastforce+ ``` wenzelm@60528 ` 276` ``` have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat ``` wenzelm@60527 ` 277` ``` proof - ``` wenzelm@60528 ` 278` ``` from * have cop: "x \ {1..p - 1} \ coprime x p" ``` wenzelm@60528 ` 279` ``` by blast ``` lp15@59667 ` 280` ``` have "coprime x p" ``` lp15@55261 ` 281` ``` apply (rule cop) ``` wenzelm@60528 ` 282` ``` using ** apply auto ``` lp15@55261 ` 283` ``` done ``` wenzelm@60527 ` 284` ``` with \x dvd p\ \1 < x\ show ?thesis ``` wenzelm@60527 ` 285` ``` by auto ``` wenzelm@60527 ` 286` ``` qed ``` lp15@59667 ` 287` ``` then show ?thesis ``` wenzelm@60526 ` 288` ``` using \2 \ p\ ``` eberlm@63633 ` 289` ``` by (simp add: prime_nat_iff) ``` lp15@59667 ` 290` ``` (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 ``` lp15@55352 ` 291` ``` not_numeral_le_zero one_dvd) ``` lp15@55261 ` 292` ```qed ``` lp15@55261 ` 293` nipkow@31719 ` 294` ```lemma phi_zero [simp]: "phi 0 = 0" ``` wenzelm@60527 ` 295` ``` unfolding phi_def ``` wenzelm@44872 ` 296` ```(* Auto hangs here. Once again, where is the simplification rule ``` wenzelm@60527 ` 297` ``` 1 \ Suc 0 coming from? *) ``` nipkow@31719 ` 298` ``` apply (auto simp add: card_eq_0_iff) ``` nipkow@31719 ` 299` ```(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) ``` wenzelm@41541 ` 300` ``` done ``` nipkow@31719 ` 301` nipkow@31719 ` 302` ```lemma phi_one [simp]: "phi 1 = 0" ``` wenzelm@44872 ` 303` ``` by (auto simp add: phi_def card_eq_0_iff) ``` nipkow@31719 ` 304` wenzelm@60527 ` 305` ```lemma (in residues) phi_eq: "phi m = card (Units R)" ``` nipkow@31719 ` 306` ``` by (simp add: phi_def res_units_eq) ``` nipkow@31719 ` 307` wenzelm@44872 ` 308` ```lemma (in residues) euler_theorem1: ``` nipkow@31719 ` 309` ``` assumes a: "gcd a m = 1" ``` nipkow@31719 ` 310` ``` shows "[a^phi m = 1] (mod m)" ``` nipkow@31719 ` 311` ```proof - ``` wenzelm@60527 ` 312` ``` from a m_gt_one have [simp]: "a mod m \ Units R" ``` nipkow@31719 ` 313` ``` by (intro mod_in_res_units) ``` nipkow@31719 ` 314` ``` from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" ``` nipkow@31719 ` 315` ``` by simp ``` wenzelm@44872 ` 316` ``` also have "\ = \" ``` wenzelm@60527 ` 317` ``` by (intro units_power_order_eq_one) auto ``` nipkow@31719 ` 318` ``` finally show ?thesis ``` nipkow@31719 ` 319` ``` by (simp add: res_to_cong_simps) ``` nipkow@31719 ` 320` ```qed ``` nipkow@31719 ` 321` nipkow@31719 ` 322` ```(* In fact, there is a two line proof! ``` nipkow@31719 ` 323` wenzelm@44872 ` 324` ```lemma (in residues) euler_theorem1: ``` nipkow@31719 ` 325` ``` assumes a: "gcd a m = 1" ``` nipkow@31719 ` 326` ``` shows "[a^phi m = 1] (mod m)" ``` nipkow@31719 ` 327` ```proof - ``` nipkow@31719 ` 328` ``` have "(a mod m) (^) (phi m) = \" ``` nipkow@31719 ` 329` ``` by (simp add: phi_eq units_power_order_eq_one a m_gt_one) ``` wenzelm@44872 ` 330` ``` then show ?thesis ``` nipkow@31719 ` 331` ``` by (simp add: res_to_cong_simps) ``` nipkow@31719 ` 332` ```qed ``` nipkow@31719 ` 333` nipkow@31719 ` 334` ```*) ``` nipkow@31719 ` 335` wenzelm@63167 ` 336` ```text \Outside the locale, we can relax the restriction \m > 1\.\ ``` nipkow@31719 ` 337` ```lemma euler_theorem: ``` wenzelm@60527 ` 338` ``` assumes "m \ 0" ``` wenzelm@60527 ` 339` ``` and "gcd a m = 1" ``` nipkow@31719 ` 340` ``` shows "[a^phi m = 1] (mod m)" ``` wenzelm@60527 ` 341` ```proof (cases "m = 0 | m = 1") ``` wenzelm@60527 ` 342` ``` case True ``` wenzelm@44872 ` 343` ``` then show ?thesis by auto ``` nipkow@31719 ` 344` ```next ``` wenzelm@60527 ` 345` ``` case False ``` wenzelm@41541 ` 346` ``` with assms show ?thesis ``` nipkow@31719 ` 347` ``` by (intro residues.euler_theorem1, unfold residues_def, auto) ``` nipkow@31719 ` 348` ```qed ``` nipkow@31719 ` 349` wenzelm@60527 ` 350` ```lemma (in residues_prime) phi_prime: "phi p = nat p - 1" ``` nipkow@31719 ` 351` ``` apply (subst phi_eq) ``` nipkow@31719 ` 352` ``` apply (subst res_prime_units_eq) ``` nipkow@31719 ` 353` ``` apply auto ``` wenzelm@41541 ` 354` ``` done ``` nipkow@31719 ` 355` eberlm@63534 ` 356` ```lemma phi_prime: "prime (int p) \ phi p = nat p - 1" ``` nipkow@31719 ` 357` ``` apply (rule residues_prime.phi_prime) ``` eberlm@63534 ` 358` ``` apply simp ``` nipkow@31719 ` 359` ``` apply (erule residues_prime.intro) ``` wenzelm@41541 ` 360` ``` done ``` nipkow@31719 ` 361` nipkow@31719 ` 362` ```lemma fermat_theorem: ``` wenzelm@60527 ` 363` ``` fixes a :: int ``` eberlm@63534 ` 364` ``` assumes "prime (int p)" ``` wenzelm@60527 ` 365` ``` and "\ p dvd a" ``` lp15@55242 ` 366` ``` shows "[a^(p - 1) = 1] (mod p)" ``` nipkow@31719 ` 367` ```proof - ``` wenzelm@60527 ` 368` ``` from assms have "[a ^ phi p = 1] (mod p)" ``` eberlm@63534 ` 369` ``` by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p] ``` eberlm@63534 ` 370` ``` simp: gcd.commute[of _ "int p"]) ``` nipkow@31719 ` 371` ``` also have "phi p = nat p - 1" ``` wenzelm@60527 ` 372` ``` by (rule phi_prime) (rule assms) ``` lp15@55242 ` 373` ``` finally show ?thesis ``` lp15@59667 ` 374` ``` by (metis nat_int) ``` nipkow@31719 ` 375` ```qed ``` nipkow@31719 ` 376` lp15@55227 ` 377` ```lemma fermat_theorem_nat: ``` eberlm@63534 ` 378` ``` assumes "prime (int p)" and "\ p dvd a" ``` wenzelm@60527 ` 379` ``` shows "[a ^ (p - 1) = 1] (mod p)" ``` wenzelm@60527 ` 380` ``` using fermat_theorem [of p a] assms ``` haftmann@62348 ` 381` ``` by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int) ``` lp15@55227 ` 382` nipkow@31719 ` 383` wenzelm@60526 ` 384` ```subsection \Wilson's theorem\ ``` nipkow@31719 ` 385` wenzelm@60527 ` 386` ```lemma (in field) inv_pair_lemma: "x \ Units R \ y \ Units R \ ``` wenzelm@60527 ` 387` ``` {x, inv x} \ {y, inv y} \ {x, inv x} \ {y, inv y} = {}" ``` nipkow@31719 ` 388` ``` apply auto ``` lp15@55352 ` 389` ``` apply (metis Units_inv_inv)+ ``` wenzelm@41541 ` 390` ``` done ``` nipkow@31719 ` 391` nipkow@31719 ` 392` ```lemma (in residues_prime) wilson_theorem1: ``` nipkow@31719 ` 393` ``` assumes a: "p > 2" ``` lp15@59730 ` 394` ``` shows "[fact (p - 1) = (-1::int)] (mod p)" ``` nipkow@31719 ` 395` ```proof - ``` wenzelm@60527 ` 396` ``` let ?Inverse_Pairs = "{{x, inv x}| x. x \ Units R - {\, \ \}}" ``` wenzelm@60527 ` 397` ``` have UR: "Units R = {\, \ \} \ \?Inverse_Pairs" ``` nipkow@31719 ` 398` ``` by auto ``` wenzelm@60527 ` 399` ``` have "(\i\Units R. i) = (\i\{\, \ \}. i) \ (\i\\?Inverse_Pairs. i)" ``` nipkow@31732 ` 400` ``` apply (subst UR) ``` nipkow@31719 ` 401` ``` apply (subst finprod_Un_disjoint) ``` lp15@55352 ` 402` ``` apply (auto intro: funcsetI) ``` wenzelm@60527 ` 403` ``` using inv_one apply auto[1] ``` wenzelm@60527 ` 404` ``` using inv_eq_neg_one_eq apply auto ``` nipkow@31719 ` 405` ``` done ``` wenzelm@60527 ` 406` ``` also have "(\i\{\, \ \}. i) = \ \" ``` nipkow@31719 ` 407` ``` apply (subst finprod_insert) ``` nipkow@31719 ` 408` ``` apply auto ``` nipkow@31719 ` 409` ``` apply (frule one_eq_neg_one) ``` wenzelm@60527 ` 410` ``` using a apply force ``` nipkow@31719 ` 411` ``` done ``` wenzelm@60527 ` 412` ``` also have "(\i\(\?Inverse_Pairs). i) = (\A\?Inverse_Pairs. (\y\A. y))" ``` wenzelm@60527 ` 413` ``` apply (subst finprod_Union_disjoint) ``` wenzelm@60527 ` 414` ``` apply auto ``` lp15@55352 ` 415` ``` apply (metis Units_inv_inv)+ ``` nipkow@31719 ` 416` ``` done ``` nipkow@31719 ` 417` ``` also have "\ = \" ``` wenzelm@60527 ` 418` ``` apply (rule finprod_one) ``` wenzelm@60527 ` 419` ``` apply auto ``` wenzelm@60527 ` 420` ``` apply (subst finprod_insert) ``` wenzelm@60527 ` 421` ``` apply auto ``` lp15@55352 ` 422` ``` apply (metis inv_eq_self) ``` nipkow@31719 ` 423` ``` done ``` wenzelm@60527 ` 424` ``` finally have "(\i\Units R. i) = \ \" ``` nipkow@31719 ` 425` ``` by simp ``` wenzelm@60527 ` 426` ``` also have "(\i\Units R. i) = (\i\Units R. i mod p)" ``` nipkow@31719 ` 427` ``` apply (rule finprod_cong') ``` wenzelm@60527 ` 428` ``` apply auto ``` nipkow@31719 ` 429` ``` apply (subst (asm) res_prime_units_eq) ``` nipkow@31719 ` 430` ``` apply auto ``` nipkow@31719 ` 431` ``` done ``` wenzelm@60527 ` 432` ``` also have "\ = (\i\Units R. i) mod p" ``` nipkow@31719 ` 433` ``` apply (rule prod_cong) ``` nipkow@31719 ` 434` ``` apply auto ``` nipkow@31719 ` 435` ``` done ``` nipkow@31719 ` 436` ``` also have "\ = fact (p - 1) mod p" ``` nipkow@64272 ` 437` ``` apply (simp add: fact_prod) ``` lp15@55242 ` 438` ``` apply (insert assms) ``` lp15@55242 ` 439` ``` apply (subst res_prime_units_eq) ``` nipkow@64272 ` 440` ``` apply (simp add: int_prod zmod_int prod_int_eq) ``` nipkow@31719 ` 441` ``` done ``` wenzelm@60527 ` 442` ``` finally have "fact (p - 1) mod p = \ \" . ``` wenzelm@60527 ` 443` ``` then show ?thesis ``` wenzelm@60528 ` 444` ``` by (metis of_nat_fact Divides.transfer_int_nat_functions(2) ``` wenzelm@60528 ` 445` ``` cong_int_def res_neg_eq res_one_eq) ``` nipkow@31719 ` 446` ```qed ``` nipkow@31719 ` 447` lp15@55352 ` 448` ```lemma wilson_theorem: ``` wenzelm@60527 ` 449` ``` assumes "prime p" ``` wenzelm@60527 ` 450` ``` shows "[fact (p - 1) = - 1] (mod p)" ``` lp15@55352 ` 451` ```proof (cases "p = 2") ``` lp15@59667 ` 452` ``` case True ``` lp15@55352 ` 453` ``` then show ?thesis ``` nipkow@64272 ` 454` ``` by (simp add: cong_int_def fact_prod) ``` lp15@55352 ` 455` ```next ``` lp15@55352 ` 456` ``` case False ``` lp15@55352 ` 457` ``` then show ?thesis ``` lp15@55352 ` 458` ``` using assms prime_ge_2_nat ``` lp15@55352 ` 459` ``` by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) ``` lp15@55352 ` 460` ```qed ``` nipkow@31719 ` 461` nipkow@31719 ` 462` ```end ```