src/HOL/Deriv.thy
changeset 41550 efa734d9b221
parent 41368 8afa26855137
child 44079 bcc60791b7b9
     1.1 --- a/src/HOL/Deriv.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -355,7 +355,7 @@
     1.4  lemma differentiableE [elim?]:
     1.5    assumes "f differentiable x"
     1.6    obtains df where "DERIV f x :> df"
     1.7 -  using prems unfolding differentiable_def ..
     1.8 +  using assms unfolding differentiable_def ..
     1.9  
    1.10  lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
    1.11  by (simp add: differentiable_def)
    1.12 @@ -408,7 +408,7 @@
    1.13    assumes "f differentiable x"
    1.14    assumes "g differentiable x"
    1.15    shows "(\<lambda>x. f x - g x) differentiable x"
    1.16 -  unfolding diff_minus using prems by simp
    1.17 +  unfolding diff_minus using assms by simp
    1.18  
    1.19  lemma differentiable_mult [simp]:
    1.20    assumes "f differentiable x"
    1.21 @@ -437,13 +437,16 @@
    1.22    assumes "f differentiable x"
    1.23    assumes "g differentiable x" and "g x \<noteq> 0"
    1.24    shows "(\<lambda>x. f x / g x) differentiable x"
    1.25 -  unfolding divide_inverse using prems by simp
    1.26 +  unfolding divide_inverse using assms by simp
    1.27  
    1.28  lemma differentiable_power [simp]:
    1.29    fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
    1.30    assumes "f differentiable x"
    1.31    shows "(\<lambda>x. f x ^ n) differentiable x"
    1.32 -  by (induct n, simp, simp add: prems)
    1.33 +  apply (induct n)
    1.34 +  apply simp
    1.35 +  apply (simp add: assms)
    1.36 +  done
    1.37  
    1.38  
    1.39  subsection {* Nested Intervals and Bisection *}
    1.40 @@ -1227,7 +1230,7 @@
    1.41    assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
    1.42    shows "f a < f b"
    1.43  proof (rule ccontr)
    1.44 -  assume "~ f a < f b"
    1.45 +  assume f: "~ f a < f b"
    1.46    have "EX l z. a < z & z < b & DERIV f z :> l
    1.47        & f b - f a = (b - a) * l"
    1.48      apply (rule MVT)
    1.49 @@ -1236,13 +1239,12 @@
    1.50        apply (metis DERIV_isCont)
    1.51       apply (metis differentiableI less_le)
    1.52      done
    1.53 -  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    1.54 +  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
    1.55        and "f b - f a = (b - a) * l"
    1.56      by auto
    1.57 -  
    1.58 -  from prems have "~(l > 0)"
    1.59 +  with assms f have "~(l > 0)"
    1.60      by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
    1.61 -  with prems show False
    1.62 +  with assms z show False
    1.63      by (metis DERIV_unique less_le)
    1.64  qed
    1.65  
    1.66 @@ -1252,9 +1254,8 @@
    1.67      "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
    1.68    shows "f a \<le> f b"
    1.69  proof (rule ccontr, cases "a = b")
    1.70 -  assume "~ f a \<le> f b"
    1.71 -  assume "a = b"
    1.72 -  with prems show False by auto
    1.73 +  assume "~ f a \<le> f b" and "a = b"
    1.74 +  then show False by auto
    1.75  next
    1.76    assume A: "~ f a \<le> f b"
    1.77    assume B: "a ~= b"
    1.78 @@ -1266,13 +1267,13 @@
    1.79        apply (metis DERIV_isCont)
    1.80       apply (metis differentiableI less_le)
    1.81      done
    1.82 -  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    1.83 +  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
    1.84        and C: "f b - f a = (b - a) * l"
    1.85      by auto
    1.86    with A have "a < b" "f b < f a" by auto
    1.87    with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
    1.88      (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
    1.89 -  with prems show False
    1.90 +  with assms z show False
    1.91      by (metis DERIV_unique order_less_imp_le)
    1.92  qed
    1.93  
    1.94 @@ -1509,14 +1510,14 @@
    1.95  theorem GMVT:
    1.96    fixes a b :: real
    1.97    assumes alb: "a < b"
    1.98 -  and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
    1.99 -  and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
   1.100 -  and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
   1.101 -  and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   1.102 +    and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   1.103 +    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
   1.104 +    and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
   1.105 +    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   1.106    shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
   1.107  proof -
   1.108    let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
   1.109 -  from prems have "a < b" by simp
   1.110 +  from assms have "a < b" by simp
   1.111    moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
   1.112    proof -
   1.113      have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp