Theory Inversion

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory Inversion = NatIntLib + FiniteLib + Mu:

(*  Title:      Inversion.thy
Author:     Jeremy Avigad and David Gray
*)

header {* Moebius inversion and variants *}

theory Inversion = NatIntLib + FiniteLib + Mu:;

subsection {* The central lemma *}

locale MITEMP2 =
fixes n      :: "int"
fixes f      :: "(int * int) => ('b::plus_ac0)"
fixes S      :: "(int * int) set"
fixes R      :: "int => (int * int) set"
fixes U      :: "int => int set"
fixes T      :: "int => (int *int) set"
fixes V      :: "int => int set"

assumes n_gr_0: "0 < n"

defines S_def:  "S    == { (d,d'). d: {)0..n} & d':{)0..n} & (d * d') <= n }"
defines R_def:  "R d  == { (c,d'). c = d & d':{)0..n} & (d * d') <= n }"
defines U_def:  "U d  == { d'. d':{)0..n} & (d * d') <= n }"
defines T_def:  "T c  == { (d,d'). (d,d'):S & (d * d') = c }"
defines V_def:  "V c  == { d'. d':{)0..n} & d' dvd c }";

lemma (in MITEMP2) calc1: "(∑x:S. f(snd x, fst x)) =
(∑d:{)0..n}. (∑x:(R d). f(snd x, fst x)))";
proof-;
have "finite {)0..n}" by auto;
moreover have "ALL d:{)0..n}. finite (R d)"
proof;
fix d;
have "finite ({d::int} <*> {)0..n})" by auto;
moreover have "(R d) <= {d} <*> {)0..n}" by (auto simp add: R_def);
ultimately show "finite (R d)" by (auto simp add: finite_subset);
qed;
moreover have "ALL x:{)0..n}. ALL y:{)0..n}. x ~= y --> (R x) Int (R y) = {}";
ultimately have "setsum (%x. f(snd x, fst x)) (UNION {)0..n} R) =
(∑d:{)0..n}. setsum (%x. f(snd x, fst x)) (R d))";
moreover have "S = UNION {)0..n} R";
by (auto simp add: S_def R_def);
ultimately show "setsum (%x. f(snd x, fst x)) S =
(∑d:{)0..n}. setsum (%x. f(snd x, fst x)) (R d))";
by auto;
qed;

lemma (in MITEMP2) calc2: "(∑d:{)0..n}. (∑x:(R d). f(snd x, fst x))) =
(∑d:{)0..n}. (∑x:(R d). f(snd x, d)))";
apply (rule setsum_cong, auto);
apply (rule setsum_cong);
apply (rule refl);
apply (subgoal_tac "fst xa = x");
apply force;
apply (unfold R_def);
apply auto;
done;

lemma (in MITEMP2) calc3: "(∑d:{)0..n}. (∑x:(R d). f(snd x, d))) =
(∑d:{)0..n}. (∑x:(U d). f(x, d)))";
apply (rule setsum_cong, auto);
proof-;
fix x;
have "finite (R x)";
proof-;
have "finite ({x} <*> {)0..n})" by auto;
moreover have "(R x) <= {x} <*> {)0..n}" by (auto simp add: R_def);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;
moreover have "inj_on snd (R x)" by (auto simp add: inj_on_def R_def);
ultimately have "setsum ((%xa. f(xa, x)) ˆ snd) (R x) =
setsum (%xa. f(xa, x)) (snd ` R x)";
by (auto simp add: setsum_reindex [THEN sym]);
moreover have "snd ` (R x) = U x" by (auto simp add: image_def R_def U_def);
ultimately have "setsum (%xa. f(snd xa, x)) (R x) =
setsum (%xa. f(xa, x)) (U x)";
thus "(∑xa:R x. f (snd xa, x)) = (∑xa:U x. f (xa, x))".;
qed;

lemma (in MITEMP2) calc4: "(∑x:S. f(snd x, fst x)) =
(∑c:{)0..n}. (∑x:(T c). f(snd x, fst x)))";
proof-;
have "finite {)0..n}" by auto;
moreover have "ALL c:{)0..n}. finite (T c)"
proof;
fix c;
have "finite ({)0..n} <*> {)0..n})" by auto;
moreover have "(T c) <= {)0..n} <*> {)0..n}"
by (auto simp add: T_def S_def);
ultimately show "finite (T c)" by (auto simp add: finite_subset);
qed;
moreover have "ALL x:{)0..n}. ALL y:{)0..n}. x ~= y -->
(T x) Int (T y) = {}";
ultimately have "setsum (%x. f(snd x, fst x)) (UNION {)0..n} T) =
(∑d:{)0..n}. setsum (%x. f(snd x, fst x)) (T d))";
moreover have "S = UNION {)0..n} T";
by (auto simp add: S_def T_def zero_less_mult_iff);
ultimately show "setsum (%x. f(snd x, fst x)) S =
(∑d:{)0..n}. setsum (%x. f(snd x, fst x)) (T d))";
by (auto);
qed;

lemma aux1: "[| 0 < (x::int); x <= n; 0 < y; y <= n; y dvd x |] ==>
x < n * y + y";
proof-;
assume "0 < x" and "x <= n" and "0 < y" and "y <= n" and "y dvd x";
then have "x * 1 <= n * y"
apply (intro mult_mono);
apply (insert prems, auto);
done;
qed;

