--- a/src/HOL/Library/normarith.ML Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Library/normarith.ML Wed Apr 28 22:20:59 2010 -0700
@@ -395,7 +395,7 @@
fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
- (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+ (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
then_conv field_comp_conv
then_conv nnf_conv
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Apr 28 22:20:59 2010 -0700
@@ -1190,7 +1190,7 @@
have d':"d / real n / 8 > 0" apply(rule divide_pos_pos)+ using d(1) unfolding n_def by auto
have *:"uniformly_continuous_on {0..1} f" by(rule compact_uniformly_continuous[OF assms(1) compact_interval])
guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] apply-apply(erule exE,(erule conjE)+) .
- note e=this[rule_format,unfolded vector_dist_norm]
+ note e=this[rule_format,unfolded dist_norm]
show ?thesis apply(rule_tac x="min (e/2) (d/real n/8)" in exI) apply(rule) defer
apply(rule,rule,rule,rule,rule) apply(erule conjE)+ proof-
show "0 < min (e / 2) (d / real n / 8)" using d' e by auto
@@ -1202,7 +1202,7 @@
show "\<bar>f x $ i - x $ i\<bar> \<le> norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as by auto
show "\<bar>f x $ i - f z $ i\<bar> \<le> norm (f x - f z)" "\<bar>x $ i - z $ i\<bar> \<le> norm (x - z)"
unfolding vector_minus_component[THEN sym] by(rule component_le_norm)+
- have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded vector_dist_norm]
+ have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
unfolding norm_minus_commute by auto
also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
finally show "norm (f y - f x) < d / real n / 8" apply- apply(rule e(2)) using as by auto
@@ -1355,14 +1355,14 @@
assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
obtains x where "x \<in> s" "f x = x" proof-
have "\<exists>e>0. s \<subseteq> cball 0 e" using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
- apply(erule_tac exE,rule_tac x=b in exI) by(auto simp add: vector_dist_norm)
+ apply(erule_tac exE,rule_tac x=b in exI) by(auto simp add: dist_norm)
then guess e apply-apply(erule exE,(erule conjE)+) . note e=this
have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
apply(rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"]) apply(rule continuous_on_compose )
apply(rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
apply(rule continuous_on_subset[OF assms(4)])
using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)] apply - defer
- using assms(5)[unfolded subset_eq] using e(2)[unfolded subset_eq mem_cball] by(auto simp add:vector_dist_norm)
+ using assms(5)[unfolded subset_eq] using e(2)[unfolded subset_eq mem_cball] by(auto simp add: dist_norm)
then guess x .. note x=this
have *:"closest_point s x = x" apply(rule closest_point_self)
apply(rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"],unfolded image_iff])
@@ -1380,7 +1380,7 @@
apply(rule,rule,erule conjE) apply(rule brouwer_ball[OF assms]) apply assumption+
apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+
unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE)
- unfolding vector_dist_norm apply(simp add: * norm_minus_commute) . note x = this
+ unfolding dist_norm apply(simp add: * norm_minus_commute) . note x = this
hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps)
hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto
thus False using x using assms by auto qed
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 28 22:20:59 2010 -0700
@@ -31,14 +31,14 @@
assume ?l note as = this[unfolded deriv_def LIM_def,rule_format]
show ?r unfolding has_derivative_def Lim_at apply- apply(rule,rule mult.bounded_linear_right)
apply safe apply(drule as,safe) apply(rule_tac x=s in exI) apply safe
- apply(erule_tac x="xa - x" in allE) unfolding vector_dist_norm netlimit_at[of x] unfolding diff_0_right norm_scaleR
+ apply(erule_tac x="xa - x" in allE) unfolding dist_norm netlimit_at[of x] unfolding diff_0_right norm_scaleR
by(auto simp add:field_simps)
next assume ?r note this[unfolded has_derivative_def Lim_at] note as=conjunct2[OF this,rule_format]
have *:"\<And>x xa f'. xa \<noteq> 0 \<Longrightarrow> \<bar>(f (xa + x) - f x) / xa - f'\<bar> = \<bar>(f (xa + x) - f x) - xa * f'\<bar> / \<bar>xa\<bar>" by(auto simp add:field_simps)
show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe)
apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE)
- unfolding vector_dist_norm diff_0_right norm_scaleR
- unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
+ unfolding dist_norm diff_0_right norm_scaleR
+ unfolding dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof
assume ?l note as = this[unfolded fderiv_def]
@@ -48,14 +48,14 @@
thus "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e"
apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE)
- unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
+ unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
assume ?r note as = this[unfolded has_derivative_def]
show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
fix e::real assume "e>0"
guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] ..
thus "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply-
apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE)
- unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
+ unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
subsection {* These are the only cases we'll care about, probably. *}
@@ -73,7 +73,7 @@
"(f has_derivative f')(at x within s) \<longleftrightarrow> bounded_linear f' \<and>
(\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm(x' - x) \<and> norm(x' - x) < d
\<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
- unfolding has_derivative_within Lim_within vector_dist_norm
+ unfolding has_derivative_within Lim_within dist_norm
unfolding diff_0_right norm_mul by (simp add: diff_diff_eq)
lemma has_derivative_at':
@@ -216,7 +216,7 @@
using assms[unfolded has_derivative_def Lim] by auto
thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
proof (rule eventually_elim1)
- case goal1 thus ?case apply - unfolding vector_dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1
+ case goal1 thus ?case apply - unfolding dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1
using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
qed
qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed
@@ -326,7 +326,7 @@
lemma Lim_mul_norm_within: fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f(x)) ---> 0) (at a within s)"
unfolding Lim_within apply(rule,rule) apply(erule_tac x=e in allE,erule impE,assumption,erule exE,erule conjE)
- apply(rule_tac x="min d 1" in exI) apply rule defer apply(rule,erule_tac x=x in ballE) unfolding vector_dist_norm diff_0_right norm_mul
+ apply(rule_tac x="min d 1" in exI) apply rule defer apply(rule,erule_tac x=x in ballE) unfolding dist_norm diff_0_right norm_mul
by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
lemma differentiable_imp_continuous_within: assumes "f differentiable (at x within s)"
@@ -339,7 +339,7 @@
apply(rule continuous_within_compose) apply(rule continuous_intros)+
by(rule linear_continuous_within[OF f'[THEN conjunct1]])
show ?thesis unfolding continuous_within using f'[THEN conjunct2, THEN Lim_mul_norm_within]
- apply-apply(drule Lim_add) apply(rule **[unfolded continuous_within]) unfolding Lim_within and vector_dist_norm
+ apply-apply(drule Lim_add) apply(rule **[unfolded continuous_within]) unfolding Lim_within and dist_norm
apply(rule,rule) apply(erule_tac x=e in allE) apply(erule impE|assumption)+ apply(erule exE,rule_tac x=d in exI)
by(auto simp add:zero * elim!:allE) qed
@@ -379,13 +379,13 @@
show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)" proof(cases "y=x")
case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero) next
case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\<in>s`]
- unfolding vector_dist_norm diff_0_right norm_mul using as(3)
- using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded vector_dist_norm]
+ unfolding dist_norm diff_0_right norm_mul using as(3)
+ using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm]
by (auto simp add: linear_0 linear_sub)
thus ?thesis by(auto simp add:algebra_simps) qed qed next
assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption)
apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI)
- apply(erule conjE,rule,assumption,rule,rule) unfolding vector_dist_norm diff_0_right norm_scaleR
+ apply(erule conjE,rule,assumption,rule,rule) unfolding dist_norm diff_0_right norm_scaleR
apply(erule_tac x=xa in ballE,erule impE) proof-
fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \<in> s" "0 < norm (y - x) \<and> norm (y - x) < d"
"norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
@@ -513,7 +513,7 @@
guess a using UNIV_witness[where 'a='a] ..
fix e::real assume "0<e" guess d using assms(3)[rule_format,OF`e>0`,of a] ..
thus "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x="x + d*\<^sub>R basis a" in bexI)
- using basis_nonzero[of a] norm_basis[of a] unfolding vector_dist_norm by auto qed
+ using basis_nonzero[of a] norm_basis[of a] unfolding dist_norm by auto qed
hence *:"netlimit (at x within s) = x" apply-apply(rule netlimit_within) unfolding trivial_limit_within by simp
show ?thesis apply(rule linear_eq_stdbasis) unfolding linear_conv_bounded_linear
apply(rule as(1,2)[THEN conjunct1])+ proof(rule,rule ccontr)
@@ -526,7 +526,7 @@
also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))"
unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto
also have "\<dots> = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus)
- finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm
+ finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding dist_norm
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed
lemma frechet_derivative_unique_at: fixes f::"real^'a \<Rightarrow> real^'b"
@@ -607,7 +607,7 @@
unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric]
unfolding inner_simps dot_basis smult_conv_scaleR by simp } note * = this
have "x + d *\<^sub>R basis j \<in> ball x e" "x - d *\<^sub>R basis j \<in> ball x e"
- unfolding mem_ball vector_dist_norm using norm_basis[of j] d by auto
+ unfolding mem_ball dist_norm using norm_basis[of j] d by auto
hence **:"((f (x - d *\<^sub>R basis j))$k \<le> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<le> (f x)$k) \<or>
((f (x - d *\<^sub>R basis j))$k \<ge> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<ge> (f x)$k)" using assms(2) by auto
have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
@@ -787,14 +787,14 @@
guess d2 using assms(5)[unfolded open_dist,rule_format,OF assms(6)] .. note d2=this
guess d using real_lbound_gt_zero[OF d1[THEN conjunct1] d2[THEN conjunct1]] .. note d=this
thus ?case apply(rule_tac x=d in exI) apply rule defer proof(rule,rule)
- fix z assume as:"norm (z - y) < d" hence "z\<in>t" using d2 d unfolding vector_dist_norm by auto
+ fix z assume as:"norm (z - y) < d" hence "z\<in>t" using d2 d unfolding dist_norm by auto
have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
unfolding g'.diff f'.diff unfolding assms(3)[unfolded o_def id_def, THEN fun_cong]
unfolding assms(7)[rule_format,OF `z\<in>t`] apply(subst norm_minus_cancel[THEN sym]) by auto
also have "\<dots> \<le> norm(f (g z) - y - f' (g z - g y)) * C" by(rule C[THEN conjunct2,rule_format])
also have "\<dots> \<le> (e / C) * norm (g z - g y) * C" apply(rule mult_right_mono)
apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]]) apply(cases "z=y") defer
- apply(rule d1[THEN conjunct2, unfolded vector_dist_norm,rule_format]) using as d C d0 by auto
+ apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format]) using as d C d0 by auto
also have "\<dots> \<le> e * norm (g z - g y)" using C by(auto simp add:field_simps)
finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)" by simp qed auto qed
have *:"(0::real) < 1 / 2" by auto guess d using lem1[rule_format,OF *] .. note d=this def B\<equiv>"C*2"
@@ -882,36 +882,36 @@
apply(rule continuous_on_intros linear_continuous_on[OF assms(5)])+
apply(rule continuous_on_subset[OF assms(2)]) apply(rule,unfold image_iff,erule bexE) proof-
fix y z assume as:"y \<in>cball (f x) e" "z = x + (g' y - g' (f x))"
- have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and vector_dist_norm by auto
+ have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and dist_norm by auto
also have "\<dots> \<le> norm (f x - y) * B" unfolding g'.diff[THEN sym] using B by auto
- also have "\<dots> \<le> e * B" using as(1)[unfolded mem_cball vector_dist_norm] using B by auto
+ also have "\<dots> \<le> e * B" using as(1)[unfolded mem_cball dist_norm] using B by auto
also have "\<dots> \<le> e1" using e unfolding less_divide_eq using B by auto
finally have "z\<in>cball x e1" unfolding mem_cball by force
thus "z \<in> s" using e1 assms(7) by auto qed next
fix y z assume as:"y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
have "norm (g' (z - f x)) \<le> norm (z - f x) * B" using B by auto
- also have "\<dots> \<le> e * B" apply(rule mult_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] and B unfolding norm_minus_commute by auto
+ also have "\<dots> \<le> e * B" apply(rule mult_right_mono) using as(2)[unfolded mem_cball dist_norm] and B unfolding norm_minus_commute by auto
also have "\<dots> < e0" using e and B unfolding less_divide_eq by auto
finally have *:"norm (x + g' (z - f x) - x) < e0" by auto
have **:"f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto
have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le> norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:algebra_simps)
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding algebra_simps ** by auto
- also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball vector_dist_norm] by auto
+ also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball dist_norm] by auto
also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2" using * and B by(auto simp add:field_simps)
also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2" by auto
- also have "\<dots> \<le> e/2 + e/2" apply(rule add_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] unfolding norm_minus_commute by auto
- finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e" unfolding mem_cball vector_dist_norm by auto
+ also have "\<dots> \<le> e/2 + e/2" apply(rule add_right_mono) using as(2)[unfolded mem_cball dist_norm] unfolding norm_minus_commute by auto
+ finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e" unfolding mem_cball dist_norm by auto
qed(insert e, auto) note lem = this
show ?thesis unfolding mem_interior apply(rule_tac x="e/2" in exI)
apply(rule,rule divide_pos_pos) prefer 3 proof
fix y assume "y \<in> ball (f x) (e/2)" hence *:"y\<in>cball (f x) (e/2)" by auto
guess z using lem[rule_format,OF *] .. note z=this
hence "norm (g' (z - f x)) \<le> norm (z - f x) * B" using B by(auto simp add:field_simps)
- also have "\<dots> \<le> e * B" apply(rule mult_right_mono) using z(1) unfolding mem_cball vector_dist_norm norm_minus_commute using B by auto
+ also have "\<dots> \<le> e * B" apply(rule mult_right_mono) using z(1) unfolding mem_cball dist_norm norm_minus_commute using B by auto
also have "\<dots> \<le> e1" using e B unfolding less_divide_eq by auto
finally have "x + g'(z - f x) \<in> t" apply- apply(rule e1[THEN conjunct2,unfolded subset_eq,rule_format])
- unfolding mem_cball vector_dist_norm by auto
+ unfolding mem_cball dist_norm by auto
thus "y \<in> f ` t" using z by auto qed(insert e, auto) qed
text {* Hence the following eccentric variant of the inverse function theorem. *)
@@ -1059,9 +1059,9 @@
show " \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" apply(rule_tac x="max M N" in exI) proof(default+)
fix m n assume as:"max M N \<le>m" "max M N\<le>n"
have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
- unfolding vector_dist_norm by(rule norm_triangle_sub)
+ unfolding dist_norm by(rule norm_triangle_sub)
also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2" using N[rule_format,OF _ _ `x\<in>s` `x0\<in>s`, of m n] and as and False by auto
- also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding vector_dist_norm by auto
+ also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding dist_norm by auto
finally show "dist (f m x) (f n x) < e" by auto qed qed qed qed
then guess g .. note g = this
have lem2:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm((f n x - f n y) - (g x - g y)) \<le> e * norm(x - y)" proof(rule,rule)
@@ -1085,7 +1085,7 @@
case False hence *:"e / 2 / norm u > 0" using `e>0` by(auto intro!: divide_pos_pos)
guess N using assms(3)[rule_format,OF *] .. note N=this
show ?thesis apply(rule_tac x=N in exI) proof(rule,rule) case goal1
- show ?case unfolding vector_dist_norm using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0`
+ show ?case unfolding dist_norm using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0`
by (auto simp add:field_simps) qed qed qed
show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule)
fix x' y z::"real^'m" and c::real
@@ -1184,9 +1184,9 @@
apply(rule mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
also have "\<dots> = (B * C * D * norm (y - x)) * norm (y - x)" by(auto simp add:field_simps)
also have "\<dots> < e * norm (y - x)" apply(rule mult_strict_right_mono)
- using as(3)[unfolded vector_dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
+ using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
- unfolding vector_dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
+ unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))" unfolding linear_linear linear_def
unfolding smult_conv_scaleR unfolding g'.add f'.scaleR f'.add g'.scaleR
unfolding h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right by auto
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 22:20:59 2010 -0700
@@ -915,11 +915,6 @@
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
using norm_ge_zero[of "x - y"] by auto
-lemma vector_dist_norm:
- fixes x :: "'a::real_normed_vector"
- shows "dist x y = norm (x - y)"
- by (rule dist_norm)
-
use "normarith.ML"
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
@@ -966,12 +961,12 @@
lemma norm_triangle_half_r:
shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
- using dist_triangle_half_r unfolding vector_dist_norm[THEN sym] by auto
+ using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2"
shows "norm (x - x') < e"
- using dist_triangle_half_l[OF assms[unfolded vector_dist_norm[THEN sym]]]
- unfolding vector_dist_norm[THEN sym] .
+ using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]]
+ unfolding dist_norm[THEN sym] .
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
by (metis order_trans norm_triangle_ineq)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 28 22:20:59 2010 -0700
@@ -137,27 +137,27 @@
hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE)
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)
fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
- hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto
+ hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
hence "y$k < a$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps)
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
moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
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)"
apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"])
unfolding norm_scaleR norm_basis by auto
- 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)
- finally show "y\<in>ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed
+ 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)
+ finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto
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)
fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
- hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto
+ hence "\<bar>(?z - y) $ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
hence "y$k > b$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps)
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
moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
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)"
apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"])
unfolding norm_scaleR norm_basis by auto
- 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)
- finally show "y\<in>ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed
+ 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)
+ finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed
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
thus ?thesis apply-apply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this
@@ -1067,7 +1067,7 @@
proof- case goal1 guess n using real_arch_pow2[of "(setsum (\<lambda>i. b$i - a$i) UNIV) / e"] .. note n=this
show ?case apply(rule_tac x=n in exI) proof(rule,rule)
fix x y assume xy:"x\<in>{A n..B n}" "y\<in>{A n..B n}"
- have "dist x y \<le> setsum (\<lambda>i. abs((x - y)$i)) UNIV" unfolding vector_dist_norm by(rule norm_le_l1)
+ have "dist x y \<le> setsum (\<lambda>i. abs((x - y)$i)) UNIV" unfolding dist_norm by(rule norm_le_l1)
also have "\<dots> \<le> setsum (\<lambda>i. B n$i - A n$i) UNIV"
proof(rule setsum_mono) fix i show "\<bar>(x - y) $ i\<bar> \<le> B n $ i - A n $ i"
using xy[unfolded mem_interval,THEN spec[where x=i]]
@@ -1417,7 +1417,7 @@
show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+)
proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2"
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"
- apply(rule dist_triangle_half_l[where y=y,unfolded vector_dist_norm])
+ apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm])
using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
qed qed
next assume "\<forall>e>0. \<exists>d. ?P e d" hence "\<forall>n::nat. \<exists>d. ?P (inverse(real (n + 1))) d" by auto
@@ -1447,7 +1447,7 @@
have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto
show "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r)
apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer
- using N2[rule_format,unfolded vector_dist_norm,of "N1+N2"]
+ using N2[rule_format,unfolded dist_norm,of "N1+N2"]
using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed
subsection {* Additivity of integral on abutting intervals. *}
@@ -1554,7 +1554,7 @@
using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
hence "\<exists>y. y \<in> ball x \<bar>x $ k - c\<bar> \<inter> {x. x $ k \<le> c}" using goal1(1) by blast
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)
- using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm)
+ using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm)
thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
qed
show "~(kk \<inter> {x. x$k \<ge> c} = {}) \<Longrightarrow> x$k \<ge> c"
@@ -1563,7 +1563,7 @@
using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
hence "\<exists>y. y \<in> ball x \<bar>x $ k - c\<bar> \<inter> {x. x $ k \<ge> c}" using goal1(1) by blast
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)
- using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm)
+ using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm)
thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
qed
qed
@@ -1676,7 +1676,7 @@
then guess e unfolding mem_interior .. note e=this
have x:"x$k = c" using x interior_subset by fastsimp
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
- have "x + (\<chi> i. if i = k then e/2 else 0) \<in> ball x e" unfolding mem_ball vector_dist_norm
+ have "x + (\<chi> i. if i = k then e/2 else 0) \<in> ball x e" unfolding mem_ball dist_norm
apply(rule le_less_trans[OF norm_le_l1]) unfolding *
unfolding setsum_delta[OF finite_UNIV] using e by auto
hence "x + (\<chi> i. if i = k then e/2 else 0) \<in> {x. x$k = c}" using e by auto
@@ -2384,7 +2384,7 @@
also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
finally show ?case .
qed
- show ?case unfolding vector_dist_norm apply(rule lem2) defer
+ show ?case unfolding dist_norm apply(rule lem2) defer
apply(rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]])
using conjunctD2[OF p(2)[unfolded fine_inter]] apply- apply assumption+ apply(rule order_trans)
apply(rule rsum_diff_bound[OF p(1), where e="2 / real M"])
@@ -2426,7 +2426,7 @@
apply-apply(rule less_le_trans,assumption) using `e>0` by auto
thus "inverse (real (N1 + N2) + 1) * content {a..b} \<le> e / 3"
unfolding inverse_eq_divide by(auto simp add:field_simps)
- show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded vector_dist_norm],auto)
+ show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded dist_norm],auto)
qed qed qed qed
subsection {* Negligible sets. *}
@@ -2510,7 +2510,7 @@
show "content l = content (l \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})" apply(rule arg_cong[where f=content])
apply(rule set_ext,rule,rule) unfolding mem_Collect_eq
proof- fix y assume y:"y\<in>l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
- 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]
+ note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this]
thus "\<bar>y $ k - c\<bar> \<le> d" unfolding Cart_nth.diff xk by auto
qed auto qed
note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
@@ -2837,7 +2837,7 @@
proof safe show "(\<lambda>y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const)
fix y assume y:"y\<in>l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
note d(2)[OF _ _ this[unfolded mem_ball]]
- 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
+ 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
from e have "0 \<le> e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" by auto qed
@@ -2960,9 +2960,9 @@
apply(rule add_mono) apply(rule d(2)[of "x$1" "u$1",unfolded o_def vec1_dest_vec1]) prefer 4
apply(rule d(2)[of "x$1" "v$1",unfolded o_def vec1_dest_vec1])
using ball[rule_format,of u] ball[rule_format,of v]
- using xk(1-2) unfolding k subset_eq by(auto simp add:vector_dist_norm norm_real)
+ using xk(1-2) unfolding k subset_eq by(auto simp add:dist_norm norm_real)
also have "... \<le> e * dest_vec1 (interval_upperbound k - interval_lowerbound k)"
- unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:vector_dist_norm norm_real field_simps)
+ unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:dist_norm norm_real field_simps)
finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \<le>
e * dest_vec1 (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bound_1[OF *] content_1[OF *] .
qed(insert as, auto) qed qed
@@ -3011,7 +3011,7 @@
proof- show "\<bar>(y - x) $ i\<bar> < e" unfolding y_def Cart_lambda_beta vector_minus_component if_P[OF refl]
apply(cases) apply(subst if_P,assumption) unfolding if_not_P unfolding i xi using di as(2) by auto
show "(\<Sum>i\<in>UNIV - {i}. \<bar>(y - x) $ i\<bar>) \<le> (\<Sum>i\<in>UNIV. 0)" unfolding y_def by auto
- qed auto thus "dist y x < e" unfolding vector_dist_norm by auto
+ qed auto thus "dist y x < e" unfolding dist_norm by auto
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
moreover have "y \<in> \<Union>s" unfolding s mem_interval
proof note simps = y_def Cart_lambda_beta if_not_P
@@ -3107,7 +3107,7 @@
have *:"y - x = norm(y - x)" using False by auto
show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {vec1 x..vec1 y}" apply(subst *) unfolding ** by auto
show "\<forall>xa\<in>{vec1 x..vec1 y}. norm (f (dest_vec1 xa) - f x) \<le> e" apply safe apply(rule less_imp_le)
- apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto
+ apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
qed(insert e,auto)
next case True have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 x}" apply(rule integrable_subinterval,rule integrable_continuous)
apply(rule continuous_on_o_dest_vec1 assms)+ unfolding not_less using assms(2) goal1 by auto
@@ -3124,7 +3124,7 @@
have *:"x - y = norm(y - x)" using True by auto
show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {vec1 y..vec1 x}" apply(subst *) unfolding ** by auto
show "\<forall>xa\<in>{vec1 y..vec1 x}. norm (f (dest_vec1 xa) - f x) \<le> e" apply safe apply(rule less_imp_le)
- apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto
+ apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
qed(insert e,auto) qed qed qed
lemma integral_has_vector_derivative': fixes f::"real^1 \<Rightarrow> 'a::banach"
@@ -3375,7 +3375,7 @@
proof(rule add_mono) case goal1 have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>" using as' by auto
thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
next case goal2 show ?case apply(rule less_imp_le) apply(cases "a = c") defer
- apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps)
+ apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
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
qed qed then guess da .. note da=conjunctD2[OF this,rule_format]
@@ -3399,7 +3399,7 @@
proof(rule add_mono) case goal1 have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>" using as' by auto
thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
next case goal2 show ?case apply(rule less_imp_le) apply(cases "b = c") defer apply(subst norm_minus_commute)
- apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps)
+ apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
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
qed qed then guess db .. note db=conjunctD2[OF this,rule_format]
@@ -3663,11 +3663,11 @@
proof- assume "x=a" have "a \<le> a" by auto
from indefinite_integral_continuous_right[OF assms(1) this `a<b` `e>0`] guess d . note d=this
show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
- unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
+ unfolding `x=a` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
next assume "x=b" have "b \<le> b" by auto
from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
- unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
+ unfolding `x=b` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
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)
from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
@@ -3675,7 +3675,7 @@
proof safe show "0 < min d1 d2" using d1 d2 by auto
fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"
thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute)
- apply(cases "y < x") unfolding vector_dist_norm apply(rule d1(2)[rule_format]) defer
+ apply(cases "y < x") unfolding dist_norm apply(rule d1(2)[rule_format]) defer
apply(rule d2(2)[rule_format]) unfolding Cart_simps not_less norm_real by(auto simp add:field_simps)
qed qed qed
@@ -3831,7 +3831,7 @@
thus "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}" unfolding s
apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s])
apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE)
- by(auto simp add:vector_dist_norm)
+ by(auto simp add:dist_norm)
qed(insert B `e>0`, auto)
next assume as:"\<forall>e>0. ?r e"
from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format]
@@ -3839,7 +3839,7 @@
have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
by(auto simp add:field_simps) qed
- have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm
+ have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm
proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
from C(2)[OF this] have "\<exists>y. (f has_integral y) {a..b}"
unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,THEN sym] unfolding s by auto
@@ -3851,7 +3851,7 @@
have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
by(auto simp add:field_simps) qed
- have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm
+ have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm
proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
@@ -4037,7 +4037,7 @@
from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format]
let ?a = "(\<chi> i. min (a$i) (-B))::real^'n" and ?b = "(\<chi> i. max (b$i) B)::real^'n"
show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b])
- proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval vector_dist_norm
+ proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval dist_norm
proof case goal1 thus ?case using component_le_norm[of x i] by(auto simp add:field_simps) qed
from B(2)[OF this] guess z .. note conjunct1[OF this]
thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto
@@ -4071,10 +4071,10 @@
from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
from real_arch_simple[of B] guess N .. note N = this
{ fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> {\<chi> i. - real n..\<chi> i. real n}" apply safe
- unfolding mem_ball mem_interval vector_dist_norm
+ unfolding mem_ball mem_interval dist_norm
proof case goal1 thus ?case using component_le_norm[of x i]
using n N by(auto simp add:field_simps) qed }
- thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto
+ thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding dist_norm apply(rule B(2)) by auto
qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i ..
note i = this[unfolded Lim_sequentially, rule_format]
@@ -4089,11 +4089,11 @@
from real_arch_simple[of ?B] guess n .. note n=this
show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute)
- apply(rule N[unfolded vector_dist_norm, of n])
+ apply(rule N[unfolded dist_norm, of n])
proof safe show "N \<le> n" using n by auto
fix x::"real^'n" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto
thus "x\<in>{a..b}" using ab by blast
- show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply-
+ show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball dist_norm apply-
proof case goal1 thus ?case using component_le_norm[of x i]
using n by(auto simp add:field_simps) qed qed qed qed qed
@@ -4159,7 +4159,7 @@
note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
def c \<equiv> "\<chi> i. min (a$i) (- (max B1 B2))" and d \<equiv> "\<chi> i. max (b$i) (max B1 B2)"
- have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm
+ have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval dist_norm
proof(rule_tac[!] allI)
case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next
case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
@@ -4622,7 +4622,7 @@
from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this
have **:"norm (integral {a..b} (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N]
- unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto
+ unfolding dist_norm apply-defer apply(subst norm_minus_commute) by auto
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
\<longrightarrow> abs(g - i$1) < e" by arith
show "norm (integral {a..b} (\<lambda>x. if x \<in> s then g x else 0) - i) < e"
--- a/src/HOL/Multivariate_Analysis/Vec1.thy Wed Apr 28 22:02:55 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy Wed Apr 28 22:20:59 2010 -0700
@@ -386,7 +386,7 @@
apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
+lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto
lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-