# HG changeset patch
# User haftmann
# Date 1379701314 -7200
# Node ID b8e62805566b3f2e07fcb3079d12eb7292b7734e
# Parent  124bb918f45f756d1339c2f68e7cca8535cca8a8
tuned proofs

diff -r 124bb918f45f -r b8e62805566b src/HOL/NSA/HDeriv.thy
--- 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)"
diff -r 124bb918f45f -r b8e62805566b src/HOL/ex/Gauge_Integration.thy
--- 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