lemma (in MITEMP2) calc5:
"(∑c:{)0..n}. (∑x:(T c). f(snd x, fst x))) =
(∑c:{)0..n}. (∑d:(V c). f(snd(d, c div d), fst(d, c div d))))";
apply (rule setsum_cong, auto);
proof-;
fix x;
assume p1:"0 < x" and p2:"x <= n";
have f_V: "finite (V x)";
proof-;
have "finite {)0..n}" by auto;
moreover have "(V x) <= {)0..n}" by (auto simp add: V_def);
ultimately show ?thesis by (auto simp add: finite_subset);
qed;
moreover have "inj_on (%d. (d, x div d)) (V x)";
by (auto simp add: V_def inj_on_def);
ultimately have "setsum ((%y. f(snd y, fst y)) ˆ (%d. (d, x div d))) (V x) =
setsum (%y. f(snd y, fst y)) ((%d. (d, x div d)) ` V x)";
by (auto simp add: setsum_reindex [THEN sym]);
moreover have "(%d. (d, x div d)) ` (V x) = (T x)";
apply (auto simp add: V_def T_def S_def image_def);
apply (rule zdiv_gr_zero, auto simp add: p1 p2);
apply (rule div_prop2, auto simp add: p1 p2 aux1);
apply (insert prems, auto simp add: int_dvd_times_div_cancel);
done;
ultimately have "setsum (%y. f(snd(y, x div y), fst(y, x div y))) (V x) =
setsum (%y. f(snd y, fst y)) (T x)";
then have "setsum (%y. f(x div y, y)) (V x) =
setsum (%y. f(snd y, fst y)) (T x)";
by (auto);
thus "(∑x:T x. f (snd x, fst x)) = (∑d:V x. f (x div d, d))" by auto;
qed;

lemma (in MITEMP2) calc6:
"(∑c:{)0..n}. (∑d:(V c). f(snd(d, c div d), fst(d, c div d)))) =
(∑c:{)0..n}. (∑d:(V c). f(c div d, d)))";
by auto;

lemma (in MITEMP2) calc7:
"(∑d:{)0..n}. (∑d':(U d). f(d', d))) =
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f(d', d)))";
apply (rule setsum_cong, auto);
apply (subgoal_tac "(U x) = {)0..n div x}", auto simp add: U_def);
proof-;
fix x and xa;
assume "0 < x" and "x * xa <= n";
then have "(x * xa) div x <= n div x";
by (insert zdiv_mono1 [of "x*xa" "n" "x"], auto);
also have "(x * xa) div x = xa";
by (insert prems, rule zdiv_zmult_self2, auto);
finally show "xa <= n div x".;
next;
fix x and xa;
assume "0 < x" and "xa <= n div x";
then have "n div x <= n div 1";
by (rule_tac a = n in zdiv_mono2, insert n_gr_0, auto);
then have "n div x <= n" by auto;
thus "xa <= n" by (insert prems, auto);
next;
fix x and xa;
assume "0 < x" and "xa <= n div x";
moreover have "0 <= x" by (insert prems, auto);
ultimately have "x * xa <= x * (n div x)";
moreover have "x * (n div x) <= n";
by (insert prems, rule zdiv_leq_prop, auto);
ultimately show "x * xa <= n" by auto;
qed;

lemma (in MITEMP2) inv_short:
"(∑d:{)0..n}. (∑d':{)0..(n div d)}. f(d', d))) =
(∑c:{)0..n}. (∑d:(V c). f(c div d, d)))";
by (insert calc1 calc2 calc3 calc4 calc5 calc6 calc7, auto);

theorem general_inversion_aux: "0 < (n::int) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f(d', d))) =
(∑c:{)0..n}. (∑d: {d'. d':{)0..n} & d' dvd c }. f(c div d, d)))";
by (auto simp add: MITEMP2_def MITEMP2.inv_short);

subsection {* General inversion laws *}

lemma general_inversion_int1: "0 < (n::int) ==>
(∑x:{x. 0 < x & x dvd n}. f x) = (∑x:{x. 0 < x & x dvd n}. f (n div x))";
apply (rule setsum_reindex_cong');
apply (erule finite_int_dvd_set);
apply (rule inj_onI);
apply (erule int_inj_div);
apply auto;
apply (unfold image_def);
apply clarify;
apply (rule_tac x = "n div x" in bexI);
apply (rule int_div_div [THEN sym]);
apply auto;
apply (erule zdiv_gr_zero);
apply auto;
apply (erule zero_less_mult_pos);
apply assumption;
done;

lemma general_inversion_int2: "0 < (n::int) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. (f d d'))) =
(∑c:{)0..n}. (∑d: {d. 0 < d & d dvd c}. (f d (c div d))))";
apply (insert general_inversion_aux [of n "%x. (f (snd x) (fst x))"]);
apply simp;
apply (rule setsum_cong);
apply auto;
apply (rule setsum_cong);
apply auto;
apply (frule zdvd_imp_le);
apply assumption;
apply (erule order_trans);
apply assumption;
done;

lemma general_inversion_int2_cor1: "0 < (n::int) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. (f d d'))) =
(∑d':{)0..n}. (∑d:{)0..(n div d')}. (f d d')))";
apply (subst general_inversion_int2);
apply assumption;
apply (subst general_inversion_int2);
apply assumption;
apply (rule setsum_cong2);
apply (subst general_inversion_int1);
apply force;
apply (rule setsum_cong2);
apply (subst int_div_div);
apply auto;
done;

lemma general_inversion_int2_cor2: "0 < (n::int) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f d')) =
(∑c:{)0..n}. (∑d: {d. 0 < d & d dvd c}. f (c div d)))";
by (rule general_inversion_int2);

