Theory RealLib

(*  Title:      RealLib.thy
    Authors:    Jeremy Avigad and Kevin Donnelly
*)

header {* Facts about the real numbers *}

theory RealLib = Complex + RingLib + FiniteLib + SetsAndFunctions:
-- {* Clean this up! *}
-- {* Eliminate duplicates *}
-- {* Generalize theorems about reals to rings *}

subsection {* Casting to reals *}

lemma real_eq_of_nat: "real = of_nat";
  apply (rule ext);
  apply (unfold real_of_nat_def);
  apply (rule refl);
  done;

lemma real_eq_of_int: "real = of_int";
  apply (rule ext);
  apply (unfold real_of_int_def);
  apply (rule refl);
  done;

lemma real_nat_zero [simp]: "real (0::nat) = 0";
  by (simp add: real_of_nat_def);

lemma real_nat_one [simp]: "real (1::nat) = 1";
  by simp;

lemma le_imp_real_of_nat_le: "(x::nat) <= y ==> 
    real x <= real y";
  by auto;

lemma divide_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
    real (x div d) + (real (x mod d)) / (real d)";
proof -;
  assume "0 < d";
  have "x = (x div d) * d + x mod d";
    by auto;
  then have "real x = real (x div d) * real d + real(x mod d)";
    by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym]);
  then have "real x / real d = … / real d";
    by simp;
  then show ?thesis;
    by (auto simp add: add_divide_distrib ring_eq_simps prems);
qed;

lemma nat_dvd_real_div: "0 < (d::nat) ==> d dvd n ==>
    real(n div d) = real n / real d";
  apply (frule divide_div_aux [of d n]);
  apply simp;
  apply (subst dvd_eq_mod_eq_0 [THEN sym]);
  apply assumption;
done;

subsection {* Misc theorems about limits and infinite sums *}

lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
  apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
  apply (subgoal_tac "(%n. b) ----> b")
  by (auto simp add: LIMSEQ_diff LIMSEQ_const)

lemma LIMSEQ_ignore_initial_segment: "f ----> a 
  ==> (%n. f(n + k)) ----> a"
  apply (unfold LIMSEQ_def) 
  apply (clarify)
  apply (drule_tac x = r in spec)
  apply (clarify)
  apply (rule_tac x = "no + k" in exI)
  by auto

lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
    f ----> a";
  apply (unfold LIMSEQ_def);
  apply clarsimp;
  apply (drule_tac x = r in spec);
  apply clarsimp;
  apply (rule_tac x = "no + k" in exI);
  apply clarsimp;
  apply (drule_tac x = "n - k" in spec);
  apply (frule mp);
  apply arith;
  apply simp;
done;

lemma LIMSEQ_diff_approach_zero: 
  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
     f ----> L";
  apply (drule LIMSEQ_add);
  apply assumption;
  apply simp;
done;

lemma LIMSEQ_diff_approach_zero2: 
  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
     g ----> L";
  apply (drule LIMSEQ_diff);
  apply assumption;
  apply simp;
done;

lemma sums_split_initial_segment: "f sums s ==> 
  (%n. f(n + k)) sums (s - sumr 0 k f)"
  apply (unfold sums_def)
  apply (simp add: sumr_offset) 
  apply (rule LIMSEQ_diff_const)
  apply (rule LIMSEQ_ignore_initial_segment)
  by assumption

lemma summable_ignore_initial_segment: "summable f ==> 
    summable (%n. f(n + k))"
  apply (unfold summable_def)
  by (auto intro: sums_split_initial_segment)

lemma suminf_minus_initial_segment: "summable f ==>
    suminf f = s ==> suminf (%n. f(n + k)) = s - sumr 0 k f"
  apply (frule summable_ignore_initial_segment)
  apply (rule sums_unique [THEN sym])
  apply (frule summable_sums)
  apply (rule sums_split_initial_segment)
  by auto

lemma suminf_split_initial_segment: "summable f ==> 
    suminf f = sumr 0 k f + suminf (%n. f(n + k))"
  by (auto simp add: suminf_minus_initial_segment)

lemma sums_const_times: "f sums a ==> (%x. c * f x) sums (c * a)";
  apply (unfold sums_def);
  apply (subgoal_tac "(λn. sumr 0 n (λx. c * f x)) = (%n. c * sumr 0 n f)");
  apply (erule ssubst);
  apply (rule LIMSEQ_mult);
  apply (rule LIMSEQ_const);
  apply assumption;
  apply (rule ext);
  apply (rule sumr_mult [THEN sym]);
done;

lemma summable_const_times: "summable f ==> summable (%x. c * f x)";
  apply (unfold summable_def);
  apply (auto intro: sums_const_times);
done;

lemma suminf_const_times: "summable f ==> suminf (%x. c * f x) = c * suminf f";
  apply (rule sym);
  apply (rule sums_unique);
  apply (rule sums_const_times);
  apply (erule summable_sums);
done;

subsection {* Facts about sumr, setsum, and setprod *}

lemma sumr_cong [rule_format]: "(ALL y. (y < x --> f y = g y)) -->
  sumr 0 x f = sumr 0 x g";
  by (induct x, simp_all);

