author huffman Tue, 09 Jun 2009 16:13:18 -0700 changeset 31558 e7a282113145 parent 31538 16068eb224c0 child 31559 ca9e56897403
remove uses of vec1 in continuity lemmas
```--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 16:13:18 2009 -0700
@@ -1213,9 +1213,22 @@
qed
qed

+lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
+unfolding open_vector_def all_1
+by (auto simp add: dest_vec1_def)
+
+lemma tendsto_dest_vec1: "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
+  unfolding tendsto_def
+  apply clarify
+  apply (drule_tac x="dest_vec1 -` S" in spec)
+  apply (simp add: open_dest_vec1_vimage)
+  done
+
+lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
+  unfolding continuous_def by (rule tendsto_dest_vec1)

lemma compact_convex_combinations:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "(real ^ 'n::finite) set"
assumes "compact s" "compact t"
shows "compact { (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
proof-
@@ -1229,9 +1242,10 @@
hence "continuous (at (pastecart u (pastecart x y)))
(\<lambda>z. fstcart (sndcart z) - dest_vec1 (fstcart z) *s fstcart (sndcart z) +
dest_vec1 (fstcart z) *s sndcart (sndcart z))"
-      apply (auto intro!: continuous_add continuous_sub continuous_mul simp add: o_def vec1_dest_vec1)
+      apply (auto intro!: continuous_add continuous_sub continuous_mul continuous_dest_vec1
+                  simp add: o_def vec1_dest_vec1)
using linear_continuous_at linear_fstcart linear_sndcart linear_sndcart
-      using linear_compose[unfolded o_def] by auto }
+      using linear_compose[unfolded o_def] by auto  }
hence "continuous_on {pastecart u w |u w. u \<in> {vec1 0..vec1 1} \<and> w \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}}
(\<lambda>z. (1 - dest_vec1 (fstcart z)) *s fstcart (sndcart z) + dest_vec1 (fstcart z) *s sndcart (sndcart z))"
apply(rule_tac continuous_at_imp_continuous_on) unfolding mem_Collect_eq
@@ -1888,7 +1902,9 @@
unfolding image_image[of "\<lambda>u. u *s x" "\<lambda>x. dest_vec1 x", THEN sym]
unfolding dest_vec1_inverval vec1_dest_vec1 by auto
have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
-    apply(rule, rule continuous_vmul) unfolding o_def vec1_dest_vec1 apply(rule continuous_at_id) by(rule compact_interval)
+    apply(rule, rule continuous_vmul)
+    apply (rule continuous_dest_vec1)
+    apply(rule continuous_at_id) by(rule compact_interval)
moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *s x} \<inter> s \<noteq> {}" apply(rule not_disjointI[OF _ assms(2)])
unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos)
ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *s x"
@@ -1925,12 +1941,13 @@
have injpi:"\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y" unfolding pi_def by auto

have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on)
-    apply rule unfolding pi_def apply(rule continuous_mul) unfolding o_def
-    apply(rule continuous_at_inv[unfolded o_def]) unfolding continuous_at_vec1_range[unfolded o_def]
-    apply(rule,rule) apply(rule_tac x=e in exI) apply(rule,assumption,rule,rule)
-    proof- fix e x y assume "0 < e" "norm (y - x::real^'n) < e"
-      thus "\<bar>norm y - norm x\<bar> < e" using norm_triangle_ineq3[of y x] by auto
-    qed(auto intro!:continuous_at_id)
+    apply rule unfolding pi_def
+    apply (rule continuous_mul)
+    apply (rule continuous_at_inv[unfolded o_def])
+    apply (rule continuous_at_norm)
+    apply simp
+    apply (rule continuous_at_id)
+    done
def sphere \<equiv> "{x::real^'n. norm x = 1}"
have pi:"\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *s x) = pi x" unfolding pi_def sphere_def by auto

