# HG changeset patch
# User paulson
# Date 1537449491 -3600
# Node ID 4dee7d3267033e5187fd905440ee3cb941cfc8ee
# Parent  a6ba77af64862a030e526a7b1681b377abd53ca1# Parent  4f94e262976d6dc61b93b01aa821fcc82098b10a
merged

diff -r a6ba77af6486 -r 4dee7d326703 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Thu Sep 20 14:18:11 2018 +0100
@@ -482,9 +482,7 @@
   by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
 
 
-subsection \<open>The traditional Rolle theorem in one dimension\<close>
-
-text \<open>Derivatives of local minima and maxima are zero.\<close>
+subsection \<open>Derivatives of local minima and maxima are zero.\<close>
 
 lemma has_derivative_local_min:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
@@ -544,7 +542,7 @@
     by (rule has_derivative_local_min)
 qed
 
-lemma differential_zero_maxmin_component: (* TODO: delete? *)
+lemma differential_zero_maxmin_component:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes k: "k \<in> Basis"
     and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)"
@@ -563,78 +561,8 @@
     unfolding fun_eq_iff by simp
 qed
 
-theorem Rolle:
-  fixes f :: "real \<Rightarrow> real"
-  assumes "a < b"
-    and fab: "f a = f b"
-    and contf: "continuous_on {a..b} f"
-    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
-  shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
-proof -
-  have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
-  proof -
-    have "(a + b) / 2 \<in> {a..b}"
-      using assms(1) by auto
-    then have *: "{a..b} \<noteq> {}"
-      by auto
-    obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d"
-      using continuous_attains_sup[OF compact_Icc * contf] by auto
-    obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y"
-      using continuous_attains_inf[OF compact_Icc * contf] by auto
-    show ?thesis
-    proof (cases "d \<in> box a b \<or> c \<in> box a b")
-      case True
-      then show ?thesis
-        by (metis c(2) d(2) box_subset_cbox subset_iff)
-    next
-      define e where "e = (a + b) /2"
-      case False
-      then have "f d = f c"
-        using d c fab by auto
-      with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
-        by force
-      then show ?thesis
-        by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>)
-    qed
-  qed
-  then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
-    by auto
-  then have "f' x = (\<lambda>v. 0)"
-    apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
-    using assms
-    apply auto
-    done
-  then show ?thesis
-    by (metis x(1))
-qed
-
-
 subsection \<open>One-dimensional mean value theorem\<close>
 
-theorem mvt:
-  fixes f :: "real \<Rightarrow> real"
-  assumes "a < b"
-    and contf: "continuous_on {a..b} f"
-    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
-  shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
-proof -
-  have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
-  proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
-    fix x
-    assume x: "a < x" "x < b"
-    show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
-        (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
-      by (intro derivative_intros derf[OF x])
-  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
-  then obtain x where
-    "x \<in> {a <..< b}"
-    "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
-  then show ?thesis
-    by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
-      zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero
-      times_divide_eq_left)
-qed
-
 lemma mvt_simple:
   fixes f :: "real \<Rightarrow> real"
   assumes "a < b"
@@ -647,7 +575,7 @@
     by (rule differentiable_imp_continuous_on)
   show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
     by (metis at_within_Icc_at derf leI order.asym that)
-qed (rule assms)
+qed (use assms in auto)
 
 lemma mvt_very_simple:
   fixes f :: "real \<Rightarrow> real"
@@ -677,9 +605,9 @@
   shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
 proof -
   have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
-    apply (rule mvt [OF \<open>a < b\<close>])
+    apply (rule mvt [OF \<open>a < b\<close>, where f = "\<lambda>x. (f b - f a) \<bullet> f x"])
     apply (intro continuous_intros contf)
-    using derf apply (blast intro: has_derivative_inner_right)
+    using derf apply (auto intro: has_derivative_inner_right)
     done
   then obtain x where x: "x \<in> {a<..<b}"
     "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
