Theory EulerPhi

(*  Title:      EulerPhi.thy
    Author:     David Gray
*)

header {* Euler's phi function *}

theory EulerPhi = NatIntLib:;

constdefs
  phi :: "int => int"
  "phi n == int (card({(x::int). (1 <= x) & (x <= n) & (zgcd(x, n) = 1)}))";

locale PHI =
  fixes n  :: "int"
  fixes S  :: "int set"
  fixes I  :: "int set"
  fixes I2 :: "int set"
  fixes A  :: "int => int set"
  fixes B  :: "int => int set"
  fixes f  :: "int => int"

  assumes n_ge_1:  "1 <= n"

  defines S_def:  "S   == {x. 1 <= x & x <= n}"
  defines I_def:  "I   == {d. 0 <= d & d dvd n}"
  defines I2_def: "I2  == {d. 1 <= d & d dvd n}"
  defines A_def:  "A d == {k. (k:S) & zgcd(k, n) = d}"
  defines B_def:  "B d == {l. (1::int) <= l & l <= (n div d) & zgcd(l, (n div d)) = 1}"
  defines f_def:  "f d == n div d";

lemma (in PHI) n_dvd_range: "[| d dvd n; 0 <= d|] ==> 1 <= d & d <= n";
proof -;
  assume "d dvd n" and "0 <= d";
  then have "1 <= d";
    apply (insert prems n_ge_1, auto);
    apply (subgoal_tac "0 ~= d", auto);
  done;
  moreover have "d <= n";
    apply (insert prems n_ge_1, auto);
    apply (frule zdvd_bounds, auto);
  done;
  ultimately show ?thesis by auto;
qed;

lemma (in PHI) n_zgcd_range: "[| 1 <= x; x <= n |] ==> 1 <= zgcd (x, n) & zgcd (x, n) <= n";
  apply (insert zgcd_zdvd2 [of x n]);
  apply (rule n_dvd_range, auto simp add: zgcd_def);
done;

lemma (in PHI) zgcd_elem_S: "[| 1 <= x; x <= n |] ==> zgcd (x, n):S";
  by (auto simp add: S_def n_zgcd_range);

lemma (in PHI) S_finite: "finite S";
  apply (subgoal_tac "S <= {1..n}");
  apply (erule finite_subset);
  apply simp;
  apply (unfold S_def);
  apply auto;
  done;

lemma (in PHI) I_sub_S: "I <= S";
  by (auto simp add: S_def I_def n_dvd_range );

lemma (in PHI) I_finite: "finite I";
  by (insert I_sub_S S_finite, auto simp add: finite_subset);

lemma (in PHI) I_elem_prop: "d:I ==> 1 <= d";
  apply (subgoal_tac "d ~= 0");
  apply (insert n_ge_1, auto simp add: I_def);
done;

lemma (in PHI) I_eq_I2: "I = I2";
  by (auto simp add: n_ge_1 I_def I2_def n_dvd_range);

lemma (in PHI) A_sub_S: "A(d) <= S";
  by (auto simp add: S_def A_def);

lemma (in PHI) A_finite: "finite(A(d))";
  by (insert A_sub_S [of d] S_finite, auto simp add: finite_subset);

lemma (in PHI) B_sub_S: "d:I ==> B(d) <= S";
proof;
  fix x;
  assume "d:I" and "x:B(d)";
  then have "x <= n";
  proof-;
    from prems have "x <= n div d" by auto;
    also have "n div d <= n div 1";
    proof-;
      from PHI_def prems have "1 <= n"; by auto;
      then have "0 <= n" by auto;
      moreover have "(0::int) < 1" by auto;
      moreover from prems have "1 <= d" by (insert prems, auto simp add: I_elem_prop);
      ultimately show "n div d <= n div 1" by (rule zdiv_mono2);
    qed;
    also have "n div 1 = n" by auto;
    finally show "x <= n".;
  qed;
  moreover from prems have "1 <= x" by auto;
  ultimately show "x:S" by (auto simp add: S_def);
qed;

lemma (in PHI) B_finite: "d:I ==> finite(B(d))";
  apply (drule B_sub_S, insert S_finite);
  apply (auto simp add: finite_subset);
done;

(* "Lemma 1" *)
lemma (in PHI) S_eq_UNION_A: "S = UNION I A";
proof -;
  have "UNION I A <= S" by (auto simp add: S_def A_def);
  moreover have "S <= UNION I A";
  proof -;
    have "S <= UNION I2 A" 
      by (insert n_zgcd_range, auto simp add: S_def A_def I2_def);
    also have "I2 = I" by (auto simp add: I_eq_I2);
    finally show "S <= UNION I A".;
  qed;
  ultimately show ?thesis by auto;
qed;

(* "Lemma 2" *)
lemma (in PHI) A_disj_prop: "ALL d1:I. ALL d2:I. d1 ~= d2 --> A(d1) Int A(d2) = {}";
  by (auto simp add: A_def);

(* "Lemma 3" *)
lemma (in PHI) n_eq_Sum_card_A: "n = setsum (%x. int(card (A(x)))) I";
proof -;
  have "n = int(card S)";
    apply (insert n_ge_1, auto simp add: S_def);
    apply (subgoal_tac "{x. 1 <= x & x <= n} = {x. 0 < x & x <= n}");
    apply (rule ssubst, force);
    apply (subgoal_tac "{x. 0 < x & x <= n} = {)0..n}");
    apply (erule ssubst);back;
    apply simp;
    apply force;
    apply auto;
    done;
  also have "S = UNION I A" by (rule S_eq_UNION_A);
  also have "int (card (UNION I A)) = setsum (%x. int (card (A(x)))) I";
    apply (subst card_UN_disjoint);
    apply (auto simp add: I_finite A_finite A_disj_prop);
    apply (subst int_setsum);
    apply (simp add: o_def);
    done;
  finally show ?thesis .;
qed;

(* "Lemma 4" *)
lemma (in PHI) zgcd_div_prop: "d:S ==> (zgcd(k, n) = d) = 
  (d dvd k & d dvd n & zgcd(k div d, n div d) = 1)";
proof -;
  assume "d: S";
  with S_def have "0 < d"; by auto;
  thus ?thesis; 
    by (rule zgcd_equiv);
qed;

(* "Lemma 5" *)
lemma (in PHI) A_inj_prop: "d:I ==> inj_on (%(k::int). k div d) (A(d))";
proof (auto simp add: inj_on_def);
  fix x and y;
  assume "d:I" and "x div d = y div d" and
         p1: "x:A(d)" and p2: "y:A(d)";
  then have "(x div d) * d = (y div d) * d" by auto;
  also have "(x div d) * d = x";
  proof -;
    have "d dvd x" by (insert p1, auto simp add: A_def);
    then show "(x div d) * d = x" by (auto simp add: dvd_def);
  qed;
  also have "(y div d) * d = y";
  proof -;
    have "d dvd y" by (insert p2, auto simp add: A_def);
    then show "(y div d) * d = y" by (auto simp add: dvd_def);
  qed;
  finally; show "x = y" .;
qed;

(* "Lemma 6" *)
lemma (in PHI) image_A_eq_B: "d:I ==> (%(k::int). k div d) ` A(d) = B(d)";  
proof (auto);
  fix k;
  assume "d:I" and "k:A(d)";
  then show "(k div d):B(d)";
  proof -;
    from prems have "1 <= k div d";
    proof (auto simp add: A_def I_def S_def);
      assume "1 <= k";
      then have "0 < k & 0 < zgcd(k,n) & zgcd(k,n) dvd k" by (auto simp add: zgcd_gr_zero1);
      then have "0 < k div zgcd(k,n)" by (auto simp add: zdiv_gr_zero);
      thus "1 <= k div zgcd(k,n)" by arith;
    qed;
    moreover from prems have "k div d <= n div d";
    proof (auto simp add: A_def I_def S_def);
      assume "1 <= k";
      then have "0 < zgcd(k,n)" by (auto simp add: zgcd_gr_zero1);
      thus "k div zgcd (k, n) <= n div zgcd (k, n)";
        by (insert prems, auto simp add: zdiv_mono1);
    qed;
    moreover from prems have "zgcd(k div d, n div d) = 1";
    proof (auto simp add: A_def I_def S_def);
      assume "1 <= k" and "k <= n";
      then have p1:"zgcd (k, n):S" by (auto simp add: zgcd_elem_S);
      thus "zgcd (k div zgcd (k, n), n div zgcd (k, n)) = 1";
        apply (insert p1); 
        apply (frule zgcd_div_prop, auto);
      done;
    qed;
    ultimately show "(k div d):B(d)" by (auto simp add: B_def);
  qed;
next;
  fix y;
  assume q: "d:I" and "y:B(d)";
  then show "y:(%k. k div d) ` A d";
  proof (auto simp add: image_def);
    have a1:"(y * d):A(d)";
    proof-;
      have "1 <= y * d";
      proof-;
        from prems have "0 < (y * d)" 
          by (insert I_elem_prop [of d], auto simp add: mult_pos);
        thus "1 <= (y * d)" by arith;
      qed;
      moreover have "y * d <= n";
      proof-;
        from prems have "y <= n div d" by auto;
        with prems have "y * d <= (n div d) * d" 
          by (auto simp add: mult_right_mono);
        also have "... = n";
          proof -;
            from prems have "d dvd n" by auto;
            thus "(n div d) * d = n" by (auto simp add: dvd_def);
          qed;
        finally show "y * d <= n".;
      qed;
      moreover have "zgcd(y * d, n) = d";
      proof-;
        from prems have p1: "d dvd (y * d) & d dvd n & zgcd( (y * d) div d, n div d) = 1";
          by (auto simp add: B_def);
        moreover from prems have p2: "d:S" by (insert prems I_sub_S, auto);
        ultimately show "zgcd(y * d, n) = d"
          by (insert p1 p2 zgcd_div_prop [of d "y * d"], auto);
      qed;
      ultimately show "(y * d):A(d)" by (auto simp add: A_def S_def);
    qed;
    moreover have a2: "y = (y * d) div d" by (insert prems, auto simp add: dvd_def);
    ultimately show "EX x:A d. y = x div d"
      apply (insert a1 a2)
      apply (rule bexI, auto);
    done;
  qed;
qed;

(* Cor 1 *)
lemma (in PHI) card_A_eq_phi: "d:I ==> int(card (A(d))) = phi(n div d)";
proof-;
  assume "d:I";
  have "card(A(d)) = card((%(k::int). k div d) ` A(d))";
  proof-;
    have "finite( A(d))" by (auto simp add: A_finite);
    moreover have "inj_on (%(k::int). k div d) (A(d))";
      by (rule A_inj_prop, insert prems, auto);
    ultimately show "card(A(d)) = card((%(k::int). k div d) ` A(d))";
      by (auto simp add: card_image);
  qed;
  also have "(%(k::int). k div d) ` A(d) = B(d)";
    by (rule image_A_eq_B, insert prems, auto);
  finally have "int(card (A(d)) ) = int (card (B(d)))" by (auto);
  also have "... = phi (n div d)";
    by (auto simp add: B_def phi_def);
  finally show ?thesis .;
qed;

(* Cor 2 *)
lemma (in PHI) n_eq_setsum_phi: "n = setsum (phi ˆ f) I";
proof-;
  have "n = setsum (%x. int(card (A(x)))) I";
    by (auto simp add: n_eq_Sum_card_A);
  also have "... = setsum (%d. phi (n div d)) I";
  proof-;
    have "finite I" by (auto simp add: I_finite);
    moreover have "ALL x:I. (%x. int(card (A(x)))) x =  (%d. phi (n div d)) x";
      by (auto simp add: card_A_eq_phi);
    ultimately show "setsum (%x. int(card (A(x)))) I = setsum (%d. phi (n div d)) I"
      apply (intro setsum_cong);
      apply auto;
      done;
  qed;
  also have "... = setsum (phi ˆ f) I";
  proof-;
    have "finite I" by (auto simp add: I_finite);
    moreover have "ALL x:I. (%d. phi (n div d)) x = (phi ˆ f) x";
      by (auto simp add: f_def);
    ultimately show "setsum (%d. phi (n div d)) I = setsum (phi ˆ f) I";
      by (intro setsum_cong, auto);
  qed;
  finally show ?thesis .;
qed;

lemma (in PHI) I_inj_prop: "inj_on f I";
proof (auto simp add: inj_on_def f_def I_def);
  fix x and y;
  assume x1:"x dvd n" and x2: "0 <= x" and 
         y1:"y dvd n" and y2: "0 <= y" and "n div x = n div y";
  then have p1: "y * (n div x) * x = y * (n div y) * x";
    by (auto);
  also have "y * (n div x) * x = y * n";
    by (insert x1 x2 p1, auto simp add: dvd_def);
  also have "y * (n div y) * x = n * x";
    by (insert y1 y2 p1, auto simp add: dvd_def);
  finally have "n * x = n * y" by auto;
  thus "x = y" by (insert n_ge_1, auto);
qed;

lemma (in PHI) f_image_I_eq_I: "f ` I = I";
proof (auto);
  fix x;
  assume "x:I";
  thus "(f x):I";
  proof-;
    have "0 <= n div x";
    proof-;
      have "0 <= n & 0 < x" by (insert prems, frule I_elem_prop, 
        auto simp add: PHI_def);
      then have "0 div x <= n div x"
        apply (clarify); 
        apply (rule zdiv_mono1, auto);
      done;
      also have "0 div x = 0" by auto;
      finally show "0 <= n div x".;
    qed;
    moreover have "(n div x) dvd n" by (insert prems, auto simp add: I_def dvd_def);
    ultimately show "(f x):I" by (auto simp add: f_def I_def);
  qed;
next;
  fix x;
  assume "x:I";
  thus "x : f ` I";
  proof (auto simp add: image_def f_def);
    have a1: "(n div x):I";
    proof-;
      have "0 <= n div x";
      proof-;
        have "0 <= n & 0 < x" by (insert prems, frule I_elem_prop, 
          auto simp add: PHI_def);
        then have "0 div x <= n div x"
          apply (clarify);
          apply (rule zdiv_mono1, auto);
        done;
        also have "0 div x = 0" by auto;
        finally show "0 <= n div x".;
      qed;
      moreover have "(n div x) dvd n" by (insert prems, auto simp add: I_def dvd_def);
      ultimately show "(n div x):I" by (auto simp add: I_def);
    qed;
    moreover have a2: "x = n div (n div x)";
    proof -;
      from prems and PHI_def have "0 < n" by auto;
      moreover have "0 < x" 
        apply (insert prems);
        apply (frule I_elem_prop, auto);
      done;
      moreover from prems have "x dvd n" by auto;
      ultimately have "n div (n div x) = x" by (auto simp add: zdiv_zdiv_prop);
      thus "x = n div (n div x)" by auto;
    qed;
    ultimately show "EX y:I. x = n div y";
      apply (insert a1 a2);
      apply (rule bexI, auto);
    done;
  qed;
qed;

(* Finally! *)
theorem (in PHI) big_prop1: "n = setsum (%d. phi(d)) I";
proof-;
  have "n = setsum (phi ˆ f) I" by (auto simp add: n_eq_setsum_phi);
  also have "... = setsum (%d. phi(d)) (f ` I)";
  proof -;
    have "finite I" by (auto simp add: I_finite);
    moreover have "inj_on f I" by (auto simp add: I_inj_prop);
    ultimately have "setsum (%d. phi(d)) (f ` I) = setsum (phi ˆ f) I";
      by (rule setsum_reindex);
    thus "setsum (phi ˆ f) I = setsum (%d. phi(d)) (f ` I)" by auto;
  qed;
  also have "... = setsum (%d. phi(d)) I";
    by (auto simp add: f_image_I_eq_I);
  finally show ?thesis .;
qed;

lemma card_gcd_set: "[| p:zprime; 0 < k |] ==> 
                     int(card({x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1})) = p^(k - 1)";
proof-;
  assume "p:zprime" and "0 < k";
  then have "{x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1} =
             {x. 1 <= x & x <= p^k & p dvd x}";
    by (auto simp add: gcd_prime_power_iff_zdvd_prop);
  also have "... = {x. EX y.(1 <= y & y <= p^(k - 1) & x = p * y)}";
  proof;
    show "{x. 1 <= x & x <= p ^ k & p dvd x} <= 
         {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}";
      proof (auto, rule_tac x = "x div p" in exI, auto);
        fix x;
        assume "1 <= x" and "x <= p ^ k" and "p dvd x";
        thus "1 <= x div p";
        proof -;
          have "0 < x & 0 < p & 0 < x div p";
            by (insert prems, auto simp add: zprime_def zdiv_gr_zero);
          thus "1 <= x div p" by auto;
        qed;
      next;
        fix x;
        assume "1 <= x" and "x <= p ^ k" and "p dvd x";
        thus "x div p <= p ^ (k - Suc 0)";
        proof -;
          have "x div p <= (p ^ k) div p";
            by (insert prems, auto simp add: zprime_def zdiv_mono1);
          also have "(p ^ k) div p = p ^ (k - 1)";
            by (insert prems, auto simp add: zpower_minus_one zprime_def);
          finally show "x div p <= p ^ (k - Suc 0)" by auto;
        qed;
      next;
        fix x;
        assume "1 <= x" and "x <= p ^ k" and "p dvd x";
        thus "x = p * (x div p)" by (auto simp add: dvd_def);
      qed;
    next;
    show "{x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y} <= {x. 1 <= x & x <= p ^ k & p dvd x}";
    proof (auto);
      fix y;
      assume "1 <= y" and "y <= p ^ (k - Suc 0)";
      thus "1 <= p * y";
      proof -;
         have "0 < y & 0 < p" by (insert prems, auto simp add: zprime_def);
         then have "0 < p * y" by (auto simp add: mult_pos);
         thus "1 <= p * y" by auto;
      qed;
    next;
      fix y;
      assume "1 <= y" and "y <= p ^ (k - Suc 0)";
      thus "p * y <= p ^ k";
      proof -;
        have "y * p <= (p ^ (k - 1)) * p";
          by (insert prems, auto simp add: zprime_def mult_right_mono);
        also have "(p ^ (k - 1)) * p = p ^ k";
          by (insert prems, auto simp add: zpower_zmult zprime_def);
        finally show "p * y <= p ^ k" by (auto simp add: zmult_ac);
      qed;
    qed;
  qed;
  finally; have "card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} =
                 card {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}"; by auto;
  also have "... = card {y. 1 <= y & y <= p^(k - 1)}";
  proof-;
    have "finite({y. 1 <= y & y <= p ^ (k - 1)})";
    proof-;
      have "finite({y. 0 < y & y <= p ^ (k - 1)})";
        apply (subgoal_tac "{y. 0 < y ∧ y ≤ p ^ (k - 1)} = 
             {)0..p ^ (k - 1)}");
        apply (erule ssubst);
        apply auto;
        done;
      also have "{y. 0 < y & y <= p ^ (k - 1)} =
                 {y. 1 <= y & y <= p ^ (k - 1)}" by auto;
      finally show "finite({y. 1 <= y & y <= p ^ (k - 1)})".;
    qed;
    moreover have "inj_on (%y.(p::int)*y) {y. 1 <= y & y <= p ^ (k - 1)}";
      by (insert prems, auto simp add: inj_on_def zprime_def);
    ultimately have "card ((%y.(p::int)*y) ` {y. 1 <= y & y <= p ^ (k - 1)}) =
                     card {y. 1 <= y & y <= p ^ (k - 1)}";
      by (rule_tac A = "{y. 1 <= y & y <= p ^ (k - 1)}" in card_image);
    also have "(%y.(p::int)*y) ` {y. 1 <= y & y <= p ^ (k - 1)} = 
                {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y}" by (auto);
    finally show "card {x. EX y. 1 <= y & y <= p ^ (k - 1) & x = p * y} =
                  card {y. 1 <= y & y <= p ^ (k - 1)}".;
  qed;
  also have "{y. 1 <= y & y <= p ^ (k - 1)} = {y. 0 < y & y <= p ^ (k - 1)}" by auto;
  finally have "int (card({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1})) = 
                int (card({y. 0 < y & y <= p ^ (k - 1)}))";
    by auto;
  also have "... = p ^ (k - 1)";
    apply (subgoal_tac "{y. 0 < y ∧ y ≤ p ^ (k - 1)} = {)0.. p^(k - 1)}");
    apply (erule ssubst);
    apply (subgoal_tac "0 <= p ^ (k - 1)");
    apply simp;
    apply (rule zero_le_power);
    apply (rule order_less_imp_le);
    apply (insert prems, auto simp add: zprime_def);
    done;
  finally show "int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) = p ^ (k - 1)".;
qed;

theorem big_prop2: " [| p : zprime; 0 < k |] ==> phi(p^k) = (p^k) - (p^(k - 1))";
proof -;
  assume "p : zprime" and "0 < k";
  then have p:"0 <= p ^ k"
  proof-;
    have "0 < p" by (insert prems, auto simp add: zprime_def);
    then have "0 < p ^ k" by (rule zpower_gr_0);
    thus "0 <= p ^ k" by auto;
  qed;
  then have "p^k = int (card {x. 0 < x & x <= p^k})";
      apply (subgoal_tac "{x. 0 < x & x <= p^k} = {)0..p^k}");
      apply auto;
      done;
  also have "{x. 0 < x & x <= p^k} = {x. 1 <= x & x <= p^k}" by auto;
  also have "... = {x. 1 <= x & x <= p^k & zgcd(x,p^k) = 1} Un
                   {x. 1 <= x & x <= p^k & zgcd(x,p^k) ~= 1}" by auto;
  finally have "p ^ k = int (card ({x. 1 <= x & x <= p^k & zgcd(x,p^k) = 1} Un
                                   {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}))".;
  also have "card ({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} Un 
                   {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
             card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} + 
             card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
  proof-;
    have "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}";
    proof-;
       have "finite {x. 1 <= x & x <= p ^ k}";
       proof-;
         from p have "finite {x. 0 < x & x <= p ^ k}";
           apply (subgoal_tac "{x. 0 < x & x <= p ^ k} = {)0..p^k}");
           apply auto; 
           done;
         also have "{x. 0 < x & x <= p ^ k} = {x. 1 <= x & x <= p ^ k}" 
           by (auto);
         finally show "finite {x. 1 <= x & x <= p ^ k}".;
       qed;
       moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} <=
                      {x. 1 <= x & x <= p ^ k}"; 
         by auto;
       ultimately show "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}";
         by (auto simp add: finite_subset);
    qed;
    moreover have "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
    proof-;
       have "finite {x. 1 <= x & x <= p ^ k}";
       proof-;
         from p have "finite {x. 0 < x & x <= p ^ k}";
           apply (subgoal_tac "{x. 0 < x & x <= p ^ k} = {)0..p^k}");
           apply auto;
           done;
         also have "{x. 0 < x & x <= p ^ k} = {x. 1 <= x & x <= p ^ k}" 
           by (auto);
         finally show "finite {x. 1 <= x & x <= p ^ k}".;
       qed;
       moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} <=
                      {x. 1 <= x & x <= p ^ k}"; 
         by auto;
       ultimately show "finite {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
         by (auto simp add: finite_subset);
    qed;
    moreover have "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1} Int
                   {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} = {}";
      by auto;
    ultimately show "card ({x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} Un 
                           {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
                     card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} + 
                     card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}";
      by (rule_tac A = "{x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}" 
        in card_Un_disjoint, auto);
  qed;
  also; have "int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1} + 
                   card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) =
              int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1}) + 
              int (card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1})";
    by (auto);
  also have "int( card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) ~= 1}) = 
      p ^ (k - 1)";
    by (insert prems, auto simp add: card_gcd_set);
  also have "int( card {x. 1 <= x & x <= p ^ k & zgcd (x, p ^ k) = 1})
      = phi(p^k)";
    by (auto simp add: phi_def);
  finally have "p ^ k = phi (p ^ k) + p ^ (k - 1)".;
  thus "phi (p ^ k) = p ^ k - p ^ (k - 1)";
    by (auto);
