# HG changeset patch
# User immler
# Date 1519318868 -3600
# Node ID 2c58505bf151c9094f768ca4acbb7ba5fe727e15
# Parent  817944aeac3fd4b369dd40b5d332709db6dda10f# Parent  bdff8bf0a75bff999eaccd5ed2ae1f913f0b23bf
merged

diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -277,14 +277,22 @@
   by (simp add: vec_eq_iff)
 
 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
+
+lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+  by (simp add: inner_axis' norm_eq_1)
+
 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   by vector
+
 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
+
 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
+
 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
   by (metis vector_mul_lcancel)
+
 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
   by (metis vector_mul_rcancel)
 
@@ -563,7 +571,7 @@
 lemma transpose_mat [simp]: "transpose (mat n) = mat n"
   by (vector transpose_def mat_def)
 
-lemma transpose_transpose: "transpose(transpose A) = A"
+lemma transpose_transpose [simp]: "transpose(transpose A) = A"
   by (vector transpose_def)
 
 lemma row_transpose [simp]:
@@ -576,10 +584,10 @@
   shows "column i (transpose A) = row i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
 
-lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
+lemma rows_transpose [simp]: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
   by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
 
-lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
+lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
   by (metis transpose_transpose rows_transpose)
 
 lemma matrix_mult_transpose_dot_column:
@@ -642,6 +650,12 @@
   by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
       field_simps sum_distrib_left sum.distrib)
 
+lemma
+  fixes A :: "real^'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_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
+
 lemma matrix_vector_mult_add_distrib [algebra_simps]:
   fixes A :: "real^'n^'m"
   shows "A *v (x + y) = A *v x + A *v y"
@@ -682,6 +696,8 @@
 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
   by (simp add: ext matrix_works)
 
+declare matrix_vector_mul [symmetric, simp]
+
 lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
 
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -4783,6 +4783,21 @@
     by (simp add: \<open>countable \<F>'\<close> countable_subset)
 qed
 
+lemma countable_disjoint_nonempty_interior_subsets:
+  fixes \<F> :: "'a::euclidean_space set set"
+  assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+  shows "countable \<F>"
+proof (rule countable_image_inj_on)
+  have "disjoint (interior ` \<F>)"
+    using pw by (simp add: disjoint_image_subset interior_subset)
+  then show "countable (interior ` \<F>)"
+    by (auto intro: countable_disjoint_open_subsets)
+  show "inj_on interior \<F>"
+    using pw apply (clarsimp simp: inj_on_def pairwise_def)
+    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+    done
+qed
+
 lemma closedin_compact:
    "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
 by (metis closedin_closed compact_Int_closed)
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -929,7 +929,7 @@
     by auto
 qed
 
-text \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix.\<close>
 
 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
@@ -945,6 +945,51 @@
 definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
 
+lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+  by (simp add: linear_iff orthogonal_transformation_def)
+
+lemma orthogonal_orthogonal_transformation:
+    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
+  by (simp add: orthogonal_def orthogonal_transformation_def)
+
+lemma orthogonal_transformation_compose:
+   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
+  by (simp add: orthogonal_transformation_def linear_compose)
+
+lemma orthogonal_transformation_neg:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
+  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
+
+lemma orthogonal_transformation_linear:
+   "orthogonal_transformation f \<Longrightarrow> linear f"
+  by (simp add: orthogonal_transformation_def)
+
+lemma orthogonal_transformation_inj:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> inj f"
+  unfolding orthogonal_transformation_def inj_on_def by (metis euclidean_eqI)
+
+lemma orthogonal_transformation_surj:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> surj f"
+  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
+
+lemma orthogonal_transformation_bij:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> bij f"
+  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
+
+lemma orthogonal_transformation_inv:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+
+lemma orthogonal_transformation_norm:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
+  by (metis orthogonal_transformation)
+
 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
   by (metis matrix_left_right_inverse orthogonal_matrix_def)
 
@@ -1038,7 +1083,13 @@
   then show ?thesis unfolding th .
 qed
 
-text \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+lemma orthogonal_transformation_det [simp]:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
+  using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+
+
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
 
 lemma scaling_linear:
   fixes f :: "real ^'n \<Rightarrow> real ^'n"
@@ -1071,20 +1122,138 @@
 lemma orthogonal_transformation_isometry:
   "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
-  apply (rule iffI)
-  apply clarify
-  apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm)
-  apply (rule conjI)
-  apply (rule isometry_linear)
-  apply simp
-  apply simp
-  apply clarify
-  apply (erule_tac x=v in allE)
-  apply (erule_tac x=0 in allE)
-  apply (simp add: dist_norm)
-  done
+  apply (auto simp: linear_0 isometry_linear)
+   apply (metis (no_types, hide_lams) dist_norm linear_diff)
+  by (metis dist_0_norm)
+
+
+lemma image_orthogonal_transformation_ball:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  assumes "orthogonal_transformation f"
+  shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` ball x r"
+  with assms show "y \<in> ball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> ball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` ball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+  fixes f :: "real^'n \<Rightarrow> real^'n"
+  assumes "orthogonal_transformation f"
+  shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` cball x r"
+  with assms show "y \<in> cball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> cball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` cball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+
+lemma orthogonal_matrix_transpose [simp]:
+     "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
+  by (auto simp: orthogonal_matrix_def)
+
+lemma orthogonal_matrix_orthonormal_columns:
+  fixes A :: "real^'n^'n"
+  shows "orthogonal_matrix A \<longleftrightarrow>
+          (\<forall>i. norm(column i A) = 1) \<and>
+          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
+  by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
+
+lemma orthogonal_matrix_orthonormal_rows:
+  fixes A :: "real^'n^'n"
+  shows "orthogonal_matrix A \<longleftrightarrow>
+          (\<forall>i. norm(row i A) = 1) \<and>
+          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
+  using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
 
