removed the dependence on abs_mult
authorpaulson
Wed Jul 27 11:28:18 2005 +0200 (2005-07-27)
changeset 1692404246269386e
parent 16923 2d9ebdc0c1ee
child 16925 0fd7b1438d28
removed the dependence on abs_mult
src/HOL/Hyperreal/HyperArith.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Tue Jul 26 18:31:18 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Wed Jul 27 11:28:18 2005 +0200
     1.3 @@ -71,8 +71,6 @@
     1.4  
     1.5  subsection{*Absolute Value Function for the Hyperreals*}
     1.6  
     1.7 -declare abs_mult [simp]
     1.8 -
     1.9  lemma hrabs_add_less:
    1.10       "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
    1.11  by (simp add: abs_if split: split_if_asm)
     2.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Tue Jul 26 18:31:18 2005 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Jul 27 11:28:18 2005 +0200
     2.3 @@ -68,10 +68,11 @@
     2.4        (x = 0 & y = 0 & z = 0)"
     2.5  by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
     2.6  
     2.7 -
     2.8 +(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
     2.9 +  result proved in Ring_and_Field*)
    2.10  lemma hrabs_hrealpow_two [simp]:
    2.11       "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
    2.12 -by (simp)
    2.13 +by (simp add: abs_mult)
    2.14  
    2.15  lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
    2.16  by (insert power_increasing [of 0 n "2::hypreal"], simp)
     3.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Jul 26 18:31:18 2005 +0200
     3.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Jul 27 11:28:18 2005 +0200
     3.3 @@ -361,7 +361,7 @@
     3.4  apply (drule spec)+
     3.5  apply auto
     3.6  apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
     3.7 -apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
     3.8 +apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric])
     3.9  done
    3.10  
    3.11  text{*Fundamental theorem of calculus (Part I)*}
     4.1 --- a/src/HOL/Hyperreal/Lim.thy	Tue Jul 26 18:31:18 2005 +0200
     4.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 27 11:28:18 2005 +0200
     4.3 @@ -178,7 +178,7 @@
     4.4  lemma LIM_mult_zero:
     4.5    assumes f: "f -- a --> 0" and g: "g -- a --> 0"
     4.6    shows "(%x. f(x) * g(x)) -- a --> 0"
     4.7 -proof (simp add: LIM_eq, clarify)
     4.8 +proof (simp add: LIM_eq abs_mult, clarify)
     4.9    fix r :: real
    4.10    assume r: "0<r"
    4.11    from LIM_D [OF f zero_less_one]
     5.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 26 18:31:18 2005 +0200
     5.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 27 11:28:18 2005 +0200
     5.3 @@ -574,7 +574,7 @@
     5.4      apply (simp add: numeral_2_eq_2 divide_inverse)
     5.5      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
     5.6                     simp add: est mult_nonneg_nonneg mult_ac divide_inverse
     5.7 -                          power_abs [symmetric])
     5.8 +                          power_abs [symmetric] abs_mult)
     5.9      done
    5.10  qed
    5.11  
     6.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Jul 26 18:31:18 2005 +0200
     6.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Jul 27 11:28:18 2005 +0200
     6.3 @@ -237,7 +237,7 @@
     6.4  done
     6.5  
     6.6  lemma HFinite_mult: "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
     6.7 -apply (simp add: HFinite_def)
     6.8 +apply (simp add: HFinite_def abs_mult)
     6.9  apply (blast intro!: SReal_mult abs_mult_less)
    6.10  done
    6.11  
    6.12 @@ -313,14 +313,15 @@
    6.13  
    6.14  lemma Infinitesimal_mult:
    6.15       "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x * y) \<in> Infinitesimal"
    6.16 -apply (auto simp add: Infinitesimal_def)
    6.17 -apply (case_tac "y=0")
    6.18 -apply (cut_tac [2] a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto)
    6.19 +apply (auto simp add: Infinitesimal_def abs_mult)
    6.20 +apply (case_tac "y=0", simp) 
    6.21 +apply (cut_tac a = "abs x" and b = 1 and c = "abs y" and d = r 
    6.22 +       in mult_strict_mono, auto)
    6.23  done
    6.24  
    6.25  lemma Infinitesimal_HFinite_mult:
    6.26       "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
    6.27 -apply (auto dest!: HFiniteD simp add: Infinitesimal_def)
    6.28 +apply (auto dest!: HFiniteD simp add: Infinitesimal_def abs_mult)
    6.29  apply (frule hrabs_less_gt_zero)
    6.30  apply (drule_tac x = "r/t" in bspec)
    6.31  apply (blast intro: SReal_divide)
    6.32 @@ -344,11 +345,11 @@
    6.33  done
    6.34  
    6.35  lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
    6.36 -apply (simp add: HInfinite_def, auto)
    6.37 +apply (auto simp add: HInfinite_def  abs_mult)
    6.38  apply (erule_tac x = 1 in ballE)
    6.39  apply (erule_tac x = r in ballE)
    6.40 -apply (case_tac "y=0")
    6.41 -apply (cut_tac [2] c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
    6.42 +apply (case_tac "y=0", simp)
    6.43 +apply (cut_tac c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
    6.44  apply (auto simp add: mult_ac)
    6.45  done
    6.46  
    6.47 @@ -422,7 +423,7 @@
    6.48  lemma not_Infinitesimal_mult:
    6.49       "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
    6.50  apply (unfold Infinitesimal_def, clarify)
    6.51 -apply (simp add: linorder_not_less)
    6.52 +apply (simp add: linorder_not_less abs_mult)
    6.53  apply (erule_tac x = "r*ra" in ballE)
    6.54  prefer 2 apply (fast intro: SReal_mult)
    6.55  apply (auto simp add: zero_less_mult_iff)
     7.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Jul 26 18:31:18 2005 +0200
     7.2 +++ b/src/HOL/Hyperreal/Poly.thy	Wed Jul 27 11:28:18 2005 +0200
     7.3 @@ -1026,7 +1026,7 @@
     7.4  apply (induct "p", auto)
     7.5  apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
     7.6  apply (rule abs_triangle_ineq)
     7.7 -apply (auto intro!: mult_mono, arith)
     7.8 +apply (auto intro!: mult_mono simp add: abs_mult, arith)
     7.9  done
    7.10  
    7.11  ML
     8.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jul 26 18:31:18 2005 +0200
     8.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 27 11:28:18 2005 +0200
     8.3 @@ -266,7 +266,7 @@
     8.4  apply (cut_tac x = r in reals_Archimedean3, auto)
     8.5  apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
     8.6  apply (rule_tac N = n and c = r in ratio_test)
     8.7 -apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
     8.8 +apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc)
     8.9  apply (rule mult_right_mono)
    8.10  apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
    8.11  apply (subst fact_Suc)
    8.12 @@ -288,7 +288,7 @@
    8.13  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
    8.14  apply (rule_tac [2] summable_exp)
    8.15  apply (rule_tac x = 0 in exI)
    8.16 -apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
    8.17 +apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    8.18  done
    8.19  
    8.20  lemma summable_cos: 
    8.21 @@ -298,7 +298,7 @@
    8.22  apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
    8.23  apply (rule_tac [2] summable_exp)
    8.24  apply (rule_tac x = 0 in exI)
    8.25 -apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff)
    8.26 +apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    8.27  done
    8.28  
    8.29  lemma lemma_STAR_sin [simp]:
    8.30 @@ -399,7 +399,7 @@
    8.31  apply (rule_tac x = 0 in exI, safe)
    8.32  apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
    8.33  apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
    8.34 -apply (auto simp add: mult_assoc power_abs)
    8.35 +apply (auto simp add: mult_assoc power_abs abs_mult)
    8.36   prefer 2
    8.37   apply (drule_tac x = 0 in spec, force)
    8.38  apply (auto simp add: power_abs mult_ac)
    8.39 @@ -412,7 +412,9 @@
    8.40  apply (auto simp add: power_abs [symmetric])
    8.41  apply (subgoal_tac "x \<noteq> 0")
    8.42  apply (subgoal_tac [3] "x \<noteq> 0")
    8.43 -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])
    8.44 +apply (auto simp del: abs_inverse 
    8.45 +            simp add: abs_inverse [symmetric] realpow_not_zero
    8.46 +            abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
    8.47  apply (auto intro!: geometric_sums  simp add: power_abs inverse_eq_divide)
    8.48  done
    8.49  
    8.50 @@ -420,7 +422,7 @@
    8.51       "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
    8.52        ==> summable (%n. f(n) * (z ^ n))"
    8.53  apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea)
    8.54 -apply (auto intro: summable_rabs_cancel simp add: power_abs [symmetric])
    8.55 +apply (auto intro: summable_rabs_cancel simp add: abs_mult power_abs [symmetric])
    8.56  done
    8.57  
    8.58  
    8.59 @@ -501,10 +503,10 @@
    8.60        ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
    8.61            \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
    8.62  apply (subst lemma_termdiff2, assumption)
    8.63 -apply (simp add: mult_commute) 
    8.64 +apply (simp add: mult_commute abs_mult) 
    8.65  apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
    8.66  apply (rule setsum_abs [THEN real_le_trans])
    8.67 -apply (simp add: mult_assoc [symmetric])
    8.68 +apply (simp add: mult_assoc [symmetric] abs_mult)
    8.69  apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
    8.70  apply (auto intro!: real_setsum_nat_ivl_bounded)
    8.71  apply (case_tac "n", auto)
    8.72 @@ -515,13 +517,15 @@
    8.73                      K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
    8.74  apply (simp (no_asm_simp) add: power_add del: setsum_op_ivl_Suc)
    8.75  apply (auto intro!: mult_mono simp del: setsum_op_ivl_Suc)
    8.76 -apply (auto intro!: power_mono simp add: power_abs simp del: setsum_op_ivl_Suc)
    8.77 +apply (auto intro!: power_mono simp add: power_abs
    8.78 +           simp del: setsum_op_ivl_Suc)
    8.79  apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
    8.80  apply (subgoal_tac [2] "0 \<le> K")
    8.81  apply (drule_tac [2] n = d in zero_le_power)
    8.82  apply (auto simp del: setsum_op_ivl_Suc)
    8.83  apply (rule setsum_abs [THEN real_le_trans])
    8.84 -apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
    8.85 +apply (rule real_setsum_nat_ivl_bounded)
    8.86 +apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
    8.87  apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
    8.88  done
    8.89  
    8.90 @@ -597,7 +601,7 @@
    8.91  apply (subgoal_tac
    8.92          "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
    8.93                = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
    8.94 -apply auto
    8.95 +apply (auto simp add: abs_mult)
    8.96  apply (drule diffs_equiv)
    8.97  apply (drule sums_summable)
    8.98  apply (simp_all add: diffs_def)