qed;


locale PHI2 =
  fixes n        :: "int"
  fixes m        :: "int"
  fixes f        :: "int => (int * int)"
  fixes SR       :: "int => int set"
  fixes ResUnits :: "int => int set"

  assumes n_ge_1:  "1 <= n"
  assumes m_ge_1:  "1 <= m"
  assumes m_n_gcd: "zgcd(m, n) = 1"

  defines f_def:        "f x == (x mod m, x mod n)"
  defines SR_def:       "SR y == {x. (0 <= x) & (x < y)}"
  defines ResUnits_def: "ResUnits y == {x. (x:(SR(y))) & zgcd(x,y) = 1}";

lemma (in PHI2) SR_m_mod_prop: "a:SR(m) ==> a mod m = a";
  apply (insert m_ge_1);
  apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_n_mod_prop: "a:SR(n) ==> a mod n = a";
  apply (insert n_ge_1);
  apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_mn_mod_prop: "a:SR(m*n) ==> a mod (m*n) = a";
  apply (insert n_ge_1 m_ge_1);
  apply (auto simp add: SR_def mod_pos_pos_trivial);
done;

lemma (in PHI2) SR_m_finite: "finite(SR(m))";
  apply (insert m_ge_1);
  apply (auto simp add: SR_def); 
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < m} = {0..m(}");
  apply auto;
done;

lemma (in PHI2) SR_m_card: "int(card(SR(m))) = m";
  apply (insert m_ge_1);
  apply (auto simp add: SR_def);
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < m} = {0..m(}");
  apply auto;
done;

lemma (in PHI2) SR_n_finite: "finite(SR(n))";
  apply (insert n_ge_1);
  apply (unfold SR_def);
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < n} = {0..n(}");
  apply auto;
done;

lemma (in PHI2) SR_n_card: "int(card(SR(n))) = n";
  apply (insert n_ge_1);
  apply (auto simp add: SR_def);
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < n} = {0..n(}");
  apply auto;
done;

lemma (in PHI2) SR_mn_finite: "finite(SR(m*n))";
  apply (insert m_ge_1 n_ge_1);
  apply (auto simp add: SR_def); 
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < m * n} = {0..m*n(}");
  apply auto;
done;

lemma (in PHI2) SR_mn_card: "int(card(SR(m*n))) = m * n";
  apply (insert m_ge_1 n_ge_1);
  apply (auto simp add: SR_def);
  apply (subgoal_tac "{x. 0 ≤ x ∧ x < m * n} = {0..m*n(}");
  apply (erule ssubst);
  apply auto;
  apply (subgoal_tac "0 < m*n");
  apply auto;
  apply (rule mult_pos);
  apply auto;
done;

lemma (in PHI2) ResUnits_m_finite: "finite(ResUnits(m))";
proof-;
  have "ResUnits(m) <= SR(m)" by (auto simp add: ResUnits_def);
  with SR_m_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) ResUnits_n_finite: "finite(ResUnits(n))";
