--- a/src/HOL/NSA/HDeriv.thy Fri Sep 20 17:08:08 2013 +0200
+++ b/src/HOL/NSA/HDeriv.thy Fri Sep 20 20:21:54 2013 +0200
@@ -342,34 +342,32 @@
lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)
-(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
lemma NSDERIV_inverse:
- fixes x :: "'a::{real_normed_field}"
- shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
-apply (simp add: nsderiv_def)
-apply (rule ballI, simp, clarify)
-apply (frule (1) Infinitesimal_add_not_zero)
-apply (simp add: add_commute)
-(*apply (auto simp add: starfun_inverse_inverse realpow_two
- simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*)
-apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc
- nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus
- del: inverse_mult_distrib inverse_minus_eq
- minus_mult_left [symmetric] minus_mult_right [symmetric])
-apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
-apply (simp (no_asm_simp) add: mult_assoc [symmetric] distrib_right
- del: minus_mult_left [symmetric] minus_mult_right [symmetric])
-apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
-apply (rule inverse_add_Infinitesimal_approx2)
-apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
- simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
-apply (rule Infinitesimal_HFinite_mult, auto)
-done
+ fixes x :: "'a::real_normed_field"
+ assumes "x \<noteq> 0" -- {* can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero *}
+ shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
+proof -
+ { fix h :: "'a star"
+ assume h_Inf: "h \<in> Infinitesimal"
+ from this assms have not_0: "star_of x + h \<noteq> 0" by (rule Infinitesimal_add_not_zero)
+ assume "h \<noteq> 0"
+ from h_Inf have "h * star_of x \<in> Infinitesimal" by (rule Infinitesimal_HFinite_mult) simp
+ with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
+ inverse (- (star_of x * star_of x))"
+ by (auto intro: inverse_add_Infinitesimal_approx2
+ dest!: hypreal_of_real_HFinite_diff_Infinitesimal
+ simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
+ with not_0 `h \<noteq> 0` assms have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
+ - (inverse (star_of x) * inverse (star_of x))"
+ by (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric]
+ nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus ring_distribs)
+ } then show ?thesis by (simp add: nsderiv_def)
+qed
subsubsection {* Equivalence of NS and Standard definitions *}
lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
-by (simp add: real_scaleR_def divide_inverse mult_commute)
+by (simp add: divide_inverse mult_commute)
text{*Now equivalence between NSDERIV and DERIV*}
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
--- a/src/HOL/ex/Gauge_Integration.thy Fri Sep 20 17:08:08 2013 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Fri Sep 20 20:21:54 2013 +0200
@@ -501,26 +501,29 @@
text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
lemma strad1:
- "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
- \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
- 0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
- \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
-apply clarify
-apply (case_tac "z = x", simp)
-apply (drule_tac x = z in spec)
-apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
- in real_mult_le_cancel_iff2 [THEN iffD1])
- apply simp
-apply (simp del: abs_inverse add: abs_mult [symmetric]
- mult_assoc [symmetric])
-apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x))
- = (f z - f x) / (z - x) - f' x")
- apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
-apply (subst mult_commute)
-apply (simp add: distrib_right diff_minus)
-apply (simp add: mult_assoc divide_inverse)
-apply (simp add: distrib_right)
-done
+ fixes z x s e :: real
+ assumes P: "(\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2)"
+ assumes "\<bar>z - x\<bar> < s"
+ shows "\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e / 2 * \<bar>z - x\<bar>"
+proof (cases "z = x")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x"
+ apply (subst mult_commute)
+ apply (simp add: distrib_right diff_minus)
+ apply (simp add: mult_assoc divide_inverse)
+ apply (simp add: distrib_right)
+ done
+ moreover from False `\<bar>z - x\<bar> < s` have "\<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2"
+ by (rule P)
+ ultimately have "\<bar>inverse (z - x)\<bar> * (\<bar>f z - f x - f' x * (z - x)\<bar> * 2)
+ \<le> \<bar>inverse (z - x)\<bar> * (e * \<bar>z - x\<bar>)"
+ using False by (simp del: abs_inverse add: abs_mult [symmetric] ac_simps)
+ with False have "\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
+ by simp
+ then show ?thesis by simp
+qed
lemma lemma_straddle:
assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
@@ -537,11 +540,11 @@
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
by (simp add: DERIV_iff2 LIM_eq)
with `0 < e` obtain s
- where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+ where "\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
by (drule_tac x="e/2" in spec, auto)
- then have strad [rule_format]:
- "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
- using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
+ with strad1 [of x s f f' e] have strad:
+ "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
+ by auto
show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
proof (safe intro!: exI)
show "0 < s" by fact