--- a/src/HOL/Complex/NSCA.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy Tue Oct 05 15:30:50 2004 +0200
@@ -673,7 +673,7 @@
simp del: realpow_Suc)
apply (rule_tac y="abs(Z x)" in order_le_less_trans)
apply (drule_tac t = "Z x" in sym)
-apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
+apply (auto simp del: realpow_Suc)
done
(* same proof *)
@@ -691,7 +691,7 @@
apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
apply (rule_tac y="abs(Z x)" in order_le_less_trans)
apply (drule_tac t = "Z x" in sym)
-apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
+apply (auto simp del: realpow_Suc)
done
lemma hcomplex_capproxI:
--- a/src/HOL/Hyperreal/HTranscendental.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Tue Oct 05 15:30:50 2004 +0200
@@ -458,17 +458,12 @@
lemma starfun_ln_Infinitesimal_less_zero:
"[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
-apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
-apply (drule bspec [where x = 1])
-apply (auto simp add: abs_if)
-done
+by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
lemma starfun_ln_HInfinite_gt_zero:
"[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
-apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
-apply (drule bspec [where x = 1])
-apply (auto simp add: abs_if)
-done
+by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
+
(*
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
--- a/src/HOL/Hyperreal/HyperDef.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Oct 05 15:30:50 2004 +0200
@@ -623,20 +623,12 @@
"abs (Abs_hypreal (hyprel `` {X})) =
Abs_hypreal(hyprel `` {%n. abs (X n)})"
apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
-apply (ultra, arith)+
+apply ultra
+apply ultra
+apply arith
done
-
-lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
-by (auto dest: add_less_le_mono)
-
-text{*The precondition could be weakened to @{term "0\<le>x"}*}
-lemma hypreal_mult_less_mono:
- "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
- by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
-
-
subsection{*Existence of Infinite Hyperreal Number*}
lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
@@ -784,7 +776,6 @@
val hypreal_one_num = thm "hypreal_one_num";
val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
-val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono";
val Rep_hypreal_omega = thm"Rep_hypreal_omega";
val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
val lemma_finite_omega_set = thm"lemma_finite_omega_set";
--- a/src/HOL/Hyperreal/HyperPow.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Tue Oct 05 15:30:50 2004 +0200
@@ -216,6 +216,11 @@
lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)"
by (simp add: hyperpow_hrabs)
+text{*The precondition could be weakened to @{term "0\<le>x"}*}
+lemma hypreal_mult_less_mono:
+ "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
+ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
+
lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)"
apply (auto simp add: hyperpow_two)
apply (rule_tac y = "1*1" in order_le_less_trans)
--- a/src/HOL/Hyperreal/Integration.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Tue Oct 05 15:30:50 2004 +0200
@@ -430,9 +430,9 @@
apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
apply (rule add_mono)
apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
- prefer 2 apply (simp, arith)
+ prefer 2 apply simp
apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
-apply (drule_tac x = v in spec, simp, arith)
+apply (drule_tac x = v in spec, simp)
apply (drule_tac x = u in spec, auto, arith)
apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)
--- a/src/HOL/Hyperreal/MacLaurin.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Oct 05 15:30:50 2004 +0200
@@ -328,7 +328,7 @@
prefer 2 apply blast
apply (drule_tac [2] diff=diff in Maclaurin)
apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
-apply (rule_tac [!] x = t in exI, auto, arith+)
+apply (rule_tac [!] x = t in exI, auto)
done
lemma Maclaurin_all_lt_objl:
--- a/src/HOL/Hyperreal/NSA.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Tue Oct 05 15:30:50 2004 +0200
@@ -22,12 +22,12 @@
HInfinite :: "hypreal set"
"HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
- (* infinitely close *)
approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
+ --{*the `infinitely close' relation*}
"x @= y == (x + -y) \<in> Infinitesimal"
- (* standard part map *)
st :: "hypreal => hypreal"
+ --{*the standard part of a hyperreal*}
"st == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
monad :: "hypreal => hypreal set"
@@ -39,8 +39,8 @@
defs (overloaded)
- (*standard real numbers as a subset of the hyperreals*)
SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+ --{*the standard real numbers as a subset of the hyperreals*}
syntax (xsymbols)
approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
@@ -50,7 +50,7 @@
-subsection{*Closure Laws for Standard Reals*}
+subsection{*Closure Laws for the Standard Reals*}
lemma SReal_add [simp]:
"[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
@@ -78,12 +78,11 @@
apply (blast intro: hypreal_of_real_minus [symmetric])
done
-lemma SReal_minus_iff: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
+lemma SReal_minus_iff [simp]: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
apply auto
apply (erule_tac [2] SReal_minus)
apply (drule SReal_minus, auto)
done
-declare SReal_minus_iff [simp]
lemma SReal_add_cancel:
"[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
@@ -96,37 +95,32 @@
apply (auto simp add: hypreal_of_real_hrabs)
done
-lemma SReal_hypreal_of_real: "hypreal_of_real x \<in> Reals"
+lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
by (simp add: SReal_def)
-declare SReal_hypreal_of_real [simp]
-lemma SReal_number_of: "(number_of w ::hypreal) \<in> Reals"
+lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals"
apply (simp only: hypreal_number_of [symmetric])
apply (rule SReal_hypreal_of_real)
done
-declare SReal_number_of [simp]
(** As always with numerals, 0 and 1 are special cases **)
-lemma Reals_0: "(0::hypreal) \<in> Reals"
+lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals"
apply (subst numeral_0_eq_0 [symmetric])
apply (rule SReal_number_of)
done
-declare Reals_0 [simp]
-lemma Reals_1: "(1::hypreal) \<in> Reals"
+lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals"
apply (subst numeral_1_eq_1 [symmetric])
apply (rule SReal_number_of)
done
-declare Reals_1 [simp]
lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
apply (unfold hypreal_divide_def)
apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
done
-(* Infinitesimal epsilon not in Reals *)
-
+text{*epsilon is not in Reals because it is an infinitesimal*}
lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
apply (simp add: SReal_def)
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
@@ -163,9 +157,8 @@
apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
done
-(*------------------------------------------------------------------
- Completeness of Reals
- ------------------------------------------------------------------*)
+text{*Completeness of Reals, but both lemmas are unused.*}
+
lemma SReal_sup_lemma:
"P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
(\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
@@ -182,14 +175,13 @@
apply (auto, rule_tac x = ya in exI, auto)
done
-(*------------------------------------------------------
- lifting of ub and property of lub
- -------------------------------------------------------*)
+
+subsection{*Lifting of the Ub and Lub Properties*}
+
lemma hypreal_of_real_isUb_iff:
"(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
(isUb (UNIV :: real set) Q Y)"
-apply (simp add: isUb_def setle_def)
-done
+by (simp add: isUb_def setle_def)
lemma hypreal_of_real_isLub1:
"isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
@@ -215,7 +207,6 @@
(isLub (UNIV :: real set) Q Y)"
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
-(* lemmas *)
lemma lemma_isUb_hypreal_of_real:
"isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
by (auto simp add: SReal_iff isUb_def)
@@ -233,7 +224,8 @@
==> \<exists>t::hypreal. isLub Reals P t"
apply (frule SReal_hypreal_of_real_image)
apply (auto, drule lemma_isUb_hypreal_of_real)
-apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
+apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
+ simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
done
@@ -265,27 +257,23 @@
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. abs x < t"
by (simp add: HFinite_def)
-lemma HFinite_hrabs_iff: "(abs x \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_hrabs_iff [iff]: "(abs x \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)
-declare HFinite_hrabs_iff [iff]
-lemma HFinite_number_of: "number_of w \<in> HFinite"
+lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
by (rule SReal_number_of [THEN SReal_subset_HFinite [THEN subsetD]])
-declare HFinite_number_of [simp]
(** As always with numerals, 0 and 1 are special cases **)
-lemma HFinite_0: "0 \<in> HFinite"
+lemma HFinite_0 [simp]: "0 \<in> HFinite"
apply (subst numeral_0_eq_0 [symmetric])
apply (rule HFinite_number_of)
done
-declare HFinite_0 [simp]
-lemma HFinite_1: "1 \<in> HFinite"
+lemma HFinite_1 [simp]: "1 \<in> HFinite"
apply (subst numeral_1_eq_1 [symmetric])
apply (rule HFinite_number_of)
done
-declare HFinite_1 [simp]
lemma HFinite_bounded: "[|x \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
apply (case_tac "x \<le> 0")
@@ -302,9 +290,8 @@
"x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
by (simp add: Infinitesimal_def)
-lemma Infinitesimal_zero: "0 \<in> Infinitesimal"
+lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
by (simp add: Infinitesimal_def)
-declare Infinitesimal_zero [iff]
lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
by auto
@@ -317,9 +304,8 @@
apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of)
done
-lemma Infinitesimal_minus_iff: "(-x:Infinitesimal) = (x:Infinitesimal)"
+lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
by (simp add: Infinitesimal_def)
-declare Infinitesimal_minus_iff [simp]
lemma Infinitesimal_diff:
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
@@ -368,6 +354,9 @@
apply (auto simp add: mult_ac)
done
+lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
+by (auto dest: add_less_le_mono)
+
lemma HInfinite_add_ge_zero:
"[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
by (auto intro!: hypreal_add_zero_less_le_mono
@@ -406,9 +395,9 @@
lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
by auto
-lemma Infinitesimal_hrabs_iff: "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+lemma Infinitesimal_hrabs_iff [iff]:
+ "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
by (auto simp add: abs_if)
-declare Infinitesimal_hrabs_iff [iff]
lemma HFinite_diff_Infinitesimal_hrabs:
"x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
@@ -486,9 +475,8 @@
lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
by (simp add: approx_def hypreal_add_commute)
-lemma approx_refl: "x @= x"
+lemma approx_refl [iff]: "x @= x"
by (simp add: approx_def Infinitesimal_def)
-declare approx_refl [iff]
lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
by (simp add: hypreal_add_commute)
@@ -543,8 +531,6 @@
val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image";
val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image";
val SReal_dense = thm "SReal_dense";
-val SReal_sup_lemma = thm "SReal_sup_lemma";
-val SReal_sup_lemma2 = thm "SReal_sup_lemma2";
val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff";
val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1";
val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2";
@@ -669,11 +655,9 @@
lemma approx_minus2: "-a @= -b ==> a @= b"
by (auto dest: approx_minus)
-lemma approx_minus_cancel: "(-a @= -b) = (a @= b)"
+lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
by (blast intro: approx_minus approx_minus2)
-declare approx_minus_cancel [simp]
-
lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
by (blast intro!: approx_add approx_minus)
@@ -683,8 +667,7 @@
del: minus_mult_left [symmetric])
lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
-apply (simp (no_asm_simp) add: approx_mult1 hypreal_mult_commute)
-done
+by (simp add: approx_mult1 hypreal_mult_commute)
lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
by (blast intro: approx_mult2 approx_trans)
@@ -756,19 +739,13 @@
done
lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
-apply (simp (no_asm_simp) add: hypreal_add_commute approx_add_mono1)
-done
+by (simp add: hypreal_add_commute approx_add_mono1)
-lemma approx_add_left_iff: "(a + b @= a + c) = (b @= c)"
+lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
by (fast elim: approx_add_left_cancel approx_add_mono1)
-declare approx_add_left_iff [simp]
-
-lemma approx_add_right_iff: "(b + a @= c + a) = (b @= c)"
-apply (simp (no_asm) add: hypreal_add_commute)
-done
-
-declare approx_add_right_iff [simp]
+lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
+by (simp add: hypreal_add_commute)
lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
@@ -791,8 +768,8 @@
lemma approx_mult_hypreal_of_real:
"[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
==> a*c @= hypreal_of_real b*hypreal_of_real d"
-apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real)
-done
+by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite
+ HFinite_hypreal_of_real)
lemma approx_SReal_mult_cancel_zero:
"[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
@@ -800,17 +777,15 @@
apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
done
-(* REM comments: newly added *)
lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
-lemma approx_mult_SReal_zero_cancel_iff:
+lemma approx_mult_SReal_zero_cancel_iff [simp]:
"[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
-declare approx_mult_SReal_zero_cancel_iff [simp]
lemma approx_SReal_mult_cancel:
"[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
@@ -818,10 +793,10 @@
apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
done
-lemma approx_SReal_mult_cancel_iff1:
+lemma approx_SReal_mult_cancel_iff1 [simp]:
"[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
-by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel)
-declare approx_SReal_mult_cancel_iff1 [simp]
+by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
+ intro: approx_SReal_mult_cancel)
lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
@@ -873,26 +848,23 @@
"hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
by (rule SReal_HFinite_diff_Infinitesimal, auto)
-lemma hypreal_of_real_Infinitesimal_iff_0:
+lemma hypreal_of_real_Infinitesimal_iff_0 [iff]:
"(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
apply auto
apply (rule ccontr)
apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto)
done
-declare hypreal_of_real_Infinitesimal_iff_0 [iff]
-lemma number_of_not_Infinitesimal:
+lemma number_of_not_Infinitesimal [simp]:
"number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
-declare number_of_not_Infinitesimal [simp]
(*again: 1 is a special case, but not 0 this time*)
-lemma one_not_Infinitesimal: "1 \<notin> Infinitesimal"
+lemma one_not_Infinitesimal [simp]: "1 \<notin> Infinitesimal"
apply (subst numeral_1_eq_1 [symmetric])
apply (rule number_of_not_Infinitesimal)
apply (simp (no_asm))
done
-declare one_not_Infinitesimal [simp]
lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
@@ -940,10 +912,9 @@
apply (simp add: hypreal_eq_minus_iff [symmetric])
done
-lemma number_of_approx_iff:
+lemma number_of_approx_iff [simp]:
"(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
by (auto simp add: SReal_approx_iff)
-declare number_of_approx_iff [simp]
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
@@ -953,18 +924,16 @@
"~ (0 @= 1)" "~ (1 @= 0)"
by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
-lemma hypreal_of_real_approx_iff:
+lemma hypreal_of_real_approx_iff [simp]:
"(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
apply auto
apply (rule inj_hypreal_of_real [THEN injD])
apply (rule SReal_approx_iff [THEN iffD1], auto)
done
-declare hypreal_of_real_approx_iff [simp]
-lemma hypreal_of_real_approx_number_of_iff:
+lemma hypreal_of_real_approx_number_of_iff [simp]:
"(hypreal_of_real k @= number_of w) = (k = number_of w)"
by (subst hypreal_of_real_approx_iff [symmetric], auto)
-declare hypreal_of_real_approx_number_of_iff [simp]
(*And also for 0 and 1.*)
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
@@ -1060,25 +1029,22 @@
apply (auto dest: order_less_le_trans)
done
-lemma lemma_hypreal_le_swap: "((x::hypreal) \<le> t + r) = (x + -t \<le> r)"
-by auto
-
lemma lemma_st_part1a:
"[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> x + -t \<le> r"
-by (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
-
-lemma lemma_hypreal_le_swap2: "(t + -r \<le> x) = (-(x + -t) \<le> (r::hypreal))"
-by auto
+apply (subgoal_tac "x \<le> t+r")
+apply (auto intro: lemma_st_part_le1)
+done
lemma lemma_st_part2a:
"[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> -(x + -t) \<le> r"
-apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2)
+apply (subgoal_tac "(t + -r \<le> x)")
+apply (auto intro: lemma_st_part_le2)
done
lemma lemma_SReal_ub:
@@ -1137,9 +1103,8 @@
==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
by (blast dest!: lemma_st_part_major)
-(*----------------------------------------------
- Existence of real and Standard Part Theorem
- ----------------------------------------------*)
+
+text{*Existence of real and Standard Part Theorem*}
lemma lemma_st_part_Ex:
"x \<in> HFinite ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
apply (frule lemma_st_part_lub, safe)
@@ -1153,9 +1118,7 @@
apply (drule lemma_st_part_Ex, auto)
done
-(*--------------------------------
- Unique real infinitely close
- -------------------------------*)
+text{*There is a unique real infinitely close*}
lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
apply (drule st_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
@@ -1164,12 +1127,10 @@
subsection{* Finite, Infinite and Infinitesimal*}
-lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}"
-
+lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
apply (simp add: HFinite_def HInfinite_def)
apply (auto dest: order_less_trans)
done
-declare HFinite_Int_HInfinite_empty [simp]
lemma HFinite_not_HInfinite:
assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
@@ -1254,7 +1215,8 @@
"[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
apply (rule approx_trans2)
-apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric])
+apply (auto intro: inverse_add_Infinitesimal_approx
+ simp add: mem_infmal_iff approx_minus_iff [symmetric])
done
lemma Infinitesimal_square_iff: "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)"
@@ -1265,15 +1227,13 @@
done
declare Infinitesimal_square_iff [symmetric, simp]
-lemma HFinite_square_iff: "(x*x \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_square_iff [simp]: "(x*x \<in> HFinite) = (x \<in> HFinite)"
apply (auto intro: HFinite_mult)
apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
done
-declare HFinite_square_iff [simp]
-lemma HInfinite_square_iff: "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
+lemma HInfinite_square_iff [simp]: "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
by (auto simp add: HInfinite_HFinite_iff)
-declare HInfinite_square_iff [simp]
lemma approx_HFinite_mult_cancel:
"[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
@@ -1332,10 +1292,9 @@
by (auto intro: HInfinite_gt_SReal)
-lemma not_HInfinite_one: "1 \<notin> HInfinite"
+lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite"
apply (simp (no_asm) add: HInfinite_HFinite_iff)
done
-declare not_HInfinite_one [simp]
lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
by (cut_tac x = x in hrabs_disj, auto)
@@ -1364,19 +1323,18 @@
apply (auto simp add: monad_zero_minus_iff [symmetric])
done
-lemma mem_monad_self: "x \<in> monad x"
+lemma mem_monad_self [simp]: "x \<in> monad x"
by (simp add: monad_def)
-declare mem_monad_self [simp]
+
-(*------------------------------------------------------------------
- Proof that x @= y ==> abs x @= abs y
- ------------------------------------------------------------------*)
-lemma approx_subset_monad: "x @= y ==> {x,y}\<le>monad x"
+subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*}
+
+lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
apply (simp (no_asm))
apply (simp add: approx_monad_iff)
done
-lemma approx_subset_monad2: "x @= y ==> {x,y}\<le>monad y"
+lemma approx_subset_monad2: "x @= y ==> {x,y} \<le> monad y"
apply (drule approx_sym)
apply (fast dest: approx_subset_monad)
done
@@ -1432,24 +1390,12 @@
"[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
-lemma approx_hrabs1:
- "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
-apply (frule lemma_approx_less_zero)
-apply (assumption+)
-apply (simp add: abs_if)
-done
-
-lemma approx_hrabs2:
- "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
-apply (frule lemma_approx_gt_zero)
-apply (assumption+)
-apply (simp add: abs_if)
-done
-
-lemma approx_hrabs: "x @= y ==> abs x @= abs y"
-apply (rule_tac Q = "x \<in> Infinitesimal" in excluded_middle [THEN disjE])
-apply (rule_tac x1 = x and y1 = 0 in linorder_less_linear [THEN disjE])
-apply (auto intro: approx_hrabs1 approx_hrabs2 Infinitesimal_approx_hrabs)
+theorem approx_hrabs: "x @= y ==> abs x @= abs y"
+apply (case_tac "x \<in> Infinitesimal")
+apply (simp add: Infinitesimal_approx_hrabs)
+apply (rule linorder_cases [of 0 x])
+apply (frule lemma_approx_gt_zero [of x y])
+apply (auto simp add: lemma_approx_less_zero [of x y])
done
lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
@@ -1480,9 +1426,6 @@
apply (auto intro: approx_trans2)
done
-lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)"
-by arith
-
(* interesting slightly counterintuitive theorem: necessary
for proving that an open interval is an NS open set
*)
@@ -1500,7 +1443,8 @@
==> abs (hypreal_of_real r + x) < hypreal_of_real y"
apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
-apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: hypreal_of_real_hrabs)
+apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
+ simp add: hypreal_of_real_hrabs)
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
@@ -1523,11 +1467,11 @@
"[| u \<in> Infinitesimal; v \<in> Infinitesimal;
hypreal_of_real x + u \<le> hypreal_of_real y + v |]
==> x \<le> y"
-apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel)
-done
+by (blast intro!: hypreal_of_real_le_iff [THEN iffD1]
+ hypreal_of_real_le_add_Infininitesimal_cancel)
lemma hypreal_of_real_less_Infinitesimal_le_zero:
- "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
+ "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
apply (rule linorder_not_less [THEN iffD1], safe)
apply (drule Infinitesimal_interval)
apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
@@ -1540,81 +1484,73 @@
apply (subgoal_tac "h = - hypreal_of_real x", auto)
done
-lemma Infinitesimal_square_cancel:
+lemma Infinitesimal_square_cancel [simp]:
"x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_interval2)
apply (rule_tac [3] zero_le_square, assumption)
apply (auto simp add: zero_le_square)
done
-declare Infinitesimal_square_cancel [simp]
-lemma HFinite_square_cancel: "x*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
+lemma HFinite_square_cancel [simp]: "x*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_bounded, assumption)
apply (auto simp add: zero_le_square)
done
-declare HFinite_square_cancel [simp]
-lemma Infinitesimal_square_cancel2:
+lemma Infinitesimal_square_cancel2 [simp]:
"x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
apply (rule Infinitesimal_square_cancel)
apply (rule hypreal_add_commute [THEN subst])
apply (simp (no_asm))
done
-declare Infinitesimal_square_cancel2 [simp]
-lemma HFinite_square_cancel2: "x*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
+lemma HFinite_square_cancel2 [simp]: "x*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
apply (rule HFinite_square_cancel)
apply (rule hypreal_add_commute [THEN subst])
apply (simp (no_asm))
done
-declare HFinite_square_cancel2 [simp]
-lemma Infinitesimal_sum_square_cancel:
+lemma Infinitesimal_sum_square_cancel [simp]:
"x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_interval2, assumption)
apply (rule_tac [2] zero_le_square, simp)
apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp)
done
-declare Infinitesimal_sum_square_cancel [simp]
-lemma HFinite_sum_square_cancel: "x*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
+lemma HFinite_sum_square_cancel [simp]:
+ "x*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_bounded, assumption)
apply (rule_tac [2] zero_le_square)
apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp)
done
-declare HFinite_sum_square_cancel [simp]
-lemma Infinitesimal_sum_square_cancel2:
+lemma Infinitesimal_sum_square_cancel2 [simp]:
"y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
apply (simp add: add_ac)
done
-declare Infinitesimal_sum_square_cancel2 [simp]
-lemma HFinite_sum_square_cancel2:
+lemma HFinite_sum_square_cancel2 [simp]:
"y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
apply (simp add: add_ac)
done
-declare HFinite_sum_square_cancel2 [simp]
-lemma Infinitesimal_sum_square_cancel3:
+lemma Infinitesimal_sum_square_cancel3 [simp]:
"z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
apply (simp add: add_ac)
done
-declare Infinitesimal_sum_square_cancel3 [simp]
-lemma HFinite_sum_square_cancel3:
+lemma HFinite_sum_square_cancel3 [simp]:
"z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
apply (simp add: add_ac)
done
-declare HFinite_sum_square_cancel3 [simp]
-lemma monad_hrabs_less: "[| y \<in> monad x; 0 < hypreal_of_real e |]
+lemma monad_hrabs_less:
+ "[| y \<in> monad x; 0 < hypreal_of_real e |]
==> abs (y + -x) < hypreal_of_real e"
apply (drule mem_monad_approx [THEN approx_sym])
apply (drule bex_Infinitesimal_iff [THEN iffD2])
@@ -1656,8 +1592,7 @@
apply (blast dest: SReal_approx_iff [THEN iffD1])
done
-(* ???should be added to simpset *)
-lemma st_hypreal_of_real: "st (hypreal_of_real x) = hypreal_of_real x"
+lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
@@ -1718,9 +1653,8 @@
finally show ?thesis .
qed
-lemma st_number_of: "st (number_of w) = number_of w"
+lemma st_number_of [simp]: "st (number_of w) = number_of w"
by (rule SReal_number_of [THEN st_SReal_eq])
-declare st_number_of [simp]
(*the theorem above for the special cases of zero and one*)
lemma [simp]: "st 0 = 0" "st 1 = 1"
@@ -1740,7 +1674,6 @@
apply (simp (no_asm_simp) add: st_add)
done
-(* lemma *)
lemma lemma_st_mult:
"[| x \<in> HFinite; y \<in> HFinite; e \<in> Infinitesimal; ea \<in> Infinitesimal |]
==> e*y + x*ea + e*ea \<in> Infinitesimal"
@@ -1787,16 +1720,13 @@
apply (subst hypreal_mult_inverse, auto)
done
-lemma st_divide:
+lemma st_divide [simp]:
"[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
==> st(x/y) = (st x) / (st y)"
-apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
-done
-declare st_divide [simp]
+by (simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
-lemma st_idempotent: "x \<in> HFinite ==> st(st(x)) = st(x)"
+lemma st_idempotent [simp]: "x \<in> HFinite ==> st(st(x)) = st(x)"
by (blast intro: st_HFinite st_approx_self approx_st_eq)
-declare st_idempotent [simp]
lemma Infinitesimal_add_st_less:
"[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
@@ -2021,10 +1951,10 @@
done
-(*-------------------------------------------------------------------------
- Proof that omega is an infinite number and
- hence that epsilon is an infinitesimal number.
- -------------------------------------------------------------------------*)
+subsection{*Proof that @{term omega} is an infinite number*}
+
+text{*It will follow that epsilon is an infinitesimal number.*}
+
lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
by (auto simp add: less_Suc_eq)
@@ -2077,9 +2007,7 @@
lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
by (auto dest!: order_le_less_trans simp add: linorder_not_le)
-(*-----------------------------------------------
- Omega is a member of HInfinite
- -----------------------------------------------*)
+text{*@{term omega} is a member of @{term HInfinite}*}
lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \<in> hypreal"
by auto
@@ -2089,31 +2017,27 @@
apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq)
done
-lemma HInfinite_omega: "omega: HInfinite"
+theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
apply (simp add: omega_def)
apply (auto intro!: FreeUltrafilterNat_HInfinite)
apply (rule bexI)
apply (rule_tac [2] lemma_hyprel_refl, auto)
apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
done
-declare HInfinite_omega [simp]
(*-----------------------------------------------
Epsilon is a member of Infinitesimal
-----------------------------------------------*)
-lemma Infinitesimal_epsilon: "epsilon \<in> Infinitesimal"
+lemma Infinitesimal_epsilon [simp]: "epsilon \<in> Infinitesimal"
by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)
-declare Infinitesimal_epsilon [simp]
-lemma HFinite_epsilon: "epsilon \<in> HFinite"
+lemma HFinite_epsilon [simp]: "epsilon \<in> HFinite"
by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
-declare HFinite_epsilon [simp]
-lemma epsilon_approx_zero: "epsilon @= 0"
+lemma epsilon_approx_zero [simp]: "epsilon @= 0"
apply (simp (no_asm) add: mem_infmal_iff [symmetric])
done
-declare epsilon_approx_zero [simp]
(*------------------------------------------------------------------------
Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
@@ -2343,15 +2267,12 @@
val less_Infinitesimal_less = thm "less_Infinitesimal_less";
val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero";
val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero";
-val approx_hrabs1 = thm "approx_hrabs1";
-val approx_hrabs2 = thm "approx_hrabs2";
val approx_hrabs = thm "approx_hrabs";
val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel";
val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal";
val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal";
val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel";
val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel";
-val hypreal_less_minus_iff = thm "hypreal_less_minus_iff";
val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less";
val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less";
val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2";
--- a/src/HOL/Hyperreal/SEQ.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Oct 05 15:30:50 2004 +0200
@@ -73,7 +73,7 @@
"( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
-apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
+apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
done
--- a/src/HOL/Hyperreal/Series.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy Tue Oct 05 15:30:50 2004 +0200
@@ -109,22 +109,14 @@
apply (auto intro: add_mono simp add: le_def)
done
-lemma sumr_ge_zero [rule_format (no_asm)]: "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumr m n f"
-apply (induct_tac "n", auto)
-apply (drule_tac x = n in spec, arith)
-done
-
-lemma sumr_ge_zero2 [rule_format (no_asm)]:
- "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
+lemma sumr_ge_zero [rule_format]: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
apply (induct_tac "n", auto)
apply (drule_tac x = n in spec, arith)
done
lemma rabs_sumr_rabs_cancel [simp]:
- "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
-apply (induct_tac "n")
-apply (auto, arith)
-done
+ "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
+by (induct_tac "n", simp_all add: add_increasing)
lemma sumr_zero [rule_format]:
"\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
@@ -480,9 +472,6 @@
val sumr_diff_mult_const = thm "sumr_diff_mult_const";
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
val sumr_le2 = thm "sumr_le2";
-val sumr_ge_zero = thm "sumr_ge_zero";
-val sumr_ge_zero2 = thm "sumr_ge_zero2";
-val sumr_rabs_ge_zero = thm "sumr_rabs_ge_zero";
val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
val sumr_zero = thm "sumr_zero";
val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
--- a/src/HOL/Hyperreal/Transcendental.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Oct 05 15:30:50 2004 +0200
@@ -52,13 +52,13 @@
lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
-apply (unfold root_def)
+apply (simp add: root_def)
apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero)
done
lemma real_root_pow_pos:
"0 < x ==> (root(Suc n) x) ^ (Suc n) = x"
-apply (unfold root_def)
+apply (simp add: root_def)
apply (drule_tac n = n in realpow_pos_nth2)
apply (auto intro: someI2)
done
@@ -68,7 +68,7 @@
lemma real_root_pos:
"0 < x ==> root(Suc n) (x ^ (Suc n)) = x"
-apply (unfold root_def)
+apply (simp add: root_def)
apply (rule some_equality)
apply (frule_tac [2] n = n in zero_less_power)
apply (auto simp add: zero_less_mult_iff)
@@ -83,17 +83,18 @@
lemma real_root_pos_pos:
"0 < x ==> 0 \<le> root(Suc n) x"
-apply (unfold root_def)
+apply (simp add: root_def)
apply (drule_tac n = n in realpow_pos_nth2)
apply (safe, rule someI2)
-apply (auto intro!: order_less_imp_le dest: zero_less_power simp add: zero_less_mult_iff)
+apply (auto intro!: order_less_imp_le dest: zero_less_power
+ simp add: zero_less_mult_iff)
done
lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x"
by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos)
lemma real_root_one [simp]: "root (Suc n) 1 = 1"
-apply (unfold root_def)
+apply (simp add: root_def)
apply (rule some_equality, auto)
apply (rule ccontr)
apply (rule_tac x = u and y = 1 in linorder_cases)
@@ -105,19 +106,19 @@
subsection{*Square Root*}
-(*lcp: needed now because 2 is a binary numeral!*)
+text{*needed because 2 is a binary numeral!*}
lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))"
-apply (simp (no_asm) del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 add: nat_numeral_0_eq_0 [symmetric])
-done
+by (simp del: nat_numeral_0_eq_0 nat_numeral_1_eq_1
+ add: nat_numeral_0_eq_0 [symmetric])
lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
-by (unfold sqrt_def, auto)
+by (simp add: sqrt_def)
lemma real_sqrt_one [simp]: "sqrt 1 = 1"
-by (unfold sqrt_def, auto)
+by (simp add: sqrt_def)
lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
-apply (unfold sqrt_def)
+apply (simp add: sqrt_def)
apply (rule iffI)
apply (cut_tac r = "root 2 x" in realpow_two_le)
apply (simp add: numeral_2_eq_2)
@@ -136,7 +137,7 @@
lemma real_pow_sqrt_eq_sqrt_pow:
"0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)"
-apply (unfold sqrt_def)
+apply (simp add: sqrt_def)
apply (subst numeral_2_eq_2)
apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp del: realpow_Suc)
done
@@ -162,8 +163,7 @@
by auto
lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
-apply (unfold sqrt_def root_def)
-apply (subst numeral_2_eq_2)
+apply (simp add: sqrt_def root_def)
apply (drule realpow_pos_nth2 [where n=1], safe)
apply (rule someI2, auto)
done
@@ -178,7 +178,7 @@
(*we need to prove something like this:
lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r"
apply (case_tac n, simp)
-apply (unfold root_def)
+apply (simp add: root_def)
apply (rule someI2 [of _ r], safe)
apply (auto simp del: realpow_Suc dest: power_inject_base)
*)
@@ -197,13 +197,15 @@
apply (simp add: zero_le_mult_iff real_sqrt_ge_zero)
done
-lemma real_sqrt_mult_distrib2: "[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)"
+lemma real_sqrt_mult_distrib2:
+ "[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)"
by (auto intro: real_sqrt_mult_distrib simp add: order_le_less)
lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
by (auto intro!: real_sqrt_ge_zero)
-lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
+lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
+ "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
@@ -239,7 +241,7 @@
apply (auto dest: real_sqrt_not_eq_zero)
done
-lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x = 0))"
+lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x=0))"
by (auto simp add: real_sqrt_eq_zero_cancel)
lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
@@ -274,9 +276,9 @@
apply (subst fact_Suc)
apply (subst real_of_nat_mult)
apply (auto simp add: abs_mult inverse_mult_distrib)
-apply (auto simp add: mult_assoc [symmetric] abs_eqI2 positive_imp_inverse_positive)
+apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
apply (rule order_less_imp_le)
-apply (rule_tac z1 = "real (Suc na) " in real_mult_less_iff1 [THEN iffD1])
+apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse)
apply (erule order_less_trans)
apply (auto simp add: mult_less_cancel_left mult_ac)
@@ -288,40 +290,39 @@
(if even n then 0
else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *
x ^ n)"
-apply (unfold real_divide_def)
-apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
+apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
apply (rule_tac [2] summable_exp)
apply (rule_tac x = 0 in exI)
-apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
+apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
done
lemma summable_cos:
"summable (%n.
(if even n then
(- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
-apply (unfold real_divide_def)
-apply (rule_tac g = " (%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n) " in summable_comparison_test)
+apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
apply (rule_tac [2] summable_exp)
apply (rule_tac x = 0 in exI)
-apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff)
+apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
done
-lemma lemma_STAR_sin [simp]: "(if even n then 0
+lemma lemma_STAR_sin [simp]:
+ "(if even n then 0
else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-apply (induct_tac "n", auto)
-done
-
-lemma lemma_STAR_cos [simp]: "0 < n -->
+by (induct_tac "n", auto)
+
+lemma lemma_STAR_cos [simp]:
+ "0 < n -->
(- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-apply (induct_tac "n", auto)
-done
-
-lemma lemma_STAR_cos1 [simp]: "0 < n -->
+by (induct_tac "n", auto)
+
+lemma lemma_STAR_cos1 [simp]:
+ "0 < n -->
(-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-apply (induct_tac "n", auto)
-done
-
-lemma lemma_STAR_cos2 [simp]: "sumr 1 n (%n. if even n
+by (induct_tac "n", auto)
+
+lemma lemma_STAR_cos2 [simp]:
+ "sumr 1 n (%n. if even n
then (- 1) ^ (n div 2)/(real (fact n)) *
0 ^ n
else 0) = 0"
@@ -330,7 +331,7 @@
done
lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
-apply (unfold exp_def)
+apply (simp add: exp_def)
apply (rule summable_exp [THEN summable_sums])
done
@@ -338,7 +339,7 @@
"(%n. (if even n then 0
else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *
x ^ n) sums sin(x)"
-apply (unfold sin_def)
+apply (simp add: sin_def)
apply (rule summable_sin [THEN summable_sums])
done
@@ -346,11 +347,12 @@
"(%n. (if even n then
(- 1) ^ (n div 2)/(real (fact n))
else 0) * x ^ n) sums cos(x)"
-apply (unfold cos_def)
+apply (simp add: cos_def)
apply (rule summable_cos [THEN summable_sums])
done
-lemma lemma_realpow_diff [rule_format (no_asm)]: "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
+lemma lemma_realpow_diff [rule_format (no_asm)]:
+ "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
apply (induct_tac "n", auto)
apply (subgoal_tac "p = Suc n")
apply (simp (no_asm_simp), auto)
@@ -372,16 +374,18 @@
apply (auto simp add: mult_ac)
done
-lemma lemma_realpow_diff_sumr2: "x ^ (Suc n) - y ^ (Suc n) =
+lemma lemma_realpow_diff_sumr2:
+ "x ^ (Suc n) - y ^ (Suc n) =
(x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
apply (induct_tac "n", simp)
apply (auto simp del: sumr_Suc)
apply (subst sumr_Suc)
apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib real_diff_def mult_ac simp del: sumr_Suc)
+apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
done
-lemma lemma_realpow_rev_sumr: "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =
+lemma lemma_realpow_rev_sumr:
+ "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =
sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
apply (case_tac "x = y")
apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
@@ -413,7 +417,7 @@
apply (rule_tac a2 = "z ^ n"
in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
-apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>))) " in exI)
+apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>)))" in exI)
apply (auto intro!: sums_mult simp add: mult_assoc)
apply (subgoal_tac "\<bar>z ^ n\<bar> * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n")
apply (auto simp add: power_abs [symmetric])
@@ -425,7 +429,8 @@
apply (auto simp add: abs_mult [symmetric] mult_assoc)
done
-lemma powser_inside: "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]
+lemma powser_inside:
+ "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]
==> summable (%n. f(n) * (z ^ n))"
apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea)
apply (auto intro: summable_rabs_cancel simp add: power_abs [symmetric])
@@ -447,13 +452,15 @@
apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
done
-lemma lemma_diffs2: "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =
+lemma lemma_diffs2:
+ "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =
sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -
(real n * c(n) * x ^ (n - Suc 0))"
by (auto simp add: lemma_diffs)
-lemma diffs_equiv: "summable (%n. (diffs c)(n) * (x ^ n)) ==>
+lemma diffs_equiv:
+ "summable (%n. (diffs c)(n) * (x ^ n)) ==>
(%n. real n * c(n) * (x ^ (n - Suc 0))) sums
(suminf(%n. (diffs c)(n) * (x ^ n)))"
apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0")
@@ -473,7 +480,7 @@
sumr 0 m (%p. (z ^ p) *
(((z + h) ^ (m - p)) - (z ^ (m - p))))"
apply (rule sumr_subst)
-apply (auto simp add: right_distrib real_diff_def power_add [symmetric] mult_ac)
+apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
done
lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"
@@ -483,7 +490,8 @@
by arith
-lemma lemma_termdiff2: " h \<noteq> 0 ==>
+lemma lemma_termdiff2:
+ " h \<noteq> 0 ==>
(((z + h) ^ n) - (z ^ n)) * inverse h -
real n * (z ^ (n - Suc 0)) =
h * sumr 0 (n - Suc 0) (%p. (z ^ p) *
@@ -499,13 +507,14 @@
apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib
sumdiff lemma_termdiff1 sumr_mult)
-apply (auto intro!: sumr_subst simp add: real_diff_def real_add_assoc)
+apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp
del: sumr_Suc realpow_Suc)
done
-lemma lemma_termdiff3: "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]
+lemma lemma_termdiff3:
+ "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]
==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))
\<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
apply (subst lemma_termdiff2, assumption)
@@ -524,7 +533,7 @@
apply (simp (no_asm_simp) add: power_add del: sumr_Suc)
apply (auto intro!: mult_mono simp del: sumr_Suc)
apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc)
-apply (rule_tac j = "real (Suc d) * (K ^ d) " in real_le_trans)
+apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
apply (subgoal_tac [2] "0 \<le> K")
apply (drule_tac [2] n = d in zero_le_power)
apply (auto simp del: sumr_Suc)
@@ -537,29 +546,28 @@
"[| 0 < k;
(\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>) |]
==> f -- 0 --> 0"
-apply (unfold LIM_def, auto)
+apply (simp add: LIM_def, auto)
apply (subgoal_tac "0 \<le> K")
-apply (drule_tac [2] x = "k/2" in spec)
-apply (frule_tac [2] real_less_half_sum)
-apply (drule_tac [2] real_gt_half_sum)
-apply (auto simp add: abs_eqI2)
-apply (rule_tac [2] c = "k/2" in mult_right_le_imp_le)
-apply (auto intro: abs_ge_zero [THEN real_le_trans])
+ prefer 2
+ apply (drule_tac x = "k/2" in spec)
+apply (simp add: );
+ apply (subgoal_tac "0 \<le> K*k", simp add: zero_le_mult_iff)
+ apply (force intro: order_trans [of _ "\<bar>f (k / 2)\<bar> * 2"])
apply (drule real_le_imp_less_or_eq, auto)
-apply (subgoal_tac "0 < (r * inverse K) * inverse 2")
-apply (rule_tac [2] real_mult_order)+
-apply (drule_tac ?d1.0 = "r * inverse K * inverse 2" and ?d2.0 = k in real_lbound_gt_zero)
-apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff)
-apply (rule_tac [2] y="\<bar>f (k / 2)\<bar> * 2" in order_trans, auto)
+apply (subgoal_tac "0 < (r * inverse K) / 2")
+apply (drule_tac ?d1.0 = "(r * inverse K) / 2" and ?d2.0 = k in real_lbound_gt_zero)
+apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff zero_less_divide_iff)
apply (rule_tac x = e in exI, auto)
apply (rule_tac y = "K * \<bar>x\<bar>" in order_le_less_trans)
-apply (rule_tac [2] y = "K * e" in order_less_trans)
-apply (rule_tac [3] c = "inverse K" in mult_right_less_imp_less, force)
+apply (force );
+apply (rule_tac y = "K * e" in order_less_trans)
apply (simp add: mult_less_cancel_left)
+apply (rule_tac c = "inverse K" in mult_right_less_imp_less)
apply (auto simp add: mult_ac)
done
-lemma lemma_termdiff5: "[| 0 < k;
+lemma lemma_termdiff5:
+ "[| 0 < k;
summable f;
\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k -->
(\<forall>n. abs(g(h) (n::nat)) \<le> (f(n) * \<bar>h\<bar>)) |]
@@ -602,7 +610,7 @@
apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
apply (rule_tac [2] x = K in powser_insidea, auto)
apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eqI1], auto)
+apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eq], auto)
apply (simp add: diffs_def mult_assoc [symmetric])
apply (subgoal_tac
"\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n)
@@ -640,7 +648,8 @@
apply (drule abs_ge_zero [THEN order_le_less_trans])
apply (simp add: mult_assoc)
apply (rule mult_left_mono)
-apply (rule add_commute [THEN subst])
+ prefer 2 apply arith
+apply (subst add_commute)
apply (simp (no_asm) add: mult_assoc [symmetric])
apply (rule lemma_termdiff3)
apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
@@ -654,8 +663,8 @@
\<bar>x\<bar> < \<bar>K\<bar> |]
==> DERIV (%x. suminf (%n. c(n) * (x ^ n))) x :>
suminf (%n. (diffs c)(n) * (x ^ n))"
-apply (unfold deriv_def)
-apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h) " in LIM_trans)
+apply (simp add: deriv_def)
+apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h)" in LIM_trans)
apply (simp add: LIM_def, safe)
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
apply (auto simp add: less_diff_eq)
@@ -666,11 +675,11 @@
apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
apply (auto simp add: add_commute)
apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption)
-apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
+apply (drule_tac x = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
apply (rule sums_unique)
apply (simp add: diff_def divide_inverse add_ac mult_ac)
apply (rule LIM_zero_cancel)
-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)
+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)
prefer 2 apply (blast intro: termdiffs_aux)
apply (simp add: LIM_def, safe)
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
@@ -686,12 +695,12 @@
apply (auto intro!: summable_sums)
apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
apply (auto simp add: add_commute)
-apply (frule_tac x = " (%n. c n * (xa + x) ^ n) " and y = " (%n. c n * x ^ n) " in sums_diff, assumption)
+apply (frule_tac x = "(%n. c n * (xa + x) ^ n) " and y = "(%n. c n * x ^ n)" in sums_diff, assumption)
apply (simp add: suminf_diff [OF sums_summable sums_summable]
right_diff_distrib [symmetric])
-apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
+apply (frule_tac x = "(%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
apply (simp add: sums_summable [THEN suminf_mult2])
-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)
+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)
apply assumption
apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
apply (rule_tac f = suminf in arg_cong)
@@ -704,13 +713,7 @@
lemma exp_fdiffs:
"diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
-apply (unfold diffs_def)
-apply (rule ext)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (subst inverse_mult_distrib)
-apply (auto simp add: mult_assoc [symmetric])
-done
+by (simp add: diffs_def mult_assoc [symmetric] del: mult_Suc)
lemma sin_fdiffs:
"diffs(%n. if even n then 0
@@ -718,13 +721,8 @@
= (%n. if even n then
(- 1) ^ (n div 2)/(real (fact n))
else 0)"
-apply (unfold diffs_def real_divide_def)
-apply (rule ext)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (subst even_nat_Suc)
-apply (subst inverse_mult_distrib, auto)
-done
+by (auto intro!: ext
+ simp add: diffs_def divide_inverse simp del: mult_Suc)
lemma sin_fdiffs2:
"diffs(%n. if even n then 0
@@ -732,24 +730,17 @@
= (if even n then
(- 1) ^ (n div 2)/(real (fact n))
else 0)"
-apply (unfold diffs_def real_divide_def)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (subst even_nat_Suc)
-apply (subst inverse_mult_distrib, auto)
-done
+by (auto intro!: ext
+ simp add: diffs_def divide_inverse simp del: mult_Suc)
lemma cos_fdiffs:
"diffs(%n. if even n then
(- 1) ^ (n div 2)/(real (fact n)) else 0)
= (%n. - (if even n then 0
else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
-apply (unfold diffs_def real_divide_def)
-apply (rule ext)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
-done
+by (auto intro!: ext
+ simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
+ simp del: mult_Suc)
lemma cos_fdiffs2:
@@ -757,11 +748,9 @@
(- 1) ^ (n div 2)/(real (fact n)) else 0) n
= - (if even n then 0
else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
-apply (unfold diffs_def real_divide_def)
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (auto simp add: mult_assoc odd_Suc_mult_two_ex)
-done
+by (auto intro!: ext
+ simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
+ simp del: mult_Suc)
text{*Now at last we can get the derivatives of exp, sin and cos*}
@@ -775,10 +764,10 @@
by (auto intro!: ext simp add: exp_def)
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
-apply (unfold exp_def)
+apply (simp add: exp_def)
apply (subst lemma_exp_ext)
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) ")
-apply (rule_tac [2] K = "1 + \<bar>x\<bar> " in termdiffs)
+apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
done
@@ -796,17 +785,17 @@
by (auto intro!: ext simp add: cos_def)
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
-apply (unfold cos_def)
+apply (simp add: cos_def)
apply (subst lemma_sin_ext)
apply (auto simp add: sin_fdiffs2 [symmetric])
-apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
+apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
done
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
apply (subst lemma_cos_ext)
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
-apply (rule_tac K = "1 + \<bar>x\<bar> " in termdiffs)
+apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
done
@@ -824,9 +813,9 @@
lemma exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> exp(x)"
apply (drule real_le_imp_less_or_eq, auto)
-apply (unfold exp_def)
+apply (simp add: exp_def)
apply (rule real_le_trans)
-apply (rule_tac [2] n = 2 and f = " (%n. inverse (real (fact n)) * x ^ n) " in series_pos_le)
+apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff)
done
@@ -902,7 +891,7 @@
by (auto intro: positive_imp_inverse_positive)
lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
-by (auto simp add: abs_eqI2)
+by auto
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
apply (induct_tac "n")
@@ -910,7 +899,7 @@
done
lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
-apply (unfold real_diff_def real_divide_def)
+apply (simp add: diff_minus divide_inverse)
apply (simp (no_asm) add: exp_add exp_minus)
done
@@ -992,7 +981,7 @@
lemma ln_div:
"[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"
-apply (unfold real_divide_def)
+apply (simp add: divide_inverse)
apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse)
done
@@ -1086,9 +1075,9 @@
by (auto intro: series_zero)
lemma cos_zero [simp]: "cos 0 = 1"
-apply (unfold cos_def)
+apply (simp add: cos_def)
apply (rule sums_unique [symmetric])
-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)
+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)
apply auto
done
@@ -1137,7 +1126,8 @@
done
(* most useful *)
-lemma DERIV_cos_cos_mult3 [simp]: "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
+lemma DERIV_cos_cos_mult3 [simp]:
+ "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
apply (rule lemma_DERIV_subst)
apply (rule DERIV_cos_cos_mult2, auto)
done
@@ -1145,12 +1135,13 @@
lemma DERIV_sin_circle_all:
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
(2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
-apply (unfold real_diff_def, safe)
-apply (rule DERIV_add)
+apply (simp only: diff_minus, safe)
+apply (rule DERIV_add)
apply (auto simp add: numeral_2_eq_2)
done
-lemma DERIV_sin_circle_all_zero [simp]: "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
+lemma DERIV_sin_circle_all_zero [simp]:
+ "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
by (cut_tac DERIV_sin_circle_all, auto)
lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
@@ -1169,7 +1160,7 @@
done
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
-apply (rule_tac a1 = "(cos x)\<twosuperior> " in add_right_cancel [THEN iffD1])
+apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
apply (simp del: realpow_Suc)
done
@@ -1220,23 +1211,26 @@
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
apply (rule lemma_DERIV_subst)
-apply (rule_tac f = " (%x. x ^ n) " in DERIV_chain2)
+apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
apply (rule DERIV_pow, auto)
done
-lemma DERIV_fun_exp: "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
+lemma DERIV_fun_exp:
+ "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
apply (rule lemma_DERIV_subst)
apply (rule_tac f = exp in DERIV_chain2)
apply (rule DERIV_exp, auto)
done
-lemma DERIV_fun_sin: "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
+lemma DERIV_fun_sin:
+ "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
apply (rule lemma_DERIV_subst)
apply (rule_tac f = sin in DERIV_chain2)
apply (rule DERIV_sin, auto)
done
-lemma DERIV_fun_cos: "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
+lemma DERIV_fun_cos:
+ "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
apply (rule lemma_DERIV_subst)
apply (rule_tac f = cos in DERIV_chain2)
apply (rule DERIV_cos, auto)
@@ -1250,13 +1244,14 @@
DERIV_Id DERIV_const DERIV_cos
(* lemma *)
-lemma lemma_DERIV_sin_cos_add: "\<forall>x.
+lemma lemma_DERIV_sin_cos_add:
+ "\<forall>x.
DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
(cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
apply (safe, rule lemma_DERIV_subst)
apply (best intro!: DERIV_intros intro: DERIV_chain2)
--{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
+apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
done
lemma sin_cos_add [simp]:
@@ -1283,7 +1278,7 @@
"\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
apply (safe, rule lemma_DERIV_subst)
apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
+apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac)
done
lemma sin_cos_minus [simp]:
@@ -1306,7 +1301,7 @@
done
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
-apply (unfold real_diff_def)
+apply (simp add: diff_minus)
apply (simp (no_asm) add: sin_add)
done
@@ -1314,7 +1309,7 @@
by (simp add: sin_diff mult_commute)
lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-apply (unfold real_diff_def)
+apply (simp add: diff_minus)
apply (simp (no_asm) add: cos_add)
done
@@ -1431,7 +1426,7 @@
apply (drule sums_minus)
apply (rule neg_less_iff_less [THEN iffD1])
apply (frule sums_unique, auto)
-apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)
+apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n)))" in order_less_trans)
apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
apply (rule sumr_pos_lt_pair)
@@ -1502,8 +1497,8 @@
declare pi_half_less_two [THEN order_less_imp_le, simp]
lemma pi_gt_zero [simp]: "0 < pi"
-apply (rule_tac c="inverse 2" in mult_less_imp_less_right)
-apply (cut_tac pi_half_gt_zero, simp_all)
+apply (insert pi_half_gt_zero)
+apply (simp add: );
done
lemma pi_neq_zero [simp]: "pi \<noteq> 0"
@@ -1533,32 +1528,24 @@
by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
-apply (unfold real_diff_def)
-apply (simp (no_asm) add: cos_add)
-done
+by (simp add: diff_minus cos_add)
lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
-apply (simp (no_asm) add: cos_add)
-done
+by (simp add: cos_add)
declare minus_sin_cos_eq [symmetric, simp]
lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
-apply (unfold real_diff_def)
-apply (simp (no_asm) add: sin_add)
-done
+by (simp add: diff_minus sin_add)
declare sin_cos_eq [symmetric, simp] cos_sin_eq [symmetric, simp]
lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
-apply (simp (no_asm) add: sin_add)
-done
+by (simp add: sin_add)
lemma sin_periodic_pi2 [simp]: "sin (pi + x) = - sin x"
-apply (simp (no_asm) add: sin_add)
-done
+by (simp add: sin_add)
lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
-apply (simp (no_asm) add: cos_add)
-done
+by (simp add: cos_add)
lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
by (simp add: sin_add cos_double)
@@ -1585,8 +1572,7 @@
by (simp add: cos_double)
lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
-apply (simp (no_asm))
-done
+by simp
lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
apply (rule sin_gt_zero, assumption)
@@ -1658,7 +1644,7 @@
apply (simp del: minus_sin_cos_eq [symmetric])
apply (cut_tac y="-y" in cos_total, simp) apply simp
apply (erule ex1E)
-apply (rule_tac a = "x - (pi/2) " in ex1I)
+apply (rule_tac a = "x - (pi/2)" in ex1I)
apply (simp (no_asm) add: real_add_assoc)
apply (rotate_tac 3)
apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all)
@@ -1677,7 +1663,8 @@
(* Pre Isabelle99-2 proof was simpler- numerals arithmetic
now causes some unwanted re-arrangements of literals! *)
-lemma cos_zero_lemma: "[| 0 \<le> x; cos x = 0 |] ==>
+lemma cos_zero_lemma:
+ "[| 0 \<le> x; cos x = 0 |] ==>
\<exists>n::nat. ~even n & x = real n * (pi/2)"
apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
apply (subgoal_tac "0 \<le> x - real n * pi &
@@ -1691,11 +1678,12 @@
apply (drule_tac x = "x - real n * pi" in spec)
apply (drule_tac x = "pi/2" in spec)
apply (simp add: cos_diff)
-apply (rule_tac x = "Suc (2 * n) " in exI)
+apply (rule_tac x = "Suc (2 * n)" in exI)
apply (simp add: real_of_nat_Suc left_distrib, auto)
done
-lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>
+lemma sin_zero_lemma:
+ "[| 0 \<le> x; sin x = 0 |] ==>
\<exists>n::nat. even n & x = real n * (pi/2)"
apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
apply (clarify, rule_tac x = "n - 1" in exI)
@@ -1705,7 +1693,8 @@
done
-lemma cos_zero_iff: "(cos x = 0) =
+lemma cos_zero_iff:
+ "(cos x = 0) =
((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
(\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
apply (rule iffI)
@@ -1718,7 +1707,8 @@
done
(* ditto: but to a lesser extent *)
-lemma sin_zero_iff: "(sin x = 0) =
+lemma sin_zero_iff:
+ "(sin x = 0) =
((\<exists>n::nat. even n & (x = real n * (pi/2))) |
(\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
apply (rule iffI)
@@ -1750,28 +1740,32 @@
lemma lemma_tan_add1:
"[| cos x \<noteq> 0; cos y \<noteq> 0 |]
==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"
-apply (unfold tan_def real_divide_def)
-apply (auto simp del: inverse_mult_distrib simp add: inverse_mult_distrib [symmetric] mult_ac)
+apply (simp add: tan_def divide_inverse)
+apply (auto simp del: inverse_mult_distrib
+ simp add: inverse_mult_distrib [symmetric] mult_ac)
apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
-apply (auto simp del: inverse_mult_distrib simp add: mult_assoc left_diff_distrib cos_add)
+apply (auto simp del: inverse_mult_distrib
+ simp add: mult_assoc left_diff_distrib cos_add)
done
lemma add_tan_eq:
"[| cos x \<noteq> 0; cos y \<noteq> 0 |]
==> tan x + tan y = sin(x + y)/(cos x * cos y)"
-apply (unfold tan_def)
+apply (simp add: tan_def)
apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
apply (auto simp add: mult_assoc left_distrib)
apply (simp (no_asm) add: sin_add)
done
-lemma tan_add: "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
+lemma tan_add:
+ "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
apply (simp (no_asm_simp) add: add_tan_eq lemma_tan_add1)
apply (simp add: tan_def)
done
-lemma tan_double: "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
+lemma tan_double:
+ "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
apply (insert tan_add [of x x])
apply (simp add: mult_2 [symmetric])
@@ -1779,9 +1773,7 @@
done
lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
-apply (unfold tan_def real_divide_def)
-apply (auto intro!: sin_gt_zero2 cos_gt_zero_pi intro!: real_mult_order positive_imp_inverse_positive)
-done
+by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
lemma tan_less_zero:
assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
@@ -1801,9 +1793,8 @@
by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
lemma LIM_cos_div_sin [simp]: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
-apply (unfold real_divide_def)
apply (subgoal_tac "(\<lambda>x. cos x * inverse (sin x)) -- pi * inverse 2 --> 0*1")
-apply simp
+apply (simp add: divide_inverse [symmetric])
apply (rule LIM_mult2)
apply (rule_tac [2] inverse_1 [THEN subst])
apply (rule_tac [2] LIM_inverse)
@@ -1817,19 +1808,15 @@
apply (simp only: LIM_def)
apply (drule_tac x = "inverse y" in spec, safe, force)
apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
-apply (rule_tac x = " (pi/2) - e" in exI)
+apply (rule_tac x = "(pi/2) - e" in exI)
apply (simp (no_asm_simp))
-apply (drule_tac x = " (pi/2) - e" in spec)
-apply (auto simp add: abs_eqI2 tan_def)
+apply (drule_tac x = "(pi/2) - e" in spec)
+apply (auto simp add: tan_def)
apply (rule inverse_less_iff_less [THEN iffD1])
apply (auto simp add: divide_inverse)
-apply (rule real_mult_order)
-apply (subgoal_tac [3] "0 < sin e")
-apply (subgoal_tac [3] "0 < cos e")
-apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: inverse_mult_distrib abs_mult)
-apply (drule_tac a = "cos e" in positive_imp_inverse_positive)
-apply (drule_tac x = "inverse (cos e) " in abs_eqI2)
-apply (auto dest!: abs_eqI2 simp add: mult_ac)
+apply (rule real_mult_order)
+apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
+apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
done
lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
@@ -1865,16 +1852,18 @@
simp add: cos_gt_zero_pi [THEN real_not_refl2, THEN not_sym])
done
-lemma arcsin_pi: "[| -1 \<le> y; y \<le> 1 |]
+lemma arcsin_pi:
+ "[| -1 \<le> y; y \<le> 1 |]
==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
apply (drule sin_total, assumption)
apply (erule ex1E)
-apply (unfold arcsin_def)
+apply (simp add: arcsin_def)
apply (rule someI2, blast)
apply (force intro: order_trans)
done
-lemma arcsin: "[| -1 \<le> y; y \<le> 1 |]
+lemma arcsin:
+ "[| -1 \<le> y; y \<le> 1 |]
==> -(pi/2) \<le> arcsin y &
arcsin y \<le> pi/2 & sin(arcsin y) = y"
apply (unfold arcsin_def)
@@ -1912,9 +1901,10 @@
apply (rule sin_total, auto)
done
-lemma arcos: "[| -1 \<le> y; y \<le> 1 |]
+lemma arcos:
+ "[| -1 \<le> y; y \<le> 1 |]
==> 0 \<le> arcos y & arcos y \<le> pi & cos(arcos y) = y"
-apply (unfold arcos_def)
+apply (simp add: arcos_def)
apply (drule cos_total, assumption)
apply (fast intro: someI2)
done
@@ -1931,7 +1921,8 @@
lemma arcos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcos y \<le> pi"
by (blast dest: arcos)
-lemma arcos_lt_bounded: "[| -1 < y; y < 1 |]
+lemma arcos_lt_bounded:
+ "[| -1 < y; y < 1 |]
==> 0 < arcos y & arcos y < pi"
apply (frule order_less_imp_le)
apply (frule_tac y = y in order_less_imp_le)
@@ -1942,19 +1933,19 @@
done
lemma arcos_cos: "[|0 \<le> x; x \<le> pi |] ==> arcos(cos x) = x"
-apply (unfold arcos_def)
+apply (simp add: arcos_def)
apply (auto intro!: some1_equality cos_total)
done
lemma arcos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arcos(cos x) = -x"
-apply (unfold arcos_def)
+apply (simp add: arcos_def)
apply (auto intro!: some1_equality cos_total)
done
lemma arctan [simp]:
"- (pi/2) < arctan y & arctan y < pi/2 & tan (arctan y) = y"
apply (cut_tac y = y in tan_total)
-apply (unfold arctan_def)
+apply (simp add: arctan_def)
apply (fast intro: someI2)
done
@@ -1999,16 +1990,16 @@
done
text{*NEEDED??*}
-lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =
- cos (xa + 1 / 2 * real (m) * pi)"
-apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
-done
+lemma [simp]:
+ "sin (x + 1 / 2 * real (Suc m) * pi) =
+ cos (x + 1 / 2 * real (m) * pi)"
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
text{*NEEDED??*}
-lemma [simp]: "sin (xa + real (Suc m) * pi / 2) =
- cos (xa + real (m) * pi / 2)"
-apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
-done
+lemma [simp]:
+ "sin (x + real (Suc m) * pi / 2) =
+ cos (x + real (m) * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
apply (rule lemma_DERIV_subst)
@@ -2023,7 +2014,7 @@
lemma sin_cos_npi2 [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
apply (cut_tac m = n in sin_cos_npi)
-apply (simp only: real_of_nat_Suc left_distrib divide_inverse, auto)
+apply (simp only: real_of_nat_Suc left_distrib add_divide_distrib, auto)
done
lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
@@ -2045,17 +2036,17 @@
done
(*NEEDED??*)
-lemma [simp]: "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
+lemma [simp]:
+ "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
done
(*NEEDED??*)
lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
-done
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
apply (rule lemma_DERIV_subst)
@@ -2085,7 +2076,8 @@
by (cut_tac x = x in sin_cos_squared_add3, auto)
-lemma real_root_less_mono: "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
+lemma real_root_less_mono:
+ "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
apply (frule order_le_less_trans, assumption)
apply (frule_tac n1 = n in real_root_pow_pos2 [THEN ssubst])
apply (rotate_tac 1, assumption)
@@ -2098,44 +2090,51 @@
apply (assumption, assumption)
apply (drule_tac x = "root (Suc n) x" in order_le_imp_less_or_eq)
apply auto
-apply (drule_tac f = "%x. x ^ (Suc n) " in arg_cong)
+apply (drule_tac f = "%x. x ^ (Suc n)" in arg_cong)
apply (auto simp add: real_root_pow_pos2 simp del: realpow_Suc)
done
-lemma real_root_le_mono: "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
+lemma real_root_le_mono:
+ "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
apply (drule_tac y = y in order_le_imp_less_or_eq)
apply (auto dest: real_root_less_mono intro: order_less_imp_le)
done
-lemma real_root_less_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
+lemma real_root_less_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
apply (auto intro: real_root_less_mono)
apply (rule ccontr, drule linorder_not_less [THEN iffD1])
apply (drule_tac x = y and n = n in real_root_le_mono, auto)
done
-lemma real_root_le_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
+lemma real_root_le_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
apply (auto intro: real_root_le_mono)
apply (simp (no_asm) add: linorder_not_less [symmetric])
apply auto
apply (drule_tac x = y and n = n in real_root_less_mono, auto)
done
-lemma real_root_eq_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
+lemma real_root_eq_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
apply (auto intro!: order_antisym)
apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
done
-lemma real_root_pos_unique: "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
+lemma real_root_pos_unique:
+ "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
by (auto dest: real_root_pos2 simp del: realpow_Suc)
-lemma real_root_mult: "[| 0 \<le> x; 0 \<le> y |]
+lemma real_root_mult:
+ "[| 0 \<le> x; 0 \<le> y |]
==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
apply (rule real_root_pos_unique)
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)
done
-lemma real_root_inverse: "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
+lemma real_root_inverse:
+ "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
apply (rule real_root_pos_unique)
apply (auto intro: real_root_pos_pos_le simp add: power_inverse [symmetric] real_root_pow_pos2 simp del: realpow_Suc)
done
@@ -2143,28 +2142,27 @@
lemma real_root_divide:
"[| 0 \<le> x; 0 \<le> y |]
==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"
-apply (unfold real_divide_def)
+apply (simp add: divide_inverse)
apply (auto simp add: real_root_mult real_root_inverse)
done
lemma real_sqrt_less_mono: "[| 0 \<le> x; x < y |] ==> sqrt(x) < sqrt(y)"
-apply (unfold sqrt_def)
-apply (auto intro: real_root_less_mono)
-done
+by (simp add: sqrt_def)
lemma real_sqrt_le_mono: "[| 0 \<le> x; x \<le> y |] ==> sqrt(x) \<le> sqrt(y)"
-apply (unfold sqrt_def)
-apply (auto intro: real_root_le_mono)
-done
-
-lemma real_sqrt_less_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
-by (unfold sqrt_def, auto)
-
-lemma real_sqrt_le_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
-by (unfold sqrt_def, auto)
-
-lemma real_sqrt_eq_iff [simp]: "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
-by (unfold sqrt_def, auto)
+by (simp add: sqrt_def)
+
+lemma real_sqrt_less_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
+by (simp add: sqrt_def)
+
+lemma real_sqrt_le_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
+by (simp add: sqrt_def)
+
+lemma real_sqrt_eq_iff [simp]:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
+by (simp add: sqrt_def)
lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
apply (rule real_sqrt_one [THEN subst], safe)
@@ -2178,7 +2176,7 @@
done
lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
-apply (unfold real_divide_def)
+apply (simp add: divide_inverse)
apply (case_tac "r=0")
apply (auto simp add: inverse_mult_distrib mult_ac)
done
@@ -2239,9 +2237,8 @@
lemma lemma_real_divide_sqrt_ge_minus_one2:
"x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
-apply (simp add: divide_const_simps);
-apply (insert minus_le_real_sqrt_sumsq [of x y])
-apply arith;
+apply (simp add: divide_const_simps)
+apply (insert minus_le_real_sqrt_sumsq [of x y], arith)
done
lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1"
@@ -2257,12 +2254,10 @@
by (simp add: linorder_not_less)
lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
-apply (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps);
-done
+by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps)
lemma cos_x_y_ge_minus_one1a [simp]: "-1 \<le> y / sqrt (x * x + y * y)"
-apply (subst add_commute, simp add: cos_x_y_ge_minus_one);
-done
+by (subst add_commute, simp add: cos_x_y_ge_minus_one)
lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1"
apply (cut_tac x = x and y = 0 in linorder_less_linear, safe)
@@ -2317,8 +2312,8 @@
apply (rotate_tac [2] 2)
apply (frule_tac [2] left_inverse [THEN subst])
prefer 2 apply assumption
-apply (erule_tac [2] V = " (1 - z) * (x + y) = x / (x + y) * (x + y) " in thin_rl)
-apply (erule_tac [2] V = "1 - z = x / (x + y) " in thin_rl)
+apply (erule_tac [2] V = "(1 - z) * (x + y) = x / (x + y) * (x + y)" in thin_rl)
+apply (erule_tac [2] V = "1 - z = x / (x + y)" in thin_rl)
apply (auto simp add: mult_assoc)
apply (auto simp add: right_distrib left_diff_distrib)
done
@@ -2355,12 +2350,13 @@
done
lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
-apply (unfold real_divide_def)
+apply (simp add: divide_inverse)
apply (frule_tac y3 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym, THEN nonzero_imp_inverse_nonzero])
apply (auto simp add: power2_eq_square)
done
-lemma cos_x_y_disj: "[| x \<noteq> 0;
+lemma cos_x_y_disj:
+ "[| x \<noteq> 0;
sin xa = y / sqrt (x * x + y * y)
|] ==> cos xa = x / sqrt (x * x + y * y) |
cos xa = - x / sqrt (x * x + y * y)"
@@ -2373,23 +2369,23 @@
done
lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0"
-apply (case_tac "x = 0")
-apply (auto simp add: abs_eqI2)
+apply (case_tac "x = 0", auto)
apply (drule_tac y = y in real_sqrt_sum_squares_gt_zero3)
apply (auto simp add: zero_less_mult_iff divide_inverse power2_eq_square)
done
-lemma polar_ex1: "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
-apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
+lemma polar_ex1:
+ "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
+apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
apply (rule_tac x = "arcos (x / sqrt (x * x + y * y))" in exI)
apply auto
apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
apply (auto simp add: power2_eq_square)
-apply (unfold arcos_def)
+apply (simp add: arcos_def)
apply (cut_tac x1 = x and y1 = y
in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one])
apply (rule someI2_ex, blast)
-apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y) " in thin_rl)
+apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y)" in thin_rl)
apply (frule sin_x_y_disj, blast)
apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
apply (auto simp add: power2_eq_square)
@@ -2400,7 +2396,8 @@
lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
-lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
+lemma polar_ex2:
+ "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
@@ -2456,8 +2453,7 @@
done
lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
-apply (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
-done
+by (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
lemma four_x_squared:
fixes x::real
@@ -2479,7 +2475,7 @@
apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
done
-declare real_sqrt_sum_squares_ge_zero [THEN abs_eqI1, simp]
+declare real_sqrt_sum_squares_ge_zero [THEN abs_eq, simp]
subsection{*A Few Theorems Involving Ln, Derivatives, etc.*}
@@ -2493,13 +2489,14 @@
apply (auto simp add: starfun hypreal_zero_def hypreal_less)
done
-lemma hypreal_add_Infinitesimal_gt_zero: "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"
+lemma hypreal_add_Infinitesimal_gt_zero:
+ "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"
apply (rule_tac c1 = "-e" in add_less_cancel_right [THEN iffD1])
apply (auto intro: Infinitesimal_less_SReal)
done
lemma NSDERIV_exp_ln_one: "0 < z ==> NSDERIV (%x. exp (ln x)) z :> 1"
-apply (unfold nsderiv_def NSLIM_def, auto)
+apply (simp add: nsderiv_def NSLIM_def, auto)
apply (rule ccontr)
apply (subgoal_tac "0 < hypreal_of_real z + h")
apply (drule STAR_exp_ln)
@@ -2511,14 +2508,16 @@
lemma DERIV_exp_ln_one: "0 < z ==> DERIV (%x. exp (ln x)) z :> 1"
by (auto intro: NSDERIV_exp_ln_one simp add: NSDERIV_DERIV_iff [symmetric])
-lemma lemma_DERIV_ln2: "[| 0 < z; DERIV ln z :> l |] ==> exp (ln z) * l = 1"
+lemma lemma_DERIV_ln2:
+ "[| 0 < z; DERIV ln z :> l |] ==> exp (ln z) * l = 1"
apply (rule DERIV_unique)
apply (rule lemma_DERIV_ln)
apply (rule_tac [2] DERIV_exp_ln_one, auto)
done
-lemma lemma_DERIV_ln3: "[| 0 < z; DERIV ln z :> l |] ==> l = 1/(exp (ln z))"
-apply (rule_tac c1 = "exp (ln z) " in real_mult_left_cancel [THEN iffD1])
+lemma lemma_DERIV_ln3:
+ "[| 0 < z; DERIV ln z :> l |] ==> l = 1/(exp (ln z))"
+apply (rule_tac c1 = "exp (ln z)" in real_mult_left_cancel [THEN iffD1])
apply (auto intro: lemma_DERIV_ln2)
done
@@ -2529,7 +2528,8 @@
(* need to rename second isCont_inverse *)
-lemma isCont_inv_fun: "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
+lemma isCont_inv_fun:
+ "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
\<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
==> isCont g (f x)"
apply (simp (no_asm) add: isCont_iff LIM_def)
@@ -2563,7 +2563,8 @@
text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
-lemma LIM_fun_gt_zero: "[| f -- c --> l; 0 < l |]
+lemma LIM_fun_gt_zero:
+ "[| f -- c --> l; 0 < l |]
==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
apply (auto simp add: LIM_def)
apply (drule_tac x = "l/2" in spec, safe, force)
@@ -2571,8 +2572,9 @@
apply (auto simp only: abs_interval_iff)
done
-lemma LIM_fun_less_zero: "[| f -- c --> l; l < 0 |]
- ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
+lemma LIM_fun_less_zero:
+ "[| f -- c --> l; l < 0 |]
+ ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
apply (auto simp add: LIM_def)
apply (drule_tac x = "-l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Oct 05 15:30:50 2004 +0200
@@ -465,7 +465,6 @@
apply (rule exI)
apply (rule exI)
apply (subst xzgcda.simps, auto)
- apply (simp add: abs_if)
done
lemma xzgcd_correct_aux2:
@@ -481,7 +480,6 @@
apply (frule_tac a = "r'" in pos_mod_sign, auto)
apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
apply (subst xzgcda.simps, auto)
- apply (simp add: abs_if)
done
lemma xzgcd_correct:
--- a/src/HOL/OrderedGroup.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Oct 05 15:30:50 2004 +0200
@@ -669,6 +669,16 @@
show ?thesis by (simp add: abs_lattice join_eq_if)
qed
+lemma abs_eq [simp]:
+ fixes a :: "'a::{lordered_ab_group_abs, linorder}"
+ shows "0 \<le> a ==> abs a = a"
+by (simp add: abs_if_lattice linorder_not_less [symmetric])
+
+lemma abs_minus_eq [simp]:
+ fixes a :: "'a::{lordered_ab_group_abs, linorder}"
+ shows "a < 0 ==> abs a = -a"
+by (simp add: abs_if_lattice linorder_not_less [symmetric])
+
lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
proof -
have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Oct 05 15:30:50 2004 +0200
@@ -230,7 +230,7 @@
by (simp add: right_diff_distrib)
also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: abs_homogenous abs_minus_eqI2)
+ by (simp add: abs_homogenous)
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
by (simp add: add_mult_distrib1 mult_assoc [symmetric])
also from nz y have "a * (h (inverse a \<cdot> y)) = h y"
@@ -250,7 +250,7 @@
by (simp add: right_diff_distrib)
also from gz x0 y'
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: abs_homogenous abs_eqI2)
+ by (simp add: abs_homogenous)
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
by (simp add: add_mult_distrib1 mult_assoc [symmetric])
also from nz y have "a * h (inverse a \<cdot> y) = h y"
--- a/src/HOL/Real/RealDef.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Tue Oct 05 15:30:50 2004 +0200
@@ -810,16 +810,6 @@
subsection{*Absolute Value Function for the Reals*}
-text{*FIXME: these should go!*}
-lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
-by (simp add: abs_if)
-
-lemma abs_eqI2: "(0::real) < x ==> abs x = x"
-by (simp add: abs_if)
-
-lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
-by (simp add: abs_if linorder_not_less [symmetric])
-
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
by (simp add: abs_if)
@@ -834,7 +824,7 @@
by (simp add: abs_if)
lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
-by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
+by (simp add: real_of_nat_ge_zero)
lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
apply (simp add: linorder_not_less)
@@ -857,27 +847,11 @@
val real_less_half_sum = thm"real_less_half_sum";
val real_gt_half_sum = thm"real_gt_half_sum";
-val abs_eqI1 = thm"abs_eqI1";
-val abs_eqI2 = thm"abs_eqI2";
-val abs_minus_eqI2 = thm"abs_minus_eqI2";
-val abs_ge_zero = thm"abs_ge_zero";
-val abs_idempotent = thm"abs_idempotent";
-val abs_eq_0 = thm"abs_eq_0";
-val abs_ge_self = thm"abs_ge_self";
-val abs_ge_minus_self = thm"abs_ge_minus_self";
-val abs_mult = thm"abs_mult";
-val abs_inverse = thm"abs_inverse";
-val abs_triangle_ineq = thm"abs_triangle_ineq";
-val abs_minus_cancel = thm"abs_minus_cancel";
-val abs_minus_add_cancel = thm"abs_minus_add_cancel";
val abs_interval_iff = thm"abs_interval_iff";
val abs_le_interval_iff = thm"abs_le_interval_iff";
val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
-val abs_le_zero_iff = thm"abs_le_zero_iff";
val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
-
-val abs_mult_less = thm"abs_mult_less";
*}
--- a/src/HOL/Real/RealPow.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Real/RealPow.thy Tue Oct 05 15:30:50 2004 +0200
@@ -51,7 +51,7 @@
by (simp add: abs_mult)
lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
-by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc)
+by (simp add: power_abs [symmetric] del: realpow_Suc)
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
by (insert power_increasing [of 0 n "2::real"], simp)
--- a/src/HOL/Ring_and_Field.thy Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Tue Oct 05 15:30:50 2004 +0200
@@ -5,7 +5,7 @@
header {* (Ordered) Rings and Fields *}
-theory Ring_and_Field
+theory Ring_and_Field
imports OrderedGroup
begin
@@ -1371,6 +1371,12 @@
lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
+by (simp add: abs_if linorder_not_less [symmetric])
+
+lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
+by (simp add: abs_if linorder_not_less [symmetric])
+
lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
proof -
let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"