proof-;
  have "ResUnits(n) <= SR(n)" by (auto simp add: ResUnits_def);
  with SR_n_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) ResUnits_mn_finite: "finite(ResUnits(m * n))";
proof-;
  have "ResUnits(m * n) <= SR(m * n)" by (auto simp add: ResUnits_def);
  with SR_mn_finite show ?thesis by (auto simp add: finite_subset);
qed;

lemma (in PHI2) zgcd_zmult_prop: "(zgcd(m * n, x) = 1) = ((zgcd(m, x) = 1) & (zgcd(n, x) = 1))";
proof;
  assume p1: "zgcd (m * n, x) = 1";
  have "zgcd(n, x) dvd zgcd(m * n, x) & zgcd(m, x) dvd zgcd(m * n, x)";
    apply (insert zgcd_zdvd_zgcd_zmult [of m x n]);
    apply (auto simp add: zgcd_zdvd_zgcd_zmult zmult_ac);
  done;
  thus "zgcd(m, x) = 1 & zgcd(n , x) = 1";
    apply (insert p1, insert PHI2_def, auto);
    apply (drule_tac n = "zgcd(m,x)" in zdvd_bounds, auto);
    apply (subgoal_tac "0 < m");
    apply (drule_tac b = x in zgcd_gr_zero1, auto); defer;
    apply (drule zdvd_bounds, auto);
    apply (subgoal_tac "0 < n");
    apply (drule_tac b = x in zgcd_gr_zero1);
    apply (insert prems, auto);
  done;
