summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 12 Apr 2017 09:27:43 +0200 | |

changeset 65465 | 067210a08a22 |

parent 65464 | f3cd78ba687c |

child 65466 | b0f89998c2a1 |

more fundamental euler's totient function on nat rather than int;
avoid generic name phi;
separate theory for euler's totient function

--- a/NEWS Wed Apr 12 13:48:07 2017 +0200 +++ b/NEWS Wed Apr 12 09:27:43 2017 +0200 @@ -66,6 +66,10 @@ fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space. INCOMPATIBILITY. +* Theory Totient in session Number_Theory introduces basic notions +about Euler's totient function previously hidden as solitary example +in theory Residues. Minor INCOMPATIBILITY. + * Session "Computional_Algebra" covers many previously scattered theories, notably Euclidean_Algorithm, Factorial_Ring, Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra, Normalized_Fraction,

--- a/src/HOL/Number_Theory/Euler_Criterion.thy Wed Apr 12 13:48:07 2017 +0200 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy Wed Apr 12 09:27:43 2017 +0200 @@ -17,17 +17,33 @@ private lemma p_minus_1_int: "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force -private lemma E_1: assumes "QuadRes p a" - shows "[a ^ ((p - 1) div 2) = 1] (mod (int p))" +private lemma E_1: + assumes "QuadRes (int p) a" + shows "[a ^ ((p - 1) div 2) = 1] (mod int p)" proof - - from assms obtain b where b: "[b ^ 2 = a] (mod p)" unfolding QuadRes_def by blast - hence "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod p)" + from assms obtain b where b: "[b ^ 2 = a] (mod int p)" + unfolding QuadRes_def by blast + then have "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod int p)" by (simp add: cong_exp_int cong_sym_int power_mult) - hence "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod p)" using odd_p by force - moreover have "~ p dvd b" - using b cong_altdef_int[of a 0 p] cong_dvd_eq_int[of "b ^ 2" a "int p"] p_a_relprime p_prime - by (auto simp: prime_dvd_power_int_iff) - ultimately show ?thesis using fermat_theorem[of p b] p_prime + then have "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod int p)" + using odd_p by force + moreover have "[b ^ (p - 1) = 1] (mod int p)" + proof - + have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)" + using p_prime proof (rule fermat_theorem) + show "\<not> p dvd nat \<bar>b\<bar>" + by (metis b cong_altdef_int cong_dvd_eq_int diff_zero int_dvd_iff p_a_relprime p_prime prime_dvd_power_int_iff prime_nat_int_transfer rel_simps(51)) + qed + then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p" + by (simp add: cong_nat_def) + then have "int (nat \<bar>b\<bar> ^ (p - 1) mod p) = int (1 mod p)" + by simp + moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)" + by (simp add: power_even_abs) + ultimately show ?thesis + by (simp add: zmod_int cong_int_def) + qed + ultimately show ?thesis by (auto intro: cong_trans_int) qed

--- a/src/HOL/Number_Theory/Pocklington.thy Wed Apr 12 13:48:07 2017 +0200 +++ b/src/HOL/Number_Theory/Pocklington.thy Wed Apr 12 09:27:43 2017 +0200 @@ -115,46 +115,6 @@ subsection\<open>Lucas's theorem\<close> -lemma phi_limit_strong: "phi(n) \<le> n - 1" -proof - - have "phi n = card {x. 0 < x \<and> x < int n \<and> coprime x (int n)}" - by (simp add: phi_def) - also have "... \<le> card {0 <..< int n}" - by (rule card_mono) auto - also have "... = card {0 <..< n}" - by (simp add: transfer_nat_int_set_functions) - also have "... \<le> n - 1" - by (metis card_greaterThanLessThan le_refl One_nat_def) - finally show ?thesis . -qed - -lemma phi_lowerbound_1: assumes n: "n \<ge> 2" - shows "phi n \<ge> 1" -proof - - have "finite {x. 0 < x \<and> x < n}" - by simp - then have "finite {x. 0 < x \<and> x < n \<and> coprime x n}" - by (auto intro: rev_finite_subset) - moreover have "{0::int <.. 1} \<subseteq> {x. 0 < x \<and> x < n \<and> coprime x n}" - using n by (auto simp add: antisym_conv) - ultimately have "card {0::int <.. 1} \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}" - by (rule card_mono) - also have "... = phi n" - by (simp add: phi_def) - finally show ?thesis - by simp -qed - -lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2" - shows "phi(int n) \<ge> 1" -by (metis n nat_le_iff nat_numeral phi_lowerbound_1) - -lemma euler_theorem_nat: - fixes m::nat - assumes "coprime a m" - shows "[a ^ phi m = 1] (mod m)" -by (metis assms le0 euler_theorem [transferred]) - lemma lucas_coprime_lemma: fixes n::nat assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)" @@ -181,22 +141,21 @@ lemma lucas_weak: fixes n::nat - assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)" - and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)" + assumes n: "n \<ge> 2" and an: "[a ^ (n - 1) = 1] (mod n)" + and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" shows "prime n" -proof- - from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+ - from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" . - from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)" - by auto - {assume "phi n \<noteq> n - 1" - with phi_limit_strong phi_lowerbound_1_nat [OF n] - have c:"phi n > 0 \<and> phi n < n - 1" - by (metis gr0I leD less_linear not_one_le_zero) - from nm[rule_format, OF c] afn have False ..} - hence "phi n = n - 1" by blast - with prime_phi phi_prime n1(1,2) show ?thesis - by auto +using \<open>n \<ge> 2\<close> proof (rule totient_prime) + show "totient n = n - 1" + proof (rule ccontr) + have "[a ^ totient n = 1] (mod n)" + by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"]) + (use n an in auto) + moreover assume "totient n \<noteq> n - 1" + then have "totient n > 0 \<and> totient n < n - 1" + using \<open>n \<ge> 2\<close> by (simp add: order_less_le) + ultimately show False + using nm by auto + qed qed lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" @@ -287,15 +246,22 @@ let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)" from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast from assms have o: "ord n a = Least ?P" by (simp add: ord_def) - {assume "n=0 \<or> n=1" with assms have "\<exists>m>0. ?P m" - by auto} - moreover - {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith - from assms have na': "coprime a n" - by (metis gcd.commute) - from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na'] - have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) } - ultimately have ex: "\<exists>m>0. ?P m" by blast + have ex: "\<exists>m>0. ?P m" + proof (cases "n \<ge> 2") + case True + moreover from assms have "coprime a n" + by (simp add: ac_simps) + then have "[a ^ totient n = 1] (mod n)" + by (rule euler_theorem) + ultimately show ?thesis + by (auto intro: exI [where x = "totient n"]) + next + case False + then have "n = 0 \<or> n = 1" + by auto + with assms show ?thesis + by auto + qed from nat_exists_least_iff'[of ?P] ex assms show ?thesis unfolding o[symmetric] by auto qed @@ -384,9 +350,9 @@ ultimately show ?rhs by blast qed -lemma order_divides_phi: - fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n" - by (metis ord_divides euler_theorem_nat gcd.commute) +lemma order_divides_totient: + "ord n a dvd totient n" if "coprime n a" + by (metis euler_theorem gcd.commute ord_divides that) lemma order_divides_expdiff: fixes n::nat and a::nat assumes na: "coprime n a" @@ -561,7 +527,8 @@ by auto} hence d1: "d = 1" by blast hence o: "ord p (a^r) = q" using d by simp - from pp phi_prime[of p] have phip: "phi p = p - 1" by simp + from pp prime_totient [of p] + have totient_eq: "totient p = p - 1" by simp {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1" from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast from n have "n \<noteq> 0" by simp @@ -570,7 +537,7 @@ hence cpa: "coprime p a" by auto have arp: "coprime (a^r) p" by (metis coprime_exp cpa gcd.commute) - from euler_theorem_nat[OF arp, simplified ord_divides] o phip + from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)" by simp then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast

--- a/src/HOL/Number_Theory/Residues.thy Wed Apr 12 13:48:07 2017 +0200 +++ b/src/HOL/Number_Theory/Residues.thy Wed Apr 12 09:27:43 2017 +0200 @@ -14,6 +14,7 @@ "~~/src/HOL/Algebra/More_Ring" "~~/src/HOL/Algebra/More_Finite_Product" "~~/src/HOL/Algebra/Multiplicative_Group" + Totient begin definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where @@ -244,129 +245,63 @@ subsection \<open>Euler's theorem\<close> -text \<open>The definition of the totient function.\<close> - -definition phi :: "int \<Rightarrow> nat" - where "phi m = card {x. 0 < x \<and> x < m \<and> coprime x m}" - -lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}" - unfolding phi_def -proof (rule bij_betw_same_card [of nat]) - show "bij_betw nat {x. 0 < x \<and> x < m \<and> coprime x m} {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}" - apply (auto simp add: inj_on_def bij_betw_def image_def) - apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) - apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int - transfer_int_nat_gcd(1) of_nat_less_iff) - done -qed - -lemma prime_phi: - assumes "2 \<le> p" "phi p = p - 1" - shows "prime p" +lemma (in residues) totient_eq: + "totient (nat m) = card (Units R)" proof - - have *: "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}" - using assms unfolding phi_def_nat - by (intro card_seteq) fastforce+ - have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat - proof - - from * have cop: "x \<in> {1..p - 1} \<Longrightarrow> coprime x p" - by blast - have "coprime x p" - apply (rule cop) - using ** apply auto - done - with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis - by auto - qed - then show ?thesis - using \<open>2 \<le> p\<close> - by (simp add: prime_nat_iff) - (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 - not_numeral_le_zero one_dvd) + have *: "inj_on nat (Units R)" + by (rule inj_onI) (auto simp add: res_units_eq) + have "totatives (nat m) = nat ` Units R" + by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1)) + (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)) + then have "card (totatives (nat m)) = card (nat ` Units R)" + by simp + also have "\<dots> = card (Units R)" + using * card_image [of nat "Units R"] by auto + finally show ?thesis + by simp qed -lemma phi_zero [simp]: "phi 0 = 0" - unfolding phi_def by (auto simp add: card_eq_0_iff) - -lemma phi_one [simp]: "phi 1 = 0" - by (auto simp add: phi_def card_eq_0_iff) +lemma (in residues_prime) totient_eq: "totient p = p - 1" + using totient_eq by (simp add: res_prime_units_eq) -lemma phi_leq: "phi x \<le> nat x - 1" -proof - - have "phi x \<le> card {1..x - 1}" - unfolding phi_def by (rule card_mono) auto - then show ?thesis by simp -qed - -lemma phi_nonzero: - "phi x > 0" if "2 \<le> x" +lemma (in residues) euler_theorem: + assumes "coprime a m" + shows "[a ^ totient (nat m) = 1] (mod m)" proof - - have "finite {y. 0 < y \<and> y < x}" - by simp - then have "finite {y. 0 < y \<and> y < x \<and> coprime y x}" - by (auto intro: rev_finite_subset) - moreover have "1 \<in> {y. 0 < y \<and> y < x \<and> coprime y x}" - using that by simp - ultimately have "card {y. 0 < y \<and> y < x \<and> coprime y x} \<noteq> 0" - by auto - then show ?thesis - by (simp add: phi_def) -qed - -lemma (in residues) phi_eq: "phi m = card (Units R)" - by (simp add: phi_def res_units_eq) - -lemma (in residues) euler_theorem1: - assumes a: "gcd a m = 1" - shows "[a^phi m = 1] (mod m)" -proof - - have "a ^ phi m mod m = 1 mod m" - by (metis assms finite_Units m_gt_one mod_in_res_units one_cong phi_eq pow_cong units_power_order_eq_one) + have "a ^ totient (nat m) mod m = 1 mod m" + by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one) then show ?thesis using res_eq_to_cong by blast qed -text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close> lemma euler_theorem: - assumes "m \<ge> 0" - and "gcd a m = 1" - shows "[a^phi m = 1] (mod m)" + fixes a m :: nat + assumes "coprime a m" + shows "[a ^ totient m = 1] (mod m)" proof (cases "m = 0 | m = 1") case True then show ?thesis by auto next case False with assms show ?thesis - by (intro residues.euler_theorem1, unfold residues_def, auto) + using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong + by (auto simp add: residues_def transfer_int_nat_gcd(1)) force qed -lemma (in residues_prime) phi_prime: "phi p = nat p - 1" - by (simp add: residues.phi_eq residues_axioms residues_prime.res_prime_units_eq residues_prime_axioms) - -lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1" - by (simp add: residues_prime.intro residues_prime.phi_prime) - lemma fermat_theorem: - fixes a :: int - assumes "prime (int p)" - and "\<not> p dvd a" - shows "[a^(p - 1) = 1] (mod p)" + fixes p a :: nat + assumes "prime p" and "\<not> p dvd a" + shows "[a ^ (p - 1) = 1] (mod p)" proof - - from assms have "[a ^ phi p = 1] (mod p)" - by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p] - simp: gcd.commute[of _ "int p"]) - also have "phi p = nat p - 1" - by (rule phi_prime) (rule assms) - finally show ?thesis - by (metis nat_int) + from assms prime_imp_coprime [of p a] have "coprime a p" + by (auto simp add: ac_simps) + then have "[a ^ totient p = 1] (mod p)" + by (rule euler_theorem) + also have "totient p = p - 1" + by (rule prime_totient) (rule assms) + finally show ?thesis . qed -lemma fermat_theorem_nat: - assumes "prime (int p)" and "\<not> p dvd a" - shows "[a ^ (p - 1) = 1] (mod p)" - using fermat_theorem [of p a] assms - by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int) - subsection \<open>Wilson's theorem\<close>

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Number_Theory/Totient.thy Wed Apr 12 09:27:43 2017 +0200 @@ -0,0 +1,164 @@ +(* Title: HOL/Number_Theory/Totient.thy + Author: Jeremy Avigad + Author: Florian Haftmann +*) + +section \<open>Fundamental facts about Euler's totient function\<close> + +theory Totient +imports + "~~/src/HOL/Computational_Algebra/Primes" +begin + +definition totatives :: "nat \<Rightarrow> nat set" + where "totatives n = {m. 0 < m \<and> m < n \<and> coprime m n}" + +lemma in_totatives_iff [simp]: + "m \<in> totatives n \<longleftrightarrow> 0 < m \<and> m < n \<and> coprime m n" + by (simp add: totatives_def) + +lemma finite_totatives [simp]: + "finite (totatives n)" + by (simp add: totatives_def) + +lemma totatives_subset: + "totatives n \<subseteq> {1..<n}" + by auto + +lemma totatives_subset_Suc_0 [simp]: + "totatives n \<subseteq> {Suc 0..<n}" + using totatives_subset [of n] by simp + +lemma totatives_0 [simp]: + "totatives 0 = {}" + using totatives_subset [of 0] by simp + +lemma totatives_1 [simp]: + "totatives 1 = {}" + using totatives_subset [of 1] by simp + +lemma totatives_Suc_0 [simp]: + "totatives (Suc 0) = {}" + using totatives_1 by simp + +lemma one_in_totatives: + assumes "n \<ge> 2" + shows "1 \<in> totatives n" + using assms by simp + +lemma minus_one_in_totatives: + assumes "n \<ge> 2" + shows "n - 1 \<in> totatives n" + using assms coprime_minus_one_nat [of n] by simp + +lemma totatives_eq_empty_iff [simp]: + "totatives n = {} \<longleftrightarrow> n \<in> {0, 1}" +proof + assume "totatives n = {}" + show "n \<in> {0, 1}" + proof (rule ccontr) + assume "n \<notin> {0, 1}" + then have "n \<ge> 2" + by simp + then have "1 \<in> totatives n" + by (rule one_in_totatives) + with \<open>totatives n = {}\<close> show False + by simp + qed +qed auto + +lemma prime_totatives: + assumes "prime p" + shows "totatives p = {1..<p}" +proof + show "{1..<p} \<subseteq> totatives p" + proof + fix n + assume "n \<in> {1..<p}" + with nat_dvd_not_less have "\<not> p dvd n" + by auto + with assms prime_imp_coprime [of p n] have "coprime p n" + by simp + with \<open>n \<in> {1..<p}\<close> show "n \<in> totatives p" + by (auto simp add: totatives_def ac_simps) + qed +qed auto + +lemma totatives_prime: + assumes "p \<ge> 2" and "totatives p = {1..<p}" + shows "prime p" +proof (rule ccontr) + from \<open>2 \<le> p\<close> have "1 < p" + by simp + moreover assume "\<not> prime p" + ultimately obtain n where "1 < n" "n < p" "n dvd p" + by (auto simp add: prime_nat_iff) + (metis Suc_lessD Suc_lessI dvd_imp_le dvd_pos_nat le_neq_implies_less) + then have "n \<in> {1..<p}" + by simp + with assms have "n \<in> totatives p" + by simp + then have "coprime n p" + by simp + with \<open>1 < n\<close> \<open>n dvd p\<close> show False + by simp +qed + +definition totient :: "nat \<Rightarrow> nat" + where "totient = card \<circ> totatives" + +lemma card_totatives [simp]: + "card (totatives n) = totient n" + by (simp add: totient_def) + +lemma totient_0 [simp]: + "totient 0 = 0" + by (simp add: totient_def) + +lemma totient_1 [simp]: + "totient 1 = 0" + by (simp add: totient_def) + +lemma totient_Suc_0 [simp]: + "totient (Suc 0) = 0" + using totient_1 by simp + +lemma prime_totient: + assumes "prime p" + shows "totient p = p - 1" + using assms prime_totatives + by (simp add: totient_def) + +lemma totient_eq_0_iff [simp]: + "totient n = 0 \<longleftrightarrow> n \<in> {0, 1}" + by (simp only: totient_def comp_def card_eq_0_iff) auto + +lemma totient_noneq_0_iff [simp]: + "totient n > 0 \<longleftrightarrow> 2 \<le> n" +proof - + have "totient n > 0 \<longleftrightarrow> totient n \<noteq> 0" + by blast + also have "\<dots> \<longleftrightarrow> 2 \<le> n" + by auto + finally show ?thesis . +qed + +lemma totient_less_eq: + "totient n \<le> n - 1" + using card_mono [of "{1..<n}" "totatives n"] by auto + +lemma totient_less_eq_Suc_0 [simp]: + "totient n \<le> n - Suc 0" + using totient_less_eq [of n] by simp + +lemma totient_prime: + assumes "2 \<le> p" "totient p = p - 1" + shows "prime p" +proof - + have "totatives p = {1..<p}" + by (rule card_subset_eq) (simp_all add: assms) + with assms show ?thesis + by (auto intro: totatives_prime) +qed + +end