# Theory Sigma

Up to index of Isabelle/HOL/Perfect-Number-Thm

theory Sigma
imports PerfectBasics Infinite_Set
`header{*Sum of divisors function*}theory Sigmaimports PerfectBasics "~~/src/HOL/Library/Infinite_Set"begindefinition divisors :: "nat => nat set" where"divisors (m::nat) == {(n::nat) . (n::nat) dvd m}"definition sigma :: "nat => nat" where"sigma m == ∑ n  |n dvd m . n"lemma sigma_divisors: "sigma(n) = ∑ (divisors(n))"by (auto simp: sigma_def divisors_def)lemma divisors_eq_dvd[iff]: "(a:divisors(n)) = (a dvd n)"by(simp add: divisors_def)lemma mult_divisors: "(a::nat)*b=c==>a: divisors c"by (unfold divisors_def dvd_def,blast)lemma mult_divisors2: "(a::nat)*b=c==>b: divisors c"by (unfold divisors_def dvd_def,auto)lemma divisorsfinite[simp]:   assumes "n>0"   shows "finite (divisors n)"proof -  from assms have  "divisors n = {m . m dvd n & m <= n}"    by (auto simp only:divisors_def dvd_imp_le)  hence "divisors n <= {m . m<=n}" by auto  thus "finite (divisors n)"    by (metis finite_Collect_le_nat finite_subset) qedlemma divs_of_zero_UNIV[simp]: "divisors(0) = UNIV"by(auto simp add: divisors_def)lemma sigma0[simp]: "sigma(0) = 0"by (simp add: sigma_def)lemma sigma1[simp]: "sigma(1) = 1"by (simp add: sigma_def)lemma prime_divisors: "prime (p::nat) <-> divisors p = {1,p} & p>1"by (auto simp add: divisors_def prime_def)lemma prime_imp_sigma: "prime (p::nat) ==> sigma(p) = p+1"proof -  assume "prime (p::nat)"  hence "p>1 ∧ divisors(p) = {1,p}" by (simp add: prime_divisors)  hence "p>1 ∧ sigma(p) = ∑ {1,p}" by (auto simp only: sigma_divisors divisors_def)  thus "sigma(p) = p+1" by simpqedlemma sigma_third_divisor:  assumes  "1 < a" "a < n" "a : divisors n"  shows "1+a+n <= sigma(n)"proof -  from assms have "finite {1,a,n} & finite (divisors n) & {1,a,n} <= divisors n" by auto  hence "∑ {1,a,n} <= ∑ (divisors n)" by (simp only: setsum_mono2)  hence "∑ {1,a,n} <= sigma n" by (simp add: sigma_divisors)  with assms show "?thesis" by autoqedlemma sigma_imp_divisors: "sigma(n)=n+1 ==> n>1 & divisors n = {n,1}"proof  assume ass:"sigma(n)=n+1"  hence "n~=0 & n~=1"    by (metis Suc_eq_plus1 n_not_Suc_n sigma0 sigma1)  thus conc1: "n>1" by simp  show "divisors n = {n,1}" (*TODO: use sigma_third_divisor *)  proof (rule ccontr)    assume "divisors n ~= {n,1}"    with conc1 have "divisors n ~= {n,1} & 1<n" by auto    moreover    from ass conc1 have "1 : divisors(n) & n : divisors n & ~0 : divisors n"      by (simp add: dvd_def divisors_def)    ultimately    have  "(EX a. a~=n & a~=1 & 1<n & a : divisors n) & 0 ~: divisors n" by auto    hence "(EX a. a~=n & a~=1 & 1<n & a~=0 & a : divisors n)" by metis    hence "EX a . a~=n & a~=1 & 1~=n & a~=0 & finite {1,a,n} & finite (divisors n) & {1,a,n} <= divisors n" by auto    hence "EX a. a~=n & a~=1 & 1~=n & a~=0 & ∑ {1,a,n} <= sigma n"      by (metis setsum_mono2_nat sigma_divisors)    hence "EX a. a~=0 & (1+a+n) <= sigma n" by auto    hence "1+n<sigma n" by auto (*TODO: this step can be deleted, should i?*)    with ass show "False" by auto  qedqedlemma sigma_imp_prime: "sigma(n)=n+1 ==> prime n"proof -  assume ass: "sigma(n)=n+1"  hence "n>1 & divisors(n)={1,n}" by (metis insert_commute sigma_imp_divisors)  thus "prime n" by (simp add: prime_divisors)qedlemma pr_pow_div_eq_sm_pr_pow:   assumes prime: "prime p"  shows "{d . d dvd p^n} = {p^f| f . f<=n}"proof  show "{p^f | f . f<=n} <= { d .  d dvd p^n}"  proof    fix x    assume "x: {p ^ f | f . f <= n}"    hence "EX i . x = p^i & i<= n"   by auto    with prime have  "x dvd p^n" by (auto simp add: divides_primepow)    thus "x : { d . d dvd p^n}" by auto  qed  next  show "{d. d dvd p ^ n} <= {p ^ f | f . f <= n}"  proof    fix x    assume "x : {d . d dvd p^n}"    hence "x dvd p^n" by auto    with prime obtain "i" where  "i <= n & x = p^i"      by (auto simp only: divides_primepow)    hence "x = p^i & i <=n" by auto    thus "x : { p^f | f . f<=n }" by auto  qedqedlemma rewrite_sum_of_powers:assumes p: "(p::nat)>1"shows "(∑ {p^m | m . m<=(n::nat)}) = (∑ i = 0 .. n . p^i)" (is "?l = ?r")proof -  have "?l = setsum (%x. x) {(op ^ p) m |m . m<= n}" by auto  also have "... = setsum (%x. x) ((op ^ p)`{m . m<= n})"    by(rule seteq_imp_setsumeq) auto  moreover with p have "inj_on (op ^p) {m . m<=n}"    by (auto simp add: inj_on_def)  ultimately have "?l = setsum (op ^ p) {m . m<=n}"    by(auto simp only: setsum_reindex_id id_def)  moreover have "{m::nat . m<=n} = {0..n}" by auto  ultimately show "?l = (∑ i = 0 .. n . p^i)" by autoqedtheorem sigma_primepower:  "prime p ==> (p - 1)*sigma(p^(e::nat)) = (p^(e+1) - 1)"proof -  assume "prime p"  hence "sigma(p^(e::nat)) = (∑i=0 .. e . p^i)"    by (simp add: pr_pow_div_eq_sm_pr_pow sigma_def rewrite_sum_of_powers prime_def)  thus "(p - 1)*sigma(p^e)=p^(e+1) - 1" by (simp only: simplify_sum_of_powers)qedlemma sigma_prime_power_two: "sigma(2^(n::nat)) = 2^(n+1) - 1"proof -  have "(2 - 1)*sigma(2^(n::nat))=2^(n+1) - 1"    by (auto simp only: sigma_primepower two_is_prime)  thus ?thesis by simpqeddeclare [[simproc del: finite_Collect]]lemma prodsums_eq_sumprods:assumes "coprime p m"shows "(∑{p^f|f. f<=n})*(∑{b. b dvd m}) = (∑ {p^f*b| f b. f <= n & b dvd m})"proof-  have "ALL x f. x dvd m --> coprime (p ^ f) x"    by(metis assms coprime_commute coprime_divisors coprime_exp dvd.eq_iff)  thus ?thesis    by(auto simp: imp_ex setsum_mult_setsum_if_inj[OF mult_inj_if_coprime_nat]            intro!: arg_cong[where f = "setsum (%x. x)"])qeddeclare [[simproc add: finite_Collect]]lemma rewrite_for_sigma_semimultiplicative:assumes "prime p"shows "{p^f*b |f b. f<=n & b dvd m} = {a*b |a b. a dvd (p^n) & b dvd m}"proof  show "{p^f * b |f b. f <= n & b dvd m} <= {a*b |a b. a dvd p ^ n & b dvd m}"  proof    fix x    assume "x : {p ^ f * b | f b. f <= n & b dvd m}"    then obtain b f where "x = p^f*b & f <= n & b dvd m" by auto    with `prime p` show "x : {a * b |a b. a dvd p ^ n & b dvd m}"      by (auto simp add: divides_primepow)  qednext  show "{a*b |a b. a dvd p ^ n & b dvd m} <= {p^f * b |f b. f <= n & b dvd m}"    using `prime p` by auto (metis assms divides_primepow)qedlemma div_decomp_comp:  "coprime m n ==> a dvd m*n <-> (EX b c . a = b * c & b dvd m & c dvd n)"by (auto simp only: division_decomp mult_dvd_mono)(*TODO logischer volgorde maken *)theorem sigma_semimultiplicative:  assumes p: "prime p" and cop: "coprime p m"  shows "sigma (p^n) * sigma m = sigma (p^n * m)" (is "?l = ?r")proof -  from cop have cop2: "coprime (p^n) m"    by (auto simp add: coprime_exp coprime_commute)  have "?l = (∑ {a . a dvd p^n})*(∑ {b . b dvd m})" by (simp add: sigma_def)  also from p have "... = (∑ {p^f| f . f<=n})*(∑ {b . b dvd m})"    by (simp add: pr_pow_div_eq_sm_pr_pow)  also from cop  have "... = (∑ {p^f*b| f b . f<=n & b dvd m})"    by (auto simp add: prodsums_eq_sumprods prime_def)  also have "... = (∑ {a*b| a b . a dvd (p^n) & b dvd m})"    by(rule seteq_imp_setsumeq,rule rewrite_for_sigma_semimultiplicative[OF p])  finally have "?l = ∑{c. c dvd (p^n*m)}" by (subst div_decomp_comp[OF cop2])  thus "?l = sigma (p^n*m)" by (auto simp add: sigma_def)qedend`