next;
  assume "zgcd (m, x) = 1 & zgcd (n, x) = 1";
  thus "zgcd (m * n, x) = 1";
    by (auto simp add: zgcd_zgcd_zmult);
qed;

lemma (in PHI2) specialized_chinese: "ALL a. ALL b. EX x. ([x = a] (mod m) & [x = b] (mod n))";
proof (auto);
  fix a b;
  have "0 < n" by (insert prems, auto simp add: PHI2_def);
  with m_n_gcd obtain u where p1:"[m*u = 1] (mod n)" using zcong_lineq_ex by auto;
  have "zgcd(n, m) = 1" by (insert prems, auto simp add: zgcd_commute PHI2_def);
  moreover have "0 < m" by (insert prems, auto simp add: PHI2_def);
  ultimately obtain v where p2:"[n * v = 1] (mod m)" using zcong_lineq_ex by auto;
  from p1 have "[m*u*b = 1*b] (mod n)" by (rule zcong_scalar);
  then have "[m*u*b = b] (mod n)" by auto;
  then have "[m*u*b + n*(v*a) = b] (mod n)" by (rule zcong_m_scalar_prop);
  then have p3: "[m*u*b + n*v*a = b] (mod n)" by (auto simp add: zmult_ac);
  from p2 have "[n*v*a = 1*a] (mod m)" by (rule zcong_scalar);
  then have "[n*v*a = a] (mod m)" by auto;
  then have "[n*v*a + m*(u*b) = a] (mod m)" by (rule zcong_m_scalar_prop);
  then have "[n*v*a + m*u*b = a] (mod m)" by (auto simp add: zmult_ac);
  then have p4: "[m*u*b + n*v*a = a] (mod m)" by (auto simp add: zadd_ac);
  have "[m*u*b + n*v*a = a] (mod m) & [m*u*b + n*v*a = b] (mod n)";
    by (insert p3 p4, auto);
  thus "EX x. [x = a] (mod m) & [x = b] (mod n)" by (auto);
