src/HOL/Number_Theory/Residues.thy
 changeset 65726 f5d64d094efe parent 65465 067210a08a22 child 65899 ab7d8c999531
equal inserted replaced
65720:c5b19f997214 65726:f5d64d094efe
`    29 `
`    29 `
`    30 definition residue_ring :: "int \<Rightarrow> int ring"`
`    30 definition residue_ring :: "int \<Rightarrow> int ring"`
`    31 where`
`    31 where`
`    32   "residue_ring m =`
`    32   "residue_ring m =`
`    33     \<lparr>carrier = {0..m - 1},`
`    33     \<lparr>carrier = {0..m - 1},`
`    34      mult = \<lambda>x y. (x * y) mod m,`
`    34      monoid.mult = \<lambda>x y. (x * y) mod m,`
`    35      one = 1,`
`    35      one = 1,`
`    36      zero = 0,`
`    36      zero = 0,`
`    37      add = \<lambda>x y. (x + y) mod m\<rparr>"`
`    37      add = \<lambda>x y. (x + y) mod m\<rparr>"`
`    38 `
`    38 `
`    39 locale residues =`
`    39 locale residues =`
`   245 `
`   245 `
`   246 subsection \<open>Euler's theorem\<close>`
`   246 subsection \<open>Euler's theorem\<close>`
`   247 `
`   247 `
`   248 lemma (in residues) totient_eq:`
`   248 lemma (in residues) totient_eq:`
`   249   "totient (nat m) = card (Units R)"`
`   249   "totient (nat m) = card (Units R)"`
`       `
`   250   thm R_def`
`   250 proof -`
`   251 proof -`
`   251   have *: "inj_on nat (Units R)"`
`   252   have *: "inj_on nat (Units R)"`
`   252     by (rule inj_onI) (auto simp add: res_units_eq)`
`   253     by (rule inj_onI) (auto simp add: res_units_eq)`
`   253   have "totatives (nat m) = nat ` Units R"`
`   254   define m' where "m' = nat m"`
`   254     by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1))`
`   255   from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)`
`   255       (smt One_nat_def image_def mem_Collect_eq nat_0 nat_eq_iff nat_less_iff of_nat_1 transfer_int_nat_gcd(1))`
`   256   from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x`
`       `
`   257     unfolding res_units_eq`
`       `
`   258     by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)`
`       `
`   259   hence "Units R = int ` totatives m'" by blast`
`       `
`   260   hence "totatives m' = nat ` Units R" by (simp add: image_image)`
`   256   then have "card (totatives (nat m)) = card (nat ` Units R)"`
`   261   then have "card (totatives (nat m)) = card (nat ` Units R)"`
`   257     by simp`
`   262     by (simp add: m'_def)`
`   258   also have "\<dots> = card (Units R)"`
`   263   also have "\<dots> = card (Units R)"`
`   259     using * card_image [of nat "Units R"] by auto`
`   264     using * card_image [of nat "Units R"] by auto`
`   260   finally show ?thesis`
`   265   finally show ?thesis by (simp add: totient_def)`
`   261     by simp`
`       `
`   262 qed`
`   266 qed`
`   263 `
`   267 `
`   264 lemma (in residues_prime) totient_eq: "totient p = p - 1"`
`   268 lemma (in residues_prime) totient_eq: "totient p = p - 1"`
`   265   using totient_eq by (simp add: res_prime_units_eq)`
`   269   using totient_eq by (simp add: res_prime_units_eq)`
`   266 `
`   270 `
`   296   from assms prime_imp_coprime [of p a] have "coprime a p"`
`   300   from assms prime_imp_coprime [of p a] have "coprime a p"`
`   297     by (auto simp add: ac_simps)`
`   301     by (auto simp add: ac_simps)`
`   298   then have "[a ^ totient p = 1] (mod p)"`
`   302   then have "[a ^ totient p = 1] (mod p)"`
`   299      by (rule euler_theorem)`
`   303      by (rule euler_theorem)`
`   300   also have "totient p = p - 1"`
`   304   also have "totient p = p - 1"`
`   301     by (rule prime_totient) (rule assms)`
`   305     by (rule totient_prime) (rule assms)`
`   302   finally show ?thesis .`
`   306   finally show ?thesis .`
`   303 qed`
`   307 qed`
`   304 `
`   308 `
`   305 `
`   309 `
`   306 subsection \<open>Wilson's theorem\<close>`
`   310 subsection \<open>Wilson's theorem\<close>`