diff -r a6ba77af6486 -r 4dee7d326703 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu Sep 20 14:18:11 2018 +0100
@@ -1180,6 +1180,10 @@
 lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"  (* FIXME drop *)
   by (simp add: INT_Int_distrib)
 
+lemma Int_Inter_eq: "A \<inter> \<Inter>\<B> = (if \<B>={} then A else (\<Inter>B\<in>\<B>. A \<inter> B))"
+                    "\<Inter>\<B> \<inter> A = (if \<B>={} then A else (\<Inter>B\<in>\<B>. B \<inter> A))"
+  by auto
+
 lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"  (* FIXME drop *)
   \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
   \<comment> \<open>Union of a family of unions\<close>
diff -r a6ba77af6486 -r 4dee7d326703 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/HOL/Deriv.thy	Thu Sep 20 14:18:11 2018 +0100
@@ -870,6 +870,11 @@
 corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
   by (rule DERIV_continuous)
 
+lemma DERIV_atLeastAtMost_imp_continuous_on:
+  assumes "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y"
+  shows "continuous_on {a..b} f"
+  by (meson DERIV_isCont assms atLeastAtMost_iff continuous_at_imp_continuous_at_within continuous_on_eq_continuous_within)
+
 lemma DERIV_continuous_on:
   "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x within s)) \<Longrightarrow> continuous_on s f"
   unfolding continuous_on_eq_continuous_within
@@ -1280,62 +1285,67 @@
    \<open>[a,b]\<close> and differentiable on the open interval \<open>(a,b)\<close>,
    and @{term "f a = f b"},
    then there exists \<open>x0 \<in> (a,b)\<close> such that @{term "f' x0 = 0"}\<close>
-theorem Rolle:
-  fixes a b :: real
-  assumes lt: "a < b"
-    and eq: "f a = f b"
-    and con: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
-    and dif [rule_format]: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
-  shows "\<exists>z. a < z \<and> z < b \<and> DERIV f z :> 0"
+theorem Rolle_deriv:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "a < b"
+    and fab: "f a = f b"
+    and contf: "continuous_on {a..b} f"
+    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+  shows "\<exists>z. a < z \<and> z < b \<and> f' z = (\<lambda>v. 0)"
 proof -
   have le: "a \<le> b"
-    using lt by simp
-  from isCont_eq_Ub [OF le con]
+    using \<open>a < b\<close> by simp
+    have "(a + b) / 2 \<in> {a..b}"
+      using assms(1) by auto
+    then have *: "{a..b} \<noteq> {}"
+      by auto
   obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" and "a \<le> x" "x \<le> b"
-    by blast
-  from isCont_eq_Lb [OF le con]
+    using continuous_attains_sup[OF compact_Icc * contf]
+    by (meson atLeastAtMost_iff)
   obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" and "a \<le> x'" "x' \<le> b"
-    by blast
+    using continuous_attains_inf[OF compact_Icc * contf] by (meson atLeastAtMost_iff)
   consider "a < x" "x < b" | "x = a \<or> x = b"
     using \<open>a \<le> x\<close> \<open>x \<le> b\<close> by arith
   then show ?thesis
   proof cases
     case 1
     \<comment> \<open>@{term f} attains its maximum within the interval\<close>
+    then obtain l where der: "DERIV f x :> l"
+      using derf differentiable_def real_differentiable_def by blast
     obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
       using lemma_interval [OF 1] by blast
     then have bound': "\<forall>y. \<bar>x - y\<bar> < d \<longrightarrow> f y \<le> f x"
       using x_max by blast
-    obtain l where der: "DERIV f x :> l"
-      using differentiableD [OF dif [OF conjI [OF 1]]] ..
     \<comment> \<open>the derivative at a local maximum is zero\<close>
     have "l = 0"
       by (rule DERIV_local_max [OF der d bound'])
-    with 1 der show ?thesis by auto
+    with 1 der derf [of x] show ?thesis
+      by (metis has_derivative_unique has_field_derivative_def mult_zero_left)
   next
     case 2
-    then have fx: "f b = f x" by (auto simp add: eq)
+    then have fx: "f b = f x" by (auto simp add: fab)
     consider "a < x'" "x' < b" | "x' = a \<or> x' = b"
       using \<open>a \<le> x'\<close> \<open>x' \<le> b\<close> by arith
     then show ?thesis
     proof cases
       case 1
         \<comment> \<open>@{term f} attains its minimum within the interval\<close>
+      then obtain l where der: "DERIV f x' :> l"
+        using derf differentiable_def real_differentiable_def by blast 
       from lemma_interval [OF 1]
       obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
         by blast
       then have bound': "\<forall>y. \<bar>x' - y\<bar> < d \<longrightarrow> f x' \<le> f y"
         using x'_min by blast
-      from differentiableD [OF dif [OF conjI [OF 1]]]
-      obtain l where der: "DERIV f x' :> l" ..
       have "l = 0" by (rule DERIV_local_min [OF der d bound'])
         \<comment> \<open>the derivative at a local minimum is zero\<close>
-      then show ?thesis using 1 der by auto
+      then show ?thesis using 1 der derf [of x'] 
+        by (metis has_derivative_unique has_field_derivative_def mult_zero_left)
     next
       case 2
         \<comment> \<open>@{term f} is constant throughout the interval\<close>
-      then have fx': "f b = f x'" by (auto simp: eq)
-      from dense [OF lt] obtain r where r: "a < r" "r < b" by blast
+      then have fx': "f b = f x'" by (auto simp: fab)
+      from dense [OF \<open>a < b\<close>] obtain r where r: "a < r" "r < b" by blast
       obtain d where d: "0 < d" and bound: "\<forall>y. \<bar>r - y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
         using lemma_interval [OF r] by blast
       have eq_fb: "f z = f b" if "a \<le> z" and "z \<le> b" for z
@@ -1351,55 +1361,68 @@
         then show "f r = f y" by (simp add: eq_fb r order_less_imp_le)
       qed
       obtain l where der: "DERIV f r :> l"
-        using differentiableD [OF dif [OF conjI [OF r]]] ..
+        using derf differentiable_def r(1) r(2) real_differentiable_def by blast
       have "l = 0"
         by (rule DERIV_local_const [OF der d bound'])
         \<comment> \<open>the derivative of a constant function is zero\<close>
-      with r der show ?thesis by auto
+      with r der derf [of r] show ?thesis
+        by (metis has_derivative_unique has_field_derivative_def mult_zero_left)
     qed
   qed
 qed
 
+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)"
+  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)"
+    using dif unfolding differentiable_def by metis
+  then have "\<exists>z. a < z \<and> z < b \<and> f' z = (\<lambda>v. 0)"
+    by (metis Rolle_deriv [OF ab])
+  then show ?thesis
+    using f' has_derivative_imp_has_field_derivative by fastforce
+qed
 
 subsection \<open>Mean Value Theorem\<close>
 
-lemma lemma_MVT: "f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b"
-  for a b :: real
-  by (cases "a = b") (simp_all add: field_simps)
+theorem mvt:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "a < b"
+    and contf: "continuous_on {a..b} f"
+    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+  obtains z where "a < z" "z < b" "f b - f a = (f' z) (b - a)"
+proof -
+  have "\<exists>x. a < x \<and> x < b \<and> (\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
+  proof (intro Rolle_deriv[OF \<open>a < b\<close>])
+    fix x
+    assume x: "a < x" "x < b"
+    show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
+        (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
+      by (intro derivative_intros derf[OF x])
+  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
+  then obtain x where
+    "a < x" "x < b"
+    "(\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)" by metis
+  then show ?thesis
+    by (metis (no_types, hide_lams) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close>
+                 less_irrefl nonzero_eq_divide_eq)
+qed
 
 theorem MVT:
   fixes a b :: real
   assumes lt: "a < b"
-    and con:  "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
+    and contf: "continuous_on {a..b} f"
     and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
   shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
 proof -
-  let ?F = "\<lambda>x. f x - ((f b - f a) / (b - a)) * x"
-  have cont_f: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
-    using con by (fast intro: continuous_intros)
-  have dif_f: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
-  proof clarify
-    fix x :: real
-    assume x: "a < x" "x < b"
-    obtain l where der: "DERIV f x :> l"
-      using differentiableD [OF dif] x by blast 
-    show "?F differentiable (at x)"
-      by (rule differentiableI [where D = "l - (f b - f a) / (b - a)"],
-          blast intro: DERIV_diff DERIV_cmult_Id der)
-  qed
-  from Rolle [where f = ?F, OF lt lemma_MVT cont_f dif_f]
-  obtain z where z: "a < z" "z < b" and der: "DERIV ?F z :> 0"
-    by blast
-  have "DERIV (\<lambda>x. ((f b - f a) / (b - a)) * x) z :> (f b - f a) / (b - a)"
-    by (rule DERIV_cmult_Id)
-  then have der_f: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z :> 0 + (f b - f a) / (b - a)"
-    by (rule DERIV_add [OF der])
-  show ?thesis
-  proof (intro exI conjI)
-    show "a < z" and "z < b" using z .
-    show "f b - f a = (b - a) * ((f b - f a) / (b - a))" by simp
-    show "DERIV f z :> ((f b - f a) / (b - a))" using der_f by simp
-  qed
+  obtain f' where derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
+    using dif unfolding differentiable_def by metis
+  then obtain z where "a < z" "z < b" "f b - f a = (f' z) (b - a)"
+    using mvt [OF lt contf] by blast
+  then show ?thesis
+    by (metis derf dif has_derivative_unique has_field_derivative_imp_has_derivative linordered_field_class.sign_simps(5) real_differentiable_def)
 qed
 
 corollary MVT2:
@@ -1411,8 +1434,8 @@
            (f has_real_derivative l) (at z) \<and>
            f b - f a = (b - a) * l"
   proof (rule MVT [OF \<open>a < b\<close>])
-    show  "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
-      using assms by (blast intro: DERIV_isCont)
+    show "continuous_on {a..b} f"
+      by (meson DERIV_continuous atLeastAtMost_iff continuous_at_imp_continuous_on der) 
     show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
       using assms by (force dest: order_less_imp_le simp add: real_differentiable_def)
   qed
@@ -1439,21 +1462,24 @@
 
 lemma DERIV_isconst_end:
   fixes f :: "real \<Rightarrow> real"
-  assumes "a < b" and contf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" 
+  assumes "a < b" and contf: "continuous_on {a..b} f"
     and 0: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
   shows "f b = f a"
-  using  MVT [OF \<open>a < b\<close>] "0" DERIV_unique contf real_differentiable_def by fastforce
+  using MVT [OF \<open>a < b\<close>] "0" DERIV_unique contf real_differentiable_def
+  by (fastforce simp: algebra_simps)
 
 lemma DERIV_isconst2:
   fixes f :: "real \<Rightarrow> real"
-  assumes "a < b" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont f x" "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
+  assumes "a < b" and contf: "continuous_on {a..b} f" and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> DERIV f x :> 0"
     and "a \<le> x" "x \<le> b"
 shows "f x = f a"
-proof (cases "x=a")
-  case False
+proof (cases "a < x")
+  case True
+  have *: "continuous_on {a..x} f"
+    using \<open>x \<le> b\<close> contf continuous_on_subset by fastforce
   show ?thesis
-    by (rule DERIV_isconst_end [where f=f]) (use False assms in auto)
-qed auto
+    by (rule DERIV_isconst_end [OF True *]) (use \<open>x \<le> b\<close> derf in auto)
+qed (use \<open>a \<le> x\<close> in auto)
 
 lemma DERIV_isconst3:
   fixes a b x y :: real
@@ -1466,18 +1492,17 @@
   case False
   let ?a = "min x y"
   let ?b = "max x y"
-
-  have "DERIV f z :> 0" if "?a \<le> z" "z \<le> ?b" for z
+  have *: "DERIV f z :> 0" if "?a \<le> z" "z \<le> ?b" for z
   proof -
     have "a < z" and "z < b"
       using that \<open>x \<in> {a <..< b}\<close> and \<open>y \<in> {a <..< b}\<close> by auto
     then have "z \<in> {a<..<b}" by auto
     then show "DERIV f z :> 0" by (rule derivable)
   qed
-  then have isCont: "\<And>z. \<lbrakk>?a \<le> z; z \<le> ?b\<rbrakk> \<Longrightarrow> isCont f z"
-    and DERIV: "\<And>z. \<lbrakk>?a < z; z < ?b\<rbrakk> \<Longrightarrow> DERIV f z :> 0"
-    using DERIV_isCont by auto
-
+  have isCont: "continuous_on {?a..?b} f"
+    by (meson * DERIV_continuous_on atLeastAtMost_iff has_field_derivative_at_within)
+  have DERIV: "\<And>z. \<lbrakk>?a < z; z < ?b\<rbrakk> \<Longrightarrow> DERIV f z :> 0"
+    using * by auto
   have "?a < ?b" using \<open>x \<noteq> y\<close> by auto
   from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y]
   show ?thesis by auto
@@ -1487,7 +1512,7 @@
   fixes f :: "real \<Rightarrow> real"
   shows "\<forall>x. DERIV f x :> 0 \<Longrightarrow> f x = f y"
   apply (rule linorder_cases [of x y])
-    apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+
+  apply (metis DERIV_continuous DERIV_isconst_end continuous_at_imp_continuous_on)+
   done
 
 lemma DERIV_const_ratio_const:
@@ -1497,12 +1522,15 @@
 proof (cases a b rule: linorder_cases)
   case less
   show ?thesis
-    using MVT [OF less] df by (auto dest: DERIV_isCont DERIV_unique simp: real_differentiable_def)
+    using MVT [OF less] df
+    by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on differentiableI)
 next
   case greater
-  show ?thesis
+  have  "f a - f b = (a - b) * k"
     using MVT [OF greater] df
-    by (fastforce dest: DERIV_continuous DERIV_unique simp: real_differentiable_def algebra_simps)
+    by (metis DERIV_continuous DERIV_unique continuous_at_imp_continuous_on differentiableI)
+  then show ?thesis
+    by (simp add: algebra_simps)
 qed auto
 
 lemma DERIV_const_ratio_const2:
@@ -1559,7 +1587,7 @@
     and f :: "real \<Rightarrow> real"
   assumes "a < b"
     and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)"
-    and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+    and con: "continuous_on {a..b} f"
   shows "f a < f b"
 proof (rule ccontr)
   assume f: "\<not> ?thesis"
@@ -1574,12 +1602,11 @@
 qed
 
 lemma DERIV_pos_imp_increasing:
-  fixes a b :: real
-    and f :: "real \<Rightarrow> real"
+  fixes a b :: real and f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> (\<exists>y. DERIV f x :> y \<and> y > 0)"
+    and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y > 0"
   shows "f a < f b"
-  by (metis DERIV_pos_imp_increasing_open [of a b f] assms DERIV_continuous less_imp_le)
+  by (metis less_le_not_le DERIV_atLeastAtMost_imp_continuous_on DERIV_pos_imp_increasing_open [OF \<open>a < b\<close>] der)
 
 lemma DERIV_nonneg_imp_nondecreasing:
   fixes a b :: real
@@ -1595,9 +1622,10 @@
   assume "a \<noteq> b"
   with \<open>a \<le> b\<close> have "a < b"
     by linarith
-  with assms have "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
-    by (metis (no_types) not_le not_less_iff_gr_or_eq  
-                         MVT [OF \<open>a < b\<close>, of f] DERIV_isCont [of f] differentiableI)
+  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
   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
@@ -1612,7 +1640,7 @@
     and f :: "real \<Rightarrow> real"
   assumes "a < b"
     and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
-    and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+    and con: "continuous_on {a..b} f"
   shows "f a > f b"
 proof -
   have "(\<lambda>x. -f x) a < (\<lambda>x. -f x) b"
@@ -1620,18 +1648,19 @@
     show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> \<exists>y. ((\<lambda>x. - f x) has_real_derivative y) (at x) \<and> 0 < y"
       using assms
       by simp (metis field_differentiable_minus neg_0_less_iff_less)
+    show "continuous_on {a..b} (\<lambda>x. - f x)"
+      using con continuous_on_minus by blast
   qed (use assms in auto)
   then show ?thesis
     by simp
 qed
 
 lemma DERIV_neg_imp_decreasing:
-  fixes a b :: real
-    and f :: "real \<Rightarrow> real"
+  fixes a b :: real and f :: "real \<Rightarrow> real"
   assumes "a < b"
-    and "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
+    and der: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> \<exists>y. DERIV f x :> y \<and> y < 0"
   shows "f a > f b"
-  by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le)
+  by (metis less_le_not_le DERIV_atLeastAtMost_imp_continuous_on DERIV_neg_imp_decreasing_open [OF \<open>a < b\<close>] der)
 
 lemma DERIV_nonpos_imp_nonincreasing:
   fixes a b :: real
@@ -1734,8 +1763,8 @@
   have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l"
   proof (rule MVT)
     from assms show "a < b" by simp
-    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont ?h x"
-      using fc gc by simp
+    show "continuous_on {a..b} ?h"
+      by (simp add: continuous_at_imp_continuous_on fc gc)
     show "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> ?h differentiable (at x)"
       using fd gd by simp
   qed
diff -r a6ba77af6486 -r 4dee7d326703 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/HOL/MacLaurin.thy	Thu Sep 20 14:18:11 2018 +0100
@@ -109,8 +109,8 @@
       show "0 < h" by fact
       show "difg 0 0 = difg 0 h"
         by (simp add: difg_0 g2)
-      show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0::nat)) x"
-        by (simp add: isCont_difg n)
+      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
@@ -125,8 +125,10 @@
       show "0 < t" by fact
       show "difg (Suc m') 0 = difg (Suc m') t"
         using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0)
