--- 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