lemma sumr_cong [rule_format]: "(ALL y. (y < x --> f y = g y)) -->
  sumr 0 x f = sumr 0 x g";
by (induct x, simp_all);

lemma sumr_le_cong [rule_format]: "(ALL y. (y < x --> f y <= g y)) -->
  sumr 0 x f <= sumr 0 x g";
apply (induct x);
apply simp;
apply auto;
apply (erule add_mono);
apply auto;
done;

lemma sumr_ge_zero_cong [rule_format]: "(ALL y. (y < x --> 0 <= g y)) 
    --> 0 <= sumr 0 x g";
  apply (subgoal_tac "sumr 0 x (%x. 0) = 0");
  apply (erule subst);
  apply (clarify);
  apply (rule sumr_le_cong);
  apply auto;
done;

lemma sumr_split_add_le: "n <= p ==> sumr 0 n f + sumr n p f = sumr 0 p f";
apply(case_tac "n < p");
apply(simp only: sumr_split_add);
apply(subgoal_tac "n = p");
by(auto);

lemma setsum_sumr: "setsum f {0..x::nat(} = sumr 0 x f";
  apply (induct_tac x);                                                  
  apply (auto);
  apply (simp add: atLeastLessThan_def); 
  apply (simp add: atLeastLessThan_def);
  apply (simp add: lessThan_Suc);
done;

lemma setsum_sumr2: "setsum f {0..x} = sumr 0 (x+1) f";
  apply (subgoal_tac "{0..x} = {0..x+1(}");
  apply (erule ssubst);
  apply (rule setsum_sumr);
  apply auto;
done;