lemma general_inversion_int2_cor3: "0 < (n::int) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f d')) =
(∑d:{)0..n}. of_int (n div d) * f d)";
apply (subst general_inversion_int2_cor1);
apply assumption;
apply (rule setsum_cong2);
apply (subst setsum_constant);
apply simp;
apply simp;
apply (subgoal_tac "of_int(n div x) = of_int(of_nat(nat(n div x)))");
apply (erule ssubst);
apply (subst of_int_of_nat_eq);
apply (rule refl);
apply (subst int_eq_of_nat [THEN sym]);
apply (subst nat_0_le);
apply (rule int_nonneg_div_nonneg);
apply auto;
done;

lemma general_inversion_int3: "0 < (n::int) ==>
(∑d:{d. 0 < d & d dvd n}.
(∑d':{d'.0 < d' & d' dvd (n div d)}. (f d' d))) =
(∑c:{c. 0 < c & c dvd n}.
(∑d: {d. 0 < d & d dvd c}. (f (c div d) d)))";
proof -;
assume "0 < n";
let ?f1 = "%d' d. if (d dvd n & d' dvd (n div d)) then f d' d else 0";
have "(∑d:{)0..n}. ∑d':{)0..n div d}. ?f1 d' d) =
(∑c:{)0..n}. ∑d:{d. 0 < d & d dvd c}. ?f1 (c div d) d)"
(is "?LHS = ?RHS");
by (intro general_inversion_int2);
also have "?LHS = (∑d:{d. 0 < d & d dvd n}.
(∑d':{d'.0 < d' & d' dvd (n div d)}. (f d' d)))" (is "?LHS = ?RHS2");
proof -;
have "?LHS = (∑d:{d. 0 < d & d dvd n}. ∑d':{)0..n div d}. ?f1 d' d) +
(∑d:{d. d:{)0..n} & ~ (d dvd n)}. ∑d':{)0..n div d}. ?f1 d' d)"
(is "?LHS = ?term1 + ?term2");
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_int_dvd_set, rule prems);
apply (rule finite_subset_GreaterThan0AtMost_int);
apply force;
apply force;
apply (rule setsum_cong);
apply auto;
apply (erule zdvd_imp_le, rule prems);
done;
also have "?term2 = 0";
apply (rule setsum_0');
apply auto;
apply (rule setsum_0');
apply auto;
done;
also have "?term1 + 0 = ?term1";
by simp;
also; have "?term1 = ?RHS2";
apply (rule setsum_cong2);
apply (subgoal_tac "{)0..n div x} = {d'. 0 < d' & d' dvd n div x} Un
{d'. 0 < d' & ~(d' dvd n div x) & d' <= n div x}");
apply (erule ssubst);
apply (subst setsum_Un_disjoint);
apply (rule finite_int_dvd_set);
apply (clarsimp);
apply (rule zdiv_gr_zero);
apply assumption;
apply (rule prems);
apply assumption;
apply (rule finite_subset_GreaterThan0AtMost_int);
apply force;
apply force;
apply (subgoal_tac "(∑d':{d'. 0 < d' & ~ d' dvd n div x &
d' <= n div x}.
if x dvd n & d' dvd n div x then f d' x else 0) = 0");
apply (erule ssubst);
apply simp;
apply (rule setsum_cong2);
apply (clarsimp);
apply (rule setsum_0');
apply clarsimp;
apply auto;
apply (erule zdvd_imp_le);
apply (rule zdiv_gr_zero);
apply (assumption, rule prems, assumption);
done;
finally show ?thesis;.;
qed;
also have "?RHS = (∑c:{c. 0 < c & c dvd n}.
(∑d: {d. 0 < d & d dvd c}. (f (c div d) d)))" (is "?RHS = ?LHS2");
proof -;
have "?RHS = (∑c:{c. 0 < c & c dvd n}.
∑d:{d. 0 < d & d dvd c}. ?f1 (c div d) d) +
(∑c:{c. 0 < c & c <= n & ~(c dvd n)}.
∑d:{d. 0 < d & d dvd c}. ?f1 (c div d) d)"
(is "?RHS = ?term1 + ?term2");
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_int_dvd_set);
apply (rule prems);
apply (rule finite_subset_GreaterThan0AtMost_int);
apply force;
apply force;
apply (rule setsum_cong);
apply auto;
apply (rule zdvd_imp_le);
apply (assumption, rule prems);
done;
also have "?term2 = 0";
apply (rule setsum_0');
apply clarsimp;
apply (rule setsum_0');
apply clarsimp;
apply (subgoal_tac "a dvd n");
apply force;
apply (subgoal_tac "(a dvd n) = (aa * (a div aa) dvd aa * (n div aa))");
apply (erule ssubst);
apply (rule zdvd_zmult_mono);
apply simp;
apply assumption;
apply (subst int_dvd_times_div_cancel2);
apply assumption+;
apply (subst int_dvd_times_div_cancel2);
apply (assumption+, rule refl);
done;
also; have "?term1 + 0 = ?term1";
by simp;
also have "... = ?LHS2";
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply auto;
apply (erule notE);
apply (erule zdvd_trans);
apply assumption;
apply (erule notE);
apply (subgoal_tac "xa * (x div xa) dvd xa * (n div xa)");
apply (rule ne_0_zdvd_prop);
prefer 2;
apply assumption;
apply force;
apply (subst int_dvd_times_div_cancel2);
apply assumption+;
apply (erule zdvd_trans, assumption);
apply (subst int_dvd_times_div_cancel2);
apply assumption+;
done;
finally show ?thesis;.;
qed;
finally show ?thesis;.;
qed;

lemma general_inversion_nat1: "0 < (n::nat) ==>
(∑x:{x. x dvd n}. f x) = (∑x:{x. x dvd n}. f (n div x))";
proof -;
assume "0 < (n::nat)";
have "(∑x:{x. 0 < x & x dvd (int n)}. (f o nat) x) =
(∑x:{x. 0 < x & x dvd (int n)}. (f o nat) ((int n) div x))"
(is "?LHS = ?RHS");
apply (rule general_inversion_int1);
done;
also have "?LHS = (∑x:{x. x dvd n}. ((f o nat) o int) x)";
apply (rule setsum_reindex_cong);
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (subst image_int_dvd_set);
apply (rule prems);
apply (rule refl)+;
done;
also have "((f o nat) o int) = f";
also have "?RHS =
(∑x:{x. x dvd n}. ((f o nat) o int) (n div x))";
apply (rule setsum_reindex_cong);
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (subgoal_tac "inj_on int {x. x dvd n}");
apply assumption;
apply (subst image_int_dvd_set);
apply (rule prems);
apply (rule refl);
apply (simp add: o_def int_div [THEN sym]);
done;
also have "((f o nat) o int) = f";
finally show ?thesis;.;
qed;

lemma general_inversion_nat2: "0 < (n::nat) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. (f d d'))) =
(∑c:{)0..n}. (∑d: {d. d dvd c}. (f d (c div d))))";
proof -;
assume "0 < (n::nat)";
have "(∑d:{)0..int n}. (∑d':{)0..((int n) div d)}. (f (nat d) (nat d')))) =
(∑c:{)0..(int n)}. (∑d: {d. 0 < d & d dvd c}.
(f (nat d) (nat (c div d)))))" (is "?LHS = ?RHS");
apply (rule general_inversion_int2);
done;
also have "?LHS = (∑d:{)0..n}. (∑d':{)0..(n div d)}. (f d d')))";
apply (rule setsum_reindex_cong');
apply simp;
apply (subgoal_tac "inj_on int {)0..n}");
apply assumption;
apply (subst image_int_GreaterThanAtMost);
apply simp;
apply (rule ext);
apply (rule sym);
apply (rule setsum_reindex_cong);
apply simp;
apply (subgoal_tac "inj_on int {)0..n div d}");
apply assumption;
apply (subst image_int_GreaterThanAtMost);
apply (subst int_div);
apply simp;
done;
also have "?RHS = (∑c:{)0..n}. (∑d: {d. d dvd c}. (f d (c div d))))";
apply (rule setsum_reindex_cong'');
apply simp;
apply (subgoal_tac "inj_on int {)0..n}");
apply assumption;
apply (subst image_int_GreaterThanAtMost);
apply simp;
apply clarsimp;
apply (rule sym);
apply (rule setsum_reindex_cong');
apply (rule finite_nat_dvd_set);
apply assumption;
apply (subgoal_tac "inj_on int {d. d dvd x}");
apply assumption;
apply (subst image_int_dvd_set);
apply (assumption, rule refl);
apply (simp add: int_div [THEN sym]);
done;
finally show ?thesis;.;
qed;

lemma general_inversion_nat2_cor1: "0 < (n::nat) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. (f d d'))) =
(∑d':{)0..n}. (∑d:{)0..(n div d')}. (f d d')))";
apply (subst general_inversion_nat2);
apply assumption;
apply (subst general_inversion_nat2);
apply assumption;
apply (rule setsum_cong2);
apply (subst general_inversion_nat1);
apply force;
apply (rule setsum_cong2);
apply simp;
apply (subst nat_div_div);
apply auto;
done;

lemma general_inversion_nat2_cor2: "0 < (n::nat) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f d')) =
(∑c:{)0..n}. (∑d: {d. d dvd c}. f (c div d)))";
by (rule general_inversion_nat2);

lemma general_inversion_nat2_cor3: "0 < (n::nat) ==>
(∑d:{)0..n}. (∑d':{)0..(n div d)}. f d')) =
(∑d:{)0..n}. of_nat (n div d) * f d)";
apply (subst general_inversion_nat2_cor1);
apply assumption;
apply (rule setsum_cong2);
apply (subst setsum_constant);
apply simp;
apply simp;
done;

lemma general_inversion_nat3: "0 < (n::nat) ==>
(∑d:{d. d dvd n}.
(∑d':{d'. d' dvd (n div d)}. (f d' d))) =
(∑c:{c. c dvd n}.
(∑d: {d. d dvd c}. (f (c div d) d)))"
(is "0 < n ==> ?LHS = ?RHS");
proof -;
assume "0 < (n::nat)";
have "(∑d:{d. 0 < d & d dvd (int n)}.
(∑d':{d'.0 < d' & d' dvd ((int n) div d)}. (f (nat d') (nat d)))) =
(∑c:{c. 0 < c & c dvd (int n)}.
(∑d: {d. 0 < d & d dvd c}. (f (nat (c div d)) (nat d))))"
(is "?LHS2 = ?RHS2");
apply (rule general_inversion_int3);
done;
also have "?LHS2 = ?LHS";
apply (rule setsum_reindex_cong'');
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (subgoal_tac "inj_on int {d. d dvd n}");
apply assumption;
apply (subst image_int_dvd_set);
apply (rule prems);
apply (rule refl);
apply clarify;
apply (rule sym);
apply (rule setsum_reindex_cong);
apply (rule finite_nat_dvd_set);
apply (rule nat_pos_div_dvd_gr_0);
apply (rule prems);
apply (assumption);
apply (subgoal_tac "inj_on int {d'. d' dvd n div x}");
apply assumption;
apply (subst image_int_dvd_set);
apply (rule nat_pos_div_dvd_gr_0, rule prems, assumption);
apply (subst int_div);
apply (rule refl);
done;
also have "?RHS2 = ?RHS";
apply (rule setsum_reindex_cong'');
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (subgoal_tac "inj_on int {c. c dvd n}");
apply assumption;
apply (subst image_int_dvd_set);
apply (rule prems, rule refl);
apply clarsimp;
apply (rule sym);
apply (rule setsum_reindex_cong');
apply (rule finite_nat_dvd_set);
apply (erule nat_pos_dvd_pos);
apply (rule prems);
apply (subgoal_tac "inj_on int {d. d dvd x}");
apply assumption;
apply (subst image_int_dvd_set);
apply (erule nat_pos_dvd_pos, rule prems);
apply (rule refl);
apply (simp add: int_div [THEN sym]);
done;
finally show ?thesis;.;
qed;

subsection {* Moebius inversion *}

lemma moebius_prop2: "0 < n ==> setsum mu {d. 0 < d ∧ d dvd n} =
(if n = 1 then 1 else 0)";
apply (rule moebius_prop, force);
done;

lemma moebius_prop_nat: "0 < n ==> setsum (%x. mu(int x))
{d. d dvd n} = (if n = 1 then 1 else 0)"
(is "0 < n ==> ?LHS = ?RHS");
proof -;
assume "0 < n";
have "setsum mu {d. 0 < d ∧ d dvd (int n)} =
(if (int n) = 1 then 1 else 0)" (is "?LHS2 = ?RHS2");
apply (rule moebius_prop2);
done;
also have "?LHS2 = ?LHS";
apply (rule setsum_reindex_cong');
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (subgoal_tac "inj_on int {d. d dvd n}");
apply assumption;
apply (subst image_int_dvd_set);
apply (rule prems);
apply (rule refl)+;
done;
also have "?RHS2 = ?RHS";
by simp;
finally show ?thesis;.;
qed;

lemma moebius_prop_nat_general: "0 < n ==>
(∑x∈{d. d dvd n}. of_int(mu (int x))) = (if n = 1 then 1 else 0)";
apply (subst setsum_of_int' [THEN sym]);
apply (subst moebius_prop_nat);
apply assumption;
apply simp;
done;

lemma moebius_prop_int_general: "0 < n ==>
(∑x∈{d. 0 < d & d dvd n}. of_int(mu x)) = (if n = 1 then 1 else 0)";
apply (subst setsum_of_int' [THEN sym]);
apply (subst moebius_prop2);
apply assumption;
apply simp;
done;

lemma mu_aux: "0 < (x::nat) ==>
(setsum (%x. f x * (if x = 1 then 1 else 0))) {d. d dvd x} =
((f 1)::'a::semiring)";
apply (subgoal_tac "{d. d dvd x} = {1} Un {d. d dvd x & d ~= 1}");
apply (erule ssubst);
apply (subst setsum_Un_disjoint);
apply simp;
apply (rule finite_subset);
apply (subgoal_tac "{d. d dvd x & d ~= 1} <= {d. d dvd x}");
apply assumption;
apply force;
apply (rule finite_nat_dvd_set);
apply assumption;
apply simp_all;
apply (subgoal_tac "(∑x∈{d. d dvd x & d ~= Suc 0}. f x *
(if x = Suc 0 then 1 else 0)) = 0");
apply simp;
apply (rule setsum_0');
apply auto;
done;

lemma mu_aux2: "0 < x ==>
(setsum (%x. f x * (if x = 1 then 1 else 0))) {)0..(x::nat)} =
((f 1)::'a::semiring)";
apply (subgoal_tac "{)0..x} = {1} Un {)1..x}");
apply (erule ssubst);
apply (subst setsum_Un_disjoint);
apply simp_all;
apply (subgoal_tac "(∑x∈{)Suc 0..x}. f x *
(if x = Suc 0 then 1 else 0)) = 0");
apply simp;
apply (rule setsum_0');
apply auto;
done;

lemma mu_inversion_nat1: "0 < (n::nat) ==> g n =
(∑d:{d. d dvd n}. (∑d':{d'. d' dvd (n div d)}.
of_int(mu(int d)) * g((n div d) div d')))"
(is "0 < n ==> g n = ?sum");
proof -;
assume "0 < n";
then have "?sum = (∑c∈{c. c dvd n}. ∑d∈{d. d dvd c}.
of_int (mu (int d)) * g (n div d div (c div d)))";
by (subst general_inversion_nat3, assumption, simp);
also have "… = (∑c∈{c. c dvd n}. ∑d∈{d. d dvd c}.
g(n div c) * of_int (mu (int d)))";
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst nat_div_div_eq_div);
apply force;
apply clarify;
apply (erule nat_pos_dvd_pos);
apply (rule prems);
done;
also have "… = (∑c∈{c. c dvd n}. g(n div c) * (∑d∈{d. d dvd c}.
of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "… = (∑c∈{c. c dvd n}. g(n div c) * (if c = 1 then 1
else 0))";
apply (rule setsum_cong2);
apply (subst moebius_prop_nat_general);
apply auto;
apply (rule nat_pos_dvd_pos);
apply (assumption, rule prems);
done;
also have "… = g n";
apply (subst mu_aux);
apply (rule prems);
apply simp;
done;
finally show ?thesis; by (rule sym);
qed;

lemma mu_inversion_nat1a: "ALL n. (0 < n -->
f n = (∑d:{d. d dvd n}. g(n div d))) ==> 0 < (n::nat) ==>
g n = (∑d:{d. d dvd n}. of_int(mu(int(d))) * f (n div d))";
proof -;
assume "ALL n. (0 < n --> f n = (∑d:{d. d dvd n}. g(n div d)))";
assume "0 < n";
show "g n = (∑d:{d. d dvd n}. of_int(mu(int(d))) * f (n div d))"
(is "g n = ?sum");
proof -;
have "?sum = (∑d:{d. d dvd n}. of_int(mu(int(d))) *
(∑d':{d'. d' dvd (n div d)}. g((n div d) div d')))";
apply (rule setsum_cong2);
apply (insert prems);
apply (drule_tac x = "n div x" in spec);
apply (subgoal_tac "0 < n div x");
apply force;
apply (rule nat_pos_div_dvd_gr_0);
apply auto;
done;
also have "… = (∑d:{d. d dvd n}. (∑d':{d'. d' dvd (n div d)}.
of_int(mu(int(d))) * g((n div d) div d')))";
apply (rule setsum_cong2);
apply (subst setsum_const_times);
apply (rule refl);
done;
also have "… = g n";
apply (subst mu_inversion_nat1);
apply (rule prems);
apply (rule refl);
done;
finally show ?thesis; by (rule sym);
qed;
qed;

lemma mu_inversion_nat2: "0 < (n::nat) ==> f n =
(∑d:{d. d dvd n}. (∑d':{d'. d' dvd (n div d)}.
of_int(mu(int d')) * f((n div d) div d')))"
(is "0 < n ==> f n = ?sum");
proof -;
assume "0 < n";
then have "?sum = (∑c∈{c. c dvd n}. ∑d∈{d. d dvd c}.
of_int (mu (int (c div d))) * f (n div d div (c div d)))";
by (subst general_inversion_nat3, assumption, simp);
also have "… =  (∑c∈{c. c dvd n}. ∑d∈{d. d dvd c}.
(of_int (mu (int d)) * f (n div (c div d) div d)))";
apply (rule setsum_cong2);
apply (subst general_inversion_nat1);
apply (insert prems);
apply clarify;
apply (erule nat_pos_dvd_pos);
apply assumption;
apply (rule setsum_cong2);
apply (subst nat_div_div);
apply auto;
apply (erule nat_pos_dvd_pos);
apply assumption;
done;
also have "… = (∑c∈{c. c dvd n}. ∑d∈{d. d dvd c}.
(f (n div c) * of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst div_mult2_eq [THEN sym]);
apply (subst mult_commute);back;back;
apply (subst nat_dvd_mult_div);
apply clarsimp;
apply (erule nat_pos_dvd_pos);
apply (erule nat_pos_dvd_pos);
apply (rule prems);
apply force;
done;
also have "… = (∑c∈{c. c dvd n}. f(n div c) * (∑d∈{d. d dvd c}.
of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "… = (∑c∈{c. c dvd n}. f(n div c) * (if c = 1 then 1
else 0))";
apply (rule setsum_cong2);
apply (subst moebius_prop_nat_general);
apply auto;
apply (rule nat_pos_dvd_pos);
apply (assumption, rule prems);
done;
also have "… = f n";
apply (subst mu_aux);
apply (rule prems);
apply simp;
done;
finally show ?thesis; by (rule sym);
qed;

lemma mu_inversion_nat2a: "ALL n. (0 < n -->
g n = (∑d:{d. d dvd n}. of_int(mu(int(d))) * f(n div d))) ==>
0 < (n::nat) ==> f n = (∑d:{d. d dvd n}. g (n div d))";
proof -;
assume "ALL n. (0 < n -->
g n = (∑d:{d. d dvd n}. of_int(mu(int(d))) * f(n div d)))";
assume "0 < n";
show "f n = (∑d:{d. d dvd n}. g (n div d))" (is "f n = ?sum");
proof -;
have "?sum = (∑d:{d. d dvd n}. (∑d':{d'. d' dvd (n div d)}.
of_int(mu(int(d'))) * f((n div d) div d')))";
apply (rule setsum_cong2);
apply (insert prems);
apply (drule_tac x = "n div x" in spec);
apply (subgoal_tac "0 < n div x");
apply force;
apply (rule nat_pos_div_dvd_gr_0);
apply auto;
done;
also have "… = f n";
apply (subst mu_inversion_nat2);
apply (rule prems);
apply (rule refl);
done;
finally show ?thesis; by (rule sym);
qed;
qed;

