src/HOL/Number_Theory/Residues.thy
changeset 66304 cde6ceffcbc7
parent 65899 ab7d8c999531
child 66305 7454317f883c
equal deleted inserted replaced
66303:210dae34b8bc 66304:cde6ceffcbc7
   376   then show ?thesis
   376   then show ?thesis
   377     using assms prime_ge_2_nat
   377     using assms prime_ge_2_nat
   378     by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
   378     by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
   379 qed
   379 qed
   380 
   380 
   381 text {*
   381 text \<open>
   382   This result can be transferred to the multiplicative group of
   382   This result can be transferred to the multiplicative group of
   383   $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
   383   $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close>
   384 
   384 
   385 lemma mod_nat_int_pow_eq:
   385 lemma mod_nat_int_pow_eq:
   386   fixes n :: nat and p a :: int
   386   fixes n :: nat and p a :: int
   387   assumes "a \<ge> 0" "p \<ge> 0"
   387   assumes "a \<ge> 0" "p \<ge> 0"
   388   shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   388   shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
   407     hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
   407     hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
   408   note * = this
   408   note * = this
   409   have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
   409   have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
   410   proof
   410   proof
   411     { fix n assume n: "n \<in> ?L"
   411     { fix n assume n: "n \<in> ?L"
   412       then have "n \<in> ?R" using `p\<ge>2` by force
   412       then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
   413     } thus "?L \<subseteq> ?R" by blast
   413     } thus "?L \<subseteq> ?R" by blast
   414     { fix n assume n: "n \<in> ?R"
   414     { fix n assume n: "n \<in> ?R"
   415       then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
   415       then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
   416     } thus "?R \<subseteq> ?L" by blast
   416     } thus "?R \<subseteq> ?L" by blast
   417   qed
   417   qed
   418   have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   418   have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
   419   proof
   419   proof
   420     { fix x assume x: "x \<in> ?L"
   420     { fix x assume x: "x \<in> ?L"
   421       then obtain i where i:"x = nat (a^i mod (int p))" by blast
   421       then obtain i where i:"x = nat (a^i mod (int p))" by blast
   422       hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   422       hence "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
   423       hence "x \<in> ?R" using i by blast
   423       hence "x \<in> ?R" using i by blast
   424     } thus "?L \<subseteq> ?R" by blast
   424     } thus "?L \<subseteq> ?R" by blast
   425     { fix x assume x: "x \<in> ?R"
   425     { fix x assume x: "x \<in> ?R"
   426       then obtain i where i:"x = nat a^i mod p" by blast
   426       then obtain i where i:"x = nat a^i mod p" by blast
   427       hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
   427       hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
   428     } thus "?R \<subseteq> ?L" by blast
   428     } thus "?R \<subseteq> ?L" by blast
   429   qed
   429   qed
   430   hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   430   hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
   431     using * a a_gen ** by presburger
   431     using * a a_gen ** by presburger
   432   moreover
   432   moreover