Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: plugin_base.dune Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Number_Theory/Residues.thy
    Author:     Jeremy Avigad

An algebraic treatment of residue rings, and resulting proofs of
Euler's theorem and Wilson's theorem.
*)

section \<open>Residue rings\<close>

theory Residues
imports
  Cong
  "HOL-Algebra.Multiplicative_Group"
  Totient
begin

definition QuadRes :: "int \ int \ bool"
  where "QuadRes p a = (\y. ([y^2 = a] (mod p)))"

definition Legendre :: "int \ int \ int"
  where "Legendre a p =
    (if ([a = 0] (mod p)) then 0
     else if QuadRes p a then 1
     else -1)"

subsection \<open>A locale for residue rings\<close>

definition residue_ring :: "int \ int ring"
  where
    "residue_ring m =
      \<lparr>carrier = {0..m - 1},
       monoid.mult = \<lambda>x y. (x * y) mod m,
       one = 1,
       zero = 0,
       add = \<lambda>x y. (x + y) mod m\<rparr>"

locale residues =
  fixes m :: int and R (structure)
  assumes m_gt_one: "m > 1"
  defines "R \ residue_ring m"
begin

lemma abelian_group: "abelian_group R"
proof -
  have "\y\{0..m - 1}. (x + y) mod m = 0" if "0 \ x" "x < m" for x
  proof (cases "x = 0")
    case True
    with m_gt_one show ?thesis by simp
  next
    case False
    then have "(x + (m - x)) mod m = 0"
      by simp
    with m_gt_one that show ?thesis
      by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
  qed
  with m_gt_one show ?thesis
    by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
qed

lemma comm_monoid: "comm_monoid R"
  unfolding R_def residue_ring_def
  apply (rule comm_monoidI)
    using m_gt_one  apply auto
  apply (metis mod_mult_right_eq mult.assoc mult.commute)
  apply (metis mult.commute)
  done

lemma cring: "cring R"
  apply (intro cringI abelian_group comm_monoid)
  unfolding R_def residue_ring_def
  apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq)
  done

end

sublocale residues < cring
  by (rule cring)

context residues
begin

text \<open>
  These lemmas translate back and forth between internal and
  external concepts.
\<close>

lemma res_carrier_eq: "carrier R = {0..m - 1}"
  by (auto simp: R_def residue_ring_def)

lemma res_add_eq: "x \ y = (x + y) mod m"
  by (auto simp: R_def residue_ring_def)

lemma res_mult_eq: "x \ y = (x * y) mod m"
  by (auto simp: R_def residue_ring_def)

lemma res_zero_eq: "\ = 0"
  by (auto simp: R_def residue_ring_def)

lemma res_one_eq: "\ = 1"
  by (auto simp: R_def residue_ring_def units_of_def)

