# 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) \ 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 HFinite; y \ HFinite|] ==> x*y \ 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 \ Infinitesimal; y \ Infinitesimal |] ==> (x * y) \ 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 \ Infinitesimal; y \ HFinite |] ==> (x * y) \ 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 \ HInfinite;y \ HInfinite|] ==> (x*y) \ 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 \ Infinitesimal; y \ Infinitesimal|] ==> (x*y) \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 = "\x\" 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 = "\x\" in mult_commute [THEN ssubst]) apply (subst fact_Suc) @@ -288,7 +288,7 @@ apply (rule_tac g = "(%n. inverse (real (fact n)) * \x\ ^ 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)) * \x\ ^ 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 < \x ^ n\ ") apply (rule_tac c="\x ^ n\" 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 \ 0") apply (subgoal_tac [3] "x \ 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)); \z\ < \x\ |] ==> summable (%n. f(n) * (z ^ n))" apply (drule_tac z = "\z\" 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)) \ real n * real (n - Suc 0) * K ^ (n - 2) * \h\" 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 \ 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 "\n. real (Suc n) * real (Suc (Suc n)) * \c (Suc (Suc n))\ * (r ^ n) = diffs (diffs (%n. \c n\)) 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)