lemma mu_inversion_nat3: "0 < (n::nat) ==> g n =
(∑d:{)0..n}. (∑d':{)0..(n div d)}.
of_int(mu(int d)) * g((n div d) div d')))"
(is "0 < n ==> g n = ?sum");
proof -;
assume "0 < n";
then have "?sum = (∑c∈{)0..n}. ∑d∈{d. d dvd c}.
of_int (mu (int d)) * g (n div d div (c div d)))";
by (subst general_inversion_nat2, assumption, simp);
also have "… = (∑c∈{)0..n}. ∑d∈{d. d dvd c}.
g(n div c) * of_int (mu (int d)))";
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst nat_div_div_eq_div);
apply force;
apply force;
done;
also have "… = (∑c∈{)0..n}. g(n div c) * (∑d∈{d. d dvd c}.
of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "… = (∑c∈{)0..n}. g(n div c) * (if c = 1 then 1
else 0))";
apply (rule setsum_cong2);
apply (subst moebius_prop_nat_general);
apply auto;
done;
also have "… = g n";
apply (subst mu_aux2);
apply (rule prems);
apply simp;
done;
finally show ?thesis; by (rule sym);
qed;

lemma mu_inversion_nat4: "0 < (n::nat) ==> f n =
(∑d:{)0..n}. (∑d':{)0..n div d}.
of_int(mu(int d')) * f((n div d) div d')))"
(is "0 < n ==> f n = ?sum");
proof -;
assume "0 < n";
then have "?sum = (∑c:{)0..n}. ∑d∈{d. d dvd c}.
of_int (mu (int (c div d))) * f (n div d div (c div d)))";
by (subst general_inversion_nat2, assumption, simp);
also have "… =  (∑c∈{)0..n}. ∑d∈{d. d dvd c}.
(of_int (mu (int d)) * f (n div (c div d) div d)))";
apply (rule setsum_cong2);
apply (subst general_inversion_nat1);
apply clarsimp;
apply (rule setsum_cong2);
apply (subst nat_div_div);
apply auto;
done;
also have "… = (∑c∈{)0..n}. ∑d∈{d. d dvd c}.
(f (n div c) * of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst div_mult2_eq [THEN sym]);
apply (subst mult_commute);back;back;
apply (subst nat_dvd_mult_div);
apply clarsimp;
apply (erule nat_pos_dvd_pos);
apply assumption;
apply simp;
done;
also have "… = (∑c∈{)0..n}. f(n div c) * (∑d∈{d. d dvd c}.
of_int (mu (int d))))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "… = (∑c∈{)0..n}. f(n div c) * (if c = 1 then 1
else 0))";
apply (rule setsum_cong2);
apply (subst moebius_prop_nat_general);
apply auto;
done;
also have "… = f n";
apply (subst mu_aux2);
apply (rule prems);
apply simp;
done;
finally show ?thesis; by (rule sym);
qed;