lemma res_units_eq: "Units R = {x. 0 < x \ x < m \ coprime x m}"
  using m_gt_one
  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
  apply (subst (asm) coprime_iff_invertible'_int)
   apply (auto simp add: cong_def)
  done

lemma res_neg_eq: "\ x = (- x) mod m"
  using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
  apply simp
  apply (rule the_equality)
   apply (simp add: mod_add_right_eq)
   apply (simp add: add.commute mod_add_right_eq)
  apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
  done

lemma finite [iff]: "finite (carrier R)"
  by (simp add: res_carrier_eq)

lemma finite_Units [iff]: "finite (Units R)"
  by (simp add: finite_ring_finite_units)

text \<open>
  The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
  residue classes. The following lemmas show that this mapping
  respects addition and multiplication on the integers.
\<close>

lemma mod_in_carrier [iff]: "a mod m \ carrier R"
  unfolding res_carrier_eq
  using insert m_gt_one by auto

lemma add_cong: "(x mod m) \ (y mod m) = (x + y) mod m"
  by (auto simp: R_def residue_ring_def mod_simps)

lemma mult_cong: "(x mod m) \ (y mod m) = (x * y) mod m"
  by (auto simp: R_def residue_ring_def mod_simps)

lemma zero_cong: "\ = 0"
  by (auto simp: R_def residue_ring_def)

lemma one_cong: "\ = 1 mod m"
  using m_gt_one by (auto simp: R_def residue_ring_def)

(* FIXME revise algebra library to use 1? *)
lemma pow_cong: "(x mod m) [^] n = x^n mod m"
  using m_gt_one
  apply (induct n)
  apply (auto simp add: nat_pow_def one_cong)
  apply (metis mult.commute mult_cong)
  done

lemma neg_cong: "\ (x mod m) = (- x) mod m"
  by (metis mod_minus_eq res_neg_eq)

lemma (in residues) prod_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m"
  by (induct set: finite) (auto simp: one_cong mult_cong)

lemma (in residues) sum_cong: "finite A \ (\i\A. (f i) mod m) = (\i\A. f i) mod m"
  by (induct set: finite) (auto simp: zero_cong add_cong)

lemma mod_in_res_units [simp]:
  assumes "1 < m" and "coprime a m"
  shows "a mod m \ Units R"
proof (cases "a mod m = 0")
  case True
  with assms show ?thesis
    by (auto simp add: res_units_eq gcd_red_int [symmetric])
next
  case False
  from assms have "0 < m" by simp
  then have "0 \ a mod m" by (rule pos_mod_sign [of m a])
  with False have "0 < a mod m" by simp
  with assms show ?thesis
    by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
qed

lemma res_eq_to_cong: "(a mod m) = (b mod m) \ [a = b] (mod m)"
  by (auto simp: cong_def)

text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
lemmas res_to_cong_simps =
  add_cong mult_cong pow_cong one_cong
  prod_cong sum_cong neg_cong res_eq_to_cong

text \<open>Other useful facts about the residue ring.\<close>
lemma one_eq_neg_one: "\ = \ \ \ m = 2"
  apply (simp add: res_one_eq res_neg_eq)
  apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
    zero_neq_one zmod_zminus1_eq_if)
  done

end

subsection \<open>Prime residues\<close>

locale residues_prime =
  fixes p :: nat and R (structure)
  assumes p_prime [intro]: "prime p"
  defines "R \ residue_ring (int p)"

sublocale residues_prime < residues p
  unfolding R_def residues_def
  using p_prime apply auto
  apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
  done

context residues_prime
begin

lemma p_coprime_left:
  "coprime p a \ \ p dvd a"
  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)

lemma p_coprime_right:
  "coprime a p \ \ p dvd a"
  using p_coprime_left [of a] by (simp add: ac_simps)

lemma p_coprime_left_int:
  "coprime (int p) a \ \ int p dvd a"
  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)

lemma p_coprime_right_int:
  "coprime a (int p) \ \ int p dvd a"
  using p_coprime_left_int [of a] by (simp add: ac_simps)

lemma is_field: "field R"
proof -
  have "0 < x \ x < int p \ coprime (int p) x" for x
    by (rule prime_imp_coprime) (auto simp add: zdvd_not_zless)
  then show ?thesis
    by (intro cring.field_intro2 cring)
      (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq ac_simps)
qed

lemma res_prime_units_eq: "Units R = {1..p - 1}"
  apply (subst res_units_eq)
  apply (auto simp add: p_coprime_right_int zdvd_not_zless)
  done

end

sublocale residues_prime < field
  by (rule is_field)

section \<open>Test cases: Euler's theorem and Wilson's theorem\<close>

subsection \<open>Euler's theorem\<close>

lemma (in residues) totatives_eq:
  "totatives (nat m) = nat ` Units R"
proof -
  from m_gt_one have "\m\ > 1"
    by simp
  then have "totatives (nat \m\) = nat ` abs ` Units R"
    by (auto simp add: totatives_def res_units_eq image_iff le_less)
      (use m_gt_one zless_nat_eq_int_zless in force)
  moreover have "\m\ = m" "abs ` Units R = Units R"
    using m_gt_one by (auto simp add: res_units_eq image_iff)
  ultimately show ?thesis
    by simp
qed

lemma (in residues) totient_eq:
  "totient (nat m) = card (Units R)"
proof  -
  have *: "inj_on nat (Units R)"
    by (rule inj_onI) (auto simp add: res_units_eq)
  then show ?thesis
    by (simp add: totient_def totatives_eq card_image)
