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