-text \<open>Can extend an isometry from unit sphere.\<close>
+lemma orthogonal_matrix_exists_basis:
+  fixes a :: "real^'n"
+  assumes "norm a = 1"
+  obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
+proof -
+  obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+   and "independent S" "card S = CARD('n)" "span S = UNIV"
+    using vector_in_orthonormal_basis assms by force
+  with independent_imp_finite obtain f0 where "bij_betw f0 (UNIV::'n set) S"
+    by (metis finite_class.finite_UNIV finite_same_card_bij)
+  then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
+    using bij_swap_iff [of k "inv f0 a" f0]
+    by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)
+  show thesis
+  proof
+    have [simp]: "\<And>i. norm (f i) = 1"
+      using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
+    have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
+      using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
+      by (auto simp: pairwise_def bij_betw_def inj_on_def)
+    show "orthogonal_matrix (\<chi> i j. f j $ i)"
+      by (simp add: orthogonal_matrix_orthonormal_columns column_def)
+    show "(\<chi> i j. f j $ i) *v axis k 1 = a"
+      by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
+  qed
+qed
+
+lemma orthogonal_transformation_exists_1:
+  fixes a b :: "real^'n"
+  assumes "norm a = 1" "norm b = 1"
+  obtains f where "orthogonal_transformation f" "f a = b"
+proof -
+  obtain k::'n where True
+    by simp
+  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+    using orthogonal_matrix_exists_basis assms by metis
+  let ?f = "\<lambda>x. (B ** transpose A) *v x"
+  show thesis
+  proof
+    show "orthogonal_transformation ?f"
+      by (simp add: AB orthogonal_matrix_mul matrix_vector_mul_linear orthogonal_transformation_matrix)
+  next
+    show "?f a = b"
+      using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
+      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+  qed
+qed
+
+lemma orthogonal_transformation_exists:
+  fixes a b :: "real^'n"
+  assumes "norm a = norm b"
+  obtains f where "orthogonal_transformation f" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  with assms show ?thesis
+    using orthogonal_transformation_isometry that by fastforce
+next
+  case False
+  then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
+    by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
+  show ?thesis
+  proof
+    have "linear f"
+      using f by (simp add: orthogonal_transformation_linear)
+    then have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
+      by (simp add: linear_cmul [of f])
+    also have "\<dots> = b /\<^sub>R norm a"
+      by (simp add: eq assms [symmetric])
+    finally show "f a = b"
+      using False by auto
+  qed (use f in auto)
+qed
+
+
+subsection \<open>Can extend an isometry from unit sphere.\<close>
 
 lemma isometry_sphere_extend:
   fixes f:: "real ^'n \<Rightarrow> real ^'n"
