Theory Chebyshev1

(*  Title:      Chebyshev1.thy
    Author:     Paul Raff and Jeremy Avigad
*)

header {* Chebycheff's functions  *}

theory Chebyshev1 = Complex + PrimeFactorsList + RealLib:;

consts
  lprime ::      "nat => real"
  Lambda ::      "nat => real"
  theta ::       "nat => real" 
  psi ::         "nat => real"
  char_prime ::  "nat => real"
  pi         ::  "nat => real"  
  nmult      ::  "nat => nat => nat"                                

defs
  lprime_def: "lprime(x) == (if (x : prime)
                 then (ln(real(x)))
                 else 0)"                  
  theta_def:  "theta(x) == sumr 0 (x+1) lprime"

  Lambda_def: "Lambda(x) == if (EX p a. (p:prime) & (p^a = x) & 0 < a) 
                 then ln(real(THE p. (EX a. (p:prime) & (p^a = x)))) 
                 else 0"
  psi_def:    "psi(x) == sumr 0 (x+1) Lambda"

  char_prime_def: "char_prime(x) == if (x:prime) 
                 then 1 
                 else 0"
  pi_def: "pi(x) == real(card({y. y<=x & y:prime}))"

  nmult_def: "nmult x y == multiplicity (int x) (int y)";

locale l =
  fixes x::"nat"
  and  A::"nat set"
  and  B::"nat set" 
  and  C::"(nat*nat) set"
  and  D::"(nat*nat) set"   
  and  E::"(nat*nat) set"
  and  F::"nat set"                         
  and  f::"nat*nat => nat"
  and  g:: "nat => (nat*nat)"
  and  G::"nat set" 
  and  H::"nat => nat set"
  and  J::"nat set"                            

defines
      A_def:"A == {y. (y:{0..x} & (EX p a. (p:prime & 0<a & p^a=y)))}"
  and B_def:"B == {y. (y:{0..x} & ~(EX p a. (p:prime & 0<a & p^a=y)))}"
  and C_def:"C == {(p,a). (p:prime & 0<a & p^a:{0..x})}"
  and D_def:"D == {(p,a). (p:prime & a = 1 & p^a:{0..x})}"
  and E_def:"E == {(p,a). (p:prime & 1 < a & p^a:{0..x})}"
  and F_def:"F == {p. p:prime & p:{0..x}}"
  and f_def:"f y == (fst y)^(snd y)"
  and g_def:"g z == (z,1)"
  and G_def:"G == {d. 0 < d & d dvd x}"
  and H_def:"H(p) == {y. y:{0..x} & (EX a. (0 < a & p^a = y))}"
  and J_def:"J == {p. p : prime & p dvd x}";

subsection {* Miscellaneaous *}

lemma prime_prop2: "a:prime ==> b:prime ==> (0<n) ==> a dvd b^n ==> a=b";
  apply (frule prime_dvd_power);
  apply (assumption);
  by (auto simp add: prime_def);

lemma dvd_self_exp [rule_format]: "0 < n --> (m::nat) dvd m^n";
  apply (induct_tac n);
  by auto;

lemma prime_prop: "a:prime ==> b:prime ==> 0<c ==> 0<d ==> a^c = b^d ==> a=b";
  apply (subgoal_tac "a dvd b^d");
  apply (erule prime_prop2);
  prefer 3;
  apply (assumption)+;
  apply (subgoal_tac "a dvd a^c");
  apply simp;
  by (erule dvd_self_exp);

lemma  power_lemma [rule_format]:  "(1::nat) < a --> (0::nat) < c --> 1 < a^c";
  apply (induct_tac c);
  apply force;
  apply auto;
  apply (subgoal_tac "1 < a * a^n");
  apply force;
  apply (subgoal_tac "1 < a");
  apply (simp only: power_gt1_lemma);
  apply auto;
done;

lemma prime_prop_lzero: "a:prime ==> b:prime ==> 0<c ==> a^c = b^d ==> a=b";
  apply (case_tac "0=d");
  apply auto;
  apply (subgoal_tac "1 < a");
  apply (subgoal_tac "1 < a^c");
  apply (force);
  apply (rule power_lemma);
  apply force;
  apply force;
  apply (subgoal_tac "2 <= a");
  apply force;
  apply (rule prime_ge_2);
  apply force;
  apply (rule prime_prop);
  apply auto;
done;

lemma prime_prop_rzero: "a:prime ==> b:prime ==> 0<d ==> a^c = b^d ==> a=b";
  apply (subgoal_tac "b^d = a^c");
  apply (subgoal_tac "b=a");
  apply force;
  apply (rule prime_prop_lzero);
  apply auto;
done;

lemma prime_prop2: "a:prime ==> b:prime ==> (0<c) ==> (0<d) ==> 
    a^c = b^d ==> c=d";
  apply (frule prime_prop);
  prefer 4;
  apply (assumption)+;
  apply simp;
  by (auto simp add:prime_def);

lemma prime_prop_pair: "(fst x):prime ==> (fst y):prime ==> 0<(snd x) ==> 0<(snd y) ==> (fst x)^(snd x) = (fst y)^(snd y) ==> x=y";     
  apply (frule prime_prop2);
  apply auto;
  apply (subgoal_tac "fst x  = fst y");           
  apply (subgoal_tac "snd x = snd y");
  apply (auto simp add: prime_prop prime_prop2);
  apply (simp add: prod_eqI);                                              
done;

lemma real_addition: "(c::real) * real(Suc x) = c + c * real(x)";
  by (simp add: real_of_nat_Suc right_distrib);

lemma setsum_bound_real: "finite A ==> ALL x:A. (f(x) <= (c::real)) ==> setsum f A <= c * real(card A)";
  apply (induct set: Finites, auto);
  apply (simp add: real_addition);                                  
done;

lemma sumr_suc: "sumr 0 x f + f x = sumr 0 (x+1) f";
  apply auto;                                                  
done;

lemma real_power: "((a::nat)^b <= x) = ((real a) ^ b <= real(x))";
  apply (simp only: real_of_nat_le_iff [THEN sym]);
  apply (simp add: realpow_real_of_nat);
done;

lemma zprime_pos: "x : zprime ==> 0 < x";
  apply (auto simp add: zprime_def);
done;

lemma int_nat_inj: "nat x = nat y ==> 0 < x ==> 0 < y ==> x = y";
  apply (subgoal_tac "int (nat x) = int (nat y)");
  apply auto;
done;

lemma setprod_multiplicity_real: "0 < n ==> real n = 
    setprod (%p. (real p)^(multiplicity p n)) 
      {p. p : zprime & p dvd n}";
apply (frule n_eq_setprod_multiplicity);
apply (subgoal_tac "real (∏p∈{p. p ∈ zprime ∧ p dvd n}. 
  p ^ multiplicity p n) = (∏p∈{p. p ∈ zprime ∧ p dvd n}. 
    (real p) ^ multiplicity p n)");
apply force;
apply (subst setprod_real_of_int);
apply (rule setprod_cong);
apply (rule refl);
apply (subst real_of_int_power);
apply (rule refl);
done;

lemma multiplicity_nmult_eq: "multiplicity x y = nmult (nat x) (nat y)";
  apply (auto simp add: nmult_def);
  apply (simp add: multiplicity_def pfactors_le_1);
  apply (subgoal_tac "x ~: zprime");
  apply (subgoal_tac "0 ~: zprime");
  apply (auto simp add: not_zprime_multiplicity_eq_0 zprime_def);
done;

subsection {* Basic properties *}

lemma Lambda_eq_aux: "[|p ∈ prime; 0 < a|]
    ==> (THE pa. pa ∈ prime ∧ (∃aa. pa ^ aa = p ^ a)) = p";
  apply (rule the_equality);
  apply auto;
  apply (erule prime_prop);
  apply assumption;
  prefer 3;
  apply assumption;
  apply (subgoal_tac "aa ~= 0");
  apply force;
  apply (subgoal_tac "p^a ~= 1");  
  apply (rule notI2);
  apply assumption;
  apply simp;
  apply (subgoal_tac "1 < p^a");
  apply force;
  apply (rule power_lemma);
  apply (force simp add: prime_def);
  apply assumption+;
