--- a/src/HOL/Ln.thy Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/Ln.thy Thu Aug 18 19:53:03 2011 -0700
@@ -18,7 +18,7 @@
inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
by (rule suminf_split_initial_segment)
also have "?a = 1 + x"
- by (simp add: numerals)
+ by (simp add: numeral_2_eq_2)
finally show ?thesis .
qed
@@ -70,13 +70,7 @@
finally show ?thesis .
qed
moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
- apply (simp add: mult_compare_simps)
- apply (simp add: assms)
- apply (subgoal_tac "0 <= x * (x * x^n)")
- apply force
- apply (rule mult_nonneg_nonneg, rule a)+
- apply (rule zero_le_power, rule a)
- done
+ by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b)
ultimately have "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) <=
(1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
apply (rule mult_mono)
@@ -162,7 +156,7 @@
apply auto
done
also from a have "... <= 1 + x"
- by (simp add: field_simps zero_compare_simps)
+ by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
finally show ?thesis .
qed
@@ -344,24 +338,17 @@
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
proof -
assume x: "exp 1 <= x" "x <= y"
- have a: "0 < x" and b: "0 < y"
- apply (insert x)
- apply (subgoal_tac "0 < exp (1::real)")
- apply arith
- apply auto
- apply (subgoal_tac "0 < exp (1::real)")
- apply arith
- apply auto
- done
+ moreover have "0 < exp (1::real)" by simp
+ ultimately have a: "0 < x" and b: "0 < y"
+ by (fast intro: less_le_trans order_trans)+
have "x * ln y - x * ln x = x * (ln y - ln x)"
by (simp add: algebra_simps)
also have "... = x * ln(y / x)"
- apply (subst ln_div)
- apply (rule b, rule a, rule refl)
- done
+ by (simp only: ln_div a b)
also have "y / x = (x + (y - x)) / x"
by simp
- also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
+ also have "... = 1 + (y - x) / x"
+ using x a by (simp add: field_simps)
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)
@@ -373,7 +360,7 @@
also have "... <= (y - x) * ln x"
apply (rule mult_left_mono)
apply (subst ln_le_cancel_iff)
- apply force
+ apply fact
apply (rule a)
apply (rule x)
using x apply simp
--- a/src/HOL/NthRoot.thy Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/NthRoot.thy Thu Aug 18 19:53:03 2011 -0700
@@ -29,7 +29,7 @@
using n1 by (rule power_increasing, simp)
finally show "a \<le> max 1 a ^ n" .
show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
- by (simp add: isCont_power)
+ by simp
qed
then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
@@ -310,7 +310,7 @@
show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
by (simp add: abs_le_iff real_root_power_cancel n)
show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
- by (simp add: isCont_power)
+ by simp
qed
thus ?thesis using n x by simp
qed
@@ -320,7 +320,7 @@
apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
apply (simp add: real_root_minus)
apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
-apply (simp add: isCont_minus isCont_root_pos)
+apply (simp add: isCont_root_pos)
done
lemma isCont_root_zero:
--- a/src/HOL/Series.thy Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/Series.thy Thu Aug 18 19:53:03 2011 -0700
@@ -26,10 +26,7 @@
suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" where
"suminf f = (THE s. f sums s)"
-syntax
- "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
-translations
- "\<Sum>i. b" == "CONST suminf (%i. b)"
+notation suminf (binder "\<Sum>" 10)
lemma [trans]: "f=g ==> g sums z ==> f sums z"
@@ -560,7 +557,7 @@
moreover have "summable ?g" by (rule summable_zero)
moreover from sm have "summable f" .
ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
- then show "0 \<le> suminf f" by (simp add: suminf_zero)
+ then show "0 \<le> suminf f" by simp
qed
--- a/src/HOL/Transcendental.thy Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/Transcendental.thy Thu Aug 18 19:53:03 2011 -0700
@@ -881,7 +881,7 @@
by (simp add: diffs_def)
lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto intro!: ext simp add: exp_def)
+by (auto simp add: exp_def)
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
apply (simp add: exp_def)
@@ -1248,7 +1248,7 @@
by (rule DERIV_diff)
thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
qed (auto simp add: assms)
- thus ?thesis by (auto simp add: suminf_zero)
+ thus ?thesis by auto
qed
subsection {* Sine and Cosine *}
@@ -1337,10 +1337,10 @@
by (auto intro!: sums_unique sums_minus sin_converges)
lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
-by (auto intro!: ext simp add: sin_def)
+ by (auto simp add: sin_def)
lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
-by (auto intro!: ext simp add: cos_def)
+ by (auto simp add: cos_def)
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
apply (simp add: cos_def)