-      show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
+      have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x"
         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
diff -r a6ba77af6486 -r 4dee7d326703 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/HOL/Transcendental.thy	Thu Sep 20 14:18:11 2018 +0100
@@ -2222,7 +2222,7 @@
     assume "x < 1"
     from dense[OF \<open>x < 1\<close>] obtain a where "x < a" "a < 1" by blast
     from \<open>x < a\<close> have "?l x < ?l a"
-    proof (rule DERIV_pos_imp_increasing, safe)
+    proof (rule DERIV_pos_imp_increasing)
       fix y
       assume "x \<le> y" "y \<le> a"
       with \<open>0 < x\<close> \<open>a < 1\<close> have "0 < 1 / y - 1" "0 < y"
@@ -3293,10 +3293,16 @@
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_sin [THEN DERIV_isCont])
 
+lemma continuous_on_sin_real: "continuous_on {a..b} sin" for a::real
+  using continuous_at_imp_continuous_on isCont_sin by blast
+
 lemma isCont_cos: "isCont cos x"
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_cos [THEN DERIV_isCont])
 
+lemma continuous_on_cos_real: "continuous_on {a..b} cos" for a::real
+  using continuous_at_imp_continuous_on isCont_cos by blast
+
 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
   for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_o2 [OF _ isCont_sin])