qed

lemma (in residues_prime) totient_eq: "totient p = p - 1"
  using totient_eq by (simp add: res_prime_units_eq)

lemma (in residues) euler_theorem:
  assumes "coprime a m"
  shows "[a ^ totient (nat m) = 1] (mod m)"
proof -
  have "a ^ totient (nat m) mod m = 1 mod m"
    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one)
  then show ?thesis
    using res_eq_to_cong by blast
qed

lemma euler_theorem:
  fixes a m :: nat
  assumes "coprime a m"
  shows "[a ^ totient m = 1] (mod m)"
proof (cases "m = 0 \ m = 1")
  case True
  then show ?thesis by auto
next
  case False
  with assms show ?thesis
    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
    by (auto simp add: residues_def gcd_int_def) fastforce
qed

lemma fermat_theorem:
  fixes p a :: nat
  assumes "prime p" and "\ p dvd a"
  shows "[a ^ (p - 1) = 1] (mod p)"
proof -
  from assms prime_imp_coprime [of p a] have "coprime a p"
    by (auto simp add: ac_simps)
  then have "[a ^ totient p = 1] (mod p)"
     by (rule euler_theorem)
  also have "totient p = p - 1"
    by (rule totient_prime) (rule assms)
  finally show ?thesis .
qed

subsection \<open>Wilson's theorem\<close>

lemma (in field) inv_pair_lemma: "x \ Units R \ y \ Units R \
    {x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}"
  apply auto
  apply (metis Units_inv_inv)+
  done

lemma (in residues_prime) wilson_theorem1:
  assumes a: "p > 2"
  shows "[fact (p - 1) = (-1::int)] (mod p)"
proof -
  let ?Inverse_Pairs = "{{x, inv x}| x. x \ Units R - {\, \ \}}"
  have UR: "Units R = {\, \ \} \ \?Inverse_Pairs"
    by auto
  have "(\i\Units R. i) = (\i\{\, \ \}. i) \ (\i\\?Inverse_Pairs. i)"
    apply (subst UR)
    apply (subst finprod_Un_disjoint)
         apply (auto intro: funcsetI)
    using inv_one apply auto[1]
    using inv_eq_neg_one_eq apply auto
    done
  also have "(\i\{\, \ \}. i) = \ \"
    apply (subst finprod_insert)
        apply auto
    apply (frule one_eq_neg_one)
    using a apply force
    done
  also have "(\i\(\?Inverse_Pairs). i) = (\A\?Inverse_Pairs. (\y\A. y))"
    apply (subst finprod_Union_disjoint)
       apply (auto simp: pairwise_def disjnt_def)
     apply (metis Units_inv_inv)+
    done
  also have "\ = \"
    apply (rule finprod_one_eqI)
     apply auto
    apply (subst finprod_insert)
        apply auto
    apply (metis inv_eq_self)
    done
  finally have "(\i\Units R. i) = \ \"
    by simp
  also have "(\i\Units R. i) = (\i\Units R. i mod p)"
    by (rule finprod_cong') (auto simp: res_units_eq)
  also have "\ = (\i\Units R. i) mod p"
    by (rule prod_cong) auto
  also have "\ = fact (p - 1) mod p"
    apply (simp add: fact_prod)
    using assms
    apply (subst res_prime_units_eq)
    apply (simp add: int_prod zmod_int prod_int_eq)
    done
  finally have "fact (p - 1) mod p = \ \" .
  then show ?thesis
    by (simp add: cong_def res_neg_eq res_one_eq zmod_int)
qed

lemma wilson_theorem:
  assumes "prime p"
  shows "[fact (p - 1) = - 1] (mod p)"
proof (cases "p = 2")
  case True
  then show ?thesis
    by (simp add: cong_def fact_prod)
next
  case False
  then show ?thesis
    using assms prime_ge_2_nat
    by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
qed

text \<open>
  This result can be transferred to the multiplicative group of
  \<open>\<int>/p\<int>\<close> for \<open>p\<close> prime.\<close>

lemma mod_nat_int_pow_eq:
  fixes n :: nat and p a :: int
  shows "a \ 0 \ p \ 0 \ (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
  by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])