@@ -1182,7 +1351,7 @@
     done
 qed
 
-text \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion.\<close>
 
 definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
 definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
@@ -1238,4 +1407,111 @@
     by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
 qed
 
+text\<open> Slightly stronger results giving rotation, but only in two or more dimensions.\<close>
+
+lemma rotation_matrix_exists_basis:
+  fixes a :: "real^'n"
+  assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
+  obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
+proof -
+  obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a"
+    using orthogonal_matrix_exists_basis assms by metis
+  with orthogonal_rotation_or_rotoinversion
+  consider "rotation_matrix A" | "rotoinversion_matrix A"
+    by metis
+  then show thesis
+  proof cases
+    assume "rotation_matrix A"
+    then show ?thesis
+      using \<open>A *v axis k 1 = a\<close> that by auto
+  next
+    obtain j where "j \<noteq> k"
+      by (metis (full_types) 2 card_2_exists ex_card)
+    let ?TA = "transpose A"
+    let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i"
+    assume "rotoinversion_matrix A"
+    then have [simp]: "det A = -1"
+      by (simp add: rotoinversion_matrix_def)
+    show ?thesis
+    proof
+      have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i
+        by (auto simp: row_def)
+      have "orthogonal_matrix ?A"
+        unfolding orthogonal_matrix_orthonormal_rows
+        using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses)
+      then show "rotation_matrix (transpose ?A)"
+        unfolding rotation_matrix_def
+        by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR])
+      show "transpose ?A *v axis k 1 = a"
+        using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong)
+    qed
+  qed
+qed
+
+lemma rotation_exists_1:
+  fixes a :: "real^'n"
+  assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
+  obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof -
+  obtain k::'n where True
+    by simp
+  obtain A B where AB: "rotation_matrix A" "rotation_matrix B"
+               and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+    using rotation_matrix_exists_basis assms by metis
+  let ?f = "\<lambda>x. (B ** transpose A) *v x"
+  show thesis
+  proof
+    show "orthogonal_transformation ?f"
+      using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force
+    show "det (matrix ?f) = 1"
+      using AB by (auto simp: det_mul rotation_matrix_def)
+    show "?f a = b"
+      using AB unfolding orthogonal_matrix_def rotation_matrix_def
+      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+  qed
+qed
+
+lemma rotation_exists:
+  fixes a :: "real^'n"
+  assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
+  obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  with assms have "a = 0" "b = 0"
+    by auto
+  then show ?thesis
+    by (metis eq_id_iff matrix_id orthogonal_transformation_id that)
+next
+  case False
+  with that show thesis
+    by (auto simp: eq linear_cmul orthogonal_transformation_def
+             intro: rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2])
+qed
+
+lemma rotation_rightward_line:
+  fixes a :: "real^'n"
+  obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
+                  "f(norm a *\<^sub>R axis k 1) = a"
+proof (cases "CARD('n) = 1")
+  case True
+  obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a"
+  proof (rule orthogonal_transformation_exists)
+    show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+      by simp
+  qed auto
+  then show thesis
+    using True that by auto
+next
+  case False
+  obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a"
+  proof (rule rotation_exists)
+    show "2 \<le> CARD('n)"
+      using False one_le_card_finite [where 'a='n] by linarith
+    show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+      by simp
+  qed auto
+  then show thesis
+    using that by blast
+qed
+
 end
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -144,6 +144,28 @@
   qed
 qed (simp_all add: infinite_UNIV_vec)
 