lemma setsum_sumr3: "setsum f {)0..x} = sumr 0 x (%n. f(n + 1))";
  apply (subgoal_tac "setsum f {)0..x} = setsum (%n. f(n+1)) {0..x(}");
  apply (erule ssubst);
  apply (rule setsum_sumr);
  apply (rule setsum_reindex_cong');
  prefer 4;
  apply simp;
  apply simp;
  apply (simp add: inj_on_def);
  apply (auto simp add: image_def);
  apply (rule_tac x = "xa - 1" in bexI);
  apply auto;
  apply arith;
done;

lemma setsum_sumr4: "(∑i=1..n. f i) = sumr 0 n (%i. f(i + 1))";
  apply (subst setsum_sumr3 [THEN sym]);
  apply (rule setsum_cong);
  apply auto;
done;

lemma setsum_sumr5_aux: "(∑i=a..a+c. f i) = sumr a (a+c+1) f";
  apply (induct_tac c);
  apply simp;
  apply simp;
  apply (subgoal_tac "{a..Suc(a+n)} = {a..a+n} Un {Suc(a+n)}");
  apply (erule ssubst);back;
  apply (subst setsum_Un_disjoint);
  apply auto;
done;
  
lemma setsum_sumr5: "(∑i=a..b. f i) = sumr a (b+1) f";
  apply (case_tac "b < a");
  apply (subgoal_tac "{a..b} = {}");
  apply simp;
  apply simp;
  apply (subgoal_tac "b = a + (b - a)");
  apply (erule ssubst);
  apply (rule setsum_sumr5_aux);
  apply arith;
done;

lemma setsum_singleton: "setsum f {n} =  f n";
  apply auto;
done;

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

lemma real_of_nat_setsum: "real (setsum (f::'a => nat) A) = 
    setsum (real o f) A";
  apply (subst real_eq_of_nat);
  apply (rule setsum_of_nat);
done;

lemma real_card_eq_setsum: "finite A ==> real (card A) = setsum (%x.1) A";
  apply (subst card_eq_setsum);
  apply assumption;
  apply (subst real_of_nat_setsum); 
  apply (unfold o_def);
  apply simp;
done;

lemma setprod_real_of_int: "real (setprod (f::'a => int) A) = 
    setprod (%x. real(f x)) A";
  apply (subst real_eq_of_int);
  apply (simp add: setprod_of_int o_def);
  done;

lemma sumr_shift: "sumr 0 n (%n. f(m + n)) = sumr m (m + n) f";
  by (induct_tac n, simp_all);

lemma sumr_zero_to_two: "sumr 0 2 f = f 0 + f 1"
proof -
  have "2 = Suc (Suc 0)"
    by simp
  hence "sumr 0 2 f = sumr 0 (Suc (Suc 0)) f"
    by (rule subst, simp)
  thus ?thesis
    by simp
qed

lemma sums_zero: "(%x. 0) sums 0";
  apply (unfold sums_def);
  apply simp;
  apply (rule LIMSEQ_const);
done;

lemma suminf_zero: "suminf (%x. 0) = 0";
  apply (rule sym);
  apply (rule sums_unique);
  apply (rule sums_zero);
done;
  
lemma summable_zero: "summable (%x. 0)";
  apply (rule sums_summable);
  apply (rule sums_zero);
done;

lemma sums_neg: "f sums s ==> (- f) sums (- s)";
  by (simp add: sums_def func_minus sumr_minus LIMSEQ_minus);

lemma summable_neg: "summable f ==> summable (- f)";
  by (auto simp add: summable_def intro: sums_neg);

lemma summable_neg2: "summable f ==> summable (%x. - f x)";
  by (frule summable_neg, unfold func_minus);

lemma suminf_neg: "summable f ==> suminf (- f) = - (suminf f)";
  apply (rule sym);
  apply (rule sums_unique);
  apply (rule sums_neg);
  apply (erule summable_sums);
done;

subsection {* Help for calculations with reals (a mess!) *}

lemma realpow_two2: "(x::real) * x = x^2"
proof -
  have "(x::real) * x = x^(Suc (Suc 0))"
    by (rule realpow_two [THEN sym])
  also have "... = x^2"
  proof -
    have "Suc (Suc 0) = 2" by simp
    thus ?thesis by (rule ssubst, simp)
  qed
  finally show ?thesis .
qed

lemma real_mult_le_one_le: assumes "0 <= (x::real)" and "0 <= y" and "y <= 1"
    shows "x * y <= x"
proof -
  from prems have "x * y <= x * 1"
    by (intro mult_left_mono);
  thus ?thesis by auto
qed

lemma real_le_one_mult_le: assumes "0 <= (x::real)" and "0 <= y" and "y <= 1"
    shows "y * x <= x"
proof -
  from prems have "y * x <= 1 * x"
    by (intro mult_right_mono);
  thus ?thesis by auto
qed

lemma real_mult_less_one_less: 
    "(0::real) < x ==> x < 1 ==> 0 < y ==> y * x < y"
proof -
  assume "(0::real) < x" and "x < 1" and "0 < y"
  have "y * x < y * 1"
    by (auto simp only: real_mult_less_mono2 prems)
  thus ?thesis 
    by simp
qed

lemma real_less_one_mult_less: 
    "(0::real) < x ==> x < 1 ==> 0 < y ==> x * y < y"
proof -
  assume "(0::real) < x" and "x < 1" and "0 < y"
  have "x * y < 1 * y"
    by (auto simp only: mult_strict_right_mono prems)
  thus ?thesis 
    by simp
qed

lemma real_inverse_le_swap: "0 < (r::real) ==> r <= x ==> 
    inverse x <= inverse r"
proof -
  assume "0 < (r::real)"
  assume "r <= x"
  then have "r < x | r = x"
    by auto
  with prems show "inverse x <= inverse r"
  proof (elim disjE)
    assume "0 < r" and "r < x"
    then have "inverse x < inverse r"
      by (intro less_imp_inverse_less);
    then show ?thesis by auto
  next assume "r = x"
     thus "inverse x <= inverse r" by auto
  qed
qed

lemma real_inverse_nat_le_one: "1 <= (n::nat) ==> inverse (real n) <= 1"
proof -
  assume "1 <= (n::nat)"
  then have "real (1::nat) <= real n"
    by (auto simp only: real_of_nat_le_iff)
  then have "1 <= real n" by simp
  then have "inverse (real n) <= inverse 1"
    by (simp only: real_inverse_le_swap)
  thus ?thesis by auto
qed

lemma real_le_mult_imp_div_pos_le: assumes a: "0 < y" and 
    b: "(x::real) <= y * z" shows "x / y <= z"
proof -
  from b have "x <= y * z" .
  also from a have "x = y * (x / y)"
    by auto
  finally have "y * (x / y) <= y * z" .
  with a show ?thesis
    by (simp only: real_mult_le_cancel_iff2)
qed

lemma real_mult_le_imp_le_div_pos: assumes a: "0 < y" and 
    b: "(x::real) * y <= z" shows "x <= z / y"
proof -
  from b a have "x * y  <= (z / y) * y" by auto
  with a show ?thesis
    by (simp only: real_mult_le_cancel_iff1)
qed

lemma real_le_mult_imp_le_div_pos2: assumes a: "0 < y" and 
    b: "y * (x::real) <= z" shows "x <= z / y"
proof -
  from b a have "y * x  <= y * (z / y)" by auto
  with a show ?thesis
    by (simp only: real_mult_le_cancel_iff2)
qed

lemma real_mult_less_imp_less_div_pos: assumes a: "0 < y" and 
    b: "(x::real) * y < z" shows "x < z / y"
proof -
  from b a have c: "x * y < (z / y) * y"
    by simp
  show ?thesis;
    apply (rule  mult_right_less_imp_less);
    apply (rule c);
    apply (rule order_less_imp_le, rule a);
    done;
qed

lemma real_div_pos_le_mono: "(x::real) <= y ==> 0 < z ==> x / z <= y / z"
  by (unfold real_divide_def, auto)

lemma real_div_neg_le_anti_mono: "(x::real) <= y ==> z < 0 ==> 
    y / z <= x / z"
  by (simp add: neg_divide_le_eq);

lemma real_div_pos_less_mono: "(x::real) < y ==> 0 < z ==> x / z < y / z"
  by (auto simp add: real_divide_def)

lemma real_pos_div_less_anti_mono: "0 < (x::real) ==> x < y ==> 0 < z
    ==> z / y < z / x"
  apply (unfold real_divide_def);
  apply (rule real_mult_inverse_cancel2)
  apply auto;
  done;

lemma real_pos_div_le_mono: "0 < (x::real) ==> x <= y ==> 0 <= z
    ==> z / y <= z / x"
  apply (unfold real_divide_def)
  apply (rule mult_left_mono);
  apply (rule le_imp_inverse_le);
  by (assumption+)

lemma real_one_div_le_anti_mono: "0 < (x::real) ==> x <= y ==>
    1 / y <= 1 / x"
  by (rule real_pos_div_le_mono [of x y 1], auto)

lemma real_ge_zero_plus_gt_zero_is_gt_zero: "(0::real) <= x ==> 
    0 < y ==> 0 < x + y"
proof -
  assume a: "(0::real) <= x" and b: "(0::real) < y"
  have "(0::real) = 0 + 0" by simp
  also from a b have "... < x + y"
    by (rule real_add_le_less_mono)
  finally show ?thesis .
qed

lemma real_gt_zero_plus_ge_zero_is_gt_zero: "(0::real) < x ==> 
    0 <= y ==> 0 < x + y"
proof -
  assume a: "(0::real) < x" and b: "(0::real) <= y"
  have "(0::real) = 0 + 0" by simp
  also from a b have "... < x + y"
    by (rule real_add_less_le_mono)
  finally show ?thesis .
qed

lemma real_ge_zero_div_gt_zero [simp]: "(0::real) <= x ==> 0 < y ==> 
    0 <= x/y"
  by (rule real_mult_le_imp_le_div_pos, auto)

lemma real_div_mult_simp: "(z::real) ~= 0 
    ==> (x / z = y) = (x = z * y)"
  by auto

lemma real_div_mult_simp2: "(z::real) ~= 0 
    ==> (y = x / z) = (x = z * y)"
  by auto

lemma real_minus_divide_distrib: "((x::real) - y) / z = x / z - y / z"
proof -
  have "x - y = x + -y"
    by auto
  then have "(x - y) / z = (x + -y) / z"
    by (rule ssubst, simp)
  also have "... = x / z + (-y) / z"
    by (rule add_divide_distrib)
  also have "... = x / z - y / z"
    by simp
  finally show ?thesis .
qed

lemma real_mult_div_cancel2: "(k::real) ~= 0 ==> (m * k) / (n * k) = m / n"
proof -
  assume "k ~= 0"
  have "m * k = k * m" by auto
  moreover have "n * k = k * n" by auto
  ultimately have "(m * k) / (n * k) = (k * m) / (k * n)" 
    by (auto simp only:)
  also have "... = m / n"
    by (rule mult_divide_cancel_left);
  finally show ?thesis .
qed

lemma unused1: "((x::real) / y) / z = (x / z) / y"
  by auto

lemma unused2: "0 < x ==> ((x::real) / y) / x = 1 / y"
  by auto
  
lemma real_neg_squared_eq_pos_squared: "(- (x::real))^2 = x^2"
  by (auto simp add: realpow_two2 [THEN sym])

lemma real_x_times_x_squared: "(x::real) * x^2 = x^3"
proof -
  have "3 = Suc 2" by auto
  hence "x^3 = x^(Suc 2)" by simp
  also have "... = x * x^2" by (rule realpow_Suc)
  finally show ?thesis by simp
qed

lemma real_one_over_pow: "(x::real) ~= 0 ==> 1 / x^n = (1 / x)^n";
apply (simp add: real_divide_def);
by (rule power_inverse);

lemma real_nat_ge_zero [simp]: "0 ≤ real (n::nat)";
by auto;

lemma real_nat_plus_one_gt_zero [simp]: "0 < real (n::nat) + 1";
apply (rule real_ge_zero_plus_gt_zero_is_gt_zero);
by auto;

lemma real_one_over_nat_plus_one_gt_zero [simp]: "0 < 1 / (real (n::nat) + 1)";
apply (rule real_mult_less_imp_less_div_pos);
apply (rule real_nat_plus_one_gt_zero);
by simp;

lemma real_one_over_nat_plus_one_ge_zero [simp]: 
  "0 ≤ 1 / (real (n::nat) + 1)";
apply (rule order_less_imp_le);
by (rule real_one_over_nat_plus_one_gt_zero);

lemma real_nat_plus_one: "real ((n::nat) + 1) = real n + 1";
by (auto intro: real_of_nat_Suc);

lemma real_frac_add: "[|b ~= 0;d ~= 0|] ==> a/b + c/(d::real) = ((a*d + c*b) / (d*b))";
by(auto simp add: add_divide_distrib); 

lemma div_ge_1: "[|0 < a;a <= (b::real)|] ==> 1 <= b / a";
apply(auto simp add: real_divide_def);
apply(rotate_tac 1);
apply(rule order_trans[of 1 "a * inverse a"]);
apply(simp add: Ring_and_Field.right_inverse);
apply (rule mult_right_mono);
apply auto;
done;

lemma real_one_over_pos: "0 < (x::real) ==> 0 < 1 / x"; 
  by (rule real_mult_less_imp_less_div_pos, auto);

lemma real_fraction_le: "0 < (w::real) ==> 0 < z ==> x * w <= y * z ==> 
    x / z <= y / w";  
  apply (rule real_le_mult_imp_div_pos_le);
  apply assumption;
  apply simp;
  apply (rule real_mult_le_imp_le_div_pos);
  apply assumption;
  apply (simp add: mult_commute);
done;

lemma real_fraction_le2: "0 <= x ==> (x::real) <= y ==> 0 < w ==> w <= z  ==>
    x / z <= y / w";
  apply (rule real_fraction_le);
  apply auto;
  apply (rule mult_mono);
  apply auto;
done;

subsection {* Casting quotients to real *}

theorem nat_div_real_div[rule_format]: 
    "0 <= real (n::nat) / real (x) - real (n div x) &
      real (n) / real (x) - real (n div x) <= 1";
  apply(auto);
  apply(case_tac "x = 0");
  apply(force simp add: DIVISION_BY_ZERO_DIV real_divide_def INVERSE_ZERO);
  apply(rule real_mult_le_imp_le_div_pos);
  apply force;
  apply simp;
  apply (subst real_of_nat_mult [THEN sym]);
  apply (subst real_of_nat_le_iff);
  apply (subst mult_commute);
  apply (subst mult_div_cancel);
  apply force;
  apply(case_tac "x = 0");
  apply simp;
  apply (simp add: compare_rls);
  apply (rule real_le_mult_imp_div_pos_le);
  apply force;
  apply (simp add: ring_distrib);
  apply (subst real_of_nat_mult [THEN sym]);
  apply (subst real_of_nat_add [THEN sym]);
  apply (subst real_of_nat_le_iff);
  apply (subst mult_div_cancel);
  apply (subgoal_tac "n mod x <= x");
  apply arith;
  apply (rule order_less_imp_le);
  apply (erule mod_less_divisor);
done;

theorems nat_div_real_div1 = nat_div_real_div [THEN conjunct1];
theorems nat_div_real_div2 = nat_div_real_div [THEN conjunct2];

lemma real_nat_div_le_real_div: "real (n div x) <= real (n::nat) / real x"; 
  apply (insert nat_div_real_div1 [of n x]);
  apply simp;
done;

subsection {* Floor and ceiling *}

lemma floor_bound: "real(x::nat) <= k ==> x <= nat(floor(k))";
  apply (drule floor_le2);
  apply (simp only: floor_real_of_nat);
  apply (subgoal_tac "nat (int x) <= nat (floor k)");
  apply (simp add: nat_int);
  apply (case_tac "x = 0");
  apply (subgoal_tac "0 <= k");
  apply (simp add: nat_le_eq_zle);
  apply (subgoal_tac "int x = 0");
  apply (simp add: real_of_int_le_iff [THEN sym]);
  apply (auto simp add: real_of_int_floor_le);
  apply (subgoal_tac "real(floor k) <= k");
  apply (erule order_trans);
  apply simp;
  apply (simp add: real_of_int_floor_le);
  apply (subgoal_tac "nat(int x) <= nat(floor k)");
  apply (simp add: nat_int);
  apply (subgoal_tac "0 < int x | 0 <= floor k");
  apply (frule nat_le_eq_zle [THEN sym]);
  apply force;
  apply force;
done;

lemma real_int_nat1: "real(int(nat(x))) = real(nat(x))";
  apply (simp only: real_of_int_real_of_nat);
done;

lemma real_int_nat: "0 <= x ==> real(x) = real(nat(x))"
  apply (subgoal_tac "real(int(nat(x))) = real(nat(x))");
  apply force;
  apply (rule real_int_nat1);
done;

lemma real_nat_floor: "0 <= x ==> real(nat(floor(x))) <= x";
  apply (subgoal_tac "0 <= floor(x)");
  apply (subgoal_tac "real(nat(floor(x))) = real(floor(x))");
  apply (erule ssubst);
  apply (auto simp add: real_of_int_floor_le);
  apply (simp add: real_int_nat);
  apply (subgoal_tac "floor 0 <= floor x");
  apply (simp add: floor_zero);
  apply (rule floor_le2);
  by simp;

lemma real_upper_bound: "0 < r ==> r <= real(nat(ceiling(r)))"; 
  apply (subgoal_tac "real(nat(ceiling(r))) = real(ceiling(r))");
  apply simp;
  apply (subgoal_tac "real(ceiling(r)) = real(int(nat(ceiling(r))))");
  apply (erule ssubst);
  apply (subst real_of_int_real_of_nat);
  apply (rule refl);
  apply simp;
  apply (insert real_of_int_ceiling_ge [of r]);
  apply (subgoal_tac "0 <= real(ceiling(r))");
  apply simp;
  apply (subgoal_tac "0 < real(ceiling(r))");
  apply force;
  apply (erule order_less_le_trans);
  apply assumption;
done;

constdefs
  natfloor :: "real => nat"
  "natfloor x  ==  nat(floor x)";

lemma real_of_nat_eq_real_of_int: "0 <= x ==> real(nat x) = real x";
  apply (subgoal_tac "real x = real(int(nat(x)))");
  apply (erule ssubst);
  apply (rule real_of_int_real_of_nat [THEN sym]);
  apply simp;
  done;

lemma floor_ge_zero_ge_zero: "0 <= x ==> 0 <= floor(x)";
  apply (subgoal_tac "0 = floor(0)"); 
  apply (erule ssubst);
  apply (erule floor_le2);
  apply simp;
done;

lemma real_natfloor_le: "0 <= x ==> real(natfloor(x)) <= x";
  apply (unfold natfloor_def);
  apply (subst real_of_nat_eq_real_of_int);
  apply (erule floor_ge_zero_ge_zero);
  apply simp;
done;
  
lemma real_natfloor_plus_one_ge: "x <= real(natfloor x) + 1";
  apply (case_tac "0 <= x");
  apply (unfold natfloor_def);
  apply (subst real_of_nat_eq_real_of_int);
  apply (erule floor_ge_zero_ge_zero);
  apply (rule real_of_int_floor_add_one_ge);
  apply simp;
done;

lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
apply (simp add: floor_def Least_def)
apply (insert real_lb_ub_int [of r], safe)
apply (rule theI2)
apply (auto intro: lemma_floor)
done

lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
apply (insert real_of_int_floor_gt_diff_one [of r])
apply (auto simp del: real_of_int_floor_gt_diff_one)
done;

lemma real_of_nat_floor_add_one_gt [simp]: "r < real (natfloor r) + 1";
apply (unfold natfloor_def);
apply (case_tac "0 <= r");
apply (subst real_of_nat_eq_real_of_int);
apply (erule floor_ge_zero_ge_zero);
apply simp;
apply simp;
done;

lemma floor_add [simp]: "floor (x + real a) = floor x + a";
  apply (subgoal_tac "floor(x + real a) <= floor x + a");
  apply (subgoal_tac "floor x + a <= floor(x + real a)");
  apply force;
  apply (subgoal_tac "floor x + a < floor (x + real a) + 1");
  apply arith;
  apply (subst real_of_int_less_iff [THEN sym]);
  apply simp;
  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1");
  apply (subgoal_tac "real (floor x) <= x");
  apply arith;
  apply (rule real_of_int_floor_le);
  apply (rule real_of_int_floor_add_one_gt);
  apply (subgoal_tac "floor (x + real a) < floor x + a + 1");
  apply arith;
  apply (subst real_of_int_less_iff [THEN sym]);  
  apply simp;
  apply (subgoal_tac "real(floor(x + real a)) <= x + real a"); 
  apply (subgoal_tac "x < real(floor x) + 1");
  apply arith;
  apply (rule real_of_int_floor_add_one_gt);
  apply (rule real_of_int_floor_le);
done;

lemma floor_subtract [simp]: "floor (x - real a) = floor x - a";
  apply (subst diff_minus)+;
  apply (subst real_of_int_minus);
  apply (rule floor_add);
done;

lemma real_le_floor [intro]: "real a <= x ==> a <= floor x";
  apply (subgoal_tac "a < floor x + 1");
  apply arith;
  apply (subst real_of_int_less_iff [THEN sym]);
  apply simp;
  apply (insert real_of_int_floor_add_one_gt [of x]); 
  apply arith;
done;

lemma real_le_natfloor [intro]: "real a <= x ==> a <= natfloor x";
  apply (unfold natfloor_def);
  apply (subgoal_tac "nat (int a) <= nat (floor x)");
  apply simp;
  apply (subst nat_le_eq_zle);
  apply (subgoal_tac "int 0 <= floor x");
  apply force;
  apply (rule real_le_floor);
  apply force;
  apply (rule real_le_floor);
  apply simp;
done;

lemma natfloor_add [simp]: "0 <= x ==> natfloor(x + real a) = natfloor x + a";
  apply (unfold natfloor_def);
  apply (subgoal_tac "real a = real (int a)");
  apply (erule ssubst);
  apply (subst floor_add); 
  apply (subst nat_add_distrib);
  apply auto;
done;

lemma natfloor_subtract [simp]: "real a <= x ==> 
    natfloor(x - real a) = natfloor x - a";
  apply (unfold natfloor_def);
  apply (subgoal_tac "real a = real (int a)");
  apply (erule ssubst);
  apply (subst floor_subtract);
  apply (subst nat_diff_distrib);
  apply auto;
done;  

lemma natfloor_ge_zero_lt_one: "0 <= x ==> x < 1 ==> natfloor x = 0";
  apply (subgoal_tac "0 <= natfloor x"); 
  apply (subgoal_tac "natfloor x < 1");
  apply arith;
  apply (unfold natfloor_def);
  apply simp;
  apply (rule floor_eq4);
  apply auto;
done;

lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 
  natfloor (x / real y) = natfloor x div y";
proof -;
  assume "1 <= (x::real)" and "0 < (y::nat)";
  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y";
    by simp;
  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + 
    real((natfloor x) mod y)";
    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]);
  have "x = real(natfloor x) + (x - real(natfloor x))";
    by simp;
  then have "x = real ((natfloor x) div y) * real y + 
      real((natfloor x) mod y) + (x - real(natfloor x))";
    by (simp add: a);
  then have "x / real y = ... / real y";
    by simp;
  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
    real y + (x - real(natfloor x)) / real y";
    by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib
      diff_divide_distrib prems);
  finally have "natfloor (x / real y) = natfloor(...)"; by simp;
  also have "... = natfloor(real((natfloor x) mod y) / 
    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))";
    by (simp add: add_ac);
  also have "... = natfloor(real((natfloor x) mod y) / 
    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y";
    apply (rule natfloor_add);
    apply (rule nonneg_plus_nonneg);
    apply (rule real_ge_zero_div_gt_zero);
    apply force;
    apply (simp add: prems);
    apply (rule real_ge_zero_div_gt_zero);
    apply simp;
    apply (rule real_natfloor_le);
    apply (auto simp add: prems);
    apply (insert prems, arith);
    done;
  also have "natfloor(real((natfloor x) mod y) / 
    real y + (x - real(natfloor x)) / real y) = 0";
    apply (rule natfloor_ge_zero_lt_one);
    apply (rule nonneg_plus_nonneg);
    apply (rule real_ge_zero_div_gt_zero);
    apply force;
    apply (force simp add: prems);
    apply (rule real_ge_zero_div_gt_zero);
    apply simp;
    apply (rule real_natfloor_le);
    apply (auto simp add: prems);
    apply (insert prems, arith);
    apply (simp add: add_divide_distrib [THEN sym]);
    apply (subst pos_divide_less_eq);
    apply (force simp add: prems);
    apply simp;
    apply (subgoal_tac "real y = real y - 1 + 1");
    apply (erule ssubst);
    apply (rule add_le_less_mono);
    apply (simp add: compare_rls);
    apply (subgoal_tac "real(natfloor x mod y) + 1 = 
      real(natfloor x mod y + 1)");
    apply (erule ssubst);
    apply (subst real_of_nat_le_iff);
    apply (subgoal_tac "natfloor x mod y < y");
    apply arith;
    apply (rule mod_less_divisor);
    apply assumption;
    apply auto;
    apply (simp add: compare_rls);
    apply (subst add_commute);
    apply (rule real_of_nat_floor_add_one_gt);
    done;
  finally show ?thesis;
    by simp;
qed;

lemma nat_le_natfloor: "0 <= x ==> y <= natfloor x ==> real y <= x";
  apply (rule order_trans); 
  apply (subgoal_tac "real y <= real (natfloor x)");
  apply assumption;
  apply force;
  apply (rule real_natfloor_le);
  apply assumption;
done;

lemma natfloor_real_id [simp]: "natfloor (real n) = n";
  by (unfold natfloor_def, simp);

lemma natfloor_neg: "x <= 0 ==> natfloor x = 0";
  apply (unfold natfloor_def);
  apply (subgoal_tac "floor x <= 0");
  apply simp;
  apply (subgoal_tac "floor x < 1");
  apply arith;
  apply (subgoal_tac "real (floor x) < real 1");
  apply force;
  apply (rule order_le_less_trans);
  apply (rule real_of_int_floor_le);
  apply simp;
done;

lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n";
  apply (subgoal_tac "z < real(natfloor z) + 1");
  apply arith;
  apply (rule real_of_nat_floor_add_one_gt);
done;

lemma natfloor_zero [simp]: "natfloor 0 = 0";
  apply (subgoal_tac "0 = real (0::nat)");
  apply (erule ssubst);
  apply (rule natfloor_real_id);
  apply simp;
done;

lemma natfloor_one [simp]: "natfloor 1 = 1";
  apply (subgoal_tac "1 = real (1::nat)");
  apply (erule ssubst);
  apply (rule natfloor_real_id);
  apply simp;
done;

lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y";
  apply (case_tac "0 <= x");
  apply (subst natfloor_def)+;
  apply (subst nat_le_eq_zle);
  apply force;
  apply (erule floor_le2); 
  apply (subst natfloor_neg);back;
  apply arith;
  apply force;
done;

lemma natfloor_plus_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1";
  apply (subgoal_tac "natfloor (x + 1) = natfloor(x + real (1::nat))");
  apply (erule ssubst);
  apply (erule natfloor_add);
  apply simp;
done;

subsection {* powr and ln *}

lemma zero_le_powr [iff]: "0 <= x powr y";
  apply (rule order_less_imp_le);
  apply simp;
done;

lemma powr_realpow: "0 < x ==> x powr (real n) = x^n";
  apply (induct n);
  apply simp;
  apply (subgoal_tac "real(Suc n) = real n + 1");
  apply (erule ssubst);
  apply (subst powr_add);
  apply simp;
  apply simp;
done;

lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0
  else x powr (real n))";
  apply (case_tac "x = 0");
  apply simp;
  apply simp;
  apply (rule powr_realpow [THEN sym]);
  apply simp;