theorem residue_prime_mult_group_has_gen:
fixes p :: nat
assumes prime_p : "prime p"
shows "\a \ {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \ UNIV}"
proof -
  have "p \ 2"
    using prime_gt_1_nat[OF prime_p] by simp
  interpret R: residues_prime p "residue_ring p"
    by (simp add: residues_prime_def prime_p)
  have car: "carrier (residue_ring (int p)) - {\\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}"
    by (auto simp add: R.zero_cong R.res_carrier_eq)

  have "x [^]\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
    if "x \ {1 .. int p - 1}" for x and i :: nat
    using that R.pow_cong[of x i] by auto
  moreover
  obtain a where a: "a \ {1 .. int p - 1}"
    and a_gen: "{1 .. int p - 1} = {a[^]\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \ UNIV}"
    using field.finite_field_mult_group_has_gen[OF R.is_field]
    by (auto simp add: car[symmetric] carrier_mult_of)
  moreover
  have "nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
  proof
    have "n \ ?R" if "n \ ?L" for n
      using that \<open>p\<ge>2\<close> by force
    then show "?L \ ?R" by blast
    have "n \ ?L" if "n \ ?R" for n
      using that \<open>p\<ge>2\<close> by (auto intro: rev_image_eqI [of "int n"])
    then show "?R \ ?L" by blast
  qed
  moreover
  have "nat ` {a^i mod (int p) | i::nat. i \ UNIV} = {nat a^i mod p | i . i \ UNIV}" (is "?L = ?R")
  proof
    have "x \ ?R" if "x \ ?L" for x
    proof -
      from that obtain i where i: "x = nat (a^i mod (int p))"
        by blast
      then have "x = nat a ^ i mod p"
        using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
      with i show ?thesis by blast
    qed
    then show "?L \ ?R" by blast
    have "x \ ?L" if "x \ ?R" for x
    proof -
      from that obtain i where i: "x = nat a^i mod p"
        by blast
      with mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> show ?thesis
        by auto
    qed
    then show "?R \ ?L" by blast
  qed
  ultimately have "{1 .. p - 1} = {nat a^i mod p | i. i \ UNIV}"
    by presburger
  moreover from a have "nat a \ {1 .. p - 1}" by force
  ultimately show ?thesis ..
qed

subsection \<open>Upper bound for the number of $n$-th roots\<close>

lemma roots_mod_prime_bound:
  fixes n c p :: nat
  assumes "prime p" "n > 0"
  defines "A \ {x\{..
  shows   "card A \ n"
proof -
  define R where "R = residue_ring (int p)"
  from assms(1) interpret residues_prime p R
    by unfold_locales (simp_all add: R_def)
  interpret R: UP_domain R "UP R" by (unfold_locales)

  let ?f = "UnivPoly.monom (UP R) \\<^bsub>R\<^esub> n \\<^bsub>(UP R)\<^esub> UnivPoly.monom (UP R) (int (c mod p)) 0"
  have in_carrier: "int (c mod p) \ carrier R"
    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)

  have "deg R ?f = n"
    using assms in_carrier by (simp add: R.deg_minus_eq)
  hence f_not_zero: "?f \ \\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
  have roots_bound: "finite {a \ carrier R. UnivPoly.eval R R id a ?f = \\<^bsub>R\<^esub>} \
                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
  have subs: "{x \ carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \
                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
    using in_carrier by (auto simp: R.evalRR_simps)
  then have "card {x \ carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \
               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
    using finite by (intro card_mono) auto
  also have "\ \ n"
    using \<open>deg R ?f = n\<close> roots_bound by linarith
  also {
    fix x assume "x \ carrier R"
    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
  }
  hence "{x \ carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} = {x \ carrier R. [x ^ n = int c] (mod p)}"
    by (fastforce simp: cong_def zmod_int)
  also have "bij_betw int A {x \ carrier R. [x ^ n = int c] (mod p)}"
    by (rule bij_betwI[of int _ _ nat])
       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
  from bij_betw_same_card[OF this] have "card {x \ carrier R. [x ^ n = int c] (mod p)} = card A" ..
  finally show ?thesis .
qed

end

¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.