# HG changeset patch
# User paulson
# Date 1122456498 -7200
# Node ID 04246269386ef008dca78fd2e8790a5f817be174
# Parent  2d9ebdc0c1ee40aff36ffca93239498f98c1c795
removed the dependence on abs_mult

diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/HyperArith.thy
--- 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)
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/HyperPow.thy
--- 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)
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/Integration.thy
--- 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)*}
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/Lim.thy
--- 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]
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/MacLaurin.thy
--- 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
 
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/NSA.thy
--- 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)
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/Poly.thy
--- 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
diff -r 2d9ebdc0c1ee -r 04246269386e src/HOL/Hyperreal/Transcendental.thy
--- 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)