end;

The central lemma

lemma calc1:

MITEMP2 n
==> (∑x∈{(d, d'). d ∈ {)0..n} ∧ d' ∈ {)0..n} ∧ d * d'n}. f (snd x, fst x)) =
(∑d∈{)0..n}. ∑x∈{(c, d').
c = dd' ∈ {)0..n} ∧ d * d'n}. f (snd x, fst x))

lemma calc2:

MITEMP2 n
==> (∑d∈{)0..n}. ∑x∈{(c, d').
c = dd' ∈ {)0..n} ∧ d * d'n}. f (snd x, fst x)) =
(∑d∈{)0..n}. ∑x∈{(c, d'). c = dd' ∈ {)0..n} ∧ d * d'n}. f (snd x, d))

lemma calc3:

MITEMP2 n
==> (∑d∈{)0..n}. ∑x∈{(c, d').
c = dd' ∈ {)0..n} ∧ d * d'n}. f (snd x, d)) =
(∑d∈{)0..n}. ∑x∈{d'. d' ∈ {)0..n} ∧ d * d'n}. f (x, d))

lemma calc4:

MITEMP2 n
==> (∑x∈{(d, d'). d ∈ {)0..n} ∧ d' ∈ {)0..n} ∧ d * d'n}. f (snd x, fst x)) =
(∑c∈{)0..n}. ∑x∈{(d, d').
(d, d')
∈ {(d, d'). d ∈ {)0..n} ∧ d' ∈ {)0..n} ∧ d * d'n} ∧
d * d' = c}. f (snd x, fst x))

lemma aux1:

[| 0 < x; xn; 0 < y; yn; y dvd x |] ==> x < n * y + y

lemma calc5:

MITEMP2 n
==> (∑c∈{)0..n}. ∑x∈{(d, d').
(d, d')
∈ {(d, d'). d ∈ {)0..n} ∧ d' ∈ {)0..n} ∧ d * d'n} ∧
d * d' = c}. f (snd x, fst x)) =
(∑c∈{)0..n}. ∑d∈{d'. d' ∈ {)0..n} ∧
d' dvd c}. f (snd (d, c div d), fst (d, c div d)))

lemma calc6:

MITEMP2 n
==> (∑c∈{)0..n}. ∑d∈{d'. d' ∈ {)0..n} ∧
d' dvd c}. f (snd (d, c div d), fst (d, c div d))) =
(∑c∈{)0..n}. ∑d∈{d'. d' ∈ {)0..n} ∧ d' dvd c}. f (c div d, d))

lemma calc7:

MITEMP2 n
==> (∑d∈{)0..n}. ∑d' | d' ∈ {)0..n} ∧ d * d'n. f (d', d)) =
(∑d∈{)0..n}. ∑d'∈{)0..n div d}. f (d', d))

lemma inv_short:

MITEMP2 n
==> (∑d∈{)0..n}. ∑d'∈{)0..n div d}. f (d', d)) =
(∑c∈{)0..n}. ∑d∈{d'. d' ∈ {)0..n} ∧ d' dvd c}. f (c div d, d))

theorem general_inversion_aux:

0 < n
==> (∑d∈{)0..n}. ∑d'∈{)0..n div d}. f (d', d)) =
(∑c∈{)0..n}. ∑d∈{d'. d' ∈ {)0..n} ∧ d' dvd c}. f (c div d, d))

General inversion laws

lemma general_inversion_int1:

0 < n ==> (∑x | 0 < xx dvd n. f x) = (∑x | 0 < xx dvd n. f (n div x))

lemma general_inversion_int2:

0 < n
==> (∑d∈{)0..n}. setsum (f d) {)0..n div d}) =
(∑c∈{)0..n}. ∑d | 0 < dd dvd c. f d (c div d))

lemma general_inversion_int2_cor1:

0 < n
==> (∑d∈{)0..n}. setsum (f d) {)0..n div d}) =
(∑d'∈{)0..n}. ∑d∈{)0..n div d'}. f d d')

