src/HOL/Hyperreal/Integration.thy
changeset 15094 a7d1a3fdc30d
parent 15093 49ede01e9ee6
child 15105 e194d4d265fb
     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Jul 30 18:37:58 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Sat Jul 31 20:54:23 2004 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  apply (rotate_tac 2)
     1.5  apply (drule_tac x = N in spec, simp)
     1.6  apply (drule_tac x = Na in spec)
     1.7 -apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
     1.8 +apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto)
     1.9  done
    1.10  
    1.11  lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
    1.12 @@ -203,7 +203,7 @@
    1.13  lemma lemma_psize1:
    1.14       "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
    1.15        ==> D1(N) < D2 (psize D2)"
    1.16 -apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
    1.17 +apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans)
    1.18  apply (erule partition_gt, assumption)
    1.19  apply (auto simp add: partition_rhs partition_le)
    1.20  done
    1.21 @@ -319,7 +319,7 @@
    1.22  apply (drule fine_min)
    1.23  apply (drule spec)+
    1.24  apply auto
    1.25 -apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
    1.26 +apply (subgoal_tac "\<bar>(rsum (D,p) f - k2) - (rsum (D,p) f - k1)\<bar> < \<bar>k1 - k2\<bar>")
    1.27  apply arith
    1.28  apply (drule add_strict_mono, assumption)
    1.29  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
    1.30 @@ -363,7 +363,7 @@
    1.31  apply (rule exI, auto)
    1.32  apply (drule spec)+
    1.33  apply auto
    1.34 -apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
    1.35 +apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
    1.36  apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
    1.37  done
    1.38  
    1.39 @@ -385,14 +385,14 @@
    1.40  
    1.41  
    1.42  (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
    1.43 -   they break the original proofs and make new proofs longer!                 *)
    1.44 +   they break the original proofs and make new proofs longer!*)
    1.45  lemma strad1:
    1.46         "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
    1.47               \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
    1.48          0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
    1.49         \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
    1.50  apply auto
    1.51 -apply (case_tac "0 < \<bar>z - x\<bar> ")
    1.52 +apply (case_tac "0 < \<bar>z - x\<bar>")
    1.53   prefer 2 apply (simp add: zero_less_abs_iff)
    1.54  apply (drule_tac x = z in spec)
    1.55  apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
    1.56 @@ -413,10 +413,12 @@
    1.57       "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
    1.58        ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
    1.59                  (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
    1.60 -                  --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
    1.61 +                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
    1.62  apply (simp add: gauge_def)
    1.63  apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
    1.64 -        (\<exists>d. 0 < d & (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> abs ((f (v) - f (u)) - (f' (x) * (v - u))) \<le> e * (v - u)))")
    1.65 +        (\<exists>d. 0 < d & 
    1.66 +             (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
    1.67 +                \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u)))")
    1.68  apply (drule choiceP, auto)
    1.69  apply (drule spec, auto)
    1.70  apply (auto simp add: DERIV_iff2 LIM_def)
    1.71 @@ -424,13 +426,14 @@
    1.72  apply (frule strad1, assumption+)
    1.73  apply (rule_tac x = s in exI, auto)
    1.74  apply (rule_tac x = u and y = v in linorder_cases, auto)
    1.75 -apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
    1.76 +apply (rule_tac j = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + 
    1.77 +                     \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
    1.78         in real_le_trans)
    1.79  apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
    1.80  apply (simp add: right_diff_distrib, arith)
    1.81 -apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
    1.82 +apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
    1.83  apply (rule add_mono)
    1.84 -apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
    1.85 +apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar>" in real_le_trans)
    1.86   prefer 2 apply simp apply arith
    1.87  apply (erule_tac [!]
    1.88         V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
    1.89 @@ -453,19 +456,19 @@
    1.90  apply (drule_tac x = "e/2" in spec, auto)
    1.91  apply (drule spec, auto)
    1.92  apply ((drule spec)+, auto)
    1.93 -apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
    1.94 +apply (drule_tac e = "ea/ (b - a)" in lemma_straddle)
    1.95  apply (auto simp add: zero_less_divide_iff)
    1.96  apply (rule exI)
    1.97  apply (auto simp add: tpart_def rsum_def)
    1.98 -apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
    1.99 +apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a")
   1.100   prefer 2
   1.101 - apply (cut_tac D = "%n. f (D n) " and m = "psize D"
   1.102 + apply (cut_tac D = "%n. f (D n)" and m = "psize D"
   1.103          in sumr_partition_eq_diff_bounds)
   1.104   apply (simp add: partition_lhs partition_rhs)
   1.105  apply (drule sym, simp)
   1.106  apply (simp (no_asm) add: sumr_diff)
   1.107  apply (rule sumr_rabs [THEN real_le_trans])
   1.108 -apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
   1.109 +apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
   1.110  apply (simp add: abs_minus_commute)
   1.111  apply (rule_tac t = ea in ssubst, assumption)
   1.112  apply (rule sumr_le2)
   1.113 @@ -775,8 +778,8 @@
   1.114  apply (drule_tac x = "na + n" in spec)
   1.115  apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   1.116  apply (simp add: tpart_def, safe)
   1.117 -apply (subgoal_tac "D n \<le> p (na + n) ")
   1.118 -apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
   1.119 +apply (subgoal_tac "D n \<le> p (na + n)")
   1.120 +apply (drule_tac y = "p (na + n)" in real_le_imp_less_or_eq)
   1.121  apply safe
   1.122  apply (simp split: split_if_asm, simp)
   1.123  apply (drule less_le_trans, assumption)
   1.124 @@ -790,7 +793,7 @@
   1.125  lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
   1.126  by (simp add: rsum_def sumr_add left_distrib)
   1.127  
   1.128 -(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
   1.129 +text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
   1.130  lemma Integral_add_fun:
   1.131      "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
   1.132       ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
   1.133 @@ -798,7 +801,7 @@
   1.134  apply ((drule_tac x = "e/2" in spec)+)
   1.135  apply auto
   1.136  apply (drule gauge_min, assumption)
   1.137 -apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
   1.138 +apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI)
   1.139  apply auto
   1.140  apply (drule fine_min)
   1.141  apply ((drule spec)+, auto)
   1.142 @@ -852,7 +855,7 @@
   1.143  apply (drule_tac x = D in spec, drule_tac x = D in spec)
   1.144  apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
   1.145  apply (frule lemma_Integral_rsum_le, assumption)
   1.146 -apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
   1.147 +apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar>")
   1.148  apply arith
   1.149  apply (drule add_strict_mono, assumption)
   1.150  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]