done;

lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x";
  apply (unfold powr_def);
  apply simp;
done;

lemma ln_bound: "1 <= x ==> ln x <= x";
  apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1");
  apply simp;
  apply (rule ln_add_one_self_le_self);
  apply simp;
done;

lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b";
  apply (case_tac "x = 1");
  apply simp;
  apply (case_tac "a = b");
  apply simp;
  apply (rule order_less_imp_le);
  apply (rule powr_less_mono);
  apply auto;
done;

lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a";
  apply (subst powr_zero_eq_one [THEN sym]);
  apply (rule powr_mono);
  apply assumption+;
done;

lemma power_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a <
    y powr a";
  apply (unfold powr_def);
  apply (rule exp_less_mono);
  apply (rule mult_strict_left_mono);
  apply (subst ln_less_cancel_iff);
  apply assumption;
  apply (rule order_less_trans);
  prefer 2;
  apply assumption+;
done;

lemma power_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <=
   y powr a";
  apply (case_tac "a = 0");
  apply simp; 
  apply (case_tac "x = y");
  apply simp;
  apply (rule order_less_imp_le);
  apply (rule power_less_mono2); 
  apply auto;
done;

lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a";
  apply (rule real_le_mult_imp_le_div_pos2);
  apply assumption;
  apply (subst ln_pwr [THEN sym]);
  apply auto;
  apply (rule ln_bound);
  apply (erule ge_one_powr_ge_zero);
  apply (erule order_less_imp_le);
