Theory Inversion

(*  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) = {}";
    by (auto simp add: R_def);
  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))";
    by (auto simp add: setsum_UN_disjoint);
  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)";
     by (auto simp add: comp_def);
  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) = {}";
    by (auto simp add: T_def);
  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))";
    by (auto simp add: setsum_UN_disjoint);
  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;
  thus ?thesis by (insert prems, auto simp add: zadd_zless_mono);
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)";
    by (auto simp add: comp_def);
  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)";
    by (auto simp add: mult_left_mono);
  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 (auto simp add: dvd_def);
  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);
    apply (simp add: prems);
    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 (force simp add: inj_on_def);
    apply (subst image_int_dvd_set);
    apply (rule prems);
    apply (rule refl)+;
    done;
  also have "((f o nat) o int) = f";
    by (simp add: o_def);
  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 (force simp add: inj_on_def);
    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";
    by (simp add: o_def);
  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);
    apply (simp add: prems);
    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 (simp add: inj_on_def);
    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 (force simp add: inj_on_def);
    apply (subst image_int_GreaterThanAtMost);
    apply (subst int_div);
    apply simp;
    apply (simp add: o_def);
    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 (simp add: inj_on_def);
    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 (force simp add: inj_on_def);
    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); 
    apply (simp add: prems);
    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 (simp add: inj_on_def);
    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 (simp add: inj_on_def);
    apply (subst image_int_dvd_set);
    apply (rule nat_pos_div_dvd_gr_0, rule prems, assumption);
    apply (subst int_div);
    apply (rule refl);
    apply (simp add: o_def);
    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 (simp add: inj_on_def);
    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 (simp add: inj_on_def);
    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);
    apply (simp add: prems);
    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 (simp add: inj_on_def);
    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);
    apply (simp add: mult_ac);
    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;
    apply (simp add: mult_ac);
    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;
    apply (simp add: mult_ac);
    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;
    apply (simp add: mult_ac);
    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;