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.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.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.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.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.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.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.127
1.128 -(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
1.129 +text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
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