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