@@ -3323,7 +3329,7 @@
   for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   unfolding continuous_on_def by (auto intro: tendsto_sin)
 
-lemma continuous_within_sin: "continuous (at z within s) sin"
+lemma continuous_within_sin: "continuous (at z within s) sin"     
   for z :: "'a::{real_normed_field,banach}"
   by (simp add: continuous_within tendsto_sin)
 
@@ -3710,7 +3716,7 @@
   proof (cases a b rule: linorder_cases)
     case less
     then obtain z where "a < z" "z < b" "(cos has_real_derivative 0) (at z)"
-      using Rolle by (metis cosd isCont_cos ab)
+      using Rolle by (metis cosd continuous_on_cos_real ab)
     then have "sin z = 0"
       using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
     then show ?thesis
@@ -3718,7 +3724,7 @@
   next
     case greater
     then obtain z where "b < z" "z < a" "(cos has_real_derivative 0) (at z)"
-      using Rolle by (metis cosd isCont_cos ab)
+      using Rolle by (metis cosd continuous_on_cos_real ab)
     then have "sin z = 0"
       using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
     then show ?thesis
@@ -4019,7 +4025,7 @@
   proof (cases a b rule: linorder_cases)
     case less
     then obtain z where "a < z" "z < b" "(cos has_real_derivative 0) (at z)"
