src/HOL/Number_Theory/Residues.thy
changeset 65416 f707dbcf11e3
parent 65066 c64d778a593a
child 65465 067210a08a22
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Apr 06 22:04:30 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Apr 06 08:33:37 2017 +0200
     1.3 @@ -8,7 +8,12 @@
     1.4  section \<open>Residue rings\<close>
     1.5  
     1.6  theory Residues
     1.7 -imports Cong MiscAlgebra
     1.8 +imports
     1.9 +  Cong
    1.10 +  "~~/src/HOL/Algebra/More_Group"
    1.11 +  "~~/src/HOL/Algebra/More_Ring"
    1.12 +  "~~/src/HOL/Algebra/More_Finite_Product"
    1.13 +  "~~/src/HOL/Algebra/Multiplicative_Group"
    1.14  begin
    1.15  
    1.16  definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
    1.17 @@ -117,10 +122,10 @@
    1.18    done
    1.19  
    1.20  lemma finite [iff]: "finite (carrier R)"
    1.21 -  by (subst res_carrier_eq) auto
    1.22 +  by (simp add: res_carrier_eq)
    1.23  
    1.24  lemma finite_Units [iff]: "finite (Units R)"
    1.25 -  by (subst res_units_eq) auto
    1.26 +  by (simp add: finite_ring_finite_units)
    1.27  
    1.28  text \<open>
    1.29    The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
    1.30 @@ -286,6 +291,28 @@
    1.31  lemma phi_one [simp]: "phi 1 = 0"
    1.32    by (auto simp add: phi_def card_eq_0_iff)
    1.33  
    1.34 +lemma phi_leq: "phi x \<le> nat x - 1"
    1.35 +proof -
    1.36 +  have "phi x \<le> card {1..x - 1}"
    1.37 +    unfolding phi_def by (rule card_mono) auto
    1.38 +  then show ?thesis by simp
    1.39 +qed
    1.40 +
    1.41 +lemma phi_nonzero:
    1.42 +  "phi x > 0" if "2 \<le> x"
    1.43 +proof -
    1.44 +  have "finite {y. 0 < y \<and> y < x}"
    1.45 +    by simp
    1.46 +  then have "finite {y. 0 < y \<and> y < x \<and> coprime y x}"
    1.47 +    by (auto intro: rev_finite_subset)
    1.48 +  moreover have "1 \<in> {y. 0 < y \<and> y < x \<and> coprime y x}"
    1.49 +    using that by simp
    1.50 +  ultimately have "card {y. 0 < y \<and> y < x \<and> coprime y x} \<noteq> 0"
    1.51 +    by auto
    1.52 +  then show ?thesis
    1.53 +    by (simp add: phi_def)
    1.54 +qed
    1.55 +
    1.56  lemma (in residues) phi_eq: "phi m = card (Units R)"
    1.57    by (simp add: phi_def res_units_eq)
    1.58  
    1.59 @@ -413,4 +440,60 @@
    1.60      by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
    1.61  qed
    1.62  
    1.63 +text {*
    1.64 +  This result can be transferred to the multiplicative group of
    1.65 +  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
    1.66 +
    1.67 +lemma mod_nat_int_pow_eq:
    1.68 +  fixes n :: nat and p a :: int
    1.69 +  assumes "a \<ge> 0" "p \<ge> 0"
    1.70 +  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
    1.71 +  using assms
    1.72 +  by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
    1.73 +
    1.74 +theorem residue_prime_mult_group_has_gen :
    1.75 + fixes p :: nat
    1.76 + assumes prime_p : "prime p"
    1.77 + shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
    1.78 +proof -
    1.79 +  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
    1.80 +  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
    1.81 +    by (simp add: prime_p)
    1.82 +  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
    1.83 +    by (auto simp add: R.zero_cong R.res_carrier_eq)
    1.84 +  obtain a where a:"a \<in> {1 .. int p - 1}"
    1.85 +         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
    1.86 +    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
    1.87 +    by (auto simp add: car[symmetric] carrier_mult_of)
    1.88 +  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
    1.89 +    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
    1.90 +  note * = this
    1.91 +  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
    1.92 +  proof
    1.93 +    { fix n assume n: "n \<in> ?L"
    1.94 +      then have "n \<in> ?R" using `p\<ge>2` by force
    1.95 +    } thus "?L \<subseteq> ?R" by blast
    1.96 +    { fix n assume n: "n \<in> ?R"
    1.97 +      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    1.98 +    } thus "?R \<subseteq> ?L" by blast
    1.99 +  qed
   1.100 +  have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   1.101 +  proof
   1.102 +    { fix x assume x: "x \<in> ?L"
   1.103 +      then obtain i where i:"x = nat (a^i mod (int p))" by blast
   1.104 +      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   1.105 +      hence "x \<in> ?R" using i by blast
   1.106 +    } thus "?L \<subseteq> ?R" by blast
   1.107 +    { fix x assume x: "x \<in> ?R"
   1.108 +      then obtain i where i:"x = nat a^i mod p" by blast
   1.109 +      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   1.110 +    } thus "?R \<subseteq> ?L" by blast
   1.111 +  qed
   1.112 +  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   1.113 +    using * a a_gen ** by presburger
   1.114 +  moreover
   1.115 +  have "nat a \<in> {1 .. p - 1}" using a by force
   1.116 +  ultimately show ?thesis ..
   1.117 +qed
   1.118 +
   1.119  end