done;

lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x";
proof -;
  assume "1 < x" and "0 < a";
  then have "ln x <= (x powr (1 / a)) / (1 / a)";
    apply (intro ln_powr_bound);
    apply (erule order_less_imp_le);
    apply (erule real_one_over_pos);
    done;
  also have "... = a * (x powr (1 / a))";
    by simp;
  finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a";
    apply (intro power_mono2);
    apply (rule order_less_imp_le, rule prems);
    apply (rule ln_gt_zero);
    apply (rule prems);
    apply assumption;
    done;
  also have "... = (a powr a) * ((x powr (1 / a)) powr a)";
    apply (rule powr_mult);
    apply (rule prems);
    apply (rule powr_gt_zero);
    done;
  also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)";
    by (rule powr_powr);
  also have "... = x";
    apply simp;
    apply (subgoal_tac "a ~= 0");
    apply (insert prems, auto);
    done;
  finally show ?thesis;.;
qed;

lemma power_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a <
    x powr a";
  apply (unfold powr_def);
  apply (rule exp_less_mono);
  apply (rule mult_strict_left_mono_neg);
  apply (subst ln_less_cancel_iff);
  apply assumption;
  apply (rule order_less_trans);
  prefer 2;
  apply assumption+;
done;

lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0";
  apply (unfold LIMSEQ_def);
  apply clarsimp;
  apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI);
  apply clarify;
  proof -;
    fix r; fix n;
    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n";
    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1";
      by (rule real_of_nat_floor_add_one_gt);
    also have "... = real(natfloor(r powr (1 / -s)) + 1)";
      by simp;
    also have "... <= real n";
      apply (subst real_of_nat_le_iff);
      apply (rule prems);
      done;
    finally have "r powr (1 / - s) < real n";.;
    then have "real n powr (- s) < (r powr (1 / - s)) powr - s"; 
      apply (intro power_less_mono2_neg);
      apply (auto simp add: prems);
      done;
    also have "... = r";
      by (simp add: powr_powr prems less_imp_neq [THEN not_sym]);
    finally show "real n powr - s < r";.;
  qed;