lemma general_inversion_int2_cor2:

0 < n
==> (∑d∈{)0..n}. setsum f {)0..n div d}) =
(∑c∈{)0..n}. ∑d | 0 < dd dvd c. f (c div d))

lemma general_inversion_int2_cor3:

0 < n
==> (∑d∈{)0..n}. setsum f {)0..n div d}) = (∑d∈{)0..n}. of_int (n div d) * f d)

lemma general_inversion_int3:

0 < n
==> (∑d | 0 < dd dvd n. ∑d' | 0 < d'd' dvd n div d. f d' d) =
(∑c | 0 < cc dvd n. ∑d | 0 < dd dvd c. f (c div d) d)

lemma general_inversion_nat1:

0 < n ==> (∑x | x dvd n. f x) = (∑x | x dvd n. f (n div x))

lemma general_inversion_nat2:

0 < n
==> (∑d∈{)0..n}. setsum (f d) {)0..n div d}) =
(∑c∈{)0..n}. ∑d | d dvd c. f d (c div d))

lemma general_inversion_nat2_cor1:

0 < n
==> (∑d∈{)0..n}. setsum (f d) {)0..n div d}) =
(∑d'∈{)0..n}. ∑d∈{)0..n div d'}. f d d')

lemma general_inversion_nat2_cor2:

