# HG changeset patch
# User nipkow
# Date 1547654611 -3600
# Node ID de2f0a24b0f00e0b372c095615d1117958f287e3
# Parent  14a8cac10eac7d220bcee68b185b298cec61741f
Reorg of material

diff -r 14a8cac10eac -r de2f0a24b0f0 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 16:18:53 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 17:03:31 2019 +0100
@@ -179,90 +179,16 @@
     by force
 qed
 
-lemma%unimportant matrix_mult_transpose_dot_column:
-  shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
-  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
-
-lemma%unimportant matrix_mult_transpose_dot_row:
-  shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
-  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
-
 lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
   using matrix_vector_mul_linear[of A]
   by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
 
-lemma%unimportant (* FIX ME needs name*)
+lemma%unimportant
   fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
   shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
     and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
   by (simp_all add: linear_continuous_at linear_continuous_on)
 
-lemma%unimportant scalar_invertible:
-  fixes A :: "('a::real_algebra_1)^'m^'n"
-  assumes "k \<noteq> 0" and "invertible A"
-  shows "invertible (k *\<^sub>R A)"
-proof -
-  obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
-    using assms unfolding invertible_def by auto
-  with \<open>k \<noteq> 0\<close>
-  have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
-    by (simp_all add: assms matrix_scalar_ac)
-  thus "invertible (k *\<^sub>R A)"
-    unfolding invertible_def by auto
-qed
-
-lemma%unimportant scalar_invertible_iff:
-  fixes A :: "('a::real_algebra_1)^'m^'n"
-  assumes "k \<noteq> 0" and "invertible A"
-  shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
-  by (simp add: assms scalar_invertible)
-
-lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
-  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
-
-lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
-  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
-
-lemma%unimportant vector_scalar_commute:
-  fixes A :: "'a::{field}^'m^'n"
-  shows "A *v (c *s x) = c *s (A *v x)"
-  by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
-
-lemma%unimportant scalar_vector_matrix_assoc:
-  fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
-  shows "(k *s x) v* A = k *s (x v* A)"
-  by (metis transpose_matrix_vector vector_scalar_commute)
- 
-lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0"
-  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-
-lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
-  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-
-lemma%unimportant vector_matrix_mul_rid [simp]:
-  fixes v :: "('a::semiring_1)^'n"
-  shows "v v* mat 1 = v"
-  by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-
-lemma%unimportant scaleR_vector_matrix_assoc:
-  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
-  shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
-  by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
-
-lemma%important vector_scaleR_matrix_ac:
-  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
-  shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
-proof%unimportant -
-  have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
-    unfolding vector_matrix_mult_def
-    by (simp add: algebra_simps)
-  with scaleR_vector_matrix_assoc
-  show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
-    by auto
-qed
-
 
 subsection%important\<open>Bounds on components etc.\ relative to operator norm\<close>
 
@@ -341,26 +267,6 @@
   finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
 qed
 
-subsection%important \<open>lambda skolemization on cartesian products\<close>
-
-lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
-   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
-proof%unimportant -
-  let ?S = "(UNIV :: 'n set)"
-  { assume H: "?rhs"
-    then have ?lhs by auto }
-  moreover
-  { assume H: "?lhs"
-    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
-    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
-    { fix i
-      from f have "P i (f i)" by metis
-      then have "P i (?x $ i)" by auto
-    }
-    hence "\<forall>i. P i (?x$i)" by metis
-    hence ?rhs by metis }
-  ultimately show ?thesis by metis
-qed
 
 lemma%unimportant rational_approximation:
   assumes "e > 0"
@@ -391,36 +297,6 @@
 lemma%unimportant vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
   unfolding inner_simps scalar_mult_eq_scaleR by auto
 
-
-text \<open>The same result in terms of square matrices.\<close>
-
-
-text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
-
-definition%unimportant "rowvector v = (\<chi> i j. (v$j))"
-
-definition%unimportant "columnvector v = (\<chi> i j. (v$i))"
-
-lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v"
-  by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
-
-lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v"
-  by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
-
-lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
-  by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
-
-lemma%unimportant dot_matrix_product:
-  "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
-  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
-
-lemma%unimportant dot_matrix_vector_mul:
-  fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
-  shows "(A *v x) \<bullet> (B *v y) =
-      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
-  unfolding dot_matrix_product transpose_columnvector[symmetric]
-    dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
-
 lemma%unimportant infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
   by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
 
@@ -601,16 +477,16 @@
   by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex)
 
 lemma%unimportant closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \<le> a}"
-  by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: closed_Collect_le continuous_on_component)
 
 lemma%unimportant closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \<ge> a}"
-  by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: closed_Collect_le continuous_on_component)
 
 lemma%unimportant open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}"
-  by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: open_Collect_less continuous_on_component)
 
 lemma%unimportant open_halfspace_component_gt_cart: "open {x::real^'n. x$i  > a}"
-  by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: open_Collect_less continuous_on_component)
 
 lemma%unimportant Lim_component_le_cart:
   fixes f :: "'a \<Rightarrow> real^'n"
@@ -651,69 +527,6 @@
     unfolding Collect_all_eq by (simp add: closed_INT)
 qed
 
-lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
-  (is "vec.dim ?A = _")
-proof%unimportant (rule vec.dim_unique)
-  let ?B = "((\<lambda>x. axis x 1) ` d)"
-  have subset_basis: "?B \<subseteq> cart_basis"
-    by (auto simp: cart_basis_def)
-  show "?B \<subseteq> ?A"
-    by (auto simp: axis_def)
-  show "vec.independent ((\<lambda>x. axis x 1) ` d)"
-    using subset_basis
-    by (rule vec.independent_mono[OF vec.independent_Basis])
-  have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n"
-  proof -
-    have "finite ?B"
-      using subset_basis finite_cart_basis
-      by (rule finite_subset)
-    have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)"
-      by (rule basis_expansion[symmetric])
-    also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)"
-      by (rule sum.mono_neutral_cong_right) (auto simp: that)
-    also have "\<dots> \<in> vec.span ?B"
-      by (simp add: vec.span_sum vec.span_clauses)
-    finally show "x \<in> vec.span ?B" .
-  qed
-  then show "?A \<subseteq> vec.span ?B" by auto
-qed (simp add: card_image inj_on_def axis_eq_axis)
-
-lemma%unimportant affinity_inverses:
-  assumes m0: "m \<noteq> (0::'a::field)"
-  shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
-  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
-  using m0
-  by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
-
-lemma%important vector_affinity_eq:
-  assumes m0: "(m::'a::field) \<noteq> 0"
-  shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
-proof%unimportant
-  assume h: "m *s x + c = y"
-  hence "m *s x = y - c" by (simp add: field_simps)
-  hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
-  then show "x = inverse m *s y + - (inverse m *s c)"
-    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
-next
-  assume h: "x = inverse m *s y + - (inverse m *s c)"
-  show "m *s x + c = y" unfolding h
-    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
-qed
-
-lemma%unimportant vector_eq_affinity:
-    "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
-  using vector_affinity_eq[where m=m and x=x and y=y and c=c]
-  by metis
-
-lemma%unimportant vector_cart:
-  fixes f :: "real^'n \<Rightarrow> real"
-  shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
-  unfolding euclidean_eq_iff[where 'a="real^'n"]
-  by simp (simp add: Basis_vec_def inner_axis)
-
-lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
-  by (rule vector_cart)
-
 subsection%important "Convex Euclidean Space"
 
 lemma%unimportant Cart_1:"(1::real^'n) = \<Sum>Basis"
@@ -778,83 +591,8 @@
     vector_cart[of "\<lambda>j. frechet_derivative f (at x) j $ k"]
   by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def)
 
-subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
-
-lemma exhaust_2:
-  fixes x :: 2
-  shows "x = 1 \<or> x = 2"
-proof (induct x)
-  case (of_int z)
-  then have "0 \<le> 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 \<le> 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 sum_1: "sum f (UNIV::1 set) = f 1"
-  unfolding UNIV_1 by simp
-
-lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
-  unfolding UNIV_2 by simp
-
-lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
-  unfolding UNIV_3 by (simp add: ac_simps)
-
-subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
-
-lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
-  by (simp add: vec_eq_iff)
-
-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_vec_def)
-
-lemma dist_vector_1:
-  fixes x :: "'a::real_normed_vector^1"
-  shows "dist x y = dist (x$1) (y$1)"
-  by (simp add: dist_norm norm_vector_1)
-
-lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
-  by (simp add: norm_vector_1)
-
-lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
-  by (auto simp add: norm_real dist_norm)
-
 subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
 
-lemma vector_one_nth [simp]:
-  fixes x :: "'a^1" shows "vec (x $ 1) = x"
-  by (metis vec_def vector_one)
-
 lemma vec_cbox_1_eq [simp]:
   shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)"
   by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
@@ -885,72 +623,6 @@
   qed
 qed simp
 
-lemma tendsto_at_within_vector_1:
-  fixes S :: "'a :: metric_space set"
-  assumes "(f \<longlongrightarrow> fx) (at x within S)"
-  shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
-proof (rule topological_tendstoI)
-  fix T :: "('a^1) set"
-  assume "open T" "vec fx \<in> T"
-  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
-    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
-  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
-    unfolding eventually_at dist_norm [symmetric]
-    by (rule ex_forward)
-       (use \<open>open T\<close> in 
-         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
-qed
-
-lemma has_derivative_vector_1:
-  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
-  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
-         (at ((vec a)::real^1) within vec ` S)"
-    using der_g
-    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
-    apply (drule tendsto_at_within_vector_1, vector)
-    apply (auto simp: algebra_simps eventually_at tendsto_def)
-    done
-
-
-subsection%unimportant\<open>Explicit vector construction from lists\<close>
-
-definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
-
-lemma vector_1 [simp]: "(vector[x]) $1 = x"
-  unfolding vector_def by simp
-
-lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
-  unfolding vector_def by simp_all
-
-lemma vector_3 [simp]:
- "(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]))"
-  by (metis vector_1 vector_one)
-
-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 interval_split_cart:
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
diff -r 14a8cac10eac -r de2f0a24b0f0 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 16:18:53 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 17:03:31 2019 +0100
@@ -669,4 +669,265 @@
   shows "rank(A ** B) \<le> rank A"
   by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
 
+
+subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
+
+lemma exhaust_2:
+  fixes x :: 2
+  shows "x = 1 \<or> x = 2"
+proof (induct x)
+  case (of_int z)
+  then have "0 \<le> 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 \<le> 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 sum_1: "sum f (UNIV::1 set) = f 1"
+  unfolding UNIV_1 by simp
+
+lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
+  unfolding UNIV_2 by simp
+
+lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
+  unfolding UNIV_3 by (simp add: ac_simps)
+
+subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
+
+lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
+  by (simp add: vec_eq_iff)
+
+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_vec_def)
+
+lemma dist_vector_1:
+  fixes x :: "'a::real_normed_vector^1"
+  shows "dist x y = dist (x$1) (y$1)"
+  by (simp add: dist_norm norm_vector_1)
+
+lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
+  by (simp add: norm_vector_1)
+
+lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
+  by (auto simp add: norm_real dist_norm)
+
+
+subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
+
+lemma vector_one_nth [simp]:
+  fixes x :: "'a^1" shows "vec (x $ 1) = x"
+  by (metis vec_def vector_one)
+
+lemma tendsto_at_within_vector_1:
+  fixes S :: "'a :: metric_space set"
+  assumes "(f \<longlongrightarrow> fx) (at x within S)"
+  shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
+proof (rule topological_tendstoI)
+  fix T :: "('a^1) set"
+  assume "open T" "vec fx \<in> T"
+  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
+    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
+  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
+    unfolding eventually_at dist_norm [symmetric]
+    by (rule ex_forward)
+       (use \<open>open T\<close> in 
+         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
+qed
+
+lemma has_derivative_vector_1:
+  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
+  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
+         (at ((vec a)::real^1) within vec ` S)"
+    using der_g
+    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
+    apply (drule tendsto_at_within_vector_1, vector)
+    apply (auto simp: algebra_simps eventually_at tendsto_def)
+    done
+
+
+subsection%unimportant\<open>Explicit vector construction from lists\<close>
+
+definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
+
+lemma vector_1 [simp]: "(vector[x]) $1 = x"
+  unfolding vector_def by simp
+
+lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
+  unfolding vector_def by simp_all
+
+lemma vector_3 [simp]:
+ "(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]))"
+  by (metis vector_1 vector_one)
+
+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%unimportant \<open>lambda skolemization on cartesian products\<close>
+
+lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
+   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
+proof%unimportant -
+  let ?S = "(UNIV :: 'n set)"
+  { assume H: "?rhs"
+    then have ?lhs by auto }
+  moreover
+  { assume H: "?lhs"
+    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
+    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
+    { fix i
+      from f have "P i (f i)" by metis
+      then have "P i (?x $ i)" by auto
+    }
+    hence "\<forall>i. P i (?x$i)" by metis
+    hence ?rhs by metis }
+  ultimately show ?thesis by metis
+qed
+
+
+text \<open>The same result in terms of square matrices.\<close>
+
+
+text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
+
+definition%unimportant "rowvector v = (\<chi> i j. (v$j))"
+
+definition%unimportant "columnvector v = (\<chi> i j. (v$i))"
+
+lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v"
+  by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
+
+lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v"
+  by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
+
+lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
+  by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
+
+lemma%unimportant dot_matrix_product:
+  "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
+  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
+
+lemma%unimportant dot_matrix_vector_mul:
+  fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
+  shows "(A *v x) \<bullet> (B *v y) =
+      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
+  unfolding dot_matrix_product transpose_columnvector[symmetric]
+    dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
+
+
+lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
+  (is "vec.dim ?A = _")
+proof%unimportant (rule vec.dim_unique)
+  let ?B = "((\<lambda>x. axis x 1) ` d)"
+  have subset_basis: "?B \<subseteq> cart_basis"
+    by (auto simp: cart_basis_def)
+  show "?B \<subseteq> ?A"
+    by (auto simp: axis_def)
+  show "vec.independent ((\<lambda>x. axis x 1) ` d)"
+    using subset_basis
+    by (rule vec.independent_mono[OF vec.independent_Basis])
+  have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n"
+  proof -
+    have "finite ?B"
+      using subset_basis finite_cart_basis
+      by (rule finite_subset)
+    have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)"
+      by (rule basis_expansion[symmetric])
+    also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)"
+      by (rule sum.mono_neutral_cong_right) (auto simp: that)
+    also have "\<dots> \<in> vec.span ?B"
+      by (simp add: vec.span_sum vec.span_clauses)
+    finally show "x \<in> vec.span ?B" .
+  qed
+  then show "?A \<subseteq> vec.span ?B" by auto
+qed (simp add: card_image inj_on_def axis_eq_axis)
+
+lemma%unimportant affinity_inverses:
+  assumes m0: "m \<noteq> (0::'a::field)"
+  shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
+  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
+  using m0
+  by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
+
+lemma%important vector_affinity_eq:
+  assumes m0: "(m::'a::field) \<noteq> 0"
+  shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
+proof%unimportant
+  assume h: "m *s x + c = y"
+  hence "m *s x = y - c" by (simp add: field_simps)
+  hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
+  then show "x = inverse m *s y + - (inverse m *s c)"
+    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+next
+  assume h: "x = inverse m *s y + - (inverse m *s c)"
+  show "m *s x + c = y" unfolding h
+    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
+qed
+
+lemma%unimportant vector_eq_affinity:
+    "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
+  using vector_affinity_eq[where m=m and x=x and y=y and c=c]
+  by metis
+
+lemma%unimportant vector_cart:
+  fixes f :: "real^'n \<Rightarrow> real"
+  shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
+  unfolding euclidean_eq_iff[where 'a="real^'n"]
+  by simp (simp add: Basis_vec_def inner_axis)
+
+lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
+  by (rule vector_cart)
+
 end
\ No newline at end of file
diff -r 14a8cac10eac -r de2f0a24b0f0 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 16:18:53 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 17:03:31 2019 +0100
@@ -1082,6 +1082,14 @@
     "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
 
+lemma%unimportant matrix_mult_transpose_dot_column:
+  shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
+
+lemma%unimportant matrix_mult_transpose_dot_row:
+  shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
+
 lemma%unimportant matrix_eq:
   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")