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.72 -          by(auto simp add:group_simps simp add:norm_minus_commute)
    1.73 +          by(auto simp add:algebra_simps simp add:norm_minus_commute)
    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"