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.4  apply (drule add_strict_mono, assumption)
     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.16 +apply (simp add: right_diff_distrib)
    1.17  apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
    1.18  apply (rule add_mono)
    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.25 +apply (simp add: right_diff_distrib)
    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.66  apply (drule add_strict_mono, assumption)
    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)
    1.75  apply (drule add_strict_mono, assumption)
    1.76  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
    1.77 -                       real_mult_less_iff1, arith)
    1.78 +                       real_mult_less_iff1)
    1.79  done
    1.80  
    1.81  lemma Cauchy_iff2: