--- a/src/HOL/Analysis/Borel_Space.thy Thu Sep 20 14:18:11 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Sep 20 18:20:02 2018 +0100
@@ -219,10 +219,7 @@
assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
shows "continuous_on A f"
apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
- apply (intro ballI Deriv.differentiableI)
- apply (rule has_field_derivative_subset[OF assms])
- apply simp_all
- done
+ using assms differentiable_at_withinI real_differentiable_def by blast
lemma%important closure_contains_Sup:
fixes S :: "real set"
--- a/src/HOL/Computational_Algebra/Polynomial.thy Thu Sep 20 14:18:11 2018 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Sep 20 18:20:02 2018 +0100
@@ -2622,10 +2622,8 @@
lemma poly_MVT: "a < b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p b - poly p a = (b - a) * poly (pderiv p) x"
for a b :: real
using MVT [of a b "poly p"]
- apply auto
- apply (rule_tac x = z in exI)
- apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
- done
+ apply simp
+ by (metis (full_types) DERIV_continuous_on DERIV_unique has_field_derivative_at_within poly_DERIV)
lemma poly_MVT':
fixes a b :: real
--- a/src/HOL/Deriv.thy Thu Sep 20 14:18:11 2018 +0100
+++ b/src/HOL/Deriv.thy Thu Sep 20 18:20:02 2018 +0100
@@ -686,14 +686,6 @@
obtains df where "(f has_real_derivative df) (at x within s)"
using assms by (auto simp: real_differentiable_def)
-lemma differentiableD:
- "f differentiable (at x within s) \<Longrightarrow> \<exists>D. (f has_real_derivative D) (at x within s)"
- by (auto elim: real_differentiableE)
-
-lemma differentiableI:
- "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
- by (force simp add: real_differentiable_def)
-
lemma has_field_derivative_iff:
"(f has_field_derivative D) (at x within S) \<longleftrightarrow>
((\<lambda>y. (f y - f x) / (y - x)) \<longlongrightarrow> D) (at x within S)"
@@ -1374,7 +1366,7 @@
corollary Rolle:
fixes a b :: real
assumes ab: "a < b" "f a = f b" "continuous_on {a..b} f"
- and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
+ and dif [rule_format]: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
shows "\<exists>z. a < z \<and> z < b \<and> DERIV f z :> 0"
proof -
obtain f' where f': "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
@@ -1523,12 +1515,12 @@
case less
show ?thesis
using MVT [OF less] df
- by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on differentiableI)
+ by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on real_differentiable_def)
next
case greater
have "f a - f b = (a - b) * k"
using MVT [OF greater] df
- by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on differentiableI)
+ by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on real_differentiable_def)
then show ?thesis
by (simp add: algebra_simps)
qed auto
@@ -1592,7 +1584,7 @@
proof (rule ccontr)
assume f: "\<not> ?thesis"
have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
- by (rule MVT) (use assms Deriv.differentiableI in \<open>force+\<close>)
+ by (rule MVT) (use assms real_differentiable_def in \<open>force+\<close>)
then obtain l z where z: "a < z" "z < b" "DERIV f z :> l" and "f b - f a = (b - a) * l"
by auto
with assms f have "\<not> l > 0"
@@ -1625,7 +1617,7 @@
moreover have "continuous_on {a..b} f"
by (meson DERIV_isCont assms(2) atLeastAtMost_iff continuous_at_imp_continuous_on)
ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
- using assms MVT [OF \<open>a < b\<close>, of f] differentiableI less_eq_real_def by blast
+ using assms MVT [OF \<open>a < b\<close>, of f] real_differentiable_def less_eq_real_def by blast
then obtain l z where lz: "a < z" "z < b" "DERIV f z :> l" and **: "f b - f a = (b - a) * l"
by auto
with * have "a < b" "f b < f a" by auto
@@ -1772,14 +1764,11 @@
then obtain c where c: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
from c have cint: "a < c \<and> c < b" by auto
- with gd have "g differentiable (at c)" by simp
- then have "\<exists>D. DERIV g c :> D" by (rule differentiableD)
- then obtain g'c where g'c: "DERIV g c :> g'c" ..
-
+ then obtain g'c where g'c: "DERIV g c :> g'c"
+ using gd real_differentiable_def by blast
from c have "a < c \<and> c < b" by auto
- with fd have "f differentiable (at c)" by simp
- then have "\<exists>D. DERIV f c :> D" by (rule differentiableD)
- then obtain f'c where f'c: "DERIV f c :> f'c" ..
+ then obtain f'c where f'c: "DERIV f c :> f'c"
+ using fd real_differentiable_def by blast
from c have "DERIV ?h c :> l" by auto
moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)"
--- a/src/HOL/MacLaurin.thy Thu Sep 20 14:18:11 2018 +0100
+++ b/src/HOL/MacLaurin.thy Thu Sep 20 18:20:02 2018 +0100
@@ -95,7 +95,7 @@
have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x"
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)"
- by (rule differentiableI [OF difg_Suc [rule_format]]) simp
+ using difg_Suc real_differentiable_def by auto
have difg_Suc_eq_0:
"\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0"
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
@@ -111,9 +111,7 @@
by (simp add: difg_0 g2)
show "continuous_on {0..h} (difg 0)"
by (simp add: continuous_at_imp_continuous_on isCont_difg n)
- show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0::nat) differentiable (at x)"
- by (simp add: differentiable_difg n)
- qed
+ qed (simp add: differentiable_difg n)
next
case (Suc m')
then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0"
@@ -129,9 +127,7 @@
using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg)
then show "continuous_on {0..t} (difg (Suc m'))"
by (simp add: continuous_at_imp_continuous_on)
- show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)"
- using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: differentiable_difg)
- qed
+ qed (use \<open>t < h\<close> \<open>Suc m' < n\<close> in \<open>simp add: differentiable_difg\<close>)
with \<open>t < h\<close> show ?case
by auto
qed
--- a/src/HOL/Transcendental.thy Thu Sep 20 14:18:11 2018 +0100
+++ b/src/HOL/Transcendental.thy Thu Sep 20 18:20:02 2018 +0100
@@ -4649,7 +4649,7 @@
then have "continuous_on {u..v} tan"
by (simp add: continuous_at_imp_continuous_on)
moreover have "\<And>x. u < x \<and> x < v \<Longrightarrow> tan differentiable (at x)"
- by (metis DERIV_tan cos_gt_zero_pi differentiableI less_numeral_extra(3) order.strict_trans u(1) v(2))
+ by (metis DERIV_tan cos_gt_zero_pi real_differentiable_def less_numeral_extra(3) order.strict_trans u(1) v(2))
ultimately obtain z where "u < z" "z < v" "DERIV tan z :> 0"
by (metis less Rolle eq)
moreover have "cos z \<noteq> 0"
@@ -4663,7 +4663,7 @@
then have "continuous_on {v..u} tan"
by (simp add: continuous_at_imp_continuous_on)
moreover have "\<And>x. v < x \<and> x < u \<Longrightarrow> tan differentiable (at x)"
- by (metis DERIV_tan cos_gt_zero_pi differentiableI less_numeral_extra(3) order.strict_trans u(2) v(1))
+ by (metis DERIV_tan cos_gt_zero_pi real_differentiable_def less_numeral_extra(3) order.strict_trans u(2) v(1))
ultimately obtain z where "v < z" "z < u" "DERIV tan z :> 0"
by (metis greater Rolle eq)
moreover have "cos z \<noteq> 0"