src/HOL/Number_Theory/Residues.thy
 changeset 32479 521cc9bf2958 parent 31952 40501bb2d57c child 35416 d8d7d1b785af
equal inserted replaced
32478:87201c60ae7d 32479:521cc9bf2958
`       `
`     1 (*  Title:      HOL/Library/Residues.thy`
`       `
`     2     ID:         `
`       `
`     3     Author:     Jeremy Avigad`
`       `
`     4 `
`       `
`     5     An algebraic treatment of residue rings, and resulting proofs of`
`       `
`     6     Euler's theorem and Wilson's theorem. `
`       `
`     7 *)`
`       `
`     8 `
`       `
`     9 header {* Residue rings *}`
`       `
`    10 `
`       `
`    11 theory Residues`
`       `
`    12 imports`
`       `
`    13    UniqueFactorization`
`       `
`    14    Binomial`
`       `
`    15    MiscAlgebra`
`       `
`    16 begin`
`       `
`    17 `
`       `
`    18 `
`       `
`    19 (*`
`       `
`    20  `
`       `
`    21   A locale for residue rings`
`       `
`    22 `
`       `
`    23 *)`
`       `
`    24 `
`       `
`    25 constdefs `
`       `
`    26   residue_ring :: "int => int ring"`
`       `
`    27   "residue_ring m == (| `
`       `
`    28     carrier =       {0..m - 1}, `
`       `
`    29     mult =          (%x y. (x * y) mod m),`
`       `
`    30     one =           1,`
`       `
`    31     zero =          0,`
`       `
`    32     add =           (%x y. (x + y) mod m) |)"`
`       `
`    33 `
`       `
`    34 locale residues =`
`       `
`    35   fixes m :: int and R (structure)`
`       `
`    36   assumes m_gt_one: "m > 1"`
`       `
`    37   defines "R == residue_ring m"`
`       `
`    38 `
`       `
`    39 context residues begin`
`       `
`    40 `
`       `
`    41 lemma abelian_group: "abelian_group R"`
`       `
`    42   apply (insert m_gt_one)`
`       `
`    43   apply (rule abelian_groupI)`
`       `
`    44   apply (unfold R_def residue_ring_def)`
`       `
`    45   apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]`
`       `
`    46     add_ac)`
`       `
`    47   apply (case_tac "x = 0")`
`       `
`    48   apply force`
`       `
`    49   apply (subgoal_tac "(x + (m - x)) mod m = 0")`
`       `
`    50   apply (erule bexI)`
`       `
`    51   apply auto`
`       `
`    52 done`
`       `
`    53 `
`       `
`    54 lemma comm_monoid: "comm_monoid R"`
`       `
`    55   apply (insert m_gt_one)`
`       `
`    56   apply (unfold R_def residue_ring_def)`
`       `
`    57   apply (rule comm_monoidI)`
`       `
`    58   apply auto`
`       `
`    59   apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")`
`       `
`    60   apply (erule ssubst)`
`       `
`    61   apply (subst zmod_zmult1_eq [symmetric])+`
`       `
`    62   apply (simp_all only: mult_ac)`
`       `
`    63 done`
`       `
`    64 `
`       `
`    65 lemma cring: "cring R"`
`       `
`    66   apply (rule cringI)`
`       `
`    67   apply (rule abelian_group)`
`       `
`    68   apply (rule comm_monoid)`
`       `
`    69   apply (unfold R_def residue_ring_def, auto)`
`       `
`    70   apply (subst mod_add_eq [symmetric])`
`       `
`    71   apply (subst mult_commute)`
`       `
`    72   apply (subst zmod_zmult1_eq [symmetric])`
`       `
`    73   apply (simp add: ring_simps)`
`       `
`    74 done`
`       `
`    75 `
`       `
`    76 end`
`       `
`    77 `
`       `
`    78 sublocale residues < cring`
`       `
`    79   by (rule cring)`
`       `
`    80 `
`       `
`    81 `
`       `
`    82 context residues begin`
`       `
`    83 `
`       `
`    84 (* These lemmas translate back and forth between internal and `
`       `
`    85    external concepts *)`
`       `
`    86 `
`       `
`    87 lemma res_carrier_eq: "carrier R = {0..m - 1}"`
`       `
`    88   by (unfold R_def residue_ring_def, auto)`
`       `
`    89 `
`       `
`    90 lemma res_add_eq: "x \<oplus> y = (x + y) mod m"`
`       `
`    91   by (unfold R_def residue_ring_def, auto)`
`       `
`    92 `
`       `
`    93 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"`
`       `
`    94   by (unfold R_def residue_ring_def, auto)`
`       `
`    95 `
`       `
`    96 lemma res_zero_eq: "\<zero> = 0"`
`       `
`    97   by (unfold R_def residue_ring_def, auto)`
`       `
`    98 `
`       `
`    99 lemma res_one_eq: "\<one> = 1"`
`       `
`   100   by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)`
`       `
`   101 `
`       `
`   102 lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"`
`       `
`   103   apply (insert m_gt_one)`
`       `
`   104   apply (unfold Units_def R_def residue_ring_def)`
`       `
`   105   apply auto`
`       `
`   106   apply (subgoal_tac "x ~= 0")`
`       `
`   107   apply auto`
`       `
`   108   apply (rule invertible_coprime_int)`
`       `
`   109   apply (subgoal_tac "x ~= 0")`
`       `
`   110   apply auto`
`       `
`   111   apply (subst (asm) coprime_iff_invertible'_int)`
`       `
`   112   apply (rule m_gt_one)`
`       `
`   113   apply (auto simp add: cong_int_def mult_commute)`
`       `
`   114 done`
`       `
`   115 `
`       `
`   116 lemma res_neg_eq: "\<ominus> x = (- x) mod m"`
`       `
`   117   apply (insert m_gt_one)`
`       `
`   118   apply (unfold R_def a_inv_def m_inv_def residue_ring_def)`
`       `
`   119   apply auto`
`       `
`   120   apply (rule the_equality)`
`       `
`   121   apply auto`
`       `
`   122   apply (subst mod_add_right_eq [symmetric])`
`       `
`   123   apply auto`
`       `
`   124   apply (subst mod_add_left_eq [symmetric])`
`       `
`   125   apply auto`
`       `
`   126   apply (subgoal_tac "y mod m = - x mod m")`
`       `
`   127   apply simp`
`       `
`   128   apply (subst zmod_eq_dvd_iff)`
`       `
`   129   apply auto`
`       `
`   130 done`
`       `
`   131 `
`       `
`   132 lemma finite [iff]: "finite(carrier R)"`
`       `
`   133   by (subst res_carrier_eq, auto)`
`       `
`   134 `
`       `
`   135 lemma finite_Units [iff]: "finite(Units R)"`
`       `
`   136   by (subst res_units_eq, auto)`
`       `
`   137 `
`       `
`   138 (* The function a -> a mod m maps the integers to the `
`       `
`   139    residue classes. The following lemmas show that this mapping `
`       `
`   140    respects addition and multiplication on the integers. *)`
`       `
`   141 `
`       `
`   142 lemma mod_in_carrier [iff]: "a mod m : carrier R"`
`       `
`   143   apply (unfold res_carrier_eq)`
`       `
`   144   apply (insert m_gt_one, auto)`
`       `
`   145 done`
`       `
`   146 `
`       `
`   147 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"`
`       `
`   148   by (unfold R_def residue_ring_def, auto, arith)`
`       `
`   149 `
`       `
`   150 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"`
`       `
`   151   apply (unfold R_def residue_ring_def, auto)`
`       `
`   152   apply (subst zmod_zmult1_eq [symmetric])`
`       `
`   153   apply (subst mult_commute)`
`       `
`   154   apply (subst zmod_zmult1_eq [symmetric])`
`       `
`   155   apply (subst mult_commute)`
`       `
`   156   apply auto`
`       `
`   157 done  `
`       `
`   158 `
`       `
`   159 lemma zero_cong: "\<zero> = 0"`
`       `
`   160   apply (unfold R_def residue_ring_def, auto)`
`       `
`   161 done`
`       `
`   162 `
`       `
`   163 lemma one_cong: "\<one> = 1 mod m"`
`       `
`   164   apply (insert m_gt_one)`
`       `
`   165   apply (unfold R_def residue_ring_def, auto)`
`       `
`   166 done`
`       `
`   167 `
`       `
`   168 (* revise algebra library to use 1? *)`
`       `
`   169 lemma pow_cong: "(x mod m) (^) n = x^n mod m"`
`       `
`   170   apply (insert m_gt_one)`
`       `
`   171   apply (induct n)`
`       `
`   172   apply (auto simp add: nat_pow_def one_cong One_nat_def)`
`       `
`   173   apply (subst mult_commute)`
`       `
`   174   apply (rule mult_cong)`
`       `
`   175 done`
`       `
`   176 `
`       `
`   177 lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"`
`       `
`   178   apply (rule sym)`
`       `
`   179   apply (rule sum_zero_eq_neg)`
`       `
`   180   apply auto`
`       `
`   181   apply (subst add_cong)`
`       `
`   182   apply (subst zero_cong)`
`       `
`   183   apply auto`
`       `
`   184 done`
`       `
`   185 `
`       `
`   186 lemma (in residues) prod_cong: `
`       `
`   187   "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"`
`       `
`   188   apply (induct set: finite)`
`       `
`   189   apply (auto simp: one_cong mult_cong)`
`       `
`   190 done`
`       `
`   191 `
`       `
`   192 lemma (in residues) sum_cong:`
`       `
`   193   "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"`
`       `
`   194   apply (induct set: finite)`
`       `
`   195   apply (auto simp: zero_cong add_cong)`
`       `
`   196 done`
`       `
`   197 `
`       `
`   198 lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> `
`       `
`   199     a mod m : Units R"`
`       `
`   200   apply (subst res_units_eq, auto)`
`       `
`   201   apply (insert pos_mod_sign [of m a])`
`       `
`   202   apply (subgoal_tac "a mod m ~= 0")`
`       `
`   203   apply arith`
`       `
`   204   apply auto`
`       `
`   205   apply (subst (asm) gcd_red_int)`
`       `
`   206   apply (subst gcd_commute_int, assumption)`
`       `
`   207 done`
`       `
`   208 `
`       `
`   209 lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" `
`       `
`   210   unfolding cong_int_def by auto`
`       `
`   211 `
`       `
`   212 (* Simplifying with these will translate a ring equation in R to a `
`       `
`   213    congruence. *)`
`       `
`   214 `
`       `
`   215 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong`
`       `
`   216     prod_cong sum_cong neg_cong res_eq_to_cong`
`       `
`   217 `
`       `
`   218 (* Other useful facts about the residue ring *)`
`       `
`   219 `
`       `
`   220 lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"`
`       `
`   221   apply (simp add: res_one_eq res_neg_eq)`
`       `
`   222   apply (insert m_gt_one)`
`       `
`   223   apply (subgoal_tac "~(m > 2)")`
`       `
`   224   apply arith`
`       `
`   225   apply (rule notI)`
`       `
`   226   apply (subgoal_tac "-1 mod m = m - 1")`
`       `
`   227   apply force`
`       `
`   228   apply (subst mod_add_self2 [symmetric])`
`       `
`   229   apply (subst mod_pos_pos_trivial)`
`       `
`   230   apply auto`
`       `
`   231 done`
`       `
`   232 `
`       `
`   233 end`
`       `
`   234 `
`       `
`   235 `
`       `
`   236 (* prime residues *)`
`       `
`   237 `
`       `
`   238 locale residues_prime =`
`       `
`   239   fixes p :: int and R (structure)`
`       `
`   240   assumes p_prime [intro]: "prime p"`
`       `
`   241   defines "R == residue_ring p"`
`       `
`   242 `
`       `
`   243 sublocale residues_prime < residues p`
`       `
`   244   apply (unfold R_def residues_def)`
`       `
`   245   using p_prime apply auto`
`       `
`   246 done`
`       `
`   247 `
`       `
`   248 context residues_prime begin`
`       `
`   249 `
`       `
`   250 lemma is_field: "field R"`
`       `
`   251   apply (rule cring.field_intro2)`
`       `
`   252   apply (rule cring)`
`       `
`   253   apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq`
`       `
`   254     res_units_eq)`
`       `
`   255   apply (rule classical)`
`       `
`   256   apply (erule notE)`
`       `
`   257   apply (subst gcd_commute_int)`
`       `
`   258   apply (rule prime_imp_coprime_int)`
`       `
`   259   apply (rule p_prime)`
`       `
`   260   apply (rule notI)`
`       `
`   261   apply (frule zdvd_imp_le)`
`       `
`   262   apply auto`
`       `
`   263 done`
`       `
`   264 `
`       `
`   265 lemma res_prime_units_eq: "Units R = {1..p - 1}"`
`       `
`   266   apply (subst res_units_eq)`
`       `
`   267   apply auto`
`       `
`   268   apply (subst gcd_commute_int)`
`       `
`   269   apply (rule prime_imp_coprime_int)`
`       `
`   270   apply (rule p_prime)`
`       `
`   271   apply (rule zdvd_not_zless)`
`       `
`   272   apply auto`
`       `
`   273 done`
`       `
`   274 `
`       `
`   275 end`
`       `
`   276 `
`       `
`   277 sublocale residues_prime < field`
`       `
`   278   by (rule is_field)`
`       `
`   279 `
`       `
`   280 `
`       `
`   281 (*`
`       `
`   282   Test cases: Euler's theorem and Wilson's theorem.`
`       `
`   283 *)`
`       `
`   284 `
`       `
`   285 `
`       `
`   286 subsection{* Euler's theorem *}`
`       `
`   287 `
`       `
`   288 (* the definition of the phi function *)`
`       `
`   289 `
`       `
`   290 constdefs`
`       `
`   291   phi :: "int => nat"`
`       `
`   292   "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" `
`       `
`   293 `
`       `
`   294 lemma phi_zero [simp]: "phi 0 = 0"`
`       `
`   295   apply (subst phi_def)`
`       `
`   296 (* Auto hangs here. Once again, where is the simplification rule `
`       `
`   297    1 == Suc 0 coming from? *)`
`       `
`   298   apply (auto simp add: card_eq_0_iff)`
`       `
`   299 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)`
`       `
`   300 done`
`       `
`   301 `
`       `
`   302 lemma phi_one [simp]: "phi 1 = 0"`
`       `
`   303   apply (auto simp add: phi_def card_eq_0_iff)`
`       `
`   304 done`
`       `
`   305 `
`       `
`   306 lemma (in residues) phi_eq: "phi m = card(Units R)"`
`       `
`   307   by (simp add: phi_def res_units_eq)`
`       `
`   308 `
`       `
`   309 lemma (in residues) euler_theorem1: `
`       `
`   310   assumes a: "gcd a m = 1"`
`       `
`   311   shows "[a^phi m = 1] (mod m)"`
`       `
`   312 proof -`
`       `
`   313   from a m_gt_one have [simp]: "a mod m : Units R"`
`       `
`   314     by (intro mod_in_res_units)`
`       `
`   315   from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"`
`       `
`   316     by simp`
`       `
`   317   also have "\<dots> = \<one>" `
`       `
`   318     by (intro units_power_order_eq_one, auto)`
`       `
`   319   finally show ?thesis`
`       `
`   320     by (simp add: res_to_cong_simps)`
`       `
`   321 qed`
`       `
`   322 `
`       `
`   323 (* In fact, there is a two line proof!`
`       `
`   324 `
`       `
`   325 lemma (in residues) euler_theorem1: `
`       `
`   326   assumes a: "gcd a m = 1"`
`       `
`   327   shows "[a^phi m = 1] (mod m)"`
`       `
`   328 proof -`
`       `
`   329   have "(a mod m) (^) (phi m) = \<one>"`
`       `
`   330     by (simp add: phi_eq units_power_order_eq_one a m_gt_one)`
`       `
`   331   thus ?thesis`
`       `
`   332     by (simp add: res_to_cong_simps)`
`       `
`   333 qed`
`       `
`   334 `
`       `
`   335 *)`
`       `
`   336 `
`       `
`   337 (* outside the locale, we can relax the restriction m > 1 *)`
`       `
`   338 `
`       `
`   339 lemma euler_theorem:`
`       `
`   340   assumes "m >= 0" and "gcd a m = 1"`
`       `
`   341   shows "[a^phi m = 1] (mod m)"`
`       `
`   342 proof (cases)`
`       `
`   343   assume "m = 0 | m = 1"`
`       `
`   344   thus ?thesis by auto`
`       `
`   345 next`
`       `
`   346   assume "~(m = 0 | m = 1)"`
`       `
`   347   with prems show ?thesis`
`       `
`   348     by (intro residues.euler_theorem1, unfold residues_def, auto)`
`       `
`   349 qed`
`       `
`   350 `
`       `
`   351 lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"`
`       `
`   352   apply (subst phi_eq)`
`       `
`   353   apply (subst res_prime_units_eq)`
`       `
`   354   apply auto`
`       `
`   355 done`
`       `
`   356 `
`       `
`   357 lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"`
`       `
`   358   apply (rule residues_prime.phi_prime)`
`       `
`   359   apply (erule residues_prime.intro)`
`       `
`   360 done`
`       `
`   361 `
`       `
`   362 lemma fermat_theorem:`
`       `
`   363   assumes "prime p" and "~ (p dvd a)"`
`       `
`   364   shows "[a^(nat p - 1) = 1] (mod p)"`
`       `
`   365 proof -`
`       `
`   366   from prems have "[a^phi p = 1] (mod p)"`
`       `
`   367     apply (intro euler_theorem)`
`       `
`   368     (* auto should get this next part. matching across`
`       `
`   369        substitutions is needed. *)`
`       `
`   370     apply (frule prime_gt_1_int, arith)`
`       `
`   371     apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)`
`       `
`   372     done`
`       `
`   373   also have "phi p = nat p - 1"`
`       `
`   374     by (rule phi_prime, rule prems)`
`       `
`   375   finally show ?thesis .`
`       `
`   376 qed`
`       `
`   377 `
`       `
`   378 `
`       `
`   379 subsection {* Wilson's theorem *}`
`       `
`   380 `
`       `
`   381 lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> `
`       `
`   382   {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" `
`       `
`   383   apply auto`
`       `
`   384   apply (erule notE)`
`       `
`   385   apply (erule inv_eq_imp_eq)`
`       `
`   386   apply auto`
`       `
`   387   apply (erule notE)`
`       `
`   388   apply (erule inv_eq_imp_eq)`
`       `
`   389   apply auto`
`       `
`   390 done`
`       `
`   391 `
`       `
`   392 lemma (in residues_prime) wilson_theorem1:`
`       `
`   393   assumes a: "p > 2"`
`       `
`   394   shows "[fact (p - 1) = - 1] (mod p)"`
`       `
`   395 proof -`
`       `
`   396   let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" `
`       `
`   397   have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"`
`       `
`   398     by auto`
`       `
`   399   have "(\<Otimes>i: Units R. i) = `
`       `
`   400     (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"`
`       `
`   401     apply (subst UR)`
`       `
`   402     apply (subst finprod_Un_disjoint)`
`       `
`   403     apply (auto intro:funcsetI)`
`       `
`   404     apply (drule sym, subst (asm) inv_eq_one_eq)`
`       `
`   405     apply auto`
`       `
`   406     apply (drule sym, subst (asm) inv_eq_neg_one_eq)`
`       `
`   407     apply auto`
`       `
`   408     done`
`       `
`   409   also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"`
`       `
`   410     apply (subst finprod_insert)`
`       `
`   411     apply auto`
`       `
`   412     apply (frule one_eq_neg_one)`
`       `
`   413     apply (insert a, force)`
`       `
`   414     done`
`       `
`   415   also have "(\<Otimes>i:(Union ?InversePairs). i) = `
`       `
`   416       (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"`
`       `
`   417     apply (subst finprod_Union_disjoint)`
`       `
`   418     apply force`
`       `
`   419     apply force`
`       `
`   420     apply clarify`
`       `
`   421     apply (rule inv_pair_lemma)`
`       `
`   422     apply auto`
`       `
`   423     done`
`       `
`   424   also have "\<dots> = \<one>"`
`       `
`   425     apply (rule finprod_one)`
`       `
`   426     apply auto`
`       `
`   427     apply (subst finprod_insert)`
`       `
`   428     apply auto`
`       `
`   429     apply (frule inv_eq_self)`
`       `
`   430     apply (auto)`
`       `
`   431     done`
`       `
`   432   finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"`
`       `
`   433     by simp`
`       `
`   434   also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"`
`       `
`   435     apply (rule finprod_cong')`
`       `
`   436     apply (auto)`
`       `
`   437     apply (subst (asm) res_prime_units_eq)`
`       `
`   438     apply auto`
`       `
`   439     done`
`       `
`   440   also have "\<dots> = (PROD i: Units R. i) mod p"`
`       `
`   441     apply (rule prod_cong)`
`       `
`   442     apply auto`
`       `
`   443     done`
`       `
`   444   also have "\<dots> = fact (p - 1) mod p"`
`       `
`   445     apply (subst fact_altdef_int)`
`       `
`   446     apply (insert prems, force)`
`       `
`   447     apply (subst res_prime_units_eq, rule refl)`
`       `
`   448     done`
`       `
`   449   finally have "fact (p - 1) mod p = \<ominus> \<one>".`
`       `
`   450   thus ?thesis`
`       `
`   451     by (simp add: res_to_cong_simps)`
`       `
`   452 qed`
`       `
`   453 `
`       `
`   454 lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"`
`       `
`   455   apply (frule prime_gt_1_int)`
`       `
`   456   apply (case_tac "p = 2")`
`       `
`   457   apply (subst fact_altdef_int, simp)`
`       `
`   458   apply (subst cong_int_def)`
`       `
`   459   apply simp`
`       `
`   460   apply (rule residues_prime.wilson_theorem1)`
`       `
`   461   apply (rule residues_prime.intro)`
`       `
`   462   apply auto`
`       `
`   463 done`
`       `
`   464 `
`       `
`   465 `
`       `
`   466 end`