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
```