src/HOL/Multivariate_Analysis/Integration.thy
changeset 36587 534418d8d494
parent 36365 18bf20d0c2df
child 36725 34c36a5cb808
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 28 22:02:55 2010 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 28 22:20:59 2010 -0700
     1.3 @@ -137,27 +137,27 @@
     1.4      hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE)
     1.5        let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$k = a$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
     1.6  	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
     1.7 -	hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto
     1.8 +	hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
     1.9  	hence "y$k < a$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps)
    1.10  	hence "y \<notin> i" unfolding ab mem_interval not_all by(rule_tac x=k in exI,auto) thus False using yi by auto qed
    1.11        moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
    1.12  	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
    1.13  	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"])
    1.14  	  unfolding norm_scaleR norm_basis by auto
    1.15 -	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps)
    1.16 -	finally show "y\<in>ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed
    1.17 +	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
    1.18 +	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
    1.19        ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto
    1.20      next let ?z = "x + (e/2) *\<^sub>R basis k" assume as:"x$k = b$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
    1.21  	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
    1.22 -	hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto
    1.23 +	hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
    1.24  	hence "y$k > b$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps)
    1.25  	hence "y \<notin> i" unfolding ab mem_interval not_all by(rule_tac x=k in exI,auto) thus False using yi by auto qed
    1.26        moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
    1.27  	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R basis k)"
    1.28  	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"])
    1.29  	  unfolding norm_scaleR norm_basis by auto
    1.30 -	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps)
    1.31 -	finally show "y\<in>ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed
    1.32 +	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
    1.33 +	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
    1.34        ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed 
    1.35      then guess x .. hence "x \<in> s \<inter> interior (\<Union>f)" unfolding lem1[where U="\<Union>f",THEN sym] using centre_in_ball e[THEN conjunct1] by auto
    1.36      thus ?thesis apply-apply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this
    1.37 @@ -1067,7 +1067,7 @@
    1.38    proof- case goal1 guess n using real_arch_pow2[of "(setsum (\<lambda>i. b$i - a$i) UNIV) / e"] .. note n=this
    1.39      show ?case apply(rule_tac x=n in exI) proof(rule,rule)
    1.40        fix x y assume xy:"x\<in>{A n..B n}" "y\<in>{A n..B n}"
    1.41 -      have "dist x y \<le> setsum (\<lambda>i. abs((x - y)$i)) UNIV" unfolding vector_dist_norm by(rule norm_le_l1)
    1.42 +      have "dist x y \<le> setsum (\<lambda>i. abs((x - y)$i)) UNIV" unfolding dist_norm by(rule norm_le_l1)
    1.43        also have "\<dots> \<le> setsum (\<lambda>i. B n$i - A n$i) UNIV"
    1.44        proof(rule setsum_mono) fix i show "\<bar>(x - y) $ i\<bar> \<le> B n $ i - A n $ i"
    1.45            using xy[unfolded mem_interval,THEN spec[where x=i]]
    1.46 @@ -1417,7 +1417,7 @@
    1.47      show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+)
    1.48      proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2"
    1.49        show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
    1.50 -        apply(rule dist_triangle_half_l[where y=y,unfolded vector_dist_norm])
    1.51 +        apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm])
    1.52          using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
    1.53      qed qed
    1.54  next assume "\<forall>e>0. \<exists>d. ?P e d" hence "\<forall>n::nat. \<exists>d. ?P (inverse(real (n + 1))) d" by auto
    1.55 @@ -1447,7 +1447,7 @@
    1.56        have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto
    1.57        show "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r)
    1.58          apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer
    1.59 -        using N2[rule_format,unfolded vector_dist_norm,of "N1+N2"]
    1.60 +        using N2[rule_format,unfolded dist_norm,of "N1+N2"]
    1.61          using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed
    1.62  
    1.63  subsection {* Additivity of integral on abutting intervals. *}
    1.64 @@ -1554,7 +1554,7 @@
    1.65            using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
    1.66          hence "\<exists>y. y \<in> ball x \<bar>x $ k - c\<bar> \<inter> {x. x $ k \<le> c}" using goal1(1) by blast 
    1.67          then guess y .. hence "\<bar>x $ k - y $ k\<bar> < \<bar>x $ k - c\<bar>" "y$k \<le> c" apply-apply(rule le_less_trans)
    1.68 -          using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm)
    1.69 +          using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm)
    1.70          thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
    1.71        qed
    1.72        show "~(kk \<inter> {x. x$k \<ge> c} = {}) \<Longrightarrow> x$k \<ge> c"
    1.73 @@ -1563,7 +1563,7 @@
    1.74            using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
    1.75          hence "\<exists>y. y \<in> ball x \<bar>x $ k - c\<bar> \<inter> {x. x $ k \<ge> c}" using goal1(1) by blast 
    1.76          then guess y .. hence "\<bar>x $ k - y $ k\<bar> < \<bar>x $ k - c\<bar>" "y$k \<ge> c" apply-apply(rule le_less_trans)
    1.77 -          using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm)
    1.78 +          using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm)
    1.79          thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
    1.80        qed
    1.81      qed
    1.82 @@ -1676,7 +1676,7 @@
    1.83          then guess e unfolding mem_interior .. note e=this
    1.84          have x:"x$k = c" using x interior_subset by fastsimp
    1.85          have *:"\<And>i. \<bar>(x - (x + (\<chi> i. if i = k then e / 2 else 0))) $ i\<bar> = (if i = k then e/2 else 0)" using e by auto
    1.86 -        have "x + (\<chi> i. if i = k then e/2 else 0) \<in> ball x e" unfolding mem_ball vector_dist_norm 
    1.87 +        have "x + (\<chi> i. if i = k then e/2 else 0) \<in> ball x e" unfolding mem_ball dist_norm 
    1.88            apply(rule le_less_trans[OF norm_le_l1]) unfolding * 
    1.89            unfolding setsum_delta[OF finite_UNIV] using e by auto 
    1.90          hence "x + (\<chi> i. if i = k then e/2 else 0) \<in> {x. x$k = c}" using e by auto
    1.91 @@ -2384,7 +2384,7 @@
    1.92          also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
    1.93          finally show ?case .
    1.94        qed
    1.95 -      show ?case unfolding vector_dist_norm apply(rule lem2) defer
    1.96 +      show ?case unfolding dist_norm apply(rule lem2) defer
    1.97          apply(rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]])
    1.98          using conjunctD2[OF p(2)[unfolded fine_inter]] apply- apply assumption+ apply(rule order_trans)
    1.99          apply(rule rsum_diff_bound[OF p(1), where e="2 / real M"])
   1.100 @@ -2426,7 +2426,7 @@
   1.101            apply-apply(rule less_le_trans,assumption) using `e>0` by auto 
   1.102          thus "inverse (real (N1 + N2) + 1) * content {a..b} \<le> e / 3"
   1.103            unfolding inverse_eq_divide by(auto simp add:field_simps)
   1.104 -        show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded vector_dist_norm],auto)
   1.105 +        show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded dist_norm],auto)
   1.106        qed qed qed qed
   1.107  
   1.108  subsection {* Negligible sets. *}
   1.109 @@ -2510,7 +2510,7 @@
   1.110        show "content l = content (l \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})" apply(rule arg_cong[where f=content])
   1.111          apply(rule set_ext,rule,rule) unfolding mem_Collect_eq
   1.112        proof- fix y assume y:"y\<in>l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
   1.113 -        note this[unfolded subset_eq mem_ball vector_dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this]
   1.114 +        note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this]
   1.115          thus "\<bar>y $ k - c\<bar> \<le> d" unfolding Cart_nth.diff xk by auto
   1.116        qed auto qed
   1.117      note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
   1.118 @@ -2837,7 +2837,7 @@
   1.119      proof safe show "(\<lambda>y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const)
   1.120        fix y assume y:"y\<in>l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
   1.121        note d(2)[OF _ _ this[unfolded mem_ball]]
   1.122 -      thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding vector_dist_norm l norm_minus_commute by fastsimp qed qed
   1.123 +      thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastsimp qed qed
   1.124    from e have "0 \<le> e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
   1.125    thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" by auto qed 
   1.126  
   1.127 @@ -2960,9 +2960,9 @@
   1.128          apply(rule add_mono) apply(rule d(2)[of "x$1" "u$1",unfolded o_def vec1_dest_vec1]) prefer 4
   1.129          apply(rule d(2)[of "x$1" "v$1",unfolded o_def vec1_dest_vec1])
   1.130          using ball[rule_format,of u] ball[rule_format,of v] 
   1.131 -        using xk(1-2) unfolding k subset_eq by(auto simp add:vector_dist_norm norm_real)
   1.132 +        using xk(1-2) unfolding k subset_eq by(auto simp add:dist_norm norm_real)
   1.133        also have "... \<le> e * dest_vec1 (interval_upperbound k - interval_lowerbound k)"
   1.134 -        unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:vector_dist_norm norm_real field_simps)
   1.135 +        unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:dist_norm norm_real field_simps)
   1.136        finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \<le>
   1.137          e * dest_vec1 (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bound_1[OF *] content_1[OF *] .
   1.138      qed(insert as, auto) qed qed
   1.139 @@ -3011,7 +3011,7 @@
   1.140        proof- show "\<bar>(y - x) $ i\<bar> < e" unfolding y_def Cart_lambda_beta vector_minus_component if_P[OF refl]
   1.141            apply(cases) apply(subst if_P,assumption) unfolding if_not_P unfolding i xi using di as(2) by auto
   1.142          show "(\<Sum>i\<in>UNIV - {i}. \<bar>(y - x) $ i\<bar>) \<le> (\<Sum>i\<in>UNIV. 0)" unfolding y_def by auto 
   1.143 -      qed auto thus "dist y x < e" unfolding vector_dist_norm by auto
   1.144 +      qed auto thus "dist y x < e" unfolding dist_norm by auto
   1.145        have "y\<notin>k" unfolding k mem_interval apply rule apply(erule_tac x=i in allE) using xyi unfolding k i xi by auto
   1.146        moreover have "y \<in> \<Union>s" unfolding s mem_interval
   1.147        proof note simps = y_def Cart_lambda_beta if_not_P
   1.148 @@ -3107,7 +3107,7 @@
   1.149          have *:"y - x = norm(y - x)" using False by auto
   1.150          show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {vec1 x..vec1 y}" apply(subst *) unfolding ** by auto
   1.151          show "\<forall>xa\<in>{vec1 x..vec1 y}. norm (f (dest_vec1 xa) - f x) \<le> e" apply safe apply(rule less_imp_le)
   1.152 -          apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto
   1.153 +          apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
   1.154        qed(insert e,auto)
   1.155      next case True have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 x}" apply(rule integrable_subinterval,rule integrable_continuous)
   1.156          apply(rule continuous_on_o_dest_vec1 assms)+  unfolding not_less using assms(2) goal1 by auto
   1.157 @@ -3124,7 +3124,7 @@
   1.158          have *:"x - y = norm(y - x)" using True by auto
   1.159          show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {vec1 y..vec1 x}" apply(subst *) unfolding ** by auto
   1.160          show "\<forall>xa\<in>{vec1 y..vec1 x}. norm (f (dest_vec1 xa) - f x) \<le> e" apply safe apply(rule less_imp_le)
   1.161 -          apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto
   1.162 +          apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
   1.163        qed(insert e,auto) qed qed qed
   1.164  
   1.165  lemma integral_has_vector_derivative': fixes f::"real^1 \<Rightarrow> 'a::banach"
   1.166 @@ -3375,7 +3375,7 @@
   1.167        proof(rule add_mono) case goal1 have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>" using as' by auto
   1.168          thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
   1.169        next case goal2 show ?case apply(rule less_imp_le) apply(cases "a = c") defer
   1.170 -          apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps)
   1.171 +          apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
   1.172        qed finally show "norm (content {vec1 a..vec1 c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4" unfolding content_1'[OF as(1)] by auto
   1.173      qed qed then guess da .. note da=conjunctD2[OF this,rule_format]
   1.174  
   1.175 @@ -3399,7 +3399,7 @@
   1.176        proof(rule add_mono) case goal1 have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>" using as' by auto
   1.177          thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
   1.178        next case goal2 show ?case apply(rule less_imp_le) apply(cases "b = c") defer apply(subst norm_minus_commute)
   1.179 -          apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps)
   1.180 +          apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
   1.181        qed finally show "norm (content {vec1 c..vec1 b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" unfolding content_1'[OF as(1)] by auto
   1.182      qed qed then guess db .. note db=conjunctD2[OF this,rule_format]
   1.183  
   1.184 @@ -3663,11 +3663,11 @@
   1.185    proof- assume "x=a" have "a \<le> a" by auto
   1.186      from indefinite_integral_continuous_right[OF assms(1) this `a<b` `e>0`] guess d . note d=this
   1.187      show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
   1.188 -      unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.189 +      unfolding `x=a` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.190    next   assume "x=b" have "b \<le> b" by auto
   1.191      from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
   1.192      show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
   1.193 -      unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.194 +      unfolding `x=b` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.195    next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: vector_less_def)
   1.196      from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
   1.197      from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
   1.198 @@ -3675,7 +3675,7 @@
   1.199      proof safe show "0 < min d1 d2" using d1 d2 by auto
   1.200        fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"
   1.201        thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute)
   1.202 -        apply(cases "y < x") unfolding vector_dist_norm apply(rule d1(2)[rule_format]) defer
   1.203 +        apply(cases "y < x") unfolding dist_norm apply(rule d1(2)[rule_format]) defer
   1.204          apply(rule d2(2)[rule_format]) unfolding Cart_simps not_less norm_real by(auto simp add:field_simps)
   1.205      qed qed qed 
   1.206  
   1.207 @@ -3831,7 +3831,7 @@
   1.208        thus "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}" unfolding s
   1.209          apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s])
   1.210          apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE)
   1.211 -        by(auto simp add:vector_dist_norm)
   1.212 +        by(auto simp add:dist_norm)
   1.213      qed(insert B `e>0`, auto)
   1.214    next assume as:"\<forall>e>0. ?r e" 
   1.215      from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format]
   1.216 @@ -3839,7 +3839,7 @@
   1.217      have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
   1.218      proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
   1.219          by(auto simp add:field_simps) qed
   1.220 -    have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm 
   1.221 +    have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm 
   1.222      proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   1.223      from C(2)[OF this] have "\<exists>y. (f has_integral y) {a..b}"
   1.224        unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,THEN sym] unfolding s by auto
   1.225 @@ -3851,7 +3851,7 @@
   1.226        have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
   1.227        proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
   1.228            by(auto simp add:field_simps) qed
   1.229 -      have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm 
   1.230 +      have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm 
   1.231        proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   1.232        note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
   1.233        note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
   1.234 @@ -4037,7 +4037,7 @@
   1.235      from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format]
   1.236      let ?a = "(\<chi> i. min (a$i) (-B))::real^'n" and ?b = "(\<chi> i. max (b$i) B)::real^'n"
   1.237      show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b])
   1.238 -    proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval vector_dist_norm
   1.239 +    proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval dist_norm
   1.240        proof case goal1 thus ?case using component_le_norm[of x i] by(auto simp add:field_simps) qed
   1.241        from B(2)[OF this] guess z .. note conjunct1[OF this]
   1.242        thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto
   1.243 @@ -4071,10 +4071,10 @@
   1.244      from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
   1.245      from real_arch_simple[of B] guess N .. note N = this
   1.246      { fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> {\<chi> i. - real n..\<chi> i. real n}" apply safe
   1.247 -        unfolding mem_ball mem_interval vector_dist_norm
   1.248 +        unfolding mem_ball mem_interval dist_norm
   1.249        proof case goal1 thus ?case using component_le_norm[of x i]
   1.250            using n N by(auto simp add:field_simps) qed }
   1.251 -    thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto
   1.252 +    thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding dist_norm apply(rule B(2)) by auto
   1.253    qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i ..
   1.254    note i = this[unfolded Lim_sequentially, rule_format]
   1.255  
   1.256 @@ -4089,11 +4089,11 @@
   1.257        from real_arch_simple[of ?B] guess n .. note n=this
   1.258        show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
   1.259          apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute)
   1.260 -        apply(rule N[unfolded vector_dist_norm, of n])
   1.261 +        apply(rule N[unfolded dist_norm, of n])
   1.262        proof safe show "N \<le> n" using n by auto
   1.263          fix x::"real^'n" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto
   1.264          thus "x\<in>{a..b}" using ab by blast 
   1.265 -        show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply-
   1.266 +        show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball dist_norm apply-
   1.267          proof case goal1 thus ?case using component_le_norm[of x i]
   1.268              using n by(auto simp add:field_simps) qed qed qed qed qed
   1.269  
   1.270 @@ -4159,7 +4159,7 @@
   1.271      note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
   1.272      note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
   1.273      def c \<equiv> "\<chi> i. min (a$i) (- (max B1 B2))" and d \<equiv> "\<chi> i. max (b$i) (max B1 B2)"
   1.274 -    have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm
   1.275 +    have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval dist_norm
   1.276      proof(rule_tac[!] allI)
   1.277        case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next
   1.278        case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   1.279 @@ -4622,7 +4622,7 @@
   1.280          from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this
   1.281          have **:"norm (integral {a..b} (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
   1.282            apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N]
   1.283 -          unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto
   1.284 +          unfolding dist_norm apply-defer apply(subst norm_minus_commute) by auto
   1.285          have *:"\<And>f1 f2 g. abs(f1 - i$1) < e / 2 \<longrightarrow> abs(f2 - g) < e / 2 \<longrightarrow> f1 \<le> f2 \<longrightarrow> f2 \<le> i$1
   1.286            \<longrightarrow> abs(g - i$1) < e" by arith
   1.287          show "norm (integral {a..b} (\<lambda>x. if x \<in> s then g x else 0) - i) < e"