+lemma countable_vector:
+  fixes B:: "'n::finite \<Rightarrow> 'a set"
+  assumes "\<And>i. countable (B i)"
+  shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
+proof -
+  have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f
+  proof -
+    have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f"
+      by (metis that PiE_iff UNIV_I vec_lambda_inverse)
+    then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}"
+      by blast
+  qed
+  then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}"
+    by blast
+  then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+    by (metis finite_class.finite_UNIV countable_PiE assms)
+  then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+    by auto
+  then show ?thesis
+    by (simp add: image_comp o_def vec_nth_inverse)
+qed
+
 subsection \<open>Group operations and class instances\<close>
 
 instantiation vec :: (zero, finite) zero
@@ -601,6 +623,9 @@
   apply (simp add: axis_def)
   done
 
+lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+  by (simp add: inner_axis inner_commute)
+
 instantiation vec :: (euclidean_space, finite) euclidean_space
 begin
 
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -5221,7 +5221,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes \<T>: "finite \<T>"
     and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
-    and neg: "\<And>S S'. \<lbrakk>S \<in> \<T>; S' \<in> \<T>; S \<noteq> S'\<rbrakk> \<Longrightarrow> negligible (S \<inter> S')"
+    and neg: "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
   shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
 proof -
   let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
@@ -5236,7 +5236,7 @@
       ultimately show "finite ?\<U>"
         by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
       show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
-        using neg by auto
+        using neg unfolding pairwise_def by auto
     qed
   next
     show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
@@ -5247,7 +5247,7 @@
         using that by blast
       ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
         by (simp add: sum.delta[OF \<T>])
-    qed 
+    qed
   next
     show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
       apply (rule has_integral_sum [OF \<T>])
@@ -5277,7 +5277,7 @@
   qed
   show ?thesis
     unfolding \<D>(6)[symmetric]
-    by (auto intro: \<D> neg assms has_integral_Union)
+    by (auto intro: \<D> neg assms has_integral_Union pairwiseI)
 qed
 
 lemma integral_combine_division_bottomup:
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -7281,6 +7281,66 @@
   with assms show ?thesis by auto
 qed
 
+lemma vector_in_orthogonal_spanningset:
+  fixes a :: "'a::euclidean_space"
+  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
+
+lemma vector_in_orthogonal_basis:
+  fixes a :: "'a::euclidean_space"
+  assumes "a \<noteq> 0"
+  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
+                  "span S = UNIV" "card S = DIM('a)"
+proof -
+  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+    using vector_in_orthogonal_spanningset .
+  show thesis
+  proof
+    show "pairwise orthogonal (S - {0})"
+      using pairwise_mono S(2) by blast
+    show "independent (S - {0})"
+      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
+    show "finite (S - {0})"
+      using \<open>independent (S - {0})\<close> independent_finite by blast
+    show "card (S - {0}) = DIM('a)"
+      using span_delete_0 [of S] S
+      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
+  qed (use S \<open>a \<noteq> 0\<close> in auto)
+qed
+
+lemma vector_in_orthonormal_basis:
+  fixes a :: "'a::euclidean_space"
+  assumes "norm a = 1"
+  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+    "independent S" "card S = DIM('a)" "span S = UNIV"
+proof -
+  have "a \<noteq> 0"
+    using assms by auto
+  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
+          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
+    by (metis vector_in_orthogonal_basis)
+  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
+  show thesis
+  proof
+    show "a \<in> ?S"
+      using \<open>a \<in> S\<close> assms image_iff by fastforce
+  next
+    show "pairwise orthogonal ?S"
+      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
+    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
+      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
+    then show "independent ?S"
+      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
+    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
+      unfolding inj_on_def
+      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
+    then show "card ?S = DIM('a)"
+      by (simp add: card_image S)
+    show "span ?S = UNIV"
+      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close> field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff)
+  qed
+qed
+
 proposition dim_orthogonal_sum:
   fixes A :: "'a::euclidean_space set"
   assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -3652,12 +3652,26 @@
     using assms by (fastforce simp: bounded_iff)
 qed
 