@@ -2015,7 +2032,7 @@
prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac  hom2) proof-
fix x::"real^'n" assume as:"x \<in> cball 0 1"
thus "continuous (at x) (\<lambda>x. norm x *s surf (pi x))" proof(cases "x=0")
-      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
+      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_norm)
using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
next guess a using UNIV_witness[where 'a = 'n] ..
obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
@@ -2332,8 +2349,8 @@

lemma convex_on_bounded_continuous:
assumes "open s" "convex_on s f" "\<forall>x\<in>s. abs(f x) \<le> b"
-  shows "continuous_on s (vec1 o f)"
-  apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_vec1_range proof(rule,rule,rule)
+  shows "continuous_on s f"
+  apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof(rule,rule,rule)
fix x e assume "x\<in>s" "(0::real) < e"
def B \<equiv> "abs b + 1"
have B:"0 < B" "\<And>x. x\<in>s \<Longrightarrow> abs (f x) \<le> B"
@@ -2398,7 +2415,7 @@

lemma convex_on_continuous:
assumes "open (s::(real^'n::finite) set)" "convex_on s f"
-  shows "continuous_on s (vec1 \<circ> f)"
+  shows "continuous_on s f"
unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
note dimge1 = dimindex_ge_1[where 'a='n]
fix x assume "x\<in>s"
@@ -2428,9 +2445,9 @@
using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component)  }
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
by(auto simp add: vector_component_simps) qed
-  hence "continuous_on (ball x d) (vec1 \<circ> f)" apply(rule_tac convex_on_bounded_continuous)
+  hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
-  thus "continuous (at x) (vec1 \<circ> f)" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
+  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed

subsection {* Line segments, starlike sets etc.                                         *)
(* Use the same overloading tricks as for intervals, so that                 *)
@@ -2975,7 +2992,8 @@
unfolding pathfinish_def linepath_def by auto

lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
-  unfolding linepath_def by(auto simp add: vec1_dest_vec1 o_def intro!: continuous_intros)
+  unfolding linepath_def
+  by (intro continuous_intros continuous_dest_vec1)

lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on)
@@ -3202,9 +3220,9 @@
have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *s x) ` (UNIV - {0})" apply(rule set_ext,rule)
unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_mul by(auto intro!: ***)
-  have "continuous_on (UNIV - {0}) (vec1 \<circ> (\<lambda>x::real^'n. 1 / norm x))" unfolding o_def continuous_on_eq_continuous_within
+  have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
-    apply(rule continuous_at_vec1_norm[unfolded o_def]) by auto
+    apply(rule continuous_at_norm[unfolded o_def]) by auto
thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
```
```--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 16:13:18 2009 -0700
@@ -1245,6 +1245,9 @@
unfolding linear_conv_bounded_linear
by (rule bounded_linear.tendsto)

+lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
+  unfolding tendsto_def Limits.eventually_at_topological by fast
+
lemma Lim_const: "((\<lambda>x. a) ---> a) net"
by (rule tendsto_const)

@@ -1271,44 +1274,73 @@
shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
by (rule tendsto_diff)

+lemma dist_triangle3: (* TODO: move *)
+  fixes x y :: "'a::metric_space"
+  shows "dist x y \<le> dist a x + dist a y"
+using dist_triangle2 [of x y a]
+by (simp add: dist_commute)
+
+lemma tendsto_dist: (* TODO: move *)
+  assumes f: "(f ---> l) net" and g: "(g ---> m) net"
+  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  hence e2: "0 < e/2" by simp
+  from tendstoD [OF f e2] tendstoD [OF g e2]
+  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net"
+  proof (rule eventually_elim2)
+    fix x assume x: "dist (f x) l < e/2" "dist (g x) m < e/2"
+    have "dist (f x) (g x) - dist l m \<le> dist (f x) l + dist (g x) m"
+      using dist_triangle2 [of "f x" "g x" "l"]
+      using dist_triangle2 [of "g x" "l" "m"]
+      by arith
+    moreover
+    have "dist l m - dist (f x) (g x) \<le> dist (f x) l + dist (g x) m"
+      using dist_triangle3 [of "l" "m" "f x"]
+      using dist_triangle [of "f x" "m" "g x"]
+      by arith
+    ultimately
+    have "dist (dist (f x) (g x)) (dist l m) \<le> dist (f x) l + dist (g x) m"
+      unfolding dist_norm real_norm_def by arith
+    with x show "dist (dist (f x) (g x)) (dist l m) < e"
+      by arith
+  qed
+qed
+
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)

lemma Lim_null_norm:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
-  by (simp add: Lim dist_norm norm_vec1)
+  shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. norm(f x)) ---> 0) net"
+  by (simp add: Lim dist_norm)

lemma Lim_null_comparison:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
+  assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
shows "(f ---> 0) net"
proof(simp add: tendsto_iff, rule+)
fix e::real assume "0<e"
{ fix x
-    assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
-    hence "dist (f x) 0 < e"  unfolding vec_def using dist_vec1[of "g x" "0"]
-      by (vector dist_norm norm_vec1 real_vector_norm_def dot_def vec1_def)
+    assume "norm (f x) \<le> g x" "dist (g x) 0 < e"
+    hence "dist (f x) 0 < e" by (simp add: dist_norm)
}
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
-    using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
-    using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (vec1 (g x)) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
+    using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
+    using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
using assms `e>0` unfolding tendsto_iff by auto
qed

-lemma Lim_component: "(f ---> l) net
-                      ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)\$i)) ---> vec1(l\$i)) net"
+lemma Lim_component:
+  fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
+  shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a \$i) ---> l\$i) net"
unfolding tendsto_iff
-  apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
-  apply (auto simp del: vector_minus_component)
-  apply (erule_tac x=e in allE)
-  apply clarify
-  apply (erule eventually_rev_mono)
-  apply (auto simp del: vector_minus_component)
-  apply (rule order_le_less_trans)
-  apply (rule component_le_norm)
-  by auto
+  apply (clarify)
+  apply (drule spec, drule (1) mp)
+  apply (erule eventually_elim1)
+  apply (erule le_less_trans [OF dist_nth_le])
+  done

lemma Lim_transform_bound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -1504,12 +1536,6 @@
netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
"netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"

-lemma dist_triangle3:
-  fixes x y :: "'a::metric_space"
-  shows "dist x y \<le> dist a x + dist a y"
-using dist_triangle2 [of x y a]
-by (simp add: dist_commute)
-
lemma netlimit_within:
assumes "\<not> trivial_limit (at a within S)"
shows "netlimit (at a within S) = a"
@@ -1694,14 +1720,14 @@
apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
by metis arith

-lemma seq_harmonic: "((\<lambda>n. vec1(inverse (real n))) ---> 0) sequentially"
+lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
proof-
{ fix e::real assume "e>0"
hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
-      by (metis dlo_simps(4) le_imp_inverse_le linorder_not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
+      by (metis not_le le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
}
-  thus ?thesis unfolding Lim_sequentially dist_norm apply simp unfolding norm_vec1 by auto
+  thus ?thesis unfolding Lim_sequentially dist_norm by simp
qed

text{* More properties of closed balls. *}
@@ -2123,26 +2149,26 @@

text{* Some theorems on sups and infs using the notion "bounded". *}

-lemma bounded_vec1:
+lemma bounded_real:
fixes S :: "real set"
-  shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
-  by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1)
-
-lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
+  shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
+  by (simp add: bounded_iff)
+
+lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
proof
fix x assume "x\<in>S"
-  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_vec1 by auto
+  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
-  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_vec1] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
+  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
next
show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
-  apply (auto simp add: bounded_vec1)
+  apply (auto simp add: bounded_real)
by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
qed

-lemma rsup_insert: assumes "bounded (vec1 ` S)"
+lemma rsup_insert: assumes "bounded S"
shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
proof(cases "S={}")
case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
@@ -2168,17 +2194,17 @@
by simp

