# HG changeset patch # User paulson # 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 "\x. x \ A \ (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 \ \x. a < x \ x < b \ 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) \ \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) \ 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) \ ((\y. (f y - f x) / (y - x)) \ 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]: "\x. a < x \ x < b \ f differentiable (at x)" + and dif [rule_format]: "\x. \a < x; x < b\ \ f differentiable (at x)" shows "\z. a < z \ z < b \ DERIV f z :> 0" proof - obtain f' where f': "\x. \a < x; x < b\ \ (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: "\ ?thesis" have "\l z. a < z \ z < b \ DERIV f z :> l \ f b - f a = (b - a) * l" - by (rule MVT) (use assms Deriv.differentiableI in \force+\) + by (rule MVT) (use assms real_differentiable_def in \force+\) 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 "\ 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 "\l z. a < z \ z < b \ DERIV f z :> l \ f b - f a = (b - a) * l" - using assms MVT [OF \a < b\, of f] differentiableI less_eq_real_def by blast + using assms MVT [OF \a < b\, 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 \ c < b \ DERIV ?h c :> l \ ?h b - ?h a = (b - a) * l" .. from c have cint: "a < c \ c < b" by auto - with gd have "g differentiable (at c)" by simp - then have "\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 \ c < b" by auto - with fd have "f differentiable (at c)" by simp - then have "\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: "\m x. m < n \ 0 \ x \ x \ h \ isCont (difg m) x" by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp have differentiable_difg: "\m x. m < n \ 0 \ x \ x \ h \ 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: "\m t. m < n \ 0 \ t \ t \ h \ DERIV (difg m) t :> 0 \ 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 "\x. 0 < x \ x < h \ 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 "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0" @@ -129,9 +127,7 @@ using \t < h\ \Suc m' < n\ by (simp add: isCont_difg) then show "continuous_on {0..t} (difg (Suc m'))" by (simp add: continuous_at_imp_continuous_on) - show "\x. 0 < x \ x < t \ difg (Suc m') differentiable (at x)" - using \t < h\ \Suc m' < n\ by (simp add: differentiable_difg) - qed + qed (use \t < h\ \Suc m' < n\ in \simp add: differentiable_difg\) with \t < h\ 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 "\x. u < x \ x < v \ 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 \ 0" @@ -4663,7 +4663,7 @@ then have "continuous_on {v..u} tan" by (simp add: continuous_at_imp_continuous_on) moreover have "\x. v < x \ x < u \ 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 \ 0"