diff -r 6849464ab10e -r 44e42d392c6e src/HOL/Multivariate_Analysis/Vec1.thy
--- a/src/HOL/Multivariate_Analysis/Vec1.thy	Mon Jun 21 14:07:00 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,405 +0,0 @@
-(*  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 [simp]: "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:: "real^_ \<Rightarrow> real^1"
-  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
-  unfolding smult_conv_scaleR
-  by (rule linear_vmul_component)
-
-lemma linear_from_scalars:
-  assumes lf: "linear (f::real^1 \<Rightarrow> real^_)"
-  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
-  unfolding smult_conv_scaleR
-  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
-
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto
-
-lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
-  shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
-  { assume ?l guess K using linear_bounded[OF `?l`] ..
-    hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
-      unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
-  thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
-    unfolding vec1_dest_vec1_simps by auto qed
-
-lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
-  unfolding vector_le_def by auto
-lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
-  unfolding vector_less_def by auto
-
-end