# HG changeset patch
# User huffman
# Date 1272309597 25200
# Node ID 3407550278407d9a61ee31cd19c2507df4ac663c
# Parent  49c7dee21a7f3344b28446452a2cee9bbb3f548a
move definitions and theorems for type real^1 to separate theory file

diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -19,7 +19,7 @@
 header {* Results connected with topological dimension. *}
 
 theory Brouwer_Fixpoint
-  imports Convex_Euclidean_Space
+  imports Convex_Euclidean_Space Vec1
 begin
 
 lemma brouwer_compactness_lemma:
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -15,17 +15,11 @@
 
 declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
 declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
-declare UNIV_1[simp]
 
 (*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
 
 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component
 
-lemma dest_vec1_simps[simp]: fixes a::"real^1"
-  shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
-  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
-  by(auto simp add: vector_le_def Cart_eq)
-
 lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
 
 lemma setsum_delta_notmem: assumes "x\<notin>s"
@@ -47,31 +41,10 @@
 
 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto
 
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
   (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   using image_affinity_interval[of m 0 a b] by auto
 
-lemma dest_vec1_inverval:
-  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
-  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
-  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
-  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
-  apply(rule_tac [!] equalityI)
-  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
-  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
-  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
-  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
-  by (auto simp add: vector_less_def vector_le_def)
-
-lemma dest_vec1_setsum: assumes "finite S"
-  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
-  using dest_vec1_sum[OF assms] by auto
-
 lemma dist_triangle_eq:
   fixes x y z :: "real ^ _"
   shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
@@ -359,9 +332,6 @@
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
 
-lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
-  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
-
 lemma convex_empty[intro]: "convex {}"
   unfolding convex_def by simp
 
@@ -1292,29 +1262,14 @@
   qed
 qed
 
-lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
-unfolding open_vector_def forall_1 by auto
-
-lemma tendsto_dest_vec1 [tendsto_intros]:
-  "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
-by(rule tendsto_Cart_nth)
-
-lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
-  unfolding continuous_def by (rule tendsto_dest_vec1)
-
 (* TODO: move *)
 lemma compact_real_interval:
   fixes a b :: real shows "compact {a..b}"
-proof -
-  have "continuous_on {vec1 a .. vec1 b} dest_vec1"
-    unfolding continuous_on
-    by (simp add: tendsto_dest_vec1 Lim_at_within Lim_ident_at)
-  moreover have "compact {vec1 a .. vec1 b}" by (rule compact_interval)
-  ultimately have "compact (dest_vec1 ` {vec1 a .. vec1 b})"
-    by (rule compact_continuous_image)
-  also have "dest_vec1 ` {vec1 a .. vec1 b} = {a..b}"
-    by (auto simp add: image_def Bex_def exists_vec1)
-  finally show ?thesis .
+proof (rule bounded_closed_imp_compact)
+  have "\<forall>y\<in>{a..b}. dist a y \<le> dist a b"
+    unfolding dist_real_def by auto
+  thus "bounded {a..b}" unfolding bounded_def by fast
+  show "closed {a..b}" by (rule closed_real_atLeastAtMost)
 qed
 
 lemma compact_convex_combinations:
@@ -2015,13 +1970,11 @@
 proof-
   obtain b where b:"b>0" "\<forall>x\<in>s. norm x \<le> b" using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
   let ?A = "{y. \<exists>u. 0 \<le> u \<and> u \<le> b / norm(x) \<and> (y = u *\<^sub>R x)}"
-  have A:"?A = (\<lambda>u. dest_vec1 u *\<^sub>R x) ` {0 .. vec1 (b / norm x)}"
-    unfolding image_image[of "\<lambda>u. u *\<^sub>R x" "\<lambda>x. dest_vec1 x", THEN sym]
-    unfolding dest_vec1_inverval vec1_dest_vec1 by auto
+  have A:"?A = (\<lambda>u. u *\<^sub>R x) ` {0 .. b / norm x}"
+    by auto
   have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
     apply(rule, rule continuous_vmul)
-    apply (rule continuous_dest_vec1)
-    apply(rule continuous_at_id) by(rule compact_interval)
+    apply(rule continuous_at_id) by(rule compact_real_interval)
   moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R 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 *\<^sub>R x"
@@ -2232,10 +2185,6 @@
 
 lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
 
-(** move this**)
-lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" 
-  apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
-
 (** This might break sooner or later. In fact it did already once. **)
 lemma convex_epigraph: 
   "convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
@@ -2264,16 +2213,11 @@
   "(\<forall>p. P (fstcart p) (sndcart p)) \<longleftrightarrow> (\<forall>x y. P x y)" apply meson
   apply(erule_tac x="pastecart x y" in allE) unfolding o_def by auto
 
-lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
-  apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto 
-
-lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
-  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
-
+(* TODO: move *)
 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
 by (cases "finite A", induct set: finite, simp_all)
 
+(* TODO: move *)
 lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
 by (cases "finite A", induct set: finite, simp_all)
 
@@ -2322,6 +2266,7 @@
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n}"
   apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
+(* FIXME: rewrite these lemmas without using vec1
 subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
 
 lemma is_interval_1:
@@ -2350,33 +2295,33 @@
 lemma convex_connected_1:
   "connected s \<longleftrightarrow> convex (s::(real^1) set)" 
 by(metis is_interval_convex convex_connected is_interval_connected_1)
-
+*)
 subsection {* Another intermediate value theorem formulation. *}
 
-lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
+lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+  assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
 proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI) 
     using assms(1) by(auto simp add: vector_le_def)
   thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