qed;

lemma (in PHI2) SR_inj_on_f: "inj_on f (SR(m * n))";
  apply (auto simp add: inj_on_def f_def);
proof-;
  fix x y;
  assume "x : SR (m * n)" and "y : SR (m * n)" and 
         "x mod m = y mod m" and "x mod n = y mod n";
  have p1: "0 < m & 0 < n"  by (insert m_ge_1 n_ge_1, auto);
  then have "[x = y] (mod m) & [x = y] (mod n)";
    by (insert prems, auto simp add: zcong_zmod_eq);
  then have p2: "[x = y] (mod m * n)";
    apply (auto);
    apply (insert prems);
    apply (rule zcong_zgcd_zmult_zmod, auto simp add: PHI2_def);
  done;
  from p1 have p3: "0 < m * n" by (auto simp add: mult_pos);
  have p4: "x mod (m*n) = y mod (m*n)";
    by (insert p2 p3 zcong_zmod_eq [of "m*n" x y], auto);
  have "0 <= x & 0 <= y & x < (m*n) & y < (m*n)" by (insert prems, auto simp add: SR_def);
  thus "x = y";
    apply (auto);
    apply (insert p1 p4, auto);
    apply (drule mod_pos_pos_trivial, auto)+;
  done;
qed;

lemma (in PHI2) f_SR_card: "card (f ` (SR(m*n))) = card(SR(m) <*> SR(n))";
proof-;
  have "card (f ` (SR(m*n))) = card( SR(m*n))";
    apply (insert SR_mn_finite SR_inj_on_f);
    apply (auto simp add: card_image);
  done;
  also have "... = card(SR(m) <*> SR(n))";
  proof-;
    have "int(card(SR(m * n))) = int(card(SR(m) <*> SR(n)))";
      apply (insert SR_m_finite SR_n_finite SR_mn_finite);
      apply (insert SR_m_card SR_n_card SR_mn_card);
      apply (auto simp add: zmult_int [THEN sym]);
      done;
    thus ?thesis by auto;
  qed;
  finally show ?thesis by auto;
