src/HOL/Number_Theory/Residues.thy
changeset 65726 f5d64d094efe
parent 65465 067210a08a22
child 65899 ab7d8c999531
equal deleted 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>