done;

lemma Lambda_eq: "p:prime ==> 0 < a ==> Lambda(p^a) = ln(real p)";
  apply (unfold Lambda_def);
  apply auto;
  apply (subst Lambda_eq_aux);
  apply auto;
done;

lemma Lambda_eq2: "~ (EX p a. p : prime & p ^ a = x & 0 < a) ==> 
  Lambda x = 0";
  apply (unfold Lambda_def);
  apply auto;
done;

lemma Lambda_zero: "Lambda 0 = 0";
  apply (subst Lambda_eq2);
  apply (auto simp add: prime_def); 
  done;

lemma Lambda_ge_zero: "0 <= Lambda x";
  apply (case_tac "EX p a. p : prime & p ^ a = x & 0 < a");
  apply (auto simp add: Lambda_eq Lambda_eq2); 
  apply (rule ln_ge_zero);
  apply (auto simp add: prime_def);
done;

lemma psi_diff1: "psi (x + 1) - psi x = Lambda (x+1)";
  by (simp add: psi_def);

lemma psi_diff2: "1 <= x ==> Lambda x = psi x - psi (x - 1)";
  apply (subgoal_tac "x = (x - 1) + 1");
  apply (erule ssubst);
  apply (subst psi_diff1 [THEN sym]);
  apply simp;
  apply simp;
done;

lemma psi_zero: "psi 0 = 0";
  by (simp add: psi_def Lambda_zero);

lemma psi_plus_one: "psi(x + 1) = psi x + Lambda(x + 1)";
  apply (unfold psi_def);
  apply auto;
done;

lemma psi_def_alt: "psi x = (∑i=1..x. Lambda i)";
  apply (induct x);
  apply (simp add: psi_zero);
  apply (subgoal_tac "Suc n = n + 1");
  apply (erule ssubst);back;
  apply (subst psi_plus_one);
  apply (case_tac "n = 0");
  apply simp;
  apply (subst setsum_range_plus_one_nat);
  apply auto;
done;

lemma psi_mono: "x <= y ==> psi x <= psi y";
  apply (unfold psi_def);
  apply (case_tac "x = y");
  apply simp;
  apply (rule sumr_le);
  apply clarify;
  apply (rule Lambda_ge_zero);
  apply simp;
done;

lemma psi_ge_zero: "0 <= psi x"; 
  apply (unfold psi_def);
  apply (rule sumr_ge_zero);
  apply (rule allI);
  apply (rule Lambda_ge_zero);
done;

lemma theta_geq_zero: "0 <= theta n";
  apply (unfold theta_def);
  apply (rule sumr_ge_zero);
  apply (unfold lprime_def);
  apply auto;
  apply (rule ln_ge_zero);
  apply (auto simp add: prime_def);
done;

lemma theta_zero: "theta 0 = 0";
  apply (unfold theta_def);
  apply simp;
  apply (unfold lprime_def);
  apply (simp add: prime_def);
done;
  
lemma theta_1_is_0: "theta(1) = 0";
  by (simp add: theta_def lprime_def prime_def);

lemma big_lemma1: "pi(2) = 1";
  apply (simp add: pi_def);
  apply (subgoal_tac "{y::nat. y <= (2::nat) & y : prime} = {2}");             
  apply (erule ssubst);    
  apply (simp add: real_of_nat_inject);
  apply auto;
  apply (case_tac "x=0");
  apply simp;
  apply (simp add: zero_not_prime);           
  apply (case_tac "x=1");                                            
  apply (simp add: one_not_prime);
  apply auto;
  apply (simp add: two_is_prime);
done;

subsection {* Comparing psi and theta *}

lemma theta_setsum_eq1: "theta(x) = setsum lprime {0..x}"; 
  apply (simp only: theta_def);
  apply (auto simp add: setsum_sumr2);                             
done;

lemma prime_partition: "{p. p<x} = {p. p<x & p:prime} Un {p. p<x & p~:prime}";
  apply auto;
done;

lemma prime_partition_le: "{p. p<=x} = {p. p<=x & p:prime} Un 
    {p. p<=x & p~:prime}";
  by auto; 