0 < n
==> (∑d∈{)0..n}. setsum f {)0..n div d}) =
(∑c∈{)0..n}. ∑d | d dvd c. f (c div d))

lemma general_inversion_nat2_cor3:

0 < n
==> (∑d∈{)0..n}. setsum f {)0..n div d}) = (∑d∈{)0..n}. of_nat (n div d) * f d)

lemma general_inversion_nat3:

0 < n
==> (∑d | d dvd n. ∑d' | d' dvd n div d. f d' d) =
(∑c | c dvd n. ∑d | d dvd c. f (c div d) d)

Moebius inversion

lemma moebius_prop2:

0 < n ==> setsum mu {d. 0 < dd dvd n} = (if n = 1 then 1 else 0)

lemma moebius_prop_nat:

0 < n ==> (∑x∈{d. d dvd n}. mu (int x)) = (if n = 1 then 1 else 0)

lemma moebius_prop_nat_general:

0 < n
==> (∑x∈{d. d dvd n}. of_int (mu (int x))) = (if n = 1 then 1::'a else 0::'a)

lemma moebius_prop_int_general:

0 < n
==> (∑x∈{d. 0 < dd dvd n}. of_int (mu x)) = (if n = 1 then 1::'a else 0::'a)

lemma mu_aux:

0 < x ==> (∑x∈{d. d dvd x}. f x * (if x = 1 then 1::'a else 0::'a)) = f 1

lemma mu_aux2:

0 < x ==> (∑x∈{)0..x}. f x * (if x = 1 then 1::'a else 0::'a)) = f 1

lemma mu_inversion_nat1:

0 < n
==> g n =
(∑d | d dvd n.
∑d' | d' dvd n div d. of_int (mu (int d)) * g (n div d div d'))

lemma mu_inversion_nat1a:

[| ∀n. 0 < n --> f n = (∑d | d dvd n. g (n div d)); 0 < n |]
==> g n = (∑d | d dvd n. of_int (mu (int d)) * f (n div d))

lemma mu_inversion_nat2:

0 < n
==> f n =
(∑d | d dvd n.
∑d' | d' dvd n div d. of_int (mu (int d')) * f (n div d div d'))

lemma mu_inversion_nat2a:

[| ∀n. 0 < n --> g n = (∑d | d dvd n. of_int (mu (int d)) * f (n div d));
0 < n |]
==> f n = (∑d | d dvd n. g (n div d))

lemma mu_inversion_nat3:

0 < n
==> g n =
(∑d∈{)0..n}. ∑d'∈{)0..n div d}. of_int (mu (int d)) * g (n div d div d'))

lemma mu_inversion_nat4:

0 < n
==> f n =
(∑d∈{)0..n}. ∑d'∈{)0..n div d}. of_int (mu (int d')) * f (n div d div d'))