-    using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
+    using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
     using assms by(auto intro!: imageI) qed
 
-lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
    \<Longrightarrow> f a$k \<le> y \<Longrightarrow> y \<le> f b$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
 by(rule ivt_increasing_component_on_1)
   (auto simp add: continuous_at_imp_continuous_on)
 
-lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
+lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+  assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
   apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
   apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
   by auto
 
-lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
     \<Longrightarrow> f b$k \<le> y \<Longrightarrow> y \<le> f a$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
 by(rule ivt_decreasing_component_on_1)
   (auto simp: continuous_at_imp_continuous_on)
@@ -3037,7 +2982,7 @@
 lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)"
   using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+
   apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
-  unfolding mem_interval_1 by auto
+  by auto
 
 lemma simple_path_join_loop:
   assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
@@ -3050,36 +2995,36 @@
     assume as:"x \<le> 1 / 2" "y \<le> 1 / 2"
     hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto
     moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
-      unfolding mem_interval_1 by auto
+      by auto
     ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
   next assume as:"x > 1 / 2" "y > 1 / 2"
     hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto
-    moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by auto
+    moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as by auto
     ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
   next assume as:"x \<le> 1 / 2" "y > 1 / 2"
     hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     moreover have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def
-      using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)[unfolded mem_interval_1]
+      using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)
       by (auto simp add: field_simps)
     ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)[unfolded mem_interval_1]
+    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
       using inj(1)[of "2 *\<^sub>R x" 0] by auto
     moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
-      unfolding joinpaths_def pathfinish_def using as(2) and xy(2)[unfolded mem_interval_1]
+      unfolding joinpaths_def pathfinish_def using as(2) and xy(2)
       using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto
     ultimately show ?thesis by auto
   next assume as:"x > 1 / 2" "y \<le> 1 / 2"
     hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     moreover have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def
-      using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)[unfolded mem_interval_1]
+      using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)
       by (auto simp add: field_simps)
     ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)[unfolded mem_interval_1]
+    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
       using inj(1)[of "2 *\<^sub>R y" 0] by auto
     moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
-      unfolding joinpaths_def pathfinish_def using as(1) and xy(1)[unfolded mem_interval_1]
+      unfolding joinpaths_def pathfinish_def using as(1) and xy(1)
       using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto
     ultimately show ?thesis by auto qed qed
 