lemma all_nonprime_set_l: "[| finite A;  ALL x:A. x ~: prime |] ==> 
    setsum lprime A = 0";
  apply (rule setsum_0');
  apply (auto simp add: lprime_def);
  done;

lemma (in l) finite_A: "finite A";
  apply (auto simp add: A_def);
  apply (rule finite_subset [of "{y. y <= x & 
    (EX p. p : prime & (EX a. 0 < a & p ^ a = y))}" "{..x}"]);
  apply auto;
  done;

lemma (in l) finite_B: "finite B";
  apply (auto simp add: B_def);
  apply (rule finite_subset [of "{y. y <= x & (
    ALL p. p : prime --> (ALL a. a = 0 | p ^ a ~= y))}" "{..x}"]);
  apply auto;
  done;

lemma (in l) A_B_disjoint: "A Int B = {}";
  apply (unfold A_def B_def);
  apply blast;
  done;

lemma (in l) A_B_all: "A Un B = {y. y<=x}";
  apply (unfold A_def B_def);
  apply auto;
  done;

lemma (in l) cor_psi_sum: "psi(x) = setsum Lambda A + setsum Lambda B";
  apply (unfold psi_def);
  apply (subst setsum_sumr2 [THEN sym]);
  apply (subst setsum_Un_disjoint [THEN sym]);
  apply (rule finite_A, rule finite_B, rule A_B_disjoint);
  apply (subgoal_tac "{0..x} = A Un B");
  apply force;
  apply (unfold A_def B_def);
  apply blast;
  done;

lemma (in l) B_kernel_for_Lambda: "y:B ==> Lambda(y) = 0";
  apply (auto simp add: B_def Lambda_def);
  apply (drule_tac x = p in spec);
  apply (clarify);
  apply (drule_tac x = a in spec);
  by auto;

lemma (in l) sum_over_B_of_Lambda_zero: "setsum Lambda B = 0";
  apply (rule setsum_0');
  apply (rule ballI);
  apply (rule B_kernel_for_Lambda);
  apply assumption;
  done;

lemma (in l) inj_on_C: "inj_on f C";
  apply (rule inj_onI);
  apply (unfold C_def f_def);
  apply (subgoal_tac "(fst xa):prime");
  apply (subgoal_tac "(fst y):prime" "0<(snd xa)" "0<snd y");
  apply (auto simp add: prime_prop_pair);
done;

lemma (in l) range_of_C_is_A: "f`C = A";                                      
  apply (auto simp add: C_def A_def f_def image_def);
  done;

lemma (in l) finite_C: "finite C";
  apply (rule finite_imageD);
  apply (subst range_of_C_is_A);
  apply (rule finite_A, rule inj_on_C);
  done;

lemma (in l) D_subset_C: "D <= C";
  by (auto simp add: D_def C_def);

lemma (in l) E_subset_C: "E <= C";                               
  by (auto simp add: E_def C_def);

lemma (in l) Lambda_reindex_1: "setsum Lambda (f`C) = setsum (Lambda o f) C";
  apply (rule setsum_reindex);
  apply (simp add: finite_C);
  apply (simp add: inj_on_C);
done;

lemma (in l) psi_Lambda_eq_over_C: "psi(x) = setsum (Lambda o f) C";
  apply (simp add: Lambda_reindex_1 [THEN sym]);
  apply (subst range_of_C_is_A);
  apply (subst cor_psi_sum);
  apply (subst sum_over_B_of_Lambda_zero);
  apply simp;
done;

lemma psi_alt_def: "psi(x) = (∑u:{(p,a). (p:prime & 0<a & p^a:{0..x})}.
Lambda((fst u)^(snd u)))"; 
  apply (subst l.psi_Lambda_eq_over_C);
  apply (unfold o_def);
  apply (rule refl);
done;
                                          
lemma (in l) C_eq_D_Un_E: "C = D Un E";
  apply (auto simp add: C_def D_def E_def);
done;

lemma (in l) D_Int_E_empty: "D Int E = {}";
  by (auto simp add: D_def E_def);

lemma (in l) finite_D: "finite D";
  apply (rule finite_subset);
  apply (rule D_subset_C);
  apply (rule finite_C);
done;

lemma (in l) finite_E: "finite E";
  apply (rule finite_subset);
  apply (rule E_subset_C);
  apply (rule finite_C);
done;

lemma (in l) setsum_C_D_E: "setsum (Lambda o f) C = setsum (Lambda o f) D + 
    setsum (Lambda o f) E";
  apply (subgoal_tac "C = D Un E");
  apply simp;                                 
  apply (rule setsum_Un_disjoint);
  apply (rule finite_D, rule finite_E, rule D_Int_E_empty, rule C_eq_D_Un_E);
done;

lemma (in l) psi_Lambda_eq: "psi(x) = setsum (Lambda o f) D + 
    setsum (Lambda o f) E";
  apply (subst setsum_C_D_E [THEN sym]);
  apply (rule psi_Lambda_eq_over_C);
done;

lemma (in l) inj_on_g_F: "inj_on g F";
  apply (auto simp add: inj_on_def F_def g_def);
done;

lemma (in l) g_image_F_is_D: "g`F = D";
  apply (auto simp add: g_def F_def D_def);
done;

lemma (in l) finite_F: "finite F";
  apply (unfold F_def);
  apply (subgoal_tac "finite {..x}");
  apply (rule finite_subset);
  prefer 2;
  apply assumption;
  apply auto;
done;

lemma (in l) reindex_Lambda_f_g: "setsum (Lambda o f) D = 
    setsum (Lambda o f o g) F";
  apply (insert g_image_F_is_D [THEN sym] inj_on_g_F finite_F);
  apply (simp add: setsum_reindex);
done;

lemma aux1 [rule_format]: "1 < (a::nat) --> 0 < b --> Suc 0 < a^b"; 
  apply (induct_tac b);
  apply force;
  apply clarsimp;
  apply (case_tac "n = 0");
  apply auto;
  apply (rule one_less_mult);
  apply auto;
done;

lemma aux2 [rule_format]: "1 < (a::nat) & 1 < b --> a < a^b";
  apply (induct_tac "b");
  apply force;
  apply clarify;
  apply simp;
  apply (rule aux1);
  apply auto;
done;

lemma aux3: "p:prime ==> 1 < a ==> ~ (p^a : prime)";
  apply (unfold prime_def);
  apply (clarsimp);
  apply (rule_tac x = "p" in exI)
  apply (rule conjI);
  apply (rule dvd_self_exp);
  apply force;
  apply (rule conjI);
  apply force;
  apply (subgoal_tac "p < p^a");
  apply force;
  apply (rule aux2);
  by auto;

lemma prime_power_must_be_one: "p:prime ==> p^a:prime ==> a=1";
  apply auto;
  apply (case_tac "a=0");           
  apply simp;                                  
  apply (simp add: prime_def);                                             
  apply (case_tac "a=1");   
  apply (simp_all add: aux3);
done;

lemma (in l) F_prop: "p:F --> (Lambda(f(g(p)))) = ln(real(p))";
  apply (unfold F_def f_def g_def);
  apply clarify;
  apply simp;
  apply (unfold Lambda_def);
  apply auto;
  apply (subgoal_tac "(THE pa::nat. pa : prime & 
   (EX aa::nat. pa ^ aa = p ^ a)) = p^a");
  apply (erule ssubst);
  apply (simp);
  apply (rule the_equality);
  apply (auto simp add: if_splits);
  apply (rule_tac x = "1" in exI);
  apply simp; 
  apply (subgoal_tac "a=1");            
  apply simp;   
  apply (subgoal_tac "aa=1");              
  apply simp;
  apply (subgoal_tac "pa^aa : prime");
  prefer 2;                                    
  apply simp;
  apply (simp only: prime_power_must_be_one);
  apply (simp only: prime_power_must_be_one);
  apply (drule_tac x = "p" in spec);
  apply simp;                                  
  apply (drule_tac x = "1" in spec); 
  apply auto;
done;

lemma (in l) sum_over_F: "setsum (Lambda o f o g) F = setsum (ln o real) F"; 
  apply (rule setsum_cong);
  apply (auto simp add: F_prop);
done;

lemma (in l) sum_over_F2_lemma1: "setsum lprime {0..x} = 
    setsum lprime ({p. p<=x & p:prime} Un {p. p<=x & p~:prime})";
  apply (subgoal_tac "{0..x} = {p. p<=x}");
  apply (erule ssubst);
  apply (subgoal_tac "{p. p<=x} = 
    ({p::nat. p <= x & p : prime} Un {p::nat. p <= x & p ~: prime})");
  apply (erule ssubst);  
  apply simp;
  apply (auto simp add: prime_partition);
done;

lemma (in l) sum_over_F2_lemma2: 
  "setsum lprime ({p. p<=x & p:prime} Un {p. p<=x & p~:prime}) = 
    setsum lprime {p. p<=x & p:prime} + setsum lprime {p. p<=x & p~:prime}";
  apply (rule setsum_Un_disjoint);
  apply auto;
  apply (rule finite_subset_AtMost_nat);
  apply force;
  apply (rule finite_subset_AtMost_nat);
  apply force;
done;

lemma (in l) l_set_of_primes: "ALL x:P. x:prime ==> 
    setsum lprime P = setsum (ln o real) P";
  apply (rule setsum_cong);
  apply (auto simp add: lprime_def);
done;

lemma (in l) sum_over_F2: "setsum (ln o real) F = theta(x)";
  apply (unfold F_def theta_def);
  apply (subst setsum_sumr2 [THEN sym]);
  apply (subst l_set_of_primes [THEN sym]);
  apply force;
  apply (subgoal_tac "setsum lprime {0..x} = 
    setsum lprime ({p. p:prime & p<=x} Un {p. p~:prime & p<=x})");
  apply (erule ssubst);
  apply (subst setsum_Un_disjoint);
  apply (rule finite_subset_AtMost_nat);
  apply auto;
  apply (rule finite_subset_AtMost_nat);
  apply auto;
  apply (subst all_nonprime_set_l);
  apply (rule finite_subset_AtMost_nat);
  apply auto;
  apply (subgoal_tac "{0..x} = 
    {p. p:prime & p<=x} Un {p. p~:prime & p<=x}");
  apply auto;
done;

lemma (in l) psi_theta_sum: "psi(x) = theta(x) + setsum (Lambda o f) E";
  apply (subst sum_over_F2 [THEN sym]);
  apply (subst sum_over_F [THEN sym]);                                     
  apply (subst reindex_Lambda_f_g [THEN sym]);           
  apply (rule psi_Lambda_eq);
done;

lemma exponent_eq_0_iff: "2 <= p ==> Suc 0 = p^a ==> a = 0";
  apply (case_tac a);
  apply (auto simp add: power_Suc);
done;

lemma (in l) Lambda_positive: "ALL x:E. 0 <= Lambda(f(x))";
  apply (auto simp add: E_def Lambda_def f_def);
  apply (subgoal_tac "0 = ln 1");                                              
  apply (erule ssubst [of "(0::real)" "ln (1::real)" _]);
  apply (subgoal_tac "0 < real((THE p::nat. p : prime & 
    (EX aa::nat. p ^ aa = a ^ b)))");
  apply (simp only: ln_le_cancel_iff);
  apply (subgoal_tac "(1 :: real) = real(1::nat)");
  apply (erule ssubst [of "(1::real)" "real (1::nat)" _]);
  apply (simp only: real_of_nat_le_iff);
  apply (auto);
  apply (rule Suc_leI);
  apply simp;
  apply (rule theI2);
  apply auto; 
  prefer 2;            
  apply (simp add: prime_pos);
  apply (case_tac "aaa = 0");
  prefer 2;                           
  apply (subgoal_tac "0 < aaa");
  prefer 2;                              
  apply simp;
  apply (subgoal_tac "p^aa = pa^aaa");
  apply (simp only: prime_prop);
  apply simp;
  apply auto;
  apply (subgoal_tac "Suc 0 = p^aa");
  prefer 2;                                   
  apply simp;
  apply (subgoal_tac "2 <= p");
  apply (subgoal_tac "0 = aa");
  prefer 2;
  apply (simp add: exponent_eq_0_iff);
  prefer 2;
  apply (simp add: prime_ge_2);
  apply (simp only: order_less_imp_not_eq [of "0" "aa"]);
done

lemma real_power_ln: "1 < a ==> 0<x ==> ((a::nat)^b <= x) = 
    (real(b) <= ln(real x)/ln(real a))";
  apply (simp only: real_power);
  apply (subgoal_tac "0 < real a ^ b");
  apply (subgoal_tac "0 < real(x)");
  apply (simp only: ln_le_cancel_iff [THEN sym]);
  apply (simp add: ln_realpow);
  apply (subgoal_tac "0 < ln (real a)");
  apply (simp add: pos_le_divide_eq);
  apply (subgoal_tac "1 < real a");
  apply (simp add: ln_gt_zero);
  apply force;
  apply force;
  apply (subgoal_tac "0 < a");
  apply (subgoal_tac "0 < a^b");
  apply (simp add: real_of_nat_less_iff);
  apply (simp add: zero_less_power);
  apply force;
done;

(*
lemma (in l) extent_of_E: "E <= {1..x} <*> 
    {1..nat(floor(ln(real x)/ln(2)))}";
  apply (auto simp add: E_def);
  apply (subgoal_tac "2 <=a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "2 <= a");
  apply (subgoal_tac "2 <= b");
  apply (subgoal_tac "a <= a^2");
  apply (subgoal_tac "a^2 <= a^b");
  apply force;
  apply (simp add: power_increasing);
  apply (subgoal_tac "0 <= a");
  apply (subgoal_tac "(a <= a^2) = (a^1 <= a^2)");
  apply (erule ssubst);
  apply (simp only: power_increasing);
  apply force;
  apply force;
  apply force;
  apply (simp add: prime_ge_2);
  apply (subst real_of_nat_le_iff [THEN sym]);
  apply (subgoal_tac "2^b <= x");
  apply (subgoal_tac "0 < x");
  apply (subgoal_tac "1 < a");
  apply (simp only: real_power_ln);
  apply (subgoal_tac "real(2::nat) = 2");
  apply (erule ssubst);
  apply (auto simp add: floor_bound);
  apply (subgoal_tac "2 <= a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "0 < a");
  apply (subgoal_tac "0 < a^b");
  apply (simp only: less_le_trans [of "0" "a^b" "x"]);
  apply (simp add: zero_less_power);
  apply (subgoal_tac "2 <= a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "2 <= a");
  apply (subgoal_tac "2^b <= a^b");
  apply force;
  apply (auto simp add: power_mono prime_ge_2);
  done;
*)

lemma (in l) extent_of_E2: "E <= {1..nat(floor(real(x) powr (1/2)))} <*> 
    {1..nat(floor(ln(real x)/ln(2)))}";
  apply (auto simp add: E_def);
  apply (subgoal_tac "2 <=a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "a <= natfloor(real x powr (1/2))");
  apply (simp add: natfloor_def);
  apply (subgoal_tac "a^2 <= x");
  apply (subgoal_tac "(real a) powr (real (2::nat)) <= real x");
  apply (subgoal_tac "((real a) powr (real (2::nat))) powr (1/2) <= (real x) powr (1/2)");
  apply (simp add: powr_powr);
  apply auto;
  apply (subgoal_tac "real a <= real x powr (1/2)");
  apply (rule real_le_natfloor);
  apply auto;
  apply (subgoal_tac "real a powr 1 = real a");
  apply force;
  apply (subst powr_one_gt_zero_iff);
  apply (subgoal_tac "2 <= a");
  apply arith;
  apply (simp add: prime_ge_2);
  apply (rule power_mono2);
  apply force+;
  apply (subgoal_tac "(2::real) = real (2::nat)");
  apply (erule ssubst);
  apply (subst powr_realpow);
  apply (subgoal_tac "2 <= a");
  apply arith;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "real a ^ 2 = real (a^2)");
  apply force;
  apply (rule realpow_real_of_nat);
  apply force+;
  apply (subgoal_tac "a^2 <= a^b");
  apply force;
  apply (rule power_increasing);
  apply force;
  apply (frule prime_ge_2);
  apply arith;
(* FIRST PART DONE! YAY! *)  
  apply (subgoal_tac "2^b <= x");
  apply (subgoal_tac "0 < x");
  apply (subgoal_tac "1 < a");
  apply (simp only: real_power_ln);
  apply (subgoal_tac "real(2::nat) = 2");
  apply (erule ssubst);
  apply (auto simp add: floor_bound);
  apply (subgoal_tac "2 <= a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "0 < a");
  apply (subgoal_tac "0 < a^b");
  apply (simp only: less_le_trans [of "0" "a^b" "x"]);
  apply (simp add: zero_less_power);
  apply (subgoal_tac "2 <= a");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "2 <= a");
  apply (subgoal_tac "2^b <= a^b");
  apply force;
  apply (auto simp add: power_mono prime_ge_2);
  done;

(*
lemma (in l) card_E_lemma: "card E <= 
    card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))})";
  apply (rule card_mono);
  prefer 2;
  apply (rule extent_of_E);
  apply simp;
  done;
*)

lemma (in l) card_E2_lemma: "card E <= 
    card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))})";
  apply (rule card_mono);
  prefer 2;
  apply (rule extent_of_E2);
  apply simp;
  done;