qed;

lemma (in PHI2) SR_image_prop: "f ` SR(m * n) <= SR(m) <*> SR(n)";
  apply (insert m_ge_1 n_ge_1);
  apply (auto simp add: SR_def f_def pos_mod_sign pos_mod_bound);
done;

lemma (in PHI2) SR_prod_finite: "finite( SR(m) <*> SR(n))";
  by (auto simp add: SR_m_finite SR_n_finite); 

lemma (in PHI2) image_SR_prop: "f ` SR(m * n) = SR(m) <*> SR(n)";
  apply (insert SR_prod_finite SR_image_prop f_SR_card);  
  apply (auto simp add: card_seteq);
done;

lemma (in PHI2) ResUnits_inj_on_f: "inj_on f (ResUnits(m * n))";
proof-;
  have "(ResUnits(m * n)) <= SR(m * n)";
    by (auto simp add: ResUnits_def SR_def);
  with SR_inj_on_f show ?thesis by (auto simp add: subset_inj_on);
qed;

lemma (in PHI2) ResUnits_prod_finite: "finite( ResUnits(m) <*> ResUnits(n))";
  by (auto simp add: ResUnits_m_finite ResUnits_n_finite); 

lemma (in PHI2) aux1_ResUnits_image_prop: "f ` ResUnits(m * n) <= ResUnits(m) <*> ResUnits(n)";
  apply (auto simp add: image_def f_def);
proof -;
  fix x;
  assume "x : ResUnits (m * n)";
  then have "zgcd(m*n, x) = 1" by (auto simp add: ResUnits_def zgcd_commute);
  then have "zgcd(m,x) = 1" by (auto simp add: zgcd_zmult_prop);
  also have "zgcd(m,x) = zgcd(m,x mod m)" by (insert zgcd_eq2 [of m x], auto);
  finally have "zgcd (m, x mod m) = 1" .;
  thus "x mod m : ResUnits m";
    apply (auto simp add: ResUnits_def zgcd_commute SR_def);
    apply (insert m_ge_1, auto simp add: pos_mod_sign pos_mod_bound);
  done;
next;
  fix x;
  assume "x : ResUnits (m * n)";
  then have "zgcd(m*n, x) = 1" by (auto simp add: ResUnits_def zgcd_commute);
  then have "zgcd(n,x) = 1" by (auto simp add: zgcd_zmult_prop);
  also have "zgcd(n,x) = zgcd(n,x mod n)" by (insert zgcd_eq2 [of n x], auto);
  finally have "zgcd (n, x mod n) = 1" .;
  thus "x mod n : ResUnits n";
    apply (auto simp add: ResUnits_def zgcd_commute SR_def);
    apply (insert n_ge_1, auto simp add: pos_mod_sign pos_mod_bound);
  done;
qed;

lemma (in PHI2) aux2_ResUnits_image_prop: "ResUnits(m) <*> ResUnits(n) <= f ` ResUnits(m * n)";
  apply (auto simp add: image_def f_def);
  apply (auto simp add: ResUnits_def);
  apply (insert specialized_chinese);
  apply (drule_tac x = a in allE, auto);
  apply (drule_tac x = b in allE, auto);
  apply (rule_tac x = "x mod (m*n)" in exI);
  apply (auto);
proof-;
  fix a b x;
  have "0 < m * n" by (insert m_ge_1 n_ge_1, auto simp add: mult_pos);
  thus "x mod (m*n) : SR(m*n)" by (auto simp add: SR_def pos_mod_sign pos_mod_bound);
next;
  fix a b x;
  assume p1: "a : SR m" and p2: "b : SR n" and
         p3: "zgcd (a, m) = 1" and p4: "zgcd (b, n) = 1" and
         "[x = a] (mod m)" and "[x = b] (mod n)";
  moreover have "0 < m & 0 < n" by (insert n_ge_1 m_ge_1, auto);
  ultimately have "x mod m = a mod m & x mod n = b mod n";
    by (auto simp add: zcong_zmod_eq);
  also have "a mod m = a" by (insert p1, auto simp add: SR_m_mod_prop);
  also have "b mod n = b" by (insert p2, auto simp add: SR_n_mod_prop);
  finally have "x mod m = a & x mod n = b" .;
  with p3 p4 have "zgcd (x mod m, m) = 1 & zgcd (x mod n, n) = 1" by auto;
  with zgcd_ac have  "zgcd (m, x mod m) = 1 & zgcd (n, x mod n) = 1" by auto;
  with zgcd_eq2 have "zgcd (m, x) = 1 & zgcd(n, x) = 1" by auto;
  with zgcd_zmult_prop have "zgcd(m * n, x) = 1" by auto;
  with zgcd_eq2 have "zgcd(m*n, x mod (m*n)) = 1" by auto;
  thus "zgcd (x mod (m * n), m * n) = 1" by (auto simp add: zgcd_ac);
next;
  fix a b x;
  assume p1: "a : SR m" and p2: "zgcd (a, m) = 1" and p3: "[x = a] (mod m)";
  then have "a = a mod m" by (auto simp add: SR_m_mod_prop);
  also have "... = x mod m";
  proof-;
    have "0 < m" by (insert m_ge_1, auto);
    with p3 zcong_sym show ?thesis;
      by (auto simp add:  zcong_zmod_eq [THEN sym]);
  qed;
  also have "... = x mod (m*n) mod m";
    by (insert m_ge_1, auto simp add: zmod_zmult_zmod);
  finally show "a = x mod (m * n) mod m" .;
next;
  fix a b x;
  assume p1: "b : SR n" and p2: "zgcd (b, n) = 1" and p3: "[x = b] (mod n)";
  then have "b = b mod n" by (auto simp add: SR_n_mod_prop);
  also have "... = x mod n";
  proof-;
    have "0 < n" by (insert n_ge_1, auto);
    with p3 zcong_sym show ?thesis;
      by (auto simp add:  zcong_zmod_eq [THEN sym]);
  qed;
  also have "... = x mod (m*n) mod n";
    by (insert n_ge_1, auto simp add: zmod_zmult_zmod2);
  finally show "b = x mod (m * n) mod n" .;
qed;

lemma (in PHI2) ResUnits_image_prop: "f ` ResUnits(m * n) = ResUnits(m) <*> ResUnits(n)";
  by (insert aux1_ResUnits_image_prop aux2_ResUnits_image_prop, auto);

lemma (in PHI2) mn_prop: "m ~= 1 | n ~= 1 ==> 1 < m * n";
proof-;
  assume "m ~= 1 | n ~= 1";
  then have "1 ~= m * n";
      by (auto, insert n_ge_1 m_ge_1 zmult_eq_1_iff [of m n], auto);
  moreover from n_ge_1 m_ge_1 have "0 < m * n";
    by (auto simp add: mult_pos);
  ultimately show ?thesis by arith;
qed;

