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