abs notation
authorpaulson
Wed Jul 28 16:25:40 2004 +0200 (2004-07-28)
changeset 1508132402f5624d1
parent 15080 7912ace86f31
child 15082 6c3276a2735b
abs notation
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:28 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 28 16:25:40 2004 +0200
     1.3 @@ -575,12 +575,12 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  lemma sin_bound_lemma:
     1.7 -    "[|x = y; abs u \<le> (v::real) |] ==> abs ((x + u) - y) \<le> v"
     1.8 +    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
     1.9  by auto
    1.10  
    1.11  lemma Maclaurin_sin_bound:
    1.12    "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
    1.13 -  x ^ m))  \<le> inverse(real (fact n)) * abs(x) ^ n"
    1.14 +  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
    1.15  proof -
    1.16    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
    1.17      by (rule_tac mult_right_mono,simp_all)
     2.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 28 16:25:28 2004 +0200
     2.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 28 16:25:40 2004 +0200
     2.3 @@ -393,16 +393,16 @@
     2.4  
     2.5  lemma powser_insidea:
     2.6       "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
     2.7 -      ==> summable (%n. abs(f(n)) * (z ^ n))"
     2.8 +      ==> summable (%n. \<bar>f(n)\<bar> * (z ^ n))"
     2.9  apply (drule summable_LIMSEQ_zero)
    2.10  apply (drule convergentI)
    2.11  apply (simp add: Cauchy_convergent_iff [symmetric])
    2.12  apply (drule Cauchy_Bseq)
    2.13  apply (simp add: Bseq_def, safe)
    2.14 -apply (rule_tac g = "%n. K * abs (z ^ n) * inverse (abs (x ^ n))" in summable_comparison_test)
    2.15 +apply (rule_tac g = "%n. K * \<bar>z ^ n\<bar> * inverse (\<bar>x ^ n\<bar>)" in summable_comparison_test)
    2.16  apply (rule_tac x = 0 in exI, safe)
    2.17 -apply (subgoal_tac "0 < abs (x ^ n) ")
    2.18 -apply (rule_tac c="abs (x ^ n)" in mult_right_le_imp_le) 
    2.19 +apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
    2.20 +apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
    2.21  apply (auto simp add: mult_assoc power_abs)
    2.22   prefer 2
    2.23   apply (drule_tac x = 0 in spec, force)
    2.24 @@ -412,7 +412,7 @@
    2.25  apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
    2.26  apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>))) " in exI)
    2.27  apply (auto intro!: sums_mult simp add: mult_assoc)
    2.28 -apply (subgoal_tac "abs (z ^ n) * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n")
    2.29 +apply (subgoal_tac "\<bar>z ^ n\<bar> * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n")
    2.30  apply (auto simp add: power_abs [symmetric])
    2.31  apply (subgoal_tac "x \<noteq> 0")
    2.32  apply (subgoal_tac [3] "x \<noteq> 0")
    2.33 @@ -502,7 +502,7 @@
    2.34                   del: sumr_Suc realpow_Suc)
    2.35  done
    2.36  
    2.37 -lemma lemma_termdiff3: "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; abs (z + h) \<le> K |]  
    2.38 +lemma lemma_termdiff3: "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
    2.39        ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
    2.40            \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
    2.41  apply (subst lemma_termdiff2, assumption)
    2.42 @@ -532,7 +532,7 @@
    2.43  
    2.44  lemma lemma_termdiff4: 
    2.45    "[| 0 < k;  
    2.46 -      (\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> abs(f h) \<le> K * \<bar>h\<bar>) |]  
    2.47 +      (\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>) |]  
    2.48     ==> f -- 0 --> 0"
    2.49  apply (unfold LIM_def, auto)
    2.50  apply (subgoal_tac "0 \<le> K")
    2.51 @@ -562,7 +562,7 @@
    2.52                      (\<forall>n. abs(g(h) (n::nat)) \<le> (f(n) * \<bar>h\<bar>)) |]  
    2.53           ==> (%h. suminf(g h)) -- 0 --> 0"
    2.54  apply (drule summable_sums)
    2.55 -apply (subgoal_tac "\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> abs (suminf (g h)) \<le> suminf f * \<bar>h\<bar>")
    2.56 +apply (subgoal_tac "\<forall>h. 0 < \<bar>h\<bar> & \<bar>h\<bar> < k --> \<bar>suminf (g h)\<bar> \<le> suminf f * \<bar>h\<bar>")
    2.57  apply (auto intro!: lemma_termdiff4 simp add: sums_summable [THEN suminf_mult, symmetric])
    2.58  apply (subgoal_tac "summable (%n. f n * \<bar>h\<bar>) ")
    2.59   prefer 2
    2.60 @@ -573,7 +573,7 @@
    2.61  apply (subgoal_tac "summable (%n. abs (g (h::real) (n::nat))) ")
    2.62   apply (rule_tac [2] g = "%n. f n * \<bar>h\<bar>" in summable_comparison_test)
    2.63    apply (rule_tac [2] x = 0 in exI, auto)
    2.64 -apply (rule_tac j = "suminf (%n. abs (g h n))" in real_le_trans)
    2.65 +apply (rule_tac j = "suminf (%n. \<bar>g h n\<bar>)" in real_le_trans)
    2.66  apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult])
    2.67  done
    2.68  
    2.69 @@ -591,7 +591,7 @@
    2.70  apply (drule dense, safe)
    2.71  apply (frule real_less_sum_gt_zero)
    2.72  apply (drule_tac
    2.73 -         f = "%n. abs (c n) * real n * real (n - Suc 0) * (r ^ (n - 2))" 
    2.74 +         f = "%n. \<bar>c n\<bar> * real n * real (n - Suc 0) * (r ^ (n - 2))" 
    2.75       and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
    2.76                               - (real n * (x ^ (n - Suc 0))))" 
    2.77         in lemma_termdiff5)
    2.78 @@ -609,7 +609,7 @@
    2.79  apply (drule sums_summable)
    2.80  apply (simp_all add: diffs_def) 
    2.81  apply (simp add: diffs_def mult_ac)
    2.82 -apply (subgoal_tac " (%n. real n * (real (Suc n) * (abs (c (Suc n)) * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * abs (c m) * inverse r) n * (r ^ n))")
    2.83 +apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
    2.84  apply auto
    2.85    prefer 2
    2.86    apply (rule ext)
    2.87 @@ -899,7 +899,7 @@
    2.88  lemma inv_exp_gt_zero [simp]: "0 < inverse(exp x)"
    2.89  by (auto intro: positive_imp_inverse_positive)
    2.90  
    2.91 -lemma abs_exp_cancel [simp]: "abs(exp x) = exp x"
    2.92 +lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
    2.93  by (auto simp add: abs_eqI2)
    2.94  
    2.95  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
    2.96 @@ -1179,7 +1179,7 @@
    2.97  lemma real_gt_one_ge_zero_add_less: "[| 1 < x; 0 \<le> y |] ==> 1 < x + (y::real)"
    2.98  by arith
    2.99  
   2.100 -lemma abs_sin_le_one [simp]: "abs(sin x) \<le> 1"
   2.101 +lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
   2.102  apply (auto simp add: linorder_not_less [symmetric])
   2.103  apply (drule_tac n = "Suc 0" in power_gt1)
   2.104  apply (auto simp del: realpow_Suc)
   2.105 @@ -1197,7 +1197,7 @@
   2.106  apply (simp add: abs_le_interval_iff del: abs_sin_le_one) 
   2.107  done
   2.108  
   2.109 -lemma abs_cos_le_one [simp]: "abs(cos x) \<le> 1"
   2.110 +lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
   2.111  apply (auto simp add: linorder_not_less [symmetric])
   2.112  apply (drule_tac n = "Suc 0" in power_gt1)
   2.113  apply (auto simp del: realpow_Suc)
   2.114 @@ -2065,7 +2065,7 @@
   2.115  lemma isCont_exp [simp]: "isCont exp x"
   2.116  by (rule DERIV_exp [THEN DERIV_isCont])
   2.117  
   2.118 -lemma sin_zero_abs_cos_one: "sin x = 0 ==> abs(cos x) = 1"
   2.119 +lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
   2.120  by (auto simp add: sin_zero_iff even_mult_two_ex)
   2.121  
   2.122  lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)"
   2.123 @@ -2550,7 +2550,7 @@
   2.124           \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   2.125           \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   2.126         ==> \<exists>e. 0 < e &  
   2.127 -             (\<forall>y. 0 < abs(y - f(x)) & abs(y - f(x)) < e --> f(g(y)) = y)"
   2.128 +             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
   2.129  apply (drule isCont_inj_range)
   2.130  prefer 2 apply (assumption, assumption, auto)
   2.131  apply (rule_tac x = e in exI, auto)