src/HOL/Deriv.thy

 
 lemma real_differentiableE [elim?]:
   assumes f: "f differentiable (at x within s)"
   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)"
 proof -

 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)"
+    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)"
     using dif unfolding differentiable_def by metis
   then have "\<exists>z. a < z \<and> z < b \<and> f' z = (\<lambda>v. 0)"

   shows "f b - f a = (b - a) * k"
 proof (cases a b rule: linorder_cases)
   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
 
 lemma DERIV_const_ratio_const2:

     and con: "continuous_on {a..b} f"
   shows "f a < f b"
 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"
     by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
   with assms z show False

   with \<open>a \<le> b\<close> have "a < b"
     by linarith
   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
   with ** have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
     (metis * add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl)

   qed
   then obtain l where l: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
   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)"
     using g'c f'c by (auto intro!: derivative_eq_intros)
   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)