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