lemma bounded_has_rinf:
-  assumes "bounded(vec1 ` S)"  "S \<noteq> {}"
+  assumes "bounded S"  "S \<noteq> {}"
shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
proof
fix x assume "x\<in>S"
-  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_vec1 by auto
+  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
next
show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
-  apply (auto simp add: bounded_vec1)
+  apply (auto simp add: bounded_real)
by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
qed

@@ -2189,7 +2215,7 @@
apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
done

-lemma rinf_insert: assumes "bounded (vec1 ` S)"
+lemma rinf_insert: assumes "bounded S"
shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
proof(cases "S={}")
case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
@@ -4050,68 +4076,52 @@
subsection{* Topological stuff lifted from and dropped to R                            *}

-lemma open_vec1:
-  fixes s :: "real set" shows
- "open(vec1 ` s) \<longleftrightarrow>
-        (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
-  unfolding open_dist apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
-
-lemma islimpt_approachable_vec1:
+lemma open_real:
fixes s :: "real set" shows
- "(vec1 x) islimpt (vec1 ` s) \<longleftrightarrow>
-         (\<forall>e>0.  \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
-  by (auto simp add: islimpt_approachable dist_vec1 vec1_eq)
-
-lemma closed_vec1:
-  fixes s :: "real set" shows
- "closed (vec1 ` s) \<longleftrightarrow>
+ "open s \<longleftrightarrow>
+        (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
+  unfolding open_dist dist_norm by simp
+
+lemma islimpt_approachable_real:
+  fixes s :: "real set"
+  shows "x islimpt s \<longleftrightarrow> (\<forall>e>0.  \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
+  unfolding islimpt_approachable dist_norm by simp
+
+lemma closed_real:
+  fixes s :: "real set"
+  shows "closed s \<longleftrightarrow>
(\<forall>x. (\<forall>e>0.  \<exists>x' \<in> s. x' \<noteq> x \<and> abs(x' - x) < e)
--> x \<in> s)"
-  unfolding closed_limpt islimpt_approachable forall_vec1 apply simp
-  unfolding dist_vec1 vec1_in_image_vec1 abs_minus_commute by auto
-
-lemma continuous_at_vec1_range:
-  fixes f :: "real ^ _ \<Rightarrow> real"
-  shows "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
+  unfolding closed_limpt islimpt_approachable dist_norm by simp
+
+lemma continuous_at_real_range:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real"
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
\<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
-  unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
+  unfolding continuous_at unfolding Lim_at
+  unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
apply(erule_tac x=e in allE) by auto

-lemma continuous_on_vec1_range:
+lemma continuous_on_real_range:
fixes f :: "'a::real_normed_vector \<Rightarrow> real"
-  shows "continuous_on s (vec1 o f) \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
-  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
-
-lemma continuous_at_vec1_norm:
-  fixes x :: "real ^ _"
-  shows "continuous (at x) (vec1 o norm)"
-  unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast
-
-lemma continuous_on_vec1_norm:
-  fixes s :: "(real ^ _) set"
-  shows "continuous_on s (vec1 o norm)"
-unfolding continuous_on_vec1_range norm_vec1[THEN sym] by (metis norm_vec1 order_le_less_trans real_abs_sub_norm)
-
-lemma continuous_at_vec1_component:
-  shows "continuous (at (a::real^'a::finite)) (\<lambda> x. vec1(x\$i))"
-proof-
-  { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
-    hence "\<bar>x \$ i - a \$ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
-  thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto
-qed
-
-lemma continuous_on_vec1_component:
-  shows "continuous_on s (\<lambda> x::real^'a::finite. vec1(x\$i))"
-proof-
-  { fix e::real and x xa assume "x\<in>s" "e>0" "xa\<in>s" "0 < norm (xa - x) \<and> norm (xa - x) < e"
-    hence "\<bar>xa \$ i - x \$ i\<bar> < e" using component_le_norm[of "xa - x" i] by auto  }
-  thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_norm by auto
-qed
-
-lemma continuous_at_vec1_infnorm:
- "continuous (at x) (vec1 o infnorm)"
-  unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_norm
+  shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
+  unfolding continuous_on_def dist_norm by simp
+
+lemma continuous_at_norm: "continuous (at x) norm"
+  unfolding continuous_at by (intro tendsto_norm Lim_ident_at)
+
+lemma continuous_on_norm: "continuous_on s norm"
+unfolding continuous_on by (intro ballI tendsto_norm Lim_at_within Lim_ident_at)
+
+lemma continuous_at_component: "continuous (at a) (\<lambda>x. x \$ i)"
+unfolding continuous_at by (intro Lim_component Lim_ident_at)
+
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x \$ i)"
+unfolding continuous_on by (intro ballI Lim_component Lim_at_within Lim_ident_at)
+
+lemma continuous_at_infnorm: "continuous (at x) infnorm"
+  unfolding continuous_at Lim_at o_def unfolding dist_norm
apply auto apply (rule_tac x=e in exI) apply auto
using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))

@@ -4119,23 +4129,23 @@

lemma compact_attains_sup:
fixes s :: "real set"
-  assumes "compact (vec1 ` s)"  "s \<noteq> {}"
+  assumes "compact s"  "s \<noteq> {}"
shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
proof-
-  from assms(1) have a:"bounded (vec1 ` s)" "closed (vec1 ` s)" unfolding compact_eq_bounded_closed by auto
+  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
{ fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_vec1, THEN spec[where x="rsup s"]]
+  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
apply(rule_tac x="rsup s" in bexI) by auto
qed

lemma compact_attains_inf:
fixes s :: "real set"
-  assumes "compact (vec1 ` s)" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
+  assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
proof-
-  from assms(1) have a:"bounded (vec1 ` s)" "closed (vec1 ` s)" unfolding compact_eq_bounded_closed by auto
+  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
{ fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s"  "rinf s \<notin> s"  "0 < e"
"\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
@@ -4145,43 +4155,40 @@
have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_vec1, THEN spec[where x="rinf s"]]
+  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
apply(rule_tac x="rinf s" in bexI) by auto
qed

lemma continuous_attains_sup:
fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s (vec1 o f)
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
==> (\<exists>x \<in> s. \<forall>y \<in> s.  f y \<le> f x)"
using compact_attains_sup[of "f ` s"]
-  using compact_continuous_image[of s "vec1 \<circ> f"] unfolding image_compose by auto
+  using compact_continuous_image[of s f] by auto

lemma continuous_attains_inf:
fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s (vec1 o f)
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
\<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
using compact_attains_inf[of "f ` s"]
-  using compact_continuous_image[of s "vec1 \<circ> f"] unfolding image_compose by auto
+  using compact_continuous_image[of s f] by auto

lemma distance_attains_sup:
-  fixes s :: "(real ^ _) set"
assumes "compact s" "s \<noteq> {}"
shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x"
-proof-
-  { fix x assume "x\<in>s" fix e::real assume "e>0"
-    { fix x' assume "x'\<in>s" and as:"norm (x' - x) < e"
-      hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
-	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
-    hence "\<exists>d>0. \<forall>x'\<in>s. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
-  thus ?thesis using assms
-    using continuous_attains_sup[of s "\<lambda>x. dist a x"]
-    unfolding continuous_on_vec1_range by (auto simp add: dist_commute)
+proof (rule continuous_attains_sup [OF assms])
+  { fix x assume "x\<in>s"
+    have "(dist a ---> dist a x) (at x within s)"
+      by (intro tendsto_dist tendsto_const Lim_at_within Lim_ident_at)
+  }
+  thus "continuous_on s (dist a)"
+    unfolding continuous_on ..
qed

text{* For *minimal* distance, we only need closure, not compactness.            *}

lemma distance_attains_inf:
-  fixes a :: "real ^ _" (* FIXME: generalize *)
+  fixes a :: "'a::heine_borel"
assumes "closed s"  "s \<noteq> {}"
shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a x \<le> dist a y"
proof-
@@ -4192,14 +4199,25 @@
moreover
{ fix x assume "x\<in>?B"
fix e::real assume "e>0"
-    { fix x' assume "x'\<in>?B" and as:"norm (x' - x) < e"
-      hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
-	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
-    hence "\<exists>d>0. \<forall>x'\<in>?B. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
-  hence "continuous_on (cball a (dist b a) \<inter> s) (vec1 \<circ> dist a)" unfolding continuous_on_vec1_range
-    by (auto  simp add: dist_commute)
-  moreover have "compact ?B" using compact_cball[of a "dist b a"] unfolding compact_eq_bounded_closed using bounded_Int and closed_Int and assms(1) by auto
-  ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y" using continuous_attains_inf[of ?B "dist a"] by fastsimp
+    { fix x' assume "x'\<in>?B" and as:"dist x' x < e"
+      from as have "\<bar>dist a x' - dist a x\<bar> < e"
+        unfolding abs_less_iff minus_diff_eq
+        using dist_triangle2 [of a x' x]
+        using dist_triangle [of a x x']
+        by arith
+    }
+    hence "\<exists>d>0. \<forall>x'\<in>?B. dist x' x < d \<longrightarrow> \<bar>dist a x' - dist a x\<bar> < e"
+      using `e>0` by auto
+  }
+  hence "continuous_on (cball a (dist b a) \<inter> s) (dist a)"
+    unfolding continuous_on Lim_within dist_norm real_norm_def
+    by fast
+  moreover have "compact ?B"
+    using compact_cball[of a "dist b a"]
+    unfolding compact_eq_bounded_closed
+    using bounded_Int and closed_Int and assms(1) by auto
+  ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y"
+    using continuous_attains_inf[of ?B "dist a"] by fastsimp
thus ?thesis by fastsimp
qed

@@ -4207,39 +4225,34 @@

lemma Lim_mul:
fixes f :: "'a \<Rightarrow> real ^ _"
-  assumes "((vec1 o c) ---> vec1 d) net"  "(f ---> l) net"
+  assumes "(c ---> d) net"  "(f ---> l) net"
shows "((\<lambda>x. c(x) *s f x) ---> (d *s l)) net"
-proof-
-  have "bilinear (\<lambda>x. op *s (dest_vec1 (x::real^1)))" unfolding bilinear_def linear_def
-    unfolding dest_vec1_add dest_vec1_cmul
-    apply vector apply auto unfolding semiring_class.right_distrib semiring_class.left_distrib by auto
-  thus ?thesis using Lim_bilinear[OF assms, of "\<lambda>x y. (dest_vec1 x) *s y"] by auto
-qed
+  unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto)

lemma Lim_vmul:
fixes c :: "'a \<Rightarrow> real"
-  shows "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
+  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
using Lim_mul[of c d net "\<lambda>x. v" v] using Lim_const[of v] by auto

lemma continuous_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
+  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *s v)"
unfolding continuous_def using Lim_vmul[of c] by auto

lemma continuous_mul:
fixes c :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net (vec1 o c) \<Longrightarrow> continuous net f
+  shows "continuous net c \<Longrightarrow> continuous net f
==> continuous net (\<lambda>x. c(x) *s f x) "
unfolding continuous_def using Lim_mul[of c] by auto

lemma continuous_on_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous_on s (vec1 o c) ==> continuous_on s (\<lambda>x. c(x) *s v)"
+  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *s v)"
unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto

lemma continuous_on_mul:
fixes c :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous_on s (vec1 o c) \<Longrightarrow> continuous_on s f
+  shows "continuous_on s c \<Longrightarrow> continuous_on s f
==> continuous_on s (\<lambda>x. c(x) *s f x)"
unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto

@@ -4247,59 +4260,27 @@

lemma Lim_inv:
fixes f :: "'a \<Rightarrow> real"
-  assumes "((vec1 o f) ---> vec1 l) (net::'a net)"  "l \<noteq> 0"
-  shows "((vec1 o inverse o f) ---> vec1(inverse l)) net"
-proof -
-  { fix e::real assume "e>0"
-    let ?d = "min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)"
-    have "0 < ?d" using `l\<noteq>0` `e>0` mult_pos_pos[of "l^2" "e/2"] by auto
-    with assms(1) have "eventually (\<lambda>x. dist ((vec1 o f) x) (vec1 l) < ?d) net"
-      by (rule tendstoD)
-    moreover
-    { fix x assume "dist ((vec1 o f) x) (vec1 l) < ?d"
-      hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" unfolding o_def dist_vec1 by auto
-      hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
-      hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
-      from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
-      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
-      hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar>  \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
-      hence "\<bar>f x * l\<bar> * 2  \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
-      hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
-	using le_imp_inverse_le[of "l^2 / 2" "\<bar>f x * l\<bar>"]  by auto
-
-      have "dist ((vec1 \<circ> inverse \<circ> f) x) (vec1 (inverse l)) < e" unfolding o_def unfolding dist_vec1
-	unfolding inverse_diff_inverse[OF fx0 `l\<noteq>0`] apply simp
-	unfolding mult_commute[of "inverse (f x)"]
-	unfolding real_divide_def[THEN sym]
-	unfolding divide_divide_eq_left
-	unfolding nonzero_abs_divide[OF fxl0]
-	using mult_less_le_imp_less[OF **, of "inverse \<bar>f x * l\<bar>", of "inverse (l^2 / 2)"] using *** using fx0 `l\<noteq>0`
-	unfolding inverse_eq_divide using `e>0` by auto
-    }
-    ultimately
-    have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
-      by (auto elim: eventually_rev_mono)
-  }
-  thus ?thesis unfolding tendsto_iff by auto
-qed
+  assumes "(f ---> l) (net::'a net)"  "l \<noteq> 0"
+  shows "((inverse o f) ---> inverse l) net"
+  unfolding o_def using assms by (rule tendsto_inverse)

lemma continuous_inv:
fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
-           ==> continuous net (vec1 o inverse o f)"
+  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
+           ==> continuous net (inverse o f)"
unfolding continuous_def using Lim_inv by auto

lemma continuous_at_within_inv:
fixes f :: "real ^ _ \<Rightarrow> real"
-  assumes "continuous (at a within s) (vec1 o f)" "f a \<noteq> 0"
-  shows "continuous (at a within s) (vec1 o inverse o f)"
+  assumes "continuous (at a within s) f" "f a \<noteq> 0"
+  shows "continuous (at a within s) (inverse o f)"
using assms unfolding continuous_within o_apply
by (rule Lim_inv)

lemma continuous_at_inv:
fixes f :: "real ^ _ \<Rightarrow> real"
-  shows "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
-         ==> continuous (at a) (vec1 o inverse o f) "
+  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
+         ==> continuous (at a) (inverse o f) "
using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto

subsection{* Preservation properties for pasted sets.                                  *}
@@ -4407,14 +4388,14 @@
text{* Hence we get the following.                                               *}

lemma compact_sup_maxdistance:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "(real ^ 'n::finite) set"
assumes "compact s"  "s \<noteq> {}"
shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. norm(u - v) \<le> norm(x - y)"
proof-
have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}"  "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
using compact_differences[OF assms(1) assms(1)]
-    using distance_attains_sup[unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
+    using distance_attains_sup[where 'a="real ^ 'n", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
thus ?thesis using x(2)[unfolded `x = a - b`] by blast
qed
@@ -4965,8 +4946,8 @@
then obtain N::nat where "inverse (real (N + 1)) < e" by auto
hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto  }
-      hence "((vec1 \<circ> (\<lambda>n. inverse (real n + 1))) ---> vec1 0) sequentially"
-	unfolding Lim_sequentially by(auto simp add: dist_vec1)
+      hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
+	unfolding Lim_sequentially by(auto simp add: dist_norm)
hence "(f ---> x) sequentially" unfolding f_def
using Lim_add[OF Lim_const, of "\<lambda>n::nat. (inverse (real n + 1)) *s ((1 / 2) *s (a + b) - x)" 0 sequentially x]
using Lim_vmul[of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *s (a + b) - x)"] by auto  }```