lemma powr_divide2: "x powr a / x powr b = x powr (a - b)";
  apply (simp add: powr_def);
  apply (subst exp_diff [THEN sym]);
  apply (simp add: left_diff_distrib);
done;

lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)";  
proof -;
  assume "exp 1 <= x" and "x <= y";
  have a: "0 < x" and b: "0 < y";
    apply (insert prems);
    apply (subgoal_tac "0 < exp 1");
    apply arith;
    apply auto;
    apply (subgoal_tac "0 < exp 1");
    apply arith;
    apply auto;
    done;
  have "x * ln y - x * ln x = x * (ln y - ln x)";
    by (simp add: ring_eq_simps);
  also have "... = x * ln(y / x)";
    apply (subst ln_div);
    apply (rule b, rule a, rule refl);
    done;
  also have "y / x = (x + (y - x)) / x";
    by simp;
  also have "... = 1 + (y - x) / x";
    apply (simp only: add_divide_distrib);
    apply (simp add: prems);
    apply (insert a, arith);
    done;
  also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)";
    apply (rule mult_left_mono);
    apply (rule ln_add_one_self_le_self);
    apply (rule real_ge_zero_div_gt_zero);
    apply (simp_all add: prems a);
    apply (rule order_less_imp_le, rule a);
    done;
  also have "... = y - x";
    apply simp;
    apply (insert a, arith);
    done;
  also have "... = (y - x) * ln (exp 1)";
    by simp;
  also have "... <= (y - x) * ln x";
    apply (rule mult_left_mono);
    apply (subst ln_le_cancel_iff);
    apply force;
    apply (rule a);
    apply (rule prems);
    apply (simp add: prems);
    done;
  also have "... = y * ln x - x * ln x";
    by (rule left_diff_distrib);
  finally have "x * ln y <= y * ln x";
    by arith;
  then have "ln y <= (y * ln x) / x";
    apply (subst pos_le_divide_eq);
    apply (rule a);
    apply (simp add: mult_ac);
    done;
  also have "... = y * (ln x / x)";
    by simp;
  finally show ?thesis; 
    apply (subst pos_divide_le_eq);
    apply (rule b);
    apply (simp add: mult_ac);
    done;
qed;


end