new simprules for abs and for things like a/b<1
authorpaulson
Tue Oct 05 15:30:50 2004 +0200 (2004-10-05)
changeset 152291eb23f805c06
parent 15228 4d332d10fa3d
child 15230 315079a40f31
new simprules for abs and for things like a/b<1
src/HOL/Complex/NSCA.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/OrderedGroup.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Complex/NSCA.thy	Mon Oct 04 15:28:03 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Tue Oct 05 15:30:50 2004 +0200
     1.3 @@ -673,7 +673,7 @@
     1.4             simp del: realpow_Suc)
     1.5  apply (rule_tac y="abs(Z x)" in order_le_less_trans)
     1.6  apply (drule_tac t = "Z x" in sym)
     1.7 -apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
     1.8 +apply (auto simp del: realpow_Suc)
     1.9  done
    1.10  
    1.11  (* same proof *)
    1.12 @@ -691,7 +691,7 @@
    1.13  apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
    1.14  apply (rule_tac y="abs(Z x)" in order_le_less_trans)
    1.15  apply (drule_tac t = "Z x" in sym)
    1.16 -apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
    1.17 +apply (auto simp del: realpow_Suc)
    1.18  done
    1.19  
    1.20  lemma hcomplex_capproxI:
     2.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Oct 04 15:28:03 2004 +0200
     2.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Tue Oct 05 15:30:50 2004 +0200
     2.3 @@ -458,17 +458,12 @@
     2.4  
     2.5  lemma starfun_ln_Infinitesimal_less_zero:
     2.6       "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
     2.7 -apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
     2.8 -apply (drule bspec [where x = 1])
     2.9 -apply (auto simp add: abs_if)
    2.10 -done
    2.11 +by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
    2.12  
    2.13  lemma starfun_ln_HInfinite_gt_zero:
    2.14       "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
    2.15 -apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
    2.16 -apply (drule bspec [where x = 1])
    2.17 -apply (auto simp add: abs_if)
    2.18 -done
    2.19 +by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
    2.20 +
    2.21  
    2.22  (*
    2.23  Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Oct 04 15:28:03 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Oct 05 15:30:50 2004 +0200
     3.3 @@ -623,20 +623,12 @@
     3.4       "abs (Abs_hypreal (hyprel `` {X})) = 
     3.5        Abs_hypreal(hyprel `` {%n. abs (X n)})"
     3.6  apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
     3.7 -apply (ultra, arith)+
     3.8 +apply ultra
     3.9 +apply ultra
    3.10 +apply arith
    3.11  done
    3.12  
    3.13  
    3.14 -
    3.15 -lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
    3.16 -by (auto dest: add_less_le_mono)
    3.17 -
    3.18 -text{*The precondition could be weakened to @{term "0\<le>x"}*}
    3.19 -lemma hypreal_mult_less_mono:
    3.20 -     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
    3.21 - by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
    3.22 -
    3.23 -
    3.24  subsection{*Existence of Infinite Hyperreal Number*}
    3.25  
    3.26  lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
    3.27 @@ -784,7 +776,6 @@
    3.28  val hypreal_one_num = thm "hypreal_one_num";
    3.29  val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
    3.30  
    3.31 -val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono";
    3.32  val Rep_hypreal_omega = thm"Rep_hypreal_omega";
    3.33  val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
    3.34  val lemma_finite_omega_set = thm"lemma_finite_omega_set";
     4.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Mon Oct 04 15:28:03 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Tue Oct 05 15:30:50 2004 +0200
     4.3 @@ -216,6 +216,11 @@
     4.4  lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1)  = x pow (1 + 1)"
     4.5  by (simp add: hyperpow_hrabs)
     4.6  
     4.7 +text{*The precondition could be weakened to @{term "0\<le>x"}*}
     4.8 +lemma hypreal_mult_less_mono:
     4.9 +     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
    4.10 + by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
    4.11 +
    4.12  lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)"
    4.13  apply (auto simp add: hyperpow_two)
    4.14  apply (rule_tac y = "1*1" in order_le_less_trans)
     5.1 --- a/src/HOL/Hyperreal/Integration.thy	Mon Oct 04 15:28:03 2004 +0200
     5.2 +++ b/src/HOL/Hyperreal/Integration.thy	Tue Oct 05 15:30:50 2004 +0200
     5.3 @@ -430,9 +430,9 @@
     5.4  apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
     5.5  apply (rule add_mono)
     5.6  apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
     5.7 - prefer 2 apply (simp, arith)
     5.8 + prefer 2 apply simp
     5.9  apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
    5.10 -apply (drule_tac x = v in spec, simp, arith)
    5.11 +apply (drule_tac x = v in spec, simp)
    5.12  apply (drule_tac x = u in spec, auto, arith)
    5.13  apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
    5.14  apply (rule order_trans)
     6.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Oct 04 15:28:03 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 05 15:30:50 2004 +0200
     6.3 @@ -328,7 +328,7 @@
     6.4  prefer 2 apply blast
     6.5  apply (drule_tac [2] diff=diff in Maclaurin)
     6.6  apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
     6.7 -apply (rule_tac [!] x = t in exI, auto, arith+)
     6.8 +apply (rule_tac [!] x = t in exI, auto)
     6.9  done
    6.10  
    6.11  lemma Maclaurin_all_lt_objl:
     7.1 --- a/src/HOL/Hyperreal/NSA.thy	Mon Oct 04 15:28:03 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Oct 05 15:30:50 2004 +0200
     7.3 @@ -22,12 +22,12 @@
     7.4    HInfinite :: "hypreal set"
     7.5     "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
     7.6  
     7.7 -  (* infinitely close *)
     7.8    approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
     7.9 +    --{*the `infinitely close' relation*}
    7.10     "x @= y       == (x + -y) \<in> Infinitesimal"
    7.11  
    7.12 -  (* standard part map *)
    7.13    st        :: "hypreal => hypreal"
    7.14 +    --{*the standard part of a hyperreal*}
    7.15     "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
    7.16  
    7.17    monad     :: "hypreal => hypreal set"
    7.18 @@ -39,8 +39,8 @@
    7.19  
    7.20  defs (overloaded)
    7.21  
    7.22 -   (*standard real numbers as a subset of the hyperreals*)
    7.23     SReal_def:      "Reals == {x. \<exists>r. x = hypreal_of_real r}"
    7.24 +     --{*the standard real numbers as a subset of the hyperreals*}
    7.25  
    7.26  syntax (xsymbols)
    7.27      approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
    7.28 @@ -50,7 +50,7 @@
    7.29  
    7.30  
    7.31  
    7.32 -subsection{*Closure Laws for  Standard Reals*}
    7.33 +subsection{*Closure Laws for the Standard Reals*}
    7.34  
    7.35  lemma SReal_add [simp]:
    7.36       "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
    7.37 @@ -78,12 +78,11 @@
    7.38  apply (blast intro: hypreal_of_real_minus [symmetric])
    7.39  done
    7.40  
    7.41 -lemma SReal_minus_iff: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
    7.42 +lemma SReal_minus_iff [simp]: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
    7.43  apply auto
    7.44  apply (erule_tac [2] SReal_minus)
    7.45  apply (drule SReal_minus, auto)
    7.46  done
    7.47 -declare SReal_minus_iff [simp]
    7.48  
    7.49  lemma SReal_add_cancel:
    7.50       "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
    7.51 @@ -96,37 +95,32 @@
    7.52  apply (auto simp add: hypreal_of_real_hrabs)
    7.53  done
    7.54  
    7.55 -lemma SReal_hypreal_of_real: "hypreal_of_real x \<in> Reals"
    7.56 +lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
    7.57  by (simp add: SReal_def)
    7.58 -declare SReal_hypreal_of_real [simp]
    7.59  
    7.60 -lemma SReal_number_of: "(number_of w ::hypreal) \<in> Reals"
    7.61 +lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals"
    7.62  apply (simp only: hypreal_number_of [symmetric])
    7.63  apply (rule SReal_hypreal_of_real)
    7.64  done
    7.65 -declare SReal_number_of [simp]
    7.66  
    7.67  (** As always with numerals, 0 and 1 are special cases **)
    7.68  
    7.69 -lemma Reals_0: "(0::hypreal) \<in> Reals"
    7.70 +lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals"
    7.71  apply (subst numeral_0_eq_0 [symmetric])
    7.72  apply (rule SReal_number_of)
    7.73  done
    7.74 -declare Reals_0 [simp]
    7.75  
    7.76 -lemma Reals_1: "(1::hypreal) \<in> Reals"
    7.77 +lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals"
    7.78  apply (subst numeral_1_eq_1 [symmetric])
    7.79  apply (rule SReal_number_of)
    7.80  done
    7.81 -declare Reals_1 [simp]
    7.82  
    7.83  lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
    7.84  apply (unfold hypreal_divide_def)
    7.85  apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
    7.86  done
    7.87  
    7.88 -(* Infinitesimal epsilon not in Reals *)
    7.89 -
    7.90 +text{*epsilon is not in Reals because it is an infinitesimal*}
    7.91  lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
    7.92  apply (simp add: SReal_def)
    7.93  apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
    7.94 @@ -163,9 +157,8 @@
    7.95  apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
    7.96  done
    7.97  
    7.98 -(*------------------------------------------------------------------
    7.99 -                   Completeness of Reals
   7.100 - ------------------------------------------------------------------*)
   7.101 +text{*Completeness of Reals, but both lemmas are unused.*}
   7.102 +
   7.103  lemma SReal_sup_lemma:
   7.104       "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
   7.105        (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
   7.106 @@ -182,14 +175,13 @@
   7.107  apply (auto, rule_tac x = ya in exI, auto)
   7.108  done
   7.109  
   7.110 -(*------------------------------------------------------
   7.111 -    lifting of ub and property of lub
   7.112 - -------------------------------------------------------*)
   7.113 +
   7.114 +subsection{*Lifting of the Ub and Lub Properties*}
   7.115 +
   7.116  lemma hypreal_of_real_isUb_iff:
   7.117        "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
   7.118         (isUb (UNIV :: real set) Q Y)"
   7.119 -apply (simp add: isUb_def setle_def)
   7.120 -done
   7.121 +by (simp add: isUb_def setle_def)
   7.122  
   7.123  lemma hypreal_of_real_isLub1:
   7.124       "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
   7.125 @@ -215,7 +207,6 @@
   7.126        (isLub (UNIV :: real set) Q Y)"
   7.127  by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
   7.128  
   7.129 -(* lemmas *)
   7.130  lemma lemma_isUb_hypreal_of_real:
   7.131       "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
   7.132  by (auto simp add: SReal_iff isUb_def)
   7.133 @@ -233,7 +224,8 @@
   7.134        ==> \<exists>t::hypreal. isLub Reals P t"
   7.135  apply (frule SReal_hypreal_of_real_image)
   7.136  apply (auto, drule lemma_isUb_hypreal_of_real)
   7.137 -apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
   7.138 +apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
   7.139 +            simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
   7.140  done
   7.141  
   7.142  
   7.143 @@ -265,27 +257,23 @@
   7.144  lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. abs x < t"
   7.145  by (simp add: HFinite_def)
   7.146  
   7.147 -lemma HFinite_hrabs_iff: "(abs x \<in> HFinite) = (x \<in> HFinite)"
   7.148 +lemma HFinite_hrabs_iff [iff]: "(abs x \<in> HFinite) = (x \<in> HFinite)"
   7.149  by (simp add: HFinite_def)
   7.150 -declare HFinite_hrabs_iff [iff]
   7.151  
   7.152 -lemma HFinite_number_of: "number_of w \<in> HFinite"
   7.153 +lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
   7.154  by (rule SReal_number_of [THEN SReal_subset_HFinite [THEN subsetD]])
   7.155 -declare HFinite_number_of [simp]
   7.156  
   7.157  (** As always with numerals, 0 and 1 are special cases **)
   7.158  
   7.159 -lemma HFinite_0: "0 \<in> HFinite"
   7.160 +lemma HFinite_0 [simp]: "0 \<in> HFinite"
   7.161  apply (subst numeral_0_eq_0 [symmetric])
   7.162  apply (rule HFinite_number_of)
   7.163  done
   7.164 -declare HFinite_0 [simp]
   7.165  
   7.166 -lemma HFinite_1: "1 \<in> HFinite"
   7.167 +lemma HFinite_1 [simp]: "1 \<in> HFinite"
   7.168  apply (subst numeral_1_eq_1 [symmetric])
   7.169  apply (rule HFinite_number_of)
   7.170  done
   7.171 -declare HFinite_1 [simp]
   7.172  
   7.173  lemma HFinite_bounded: "[|x \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
   7.174  apply (case_tac "x \<le> 0")
   7.175 @@ -302,9 +290,8 @@
   7.176        "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
   7.177  by (simp add: Infinitesimal_def)
   7.178  
   7.179 -lemma Infinitesimal_zero: "0 \<in> Infinitesimal"
   7.180 +lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
   7.181  by (simp add: Infinitesimal_def)
   7.182 -declare Infinitesimal_zero [iff]
   7.183  
   7.184  lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
   7.185  by auto
   7.186 @@ -317,9 +304,8 @@
   7.187  apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of)
   7.188  done
   7.189  
   7.190 -lemma Infinitesimal_minus_iff: "(-x:Infinitesimal) = (x:Infinitesimal)"
   7.191 +lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
   7.192  by (simp add: Infinitesimal_def)
   7.193 -declare Infinitesimal_minus_iff [simp]
   7.194  
   7.195  lemma Infinitesimal_diff:
   7.196       "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
   7.197 @@ -368,6 +354,9 @@
   7.198  apply (auto simp add: mult_ac)
   7.199  done
   7.200  
   7.201 +lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
   7.202 +by (auto dest: add_less_le_mono)
   7.203 +
   7.204  lemma HInfinite_add_ge_zero:
   7.205        "[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
   7.206  by (auto intro!: hypreal_add_zero_less_le_mono 
   7.207 @@ -406,9 +395,9 @@
   7.208  lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
   7.209  by auto
   7.210  
   7.211 -lemma Infinitesimal_hrabs_iff: "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   7.212 +lemma Infinitesimal_hrabs_iff [iff]:
   7.213 +     "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
   7.214  by (auto simp add: abs_if)
   7.215 -declare Infinitesimal_hrabs_iff [iff]
   7.216  
   7.217  lemma HFinite_diff_Infinitesimal_hrabs:
   7.218       "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
   7.219 @@ -486,9 +475,8 @@
   7.220  lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
   7.221  by (simp add: approx_def hypreal_add_commute)
   7.222  
   7.223 -lemma approx_refl: "x @= x"
   7.224 +lemma approx_refl [iff]: "x @= x"
   7.225  by (simp add: approx_def Infinitesimal_def)
   7.226 -declare approx_refl [iff]
   7.227  
   7.228  lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
   7.229  by (simp add: hypreal_add_commute)
   7.230 @@ -543,8 +531,6 @@
   7.231  val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image";
   7.232  val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image";
   7.233  val SReal_dense = thm "SReal_dense";
   7.234 -val SReal_sup_lemma = thm "SReal_sup_lemma";
   7.235 -val SReal_sup_lemma2 = thm "SReal_sup_lemma2";
   7.236  val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff";
   7.237  val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1";
   7.238  val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2";
   7.239 @@ -669,11 +655,9 @@
   7.240  lemma approx_minus2: "-a @= -b ==> a @= b"
   7.241  by (auto dest: approx_minus)
   7.242  
   7.243 -lemma approx_minus_cancel: "(-a @= -b) = (a @= b)"
   7.244 +lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
   7.245  by (blast intro: approx_minus approx_minus2)
   7.246  
   7.247 -declare approx_minus_cancel [simp]
   7.248 -
   7.249  lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
   7.250  by (blast intro!: approx_add approx_minus)
   7.251  
   7.252 @@ -683,8 +667,7 @@
   7.253           del: minus_mult_left [symmetric])
   7.254  
   7.255  lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
   7.256 -apply (simp (no_asm_simp) add: approx_mult1 hypreal_mult_commute)
   7.257 -done
   7.258 +by (simp add: approx_mult1 hypreal_mult_commute)
   7.259  
   7.260  lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
   7.261  by (blast intro: approx_mult2 approx_trans)
   7.262 @@ -756,19 +739,13 @@
   7.263  done
   7.264  
   7.265  lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
   7.266 -apply (simp (no_asm_simp) add: hypreal_add_commute approx_add_mono1)
   7.267 -done
   7.268 +by (simp add: hypreal_add_commute approx_add_mono1)
   7.269  
   7.270 -lemma approx_add_left_iff: "(a + b @= a + c) = (b @= c)"
   7.271 +lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
   7.272  by (fast elim: approx_add_left_cancel approx_add_mono1)
   7.273  
   7.274 -declare approx_add_left_iff [simp]
   7.275 -
   7.276 -lemma approx_add_right_iff: "(b + a @= c + a) = (b @= c)"
   7.277 -apply (simp (no_asm) add: hypreal_add_commute)
   7.278 -done
   7.279 -
   7.280 -declare approx_add_right_iff [simp]
   7.281 +lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
   7.282 +by (simp add: hypreal_add_commute)
   7.283  
   7.284  lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
   7.285  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
   7.286 @@ -791,8 +768,8 @@
   7.287  lemma approx_mult_hypreal_of_real:
   7.288       "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
   7.289        ==> a*c @= hypreal_of_real b*hypreal_of_real d"
   7.290 -apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real)
   7.291 -done
   7.292 +by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite 
   7.293 +                  HFinite_hypreal_of_real)
   7.294  
   7.295  lemma approx_SReal_mult_cancel_zero:
   7.296       "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.297 @@ -800,17 +777,15 @@
   7.298  apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
   7.299  done
   7.300  
   7.301 -(* REM comments: newly added *)
   7.302  lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
   7.303  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
   7.304  
   7.305  lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
   7.306  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   7.307  
   7.308 -lemma approx_mult_SReal_zero_cancel_iff:
   7.309 +lemma approx_mult_SReal_zero_cancel_iff [simp]:
   7.310       "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.311  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   7.312 -declare approx_mult_SReal_zero_cancel_iff [simp]
   7.313  
   7.314  lemma approx_SReal_mult_cancel:
   7.315       "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.316 @@ -818,10 +793,10 @@
   7.317  apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
   7.318  done
   7.319  
   7.320 -lemma approx_SReal_mult_cancel_iff1:
   7.321 +lemma approx_SReal_mult_cancel_iff1 [simp]:
   7.322       "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.323 -by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel)
   7.324 -declare approx_SReal_mult_cancel_iff1 [simp]
   7.325 +by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   7.326 +         intro: approx_SReal_mult_cancel)
   7.327  
   7.328  lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
   7.329  apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   7.330 @@ -873,26 +848,23 @@
   7.331       "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
   7.332  by (rule SReal_HFinite_diff_Infinitesimal, auto)
   7.333  
   7.334 -lemma hypreal_of_real_Infinitesimal_iff_0:
   7.335 +lemma hypreal_of_real_Infinitesimal_iff_0 [iff]:
   7.336       "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
   7.337  apply auto
   7.338  apply (rule ccontr)
   7.339  apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto)
   7.340  done
   7.341 -declare hypreal_of_real_Infinitesimal_iff_0 [iff]
   7.342  
   7.343 -lemma number_of_not_Infinitesimal:
   7.344 +lemma number_of_not_Infinitesimal [simp]:
   7.345       "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
   7.346  by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
   7.347 -declare number_of_not_Infinitesimal [simp]
   7.348  
   7.349  (*again: 1 is a special case, but not 0 this time*)
   7.350 -lemma one_not_Infinitesimal: "1 \<notin> Infinitesimal"
   7.351 +lemma one_not_Infinitesimal [simp]: "1 \<notin> Infinitesimal"
   7.352  apply (subst numeral_1_eq_1 [symmetric])
   7.353  apply (rule number_of_not_Infinitesimal)
   7.354  apply (simp (no_asm))
   7.355  done
   7.356 -declare one_not_Infinitesimal [simp]
   7.357  
   7.358  lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.359  apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   7.360 @@ -940,10 +912,9 @@
   7.361  apply (simp add: hypreal_eq_minus_iff [symmetric])
   7.362  done
   7.363  
   7.364 -lemma number_of_approx_iff:
   7.365 +lemma number_of_approx_iff [simp]:
   7.366       "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
   7.367  by (auto simp add: SReal_approx_iff)
   7.368 -declare number_of_approx_iff [simp]
   7.369  
   7.370  (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
   7.371  lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
   7.372 @@ -953,18 +924,16 @@
   7.373                "~ (0 @= 1)" "~ (1 @= 0)"
   7.374  by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
   7.375  
   7.376 -lemma hypreal_of_real_approx_iff:
   7.377 +lemma hypreal_of_real_approx_iff [simp]:
   7.378       "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
   7.379  apply auto
   7.380  apply (rule inj_hypreal_of_real [THEN injD])
   7.381  apply (rule SReal_approx_iff [THEN iffD1], auto)
   7.382  done
   7.383 -declare hypreal_of_real_approx_iff [simp]
   7.384  
   7.385 -lemma hypreal_of_real_approx_number_of_iff:
   7.386 +lemma hypreal_of_real_approx_number_of_iff [simp]:
   7.387       "(hypreal_of_real k @= number_of w) = (k = number_of w)"
   7.388  by (subst hypreal_of_real_approx_iff [symmetric], auto)
   7.389 -declare hypreal_of_real_approx_number_of_iff [simp]
   7.390  
   7.391  (*And also for 0 and 1.*)
   7.392  (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
   7.393 @@ -1060,25 +1029,22 @@
   7.394  apply (auto dest: order_less_le_trans)
   7.395  done
   7.396  
   7.397 -lemma lemma_hypreal_le_swap: "((x::hypreal) \<le> t + r) = (x + -t \<le> r)"
   7.398 -by auto
   7.399 -
   7.400  lemma lemma_st_part1a:
   7.401       "[| x \<in> HFinite;
   7.402           isLub Reals {s. s \<in> Reals & s < x} t;
   7.403           r \<in> Reals; 0 < r |]
   7.404        ==> x + -t \<le> r"
   7.405 -by (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
   7.406 -
   7.407 -lemma lemma_hypreal_le_swap2: "(t + -r \<le> x) = (-(x + -t) \<le> (r::hypreal))"
   7.408 -by auto
   7.409 +apply (subgoal_tac "x \<le> t+r") 
   7.410 +apply (auto intro: lemma_st_part_le1)
   7.411 +done
   7.412  
   7.413  lemma lemma_st_part2a:
   7.414       "[| x \<in> HFinite;
   7.415           isLub Reals {s. s \<in> Reals & s < x} t;
   7.416           r \<in> Reals;  0 < r |]
   7.417        ==> -(x + -t) \<le> r"
   7.418 -apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2)
   7.419 +apply (subgoal_tac "(t + -r \<le> x)") 
   7.420 +apply (auto intro: lemma_st_part_le2)
   7.421  done
   7.422  
   7.423  lemma lemma_SReal_ub:
   7.424 @@ -1137,9 +1103,8 @@
   7.425        ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
   7.426  by (blast dest!: lemma_st_part_major)
   7.427  
   7.428 -(*----------------------------------------------
   7.429 -  Existence of real and Standard Part Theorem
   7.430 - ----------------------------------------------*)
   7.431 +
   7.432 +text{*Existence of real and Standard Part Theorem*}
   7.433  lemma lemma_st_part_Ex:
   7.434       "x \<in> HFinite ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
   7.435  apply (frule lemma_st_part_lub, safe)
   7.436 @@ -1153,9 +1118,7 @@
   7.437  apply (drule lemma_st_part_Ex, auto)
   7.438  done
   7.439  
   7.440 -(*--------------------------------
   7.441 -  Unique real infinitely close
   7.442 - -------------------------------*)
   7.443 +text{*There is a unique real infinitely close*}
   7.444  lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
   7.445  apply (drule st_part_Ex, safe)
   7.446  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   7.447 @@ -1164,12 +1127,10 @@
   7.448  
   7.449  subsection{* Finite, Infinite and Infinitesimal*}
   7.450  
   7.451 -lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}"
   7.452 -
   7.453 +lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
   7.454  apply (simp add: HFinite_def HInfinite_def)
   7.455  apply (auto dest: order_less_trans)
   7.456  done
   7.457 -declare HFinite_Int_HInfinite_empty [simp]
   7.458  
   7.459  lemma HFinite_not_HInfinite: 
   7.460    assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
   7.461 @@ -1254,7 +1215,8 @@
   7.462       "[| x \<in> HFinite - Infinitesimal;
   7.463           h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
   7.464  apply (rule approx_trans2)
   7.465 -apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric])
   7.466 +apply (auto intro: inverse_add_Infinitesimal_approx 
   7.467 +            simp add: mem_infmal_iff approx_minus_iff [symmetric])
   7.468  done
   7.469  
   7.470  lemma Infinitesimal_square_iff: "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)"
   7.471 @@ -1265,15 +1227,13 @@
   7.472  done
   7.473  declare Infinitesimal_square_iff [symmetric, simp]
   7.474  
   7.475 -lemma HFinite_square_iff: "(x*x \<in> HFinite) = (x \<in> HFinite)"
   7.476 +lemma HFinite_square_iff [simp]: "(x*x \<in> HFinite) = (x \<in> HFinite)"
   7.477  apply (auto intro: HFinite_mult)
   7.478  apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
   7.479  done
   7.480 -declare HFinite_square_iff [simp]
   7.481  
   7.482 -lemma HInfinite_square_iff: "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
   7.483 +lemma HInfinite_square_iff [simp]: "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
   7.484  by (auto simp add: HInfinite_HFinite_iff)
   7.485 -declare HInfinite_square_iff [simp]
   7.486  
   7.487  lemma approx_HFinite_mult_cancel:
   7.488       "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   7.489 @@ -1332,10 +1292,9 @@
   7.490  by (auto intro: HInfinite_gt_SReal)
   7.491  
   7.492  
   7.493 -lemma not_HInfinite_one: "1 \<notin> HInfinite"
   7.494 +lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite"
   7.495  apply (simp (no_asm) add: HInfinite_HFinite_iff)
   7.496  done
   7.497 -declare not_HInfinite_one [simp]
   7.498  
   7.499  lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
   7.500  by (cut_tac x = x in hrabs_disj, auto)
   7.501 @@ -1364,19 +1323,18 @@
   7.502  apply (auto simp add: monad_zero_minus_iff [symmetric])
   7.503  done
   7.504  
   7.505 -lemma mem_monad_self: "x \<in> monad x"
   7.506 +lemma mem_monad_self [simp]: "x \<in> monad x"
   7.507  by (simp add: monad_def)
   7.508 -declare mem_monad_self [simp]
   7.509 +
   7.510  
   7.511 -(*------------------------------------------------------------------
   7.512 -         Proof that x @= y ==> abs x @= abs y
   7.513 - ------------------------------------------------------------------*)
   7.514 -lemma approx_subset_monad: "x @= y ==> {x,y}\<le>monad x"
   7.515 +subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*}
   7.516 +
   7.517 +lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
   7.518  apply (simp (no_asm))
   7.519  apply (simp add: approx_monad_iff)
   7.520  done
   7.521  
   7.522 -lemma approx_subset_monad2: "x @= y ==> {x,y}\<le>monad y"
   7.523 +lemma approx_subset_monad2: "x @= y ==> {x,y} \<le> monad y"
   7.524  apply (drule approx_sym)
   7.525  apply (fast dest: approx_subset_monad)
   7.526  done
   7.527 @@ -1432,24 +1390,12 @@
   7.528       "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   7.529  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
   7.530  
   7.531 -lemma approx_hrabs1:
   7.532 -     "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   7.533 -apply (frule lemma_approx_less_zero)
   7.534 -apply (assumption+)
   7.535 -apply (simp add: abs_if) 
   7.536 -done
   7.537 -
   7.538 -lemma approx_hrabs2:
   7.539 -     "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
   7.540 -apply (frule lemma_approx_gt_zero)
   7.541 -apply (assumption+)
   7.542 -apply (simp add: abs_if) 
   7.543 -done
   7.544 -
   7.545 -lemma approx_hrabs: "x @= y ==> abs x @= abs y"
   7.546 -apply (rule_tac Q = "x \<in> Infinitesimal" in excluded_middle [THEN disjE])
   7.547 -apply (rule_tac x1 = x and y1 = 0 in linorder_less_linear [THEN disjE])
   7.548 -apply (auto intro: approx_hrabs1 approx_hrabs2 Infinitesimal_approx_hrabs)
   7.549 +theorem approx_hrabs: "x @= y ==> abs x @= abs y"
   7.550 +apply (case_tac "x \<in> Infinitesimal") 
   7.551 +apply (simp add: Infinitesimal_approx_hrabs)
   7.552 +apply (rule linorder_cases [of 0 x])  
   7.553 +apply (frule lemma_approx_gt_zero [of x y]) 
   7.554 +apply (auto simp add: lemma_approx_less_zero [of x y])  
   7.555  done
   7.556  
   7.557  lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
   7.558 @@ -1480,9 +1426,6 @@
   7.559  apply (auto intro: approx_trans2)
   7.560  done
   7.561  
   7.562 -lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)"
   7.563 -by arith
   7.564 -
   7.565  (* interesting slightly counterintuitive theorem: necessary
   7.566     for proving that an open interval is an NS open set
   7.567  *)
   7.568 @@ -1500,7 +1443,8 @@
   7.569        ==> abs (hypreal_of_real r + x) < hypreal_of_real y"
   7.570  apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
   7.571  apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
   7.572 -apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: hypreal_of_real_hrabs)
   7.573 +apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
   7.574 +            simp add: hypreal_of_real_hrabs)
   7.575  done
   7.576  
   7.577  lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
   7.578 @@ -1523,11 +1467,11 @@
   7.579       "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
   7.580           hypreal_of_real x + u \<le> hypreal_of_real y + v |]
   7.581        ==> x \<le> y"
   7.582 -apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel)
   7.583 -done
   7.584 +by (blast intro!: hypreal_of_real_le_iff [THEN iffD1] 
   7.585 +                  hypreal_of_real_le_add_Infininitesimal_cancel)
   7.586  
   7.587  lemma hypreal_of_real_less_Infinitesimal_le_zero:
   7.588 -     "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
   7.589 +    "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
   7.590  apply (rule linorder_not_less [THEN iffD1], safe)
   7.591  apply (drule Infinitesimal_interval)
   7.592  apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
   7.593 @@ -1540,81 +1484,73 @@
   7.594  apply (subgoal_tac "h = - hypreal_of_real x", auto)
   7.595  done
   7.596  
   7.597 -lemma Infinitesimal_square_cancel:
   7.598 +lemma Infinitesimal_square_cancel [simp]:
   7.599       "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   7.600  apply (rule Infinitesimal_interval2)
   7.601  apply (rule_tac [3] zero_le_square, assumption)
   7.602  apply (auto simp add: zero_le_square)
   7.603  done
   7.604 -declare Infinitesimal_square_cancel [simp]
   7.605  
   7.606 -lemma HFinite_square_cancel: "x*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
   7.607 +lemma HFinite_square_cancel [simp]: "x*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
   7.608  apply (rule HFinite_bounded, assumption)
   7.609  apply (auto simp add: zero_le_square)
   7.610  done
   7.611 -declare HFinite_square_cancel [simp]
   7.612  
   7.613 -lemma Infinitesimal_square_cancel2:
   7.614 +lemma Infinitesimal_square_cancel2 [simp]:
   7.615       "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
   7.616  apply (rule Infinitesimal_square_cancel)
   7.617  apply (rule hypreal_add_commute [THEN subst])
   7.618  apply (simp (no_asm))
   7.619  done
   7.620 -declare Infinitesimal_square_cancel2 [simp]
   7.621  
   7.622 -lemma HFinite_square_cancel2: "x*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
   7.623 +lemma HFinite_square_cancel2 [simp]: "x*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
   7.624  apply (rule HFinite_square_cancel)
   7.625  apply (rule hypreal_add_commute [THEN subst])
   7.626  apply (simp (no_asm))
   7.627  done
   7.628 -declare HFinite_square_cancel2 [simp]
   7.629  
   7.630 -lemma Infinitesimal_sum_square_cancel:
   7.631 +lemma Infinitesimal_sum_square_cancel [simp]:
   7.632       "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   7.633  apply (rule Infinitesimal_interval2, assumption)
   7.634  apply (rule_tac [2] zero_le_square, simp)
   7.635  apply (insert zero_le_square [of y]) 
   7.636  apply (insert zero_le_square [of z], simp)
   7.637  done
   7.638 -declare Infinitesimal_sum_square_cancel [simp]
   7.639  
   7.640 -lemma HFinite_sum_square_cancel: "x*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
   7.641 +lemma HFinite_sum_square_cancel [simp]:
   7.642 +     "x*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
   7.643  apply (rule HFinite_bounded, assumption)
   7.644  apply (rule_tac [2] zero_le_square)
   7.645  apply (insert zero_le_square [of y]) 
   7.646  apply (insert zero_le_square [of z], simp)
   7.647  done
   7.648 -declare HFinite_sum_square_cancel [simp]
   7.649  
   7.650 -lemma Infinitesimal_sum_square_cancel2:
   7.651 +lemma Infinitesimal_sum_square_cancel2 [simp]:
   7.652       "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   7.653  apply (rule Infinitesimal_sum_square_cancel)
   7.654  apply (simp add: add_ac)
   7.655  done
   7.656 -declare Infinitesimal_sum_square_cancel2 [simp]
   7.657  
   7.658 -lemma HFinite_sum_square_cancel2:
   7.659 +lemma HFinite_sum_square_cancel2 [simp]:
   7.660       "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
   7.661  apply (rule HFinite_sum_square_cancel)
   7.662  apply (simp add: add_ac)
   7.663  done
   7.664 -declare HFinite_sum_square_cancel2 [simp]
   7.665  
   7.666 -lemma Infinitesimal_sum_square_cancel3:
   7.667 +lemma Infinitesimal_sum_square_cancel3 [simp]:
   7.668       "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   7.669  apply (rule Infinitesimal_sum_square_cancel)
   7.670  apply (simp add: add_ac)
   7.671  done
   7.672 -declare Infinitesimal_sum_square_cancel3 [simp]
   7.673  
   7.674 -lemma HFinite_sum_square_cancel3:
   7.675 +lemma HFinite_sum_square_cancel3 [simp]:
   7.676       "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
   7.677  apply (rule HFinite_sum_square_cancel)
   7.678  apply (simp add: add_ac)
   7.679  done
   7.680 -declare HFinite_sum_square_cancel3 [simp]
   7.681  
   7.682 -lemma monad_hrabs_less: "[| y \<in> monad x; 0 < hypreal_of_real e |]
   7.683 +lemma monad_hrabs_less:
   7.684 +     "[| y \<in> monad x; 0 < hypreal_of_real e |]
   7.685        ==> abs (y + -x) < hypreal_of_real e"
   7.686  apply (drule mem_monad_approx [THEN approx_sym])
   7.687  apply (drule bex_Infinitesimal_iff [THEN iffD2])
   7.688 @@ -1656,8 +1592,7 @@
   7.689  apply (blast dest: SReal_approx_iff [THEN iffD1])
   7.690  done
   7.691  
   7.692 -(* ???should be added to simpset *)
   7.693 -lemma st_hypreal_of_real: "st (hypreal_of_real x) = hypreal_of_real x"
   7.694 +lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
   7.695  by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
   7.696  
   7.697  lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
   7.698 @@ -1718,9 +1653,8 @@
   7.699    finally show ?thesis .
   7.700  qed
   7.701  
   7.702 -lemma st_number_of: "st (number_of w) = number_of w"
   7.703 +lemma st_number_of [simp]: "st (number_of w) = number_of w"
   7.704  by (rule SReal_number_of [THEN st_SReal_eq])
   7.705 -declare st_number_of [simp]
   7.706  
   7.707  (*the theorem above for the special cases of zero and one*)
   7.708  lemma [simp]: "st 0 = 0" "st 1 = 1"
   7.709 @@ -1740,7 +1674,6 @@
   7.710  apply (simp (no_asm_simp) add: st_add)
   7.711  done
   7.712  
   7.713 -(* lemma *)
   7.714  lemma lemma_st_mult:
   7.715       "[| x \<in> HFinite; y \<in> HFinite; e \<in> Infinitesimal; ea \<in> Infinitesimal |]
   7.716        ==> e*y + x*ea + e*ea \<in> Infinitesimal"
   7.717 @@ -1787,16 +1720,13 @@
   7.718  apply (subst hypreal_mult_inverse, auto)
   7.719  done
   7.720  
   7.721 -lemma st_divide:
   7.722 +lemma st_divide [simp]:
   7.723       "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
   7.724        ==> st(x/y) = (st x) / (st y)"
   7.725 -apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
   7.726 -done
   7.727 -declare st_divide [simp]
   7.728 +by (simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
   7.729  
   7.730 -lemma st_idempotent: "x \<in> HFinite ==> st(st(x)) = st(x)"
   7.731 +lemma st_idempotent [simp]: "x \<in> HFinite ==> st(st(x)) = st(x)"
   7.732  by (blast intro: st_HFinite st_approx_self approx_st_eq)
   7.733 -declare st_idempotent [simp]
   7.734  
   7.735  lemma Infinitesimal_add_st_less:
   7.736       "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |] 
   7.737 @@ -2021,10 +1951,10 @@
   7.738  done
   7.739  
   7.740  
   7.741 -(*-------------------------------------------------------------------------
   7.742 -       Proof that omega is an infinite number and
   7.743 -       hence that epsilon is an infinitesimal number.
   7.744 - -------------------------------------------------------------------------*)
   7.745 +subsection{*Proof that @{term omega} is an infinite number*}
   7.746 +
   7.747 +text{*It will follow that epsilon is an infinitesimal number.*}
   7.748 +
   7.749  lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
   7.750  by (auto simp add: less_Suc_eq)
   7.751  
   7.752 @@ -2077,9 +2007,7 @@
   7.753  lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
   7.754  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
   7.755  
   7.756 -(*-----------------------------------------------
   7.757 -       Omega is a member of HInfinite
   7.758 - -----------------------------------------------*)
   7.759 +text{*@{term omega} is a member of @{term HInfinite}*}
   7.760  
   7.761  lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \<in> hypreal"
   7.762  by auto
   7.763 @@ -2089,31 +2017,27 @@
   7.764  apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq)
   7.765  done
   7.766  
   7.767 -lemma HInfinite_omega: "omega: HInfinite"
   7.768 +theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
   7.769  apply (simp add: omega_def)
   7.770  apply (auto intro!: FreeUltrafilterNat_HInfinite)
   7.771  apply (rule bexI)
   7.772  apply (rule_tac [2] lemma_hyprel_refl, auto)
   7.773  apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
   7.774  done
   7.775 -declare HInfinite_omega [simp]
   7.776  
   7.777  (*-----------------------------------------------
   7.778         Epsilon is a member of Infinitesimal
   7.779   -----------------------------------------------*)
   7.780  
   7.781 -lemma Infinitesimal_epsilon: "epsilon \<in> Infinitesimal"
   7.782 +lemma Infinitesimal_epsilon [simp]: "epsilon \<in> Infinitesimal"
   7.783  by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)
   7.784 -declare Infinitesimal_epsilon [simp]
   7.785  
   7.786 -lemma HFinite_epsilon: "epsilon \<in> HFinite"
   7.787 +lemma HFinite_epsilon [simp]: "epsilon \<in> HFinite"
   7.788  by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
   7.789 -declare HFinite_epsilon [simp]
   7.790  
   7.791 -lemma epsilon_approx_zero: "epsilon @= 0"
   7.792 +lemma epsilon_approx_zero [simp]: "epsilon @= 0"
   7.793  apply (simp (no_asm) add: mem_infmal_iff [symmetric])
   7.794  done
   7.795 -declare epsilon_approx_zero [simp]
   7.796  
   7.797  (*------------------------------------------------------------------------
   7.798    Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
   7.799 @@ -2343,15 +2267,12 @@
   7.800  val less_Infinitesimal_less = thm "less_Infinitesimal_less";
   7.801  val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero";
   7.802  val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero";
   7.803 -val approx_hrabs1 = thm "approx_hrabs1";
   7.804 -val approx_hrabs2 = thm "approx_hrabs2";
   7.805  val approx_hrabs = thm "approx_hrabs";
   7.806  val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel";
   7.807  val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal";
   7.808  val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal";
   7.809  val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel";
   7.810  val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel";
   7.811 -val hypreal_less_minus_iff = thm "hypreal_less_minus_iff";
   7.812  val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less";
   7.813  val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less";
   7.814  val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2";
     8.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 04 15:28:03 2004 +0200
     8.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Tue Oct 05 15:30:50 2004 +0200
     8.3 @@ -73,7 +73,7 @@
     8.4        "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
     8.5  apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
     8.6  apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
     8.7 -apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
     8.8 +apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
     8.9  done
    8.10  
    8.11  
     9.1 --- a/src/HOL/Hyperreal/Series.thy	Mon Oct 04 15:28:03 2004 +0200
     9.2 +++ b/src/HOL/Hyperreal/Series.thy	Tue Oct 05 15:30:50 2004 +0200
     9.3 @@ -109,22 +109,14 @@
     9.4  apply (auto intro: add_mono simp add: le_def)
     9.5  done
     9.6  
     9.7 -lemma sumr_ge_zero [rule_format (no_asm)]: "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumr m n f"
     9.8 -apply (induct_tac "n", auto)
     9.9 -apply (drule_tac x = n in spec, arith)
    9.10 -done
    9.11 -
    9.12 -lemma sumr_ge_zero2 [rule_format (no_asm)]:
    9.13 -     "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
    9.14 +lemma sumr_ge_zero [rule_format]: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
    9.15  apply (induct_tac "n", auto)
    9.16  apply (drule_tac x = n in spec, arith)
    9.17  done
    9.18  
    9.19  lemma rabs_sumr_rabs_cancel [simp]:
    9.20 -     "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
    9.21 -apply (induct_tac "n")
    9.22 -apply (auto, arith)
    9.23 -done
    9.24 +     "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
    9.25 +by (induct_tac "n", simp_all add: add_increasing)
    9.26  
    9.27  lemma sumr_zero [rule_format]:
    9.28       "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
    9.29 @@ -480,9 +472,6 @@
    9.30  val sumr_diff_mult_const = thm "sumr_diff_mult_const";
    9.31  val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
    9.32  val sumr_le2 = thm "sumr_le2";
    9.33 -val sumr_ge_zero = thm "sumr_ge_zero";
    9.34 -val sumr_ge_zero2 = thm "sumr_ge_zero2";
    9.35 -val sumr_rabs_ge_zero = thm "sumr_rabs_ge_zero";
    9.36  val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
    9.37  val sumr_zero = thm "sumr_zero";
    9.38  val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
    10.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 04 15:28:03 2004 +0200
    10.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 05 15:30:50 2004 +0200
    10.3 @@ -52,13 +52,13 @@
    10.4  
    10.5  
    10.6  lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
    10.7 -apply (unfold root_def)
    10.8 +apply (simp add: root_def)
    10.9  apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero)
   10.10  done
   10.11  
   10.12  lemma real_root_pow_pos: 
   10.13       "0 < x ==> (root(Suc n) x) ^ (Suc n) = x"
   10.14 -apply (unfold root_def)
   10.15 +apply (simp add: root_def)
   10.16  apply (drule_tac n = n in realpow_pos_nth2)
   10.17  apply (auto intro: someI2)
   10.18  done
   10.19 @@ -68,7 +68,7 @@
   10.20  
   10.21  lemma real_root_pos: 
   10.22       "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"
   10.23 -apply (unfold root_def)
   10.24 +apply (simp add: root_def)
   10.25  apply (rule some_equality)
   10.26  apply (frule_tac [2] n = n in zero_less_power)
   10.27  apply (auto simp add: zero_less_mult_iff)
   10.28 @@ -83,17 +83,18 @@
   10.29  
   10.30  lemma real_root_pos_pos: 
   10.31       "0 < x ==> 0 \<le> root(Suc n) x"
   10.32 -apply (unfold root_def)
   10.33 +apply (simp add: root_def)
   10.34  apply (drule_tac n = n in realpow_pos_nth2)
   10.35  apply (safe, rule someI2)
   10.36 -apply (auto intro!: order_less_imp_le dest: zero_less_power simp add: zero_less_mult_iff)
   10.37 +apply (auto intro!: order_less_imp_le dest: zero_less_power 
   10.38 +            simp add: zero_less_mult_iff)
   10.39  done
   10.40  
   10.41  lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x"
   10.42  by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos)
   10.43  
   10.44  lemma real_root_one [simp]: "root (Suc n) 1 = 1"
   10.45 -apply (unfold root_def)
   10.46 +apply (simp add: root_def)
   10.47  apply (rule some_equality, auto)
   10.48  apply (rule ccontr)
   10.49  apply (rule_tac x = u and y = 1 in linorder_cases)
   10.50 @@ -105,19 +106,19 @@
   10.51  
   10.52  subsection{*Square Root*}
   10.53  
   10.54 -(*lcp: needed now because 2 is a binary numeral!*)
   10.55 +text{*needed because 2 is a binary numeral!*}
   10.56  lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))"
   10.57 -apply (simp (no_asm) del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 add: nat_numeral_0_eq_0 [symmetric])
   10.58 -done
   10.59 +by (simp del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 
   10.60 +         add: nat_numeral_0_eq_0 [symmetric])
   10.61  
   10.62  lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
   10.63 -by (unfold sqrt_def, auto)
   10.64 +by (simp add: sqrt_def)
   10.65  
   10.66  lemma real_sqrt_one [simp]: "sqrt 1 = 1"
   10.67 -by (unfold sqrt_def, auto)
   10.68 +by (simp add: sqrt_def)
   10.69  
   10.70  lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   10.71 -apply (unfold sqrt_def)
   10.72 +apply (simp add: sqrt_def)
   10.73  apply (rule iffI) 
   10.74   apply (cut_tac r = "root 2 x" in realpow_two_le)
   10.75   apply (simp add: numeral_2_eq_2)
   10.76 @@ -136,7 +137,7 @@
   10.77  
   10.78  lemma real_pow_sqrt_eq_sqrt_pow: 
   10.79        "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)"
   10.80 -apply (unfold sqrt_def)
   10.81 +apply (simp add: sqrt_def)
   10.82  apply (subst numeral_2_eq_2)
   10.83  apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp del: realpow_Suc)
   10.84  done
   10.85 @@ -162,8 +163,7 @@
   10.86  by auto
   10.87  
   10.88  lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
   10.89 -apply (unfold sqrt_def root_def)
   10.90 -apply (subst numeral_2_eq_2)
   10.91 +apply (simp add: sqrt_def root_def)
   10.92  apply (drule realpow_pos_nth2 [where n=1], safe)
   10.93  apply (rule someI2, auto)
   10.94  done
   10.95 @@ -178,7 +178,7 @@
   10.96  (*we need to prove something like this:
   10.97  lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r"
   10.98  apply (case_tac n, simp) 
   10.99 -apply (unfold root_def) 
  10.100 +apply (simp add: root_def) 
  10.101  apply (rule someI2 [of _ r], safe)
  10.102  apply (auto simp del: realpow_Suc dest: power_inject_base)
  10.103  *)
  10.104 @@ -197,13 +197,15 @@
  10.105  apply (simp add: zero_le_mult_iff real_sqrt_ge_zero) 
  10.106  done
  10.107  
  10.108 -lemma real_sqrt_mult_distrib2: "[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) =  sqrt(x) * sqrt(y)"
  10.109 +lemma real_sqrt_mult_distrib2:
  10.110 +     "[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) =  sqrt(x) * sqrt(y)"
  10.111  by (auto intro: real_sqrt_mult_distrib simp add: order_le_less)
  10.112  
  10.113  lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
  10.114  by (auto intro!: real_sqrt_ge_zero)
  10.115  
  10.116 -lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
  10.117 +lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
  10.118 +     "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
  10.119  by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
  10.120  
  10.121  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
  10.122 @@ -239,7 +241,7 @@
  10.123  apply (auto dest: real_sqrt_not_eq_zero)
  10.124  done
  10.125  
  10.126 -lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x = 0))"
  10.127 +lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x=0))"
  10.128  by (auto simp add: real_sqrt_eq_zero_cancel)
  10.129  
  10.130  lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
  10.131 @@ -274,9 +276,9 @@
  10.132  apply (subst fact_Suc)
  10.133  apply (subst real_of_nat_mult)
  10.134  apply (auto simp add: abs_mult inverse_mult_distrib)
  10.135 -apply (auto simp add: mult_assoc [symmetric] abs_eqI2 positive_imp_inverse_positive)
  10.136 +apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
  10.137  apply (rule order_less_imp_le)
  10.138 -apply (rule_tac z1 = "real (Suc na) " in real_mult_less_iff1 [THEN iffD1])
  10.139 +apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
  10.140  apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse)
  10.141  apply (erule order_less_trans)
  10.142  apply (auto simp add: mult_less_cancel_left mult_ac)
  10.143 @@ -288,40 +290,39 @@
  10.144             (if even n then 0  
  10.145             else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
  10.146                  x ^ n)"
  10.147 -apply (unfold real_divide_def)
  10.148 -apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
  10.149 +apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
  10.150  apply (rule_tac [2] summable_exp)
  10.151  apply (rule_tac x = 0 in exI)
  10.152 -apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
  10.153 +apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
  10.154  done
  10.155  
  10.156  lemma summable_cos: 
  10.157        "summable (%n.  
  10.158             (if even n then  
  10.159             (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
  10.160 -apply (unfold real_divide_def)
  10.161 -apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
  10.162 +apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
  10.163  apply (rule_tac [2] summable_exp)
  10.164  apply (rule_tac x = 0 in exI)
  10.165 -apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
  10.166 +apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
  10.167  done
  10.168  
  10.169 -lemma lemma_STAR_sin [simp]: "(if even n then 0  
  10.170 +lemma lemma_STAR_sin [simp]:
  10.171 +     "(if even n then 0  
  10.172         else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
  10.173 -apply (induct_tac "n", auto)
  10.174 -done
  10.175 -
  10.176 -lemma lemma_STAR_cos [simp]: "0 < n -->  
  10.177 +by (induct_tac "n", auto)
  10.178 +
  10.179 +lemma lemma_STAR_cos [simp]:
  10.180 +     "0 < n -->  
  10.181        (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
  10.182 -apply (induct_tac "n", auto)
  10.183 -done
  10.184 -
  10.185 -lemma lemma_STAR_cos1 [simp]: "0 < n -->  
  10.186 +by (induct_tac "n", auto)
  10.187 +
  10.188 +lemma lemma_STAR_cos1 [simp]:
  10.189 +     "0 < n -->  
  10.190        (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
  10.191 -apply (induct_tac "n", auto)
  10.192 -done
  10.193 -
  10.194 -lemma lemma_STAR_cos2 [simp]: "sumr 1 n (%n. if even n  
  10.195 +by (induct_tac "n", auto)
  10.196 +
  10.197 +lemma lemma_STAR_cos2 [simp]:
  10.198 +     "sumr 1 n (%n. if even n  
  10.199                      then (- 1) ^ (n div 2)/(real (fact n)) *  
  10.200                            0 ^ n  
  10.201                      else 0) = 0"
  10.202 @@ -330,7 +331,7 @@
  10.203  done
  10.204  
  10.205  lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
  10.206 -apply (unfold exp_def)
  10.207 +apply (simp add: exp_def)
  10.208  apply (rule summable_exp [THEN summable_sums])
  10.209  done
  10.210  
  10.211 @@ -338,7 +339,7 @@
  10.212        "(%n. (if even n then 0  
  10.213              else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
  10.214                   x ^ n) sums sin(x)"
  10.215 -apply (unfold sin_def)
  10.216 +apply (simp add: sin_def)
  10.217  apply (rule summable_sin [THEN summable_sums])
  10.218  done
  10.219  
  10.220 @@ -346,11 +347,12 @@
  10.221        "(%n. (if even n then  
  10.222             (- 1) ^ (n div 2)/(real (fact n))  
  10.223             else 0) * x ^ n) sums cos(x)"
  10.224 -apply (unfold cos_def)
  10.225 +apply (simp add: cos_def)
  10.226  apply (rule summable_cos [THEN summable_sums])
  10.227  done
  10.228  
  10.229 -lemma lemma_realpow_diff [rule_format (no_asm)]: "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
  10.230 +lemma lemma_realpow_diff [rule_format (no_asm)]:
  10.231 +     "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
  10.232  apply (induct_tac "n", auto)
  10.233  apply (subgoal_tac "p = Suc n")
  10.234  apply (simp (no_asm_simp), auto)
  10.235 @@ -372,16 +374,18 @@
  10.236  apply (auto simp add: mult_ac)
  10.237  done
  10.238  
  10.239 -lemma lemma_realpow_diff_sumr2: "x ^ (Suc n) - y ^ (Suc n) =  
  10.240 +lemma lemma_realpow_diff_sumr2:
  10.241 +     "x ^ (Suc n) - y ^ (Suc n) =  
  10.242        (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
  10.243  apply (induct_tac "n", simp)
  10.244  apply (auto simp del: sumr_Suc)
  10.245  apply (subst sumr_Suc)
  10.246  apply (drule sym)
  10.247 -apply (auto simp add: lemma_realpow_diff_sumr right_distrib real_diff_def mult_ac simp del: sumr_Suc)
  10.248 +apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
  10.249  done
  10.250  
  10.251 -lemma lemma_realpow_rev_sumr: "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =  
  10.252 +lemma lemma_realpow_rev_sumr:
  10.253 +     "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =  
  10.254        sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
  10.255  apply (case_tac "x = y")
  10.256  apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
  10.257 @@ -413,7 +417,7 @@
  10.258  apply (rule_tac a2 = "z ^ n" 
  10.259         in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
  10.260  apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
  10.261 -apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>))) " in exI)
  10.262 +apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>)))" in exI)
  10.263  apply (auto intro!: sums_mult simp add: mult_assoc)
  10.264  apply (subgoal_tac "\<bar>z ^ n\<bar> * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n")
  10.265  apply (auto simp add: power_abs [symmetric])
  10.266 @@ -425,7 +429,8 @@
  10.267  apply (auto simp add: abs_mult [symmetric] mult_assoc)
  10.268  done
  10.269  
  10.270 -lemma powser_inside: "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
  10.271 +lemma powser_inside:
  10.272 +     "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
  10.273        ==> summable (%n. f(n) * (z ^ n))"
  10.274  apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea)
  10.275  apply (auto intro: summable_rabs_cancel simp add: power_abs [symmetric])
  10.276 @@ -447,13 +452,15 @@
  10.277  apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
  10.278  done
  10.279  
  10.280 -lemma lemma_diffs2: "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  
  10.281 +lemma lemma_diffs2:
  10.282 +     "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  
  10.283        sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -  
  10.284        (real n * c(n) * x ^ (n - Suc 0))"
  10.285  by (auto simp add: lemma_diffs)
  10.286  
  10.287  
  10.288 -lemma diffs_equiv: "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
  10.289 +lemma diffs_equiv:
  10.290 +     "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
  10.291        (%n. real n * c(n) * (x ^ (n - Suc 0))) sums  
  10.292           (suminf(%n. (diffs c)(n) * (x ^ n)))"
  10.293  apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0")
  10.294 @@ -473,7 +480,7 @@
  10.295          sumr 0 m (%p. (z ^ p) *  
  10.296          (((z + h) ^ (m - p)) - (z ^ (m - p))))"
  10.297  apply (rule sumr_subst)
  10.298 -apply (auto simp add: right_distrib real_diff_def power_add [symmetric] mult_ac)
  10.299 +apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
  10.300  done
  10.301  
  10.302  lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"
  10.303 @@ -483,7 +490,8 @@
  10.304  by arith
  10.305  
  10.306  
  10.307 -lemma lemma_termdiff2: " h \<noteq> 0 ==>  
  10.308 +lemma lemma_termdiff2:
  10.309 +     " h \<noteq> 0 ==>  
  10.310          (((z + h) ^ n) - (z ^ n)) * inverse h -  
  10.311              real n * (z ^ (n - Suc 0)) =  
  10.312           h * sumr 0 (n - Suc 0) (%p. (z ^ p) *  
  10.313 @@ -499,13 +507,14 @@
  10.314  apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
  10.315  apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
  10.316                  sumdiff lemma_termdiff1 sumr_mult)
  10.317 -apply (auto intro!: sumr_subst simp add: real_diff_def real_add_assoc)
  10.318 +apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
  10.319  apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
  10.320  apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
  10.321                   del: sumr_Suc realpow_Suc)
  10.322  done
  10.323  
  10.324 -lemma lemma_termdiff3: "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
  10.325 +lemma lemma_termdiff3:
  10.326 +     "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
  10.327        ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
  10.328            \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
  10.329  apply (subst lemma_termdiff2, assumption)
  10.330 @@ -524,7 +533,7 @@
  10.331  apply (simp (no_asm_simp) add: power_add del: sumr_Suc)
  10.332  apply (auto intro!: mult_mono simp del: sumr_Suc)
  10.333  apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc)
  10.334 -apply (rule_tac j = "real (Suc d) * (K ^ d) " in real_le_trans)
  10.335 +apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
  10.336  apply (subgoal_tac [2] "0 \<le> K")
  10.337  apply (drule_tac [2] n = d in zero_le_power)
  10.338  apply (auto simp del: sumr_Suc)
  10.339 @@ -537,29 +546,28 @@
  10.340    "[| 0 < k;  
  10.341        (\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>) |]  
  10.342     ==> f -- 0 --> 0"
  10.343 -apply (unfold LIM_def, auto)
  10.344 +apply (simp add: LIM_def, auto)
  10.345  apply (subgoal_tac "0 \<le> K")
  10.346 -apply (drule_tac [2] x = "k/2" in spec)
  10.347 -apply (frule_tac [2] real_less_half_sum)
  10.348 -apply (drule_tac [2] real_gt_half_sum)
  10.349 -apply (auto simp add: abs_eqI2)
  10.350 -apply (rule_tac [2] c = "k/2" in mult_right_le_imp_le)
  10.351 -apply (auto intro: abs_ge_zero [THEN real_le_trans])
  10.352 + prefer 2
  10.353 + apply (drule_tac x = "k/2" in spec)
  10.354 +apply (simp add: ); 
  10.355 + apply (subgoal_tac "0 \<le> K*k", simp add: zero_le_mult_iff) 
  10.356 + apply (force intro: order_trans [of _ "\<bar>f (k / 2)\<bar> * 2"]) 
  10.357  apply (drule real_le_imp_less_or_eq, auto)
  10.358 -apply (subgoal_tac "0 < (r * inverse K) * inverse 2")
  10.359 -apply (rule_tac [2] real_mult_order)+
  10.360 -apply (drule_tac ?d1.0 = "r * inverse K * inverse 2" and ?d2.0 = k in real_lbound_gt_zero)
  10.361 -apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff)
  10.362 -apply (rule_tac [2] y="\<bar>f (k / 2)\<bar> * 2" in order_trans, auto)
  10.363 +apply (subgoal_tac "0 < (r * inverse K) / 2")
  10.364 +apply (drule_tac ?d1.0 = "(r * inverse K) / 2" and ?d2.0 = k in real_lbound_gt_zero)
  10.365 +apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff zero_less_divide_iff)
  10.366  apply (rule_tac x = e in exI, auto)
  10.367  apply (rule_tac y = "K * \<bar>x\<bar>" in order_le_less_trans)
  10.368 -apply (rule_tac [2] y = "K * e" in order_less_trans)
  10.369 -apply (rule_tac [3] c = "inverse K" in mult_right_less_imp_less, force)
  10.370 +apply (force ); 
  10.371 +apply (rule_tac y = "K * e" in order_less_trans)
  10.372  apply (simp add: mult_less_cancel_left)
  10.373 +apply (rule_tac c = "inverse K" in mult_right_less_imp_less)
  10.374  apply (auto simp add: mult_ac)
  10.375  done
  10.376  
  10.377 -lemma lemma_termdiff5: "[| 0 < k;  
  10.378 +lemma lemma_termdiff5:
  10.379 +     "[| 0 < k;  
  10.380              summable f;  
  10.381              \<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k -->  
  10.382                      (\<forall>n. abs(g(h) (n::nat)) \<le> (f(n) * \<bar>h\<bar>)) |]  
  10.383 @@ -602,7 +610,7 @@
  10.384  apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
  10.385  apply (rule_tac [2] x = K in powser_insidea, auto)
  10.386  apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
  10.387 -apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eqI1], auto)
  10.388 +apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eq], auto)
  10.389  apply (simp add: diffs_def mult_assoc [symmetric])
  10.390  apply (subgoal_tac
  10.391          "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
  10.392 @@ -640,7 +648,8 @@
  10.393  apply (drule abs_ge_zero [THEN order_le_less_trans])
  10.394  apply (simp add: mult_assoc)
  10.395  apply (rule mult_left_mono)
  10.396 -apply (rule add_commute [THEN subst])
  10.397 + prefer 2 apply arith 
  10.398 +apply (subst add_commute)
  10.399  apply (simp (no_asm) add: mult_assoc [symmetric])
  10.400  apply (rule lemma_termdiff3)
  10.401  apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
  10.402 @@ -654,8 +663,8 @@
  10.403          \<bar>x\<bar> < \<bar>K\<bar> |]  
  10.404       ==> DERIV (%x. suminf (%n. c(n) * (x ^ n)))  x :>  
  10.405               suminf (%n. (diffs c)(n) * (x ^ n))"
  10.406 -apply (unfold deriv_def)
  10.407 -apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h) " in LIM_trans)
  10.408 +apply (simp add: deriv_def)
  10.409 +apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h)" in LIM_trans)
  10.410  apply (simp add: LIM_def, safe)
  10.411  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
  10.412  apply (auto simp add: less_diff_eq)
  10.413 @@ -666,11 +675,11 @@
  10.414  apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
  10.415  apply (auto simp add: add_commute)
  10.416  apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
  10.417 -apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
  10.418 +apply (drule_tac x = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
  10.419  apply (rule sums_unique)
  10.420  apply (simp add: diff_def divide_inverse add_ac mult_ac)
  10.421  apply (rule LIM_zero_cancel)
  10.422 -apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)
  10.423 +apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0)))))" in LIM_trans)
  10.424   prefer 2 apply (blast intro: termdiffs_aux) 
  10.425  apply (simp add: LIM_def, safe)
  10.426  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
  10.427 @@ -686,12 +695,12 @@
  10.428  apply (auto intro!: summable_sums)
  10.429  apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
  10.430  apply (auto simp add: add_commute)
  10.431 -apply (frule_tac x = " (%n. c n * (xa + x) ^ n) " and y = " (%n. c n * x ^ n) " in sums_diff, assumption)
  10.432 +apply (frule_tac x = "(%n. c n * (xa + x) ^ n) " and y = "(%n. c n * x ^ n)" in sums_diff, assumption)
  10.433  apply (simp add: suminf_diff [OF sums_summable sums_summable] 
  10.434                 right_diff_distrib [symmetric])
  10.435 -apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
  10.436 +apply (frule_tac x = "(%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
  10.437  apply (simp add: sums_summable [THEN suminf_mult2])
  10.438 -apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
  10.439 +apply (frule_tac x = "(%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = "(%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
  10.440  apply assumption
  10.441  apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
  10.442  apply (rule_tac f = suminf in arg_cong)
  10.443 @@ -704,13 +713,7 @@
  10.444  
  10.445  lemma exp_fdiffs: 
  10.446        "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
  10.447 -apply (unfold diffs_def)
  10.448 -apply (rule ext)
  10.449 -apply (subst fact_Suc)
  10.450 -apply (subst real_of_nat_mult)
  10.451 -apply (subst inverse_mult_distrib)
  10.452 -apply (auto simp add: mult_assoc [symmetric])
  10.453 -done
  10.454 +by (simp add: diffs_def mult_assoc [symmetric] del: mult_Suc)
  10.455  
  10.456  lemma sin_fdiffs: 
  10.457        "diffs(%n. if even n then 0  
  10.458 @@ -718,13 +721,8 @@
  10.459         = (%n. if even n then  
  10.460                   (- 1) ^ (n div 2)/(real (fact n))  
  10.461                else 0)"
  10.462 -apply (unfold diffs_def real_divide_def)
  10.463 -apply (rule ext)
  10.464 -apply (subst fact_Suc)
  10.465 -apply (subst real_of_nat_mult)
  10.466 -apply (subst even_nat_Suc)
  10.467 -apply (subst inverse_mult_distrib, auto)
  10.468 -done
  10.469 +by (auto intro!: ext 
  10.470 +         simp add: diffs_def divide_inverse simp del: mult_Suc)
  10.471  
  10.472  lemma sin_fdiffs2: 
  10.473         "diffs(%n. if even n then 0  
  10.474 @@ -732,24 +730,17 @@
  10.475         = (if even n then  
  10.476                   (- 1) ^ (n div 2)/(real (fact n))  
  10.477                else 0)"
  10.478 -apply (unfold diffs_def real_divide_def)
  10.479 -apply (subst fact_Suc)
  10.480 -apply (subst real_of_nat_mult)
  10.481 -apply (subst even_nat_Suc)
  10.482 -apply (subst inverse_mult_distrib, auto)
  10.483 -done
  10.484 +by (auto intro!: ext 
  10.485 +         simp add: diffs_def divide_inverse simp del: mult_Suc)
  10.486  
  10.487  lemma cos_fdiffs: 
  10.488        "diffs(%n. if even n then  
  10.489                   (- 1) ^ (n div 2)/(real (fact n)) else 0)  
  10.490         = (%n. - (if even n then 0  
  10.491             else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
  10.492 -apply (unfold diffs_def real_divide_def)
  10.493 -apply (rule ext)
  10.494 -apply (subst fact_Suc)
  10.495 -apply (subst real_of_nat_mult)
  10.496 -apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
  10.497 -done
  10.498 +by (auto intro!: ext 
  10.499 +         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
  10.500 +         simp del: mult_Suc)
  10.501  
  10.502  
  10.503  lemma cos_fdiffs2: 
  10.504 @@ -757,11 +748,9 @@
  10.505                   (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
  10.506         = - (if even n then 0  
  10.507             else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
  10.508 -apply (unfold diffs_def real_divide_def)
  10.509 -apply (subst fact_Suc)
  10.510 -apply (subst real_of_nat_mult) 
  10.511 -apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
  10.512 -done
  10.513 +by (auto intro!: ext 
  10.514 +         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
  10.515 +         simp del: mult_Suc)
  10.516  
  10.517  text{*Now at last we can get the derivatives of exp, sin and cos*}
  10.518  
  10.519 @@ -775,10 +764,10 @@
  10.520  by (auto intro!: ext simp add: exp_def)
  10.521  
  10.522  lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
  10.523 -apply (unfold exp_def)
  10.524 +apply (simp add: exp_def)
  10.525  apply (subst lemma_exp_ext)
  10.526  apply (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n) ")
  10.527 -apply (rule_tac [2] K = "1 + \<bar>x\<bar> " in termdiffs)
  10.528 +apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
  10.529  apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
  10.530  done
  10.531  
  10.532 @@ -796,17 +785,17 @@
  10.533  by (auto intro!: ext simp add: cos_def)
  10.534  
  10.535  lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
  10.536 -apply (unfold cos_def)
  10.537 +apply (simp add: cos_def)
  10.538  apply (subst lemma_sin_ext)
  10.539  apply (auto simp add: sin_fdiffs2 [symmetric])
  10.540 -apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
  10.541 +apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
  10.542  apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
  10.543  done
  10.544  
  10.545  lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  10.546  apply (subst lemma_cos_ext)
  10.547  apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
  10.548 -apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
  10.549 +apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
  10.550  apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
  10.551  done
  10.552  
  10.553 @@ -824,9 +813,9 @@
  10.554  
  10.555  lemma exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> exp(x)"
  10.556  apply (drule real_le_imp_less_or_eq, auto)
  10.557 -apply (unfold exp_def)
  10.558 +apply (simp add: exp_def)
  10.559  apply (rule real_le_trans)
  10.560 -apply (rule_tac [2] n = 2 and f = " (%n. inverse (real (fact n)) * x ^ n) " in series_pos_le)
  10.561 +apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
  10.562  apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff)
  10.563  done
  10.564  
  10.565 @@ -902,7 +891,7 @@
  10.566  by (auto intro: positive_imp_inverse_positive)
  10.567  
  10.568  lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
  10.569 -by (auto simp add: abs_eqI2)
  10.570 +by auto
  10.571  
  10.572  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
  10.573  apply (induct_tac "n")
  10.574 @@ -910,7 +899,7 @@
  10.575  done
  10.576  
  10.577  lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
  10.578 -apply (unfold real_diff_def real_divide_def)
  10.579 +apply (simp add: diff_minus divide_inverse)
  10.580  apply (simp (no_asm) add: exp_add exp_minus)
  10.581  done
  10.582  
  10.583 @@ -992,7 +981,7 @@
  10.584  
  10.585  lemma ln_div: 
  10.586      "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"
  10.587 -apply (unfold real_divide_def)
  10.588 +apply (simp add: divide_inverse)
  10.589  apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse)
  10.590  done
  10.591  
  10.592 @@ -1086,9 +1075,9 @@
  10.593  by (auto intro: series_zero)
  10.594  
  10.595  lemma cos_zero [simp]: "cos 0 = 1"
  10.596 -apply (unfold cos_def)
  10.597 +apply (simp add: cos_def)
  10.598  apply (rule sums_unique [symmetric])
  10.599 -apply (cut_tac n = 1 and f = " (%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n) " in lemma_series_zero2)
  10.600 +apply (cut_tac n = 1 and f = "(%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2)
  10.601  apply auto
  10.602  done
  10.603  
  10.604 @@ -1137,7 +1126,8 @@
  10.605  done
  10.606  
  10.607  (* most useful *)
  10.608 -lemma DERIV_cos_cos_mult3 [simp]: "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
  10.609 +lemma DERIV_cos_cos_mult3 [simp]:
  10.610 +     "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
  10.611  apply (rule lemma_DERIV_subst)
  10.612  apply (rule DERIV_cos_cos_mult2, auto)
  10.613  done
  10.614 @@ -1145,12 +1135,13 @@
  10.615  lemma DERIV_sin_circle_all: 
  10.616       "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
  10.617               (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
  10.618 -apply (unfold real_diff_def, safe)
  10.619 -apply (rule DERIV_add)
  10.620 +apply (simp only: diff_minus, safe)
  10.621 +apply (rule DERIV_add) 
  10.622  apply (auto simp add: numeral_2_eq_2)
  10.623  done
  10.624  
  10.625 -lemma DERIV_sin_circle_all_zero [simp]: "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
  10.626 +lemma DERIV_sin_circle_all_zero [simp]:
  10.627 +     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
  10.628  by (cut_tac DERIV_sin_circle_all, auto)
  10.629  
  10.630  lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
  10.631 @@ -1169,7 +1160,7 @@
  10.632  done
  10.633  
  10.634  lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
  10.635 -apply (rule_tac a1 = "(cos x)\<twosuperior> " in add_right_cancel [THEN iffD1])
  10.636 +apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
  10.637  apply (simp del: realpow_Suc)
  10.638  done
  10.639  
  10.640 @@ -1220,23 +1211,26 @@
  10.641  lemma DERIV_fun_pow: "DERIV g x :> m ==>  
  10.642        DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  10.643  apply (rule lemma_DERIV_subst)
  10.644 -apply (rule_tac f = " (%x. x ^ n) " in DERIV_chain2)
  10.645 +apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
  10.646  apply (rule DERIV_pow, auto)
  10.647  done
  10.648  
  10.649 -lemma DERIV_fun_exp: "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
  10.650 +lemma DERIV_fun_exp:
  10.651 +     "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
  10.652  apply (rule lemma_DERIV_subst)
  10.653  apply (rule_tac f = exp in DERIV_chain2)
  10.654  apply (rule DERIV_exp, auto)
  10.655  done
  10.656  
  10.657 -lemma DERIV_fun_sin: "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
  10.658 +lemma DERIV_fun_sin:
  10.659 +     "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
  10.660  apply (rule lemma_DERIV_subst)
  10.661  apply (rule_tac f = sin in DERIV_chain2)
  10.662  apply (rule DERIV_sin, auto)
  10.663  done
  10.664  
  10.665 -lemma DERIV_fun_cos: "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
  10.666 +lemma DERIV_fun_cos:
  10.667 +     "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
  10.668  apply (rule lemma_DERIV_subst)
  10.669  apply (rule_tac f = cos in DERIV_chain2)
  10.670  apply (rule DERIV_cos, auto)
  10.671 @@ -1250,13 +1244,14 @@
  10.672                      DERIV_Id DERIV_const DERIV_cos
  10.673  
  10.674  (* lemma *)
  10.675 -lemma lemma_DERIV_sin_cos_add: "\<forall>x.  
  10.676 +lemma lemma_DERIV_sin_cos_add:
  10.677 +     "\<forall>x.  
  10.678           DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
  10.679                 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
  10.680  apply (safe, rule lemma_DERIV_subst)
  10.681  apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  10.682    --{*replaces the old @{text DERIV_tac}*}
  10.683 -apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
  10.684 +apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
  10.685  done
  10.686  
  10.687  lemma sin_cos_add [simp]:
  10.688 @@ -1283,7 +1278,7 @@
  10.689      "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
  10.690  apply (safe, rule lemma_DERIV_subst)
  10.691  apply (best intro!: DERIV_intros intro: DERIV_chain2) 
  10.692 -apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
  10.693 +apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
  10.694  done
  10.695  
  10.696  lemma sin_cos_minus [simp]: 
  10.697 @@ -1306,7 +1301,7 @@
  10.698  done
  10.699  
  10.700  lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
  10.701 -apply (unfold real_diff_def)
  10.702 +apply (simp add: diff_minus)
  10.703  apply (simp (no_asm) add: sin_add)
  10.704  done
  10.705  
  10.706 @@ -1314,7 +1309,7 @@
  10.707  by (simp add: sin_diff mult_commute)
  10.708  
  10.709  lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
  10.710 -apply (unfold real_diff_def)
  10.711 +apply (simp add: diff_minus)
  10.712  apply (simp (no_asm) add: cos_add)
  10.713  done
  10.714  
  10.715 @@ -1431,7 +1426,7 @@
  10.716  apply (drule sums_minus)
  10.717  apply (rule neg_less_iff_less [THEN iffD1]) 
  10.718  apply (frule sums_unique, auto)
  10.719 -apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)
  10.720 +apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n)))" in order_less_trans)
  10.721  apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
  10.722  apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
  10.723  apply (rule sumr_pos_lt_pair)
  10.724 @@ -1502,8 +1497,8 @@
  10.725  declare pi_half_less_two [THEN order_less_imp_le, simp]
  10.726  
  10.727  lemma pi_gt_zero [simp]: "0 < pi"
  10.728 -apply (rule_tac c="inverse 2" in mult_less_imp_less_right) 
  10.729 -apply (cut_tac pi_half_gt_zero, simp_all)
  10.730 +apply (insert pi_half_gt_zero) 
  10.731 +apply (simp add: ); 
  10.732  done
  10.733  
  10.734  lemma pi_neq_zero [simp]: "pi \<noteq> 0"
  10.735 @@ -1533,32 +1528,24 @@
  10.736  by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
  10.737  
  10.738  lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  10.739 -apply (unfold real_diff_def)
  10.740 -apply (simp (no_asm) add: cos_add)
  10.741 -done
  10.742 +by (simp add: diff_minus cos_add)
  10.743  
  10.744  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
  10.745 -apply (simp (no_asm) add: cos_add)
  10.746 -done
  10.747 +by (simp add: cos_add)
  10.748  declare minus_sin_cos_eq [symmetric, simp]
  10.749  
  10.750  lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
  10.751 -apply (unfold real_diff_def)
  10.752 -apply (simp (no_asm) add: sin_add)
  10.753 -done
  10.754 +by (simp add: diff_minus sin_add)
  10.755  declare sin_cos_eq [symmetric, simp] cos_sin_eq [symmetric, simp]
  10.756  
  10.757  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
  10.758 -apply (simp (no_asm) add: sin_add)
  10.759 -done
  10.760 +by (simp add: sin_add)
  10.761  
  10.762  lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
  10.763 -apply (simp (no_asm) add: sin_add)
  10.764 -done
  10.765 +by (simp add: sin_add)
  10.766  
  10.767  lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
  10.768 -apply (simp (no_asm) add: cos_add)
  10.769 -done
  10.770 +by (simp add: cos_add)
  10.771  
  10.772  lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
  10.773  by (simp add: sin_add cos_double)
  10.774 @@ -1585,8 +1572,7 @@
  10.775  by (simp add: cos_double)
  10.776  
  10.777  lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
  10.778 -apply (simp (no_asm))
  10.779 -done
  10.780 +by simp
  10.781  
  10.782  lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
  10.783  apply (rule sin_gt_zero, assumption)
  10.784 @@ -1658,7 +1644,7 @@
  10.785  apply (simp del: minus_sin_cos_eq [symmetric])
  10.786  apply (cut_tac y="-y" in cos_total, simp) apply simp 
  10.787  apply (erule ex1E)
  10.788 -apply (rule_tac a = "x - (pi/2) " in ex1I)
  10.789 +apply (rule_tac a = "x - (pi/2)" in ex1I)
  10.790  apply (simp (no_asm) add: real_add_assoc)
  10.791  apply (rotate_tac 3)
  10.792  apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all) 
  10.793 @@ -1677,7 +1663,8 @@
  10.794  
  10.795  (* Pre Isabelle99-2 proof was simpler- numerals arithmetic 
  10.796     now causes some unwanted re-arrangements of literals!   *)
  10.797 -lemma cos_zero_lemma: "[| 0 \<le> x; cos x = 0 |] ==>  
  10.798 +lemma cos_zero_lemma:
  10.799 +     "[| 0 \<le> x; cos x = 0 |] ==>  
  10.800        \<exists>n::nat. ~even n & x = real n * (pi/2)"
  10.801  apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
  10.802  apply (subgoal_tac "0 \<le> x - real n * pi & 
  10.803 @@ -1691,11 +1678,12 @@
  10.804  apply (drule_tac x = "x - real n * pi" in spec)
  10.805  apply (drule_tac x = "pi/2" in spec)
  10.806  apply (simp add: cos_diff)
  10.807 -apply (rule_tac x = "Suc (2 * n) " in exI)
  10.808 +apply (rule_tac x = "Suc (2 * n)" in exI)
  10.809  apply (simp add: real_of_nat_Suc left_distrib, auto)
  10.810  done
  10.811  
  10.812 -lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>  
  10.813 +lemma sin_zero_lemma:
  10.814 +     "[| 0 \<le> x; sin x = 0 |] ==>  
  10.815        \<exists>n::nat. even n & x = real n * (pi/2)"
  10.816  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  10.817   apply (clarify, rule_tac x = "n - 1" in exI)
  10.818 @@ -1705,7 +1693,8 @@
  10.819  done
  10.820  
  10.821  
  10.822 -lemma cos_zero_iff: "(cos x = 0) =  
  10.823 +lemma cos_zero_iff:
  10.824 +     "(cos x = 0) =  
  10.825        ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |    
  10.826         (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  10.827  apply (rule iffI)
  10.828 @@ -1718,7 +1707,8 @@
  10.829  done
  10.830  
  10.831  (* ditto: but to a lesser extent *)
  10.832 -lemma sin_zero_iff: "(sin x = 0) =  
  10.833 +lemma sin_zero_iff:
  10.834 +     "(sin x = 0) =  
  10.835        ((\<exists>n::nat. even n & (x = real n * (pi/2))) |    
  10.836         (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
  10.837  apply (rule iffI)
  10.838 @@ -1750,28 +1740,32 @@
  10.839  lemma lemma_tan_add1: 
  10.840        "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
  10.841          ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"
  10.842 -apply (unfold tan_def real_divide_def)
  10.843 -apply (auto simp del: inverse_mult_distrib simp add: inverse_mult_distrib [symmetric] mult_ac)
  10.844 +apply (simp add: tan_def divide_inverse)
  10.845 +apply (auto simp del: inverse_mult_distrib 
  10.846 +            simp add: inverse_mult_distrib [symmetric] mult_ac)
  10.847  apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
  10.848 -apply (auto simp del: inverse_mult_distrib simp add: mult_assoc left_diff_distrib cos_add)
  10.849 +apply (auto simp del: inverse_mult_distrib 
  10.850 +            simp add: mult_assoc left_diff_distrib cos_add)
  10.851  done
  10.852  
  10.853  lemma add_tan_eq: 
  10.854        "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
  10.855         ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
  10.856 -apply (unfold tan_def)
  10.857 +apply (simp add: tan_def)
  10.858  apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
  10.859  apply (auto simp add: mult_assoc left_distrib)
  10.860  apply (simp (no_asm) add: sin_add)
  10.861  done
  10.862  
  10.863 -lemma tan_add: "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]  
  10.864 +lemma tan_add:
  10.865 +     "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]  
  10.866        ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  10.867  apply (simp (no_asm_simp) add: add_tan_eq lemma_tan_add1)
  10.868  apply (simp add: tan_def)
  10.869  done
  10.870  
  10.871 -lemma tan_double: "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]  
  10.872 +lemma tan_double:
  10.873 +     "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]  
  10.874        ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
  10.875  apply (insert tan_add [of x x]) 
  10.876  apply (simp add: mult_2 [symmetric])  
  10.877 @@ -1779,9 +1773,7 @@
  10.878  done
  10.879  
  10.880  lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  10.881 -apply (unfold tan_def real_divide_def)
  10.882 -apply (auto intro!: sin_gt_zero2 cos_gt_zero_pi intro!: real_mult_order positive_imp_inverse_positive)
  10.883 -done
  10.884 +by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi) 
  10.885  
  10.886  lemma tan_less_zero: 
  10.887    assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
  10.888 @@ -1801,9 +1793,8 @@
  10.889  by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
  10.890  
  10.891  lemma LIM_cos_div_sin [simp]: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
  10.892 -apply (unfold real_divide_def)
  10.893  apply (subgoal_tac "(\<lambda>x. cos x * inverse (sin x)) -- pi * inverse 2 --> 0*1")
  10.894 -apply simp 
  10.895 +apply (simp add: divide_inverse [symmetric])
  10.896  apply (rule LIM_mult2)
  10.897  apply (rule_tac [2] inverse_1 [THEN subst])
  10.898  apply (rule_tac [2] LIM_inverse)
  10.899 @@ -1817,19 +1808,15 @@
  10.900  apply (simp only: LIM_def)
  10.901  apply (drule_tac x = "inverse y" in spec, safe, force)
  10.902  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
  10.903 -apply (rule_tac x = " (pi/2) - e" in exI)
  10.904 +apply (rule_tac x = "(pi/2) - e" in exI)
  10.905  apply (simp (no_asm_simp))
  10.906 -apply (drule_tac x = " (pi/2) - e" in spec)
  10.907 -apply (auto simp add: abs_eqI2 tan_def)
  10.908 +apply (drule_tac x = "(pi/2) - e" in spec)
  10.909 +apply (auto simp add: tan_def)
  10.910  apply (rule inverse_less_iff_less [THEN iffD1])
  10.911  apply (auto simp add: divide_inverse)
  10.912 -apply (rule real_mult_order)
  10.913 -apply (subgoal_tac [3] "0 < sin e")
  10.914 -apply (subgoal_tac [3] "0 < cos e")
  10.915 -apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: inverse_mult_distrib abs_mult)
  10.916 -apply (drule_tac a = "cos e" in positive_imp_inverse_positive)
  10.917 -apply (drule_tac x = "inverse (cos e) " in abs_eqI2)
  10.918 -apply (auto dest!: abs_eqI2 simp add: mult_ac)
  10.919 +apply (rule real_mult_order) 
  10.920 +apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
  10.921 +apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute) 
  10.922  done
  10.923  
  10.924  lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
  10.925 @@ -1865,16 +1852,18 @@
  10.926  	    simp add: cos_gt_zero_pi [THEN real_not_refl2, THEN not_sym]) 
  10.927  done
  10.928  
  10.929 -lemma arcsin_pi: "[| -1 \<le> y; y \<le> 1 |]  
  10.930 +lemma arcsin_pi:
  10.931 +     "[| -1 \<le> y; y \<le> 1 |]  
  10.932        ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
  10.933  apply (drule sin_total, assumption)
  10.934  apply (erule ex1E)
  10.935 -apply (unfold arcsin_def)
  10.936 +apply (simp add: arcsin_def)
  10.937  apply (rule someI2, blast) 
  10.938  apply (force intro: order_trans) 
  10.939  done
  10.940  
  10.941 -lemma arcsin: "[| -1 \<le> y; y \<le> 1 |]  
  10.942 +lemma arcsin:
  10.943 +     "[| -1 \<le> y; y \<le> 1 |]  
  10.944        ==> -(pi/2) \<le> arcsin y &  
  10.945             arcsin y \<le> pi/2 & sin(arcsin y) = y"
  10.946  apply (unfold arcsin_def)
  10.947 @@ -1912,9 +1901,10 @@
  10.948  apply (rule sin_total, auto)
  10.949  done
  10.950  
  10.951 -lemma arcos: "[| -1 \<le> y; y \<le> 1 |]  
  10.952 +lemma arcos:
  10.953 +     "[| -1 \<le> y; y \<le> 1 |]  
  10.954        ==> 0 \<le> arcos y & arcos y \<le> pi & cos(arcos y) = y"
  10.955 -apply (unfold arcos_def)
  10.956 +apply (simp add: arcos_def)
  10.957  apply (drule cos_total, assumption)
  10.958  apply (fast intro: someI2)
  10.959  done
  10.960 @@ -1931,7 +1921,8 @@
  10.961  lemma arcos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcos y \<le> pi"
  10.962  by (blast dest: arcos)
  10.963  
  10.964 -lemma arcos_lt_bounded: "[| -1 < y; y < 1 |]  
  10.965 +lemma arcos_lt_bounded:
  10.966 +     "[| -1 < y; y < 1 |]  
  10.967        ==> 0 < arcos y & arcos y < pi"
  10.968  apply (frule order_less_imp_le)
  10.969  apply (frule_tac y = y in order_less_imp_le)
  10.970 @@ -1942,19 +1933,19 @@
  10.971  done
  10.972  
  10.973  lemma arcos_cos: "[|0 \<le> x; x \<le> pi |] ==> arcos(cos x) = x"
  10.974 -apply (unfold arcos_def)
  10.975 +apply (simp add: arcos_def)
  10.976  apply (auto intro!: some1_equality cos_total)
  10.977  done
  10.978  
  10.979  lemma arcos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arcos(cos x) = -x"
  10.980 -apply (unfold arcos_def)
  10.981 +apply (simp add: arcos_def)
  10.982  apply (auto intro!: some1_equality cos_total)
  10.983  done
  10.984  
  10.985  lemma arctan [simp]:
  10.986       "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
  10.987  apply (cut_tac y = y in tan_total)
  10.988 -apply (unfold arctan_def)
  10.989 +apply (simp add: arctan_def)
  10.990  apply (fast intro: someI2)
  10.991  done
  10.992  
  10.993 @@ -1999,16 +1990,16 @@
  10.994  done
  10.995  
  10.996  text{*NEEDED??*}
  10.997 -lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  
  10.998 -      cos (xa + 1 / 2 * real  (m) * pi)"
  10.999 -apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
 10.1000 -done
 10.1001 +lemma [simp]:
 10.1002 +     "sin (x + 1 / 2 * real (Suc m) * pi) =  
 10.1003 +      cos (x + 1 / 2 * real  (m) * pi)"
 10.1004 +by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
 10.1005  
 10.1006  text{*NEEDED??*}
 10.1007 -lemma [simp]: "sin (xa + real (Suc m) * pi / 2) =  
 10.1008 -      cos (xa + real (m) * pi / 2)"
 10.1009 -apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
 10.1010 -done
 10.1011 +lemma [simp]:
 10.1012 +     "sin (x + real (Suc m) * pi / 2) =  
 10.1013 +      cos (x + real (m) * pi / 2)"
 10.1014 +by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 10.1015  
 10.1016  lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
 10.1017  apply (rule lemma_DERIV_subst)
 10.1018 @@ -2023,7 +2014,7 @@
 10.1019  
 10.1020  lemma sin_cos_npi2 [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
 10.1021  apply (cut_tac m = n in sin_cos_npi)
 10.1022 -apply (simp only: real_of_nat_Suc left_distrib divide_inverse, auto)
 10.1023 +apply (simp only: real_of_nat_Suc left_distrib add_divide_distrib, auto)
 10.1024  done
 10.1025  
 10.1026  lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
 10.1027 @@ -2045,17 +2036,17 @@
 10.1028  done
 10.1029  
 10.1030  (*NEEDED??*)
 10.1031 -lemma [simp]: "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
 10.1032 +lemma [simp]:
 10.1033 +     "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
 10.1034  apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
 10.1035  done
 10.1036  
 10.1037  (*NEEDED??*)
 10.1038  lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
 10.1039 -apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
 10.1040 -done
 10.1041 +by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
 10.1042  
 10.1043  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
 10.1044 -by (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
 10.1045 +by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
 10.1046  
 10.1047  lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
 10.1048  apply (rule lemma_DERIV_subst)
 10.1049 @@ -2085,7 +2076,8 @@
 10.1050  by (cut_tac x = x in sin_cos_squared_add3, auto)
 10.1051  
 10.1052  
 10.1053 -lemma real_root_less_mono: "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
 10.1054 +lemma real_root_less_mono:
 10.1055 +     "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
 10.1056  apply (frule order_le_less_trans, assumption)
 10.1057  apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst])
 10.1058  apply (rotate_tac 1, assumption)
 10.1059 @@ -2098,44 +2090,51 @@
 10.1060  apply (assumption, assumption)
 10.1061  apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq)
 10.1062  apply auto
 10.1063 -apply (drule_tac f = "%x. x ^ (Suc n) " in arg_cong)
 10.1064 +apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong)
 10.1065  apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc)
 10.1066  done
 10.1067  
 10.1068 -lemma real_root_le_mono: "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
 10.1069 +lemma real_root_le_mono:
 10.1070 +     "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
 10.1071  apply (drule_tac y = y in order_le_imp_less_or_eq)
 10.1072  apply (auto dest: real_root_less_mono intro: order_less_imp_le)
 10.1073  done
 10.1074  
 10.1075 -lemma real_root_less_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
 10.1076 +lemma real_root_less_iff [simp]:
 10.1077 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
 10.1078  apply (auto intro: real_root_less_mono)
 10.1079  apply (rule ccontr, drule linorder_not_less [THEN iffD1])
 10.1080  apply (drule_tac x = y and n = n in real_root_le_mono, auto)
 10.1081  done
 10.1082  
 10.1083 -lemma real_root_le_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
 10.1084 +lemma real_root_le_iff [simp]:
 10.1085 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
 10.1086  apply (auto intro: real_root_le_mono)
 10.1087  apply (simp (no_asm) add: linorder_not_less [symmetric])
 10.1088  apply auto
 10.1089  apply (drule_tac x = y and n = n in real_root_less_mono, auto)
 10.1090  done
 10.1091  
 10.1092 -lemma real_root_eq_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
 10.1093 +lemma real_root_eq_iff [simp]:
 10.1094 +     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
 10.1095  apply (auto intro!: order_antisym)
 10.1096  apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
 10.1097  apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
 10.1098  done
 10.1099  
 10.1100 -lemma real_root_pos_unique: "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
 10.1101 +lemma real_root_pos_unique:
 10.1102 +     "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
 10.1103  by (auto dest: real_root_pos2 simp del: realpow_Suc)
 10.1104  
 10.1105 -lemma real_root_mult: "[| 0 \<le> x; 0 \<le> y |] 
 10.1106 +lemma real_root_mult:
 10.1107 +     "[| 0 \<le> x; 0 \<le> y |] 
 10.1108        ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
 10.1109  apply (rule real_root_pos_unique)
 10.1110  apply (auto intro!: real_root_pos_pos_le simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 simp del: realpow_Suc)
 10.1111  done
 10.1112  
 10.1113 -lemma real_root_inverse: "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
 10.1114 +lemma real_root_inverse:
 10.1115 +     "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
 10.1116  apply (rule real_root_pos_unique)
 10.1117  apply (auto intro: real_root_pos_pos_le simp add: power_inverse [symmetric] real_root_pow_pos2 simp del: realpow_Suc)
 10.1118  done
 10.1119 @@ -2143,28 +2142,27 @@
 10.1120  lemma real_root_divide: 
 10.1121       "[| 0 \<le> x; 0 \<le> y |]  
 10.1122        ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"
 10.1123 -apply (unfold real_divide_def)
 10.1124 +apply (simp add: divide_inverse)
 10.1125  apply (auto simp add: real_root_mult real_root_inverse)
 10.1126  done
 10.1127  
 10.1128  lemma real_sqrt_less_mono: "[| 0 \<le> x; x < y |] ==> sqrt(x) < sqrt(y)"
 10.1129 -apply (unfold sqrt_def)
 10.1130 -apply (auto intro: real_root_less_mono)
 10.1131 -done
 10.1132 +by (simp add: sqrt_def)
 10.1133  
 10.1134  lemma real_sqrt_le_mono: "[| 0 \<le> x; x \<le> y |] ==> sqrt(x) \<le> sqrt(y)"
 10.1135 -apply (unfold sqrt_def)
 10.1136 -apply (auto intro: real_root_le_mono)
 10.1137 -done
 10.1138 -
 10.1139 -lemma real_sqrt_less_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
 10.1140 -by (unfold sqrt_def, auto)
 10.1141 -
 10.1142 -lemma real_sqrt_le_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
 10.1143 -by (unfold sqrt_def, auto)
 10.1144 -
 10.1145 -lemma real_sqrt_eq_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
 10.1146 -by (unfold sqrt_def, auto)
 10.1147 +by (simp add: sqrt_def)
 10.1148 +
 10.1149 +lemma real_sqrt_less_iff [simp]:
 10.1150 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
 10.1151 +by (simp add: sqrt_def)
 10.1152 +
 10.1153 +lemma real_sqrt_le_iff [simp]:
 10.1154 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
 10.1155 +by (simp add: sqrt_def)
 10.1156 +
 10.1157 +lemma real_sqrt_eq_iff [simp]:
 10.1158 +     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
 10.1159 +by (simp add: sqrt_def)
 10.1160  
 10.1161  lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
 10.1162  apply (rule real_sqrt_one [THEN subst], safe)
 10.1163 @@ -2178,7 +2176,7 @@
 10.1164  done
 10.1165  
 10.1166  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
 10.1167 -apply (unfold real_divide_def)
 10.1168 +apply (simp add: divide_inverse)
 10.1169  apply (case_tac "r=0")
 10.1170  apply (auto simp add: inverse_mult_distrib mult_ac)
 10.1171  done
 10.1172 @@ -2239,9 +2237,8 @@
 10.1173  
 10.1174  lemma lemma_real_divide_sqrt_ge_minus_one2:
 10.1175       "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
 10.1176 -apply (simp add: divide_const_simps); 
 10.1177 -apply (insert minus_le_real_sqrt_sumsq [of x y])
 10.1178 -apply arith;
 10.1179 +apply (simp add: divide_const_simps) 
 10.1180 +apply (insert minus_le_real_sqrt_sumsq [of x y], arith)
 10.1181  done
 10.1182  
 10.1183  lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1"
 10.1184 @@ -2257,12 +2254,10 @@
 10.1185  by (simp add: linorder_not_less)
 10.1186  
 10.1187  lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
 10.1188 -apply (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps); 
 10.1189 -done
 10.1190 +by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps)
 10.1191  
 10.1192  lemma cos_x_y_ge_minus_one1a [simp]: "-1 \<le> y / sqrt (x * x + y * y)"
 10.1193 -apply (subst add_commute, simp add: cos_x_y_ge_minus_one); 
 10.1194 -done
 10.1195 +by (subst add_commute, simp add: cos_x_y_ge_minus_one)
 10.1196  
 10.1197  lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1" 
 10.1198  apply (cut_tac x = x and y = 0 in linorder_less_linear, safe)
 10.1199 @@ -2317,8 +2312,8 @@
 10.1200  apply (rotate_tac [2] 2)
 10.1201  apply (frule_tac [2] left_inverse [THEN subst])
 10.1202  prefer 2 apply assumption
 10.1203 -apply (erule_tac [2] V = " (1 - z) * (x + y) = x / (x + y) * (x + y) " in thin_rl)
 10.1204 -apply (erule_tac [2] V = "1 - z = x / (x + y) " in thin_rl)
 10.1205 +apply (erule_tac [2] V = "(1 - z) * (x + y) = x / (x + y) * (x + y)" in thin_rl)
 10.1206 +apply (erule_tac [2] V = "1 - z = x / (x + y)" in thin_rl)
 10.1207  apply (auto simp add: mult_assoc)
 10.1208  apply (auto simp add: right_distrib left_diff_distrib)
 10.1209  done
 10.1210 @@ -2355,12 +2350,13 @@
 10.1211  done
 10.1212  
 10.1213  lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
 10.1214 -apply (unfold real_divide_def)
 10.1215 +apply (simp add: divide_inverse)
 10.1216  apply (frule_tac y3 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym, THEN nonzero_imp_inverse_nonzero])
 10.1217  apply (auto simp add: power2_eq_square)
 10.1218  done
 10.1219  
 10.1220 -lemma cos_x_y_disj: "[| x \<noteq> 0;  
 10.1221 +lemma cos_x_y_disj:
 10.1222 +     "[| x \<noteq> 0;  
 10.1223           sin xa = y / sqrt (x * x + y * y)  
 10.1224        |] ==>  cos xa = x / sqrt (x * x + y * y) |  
 10.1225                cos xa = - x / sqrt (x * x + y * y)"
 10.1226 @@ -2373,23 +2369,23 @@
 10.1227  done
 10.1228  
 10.1229  lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0"
 10.1230 -apply (case_tac "x = 0")
 10.1231 -apply (auto simp add: abs_eqI2)
 10.1232 +apply (case_tac "x = 0", auto)
 10.1233  apply (drule_tac y = y in real_sqrt_sum_squares_gt_zero3)
 10.1234  apply (auto simp add: zero_less_mult_iff divide_inverse power2_eq_square)
 10.1235  done
 10.1236  
 10.1237 -lemma polar_ex1: "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 10.1238 -apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
 10.1239 +lemma polar_ex1:
 10.1240 +     "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 10.1241 +apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
 10.1242  apply (rule_tac x = "arcos (x / sqrt (x * x + y * y))" in exI)
 10.1243  apply auto
 10.1244  apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
 10.1245  apply (auto simp add: power2_eq_square)
 10.1246 -apply (unfold arcos_def)
 10.1247 +apply (simp add: arcos_def)
 10.1248  apply (cut_tac x1 = x and y1 = y 
 10.1249         in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one])
 10.1250  apply (rule someI2_ex, blast)
 10.1251 -apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y) " in thin_rl)
 10.1252 +apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y)" in thin_rl)
 10.1253  apply (frule sin_x_y_disj, blast)
 10.1254  apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
 10.1255  apply (auto simp add: power2_eq_square)
 10.1256 @@ -2400,7 +2396,8 @@
 10.1257  lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
 10.1258  by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
 10.1259  
 10.1260 -lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 10.1261 +lemma polar_ex2:
 10.1262 +     "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 10.1263  apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
 10.1264  apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
 10.1265  apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI) 
 10.1266 @@ -2456,8 +2453,7 @@
 10.1267  done
 10.1268  
 10.1269  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
 10.1270 -apply (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
 10.1271 -done
 10.1272 +by (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
 10.1273  
 10.1274  lemma four_x_squared: 
 10.1275    fixes x::real
 10.1276 @@ -2479,7 +2475,7 @@
 10.1277  apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
 10.1278  done
 10.1279  
 10.1280 -declare real_sqrt_sum_squares_ge_zero [THEN abs_eqI1, simp]
 10.1281 +declare real_sqrt_sum_squares_ge_zero [THEN abs_eq, simp]
 10.1282  
 10.1283  
 10.1284  subsection{*A Few Theorems Involving Ln, Derivatives, etc.*}
 10.1285 @@ -2493,13 +2489,14 @@
 10.1286  apply (auto simp add: starfun hypreal_zero_def hypreal_less)
 10.1287  done
 10.1288  
 10.1289 -lemma hypreal_add_Infinitesimal_gt_zero: "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"
 10.1290 +lemma hypreal_add_Infinitesimal_gt_zero:
 10.1291 +     "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"
 10.1292  apply (rule_tac c1 = "-e" in add_less_cancel_right [THEN iffD1])
 10.1293  apply (auto intro: Infinitesimal_less_SReal)
 10.1294  done
 10.1295  
 10.1296  lemma NSDERIV_exp_ln_one: "0 < z ==> NSDERIV (%x. exp (ln x)) z :> 1"
 10.1297 -apply (unfold nsderiv_def NSLIM_def, auto)
 10.1298 +apply (simp add: nsderiv_def NSLIM_def, auto)
 10.1299  apply (rule ccontr)
 10.1300  apply (subgoal_tac "0 < hypreal_of_real z + h")
 10.1301  apply (drule STAR_exp_ln)
 10.1302 @@ -2511,14 +2508,16 @@
 10.1303  lemma DERIV_exp_ln_one: "0 < z ==> DERIV (%x. exp (ln x)) z :> 1"
 10.1304  by (auto intro: NSDERIV_exp_ln_one simp add: NSDERIV_DERIV_iff [symmetric])
 10.1305  
 10.1306 -lemma lemma_DERIV_ln2: "[| 0 < z; DERIV ln z :> l |] ==>  exp (ln z) * l = 1"
 10.1307 +lemma lemma_DERIV_ln2:
 10.1308 +     "[| 0 < z; DERIV ln z :> l |] ==>  exp (ln z) * l = 1"
 10.1309  apply (rule DERIV_unique)
 10.1310  apply (rule lemma_DERIV_ln)
 10.1311  apply (rule_tac [2] DERIV_exp_ln_one, auto)
 10.1312  done
 10.1313  
 10.1314 -lemma lemma_DERIV_ln3: "[| 0 < z; DERIV ln z :> l |] ==>  l = 1/(exp (ln z))"
 10.1315 -apply (rule_tac c1 = "exp (ln z) " in real_mult_left_cancel [THEN iffD1])
 10.1316 +lemma lemma_DERIV_ln3:
 10.1317 +     "[| 0 < z; DERIV ln z :> l |] ==>  l = 1/(exp (ln z))"
 10.1318 +apply (rule_tac c1 = "exp (ln z)" in real_mult_left_cancel [THEN iffD1])
 10.1319  apply (auto intro: lemma_DERIV_ln2)
 10.1320  done
 10.1321  
 10.1322 @@ -2529,7 +2528,8 @@
 10.1323  
 10.1324  (* need to rename second isCont_inverse *)
 10.1325  
 10.1326 -lemma isCont_inv_fun: "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
 10.1327 +lemma isCont_inv_fun:
 10.1328 +     "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
 10.1329           \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
 10.1330        ==> isCont g (f x)"
 10.1331  apply (simp (no_asm) add: isCont_iff LIM_def)
 10.1332 @@ -2563,7 +2563,8 @@
 10.1333  
 10.1334  
 10.1335  text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
 10.1336 -lemma LIM_fun_gt_zero: "[| f -- c --> l; 0 < l |]  
 10.1337 +lemma LIM_fun_gt_zero:
 10.1338 +     "[| f -- c --> l; 0 < l |]  
 10.1339           ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
 10.1340  apply (auto simp add: LIM_def)
 10.1341  apply (drule_tac x = "l/2" in spec, safe, force)
 10.1342 @@ -2571,8 +2572,9 @@
 10.1343  apply (auto simp only: abs_interval_iff)
 10.1344  done
 10.1345  
 10.1346 -lemma LIM_fun_less_zero: "[| f -- c --> l; l < 0 |]  
 10.1347 -         ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
 10.1348 +lemma LIM_fun_less_zero:
 10.1349 +     "[| f -- c --> l; l < 0 |]  
 10.1350 +      ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
 10.1351  apply (auto simp add: LIM_def)
 10.1352  apply (drule_tac x = "-l/2" in spec, safe, force)
 10.1353  apply (rule_tac x = s in exI)
    11.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Oct 04 15:28:03 2004 +0200
    11.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 05 15:30:50 2004 +0200
    11.3 @@ -465,7 +465,6 @@
    11.4    apply (rule exI)
    11.5    apply (rule exI)
    11.6    apply (subst xzgcda.simps, auto)
    11.7 -  apply (simp add: abs_if)
    11.8    done
    11.9  
   11.10  lemma xzgcd_correct_aux2:
   11.11 @@ -481,7 +480,6 @@
   11.12     apply (frule_tac a = "r'" in pos_mod_sign, auto)
   11.13    apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   11.14    apply (subst xzgcda.simps, auto)
   11.15 -  apply (simp add: abs_if)
   11.16    done
   11.17  
   11.18  lemma xzgcd_correct:
    12.1 --- a/src/HOL/OrderedGroup.thy	Mon Oct 04 15:28:03 2004 +0200
    12.2 +++ b/src/HOL/OrderedGroup.thy	Tue Oct 05 15:30:50 2004 +0200
    12.3 @@ -669,6 +669,16 @@
    12.4    show ?thesis by (simp add: abs_lattice join_eq_if)
    12.5  qed
    12.6  
    12.7 +lemma abs_eq [simp]:
    12.8 +  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
    12.9 +  shows  "0 \<le> a ==> abs a = a"
   12.10 +by (simp add: abs_if_lattice linorder_not_less [symmetric]) 
   12.11 +
   12.12 +lemma abs_minus_eq [simp]: 
   12.13 +  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
   12.14 +  shows "a < 0 ==> abs a = -a"
   12.15 +by (simp add: abs_if_lattice linorder_not_less [symmetric])
   12.16 +
   12.17  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
   12.18  proof -
   12.19    have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
    13.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 04 15:28:03 2004 +0200
    13.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Oct 05 15:30:50 2004 +0200
    13.3 @@ -230,7 +230,7 @@
    13.4  	by (simp add: right_diff_distrib)
    13.5        also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
    13.6            p (a \<cdot> (inverse a \<cdot> y + x0))"
    13.7 -        by (simp add: abs_homogenous abs_minus_eqI2)
    13.8 +        by (simp add: abs_homogenous)
    13.9        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   13.10          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   13.11        also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
   13.12 @@ -250,7 +250,7 @@
   13.13  	by (simp add: right_diff_distrib)
   13.14        also from gz x0 y'
   13.15        have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
   13.16 -        by (simp add: abs_homogenous abs_eqI2)
   13.17 +        by (simp add: abs_homogenous)
   13.18        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
   13.19          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
   13.20        also from nz y have "a * h (inverse a \<cdot> y) = h y"
    14.1 --- a/src/HOL/Real/RealDef.thy	Mon Oct 04 15:28:03 2004 +0200
    14.2 +++ b/src/HOL/Real/RealDef.thy	Tue Oct 05 15:30:50 2004 +0200
    14.3 @@ -810,16 +810,6 @@
    14.4  
    14.5  subsection{*Absolute Value Function for the Reals*}
    14.6  
    14.7 -text{*FIXME: these should go!*}
    14.8 -lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
    14.9 -by (simp add: abs_if)
   14.10 -
   14.11 -lemma abs_eqI2: "(0::real) < x ==> abs x = x"
   14.12 -by (simp add: abs_if)
   14.13 -
   14.14 -lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
   14.15 -by (simp add: abs_if linorder_not_less [symmetric])
   14.16 -
   14.17  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
   14.18  by (simp add: abs_if)
   14.19  
   14.20 @@ -834,7 +824,7 @@
   14.21  by (simp add: abs_if)
   14.22  
   14.23  lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
   14.24 -by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
   14.25 +by (simp add: real_of_nat_ge_zero)
   14.26  
   14.27  lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
   14.28  apply (simp add: linorder_not_less)
   14.29 @@ -857,27 +847,11 @@
   14.30  val real_less_half_sum = thm"real_less_half_sum";
   14.31  val real_gt_half_sum = thm"real_gt_half_sum";
   14.32  
   14.33 -val abs_eqI1 = thm"abs_eqI1";
   14.34 -val abs_eqI2 = thm"abs_eqI2";
   14.35 -val abs_minus_eqI2 = thm"abs_minus_eqI2";
   14.36 -val abs_ge_zero = thm"abs_ge_zero";
   14.37 -val abs_idempotent = thm"abs_idempotent";
   14.38 -val abs_eq_0 = thm"abs_eq_0";
   14.39 -val abs_ge_self = thm"abs_ge_self";
   14.40 -val abs_ge_minus_self = thm"abs_ge_minus_self";
   14.41 -val abs_mult = thm"abs_mult";
   14.42 -val abs_inverse = thm"abs_inverse";
   14.43 -val abs_triangle_ineq = thm"abs_triangle_ineq";
   14.44 -val abs_minus_cancel = thm"abs_minus_cancel";
   14.45 -val abs_minus_add_cancel = thm"abs_minus_add_cancel";
   14.46  val abs_interval_iff = thm"abs_interval_iff";
   14.47  val abs_le_interval_iff = thm"abs_le_interval_iff";
   14.48  val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
   14.49 -val abs_le_zero_iff = thm"abs_le_zero_iff";
   14.50  val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
   14.51  val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
   14.52 -
   14.53 -val abs_mult_less = thm"abs_mult_less";
   14.54  *}
   14.55  
   14.56  
    15.1 --- a/src/HOL/Real/RealPow.thy	Mon Oct 04 15:28:03 2004 +0200
    15.2 +++ b/src/HOL/Real/RealPow.thy	Tue Oct 05 15:30:50 2004 +0200
    15.3 @@ -51,7 +51,7 @@
    15.4  by (simp add: abs_mult)
    15.5  
    15.6  lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
    15.7 -by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc)
    15.8 +by (simp add: power_abs [symmetric] del: realpow_Suc)
    15.9  
   15.10  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
   15.11  by (insert power_increasing [of 0 n "2::real"], simp)
    16.1 --- a/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:28:03 2004 +0200
    16.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Oct 05 15:30:50 2004 +0200
    16.3 @@ -5,7 +5,7 @@
    16.4  
    16.5  header {* (Ordered) Rings and Fields *}
    16.6  
    16.7 -theory Ring_and_Field 
    16.8 +theory Ring_and_Field
    16.9  imports OrderedGroup
   16.10  begin
   16.11  
   16.12 @@ -1371,6 +1371,12 @@
   16.13  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
   16.14    by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
   16.15  
   16.16 +lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
   16.17 +by (simp add: abs_if linorder_not_less [symmetric]) 
   16.18 +
   16.19 +lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
   16.20 +by (simp add: abs_if linorder_not_less [symmetric])
   16.21 +
   16.22  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
   16.23  proof -
   16.24    let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"