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
```