--- a/src/HOL/Hyperreal/HyperArith.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Wed Jul 27 11:28:18 2005 +0200
@@ -71,8 +71,6 @@
subsection{*Absolute Value Function for the Hyperreals*}
-declare abs_mult [simp]
-
lemma hrabs_add_less:
"[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
by (simp add: abs_if split: split_if_asm)
--- a/src/HOL/Hyperreal/HyperPow.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Wed Jul 27 11:28:18 2005 +0200
@@ -68,10 +68,11 @@
(x = 0 & y = 0 & z = 0)"
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
-
+(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
+ result proved in Ring_and_Field*)
lemma hrabs_hrealpow_two [simp]:
"abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
-by (simp)
+by (simp add: abs_mult)
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
by (insert power_increasing [of 0 n "2::hypreal"], simp)
--- a/src/HOL/Hyperreal/Integration.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 27 11:28:18 2005 +0200
@@ -361,7 +361,7 @@
apply (drule spec)+
apply auto
apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
+apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric])
done
text{*Fundamental theorem of calculus (Part I)*}
--- a/src/HOL/Hyperreal/Lim.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 27 11:28:18 2005 +0200
@@ -178,7 +178,7 @@
lemma LIM_mult_zero:
assumes f: "f -- a --> 0" and g: "g -- a --> 0"
shows "(%x. f(x) * g(x)) -- a --> 0"
-proof (simp add: LIM_eq, clarify)
+proof (simp add: LIM_eq abs_mult, clarify)
fix r :: real
assume r: "0<r"
from LIM_D [OF f zero_less_one]
--- a/src/HOL/Hyperreal/MacLaurin.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 27 11:28:18 2005 +0200
@@ -574,7 +574,7 @@
apply (simp add: numeral_2_eq_2 divide_inverse)
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
simp add: est mult_nonneg_nonneg mult_ac divide_inverse
- power_abs [symmetric])
+ power_abs [symmetric] abs_mult)
done
qed
--- a/src/HOL/Hyperreal/NSA.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Jul 27 11:28:18 2005 +0200
@@ -237,7 +237,7 @@
done
lemma HFinite_mult: "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
-apply (simp add: HFinite_def)
+apply (simp add: HFinite_def abs_mult)
apply (blast intro!: SReal_mult abs_mult_less)
done
@@ -313,14 +313,15 @@
lemma Infinitesimal_mult:
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x * y) \<in> Infinitesimal"
-apply (auto simp add: Infinitesimal_def)
-apply (case_tac "y=0")
-apply (cut_tac [2] a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto)
+apply (auto simp add: Infinitesimal_def abs_mult)
+apply (case_tac "y=0", simp)
+apply (cut_tac a = "abs x" and b = 1 and c = "abs y" and d = r
+ in mult_strict_mono, auto)
done
lemma Infinitesimal_HFinite_mult:
"[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
-apply (auto dest!: HFiniteD simp add: Infinitesimal_def)
+apply (auto dest!: HFiniteD simp add: Infinitesimal_def abs_mult)
apply (frule hrabs_less_gt_zero)
apply (drule_tac x = "r/t" in bspec)
apply (blast intro: SReal_divide)
@@ -344,11 +345,11 @@
done
lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
-apply (simp add: HInfinite_def, auto)
+apply (auto simp add: HInfinite_def abs_mult)
apply (erule_tac x = 1 in ballE)
apply (erule_tac x = r in ballE)
-apply (case_tac "y=0")
-apply (cut_tac [2] c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
+apply (case_tac "y=0", simp)
+apply (cut_tac c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
apply (auto simp add: mult_ac)
done
@@ -422,7 +423,7 @@
lemma not_Infinitesimal_mult:
"[| x \<notin> Infinitesimal; y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
apply (unfold Infinitesimal_def, clarify)
-apply (simp add: linorder_not_less)
+apply (simp add: linorder_not_less abs_mult)
apply (erule_tac x = "r*ra" in ballE)
prefer 2 apply (fast intro: SReal_mult)
apply (auto simp add: zero_less_mult_iff)
--- a/src/HOL/Hyperreal/Poly.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Wed Jul 27 11:28:18 2005 +0200
@@ -1026,7 +1026,7 @@
apply (induct "p", auto)
apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono, arith)
+apply (auto intro!: mult_mono simp add: abs_mult, arith)
done
ML
--- a/src/HOL/Hyperreal/Transcendental.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Jul 27 11:28:18 2005 +0200
@@ -266,7 +266,7 @@
apply (cut_tac x = r in reals_Archimedean3, auto)
apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
apply (rule_tac N = n and c = r in ratio_test)
-apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
+apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc)
apply (rule mult_right_mono)
apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
apply (subst fact_Suc)
@@ -288,7 +288,7 @@
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: divide_inverse power_abs [symmetric] zero_le_mult_iff)
+apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
lemma summable_cos:
@@ -298,7 +298,7 @@
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: divide_inverse power_abs [symmetric] zero_le_mult_iff)
+apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
lemma lemma_STAR_sin [simp]:
@@ -399,7 +399,7 @@
apply (rule_tac x = 0 in exI, safe)
apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le)
-apply (auto simp add: mult_assoc power_abs)
+apply (auto simp add: mult_assoc power_abs abs_mult)
prefer 2
apply (drule_tac x = 0 in spec, force)
apply (auto simp add: power_abs mult_ac)
@@ -412,7 +412,9 @@
apply (auto simp add: power_abs [symmetric])
apply (subgoal_tac "x \<noteq> 0")
apply (subgoal_tac [3] "x \<noteq> 0")
-apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
+apply (auto simp del: abs_inverse
+ simp add: abs_inverse [symmetric] realpow_not_zero
+ abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide)
done
@@ -420,7 +422,7 @@
"[| 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])
+apply (auto intro: summable_rabs_cancel simp add: abs_mult power_abs [symmetric])
done
@@ -501,10 +503,10 @@
==> 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)
-apply (simp add: mult_commute)
+apply (simp add: mult_commute abs_mult)
apply (simp add: mult_commute [of _ "K ^ (n - 2)"])
apply (rule setsum_abs [THEN real_le_trans])
-apply (simp add: mult_assoc [symmetric])
+apply (simp add: mult_assoc [symmetric] abs_mult)
apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
apply (auto intro!: real_setsum_nat_ivl_bounded)
apply (case_tac "n", auto)
@@ -515,13 +517,15 @@
K ^ p * (real (Suc (Suc (p + d))) * K ^ d)")
apply (simp (no_asm_simp) add: power_add del: setsum_op_ivl_Suc)
apply (auto intro!: mult_mono simp del: setsum_op_ivl_Suc)
-apply (auto intro!: power_mono simp add: power_abs simp del: setsum_op_ivl_Suc)
+apply (auto intro!: power_mono simp add: power_abs
+ simp del: setsum_op_ivl_Suc)
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: setsum_op_ivl_Suc)
apply (rule setsum_abs [THEN real_le_trans])
-apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
+apply (rule real_setsum_nat_ivl_bounded)
+apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
done
@@ -597,7 +601,7 @@
apply (subgoal_tac
"\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n)
= diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ")
-apply auto
+apply (auto simp add: abs_mult)
apply (drule diffs_equiv)
apply (drule sums_summable)
apply (simp_all add: diffs_def)