-      using Rolle by (metis cosd isCont_cos ab)
+      using Rolle by (metis cosd continuous_on_cos_real ab)
     then have "sin z = 0"
       using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
     then show ?thesis
@@ -4027,7 +4033,7 @@
   next
     case greater
     then obtain z where "b < z" "z < a" "(cos has_real_derivative 0) (at z)"
-      using Rolle by (metis cosd isCont_cos ab)
+      using Rolle by (metis cosd continuous_on_cos_real ab)
     then have "sin z = 0"
       using DERIV_cos DERIV_unique neg_equal_0_iff_equal by blast
     then show ?thesis
@@ -4639,7 +4645,9 @@
   proof (cases u v rule: linorder_cases)
     case less
     have "\<And>x. u \<le> x \<and> x \<le> v \<longrightarrow> isCont tan x"
-      by (metis cos_gt_zero_pi isCont_tan less_numeral_extra(3) less_trans order.not_eq_order_implies_strict u v)
+      by (metis cos_gt_zero_pi isCont_tan le_less_trans less_irrefl less_le_trans u(1) v(2))
+    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))
     ultimately obtain z where "u < z" "z < v" "DERIV tan z :> 0"
@@ -4651,13 +4659,15 @@
   next
     case greater
     have "\<And>x. v \<le> x \<and> x \<le> u \<Longrightarrow> isCont tan x"
