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