optimize some proofs
authorhuffman
Thu Aug 18 19:53:03 2011 -0700 (2011-08-18)
changeset 44289d81d09cdab9c
parent 44288 fe9c2398c330
child 44290 23a5137162ea
optimize some proofs
src/HOL/Ln.thy
src/HOL/NthRoot.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Ln.thy	Thu Aug 18 18:10:23 2011 -0700
     1.2 +++ b/src/HOL/Ln.thy	Thu Aug 18 19:53:03 2011 -0700
     1.3 @@ -18,7 +18,7 @@
     1.4        inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
     1.5      by (rule suminf_split_initial_segment)
     1.6    also have "?a = 1 + x"
     1.7 -    by (simp add: numerals)
     1.8 +    by (simp add: numeral_2_eq_2)
     1.9    finally show ?thesis .
    1.10  qed
    1.11  
    1.12 @@ -70,13 +70,7 @@
    1.13        finally show ?thesis .
    1.14      qed
    1.15      moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
    1.16 -      apply (simp add: mult_compare_simps)
    1.17 -      apply (simp add: assms)
    1.18 -      apply (subgoal_tac "0 <= x * (x * x^n)")
    1.19 -      apply force
    1.20 -      apply (rule mult_nonneg_nonneg, rule a)+
    1.21 -      apply (rule zero_le_power, rule a)
    1.22 -      done
    1.23 +      by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b)
    1.24      ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
    1.25          (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
    1.26        apply (rule mult_mono)
    1.27 @@ -162,7 +156,7 @@
    1.28      apply auto
    1.29      done
    1.30    also from a have "... <= 1 + x"
    1.31 -    by (simp add: field_simps zero_compare_simps)
    1.32 +    by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
    1.33    finally show ?thesis .
    1.34  qed
    1.35  
    1.36 @@ -344,24 +338,17 @@
    1.37  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
    1.38  proof -
    1.39    assume x: "exp 1 <= x" "x <= y"
    1.40 -  have a: "0 < x" and b: "0 < y"
    1.41 -    apply (insert x)
    1.42 -    apply (subgoal_tac "0 < exp (1::real)")
    1.43 -    apply arith
    1.44 -    apply auto
    1.45 -    apply (subgoal_tac "0 < exp (1::real)")
    1.46 -    apply arith
    1.47 -    apply auto
    1.48 -    done
    1.49 +  moreover have "0 < exp (1::real)" by simp
    1.50 +  ultimately have a: "0 < x" and b: "0 < y"
    1.51 +    by (fast intro: less_le_trans order_trans)+
    1.52    have "x * ln y - x * ln x = x * (ln y - ln x)"
    1.53      by (simp add: algebra_simps)
    1.54    also have "... = x * ln(y / x)"
    1.55 -    apply (subst ln_div)
    1.56 -    apply (rule b, rule a, rule refl)
    1.57 -    done
    1.58 +    by (simp only: ln_div a b)
    1.59    also have "y / x = (x + (y - x)) / x"
    1.60      by simp
    1.61 -  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
    1.62 +  also have "... = 1 + (y - x) / x"
    1.63 +    using x a by (simp add: field_simps)
    1.64    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
    1.65      apply (rule mult_left_mono)
    1.66      apply (rule ln_add_one_self_le_self)
    1.67 @@ -373,7 +360,7 @@
    1.68    also have "... <= (y - x) * ln x"
    1.69      apply (rule mult_left_mono)
    1.70      apply (subst ln_le_cancel_iff)
    1.71 -    apply force
    1.72 +    apply fact
    1.73      apply (rule a)
    1.74      apply (rule x)
    1.75      using x apply simp
     2.1 --- a/src/HOL/NthRoot.thy	Thu Aug 18 18:10:23 2011 -0700
     2.2 +++ b/src/HOL/NthRoot.thy	Thu Aug 18 19:53:03 2011 -0700
     2.3 @@ -29,7 +29,7 @@
     2.4        using n1 by (rule power_increasing, simp)
     2.5      finally show "a \<le> max 1 a ^ n" .
     2.6      show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
     2.7 -      by (simp add: isCont_power)
     2.8 +      by simp
     2.9    qed
    2.10    then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
    2.11    with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
    2.12 @@ -310,7 +310,7 @@
    2.13      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
    2.14        by (simp add: abs_le_iff real_root_power_cancel n)
    2.15      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
    2.16 -      by (simp add: isCont_power)
    2.17 +      by simp
    2.18    qed
    2.19    thus ?thesis using n x by simp
    2.20  qed
    2.21 @@ -320,7 +320,7 @@
    2.22  apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
    2.23  apply (simp add: real_root_minus)
    2.24  apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
    2.25 -apply (simp add: isCont_minus isCont_root_pos)
    2.26 +apply (simp add: isCont_root_pos)
    2.27  done
    2.28  
    2.29  lemma isCont_root_zero:
     3.1 --- a/src/HOL/Series.thy	Thu Aug 18 18:10:23 2011 -0700
     3.2 +++ b/src/HOL/Series.thy	Thu Aug 18 19:53:03 2011 -0700
     3.3 @@ -26,10 +26,7 @@
     3.4     suminf   :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" where
     3.5     "suminf f = (THE s. f sums s)"
     3.6  
     3.7 -syntax
     3.8 -  "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
     3.9 -translations
    3.10 -  "\<Sum>i. b" == "CONST suminf (%i. b)"
    3.11 +notation suminf (binder "\<Sum>" 10)
    3.12  
    3.13  
    3.14  lemma [trans]: "f=g ==> g sums z ==> f sums z"
    3.15 @@ -560,7 +557,7 @@
    3.16    moreover have "summable ?g" by (rule summable_zero)
    3.17    moreover from sm have "summable f" .
    3.18    ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
    3.19 -  then show "0 \<le> suminf f" by (simp add: suminf_zero)
    3.20 +  then show "0 \<le> suminf f" by simp
    3.21  qed
    3.22  
    3.23  
     4.1 --- a/src/HOL/Transcendental.thy	Thu Aug 18 18:10:23 2011 -0700
     4.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 18 19:53:03 2011 -0700
     4.3 @@ -881,7 +881,7 @@
     4.4  by (simp add: diffs_def)
     4.5  
     4.6  lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
     4.7 -by (auto intro!: ext simp add: exp_def)
     4.8 +by (auto simp add: exp_def)
     4.9  
    4.10  lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
    4.11  apply (simp add: exp_def)
    4.12 @@ -1248,7 +1248,7 @@
    4.13        by (rule DERIV_diff)
    4.14      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
    4.15    qed (auto simp add: assms)
    4.16 -  thus ?thesis by (auto simp add: suminf_zero)
    4.17 +  thus ?thesis by auto
    4.18  qed
    4.19  
    4.20  subsection {* Sine and Cosine *}
    4.21 @@ -1337,10 +1337,10 @@
    4.22  by (auto intro!: sums_unique sums_minus sin_converges)
    4.23  
    4.24  lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
    4.25 -by (auto intro!: ext simp add: sin_def)
    4.26 +  by (auto simp add: sin_def)
    4.27  
    4.28  lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
    4.29 -by (auto intro!: ext simp add: cos_def)
    4.30 +  by (auto simp add: cos_def)
    4.31  
    4.32  lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
    4.33  apply (simp add: cos_def)