src/HOL/Number_Theory/Residues.thy
 changeset 66304 cde6ceffcbc7 parent 65899 ab7d8c999531 child 66305 7454317f883c
equal 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`