# HG changeset patch
# User paulson
# Date 1096896483 -7200
# Node ID 4d332d10fa3d63534dd57716ac7d6ab1ab1e9c8e
# Parent  804ecdc08cf2f4abee39a67d5b842610e125c596
revised simprules for division

diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Complex/CLim.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -883,7 +883,7 @@
 subsection{* Differentiation of Natural Number Powers*}
 
 lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1"
-by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def)
+by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def divide_self del: divide_self_if)
 
 lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1"
 by (simp add: NSCDERIV_CDERIV_iff [symmetric])
diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -1286,7 +1286,7 @@
   apply (subst setprod_Un_Int [symmetric], auto)
   apply (subgoal_tac "finite (A Int B)")
   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-  apply (subst times_divide_eq_right [THEN sym], auto)
+  apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
   done
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
@@ -1297,7 +1297,7 @@
   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
   apply (erule ssubst)
   apply (subst times_divide_eq_right [THEN sym])
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: mult_ac divide_self)
   done
 
 lemma setprod_inversef: "finite A ==>
diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -30,13 +30,13 @@
   isCont :: "[real=>real,real] => bool"
   "isCont f a == (f -- a --> (f a))"
 
-  (* NS definition dispenses with limit notions *)
   isNSCont :: "[real=>real,real] => bool"
+    --{*NS definition dispenses with limit notions*}
   "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
 			   ( *f* f) y @= hypreal_of_real (f a))"
 
-  (* differentiation: D is derivative of function f at x *)
   deriv:: "[real=>real,real,real] => bool"
+    --{*Differentiation: D is derivative of function f at x*}
 			    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
 
@@ -66,9 +66,10 @@
   "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 
-(*Used in the proof of the Bolzano theorem*)
 consts
   Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
+    --{*Used in the proof of the Bolzano theorem*}
+
 
 primrec
   "Bolzano_bisect P a b 0 = (a,b)"
@@ -91,9 +92,8 @@
       ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
 by (simp add: LIM_eq)
 
-lemma LIM_const: "(%x. k) -- x --> k"
+lemma LIM_const [simp]: "(%x. k) -- x --> k"
 by (simp add: LIM_def)
-declare LIM_const [simp]
 
 lemma LIM_add:
   assumes f: "f -- a --> L" and g: "g -- a --> M"
@@ -237,14 +237,13 @@
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify) 
 apply (drule_tac x = u in spec, clarify)
 apply (drule_tac x = s in spec, clarify)
-apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u")
+apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & \<bar>(xa n) + - x\<bar> < s --> \<bar>f (xa n) + - L\<bar> < u")
 prefer 2 apply blast
 apply (drule FreeUltrafilterNat_all, ultra)
 done
 
-(*---------------------------------------------------------------------
-    Limit: NS definition ==> standard definition
- ---------------------------------------------------------------------*)
+
+subsubsection{*Limit: The NS definition implies the standard definition.*}
 
 lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
          \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
@@ -270,14 +269,12 @@
 by auto
 
 
-(*-------------------
-    NSLIM => LIM
- -------------------*)
+text{*NSLIM => LIM*}
 
 lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
 apply (simp add: LIM_def NSLIM_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
-apply (rule ccontr, simp)  
+apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2, safe)
 apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
@@ -289,52 +286,37 @@
 done
 
 
-(**** Key result ****)
-lemma LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
+theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
 by (blast intro: LIM_NSLIM NSLIM_LIM)
 
-(*-------------------------------------------------------------------*)
-(*   Proving properties of limits using nonstandard definition and   *)
-(*   hence, the properties hold for standard limits as well          *)
-(*-------------------------------------------------------------------*)
-(*------------------------------------------------
-      NSLIM_mult and hence (trivially) LIM_mult
- ------------------------------------------------*)
+text{*Proving properties of limits using nonstandard definition.
+      The properties hold for standard limits as well!*}
 
 lemma NSLIM_mult:
      "[| f -- x --NS> l; g -- x --NS> m |]
       ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
-apply (simp add: NSLIM_def)
-apply (auto intro!: approx_mult_HFinite)
-done
+by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
 
-lemma LIM_mult2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
+lemma LIM_mult2:
+     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
 by (simp add: LIM_NSLIM_iff NSLIM_mult)
 
-(*----------------------------------------------
-      NSLIM_add and hence (trivially) LIM_add
-      Note the much shorter proof
- ----------------------------------------------*)
 lemma NSLIM_add:
      "[| f -- x --NS> l; g -- x --NS> m |]
       ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
-apply (simp add: NSLIM_def)
-apply (auto intro!: approx_add)
-done
+by (auto simp add: NSLIM_def intro!: approx_add)
 
-lemma LIM_add2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
+lemma LIM_add2:
+     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
 by (simp add: LIM_NSLIM_iff NSLIM_add)
 
 
-lemma NSLIM_const: "(%x. k) -- x --NS> k"
+lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
 by (simp add: NSLIM_def)
 
-declare NSLIM_const [simp]
-
 lemma LIM_const2: "(%x. k) -- x --> k"
 by (simp add: LIM_NSLIM_iff)
 
-
 lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
 by (simp add: NSLIM_def)
 
@@ -363,9 +345,9 @@
 
 lemma NSLIM_zero:
   assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
-proof -;
+proof -
   have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
-    by (rule NSLIM_add_minus [OF f NSLIM_const]) 
+    by (rule NSLIM_add_minus [OF f NSLIM_const])
   thus ?thesis by simp
 qed
 
@@ -382,8 +364,6 @@
 apply (auto simp add: diff_minus add_assoc)
 done
 
-
-
 lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
 apply (simp add: NSLIM_def)
 apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
@@ -400,10 +380,10 @@
 
 lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
 apply (rule ccontr)
-apply (blast dest: NSLIM_const_not_eq) 
+apply (blast dest: NSLIM_const_not_eq)
 done
 
-(* can actually be proved more easily by unfolding def! *)
+text{* can actually be proved more easily by unfolding the definition!*}
 lemma NSLIM_unique: "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M"
 apply (drule NSLIM_minus)
 apply (drule NSLIM_add, assumption)
@@ -428,10 +408,9 @@
 by (simp add: NSLIM_def)
 
 
-(*-----------------------------------------------------------------------------
-   Derivatives and Continuity - NS and Standard properties
- -----------------------------------------------------------------------------*)
-text{*Continuity*}
+subsection{* Derivatives and Continuity: NS and Standard properties*}
+
+subsubsection{*Continuity*}
 
 lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
 by (simp add: isNSCont_def)
@@ -444,38 +423,28 @@
 apply (rule_tac Q = "y = hypreal_of_real a" in excluded_middle [THEN disjE], auto)
 done
 
-(*-----------------------------------------------------
-    NS continuity can be defined using NS Limit in
-    similar fashion to standard def of continuity
- -----------------------------------------------------*)
+text{*NS continuity can be defined using NS Limit in
+    similar fashion to standard def of continuity*}
 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
 by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
 
-(*----------------------------------------------
-  Hence, NS continuity can be given
-  in terms of standard limit
- ---------------------------------------------*)
+text{*Hence, NS continuity can be given
+  in terms of standard limit*}
 lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
 by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
 
-(*-----------------------------------------------
-  Moreover, it's trivial now that NS continuity
-  is equivalent to standard continuity
- -----------------------------------------------*)
+text{*Moreover, it's trivial now that NS continuity
+  is equivalent to standard continuity*}
 lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
 apply (simp add: isCont_def)
 apply (rule isNSCont_LIM_iff)
 done
 
-(*----------------------------------------
-  Standard continuity ==> NS continuity
- ----------------------------------------*)
+text{*Standard continuity ==> NS continuity*}
 lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
 by (erule isNSCont_isCont_iff [THEN iffD2])
 
-(*----------------------------------------
-  NS continuity ==> Standard continuity
- ----------------------------------------*)
+text{*NS continuity ==> Standard continuity*}
 lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
 by (erule isNSCont_isCont_iff [THEN iffD1])
 
@@ -488,7 +457,7 @@
 apply (drule_tac [2] x = "-hypreal_of_real a + x" in spec, safe, simp)
 apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
 apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
- prefer 3 apply (simp add: add_commute) 
+ prefer 3 apply (simp add: add_commute)
 apply (rule_tac [2] z = x in eq_Abs_hypreal)
 apply (rule_tac [4] z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_of_real_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
@@ -503,24 +472,20 @@
 lemma isCont_iff: "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))"
 by (simp add: isCont_def LIM_isCont_iff)
 
-(*--------------------------------------------------------------------------
-   Immediate application of nonstandard criterion for continuity can offer
-   very simple proofs of some standard property of continuous functions
- --------------------------------------------------------------------------*)
+text{*Immediate application of nonstandard criterion for continuity can offer
+   very simple proofs of some standard property of continuous functions*}
 text{*sum continuous*}
 lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"
 by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
 
 text{*mult continuous*}
 lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
-by (auto intro!: starfun_mult_HFinite_approx 
-            simp del: starfun_mult [symmetric] 
+by (auto intro!: starfun_mult_HFinite_approx
+            simp del: starfun_mult [symmetric]
             simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
 
-(*-------------------------------------------
-     composition of continuous functions
-     Note very short straightforard proof!
- ------------------------------------------*)
+text{*composition of continuous functions
+     Note very short straightforard proof!*}
 lemma isCont_o: "[| isCont f a; isCont g (f a) |] ==> isCont (g o f) a"
 by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric])
 
@@ -548,23 +513,20 @@
 apply (auto intro: isCont_add isCont_minus)
 done
 
-lemma isCont_const: "isCont (%x. k) a"
+lemma isCont_const [simp]: "isCont (%x. k) a"
 by (simp add: isCont_def)
-declare isCont_const [simp]
 
-lemma isNSCont_const: "isNSCont (%x. k) a"
+lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
 by (simp add: isNSCont_def)
-declare isNSCont_const [simp]
 
-lemma isNSCont_rabs: "isNSCont abs a"
+lemma isNSCont_abs [simp]: "isNSCont abs a"
 apply (simp add: isNSCont_def)
 apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
 done
-declare isNSCont_rabs [simp]
 
-lemma isCont_rabs: "isCont abs a"
+lemma isCont_abs [simp]: "isCont abs a"
 by (auto simp add: isNSCont_isCont_iff [symmetric])
-declare isCont_rabs [simp]
+
 
 (****************************************************************
 (%* Leave as commented until I add topology theory or remove? *%)
@@ -656,14 +618,13 @@
 lemma lemma_simpu: "\<forall>n. \<bar>X n + -Y n\<bar> < inverse (real(Suc n)) &
           r \<le> abs (f (X n) + - f(Y n)) ==>
           \<forall>n. \<bar>X n + - Y n\<bar> < inverse (real(Suc n))"
-apply auto
-done
+by auto
 
 lemma isNSUCont_isUCont:
      "isNSUCont f ==> isUCont f"
 apply (simp add: isNSUCont_def isUCont_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule ccontr, simp) 
+apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2u, safe)
 apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
@@ -671,7 +632,6 @@
 apply (simp add: starfun hypreal_minus hypreal_add, auto)
 apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
-apply (rotate_tac 2)
 apply (drule_tac x = r in spec, clarify)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
@@ -687,10 +647,10 @@
 lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"
 by (simp add: deriv_def)
 
-lemma NS_DERIV_D: "DERIV f x :> D ==>
-           (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"
+lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"
 by (simp add: deriv_def LIM_NSLIM_iff)
 
+
 subsubsection{*Uniqueness*}
 
 lemma DERIV_unique:
@@ -703,8 +663,8 @@
      "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"
 apply (simp add: nsderiv_def)
 apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero)
-apply (auto dest!: bspec [where x=epsilon] 
-            intro!: inj_hypreal_of_real [THEN injD] 
+apply (auto dest!: bspec [where x=epsilon]
+            intro!: inj_hypreal_of_real [THEN injD]
             dest: approx_trans3)
 done
 
@@ -778,9 +738,9 @@
 
 subsection{*Equivalence of NS and standard definitions of differentiation*}
 
-text{*First NSDERIV in terms of NSLIM*}
+subsubsection{*First NSDERIV in terms of NSLIM*}
 
-(*--- first equivalence ---*)
+text{*first equivalence *}
 lemma NSDERIV_NSLIM_iff:
       "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"
 apply (simp add: nsderiv_def NSLIM_def, auto)
@@ -790,10 +750,10 @@
 apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
 done
 
-(*--- second equivalence ---*)
+text{*second equivalence *}
 lemma NSDERIV_NSLIM_iff2:
      "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
-by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric] 
+by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric]
               LIM_NSLIM_iff [symmetric])
 
 (* while we're at it! *)
@@ -853,16 +813,14 @@
 lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
 by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
 
-(*---------------------------------------------------
-         Differentiability implies continuity
-         nice and simple "algebraic" proof
- --------------------------------------------------*)
+text{*Differentiability implies continuity
+         nice and simple "algebraic" proof*}
 lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
 apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
 apply (drule approx_minus_iff [THEN iffD1])
 apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
 apply (drule_tac x = "-hypreal_of_real x + xa" in bspec)
- prefer 2 apply (simp add: add_assoc [symmetric]) 
+ prefer 2 apply (simp add: add_assoc [symmetric])
 apply (auto simp add: mem_infmal_iff [symmetric] hypreal_add_commute)
 apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
@@ -870,35 +828,29 @@
 apply (drule_tac x3=D in
            HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
              THEN mem_infmal_iff [THEN iffD1]])
-apply (auto simp add: mult_commute 
+apply (auto simp add: mult_commute
             intro: approx_trans approx_minus_iff [THEN iffD2])
 done
 
 text{*Now Sandard proof*}
 lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x"
-by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric] 
+by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
               NSDERIV_isNSCont)
 
 
-(*----------------------------------------------------------------------------
-      Differentiation rules for combinations of functions
+text{*Differentiation rules for combinations of functions
       follow from clear, straightforard, algebraic
-      manipulations
- ----------------------------------------------------------------------------*)
+      manipulations*}
 text{*Constant function*}
 
 (* use simple constant nslimit theorem *)
-lemma NSDERIV_const: "(NSDERIV (%x. k) x :> 0)"
+lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)"
 by (simp add: NSDERIV_NSLIM_iff)
-declare NSDERIV_const [simp]
 
-lemma DERIV_const: "(DERIV (%x. k) x :> 0)"
+lemma DERIV_const [simp]: "(DERIV (%x. k) x :> 0)"
 by (simp add: NSDERIV_DERIV_iff [symmetric])
-declare DERIV_const [simp]
 
-(*-----------------------------------------------------
-    Sum of functions- proved easily
- ----------------------------------------------------*)
+text{*Sum of functions- proved easily*}
 
 
 lemma NSDERIV_add: "[| NSDERIV f x :> Da;  NSDERIV g x :> Db |]
@@ -915,10 +867,8 @@
 apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric])
 done
 
-(*-----------------------------------------------------
-  Product of functions - Proof is trivial but tedious
-  and long due to rearrangement of terms
- ----------------------------------------------------*)
+text{*Product of functions - Proof is trivial but tedious
+  and long due to rearrangement of terms*}
 
 lemma lemma_nsderiv1: "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"
 by (simp add: right_distrib)
@@ -944,27 +894,27 @@
 apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
 apply (drule_tac D = Db in lemma_nsderiv2)
 apply (drule_tac [4]
-     approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) 
-apply (auto intro!: approx_add_mono1 
+     approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
+apply (auto intro!: approx_add_mono1
             simp add: left_distrib right_distrib mult_commute add_assoc)
-apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)" 
+apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)"
          in add_commute [THEN subst])
-apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] 
-                    Infinitesimal_add Infinitesimal_mult 
-                    Infinitesimal_hypreal_of_real_mult 
+apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
+                    Infinitesimal_add Infinitesimal_mult
+                    Infinitesimal_hypreal_of_real_mult
                     Infinitesimal_hypreal_of_real_mult2
           simp add: add_assoc [symmetric])
 done
 
 lemma DERIV_mult:
-     "[| DERIV f x :> Da; DERIV g x :> Db |] 
+     "[| DERIV f x :> Da; DERIV g x :> Db |]
       ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
 by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
 
 text{*Multiplying by a constant*}
 lemma NSDERIV_cmult: "NSDERIV f x :> D
       ==> NSDERIV (%x. c * f x) x :> c*D"
-apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 
+apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
                   minus_mult_right right_distrib [symmetric])
 apply (erule NSLIM_const [THEN NSLIM_mult])
 done
@@ -974,7 +924,7 @@
 
 lemma DERIV_cmult:
       "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
-apply (simp only: deriv_def times_divide_eq_right [symmetric] 
+apply (simp only: deriv_def times_divide_eq_right [symmetric]
                   NSDERIV_NSLIM_iff minus_mult_right right_distrib [symmetric])
 apply (erule LIM_const [THEN LIM_mult2])
 done
@@ -983,10 +933,10 @@
 lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
 proof (simp add: NSDERIV_NSLIM_iff)
   assume "(\<lambda>h. (f (x + h) + - f x) / h) -- 0 --NS> D"
-  hence deriv: "(\<lambda>h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D" 
+  hence deriv: "(\<lambda>h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D"
     by (rule NSLIM_minus)
   have "\<forall>h. - ((f (x + h) + - f x) / h) = (- f (x + h) + f x) / h"
-    by (simp add: minus_divide_left) 
+    by (simp add: minus_divide_left)
   with deriv
   show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
 qed
@@ -1016,9 +966,7 @@
 apply (blast intro: DERIV_add_minus)
 done
 
-(*---------------------------------------------------------------
-                     (NS) Increment
- ---------------------------------------------------------------*)
+text{*(NS) Increment*}
 lemma incrementI:
       "f NSdifferentiable x ==>
       increment f x h = ( *f* f) (hypreal_of_real(x) + h) +
@@ -1036,15 +984,15 @@
       ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
 apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
 apply (drule bspec, auto)
-apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) 
-apply (frule_tac b1 = "hypreal_of_real (D) + y" 
+apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
+apply (frule_tac b1 = "hypreal_of_real (D) + y"
         in hypreal_mult_right_cancel [THEN iffD2])
 apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
 apply assumption
 apply (simp add: times_divide_eq_right [symmetric] del: times_divide_eq_right)
 apply (auto simp add: left_distrib)
 done
- 
+
 lemma increment_thm2:
      "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
       ==> \<exists>e \<in> Infinitesimal. increment f x h =
@@ -1054,7 +1002,7 @@
 
 lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
       ==> increment f x h \<approx> 0"
-apply (drule increment_thm2, 
+apply (drule increment_thm2,
        auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
 apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
 done
@@ -1119,9 +1067,7 @@
 lemma lemma_chain: "(z::hypreal) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
 by auto
 
-(*------------------------------------------------------
-  This proof uses both definitions of differentiability.
- ------------------------------------------------------*)
+text{*This proof uses both definitions of differentiability.*}
 lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
       ==> NSDERIV (f o g) x :> Da * Db"
 apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
@@ -1148,25 +1094,21 @@
 by (auto dest: DERIV_chain simp add: o_def)
 
 text{*Differentiation of natural number powers*}
-lemma NSDERIV_Id: "NSDERIV (%x. x) x :> 1"
-by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def starfun_Id)
-declare NSDERIV_Id [simp]
+lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
+by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if)
 
 (*derivative of the identity function*)
-lemma DERIV_Id: "DERIV (%x. x) x :> 1"
+lemma DERIV_Id [simp]: "DERIV (%x. x) x :> 1"
 by (simp add: NSDERIV_DERIV_iff [symmetric])
-declare DERIV_Id [simp]
 
 lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
 
 (*derivative of linear multiplication*)
-lemma DERIV_cmult_Id: "DERIV (op * c) x :> c"
+lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
 by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
-declare DERIV_cmult_Id [simp]
 
-lemma NSDERIV_cmult_Id: "NSDERIV (op * c) x :> c"
+lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
 by (simp add: NSDERIV_DERIV_iff)
-declare NSDERIV_cmult_Id [simp]
 
 lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
 apply (induct_tac "n")
@@ -1181,28 +1123,26 @@
 lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
 by (simp add: NSDERIV_DERIV_iff DERIV_pow)
 
-(*---------------------------------------------------------------
-                    Power of -1
- ---------------------------------------------------------------*)
+text{*Power of -1*}
 
 (*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
 lemma NSDERIV_inverse:
      "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
 apply (simp add: nsderiv_def)
-apply (rule ballI, simp, clarify) 
+apply (rule ballI, simp, clarify)
 apply (frule Infinitesimal_add_not_zero)
-prefer 2 apply (simp add: add_commute) 
-apply (auto simp add: starfun_inverse_inverse realpow_two 
+prefer 2 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 inverse_mult_distrib [symmetric]
               inverse_minus_eq [symmetric] add_ac mult_ac
-            del: inverse_mult_distrib inverse_minus_eq 
+            del: inverse_mult_distrib inverse_minus_eq
                  minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
             del: minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (rule_tac y = " inverse (- hypreal_of_real x * hypreal_of_real x) " in approx_trans)
 apply (rule inverse_add_Infinitesimal_approx2)
-apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal 
+apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
             simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
 apply (rule Infinitesimal_HFinite_mult2, auto)
 done
@@ -1232,7 +1172,7 @@
 apply (drule_tac [2] DERIV_mult)
 apply (assumption+)
 apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
-                 mult_ac 
+                 mult_ac
      del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
 done
 
@@ -1255,17 +1195,17 @@
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
-    show "isCont ?g x" using der 
-      by (simp add: isCont_iff DERIV_iff diff_minus 
+    show "isCont ?g x" using der
+      by (simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
     show "?g x = l" by simp
   qed
 next
   assume "?rhs"
-  then obtain g where 
+  then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
-  thus "(DERIV f x :> l)" 
-     by (auto simp add: isCont_iff DERIV_iff diff_minus 
+  thus "(DERIV f x :> l)"
+     by (auto simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
 qed
 
@@ -1285,10 +1225,10 @@
   from nsc
   have "\<forall>w. w \<noteq> hypreal_of_real x \<and> w \<approx> hypreal_of_real x \<longrightarrow>
          ( *f* g) w * (w - hypreal_of_real x) / (w - hypreal_of_real x) \<approx>
-         hypreal_of_real (g x)" 
+         hypreal_of_real (g x)"
     by (simp add: diff_minus isNSCont_def)
   thus ?thesis using all
-    by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) 
+    by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
 qed
 
 (*--------------------------------------------------------------------------*)
@@ -1428,9 +1368,9 @@
  next
   case (Suc n)
   thus ?case
- by (auto simp del: surjective_pairing [symmetric] 
-             simp add: Let_def split_def Bolzano_bisect_le [OF le] 
-     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"]) 
+ by (auto simp del: surjective_pairing [symmetric]
+             simp add: Let_def split_def Bolzano_bisect_le [OF le]
+     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"])
 qed
 
 (*Now we re-package P_prem as a formula*)
@@ -1458,7 +1398,7 @@
 apply (simp add: LIMSEQ_def)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
-apply (drule real_less_half_sum, auto) 
+apply (drule real_less_half_sum, auto)
 apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec)
 apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
 apply safe
@@ -1494,7 +1434,7 @@
 apply (rule ccontr)
 apply (subgoal_tac "a \<le> x & x \<le> b")
  prefer 2
- apply simp 
+ apply simp
  apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
 apply (drule_tac x = x in spec)+
 apply simp
@@ -1513,7 +1453,7 @@
          a \<le> b;
          (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
       |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
-apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify) 
+apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
 apply (drule IVT [where f = "%x. - f x"], assumption)
 apply (auto intro: isCont_minus)
 done
@@ -1578,7 +1518,7 @@
 apply (drule isCont_bounded, assumption)
 apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
 apply (rule exI, auto)
-apply (auto dest!: spec simp add: linorder_not_less) 
+apply (auto dest!: spec simp add: linorder_not_less)
 done
 
 (*----------------------------------------------------------------------------*)
@@ -1597,7 +1537,7 @@
   show ?thesis
   proof (intro exI, intro conjI)
     show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
-    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M" 
+    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M"
     proof (rule ccontr)
       assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
       with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
@@ -1607,15 +1547,15 @@
       from isCont_bounded [OF le this]
       obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
       have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
-        by (simp add: M3 compare_rls) 
-      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k 
-        by (auto intro: order_le_less_trans [of _ k]) 
-      with Minv 
-      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))" 
+        by (simp add: M3 compare_rls)
+      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
+        by (auto intro: order_le_less_trans [of _ k])
+      with Minv
+      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))"
         by (intro strip less_imp_inverse_less, simp_all)
-      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x" 
+      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x"
         by simp
-      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le 
+      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le
         by (simp, arith)
       from M2 [OF this]
       obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
@@ -1673,7 +1613,7 @@
               (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
     by (simp add: diff_minus)
   then obtain s
-        where s:   "0 < s" 
+        where s:   "0 < s"
           and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
     by auto
   thus ?thesis
@@ -1681,11 +1621,11 @@
     show "0<s" .
     fix h::real
     assume "0 < h \<and> h < s"
-    with all [of h] show "f x < f (x+h)" 
-    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 
+    with all [of h] show "f x < f (x+h)"
+    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
-      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" 
-      with l 
+      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
+      with l
       have "0 < (f (x+h) - f x) / h" by arith
       thus "f x < f (x+h)"
 	by (simp add: pos_less_divide_eq h)
@@ -1703,7 +1643,7 @@
               (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
     by (simp add: diff_minus)
   then obtain s
-        where s:   "0 < s" 
+        where s:   "0 < s"
           and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
     by auto
   thus ?thesis
@@ -1711,11 +1651,11 @@
     show "0<s" .
     fix h::real
     assume "0 < h \<and> h < s"
-    with all [of "-h"] show "f x < f (x-h)" 
-    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 
+    with all [of "-h"] show "f x < f (x-h)"
+    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
-      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" 
-      with l 
+      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
+      with l
       have "0 < (f (x-h) - f x) / h" by arith
       thus "f x < f (x-h)"
 	by (simp add: pos_less_divide_eq h)
@@ -1723,7 +1663,7 @@
   qed
 qed
 
-lemma DERIV_local_max: 
+lemma DERIV_local_max:
   assumes der: "DERIV f x :> l"
       and d:   "0 < d"
       and le:  "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
@@ -1737,7 +1677,7 @@
              and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
   from real_lbound_gt_zero [OF d d']
   obtain e where "0 < e \<and> e < d \<and> e < d'" ..
-  with lt le [THEN spec [where x="x-e"]] 
+  with lt le [THEN spec [where x="x-e"]]
   show ?thesis by (auto simp add: abs_if)
 next
   case greater
@@ -1764,7 +1704,7 @@
 
 text{*Lemma about introducing open ball in open interval*}
 lemma lemma_interval_lt:
-     "[| a < x;  x < b |] 
+     "[| a < x;  x < b |]
       ==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
 apply (simp add: abs_interval_iff)
 apply (insert linorder_linear [of "x-a" "b-x"], safe)
@@ -1779,11 +1719,11 @@
 done
 
 text{*Rolle's Theorem.
-   If @{term f} is defined and continuous on the closed interval 
-   @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, 
+   If @{term f} is defined and continuous on the closed interval
+   @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"},
    and @{term "f(a) = f(b)"},
    then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}*}
-theorem Rolle: 
+theorem Rolle:
   assumes lt: "a < b"
       and eq: "f(a) = f(b)"
       and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
@@ -1792,12 +1732,12 @@
 proof -
   have le: "a \<le> b" using lt by simp
   from isCont_eq_Ub [OF le con]
-  obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" 
-             and alex: "a \<le> x" and xleb: "x \<le> b" 
+  obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x"
+             and alex: "a \<le> x" and xleb: "x \<le> b"
     by blast
   from isCont_eq_Lb [OF le con]
-  obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" 
-              and alex': "a \<le> x'" and x'leb: "x' \<le> b" 
+  obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z"
+              and alex': "a \<le> x'" and x'leb: "x' \<le> b"
     by blast
   show ?thesis
   proof cases
@@ -1811,13 +1751,13 @@
       by blast
     from differentiableD [OF dif [OF axb]]
     obtain l where der: "DERIV f x :> l" ..
-    have "l=0" by (rule DERIV_local_max [OF der d bound']) 
+    have "l=0" by (rule DERIV_local_max [OF der d bound'])
         --{*the derivative at a local maximum is zero*}
     thus ?thesis using ax xb der by auto
   next
     assume notaxb: "~ (a < x & x < b)"
     hence xeqab: "x=a | x=b" using alex xleb by arith
-    hence fb_eq_fx: "f b = f x" by (auto simp add: eq) 
+    hence fb_eq_fx: "f b = f x" by (auto simp add: eq)
     show ?thesis
     proof cases
       assume ax'b: "a < x' & x' < b"
@@ -1830,21 +1770,21 @@
 	by blast
       from differentiableD [OF dif [OF ax'b]]
       obtain l where der: "DERIV f x' :> l" ..
-      have "l=0" by (rule DERIV_local_min [OF der d bound']) 
+      have "l=0" by (rule DERIV_local_min [OF der d bound'])
         --{*the derivative at a local minimum is zero*}
       thus ?thesis using ax' x'b der by auto
     next
       assume notax'b: "~ (a < x' & x' < b)"
         --{*@{term f} is constant througout the interval*}
       hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith
-      hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) 
+      hence fb_eq_fx': "f b = f x'" by (auto simp add: eq)
       from dense [OF lt]
       obtain r where ar: "a < r" and rb: "r < b" by blast
       from lemma_interval [OF ar rb]
       obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
 	by blast
-      have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b" 
-      proof (clarify) 
+      have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b"
+      proof (clarify)
         fix z::real
         assume az: "a \<le> z" and zb: "z \<le> b"
         show "f z = f b"
@@ -1857,12 +1797,12 @@
       proof (intro strip)
         fix y::real
         assume lt: "\<bar>r-y\<bar> < d"
-        hence "f y = f b" by (simp add: eq_fb bound) 
+        hence "f y = f b" by (simp add: eq_fb bound)
         thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le)
       qed
       from differentiableD [OF dif [OF conjI [OF ar rb]]]
       obtain l where der: "DERIV f r :> l" ..
-      have "l=0" by (rule DERIV_local_const [OF der d bound']) 
+      have "l=0" by (rule DERIV_local_const [OF der d bound'])
         --{*the derivative of a constant function is zero*}
       thus ?thesis using ar rb der by auto
     qed
@@ -1877,14 +1817,14 @@
 proof cases
   assume "a=b" thus ?thesis by simp
 next
-  assume "a\<noteq>b" 
+  assume "a\<noteq>b"
   hence ba: "b-a \<noteq> 0" by arith
   show ?thesis
     by (rule real_mult_left_cancel [OF ba, THEN iffD1],
         simp add: right_diff_distrib, simp add: left_diff_distrib)
 qed
 
-theorem MVT: 
+theorem MVT:
   assumes lt:  "a < b"
       and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
       and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
@@ -1893,7 +1833,7 @@
 proof -
   let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
   have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
-    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id) 
+    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id)
   have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
   proof (clarify)
     fix x::real
@@ -1902,17 +1842,17 @@
     obtain l where der: "DERIV f x :> l" ..
     show "?F differentiable x"
       by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
-          blast intro: DERIV_diff DERIV_cmult_Id der) 
-  qed  
+          blast intro: DERIV_diff DERIV_cmult_Id der)
+  qed
   from Rolle [where f = ?F, OF lt lemma_MVT contF difF]
-  obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0" 
+  obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0"
     by blast
   have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)"
     by (rule DERIV_cmult_Id)
-  hence derF: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z 
+  hence derF: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z
                    :> 0 + (f b - f a) / (b - a)"
     by (rule DERIV_add [OF der])
-  show ?thesis  
+  show ?thesis
   proof (intro exI conjI)
     show "a < z" .
     show "z < b" .
@@ -1969,13 +1909,11 @@
 apply (auto dest!: DERIV_const_ratio_const simp add: real_mult_assoc)
 done
 
-lemma real_average_minus_first: "((a + b) /2 - a) = (b-a)/(2::real)"
+lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
 by auto
-declare real_average_minus_first [simp]
 
-lemma real_average_minus_second: "((b + a)/2 - a) = (b-a)/(2::real)"
+lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
 by auto
-declare real_average_minus_second [simp]
 
 text{*Gallileo's "trick": average velocity = av. of end velocities*}
 
@@ -1989,7 +1927,7 @@
   case less
   have "(v b - v a) / (b - a) = k"
     by (rule DERIV_const_ratio_const2 [OF neq der])
-  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp 
+  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
   moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k"
     by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
   ultimately show ?thesis using neq by force
@@ -1997,10 +1935,10 @@
   case greater
   have "(v b - v a) / (b - a) = k"
     by (rule DERIV_const_ratio_const2 [OF neq der])
-  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp 
+  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
   moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k"
     by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
-  ultimately show ?thesis using neq by (force simp add: add_commute) 
+  ultimately show ?thesis using neq by (force simp add: add_commute)
 qed
 
 
@@ -2014,14 +1952,14 @@
   shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
 proof (rule ccontr)
   assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
-  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto 
+  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
   show False
   proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
     case le
     from d cont all [of "x+d"]
-    have flef: "f(x+d) \<le> f x" 
-     and xlex: "x - d \<le> x" 
-     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z" 
+    have flef: "f(x+d) \<le> f x"
+     and xlex: "x - d \<le> x"
+     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
        by (auto simp add: abs_if)
     from IVT [OF le flef xlex cont']
     obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
@@ -2032,9 +1970,9 @@
   next
     case ge
     from d cont all [of "x-d"]
-    have flef: "f(x-d) \<le> f x" 
-     and xlex: "x \<le> x+d" 
-     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" 
+    have flef: "f(x-d) \<le> f x"
+     and xlex: "x \<le> x+d"
+     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
        by (auto simp add: abs_if)
     from IVT2 [OF ge flef xlex cont']
     obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
@@ -2054,13 +1992,13 @@
       ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
 apply (insert lemma_isCont_inj
           [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
-apply (simp add: isCont_minus linorder_not_le) 
+apply (simp add: isCont_minus linorder_not_le)
 done
 
-text{*Show there's an interval surrounding @{term "f(x)"} in 
+text{*Show there's an interval surrounding @{term "f(x)"} in
 @{text "f[[x - d, x + d]]"} .*}
 
-lemma isCont_inj_range: 
+lemma isCont_inj_range:
   assumes d: "0 < d"
       and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
@@ -2069,7 +2007,7 @@
   have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
     by (auto simp add: abs_le_interval_iff)
   from isCont_Lb_Ub [OF this]
-  obtain L M 
+  obtain L M
   where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
     and all2 [rule_format]:
            "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
@@ -2101,7 +2039,7 @@
       with e have "L \<le> y \<and> y \<le> M" by arith
       from all2 [OF this]
       obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
-      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
+      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
         by (force simp add: abs_le_interval_iff)
     qed
   qed
@@ -2124,10 +2062,10 @@
     from real_lbound_gt_zero [OF r d]
     obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
     with inj cont
-    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z" 
+    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
                   "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
     from isCont_inj_range [OF e this]
-    obtain e' where e': "0 < e'" 
+    obtain e' where e': "0 < e'"
         and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
           by blast
     show "\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
@@ -2142,7 +2080,7 @@
       qed
     qed
   qed
-qed  
+qed
 
 ML
 {*
@@ -2225,8 +2163,6 @@
 val isCont_diff = thm "isCont_diff";
 val isCont_const = thm "isCont_const";
 val isNSCont_const = thm "isNSCont_const";
-val isNSCont_rabs = thm "isNSCont_rabs";
-val isCont_rabs = thm "isCont_rabs";
 val isNSUContD = thm "isNSUContD";
 val isUCont_isCont = thm "isUCont_isCont";
 val isUCont_isNSUCont = thm "isUCont_isNSUCont";
diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -171,6 +171,9 @@
 lemma real_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> sqrt(x)"
 by (auto intro: real_sqrt_gt_zero simp add: order_le_less)
 
+lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
+by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) 
+
 
 (*we need to prove something like this:
 lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r"
@@ -920,13 +923,13 @@
   hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
     by (auto simp add: exp_add exp_minus)
   thus ?thesis
-    by (simp add: divide_inverse [symmetric] pos_less_divide_eq)
+    by (simp add: divide_inverse [symmetric] pos_less_divide_eq 
+             del: divide_self_if)
 qed
 
 lemma exp_less_cancel: "exp x < exp y ==> x < y"
-apply (rule ccontr) 
-apply (simp add: linorder_not_less order_le_less) 
-apply (auto dest: exp_less_mono)
+apply (simp add: linorder_not_le [symmetric]) 
+apply (auto simp add: order_le_less exp_less_mono) 
 done
 
 lemma exp_less_cancel_iff [iff]: "(exp(x) < exp(y)) = (x < y)"
@@ -2183,20 +2186,23 @@
 
 subsection{*Theorems About Sqrt, Transcendental Functions for Complex*}
 
-lemma lemma_real_divide_sqrt: 
-    "0 < x ==> 0 \<le> x/(sqrt (x * x + y * y))"
-apply (unfold real_divide_def)
-apply (rule real_mult_order [THEN order_less_imp_le], assumption)
-apply (subgoal_tac "0 < inverse (sqrt (x\<twosuperior> + y\<twosuperior>))") 
- apply (simp add: numeral_2_eq_2)
-apply (simp add: real_sqrt_sum_squares_ge1 [THEN [2] order_less_le_trans]) 
-done
+lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
+proof (rule order_trans)
+  show "x \<le> sqrt(x*x)" by (simp add: abs_if) 
+  show "sqrt (x * x) \<le> sqrt (x * x + y * y)"
+    by (rule real_sqrt_le_mono, auto) 
+qed
+
+lemma minus_le_real_sqrt_sumsq [simp]: "-x \<le> sqrt (x * x + y * y)"
+proof (rule order_trans)
+  show "-x \<le> sqrt(x*x)" by (simp add: abs_if) 
+  show "sqrt (x * x) \<le> sqrt (x * x + y * y)"
+    by (rule real_sqrt_le_mono, auto) 
+qed
 
 lemma lemma_real_divide_sqrt_ge_minus_one:
-     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
-apply (rule real_le_trans)
-apply (rule_tac [2] lemma_real_divide_sqrt, auto)
-done
+     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))" 
+by (simp add: divide_const_simps linorder_not_le [symmetric])
 
 lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)"
 apply (rule real_sqrt_gt_zero)
@@ -2233,36 +2239,32 @@
 
 lemma lemma_real_divide_sqrt_ge_minus_one2:
      "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
-apply (case_tac "y = 0", auto)
-apply (frule abs_minus_eqI2)
-apply (auto simp add: inverse_minus_eq)
-apply (rule order_less_imp_le)
-apply (rule_tac z1 = "sqrt (x * x + y * y) " in real_mult_less_iff1 [THEN iffD1])
-apply (frule_tac [2] y2 = y in
-       real_sqrt_sum_squares_gt_zero1 [THEN real_not_refl2, THEN not_sym])
-apply (auto intro: real_sqrt_sum_squares_gt_zero1 simp add: mult_ac)
-apply (cut_tac x = "-x" and y = y in real_sqrt_sum_squares_ge1)
-apply (drule order_le_less [THEN iffD1], safe) 
-apply (simp add: numeral_2_eq_2)
-apply (drule sym [THEN real_sqrt_sum_squares_eq_cancel], simp)
+apply (simp add: divide_const_simps); 
+apply (insert minus_le_real_sqrt_sumsq [of x y])
+apply arith;
 done
 
 lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1"
 by (cut_tac x = "-x" and y = y in lemma_real_divide_sqrt_ge_minus_one2, auto)
 
+lemma minus_sqrt_le: "- sqrt (x * x + y * y) \<le> x"
+by (insert minus_le_real_sqrt_sumsq [of x y], arith) 
+
+lemma minus_sqrt_le2: "- sqrt (x * x + y * y) \<le> y"
+by (subst add_commute, simp add: minus_sqrt_le) 
+
+lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
+by (simp add: linorder_not_less)
 
 lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
-apply (cut_tac x = x and y = 0 in linorder_less_linear, safe)
-apply (rule lemma_real_divide_sqrt_ge_minus_one2)
-apply (rule_tac [3] lemma_real_divide_sqrt_ge_minus_one, auto)
+apply (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps); 
 done
 
 lemma cos_x_y_ge_minus_one1a [simp]: "-1 \<le> y / sqrt (x * x + y * y)"
-apply (cut_tac x = y and y = x in cos_x_y_ge_minus_one)
-apply (simp add: real_add_commute)
+apply (subst add_commute, simp add: cos_x_y_ge_minus_one); 
 done
 
-lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1"
+lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1" 
 apply (cut_tac x = x and y = 0 in linorder_less_linear, safe)
 apply (rule lemma_real_divide_sqrt_le_one)
 apply (rule_tac [3] lemma_real_divide_sqrt_le_one2, auto)
@@ -2281,23 +2283,19 @@
 
 lemma cos_abs_x_y_ge_minus_one [simp]:
      "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
-apply (cut_tac x = x and y = 0 in linorder_less_linear)
-apply (auto simp add: abs_minus_eqI2 abs_eqI2)
-apply (drule lemma_real_divide_sqrt_ge_minus_one, force)
-done
+by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]) 
 
 lemma cos_abs_x_y_le_one [simp]: "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1"
-apply (cut_tac x = x and y = 0 in linorder_less_linear)
-apply (auto simp add: abs_minus_eqI2 abs_eqI2)
-apply (drule lemma_real_divide_sqrt_ge_minus_one2, force)
+apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y]) 
+apply (auto simp add: divide_const_simps abs_if linorder_neq_iff) 
 done
 
 declare cos_arcos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
 declare arcos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
 
 lemma minus_pi_less_zero: "-pi < 0"
-apply (simp (no_asm))
-done
+by simp
+
 declare minus_pi_less_zero [simp]
 declare minus_pi_less_zero [THEN order_less_imp_le, simp]
 
@@ -2404,15 +2402,15 @@
 
 lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
-apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
-apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
+apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
+apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI) 
 apply (auto dest: real_sum_squares_cancel2a 
             simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)
 apply (unfold arcsin_def)
 apply (cut_tac x1 = x and y1 = y 
        in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
 apply (rule someI2_ex, blast)
-apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)
+apply (erule_tac V = "EX! v. ?P v" in thin_rl)
 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast)
 apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff)
 apply (drule cos_ge_zero, force)
@@ -2459,7 +2457,6 @@
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
 apply (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
-apply (rule_tac z1 = "sqrt 2" in real_mult_less_iff1 [THEN iffD1], auto)
 done
 
 lemma four_x_squared: 
diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -215,6 +215,95 @@
 declare divide_eq_eq [of _ "number_of w", standard, simp]
 
 
+subsection{*Optional Simplification Rules Involving Constants*}
+
+text{*Simplify quotients that are compared with a literal constant.*}
+
+lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
+lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
+lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
+lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
+lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
+lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
+
+text{*Simplify quotients that are compared with the value 1.*}
+
+lemma le_divide_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
+by (auto simp add: le_divide_eq)
+
+lemma divide_le_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
+by (auto simp add: divide_le_eq)
+
+lemma less_divide_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
+by (auto simp add: less_divide_eq)
+
+lemma divide_less_eq_1:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
+by (auto simp add: divide_less_eq)
+
+
+text{*Not good as automatic simprules because they cause case splits.*}
+lemmas divide_const_simps =
+  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
+  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
+  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
+
+
+subsection{*Conditional Simplification Rules: No Case Splits*}
+
+lemma le_divide_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
+by (auto simp add: le_divide_eq)
+
+lemma le_divide_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
+by (auto simp add: le_divide_eq)
+
+lemma divide_le_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
+by (auto simp add: divide_le_eq)
+
+lemma divide_le_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
+by (auto simp add: divide_le_eq)
+
+lemma less_divide_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
+by (auto simp add: less_divide_eq)
+
+lemma less_divide_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
+by (auto simp add: less_divide_eq)
+
+lemma divide_less_eq_1_pos [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
+by (auto simp add: divide_less_eq)
+
+lemma eq_divide_eq_1 [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
+by (auto simp add: eq_divide_eq)
+
+lemma divide_eq_eq_1 [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
+by (auto simp add: divide_eq_eq)
+
+
 subsubsection{*Division By @{term "-1"}*}
 
 lemma divide_minus1 [simp]:
diff -r 804ecdc08cf2 -r 4d332d10fa3d src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:28:03 2004 +0200
@@ -580,12 +580,16 @@
 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
 by (simp add: divide_inverse)
 
-lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
+lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   by (simp add: divide_inverse)
 
 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
 by (simp add: divide_inverse)
 
+lemma divide_self_if [simp]:
+     "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
+  by (simp add: divide_self)
+
 lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
 by (simp add: divide_inverse)