(*
lemma (in l) card_E_lemma2: 
    "card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))}) = 
      card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply simp;
done;
*)

lemma (in l) card_E2_lemma2: 
    "card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))}) = 
      card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply simp;
done;

(*
lemma (in l) card_E_lemma3: 
    "card ({1..x} <*> {1..nat(floor(ln(real x)/ln(2)))}) <= 
      card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply (auto simp add: card_E_lemma2);
done;
*)

lemma (in l) card_E2_lemma3: 
    "card ({1..nat(floor(real(x) powr (1/2)))} <*> {1..nat(floor(ln(real x)/ln(2)))}) <= 
      card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply (auto simp add: card_E2_lemma2);
done;

(*
lemma (in l) card_E:
    "card E <= card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply (insert card_E_lemma3);
  apply (insert card_E_lemma);
  apply (erule le_trans);
  apply assumption;
done;
*)

lemma (in l) card_E2:
    "card E <= card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))}";
  apply (insert card_E2_lemma3);
  apply (insert card_E2_lemma);
  apply (erule le_trans);
  apply assumption;
done;

(*
lemma card_E_real_lemma4: "real(floor(ln(real x)/ln(2))) <= ln(real x)/ln(2)";
  apply (simp add: real_of_int_floor_le);
done;
*)

lemma card_E2_real_lemma4: "real(floor(ln(real x)/ln(2))) <= ln(real x)/ln(2)";
  apply (simp add: real_of_int_floor_le);
done;

(*
lemma (in l) real_card_E: "real(card E) <= 
    real(card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))})";
  apply (simp only: real_of_nat_le_iff);
  apply (rule card_E);
done;
*)

lemma (in l) real_card_E2: "real(card E) <= 
    real(card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))})";
  apply (simp only: real_of_nat_le_iff);
  apply (rule card_E2);
done;

(*
lemma (in l) card_E_real_lemma6: "0 < x ==> 
    real(card {1..nat(floor(ln(real x)/ln(2)))}) <= ln(real x)/ln(2)";
  apply simp;
  apply (subgoal_tac "0 <= ln(real x) / ln 2");
  apply (rule real_nat_floor);
  apply auto;
  done;
*)

