src/HOL/Multivariate_Analysis/Integration.thy
 changeset 36365 18bf20d0c2df parent 36362 06475a1547cb parent 36350 bc7982c54e37 child 36587 534418d8d494
```     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 09:37:46 2010 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 09:45:22 2010 -0700
1.3 @@ -1131,7 +1131,7 @@
1.4      guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this
1.5      guess p by(rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this
1.6      let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
1.7 -      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:group_simps norm_minus_commute)
1.8 +      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:algebra_simps norm_minus_commute)
1.9      also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
1.10        apply(rule add_strict_mono) apply(rule_tac[!] d2(2) d1(2)) using p unfolding fine_def by auto
1.11      finally show False by auto
1.12 @@ -1244,7 +1244,7 @@
1.13            unfolding scaleR_right_distrib setsum_addf[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,THEN sym]
1.14            by(rule setsum_cong2,auto)
1.15          have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) = norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
1.16 -          unfolding * by(auto simp add:group_simps) also let ?res = "\<dots>"
1.17 +          unfolding * by(auto simp add:algebra_simps) also let ?res = "\<dots>"
1.18          from as have *:"d1 fine p" "d2 fine p" unfolding fine_inter by auto
1.19          have "?res < e/2 + e/2" apply(rule le_less_trans[OF norm_triangle_ineq])
1.20            apply(rule add_strict_mono) using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)] by auto
1.21 @@ -1268,7 +1268,7 @@
1.22
1.23  lemma has_integral_sub:
1.24    shows "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_integral (k - l)) s"
1.25 -  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding group_simps by auto
1.26 +  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding algebra_simps by auto
1.27
1.28  lemma integral_0: "integral s (\<lambda>x::real^'n. 0::real^'m) = 0"
1.29    by(rule integral_unique has_integral_0)+
1.30 @@ -1703,7 +1703,7 @@
1.31        proof- guess p using fine_division_exists[OF d(1), of a' b] . note p=this
1.32          show ?thesis using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
1.33            using as unfolding interval_split b'_def[symmetric] a'_def[symmetric]
1.34 -          using p using assms by(auto simp add:group_simps)
1.35 +          using p using assms by(auto simp add:algebra_simps)
1.36        qed qed
1.37      show "?P {x. x \$ k \<ge> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
1.38      proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x \$ k \<ge> c} \<and> d fine p1 \<and> p2 tagged_division_of {a..b} \<inter> {x. x \$ k \<ge> c} \<and> d fine p2"
1.39 @@ -1711,7 +1711,7 @@
1.40        proof- guess p using fine_division_exists[OF d(1), of a b'] . note p=this
1.41          show ?thesis using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
1.42            using as unfolding interval_split b'_def[symmetric] a'_def[symmetric]
1.43 -          using p using assms by(auto simp add:group_simps) qed qed qed qed
1.44 +          using p using assms by(auto simp add:algebra_simps) qed qed qed qed
1.45
1.46  subsection {* Generalized notion of additivity. *}
1.47
1.48 @@ -1847,7 +1847,7 @@
1.49
1.50  lemma monoidal_monoid[intro]:
1.51    shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
1.52 -  unfolding monoidal_def neutral_monoid by(auto simp add: group_simps)
1.53 +  unfolding monoidal_def neutral_monoid by(auto simp add: algebra_simps)
1.54
1.55  lemma operative_integral: fixes f::"real^'n \<Rightarrow> 'a::banach"
1.56    shows "operative (lifted(op +)) (\<lambda>i. if f integrable_on i then Some(integral i f) else None)"
1.57 @@ -2380,8 +2380,8 @@
1.58        have lem2:"\<And>s1 s2 i1 i2. norm(s2 - s1) \<le> e/2 \<Longrightarrow> norm(s1 - i1) < e / 4 \<Longrightarrow> norm(s2 - i2) < e / 4 \<Longrightarrow>norm(i1 - i2) < e"
1.59        proof- case goal1 have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
1.60            using norm_triangle_ineq[of "i1 - s1" "s1 - i2"]
1.61 -          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"] by(auto simp add:group_simps)
1.62 -        also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:group_simps)
1.63 +          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"] by(auto simp add:algebra_simps)
1.64 +        also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
1.65          finally show ?case .
1.66        qed
1.67        show ?case unfolding vector_dist_norm apply(rule lem2) defer
1.68 @@ -2398,7 +2398,7 @@
1.69          also have "\<dots> = 2 / real M" unfolding real_divide_def by auto
1.70          finally show "norm (g n x - g m x) \<le> 2 / real M"
1.71            using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
1.74        qed qed qed
1.75    from this[unfolded convergent_eq_cauchy[THEN sym]] guess s .. note s=this
1.76
1.77 @@ -2412,8 +2412,8 @@
1.78      have lem:"\<And>sf sg i. norm(sf - sg) \<le> e / 3 \<Longrightarrow> norm(i - s) < e / 3 \<Longrightarrow> norm(sg - i) < e / 3 \<Longrightarrow> norm(sf - s) < e"
1.79      proof- case goal1 have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
1.80          using norm_triangle_ineq[of "sf - sg" "sg - s"]
1.81 -        using norm_triangle_ineq[of "sg -  i" " i - s"] by(auto simp add:group_simps)
1.82 -      also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:group_simps)
1.83 +        using norm_triangle_ineq[of "sg -  i" " i - s"] by(auto simp add:algebra_simps)
1.84 +      also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
1.85        finally show ?case .
1.86      qed
1.87      show ?case apply(rule_tac x=g' in exI) apply(rule,rule g')
1.88 @@ -2955,7 +2955,7 @@
1.89        have ball:"\<forall>xa\<in>k. xa \<in> ball x (d (dest_vec1 x))" using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`,unfolded split_conv subset_eq] .
1.90        have "norm ((v\$1 - u\$1) *\<^sub>R f' x - (f v - f u)) \<le> norm (f u - f x - (u\$1 - x\$1) *\<^sub>R f' x) + norm (f v - f x - (v\$1 - x\$1) *\<^sub>R f' x)"
1.91          apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
1.92 -        unfolding scaleR.diff_left by(auto simp add:group_simps)
1.93 +        unfolding scaleR.diff_left by(auto simp add:algebra_simps)
1.94        also have "... \<le> e * norm (dest_vec1 u - dest_vec1 x) + e * norm (dest_vec1 v - dest_vec1 x)"
1.95          apply(rule add_mono) apply(rule d(2)[of "x\$1" "u\$1",unfolded o_def vec1_dest_vec1]) prefer 4
1.96          apply(rule d(2)[of "x\$1" "v\$1",unfolded o_def vec1_dest_vec1])
1.97 @@ -3097,7 +3097,7 @@
1.98    proof(rule,rule,rule d,safe) case goal1 show ?case proof(cases "y < x")
1.99        case False have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 y}" apply(rule integrable_subinterval,rule integrable_continuous)
1.100          apply(rule continuous_on_o_dest_vec1 assms)+  unfolding not_less using assms(2) goal1 by auto
1.101 -      hence *:"?I a y - ?I a x = ?I x y" unfolding group_simps apply(subst eq_commute) apply(rule integral_combine)
1.102 +      hence *:"?I a y - ?I a x = ?I x y" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
1.103          using False unfolding not_less using assms(2) goal1 by auto
1.104        have **:"norm (y - x) = content {vec1 x..vec1 y}" apply(subst content_1) using False unfolding not_less by auto
1.105        show ?thesis unfolding ** apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x) o dest_vec1"]) unfolding * unfolding o_def
1.106 @@ -3111,7 +3111,7 @@
1.107        qed(insert e,auto)
1.108      next case True have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 x}" apply(rule integrable_subinterval,rule integrable_continuous)
1.109          apply(rule continuous_on_o_dest_vec1 assms)+  unfolding not_less using assms(2) goal1 by auto
1.110 -      hence *:"?I a x - ?I a y = ?I y x" unfolding group_simps apply(subst eq_commute) apply(rule integral_combine)
1.111 +      hence *:"?I a x - ?I a y = ?I y x" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
1.112          using True using assms(2) goal1 by auto
1.113        have **:"norm (y - x) = content {vec1 y..vec1 x}" apply(subst content_1) using True unfolding not_less by auto
1.114        have ***:"\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" unfolding scaleR_left.diff by auto
1.115 @@ -3193,7 +3193,7 @@
1.116            apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI)
1.117            using X(2) assms(3)[rule_format,of x] by auto
1.118        qed note ** = d(2)[OF this] have *:"inj_on (\<lambda>(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastsimp
1.119 -       have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding group_simps add_left_cancel
1.120 +       have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
1.121          unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
1.122          apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
1.123        also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym]
1.124 @@ -3331,7 +3331,7 @@
1.125
1.126  lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
1.127    apply(subst(asm)(2) norm_minus_cancel[THEN sym])
1.128 -  apply(drule norm_triangle_le) by(auto simp add:group_simps)
1.129 +  apply(drule norm_triangle_le) by(auto simp add:algebra_simps)
1.130
1.131  lemma fundamental_theorem_of_calculus_interior:
1.132    assumes"a \<le> b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
1.133 @@ -3640,11 +3640,11 @@
1.134    proof safe show "0 < ?d" using d(1) assms(3) unfolding Cart_simps by auto
1.135      fix t::"_^1" assume as:"c \<le> t" "t\$1 < c\$1 + ?d"
1.136      have *:"integral{a..c} f = integral{a..b} f - integral{c..b} f"
1.137 -      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding group_simps
1.138 +      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding algebra_simps
1.139        apply(rule_tac[!] integral_combine) using assms as unfolding Cart_simps by auto
1.140      have "(- c)\$1 - d < (- t)\$1 \<and> - t \<le> - c" using as by auto note d(2)[rule_format,OF this]
1.141      thus "norm (integral {a..c} f - integral {a..t} f) < e" unfolding *
1.142 -      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:group_simps) qed qed
1.143 +      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:algebra_simps) qed qed
1.144
1.145  declare dest_vec1_eq[simp del] not_less[simp] not_le[simp]
1.146
1.147 @@ -3714,7 +3714,7 @@
1.148      apply safe apply(rule conv) using assms(4,7) by auto
1.149    have *:"\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
1.150    proof- case goal1 hence "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
1.151 -      unfolding scaleR_simps by(auto simp add:group_simps)
1.152 +      unfolding scaleR_simps by(auto simp add:algebra_simps)
1.153      thus ?case using `x\<noteq>c` by auto qed
1.154    have as2:"finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}" using assms(2)
1.155      apply(rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
1.156 @@ -4389,7 +4389,7 @@
1.157    have *:"\<And>ir ip i cr cp. norm((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow>
1.158      ip + ir = i \<Longrightarrow> norm(cp - ip) \<le> e + k"
1.159    proof- case goal1 thus ?case  using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"]
1.160 -      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed
1.161 +      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:algebra_simps) qed
1.162
1.163    have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
1.164      unfolding split_def setsum_subtractf ..
1.165 @@ -4500,7 +4500,7 @@
1.166              norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e"
1.167        proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
1.168            norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel
1.169 -          by(auto simp add:group_simps) qed
1.170 +          by(auto simp add:algebra_simps) qed
1.171        show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where
1.172            b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
1.173        proof safe case goal1
1.174 @@ -5151,7 +5151,7 @@
1.175    assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
1.176    shows "(\<lambda>x. f(x) - g(x)) absolutely_integrable_on s"
1.177    using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
1.178 -  unfolding group_simps .
1.179 +  unfolding algebra_simps .
1.180
1.181  lemma absolutely_integrable_linear: fixes f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
1.182    assumes "f absolutely_integrable_on s" "bounded_linear h"
```