lemma (in PHI2) aux1_big_prop3: "m ~= 1 | n ~= 1 ==>
    {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = ResUnits(m*n)";
  apply (auto simp add: PHI2_def ResUnits_def SR_def);
  apply (case_tac "x = m * n");
  apply (insert mn_prop);
  apply (auto);
  apply (case_tac "x = m * n");
  apply (insert mn_prop);
  apply (auto);
  apply (case_tac "x = 0", auto);
  apply (case_tac "x = 0", auto);
done;

lemma (in PHI2) aux2_big_prop3: "m ~= 1 ==> 
                  {x. 1 <= x & x <= m & zgcd (x, m) = 1} = ResUnits(m)";
  apply (auto simp add: ResUnits_def SR_def);
  apply (case_tac "x = m", auto);
  apply (case_tac "x = 0", auto);
done;

lemma (in PHI2) aux3_big_prop3: "n ~= 1 ==> 
                  {x. 1 <= x & x <= n & zgcd (x, n) = 1} = ResUnits(n)";
  apply (auto simp add: ResUnits_def SR_def);
  apply (case_tac "x = n", auto);
  apply (case_tac "x = 0", auto);
done;

(* FINALLY *)

theorem (in PHI2) big_prop3: "phi(m * n) = phi(m) * phi(n)";
proof-;
  have "phi(m*n) = int(card(ResUnits(m*n)))";
    apply (auto simp add: phi_def);
    apply (case_tac "m = 1");
    apply (case_tac "n = 1");defer;defer;
    apply (case_tac "n = 1");
  proof-;
    assume "m ~= 1";
    then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
      by (auto simp add: aux1_big_prop3);
  next;
    assume "m ~= 1";
    then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
      by (auto simp add: aux1_big_prop3);
  next;
    assume "m = 1" and "n = 1";
    then have "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card {x. (1::int) <= x & x <= 1}";
      by(auto);
    also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
      by (auto);
    also have "card {x. (0::int) < x & x <= 1} = nat 1";
      apply (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}");
      apply auto;
      done;
    finally have p1: "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = nat 1" .;
    from prems have "card (ResUnits (m * n)) = card {x. (0::int) <= x & x < 1}";
      by (auto); 
    also have "... = nat 1"
      apply (subgoal_tac "{x. (0::int) <= x & x < 1} = {0..1(}");
      apply auto;
      done;
    finally have "card (ResUnits (m * n)) = nat 1" .;
    with p1 show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
      by (auto);
  next;
    assume "n ~= 1";
    then show "card {x. 1 <= x & x <= m * n & zgcd (x, m * n) = 1} = card (ResUnits (m * n))";
      by (auto simp add: aux1_big_prop3);
  qed;
  also have "card (ResUnits (m * n)) = card (f ` ResUnits (m * n))";
    apply (insert ResUnits_mn_finite ResUnits_inj_on_f);
    apply (auto simp add: card_image);
  done;
  also have "f ` ResUnits (m * n) = ResUnits(m) <*> ResUnits(n)";
    by (auto simp add: ResUnits_image_prop);
  also have "card (ResUnits m <*> ResUnits n) = card (ResUnits m) * card (ResUnits n)";
    apply (insert ResUnits_m_finite ResUnits_n_finite);
    by (simp add: setsum_constant);
  also have "int (card (ResUnits m) * card (ResUnits n)) = int (card (ResUnits m)) * int (card (ResUnits n))";
    by (auto simp add: zmult_int);
  also have "int (card (ResUnits m)) = phi (m)";
    apply (auto simp add: phi_def);
    apply (case_tac "m = 1");
  proof-;
    assume "m = 1";
    then have "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = card {x. (1::int) <= x & x <= 1}";
      by(auto);
    also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
      by (auto);
    also have "card {x. (0::int) < x & x <= 1} = nat 1";
      by (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}", auto);
    finally have p1: "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = nat 1" .;
    from prems have "card (ResUnits (m)) = card {x. (0::int) <= x & x < 1}";
      by (auto);
    also have "... = nat 1" 
      apply (subgoal_tac "{x. 0 ≤ x ∧ x < 1} = {0..1(}");
      apply (erule ssubst);
      apply auto;
      done;
    finally have "card (ResUnits (m)) = nat 1" .;
    with p1 have "card {x. 1 <= x & x <= m & zgcd (x, m) = 1} = card (ResUnits (m))";
      by (auto);
    then show "card (ResUnits m) = card {x. 1 <= x & x <= m & zgcd (x, m) = 1}"
      by auto;
  next;
    assume "m ~= 1";
    then show "card (ResUnits m) = card {x. 1 <= x & x <= m & zgcd (x, m) = 1}"
      by(auto simp add: aux2_big_prop3);
  qed;
  also have "int (card (ResUnits n)) = phi (n)";
    apply (auto simp add: phi_def);
    apply (case_tac "n = 1");
  proof-;
    assume "n = 1";
    then have "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = card {x. (1::int) <= x & x <= 1}";
      by(auto);
    also have "{x. (1::int) <= x & x <= 1} = {x. (0::int) < x & x <= 1}";
      by (auto);
    also have "card {x. (0::int) < x & x <= 1} = nat 1";
      apply (subgoal_tac "{x. (0::int) < x & x <= 1} = {)0..1}");
      apply (erule ssubst);
      apply auto;
      done;
    finally have p1: "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = nat 1" .;
    from prems have "card (ResUnits (n)) = card {x. (0::int) <= x & x < 1}";
      by (auto);
    also have "... = nat 1"
      apply (subgoal_tac "{x. 0 ≤ x ∧ x < 1} = {0..1(}"); 
      apply (erule ssubst, auto);
      done;
    finally have "card (ResUnits (n)) = nat 1" .;
    with p1 have "card {x. 1 <= x & x <= n & zgcd (x, n) = 1} = card (ResUnits (n))";
      by (auto);
    then show "card (ResUnits n) = card {x. 1 <= x & x <= n & zgcd (x, n) = 1}"
      by auto;
  next;
    assume "n ~= 1";
    then show "card (ResUnits n) = card {x. 1 <= x & x <= n & zgcd (x, n) = 1}"
      by(auto simp add: aux3_big_prop3);
  qed;
  finally show ?thesis .;
qed;

end