lemma (in l) card_E2_real_lemma6: "0 < x ==> 
    real(card {1..nat(floor(ln(real x)/ln(2)))}) <= ln(real x)/ln(2)";
  apply simp;
  apply (subgoal_tac "0 <= ln(real x) / ln 2");
  apply (rule real_nat_floor);
  apply auto;
  done;

(*
lemma (in l) card_E_real: "0 < x ==> real(card E) <= 
    real(x) * ln(real x)/ln(2)";
  proof-;
    assume pos: "0 < x";
    have step1: "real(card E) <= 
        real(card {1..x} * card {1..nat(floor(ln(real x)/ln(2)))})";
      by (rule real_card_E);
    also have step2: "... = 
        real(card {1..x}) * real(card {1..nat(floor(ln(real x)/ln(2)))})";
      by (rule real_of_nat_mult);
    also have step3: "... <= real(x) * ln(real x)/ln(2)";
      apply (simp add: card_E_real_lemma6);
      apply (subgoal_tac "real x * ln (real x) / ln 2 = 
        real x * (ln (real x) / ln 2)");
      apply (erule ssubst);
      apply (rule mult_left_mono);
      apply (subgoal_tac "0<= ln(real x)/ln 2");
      apply (rule real_nat_floor);
      apply force;
      apply (subgoal_tac "1<= real x");
      apply (drule ln_ge_zero);
      apply (subgoal_tac "0 < ln 2");
      apply (simp add: real_ge_zero_div_gt_zero);
      apply auto;
      apply (subgoal_tac "1<=x");
      apply (auto simp add: pos);
      apply (simp add: pos Suc_leI);
      done;
    finally show ?thesis;.;
qed;
*)

lemma (in l) card_E2_real: "0 < x ==> real(card E) <= 
    real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)";
  proof-;
    assume pos: "0 < x";
    have step1: "real(card E) <= 
        real(card {1..nat(floor(real(x) powr (1/2)))} * card {1..nat(floor(ln(real x)/ln(2)))})";
      by (rule real_card_E2);
    also have step2: "... = 
        real(card {1..nat(floor(real(x) powr (1/2)))}) * real(card {1..nat(floor(ln(real x)/ln(2)))})";
      by (rule real_of_nat_mult);
    also have step3: "... <= real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)";
      apply (simp add: card_E2_real_lemma6);
      apply (subgoal_tac "real (nat(floor(real(x) powr (1/2)))) * ln (real x) / ln 2 = 
        real (nat(floor(real(x) powr (1/2)))) * (ln (real x) / ln 2)");
      apply (erule ssubst);
      apply (rule mult_left_mono);
      apply (subgoal_tac "0<= ln(real x)/ln 2");
      apply (rule real_nat_floor);
      apply force;
      apply (subgoal_tac "1<= real x");
      apply (drule ln_ge_zero);
      apply (subgoal_tac "0 < ln 2");
      apply (simp add: real_ge_zero_div_gt_zero);
      apply auto;
      apply (subgoal_tac "1<=x");
      apply (auto simp add: pos);
      apply (simp add: pos Suc_leI);
      done;
    finally show ?thesis;.;
qed;

lemma (in l) E_bound_with_f: "y:E --> f(y) <= x";
  apply (auto simp add: E_def);                                               
  apply (auto simp add: f_def);
done;

lemma Lambda_prop: "ALL x. (0 < x --> Lambda(x) <= ln(real(x)))";
  apply (auto simp add: Lambda_def);
  apply (rule theI2);
  apply auto;
  apply (rule prime_prop_rzero);
  apply auto;
  apply (case_tac "aa=0");
  apply auto;
  apply (subgoal_tac "Suc 0 < p^1");
  apply (subgoal_tac "p^1 <= p^a");
  apply force;
  apply (rule power_increasing);
  apply force;
  apply force;
  apply (subgoal_tac "2 <= p^1");
  apply force;
  apply (subgoal_tac "2 <= p");
  apply (subgoal_tac "p = p^1");
  apply force;
  apply (rule power_one_right [THEN sym]);
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "x = p");
  apply (subgoal_tac "real(x) = real(p)");
  apply auto;
  apply (subgoal_tac "p^1 <= p^a");
  apply force;
  apply (rule power_increasing);
  apply force;
  apply force;
  apply (rule prime_prop_rzero);
  apply auto;
done;

lemma (in l) E_bound: "0 < x ==> y:E ==> (Lambda o f)(y) <= ln(real(x))";
  apply (auto simp add: E_def);
  apply (auto simp add: f_def);
  apply (subgoal_tac "0 < xa^y");
  apply (subgoal_tac "Lambda(xa^y) <= ln(real(xa^y))");
  apply (subgoal_tac "ln(real(xa^y)) <= ln(real(x))");
  apply force;
  apply (simp only: ln_le_cancel_iff);
  apply (simp add: Lambda_prop);
  apply (subgoal_tac "xa^1 <= xa^y");
  apply (subgoal_tac "0 < xa");
  apply force;
  apply (subgoal_tac "2 <= xa");
  apply force;
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "1 <= y");
  apply (rule power_increasing);
  apply auto;
  apply (subgoal_tac "2 <= xa");
  apply force;
  apply (auto simp add: prime_ge_2);
done;

