# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1537464002 -3600
# Node ID e2858770997a5f44b0b971a0f8b9abe80aa00770
# Parent  4dee7d3267033e5187fd905440ee3cb941cfc8ee
removal of more redundancies, and fixes

diff -r 4dee7d326703 -r e2858770997a src/HOL/Analysis/Borel_Space.thy
--- 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"
diff -r 4dee7d326703 -r e2858770997a src/HOL/Computational_Algebra/Polynomial.thy
--- 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
diff -r 4dee7d326703 -r e2858770997a src/HOL/Deriv.thy
--- 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)"
diff -r 4dee7d326703 -r e2858770997a src/HOL/MacLaurin.thy
--- 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
diff -r 4dee7d326703 -r e2858770997a src/HOL/Transcendental.thy
--- 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"