-      by (metis cos_gt_zero_pi isCont_tan less_numeral_extra(3) less_trans order.not_eq_order_implies_strict u v)
+      by (metis cos_gt_zero_pi isCont_tan le_less_trans less_irrefl less_le_trans u(2) v(1))
+    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))
     ultimately obtain z where "v < z" "z < u" "DERIV tan z :> 0"
       by (metis greater Rolle eq)
     moreover have "cos z \<noteq> 0"
-      by (metis  \<open>v < z\<close> \<open>z < u\<close> cos_gt_zero_pi less_le_trans linorder_not_less not_less_iff_gr_or_eq u(2) v(1))
+      by (metis \<open>v < z\<close> \<open>z < u\<close> cos_gt_zero_pi less_eq_real_def less_le_trans order_less_irrefl u(2) v(1))
     ultimately show ?thesis
       using DERIV_unique [OF _ DERIV_tan] by fastforce
   qed auto
@@ -5756,8 +5766,8 @@
           using \<open>-r < a\<close> \<open>b < r\<close> by auto
         then show "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. suminf (?c x) - arctan x) y :> 0"
           using \<open>\<bar>x\<bar> < r\<close> by auto
-        show "\<And>y. \<lbrakk>a \<le> y; y \<le> b\<rbrakk> \<Longrightarrow>  isCont (\<lambda>x. suminf (?c x) - arctan x) y"
-          using DERIV_in_rball DERIV_isCont by auto
+        show "continuous_on {a..b} (\<lambda>x. suminf (?c x) - arctan x)"
+          using DERIV_in_rball DERIV_atLeastAtMost_imp_continuous_on by blast
       qed
     qed