@@ -3092,22 +3037,22 @@
   fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
   show "x = y" proof(cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
     assume "x \<le> 1 / 2" "y \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
-      unfolding mem_interval_1 joinpaths_def by auto
+      unfolding joinpaths_def by auto
   next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
-      unfolding mem_interval_1 joinpaths_def by auto
+      unfolding joinpaths_def by auto
   next assume as:"x \<le> 1 / 2" "y > 1 / 2" 
     hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto
     thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
-      unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+      unfolding pathstart_def pathfinish_def joinpaths_def
       by auto
   next assume as:"x > 1 / 2" "y \<le> 1 / 2" 
     hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto
     thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
-      unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+      unfolding pathstart_def pathfinish_def joinpaths_def
       by auto qed qed
 
 lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
@@ -3178,8 +3123,7 @@
   unfolding pathfinish_def linepath_def by auto
 
 lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
-  unfolding linepath_def
-  by (intro continuous_intros continuous_dest_vec1)
+  unfolding linepath_def by (intro continuous_intros)
 
 lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
   using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on)
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -763,6 +763,9 @@
   have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
   show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
 
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
 lemma differentiable_bound_real: fixes f::"real \<Rightarrow> real"
   assumes "convex s" "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
   shows "norm(f x - f y) \<le> B * norm(x - y)" 
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -5,7 +5,7 @@
 header {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
-imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations Vec1
 begin
 
 subsection{* First some facts about products*}
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -12,56 +12,6 @@
 uses "positivstellensatz.ML" ("normarith.ML")
 begin
 
-text{* Some common special cases.*}
-
-lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
-  by (metis num1_eq_iff)
-
-lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
-  by auto (metis num1_eq_iff)
-
-lemma exhaust_2:
-  fixes x :: 2 shows "x = 1 \<or> x = 2"
-proof (induct x)
-  case (of_int z)
-  then have "0 <= z" and "z < 2" by simp_all
-  then have "z = 0 | z = 1" by arith
-  then show ?case by auto
-qed
-
-lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
-  by (metis exhaust_2)
-
-lemma exhaust_3:
-  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
-proof (induct x)
-  case (of_int z)
-  then have "0 <= z" and "z < 3" by simp_all
-  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
-  then show ?case by auto
-qed
-
-lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
-  by (metis exhaust_3)
-
-lemma UNIV_1: "UNIV = {1::1}"
-  by (auto simp add: num1_eq_iff)
-
-lemma UNIV_2: "UNIV = {1::2, 2::2}"
-  using exhaust_2 by auto
-
-lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
-  using exhaust_3 by auto
-
-lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
-  unfolding UNIV_1 by simp
-
-lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
-  unfolding UNIV_2 by simp
-
-lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
-  unfolding UNIV_3 by (simp add: add_ac)
-
 subsection{* Basic componentwise operations on vectors. *}
 
 instantiation cart :: (plus,finite) plus
@@ -114,7 +64,7 @@
   instance by (intro_classes)
 end
 
-text{* The ordering on @{typ "real^1"} is linear. *}
+text{* The ordering on one-dimensional vectors is linear. *}
 
 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin
@@ -123,11 +73,6 @@
       by (auto intro!: card_ge_0_finite) qed
 end
 
-instantiation num1 :: cart_one begin
-instance proof
-  show "CARD(1) = Suc 0" by auto
-qed end
-
 instantiation cart :: (linorder,cart_one) linorder begin
 instance proof
   guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
@@ -667,26 +612,6 @@
   show ?case by (simp add: h)
 qed
 
-subsection{* The collapse of the general concepts to dimension one. *}
-
-lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
-  by (simp add: Cart_eq)
-
-lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
-  apply auto
-  apply (erule_tac x= "x$1" in allE)
-  apply (simp only: vector_one[symmetric])
-  done
-
-lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
-  by (simp add: norm_vector_def UNIV_1)
-
-lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
-  by (simp add: norm_vector_1)
-
-lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
-  by (auto simp add: norm_real dist_norm)
-
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
 lemma connected_real_lemma:
@@ -747,7 +672,7 @@
     ultimately show ?thesis using alb by metis
 qed
 
-text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *}
+text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
 
 lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
 proof-
@@ -1364,67 +1289,6 @@
 lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
   by (simp add: orthogonal_def inner_commute)
 