+lemma bounded_plus:
+  fixes S ::"'a::real_normed_vector set"
+  assumes "bounded S" "bounded T"
+  shows "bounded ((\<lambda>(x,y). x + y) ` (S \<times> T))"
+  using bounded_plus_comp [of fst "S \<times> T" snd] assms
+  by (auto simp: split_def split: if_split_asm)
+
 lemma bounded_minus_comp:
   "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
   for f g::"'a \<Rightarrow> 'b::real_normed_vector"
   using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
   by auto
 
+lemma bounded_minus:
+  fixes S ::"'a::real_normed_vector set"
+  assumes "bounded S" "bounded T"
+  shows "bounded ((\<lambda>(x,y). x - y) ` (S \<times> T))"
+  using bounded_minus_comp [of fst "S \<times> T" snd] assms
+  by (auto simp: split_def split: if_split_asm)
+
 
 subsection \<open>Compactness\<close>
 
@@ -4014,7 +4028,6 @@
          \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
 by (metis Int_Diff open_delete openin_open)
 
-
 text\<open>Compactness expressed with filters\<close>
 
 lemma closure_iff_nhds_not_empty:
@@ -4643,6 +4656,27 @@
   shows "~ compact (UNIV::'a set)"
     by (simp add: compact_eq_bounded_closed)
 
+text\<open>Representing sets as the union of a chain of compact sets.\<close>
+lemma closed_Union_compact_subsets:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes "closed S"
+  obtains F where "\<And>n. compact(F n)" "\<And>n. F n \<subseteq> S" "\<And>n. F n \<subseteq> F(Suc n)"
+                  "(\<Union>n. F n) = S" "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. K \<subseteq> F n"
+proof
+  show "compact (S \<inter> cball 0 (of_nat n))" for n
+    using assms compact_eq_bounded_closed by auto
+next
+  show "(\<Union>n. S \<inter> cball 0 (real n)) = S"
+    by (auto simp: real_arch_simple)
+next
+  fix K :: "'a set"
+  assume "compact K" "K \<subseteq> S"
+  then obtain N where "K \<subseteq> cball 0 N"
+    by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
+  then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)"
+    by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
+qed auto
+
 instance real :: heine_borel
 proof
   fix f :: "nat \<Rightarrow> real"
@@ -5062,10 +5096,7 @@
 
 lemma continuous_within_eps_delta:
   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
-  unfolding continuous_within and Lim_within
-  apply auto
-  apply (metis dist_nz dist_self, blast)
-  done
+  unfolding continuous_within and Lim_within  by fastforce
 
 corollary continuous_at_eps_delta:
   "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -332,34 +332,6 @@
     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
 qed
 
-lemma delta [simp]:
-  assumes fS: "finite S"
-  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-proof -
-  let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
-  show ?thesis
-  proof (cases "a \<in> S")
-    case False
-    then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
-    with False show ?thesis by simp
-  next
-    case True
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    from True have eq: "S = ?A \<union> ?B" by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
-      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
-    with True show ?thesis by simp
-  qed
-qed
-
-lemma delta' [simp]:
-  assumes fin: "finite S"
-  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-  using delta [OF fin, of a b, symmetric] by (auto intro: cong)
-
 lemma delta_remove:
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
@@ -384,6 +356,16 @@
   qed
 qed
 
+lemma delta [simp]:
+  assumes fS: "finite S"
+  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+  by (simp add: delta_remove [OF assms])
+
+lemma delta' [simp]:
+  assumes fin: "finite S"
+  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+  using delta [OF fin, of a b, symmetric] by (auto intro: cong)
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fin: "finite A"
diff -r bdff8bf0a75b -r 2c58505bf151 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Thu Feb 22 15:17:25 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -10,6 +10,9 @@
 
 definition "indicator S x = (if x \<in> S then 1 else 0)"
 
+text\<open>Type constrained version\<close>
+abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
+
 lemma indicator_simps[simp]:
   "x \<in> S \<Longrightarrow> indicator S x = 1"
   "x \<notin> S \<Longrightarrow> indicator S x = 0"