# HG changeset patch
# User huffman
# Date 1313722383 25200
# Node ID d81d09cdab9c221442f4dba0e44b86447b04d7eb
# Parent  fe9c2398c330d4bdc8870b14d136fefe548ec1c5
optimize some proofs

diff -r fe9c2398c330 -r d81d09cdab9c src/HOL/Ln.thy
--- 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
diff -r fe9c2398c330 -r d81d09cdab9c src/HOL/NthRoot.thy
--- 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:
diff -r fe9c2398c330 -r d81d09cdab9c src/HOL/Series.thy
--- 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
 
 
diff -r fe9c2398c330 -r d81d09cdab9c src/HOL/Transcendental.thy
--- 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)