src/HOL/Hyperreal/Integration.thy
 changeset 20217 25b068a99d2b parent 19765 dfe940911617 child 20256 5024ba0831a6
```     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 13:31:07 2006 +0200
1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 19:23:04 2006 +0200
1.3 @@ -323,7 +323,6 @@
1.5  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
1.6                  mult_less_cancel_right)
1.7 -apply arith
1.8  done
1.9
1.10  lemma Integral_zero [simp]: "Integral(a,a) f 0"
1.11 @@ -423,7 +422,7 @@
1.12                       \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
1.13         in order_trans)
1.14  apply (rule abs_triangle_ineq [THEN [2] order_trans])
1.15 -apply (simp add: right_diff_distrib, arith)
1.17  apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
1.19  apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
1.20 @@ -434,7 +433,7 @@
1.21  apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
1.22  apply (rule order_trans)
1.23  apply (auto simp add: abs_le_interval_iff)
1.24 -apply (simp add: right_diff_distrib, arith)
1.26  done
1.27
1.28  lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
1.29 @@ -577,7 +576,7 @@
1.30  apply (auto dest: partition_lt_cancel)
1.31  apply (rule_tac x=N and y=n in linorder_cases)
1.32  apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
1.33 -apply (drule_tac n = n in partition_lt_gen, auto, arith)
1.34 +apply (drule_tac n = n in partition_lt_gen, auto)
1.35  apply (drule_tac x = n in spec)
1.36  apply (simp split: split_if_asm)
1.37  done
1.38 @@ -741,7 +740,6 @@
1.39        ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
1.40  apply (simp add: tpart_def partition_def, safe)
1.41  apply (rule_tac x = "N - n" in exI, auto)
1.42 -apply (drule_tac x = "na + n" in spec, arith)+
1.43  done
1.44
1.45  lemma fine_right1:
1.46 @@ -752,7 +750,7 @@
1.47        ==> fine ga (%x. D(x + n),%x. p(x + n))"
1.48  apply (auto simp add: fine_def gauge_def)
1.49  apply (drule_tac x = "na + n" in spec)
1.50 -apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
1.51 +apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
1.52  apply (simp add: tpart_def, safe)
1.53  apply (subgoal_tac "D n \<le> p (na + n)")
1.54  apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
1.55 @@ -783,7 +781,7 @@
1.56  apply ((drule spec)+, auto)
1.57  apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
1.58  apply (auto simp only: rsum_add left_distrib [symmetric]
1.59 -                mult_2_right [symmetric] real_mult_less_iff1, arith)
1.60 +                mult_2_right [symmetric] real_mult_less_iff1)
1.61  done
1.62
1.63  lemma partition_lt_gen2:
1.64 @@ -834,7 +832,7 @@
1.65  apply arith
1.67  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
1.68 -                       real_mult_less_iff1, arith)
1.69 +                       real_mult_less_iff1)
1.70  done
1.71
1.72  lemma Integral_imp_Cauchy:
1.73 @@ -853,7 +851,7 @@
1.74  apply (erule_tac V = "0 < e" in thin_rl)