-subsection{* Explicit vector construction from lists. *}
-
-primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
-where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
-
-lemma from_nat [simp]: "from_nat = of_nat"
-by (rule ext, induct_tac x, simp_all)
-
-primrec
-  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
-where
-  "list_fun n [] = (\<lambda>x. 0)"
-| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
-
-definition "vector l = (\<chi> i. list_fun 1 l i)"
-(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
-
-lemma vector_1: "(vector[x]) $1 = x"
-  unfolding vector_def by simp
-
-lemma vector_2:
- "(vector[x,y]) $1 = x"
- "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
-  unfolding vector_def by simp_all
-
-lemma vector_3:
- "(vector [x,y,z] ::('a::zero)^3)$1 = x"
- "(vector [x,y,z] ::('a::zero)^3)$2 = y"
- "(vector [x,y,z] ::('a::zero)^3)$3 = z"
-  unfolding vector_def by simp_all
-
-lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (subgoal_tac "vector [v$1] = v")
-  apply simp
-  apply (vector vector_def)
-  apply simp
-  done
-
-lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (subgoal_tac "vector [v$1, v$2] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_2)
-  done
-
-lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (erule_tac x="v$3" in allE)
-  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_3)
-  done
-
 subsection{* Linear functions. *}
 
 definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"
@@ -2216,33 +2080,6 @@
   apply (rule onorm_triangle)
   by assumption+
 
-(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
-
-abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
-
-abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
-  where "dest_vec1 x \<equiv> (x$1)"
-
-lemma vec1_component[simp]: "(vec1 x)$1 = x"
-  by simp
-
-lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
-  by (simp_all add:  Cart_eq)
-
-declare vec1_dest_vec1(1) [simp]
-
-lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
-  by (metis vec1_dest_vec1(1))
-
-lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
-  by (metis vec1_dest_vec1(1))
-
-lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(2))
-
-lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(1))
-
 lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
 
 lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
@@ -2250,9 +2087,6 @@
 lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def)
 lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
 
-lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
-  apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
 lemma vec_setsum: assumes fS: "finite S"
   shows "vec(setsum f S) = setsum (vec o f) S"
   apply (induct rule: finite_induct[OF fS])
@@ -2260,70 +2094,6 @@
   apply (auto simp add: vec_add)
   done
 
-lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
-  by (simp)
-
-lemma dest_vec1_vec: "dest_vec1(vec x) = x"
-  by (simp)
-
-lemma dest_vec1_sum: assumes fS: "finite S"
-  shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
-  apply (induct rule: finite_induct[OF fS])
-  apply simp
-  apply auto
-  done
-
-lemma norm_vec1: "norm(vec1 x) = abs(x)"
-  by (simp add: vec_def norm_real)
-
-lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
-  by (simp only: dist_real vec1_component)
-lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
-  by (metis vec1_dest_vec1(1) norm_vec1)
-
-lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
-   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
-
-lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
-  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
-  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
-  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
-
-lemma linear_vmul_dest_vec1:
-  fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
-  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
-  apply (rule linear_vmul_component)
-  by auto
-
-lemma linear_from_scalars:
-  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
-  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
-  apply (rule ext)
-  apply (subst matrix_works[OF lf, symmetric])
-  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def  mult_commute UNIV_1)
-  done
-
-lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
-  shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
-  apply (rule ext)
-  apply (subst matrix_works[OF lf, symmetric])
-  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
-  done
-
-lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
-  by (simp add: dest_vec1_eq[symmetric])
-
-lemma setsum_scalars: assumes fS: "finite S"
-  shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
-  unfolding vec_setsum[OF fS] by simp
-
-lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
-  apply (cases "dest_vec1 x \<le> dest_vec1 y")
-  apply simp
-  apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
-  apply (auto)
-  done
-
 text{* Pasting vectors. *}
 
 lemma linear_fstcart[intro]: "linear fstcart"
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 11:08:49 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -3204,22 +3204,6 @@
                            --> dist (f x') (f x) < e)"
 
 
-text{* Lifting and dropping *}
-
-lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
-  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
-  using assms unfolding continuous_on_iff apply safe
-  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
-  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
-  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
-
-lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
-  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
-  using assms unfolding continuous_on_iff apply safe
-  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
-  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
-  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
-
 text{* Some simple consequential lemmas. *}
 
 lemma uniformly_continuous_imp_continuous:
@@ -4098,9 +4082,6 @@
   shows "bounded_linear f ==> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
-lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
-  by(rule linear_continuous_on[OF bounded_linear_vec1])
-
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
@@ -4722,20 +4703,6 @@
   "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
   using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
 
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
-lemma vec1_interval:fixes a::"real" shows
-  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
-  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
-  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
-  unfolding forall_1 unfolding vec1_dest_vec1_simps
-  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
-  apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
-
 lemma interval_eq_empty: fixes a :: "real^'n" shows
  "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
  "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
@@ -4918,10 +4885,7 @@
 qed
 
 lemma open_interval_real[intro]: fixes a :: "real" shows "open {a<..<b}"
-  using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
-  apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
-  unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
-  by(auto simp add: dist_vec1 dist_real_def vector_less_def)
+  by (rule open_real_greaterThanLessThan)
 
 lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
 proof-
@@ -5112,56 +5076,6 @@
   unfolding closure_open_interval[OF assms, THEN sym] unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
 
-(* Some special cases for intervals in R^1.                                  *)
-
-lemma interval_cases_1: fixes x :: "real^1" shows
- "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
-  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma in_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
-  (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma interval_eq_empty_1: fixes a :: "real^1" shows
-  "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
-  "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
-  unfolding interval_eq_empty and ex_1 by auto
-
-lemma subset_interval_1: fixes a :: "real^1" shows
- "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
-                dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
- "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
-  unfolding subset_interval[of a b c d] unfolding forall_1 by auto
-
-lemma eq_interval_1: fixes a :: "real^1" shows
- "{a .. b} = {c .. d} \<longleftrightarrow>
-          dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
-          dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
-unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
-unfolding subset_interval_1(1)[of a b c d]
-unfolding subset_interval_1(1)[of c d a b]
-by auto
-
-lemma disjoint_interval_1: fixes a :: "real^1" shows
-  "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
-  "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  unfolding disjoint_interval and ex_1 by auto
-
-lemma open_closed_interval_1: fixes a :: "real^1" shows
- "{a<..<b} = {a .. b} - {a, b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
-lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
 (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
 
 lemma closed_interval_left: fixes b::"real^'n"
@@ -5295,14 +5209,6 @@
   shows "l$i = b"
   using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
 
-lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
-  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
-  using Lim_component_le[of f l net 1 b] by auto
-
-lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
- "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
-  using Lim_component_ge[of f l net b 1] by auto
-
 text{* Limits relative to a union.                                               *}
 
 lemma eventually_within_Un:
@@ -5359,22 +5265,6 @@
  "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s.  z$k = a)"
   using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
 
-text{* Also more convenient formulations of monotone convergence.                *}
-
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
-  assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
-  shows "\<exists>l. (s ---> l) sequentially"
-proof-
-  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
-  { fix m::nat
-    have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
-      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
-  hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
-  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
-  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
-    unfolding dist_norm unfolding abs_dest_vec1  by auto
-qed
-
 subsection{* Basic homeomorphism definitions.                                          *}
 
 definition "homeomorphism s t f g \<equiv>
diff -r 49c7dee21a7f -r 340755027840 src/HOL/Multivariate_Analysis/Vec1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy	Mon Apr 26 12:19:57 2010 -0700
@@ -0,0 +1,389 @@
+(*  Title:      Multivariate_Analysis/Vec1.thy
+    Author:     Amine Chaieb, University of Cambridge
+    Author:     Robert Himmelmann, TU Muenchen
+*)
+
+header {* Vectors of size 1, 2, or 3 *}
+
+theory Vec1
+imports Topology_Euclidean_Space
+begin
+
+text{* Some common special cases.*}
+
+lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
+  by (metis num1_eq_iff)
+
+lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
+  by auto (metis num1_eq_iff)
+
+lemma exhaust_2:
+  fixes x :: 2 shows "x = 1 \<or> x = 2"
+proof (induct x)
+  case (of_int z)
+  then have "0 <= z" and "z < 2" by simp_all
+  then have "z = 0 | z = 1" by arith
+  then show ?case by auto
+qed
+
+lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
+  by (metis exhaust_2)
+
+lemma exhaust_3:
+  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
+proof (induct x)
+  case (of_int z)
+  then have "0 <= z" and "z < 3" by simp_all
+  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+  then show ?case by auto
+qed
+
+lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
+  by (metis exhaust_3)
+
+lemma UNIV_1 [simp]: "UNIV = {1::1}"
+  by (auto simp add: num1_eq_iff)
+
+lemma UNIV_2: "UNIV = {1::2, 2::2}"
+  using exhaust_2 by auto
+
+lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
+  using exhaust_3 by auto
+
+lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
+  unfolding UNIV_1 by simp
+
+lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
+  unfolding UNIV_2 by simp
+
+lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
+  unfolding UNIV_3 by (simp add: add_ac)
+
+instantiation num1 :: cart_one begin
+instance proof
+  show "CARD(1) = Suc 0" by auto
+qed end
+
+(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
+
+abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
+
+abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
+  where "dest_vec1 x \<equiv> (x$1)"
+
+lemma vec1_component[simp]: "(vec1 x)$1 = x"
+  by simp
+
+lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
+  by (simp_all add:  Cart_eq)
+
+declare vec1_dest_vec1(1) [simp]
+
+lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
+  by (metis vec1_dest_vec1(1))
+
+lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
+  by (metis vec1_dest_vec1(1))
+
+lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
+  by (metis vec1_dest_vec1(2))
+
+lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
+  by (metis vec1_dest_vec1(1))
+
+subsection{* The collapse of the general concepts to dimension one. *}
+
+lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
+  by (simp add: Cart_eq)
+
+lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
+  apply auto
+  apply (erule_tac x= "x$1" in allE)
+  apply (simp only: vector_one[symmetric])
+  done
+
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+  by (simp add: norm_vector_def)
+
+lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
+  by (simp add: norm_vector_1)
+
+lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
+  by (auto simp add: norm_real dist_norm)
+
+subsection{* Explicit vector construction from lists. *}
+
+primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
+where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
+
+lemma from_nat [simp]: "from_nat = of_nat"
+by (rule ext, induct_tac x, simp_all)
+
+primrec
+  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
+where
+  "list_fun n [] = (\<lambda>x. 0)"
+| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
+
+definition "vector l = (\<chi> i. list_fun 1 l i)"
+(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
+
+lemma vector_1: "(vector[x]) $1 = x"
+  unfolding vector_def by simp
+
+lemma vector_2:
+ "(vector[x,y]) $1 = x"
+ "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
+  unfolding vector_def by simp_all
+
+lemma vector_3:
+ "(vector [x,y,z] ::('a::zero)^3)$1 = x"
+ "(vector [x,y,z] ::('a::zero)^3)$2 = y"
+ "(vector [x,y,z] ::('a::zero)^3)$3 = z"
+  unfolding vector_def by simp_all
+
+lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (subgoal_tac "vector [v$1] = v")
+  apply simp
+  apply (vector vector_def)
+  apply simp
+  done
+
+lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (erule_tac x="v$2" in allE)
+  apply (subgoal_tac "vector [v$1, v$2] = v")
+  apply simp
+  apply (vector vector_def)
+  apply (simp add: forall_2)
+  done
+
+lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (erule_tac x="v$2" in allE)
+  apply (erule_tac x="v$3" in allE)
+  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
+  apply simp
+  apply (vector vector_def)
+  apply (simp add: forall_3)
+  done
+
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
+  by (simp)
+
+lemma dest_vec1_vec: "dest_vec1(vec x) = x"
+  by (simp)
+
+lemma dest_vec1_sum: assumes fS: "finite S"
+  shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
+  apply (induct rule: finite_induct[OF fS])
+  apply simp
+  apply auto
+  done
+
+lemma norm_vec1: "norm(vec1 x) = abs(x)"
+  by (simp add: vec_def norm_real)
+
+lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
+  by (simp only: dist_real vec1_component)
+lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
+  by (metis vec1_dest_vec1(1) norm_vec1)
+
+lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
+   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+
+lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
+  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
+  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
+  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
+
+lemma linear_vmul_dest_vec1:
+  fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
+  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
+  apply (rule linear_vmul_component)
+  by auto
+
+lemma linear_from_scalars:
+  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
+  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
+  apply (rule ext)
+  apply (subst matrix_works[OF lf, symmetric])
+  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute)
+  done
+
+lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
+  shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
+  apply (rule ext)
+  apply (subst matrix_works[OF lf, symmetric])
+  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
+  done
+
+lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: dest_vec1_eq[symmetric])
+
+lemma setsum_scalars: assumes fS: "finite S"
+  shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
+  unfolding vec_setsum[OF fS] by simp
+
+lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
+  apply (cases "dest_vec1 x \<le> dest_vec1 y")
+  apply simp
+  apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
+  apply (auto)
+  done
+
+text{* Lifting and dropping *}
+
+lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
+  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
+  using assms unfolding continuous_on_iff apply safe
+  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
+  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
+  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
+  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
+  using assms unfolding continuous_on_iff apply safe
+  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
+  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
+  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
+  by(rule linear_continuous_on[OF bounded_linear_vec1])
+
+lemma mem_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
+ "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+by(simp_all add: Cart_eq vector_less_def vector_le_def)
+
+lemma vec1_interval:fixes a::"real" shows
+  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
+  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
+  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
+  unfolding forall_1 unfolding vec1_dest_vec1_simps
+  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+(* Some special cases for intervals in R^1.                                  *)
+
+lemma interval_cases_1: fixes x :: "real^1" shows
+ "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
+  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma in_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
+  (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma interval_eq_empty_1: fixes a :: "real^1" shows
+  "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
+  "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
+  unfolding interval_eq_empty and ex_1 by auto
+
+lemma subset_interval_1: fixes a :: "real^1" shows
+ "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
+                dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+  unfolding subset_interval[of a b c d] unfolding forall_1 by auto
+
+lemma eq_interval_1: fixes a :: "real^1" shows
+ "{a .. b} = {c .. d} \<longleftrightarrow>
+          dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
+          dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
+unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
+unfolding subset_interval_1(1)[of a b c d]
+unfolding subset_interval_1(1)[of c d a b]
+by auto
+
+lemma disjoint_interval_1: fixes a :: "real^1" shows
+  "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
+  "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  unfolding disjoint_interval and ex_1 by auto
+
+lemma open_closed_interval_1: fixes a :: "real^1" shows
+ "{a<..<b} = {a .. b} - {a, b}"
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
+  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
+  using Lim_component_le[of f l net 1 b] by auto
+
+lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
+ "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
+  using Lim_component_ge[of f l net b 1] by auto
+
+text{* Also more convenient formulations of monotone convergence.                *}
+
+lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
+  assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
+  shows "\<exists>l. (s ---> l) sequentially"
+proof-
+  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
+  { fix m::nat
+    have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
+      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
+  hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
+  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
+  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
+    unfolding dist_norm unfolding abs_dest_vec1  by auto
+qed
+
+lemma dest_vec1_simps[simp]: fixes a::"real^1"
+  shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
+  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
+  by(auto simp add: vector_le_def Cart_eq)
+
+lemma dest_vec1_inverval:
+  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
+  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
+  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
+  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
+  apply(rule_tac [!] equalityI)
+  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
+  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
+  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
+  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
+  by (auto simp add: vector_less_def vector_le_def)
+
+lemma dest_vec1_setsum: assumes "finite S"
+  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
+  using dest_vec1_sum[OF assms] by auto
+
+lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
+unfolding open_vector_def forall_1 by auto
+
+lemma tendsto_dest_vec1 [tendsto_intros]:
+  "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
+by(rule tendsto_Cart_nth)
+
+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 forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" 
+  apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
+
+lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
+  apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto 
+
+lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
+  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
+
+end