(*
lemma (in l) sum_over_E_of_Lambda_o_f: "0 < x ==> 
    setsum (Lambda o f) E <=  real(x) * ln(real(x)) * ln(real(x)) / ln 2";
  apply (subgoal_tac "setsum (Lambda o f) E <= real(card E) * ln(real(x))");
  apply (subgoal_tac "real(card E) <= real(x) * ln(real x)/ln(2)");
  apply (subgoal_tac "real(card E) * ln(real(x)) <= 
    real(x) * ln(real x)/ln(2) * ln(real(x))");
  apply (subgoal_tac "setsum (Lambda o f) E <= 
    real(x) * ln(real x)/ln(2) * ln(real(x))");
  apply force;
  apply force;
  apply (subgoal_tac "0 <= ln(real(x))");
  apply (rule mult_right_mono);
  apply force;
  apply (subgoal_tac "1 <= x");
  apply (simp add: ln_ge_zero);
  apply force;
  apply (subgoal_tac "1 <= x");
  apply (simp add: ln_ge_zero);
  apply force;
  apply (simp add: card_E_real);
  apply (subgoal_tac "real (card E) * ln (real x) = 
    ln (real x) * real (card E)");
  apply (erule ssubst);
  apply (rule setsum_bound_real);
  apply (simp add: finite_E);
  apply (rule ballI);
  apply (rule E_bound);
  apply auto;
done;
*)

lemma (in l) sum_over_E2_of_Lambda_o_f: "0 < x ==> 
    setsum (Lambda o f) E <=  real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2";
  apply (subgoal_tac "setsum (Lambda o f) E <= real(card E) * ln(real(x))");
  apply (subgoal_tac "real(card E) <= real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2)");
  apply (subgoal_tac "real(card E) * ln(real(x)) <= 
    real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2) * ln(real(x))");
  apply (subgoal_tac "setsum (Lambda o f) E <= 
    real(nat(floor(real(x) powr (1/2)))) * ln(real x)/ln(2) * ln(real(x))");
  apply force;
  apply force;
  apply (subgoal_tac "0 <= ln(real(x))");
  apply (rule mult_right_mono);
  apply force;
  apply (subgoal_tac "1 <= x");
  apply (simp add: ln_ge_zero);
  apply force;
  apply (subgoal_tac "1 <= x");
  apply (simp add: ln_ge_zero);
  apply force;
  apply (simp add: card_E2_real);
  apply (subgoal_tac "real (card E) * ln (real x) = 
    ln (real x) * real (card E)");
  apply (erule ssubst);
  apply (rule setsum_bound_real);
  apply (simp add: finite_E);
  apply (rule ballI);
  apply (rule E_bound);
  apply auto;
done;

(*
lemma (in l) psi_theta_bound: "0 < x ==> psi(x) <= 
    theta(x) + real(x) * ln(real(x)) * ln(real(x)) / ln 2";
  apply (subgoal_tac "psi(x) = theta(x) + setsum (Lambda o f) E");
  apply (subgoal_tac "setsum (Lambda o f) E <= 
    real(x) * ln(real(x)) * ln(real(x)) / ln 2");
  apply auto;
  apply (auto simp add: psi_theta_sum sum_over_E_of_Lambda_o_f);
done;
*)

lemma (in l) psi_theta_bound_for_real_aux: "0 < x ==> psi(x) <= 
    theta(x) + real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2";
  apply (subgoal_tac "psi(x) = theta(x) + setsum (Lambda o f) E");
  apply (subgoal_tac "setsum (Lambda o f) E <= 
    real(nat(floor(real(x) powr (1/2)))) * ln(real(x)) * ln(real(x)) / ln 2");
  apply auto;
  apply (auto simp add: psi_theta_sum sum_over_E2_of_Lambda_o_f);
done;

lemma psi_theta_bound_for_real: "0 < x ==> psi(x) <= 
    theta(x) + real(x) powr (1/2) * ln(real(x)) * ln(real(x)) / ln 2";
  apply (rule order_trans);
  apply (erule l.psi_theta_bound_for_real_aux);
  apply (rule add_left_mono);
  apply (rule divide_right_mono);
  apply (rule mult_right_mono)+;
  apply (subgoal_tac "nat(floor (?t)) = natfloor(?t)");
  apply (erule ssubst);
  apply (rule real_natfloor_le);
  apply (rule order_less_imp_le);
  apply (rule powr_gt_zero);
  apply (simp add: natfloor_def);
  apply auto;
done;

subsection {* Comparing pi and theta *}

lemma pi_set_zero: "finite A ==> ALL x:A.  x~:prime ==> 
    setsum char_prime A = 0";
  apply (rule setsum_0');
  apply (unfold char_prime_def);
  apply auto;
done;

lemma setsum_prime_split: "setsum f {p. p<=x} = 
    setsum f {p. p<=x & p:prime} + setsum f {p. p<=x & p~:prime}";
  apply (simp add: prime_partition_le);
  apply (rule setsum_Un_disjoint);
  apply auto;
  apply (auto intro: finite_subset_AtMost_nat);
done;

lemma setsum_char_prime_zero: "setsum char_prime {p. p<=x & p~:prime} = 0";
  apply (rule pi_set_zero);                                                
  by (auto intro: finite_subset_AtMost_nat);

lemma pi_setsum_equiv: "pi(x) = setsum char_prime {p. p<=x}";
  apply (auto simp add: pi_def char_prime_def);
  apply (simp add: setsum_prime_split);
  apply (simp add: setsum_char_prime_zero);
  apply (subgoal_tac "setsum char_prime {p::nat. p <= x & p : prime} = 
    setsum (%x. 1) {p::nat. p <= x & p : prime}");
  apply (erule ssubst);
  apply (subst real_card_eq_setsum);
  apply (force intro: finite_subset_AtMost_nat);
  apply simp;
  apply (rule setsum_cong [of "{p::nat. p <= x & p : prime}" 
    "{p::nat. p <= x & p : prime}" "char_prime" "%x. 1"]);
  apply (auto simp add: char_prime_def);       
done;

lemma pi_sumr_equiv: "pi(x) = sumr 0 (x+1) char_prime";
  apply (simp only: pi_setsum_equiv);
  apply (subgoal_tac "{p::nat. p <= x} = {0..x}");
  apply (erule ssubst);
  apply (auto simp add: setsum_sumr2);
done;

lemma pi_Suc: "pi(Suc x) = char_prime(Suc x) + pi(x)";
  apply (case_tac "(Suc x):prime");
  apply (simp add: pi_def char_prime_def);
  apply (subgoal_tac "{y::nat. y <= Suc x & y : prime} = 
    {y::nat. y <= x & y : prime} Un {Suc x}");
  apply (erule ssubst);
  apply (subst card_Un_disjoint);
  apply (force intro: finite_subset_AtMost_nat);
  apply simp;
  apply force;
  apply simp;
  apply auto;
  apply (simp add: pi_def char_prime_def);
  apply (rule arg_cong);back;
  apply auto;
  apply (case_tac "xa = Suc x");
  apply auto;
done;

lemma char_prime_def_eq: "1 <= n ==> 
    (theta(n+1) - theta(n)) / ln(real(n+1)) = char_prime(n+1)";
  apply (auto simp add: theta_def);
  apply (case_tac "Suc n:prime");
  apply (auto simp add: lprime_def char_prime_def real_divide_def);
done;

lemma nat_int_inj_on: "inj_on (%x. nat x) {p. p:zprime & (p dvd x)}";
  apply (rule inj_onI);
  apply auto;
  apply (rule int_nat_inj);
  apply (auto simp add: zprime_pos);
done;

lemma int_nat_inj_on: "inj_on int {p. p:prime & p dvd x}";
  apply (rule inj_onI);                                                        
  apply auto;
done;

subsection {* Expressing ln in terms of Lambda *}

lemma ln_product_sum: "finite A ==> ALL x:A. (0 < f(x)) ==> 
    ln (setprod f A) = setsum (ln o f) A";     
  apply (induct set: Finites);
  apply (simp add: setprod_def setsum_def);
  apply (simp add: setprod_insert setsum_insert);
  apply (subst ln_mult);
  apply (auto simp add: setprod_pos o_def);
done;

lemma multiplicity_eq_1: "1 < n ==> ln(real n) = 
    ln(setprod (%p. (real p)^(multiplicity p n)) {p. 0 < p & p : zprime & 
      p dvd n})";
  apply (subst ln_inj_iff);
  apply force;
  apply (rule setprod_pos);
  apply auto;
  apply (subgoal_tac "{p. 0 < p ∧ p ∈ zprime ∧ p dvd n} = 
    {p. p ∈ zprime ∧ p dvd n}");
  apply (erule ssubst);
  apply (rule setprod_multiplicity_real);
  apply (auto simp add: zprime_def);
done;

lemma divisor_set_fact:  "1 < n ==> {p::int. 0 < p & p : zprime & p dvd n} <= 
    {-n..n}";
  apply auto;
  apply (subgoal_tac "(-n <= x) = (-x <= n)");          
  apply (erule ssubst);                                                      
  apply (simp add: zdvd_imp_le);
  apply auto;
done;

lemma multiplicity_eq_2: "1 < n ==> ln(real n) = 
    setsum (%p. ln ((real p)^(multiplicity p n))) {p. 0 < p & p : zprime & 
      p dvd n}";
  apply (subst multiplicity_eq_1);
  apply (assumption);
  apply (subst ln_product_sum);
  apply (force intro: finite_subset_GreaterThan0AtMost_int zdvd_imp_le);
  apply force;
  apply (simp add: o_def);
done;

lemma multiplicity_eq_3: "1 < n ==> ln(real n) = 
    setsum (%p. real(multiplicity p n) * ln(real p)) {p. 0 < p & p : zprime & 
      p dvd n}";
  apply (subst multiplicity_eq_2, assumption);
  apply (rule setsum_cong);
  apply (rule refl);
  apply (subst ln_realpow);
  apply force;
  apply (rule refl);
done;

lemma (in l) finite_G: "0 < x ==> finite G";
  apply (unfold G_def);
  apply (rule finite_subset_GreaterThan0AtMost_nat);
  apply (auto intro: dvd_imp_le);
done;

lemma (in l) G_fact: "0 < x ==> G = (G Int A) Un (G Int B)";
  by (auto simp add: G_def A_def B_def dvd_def);

lemma (in l) Lambda_over_G_lemma1: "0 < x ==> 
    setsum Lambda G = setsum Lambda ((G Int A) Un (G Int B))";
  apply (rule setsum_cong);
  apply (simp only: G_fact [THEN sym]);
  by auto;                                     

lemma (in l) Lambda_over_G_lemma2: "0 < x ==> 
    setsum Lambda G = setsum Lambda (G Int A) + setsum Lambda (G Int B)";
  apply (subgoal_tac "setsum Lambda G = 
    setsum Lambda ((G Int A) Un (G Int B))");
  apply (erule ssubst);
  apply (subst setsum_Un_disjoint);
  apply (simp add: finite_subset finite_G);
  apply (simp add: finite_subset finite_G);
  apply (subgoal_tac "G Int A Int (G Int B) = G Int (A Int B)");
  apply (erule ssubst);
  apply (simp add: A_B_disjoint);
  apply force;
  apply (rule refl);
  apply (subst G_fact [THEN sym]);
  apply assumption;
  apply (rule refl);
done;

lemma (in l) Lambda_over_G_lemma3: "0 < x ==> setsum Lambda (G Int B) = 0";
  apply (rule setsum_0');
  apply (insert B_kernel_for_Lambda, blast);
done;

lemma (in l) Lambda_over_G_lemma4: "0 < x ==> 
    setsum Lambda G = setsum Lambda (G Int A)";            
  apply (auto simp add: Lambda_over_G_lemma2 Lambda_over_G_lemma3);
done;

lemma (in l) G_Int_A_Un_over_J: "G Int A = UNION J (%p. H(p) Int G)";
  apply (auto simp add: G_def A_def J_def H_def);
  apply (rule_tac x = "p" in exI);
  apply auto;
  apply (subgoal_tac "p dvd p^a");
  prefer 2;                                
  apply (case_tac a);                                         
  apply auto;
  apply (rule dvd_trans);           
  apply auto;                                  
done;

lemma (in l) finite_J: "0 < x ==> finite J";
  apply (simp add: J_def);
  apply (rule finite_subset_GreaterThan0AtMost_nat);
  apply auto;
  apply (erule prime_pos);
  apply (erule dvd_imp_le);
  apply assumption;
done;

lemma (in l) finite_H_p: "0 < x ==> finite (H(p))";
  apply (simp add: H_def);
  apply (rule finite_subset_AtMost_nat);                                             
  apply auto;
done;

lemma (in l) different_H: "0 < x ==> p1:prime ==> p2:prime ==> 
    p1 ~= p2 ==> H(p1) Int H(p2) = {}";
  apply (auto simp add: H_def);
  apply (simp add: prime_prop);                             
done;

lemma (in l) setsum_Lambda_G_lemma1: "0 < x ==> setsum Lambda G = 
    setsum (%p. setsum Lambda (H(p) Int G)) J";
  apply (simp add: Lambda_over_G_lemma4);
  apply (simp only: G_Int_A_Un_over_J);
  apply (rule setsum_UN_disjoint [of "J" "(%p. H(p) Int G)" "Lambda"]);
  apply (rule finite_J);
  apply (assumption);
  apply (force intro: finite_H_p);
  apply auto;
  apply (subgoal_tac "xa: H p Int H j");           
  apply (subgoal_tac "H p Int H j = {}");
  apply simp;
  apply (simp add: J_def different_H);
  apply (rule IntI);                                    
  apply auto;                                                      
done;

lemma (in l) inj_on_prime_power: "inj_on (%x. (p::nat)^x) {1..nmult p x}";
  apply (auto);
  apply (rule inj_onI);
  apply (case_tac "p:prime");
  apply (auto simp add: prime_prop2);
  apply (simp add: nmult_def);
  apply (subgoal_tac "multiplicity (int p) (int x) = 0");
  apply simp;
  apply (subgoal_tac "(int p)~:zprime");
  apply (rule not_zprime_multiplicity_eq_0 [of "int p" "int x"]);
  apply auto;
  apply (simp add: int_prime_prop);           
done;

lemma nat_int_dvd: "(int(x) dvd int(y)) = (x dvd y)";
  apply (simp only: zdvd_iff_zmod_eq_0);
  apply (simp only: dvd_eq_mod_eq_0);
  apply auto;
  apply (auto simp add: mod_eq_0_iff);
  apply (case_tac "0 <= q");                                    
  apply (rule_tac x = "nat q" in exI);
  apply (auto simp add: int_eq_iff);
  apply (auto simp add: nat_mult_distrib);
  apply (auto simp add: zmod_eq_0_iff);
  apply (rule_tac x = "int q" in exI);
  apply (auto simp add: zmult_int);                                    
done;

lemma nat_zmult_multiplicity_lemma1: 
    "(int p) ^ multiplicity (int p) (int n) dvd (int n)";
  apply (auto simp add: multiplicity_zdvd);
done;

lemma nat_zmult_multiplicity_lemma2: 
    "int (p ^ multiplicity (int p) (int n)) dvd (int n)";
  apply (auto simp add: zpow_int nat_zmult_multiplicity_lemma1);
done;

lemma nat_zmult_multiplicity: "p ^ multiplicity (int p) (int n) dvd n"; 
  apply (auto simp add: nat_int_dvd [THEN sym]);
  apply (auto simp add: nat_zmult_multiplicity_lemma2); 
done;

lemma power_dvd_prop: "p^b dvd (x::nat) ==> a <= b ==> p^a dvd x";
  apply (auto simp add: dvd_def);
  apply (rule_tac x = "k * (p ^ (b-a))" in exI);
  apply auto;
  apply (auto simp add: power_add [THEN sym]);           
done;

lemma power_le_prop1 [rule_format]: "1 <= (p::nat) ==> a <= b --> p^a <= p^b";
  apply (induct_tac b);
  apply auto;
  apply (subgoal_tac "a = Suc n");           
  apply auto;
  apply (subgoal_tac "p^n <= p*p^n");
  apply (simp only: le_trans [of "p^a" "p^n" "p*p^n"]);
  apply auto;                                                     
done;

lemma power_le_prop: "1 < p ==> p^b <= (x::nat) ==> a <= b ==> p^a <= x";
  apply (subgoal_tac "p^a <= p^b");
  apply auto;
  apply (auto simp add: power_le_prop1);           
done;

lemma nat_zmult_multiplicity_le: "0<n ==> 
    p ^ multiplicity (int p) (int n) <= n";
  apply (subgoal_tac "p^multiplicity (int p) (int n) dvd n");
  apply (simp add: dvd_imp_le);
  apply (simp add: nat_zmult_multiplicity);                             
done;

lemma multiplicity_power_dvd: "0<n ==> p:prime ==> 
    (k <= multiplicity (int p) (int n)) = (p^k dvd n)";
  apply auto;
  apply (subgoal_tac "p^multiplicity (int p) (int n) dvd n");
  apply (rule power_dvd_prop);
  apply assumption+;
  apply (simp add: nat_zmult_multiplicity);
  apply (subgoal_tac "(int p):zprime");
  apply (subgoal_tac "(int p)^k dvd (int n)");
  apply (simp add: aux9);
  apply (subgoal_tac "int p ^ k = int(p^k)");
  apply (erule ssubst);
  apply (simp only: nat_int_dvd [THEN sym]); 
  apply (simp only: zpow_int [THEN sym]);
  apply (auto simp add: int_prime_prop);
done;

lemma multiplicity_power_dvd_imp1: "0 < n ==> p : prime ==>
    p ^ k dvd n ==> k <= multiplicity (int p) (int n)";
  apply (subst multiplicity_power_dvd);
  apply assumption+;
  done;

lemma (in l) G_Int_Hp_eq: "0 < x ==> p:prime ==> 
    (%x. p^x) ` {1..nmult p x} = G Int H(p)";
  apply auto;
  apply (simp add: G_def);
  apply (simp add: nmult_def);
  apply auto;
  apply (subgoal_tac "2 <= p");           
  apply (simp);                        
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "1 < p");
  apply (subgoal_tac "p ^ multiplicity (int p) (int x) dvd x");
  apply (rule power_dvd_prop);
  apply assumption+;
  apply (simp add: nat_zmult_multiplicity);
  apply (simp add: prime_ge_2);
  apply (subgoal_tac "2 <= p");
  apply simp;
  apply (rule prime_ge_2,assumption);
  apply (unfold H_def nmult_def);
  apply clarsimp;
  apply (rule conjI);
  apply (subgoal_tac "1 < p");    
  apply (subgoal_tac "p ^ multiplicity (int p) (int x) <= x");
  apply (rule power_le_prop);
  apply assumption+;
  apply (subgoal_tac "p ^ multiplicity (int p) (int x) <= x");
  apply (subgoal_tac "1 < p");
  apply (rule power_le_prop);
  apply assumption+;
  apply force;
  apply assumption;
  apply (simp add: nat_zmult_multiplicity_le);
  apply (subgoal_tac "2 <= p");
  apply simp;            
  apply (erule prime_ge_2);
  apply (rule_tac x = "xa" in exI);
  apply simp;
  apply (unfold G_def image_def);
  apply simp;
  apply clarify;
  apply (rule_tac x = a in bexI);
  apply (rule refl);
  apply auto;
  apply (subst multiplicity_power_dvd); 
  apply auto;
  apply (subgoal_tac "0 < p ^ a");
  apply (erule order_less_le_trans);back;back;
  apply assumption;
  apply auto;
done;

lemma (in l) card_multiplicity_eq: "0 < x ==> p:prime ==> 
    card(G Int H(p)) = multiplicity (int p) (int x)";
  apply (subst G_Int_Hp_eq [THEN sym]);
  apply assumption+;
  apply (subst card_image);
  apply simp;
  apply (rule inj_on_prime_power);
  apply (simp add: nmult_def);
done;

lemma (in l) setsum_Lambda_G_int_Hp: "0 < x ==> p:prime ==> 
  setsum Lambda (G Int H(p)) = ln (real p) * 
    real (multiplicity (int p) (int x))";
proof -;
  assume "0 < x" and "p:prime";
  have "ALL x:(G Int H(p)). Lambda x = ln (real p)"; 
    by (auto simp add: G_def H_def prems Lambda_eq);
  then have "setsum Lambda (G Int H(p)) = 
      setsum (%x. ln (real p)) (G Int H(p))";
    apply (intro setsum_cong);
    apply (rule refl);
    apply (erule bspec);
    apply assumption;
    done;
  also have "… = real(card (G Int H(p))) * ln (real p)";
    apply (subst setsum_constant);
    apply (rule finite_subset);
    prefer 2;
    apply (rule finite_G);
    apply (rule prems);
    apply force;
    apply (simp add: real_eq_of_nat);
    done;
  also have "card (G ∩ H p) = multiplicity (int p) (int x)"
    by (rule card_multiplicity_eq);
  finally show ?thesis;
    by simp;
qed;

lemma (in l) setsum_Lambda_G_lemma2: "0 < x ==> setsum Lambda G = 
    setsum (%p. ln (real p) * real (multiplicity (int p) (int x))) J";
  apply (subst setsum_Lambda_G_lemma1);
  apply assumption;
  apply (rule setsum_cong);
  apply (rule refl);
  apply (subgoal_tac "H xa Int G = G Int H xa");
  apply (erule ssubst);
  apply (erule setsum_Lambda_G_int_Hp);
  apply (simp add: J_def);
  apply auto;
done;

lemma multiplicity_eq_4: "0 < n ==> ln(real n) = 
    setsum (%p. real(multiplicity p n) * ln(real p)) {p. 0 < p & p : zprime &
      p dvd n}";
  apply (subgoal_tac "n = 1 | 1 < n");
  apply (erule disjE);
  apply (simp add: multiplicity_p_1_eq_0 setsum_0);
  apply (elim multiplicity_eq_3);
  apply force;
done;

lemma multiplicity_eq_5: "0 < n ==> ln(real n) = 
    setsum (%p. real(multiplicity (int p) (int n)) * ln(real p)) 
      {p. 0 < p & p : prime & p dvd n}";
  apply (subgoal_tac "real n = real (int n)");
  apply (erule ssubst);
  apply (subst multiplicity_eq_4);
  apply force;
  apply (rule setsum_reindex_cong);
  apply (rule finite_subset_AtMost_nat);
  apply clarify;
  apply (erule dvd_imp_le);
  apply assumption;
  apply (subgoal_tac "inj_on int {p. 0 < p ∧ p ∈ prime ∧ p dvd n}");
  apply assumption;
  apply (force simp add: inj_on_def);
  apply (unfold image_def);
  apply auto;
  apply (rule_tac x = "nat x" in exI);
  apply (auto simp add: nat_prime_prop);
  apply (subgoal_tac "nat x dvd nat (int n)");
  apply simp;
  apply (rule nat_int_dvd_prop);
  apply assumption;
  apply assumption;
  apply (simp add: int_nat_dvd_prop);
  apply (rule ext);
  apply (unfold o_def);
  apply (subgoal_tac "real p = real (int p)");
  apply (erule subst);
  apply (rule refl);
  apply simp;
done;

lemma ln_eq_setsum_Lambda: "0 < (n::nat) ==> ln (real n) = 
    setsum Lambda {d. d dvd n}";
  apply (subgoal_tac "{d. d dvd n} = {d. 0 < d & d dvd n}");
  apply (erule ssubst);
  apply (subst l.setsum_Lambda_G_lemma2);
  apply assumption;
  apply (subst multiplicity_eq_5);
  apply assumption;
  apply (rule setsum_cong);
  apply auto;
  apply (rule prime_pos);
  apply assumption;
  apply (erule dvd_pos_pos);
  apply assumption;
done;

lemma ln_eq_setsum_Lambda2: "0 < n ==> ln (real n) = 
    (∑x:{(p, a). 0 < a & p : prime & p ^ a dvd n}. 
      ln (real (fst x)))";
proof -; 
  assume "0 < (n::nat)";
  have "ln (real n) = (∑d:{d. d dvd n}. Lambda d)";
    by (rule ln_eq_setsum_Lambda);
  also have "... = 
    (∑d:{d. d dvd n & (EX p a. 0 < a & p : prime & d = p ^ a)}. 
      Lambda d) + 
    (∑d:{d. d dvd n & ~(EX p a. 0 < a & p : prime & d = p ^ a)}.
      Lambda d)" (is "... = ?term1 + ?term2");
    apply (subst setsum_Un_disjoint [THEN sym]);
    apply (rule finite_subset);
    prefer 2;
    apply (rule finite_nat_dvd_set);
    apply (rule prems);
    apply force;
    apply (rule finite_subset);
    prefer 2;
    apply (rule finite_nat_dvd_set);
    apply (rule prems);
    apply force;
    apply blast;
    apply (rule setsum_cong);
    apply blast;
    apply force;
    done;
  also have "?term2 = 0";
    apply (rule setsum_0');
    apply (rule ballI);
    apply (rule Lambda_eq2);
    apply auto;
    done;
  also have "?term1 + 0 = ?term1";
    by simp;
  also have "... = (∑x:{(p,a). 0 < a & p : prime & p^a dvd n}.
    Lambda((%x. (fst x)^(snd x))x))";
    apply (subst setsum_reindex' [THEN sym]);back;
    apply (rule finite_subset);
    prefer 2;
    apply (rule l.finite_C [of n]);
    apply auto;
    apply (erule dvd_imp_le);
    apply (rule prems);
    apply (rule subset_inj_on);
    prefer 2;
    apply (rule l.inj_on_C);
    apply auto;
    apply (erule dvd_imp_le);
    apply (rule prems);
    apply (rule setsum_cong);
    apply (auto simp add: image_def);
    done;
  finally show ?thesis;
    apply (elim ssubst);
    apply (rule setsum_cong2);
    apply (rule Lambda_eq);
    apply auto;
    done;
qed;


end;