--- a/src/HOL/Complex.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Complex.thy Mon May 23 15:33:24 2016 +0100
@@ -799,9 +799,15 @@
lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
by (metis cis_conv_exp cis_pi mult.commute)
+lemma exp_pi_i' [simp]: "exp(ii * of_real pi) = -1"
+ using cis_conv_exp cis_pi by auto
+
lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
by (simp add: exp_eq_polar complex_eq_iff)
+lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
+ by (metis exp_two_pi_i mult.commute)
+
subsubsection \<open>Complex argument\<close>
definition arg :: "complex \<Rightarrow> real" where
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 23 15:33:24 2016 +0100
@@ -1,9 +1,8 @@
(* Title: HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
- Author: Robert Himmelmann, TU Muenchen
- Author: Bogdan Grechuk, University of Edinburgh
+ Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh; LCP
*)
-section \<open>Convex sets, functions and related things.\<close>
+section \<open>Convex sets, functions and related things\<close>
theory Convex_Euclidean_Space
imports
@@ -70,7 +69,7 @@
also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f (x - y) = 0 \<longrightarrow> x - y = 0)"
by (simp add: linear_sub[OF lf])
also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. f x = 0 \<longrightarrow> x = 0)"
- using \<open>subspace S\<close> subspace_def[of S] subspace_sub[of S] by auto
+ using \<open>subspace S\<close> subspace_def[of S] subspace_diff[of S] by auto
finally show ?thesis .
qed
@@ -426,6 +425,12 @@
lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
unfolding affine_def by auto
+lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
+ apply (clarsimp simp add: affine_def)
+ apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
+ apply (auto simp: algebra_simps)
+ done
+
lemma affine_affine_hull [simp]: "affine(affine hull s)"
unfolding hull_def
using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
@@ -2915,11 +2920,16 @@
lemma aff_dim_subspace:
fixes S :: "'n::euclidean_space set"
- assumes "S \<noteq> {}"
- and "subspace S"
+ assumes "subspace S"
shows "aff_dim S = int (dim S)"
- using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S]
- by auto
+proof (cases "S={}")
+ case True with assms show ?thesis
+ by (simp add: subspace_affine)
+next
+ case False
+ with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
+ show ?thesis by auto
+qed
lemma aff_dim_zero:
fixes S :: "'n::euclidean_space set"
@@ -2964,6 +2974,41 @@
then show ?thesis by auto
qed
+lemma affine_independent_card_dim_diffs:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "~ affine_dependent S" "a \<in> S"
+ shows "card S = dim {x - a|x. x \<in> S} + 1"
+proof -
+ have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
+ have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
+ proof (cases "x = a")
+ case True then show ?thesis by simp
+ next
+ case False then show ?thesis
+ using assms by (blast intro: span_superset that)
+ qed
+ have "\<not> affine_dependent (insert a S)"
+ by (simp add: assms insert_absorb)
+ then have 3: "independent {b - a |b. b \<in> S - {a}}"
+ using dependent_imp_affine_dependent by fastforce
+ have "{b - a |b. b \<in> S - {a}} = (\<lambda>b. b-a) ` (S - {a})"
+ by blast
+ then have "card {b - a |b. b \<in> S - {a}} = card ((\<lambda>b. b-a) ` (S - {a}))"
+ by simp
+ also have "... = card (S - {a})"
+ by (metis (no_types, lifting) card_image diff_add_cancel inj_onI)
+ also have "... = card S - 1"
+ by (simp add: aff_independent_finite assms)
+ finally have 4: "card {b - a |b. b \<in> S - {a}} = card S - 1" .
+ have "finite S"
+ by (meson assms aff_independent_finite)
+ with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
+ moreover have "dim {x - a |x. x \<in> S} = card S - 1"
+ using 2 by (blast intro: dim_unique [OF 1 _ 3 4])
+ ultimately show ?thesis
+ by auto
+qed
+
lemma independent_card_le_aff_dim:
fixes B :: "'n::euclidean_space set"
assumes "B \<subseteq> V"
@@ -3361,11 +3406,11 @@
lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
by (metis affine_hull_eq affine_sing)
-lemma rel_interior_sing [simp]: "rel_interior {a :: 'n::euclidean_space} = {a}"
- unfolding rel_interior_ball affine_hull_sing
- apply auto
- apply (rule_tac x = "1 :: real" in exI)
- apply simp
+lemma rel_interior_sing [simp]:
+ fixes a :: "'n::euclidean_space" shows "rel_interior {a} = {a}"
+ apply (auto simp: rel_interior_ball)
+ apply (rule_tac x=1 in exI)
+ apply force
done
lemma subset_rel_interior:
@@ -3671,7 +3716,7 @@
ultimately show ?thesis by auto
qed
-lemma closure_aff_dim:
+lemma closure_aff_dim [simp]:
fixes S :: "'n::euclidean_space set"
shows "aff_dim (closure S) = aff_dim S"
proof -
@@ -3911,7 +3956,7 @@
moreover have "f x - f xy = f (x - xy)"
using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
moreover have *: "x - xy \<in> span S"
- using subspace_sub[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
+ using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
affine_hull_subset_span[of S] span_inc
by auto
moreover from * have "e1 * norm (x - xy) \<le> norm (f (x - xy))"
@@ -6570,6 +6615,17 @@
"\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
+lemma closed_segment_translation:
+ "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
+apply safe
+apply (rule_tac x="x-c" in image_eqI)
+apply (auto simp: in_segment algebra_simps)
+done
+
+lemma open_segment_translation:
+ "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
+by (simp add: open_segment_def closed_segment_translation translation_diff)
+
lemma open_segment_PairD:
"(x, x') \<in> open_segment (a, a') (b, b')
\<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
@@ -6782,6 +6838,118 @@
fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
+lemma dist_in_closed_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> closed_segment a b"
+ shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
+proof (intro conjI)
+ obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+ using assms by (force simp: in_segment algebra_simps)
+ have "dist x a = u * dist a b"
+ apply (simp add: dist_norm algebra_simps x)
+ by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
+ also have "... \<le> dist a b"
+ by (simp add: mult_left_le_one_le u)
+ finally show "dist x a \<le> dist a b" .
+ have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+ by (simp add: dist_norm algebra_simps x)
+ also have "... = (1-u) * dist a b"
+ proof -
+ have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+ using \<open>u \<le> 1\<close> by force
+ then show ?thesis
+ by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+ qed
+ also have "... \<le> dist a b"
+ by (simp add: mult_left_le_one_le u)
+ finally show "dist x b \<le> dist a b" .
+qed
+
+lemma dist_in_open_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment a b"
+ shows "dist x a < dist a b \<and> dist x b < dist a b"
+proof (intro conjI)
+ obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+ using assms by (force simp: in_segment algebra_simps)
+ have "dist x a = u * dist a b"
+ apply (simp add: dist_norm algebra_simps x)
+ by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
+ also have *: "... < dist a b"
+ by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
+ finally show "dist x a < dist a b" .
+ have ab_ne0: "dist a b \<noteq> 0"
+ using * by fastforce
+ have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+ by (simp add: dist_norm algebra_simps x)
+ also have "... = (1-u) * dist a b"
+ proof -
+ have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+ using \<open>u < 1\<close> by force
+ then show ?thesis
+ by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+ qed
+ also have "... < dist a b"
+ using ab_ne0 \<open>0 < u\<close> by simp
+ finally show "dist x b < dist a b" .
+qed
+
+lemma dist_decreases_open_segment_0:
+ fixes x :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment 0 b"
+ shows "dist c x < dist c 0 \<or> dist c x < dist c b"
+proof (rule ccontr, clarsimp simp: not_less)
+ obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
+ using assms by (auto simp: in_segment)
+ have xb: "x \<bullet> b < b \<bullet> b"
+ using u x by auto
+ assume "norm c \<le> dist c x"
+ then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
+ by (simp add: dist_norm norm_le)
+ moreover have "0 < x \<bullet> b"
+ using u x by auto
+ ultimately have less: "c \<bullet> b < x \<bullet> b"
+ by (simp add: x algebra_simps inner_commute u)
+ assume "dist c b \<le> dist c x"
+ then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
+ by (simp add: dist_norm norm_le)
+ then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
+ by (simp add: x algebra_simps inner_commute)
+ then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
+ by (simp add: algebra_simps)
+ then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
+ using \<open>u < 1\<close> by auto
+ with xb have "c \<bullet> b \<ge> x \<bullet> b"
+ by (auto simp: x algebra_simps inner_commute)
+ with less show False by auto
+qed
+
+proposition dist_decreases_open_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment a b"
+ shows "dist c x < dist c a \<or> dist c x < dist c b"
+proof -
+ have *: "x - a \<in> open_segment 0 (b - a)" using assms
+ by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
+ show ?thesis
+ using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
+ by (simp add: dist_norm)
+qed
+
+lemma dist_decreases_closed_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> closed_segment a b"
+ shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
+apply (cases "x \<in> open_segment a b")
+ using dist_decreases_open_segment less_eq_real_def apply blast
+by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
+
+lemma convex_intermediate_ball:
+ fixes a :: "'a :: euclidean_space"
+ shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
+apply (simp add: convex_contains_open_segment, clarify)
+by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
lemma segment_eq_compose:
@@ -8157,6 +8325,28 @@
definition "rel_frontier S = closure S - rel_interior S"
+lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
+ by (simp add: rel_frontier_def)
+
+lemma rel_frontier_sing [simp]:
+ fixes a :: "'n::euclidean_space"
+ shows "rel_frontier {a} = {}"
+ by (simp add: rel_frontier_def)
+
+lemma rel_frontier_cball [simp]:
+ fixes a :: "'n::euclidean_space"
+ shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
+proof (cases rule: linorder_cases [of r 0])
+ case less then show ?thesis
+ by (force simp: sphere_def)
+next
+ case equal then show ?thesis by simp
+next
+ case greater then show ?thesis
+ apply simp
+ by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
+qed
+
lemma closed_affine_hull:
fixes S :: "'n::euclidean_space set"
shows "closed (affine hull S)"
@@ -8190,6 +8380,43 @@
done
qed
+lemma closed_rel_boundary:
+ fixes S :: "'n::euclidean_space set"
+ shows "closed S \<Longrightarrow> closed(S - rel_interior S)"
+by (metis closed_rel_frontier closure_closed rel_frontier_def)
+
+lemma compact_rel_boundary:
+ fixes S :: "'n::euclidean_space set"
+ shows "compact S \<Longrightarrow> compact(S - rel_interior S)"
+by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)
+
+lemma bounded_rel_frontier:
+ fixes S :: "'n::euclidean_space set"
+ shows "bounded S \<Longrightarrow> bounded(rel_frontier S)"
+by (simp add: bounded_closure bounded_diff rel_frontier_def)
+
+lemma compact_rel_frontier_bounded:
+ fixes S :: "'n::euclidean_space set"
+ shows "bounded S \<Longrightarrow> compact(rel_frontier S)"
+using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast
+
+lemma compact_rel_frontier:
+ fixes S :: "'n::euclidean_space set"
+ shows "compact S \<Longrightarrow> compact(rel_frontier S)"
+by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)
+
+lemma convex_same_rel_interior_closure:
+ fixes S :: "'n::euclidean_space set"
+ shows "\<lbrakk>convex S; convex T\<rbrakk>
+ \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> closure S = closure T"
+by (simp add: closure_eq_rel_interior_eq)
+
+lemma convex_same_rel_interior_closure_straddle:
+ fixes S :: "'n::euclidean_space set"
+ shows "\<lbrakk>convex S; convex T\<rbrakk>
+ \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
+ rel_interior S \<subseteq> T \<and> T \<subseteq> closure S"
+by (simp add: closure_eq_between convex_same_rel_interior_closure)
lemma convex_rel_frontier_aff_dim:
fixes S1 S2 :: "'n::euclidean_space set"
@@ -10701,6 +10928,16 @@
shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
by (auto simp: setdist_eq_0_bounded)
+lemma setdist_neq_0_sing_1:
+ fixes s :: "'a::euclidean_space set"
+ shows "\<lbrakk>setdist {x} s = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
+by auto
+
+lemma setdist_neq_0_sing_2:
+ fixes s :: "'a::euclidean_space set"
+ shows "\<lbrakk>setdist s {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
+by auto
+
lemma setdist_sing_in_set:
fixes s :: "'a::euclidean_space set"
shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
@@ -12046,6 +12283,42 @@
done
qed
+proposition orthonormal_basis_subspace:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "subspace S"
+ obtains B where "B \<subseteq> S" "pairwise orthogonal B"
+ and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+ and "independent B" "card B = dim S" "span B = S"
+proof -
+ obtain B where "0 \<notin> B" "B \<subseteq> S"
+ and orth: "pairwise orthogonal B"
+ and "independent B" "card B = dim S" "span B = S"
+ by (blast intro: orthogonal_basis_subspace [OF assms])
+ have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
+ using \<open>span B = S\<close> span_clauses(1) span_mul by fastforce
+ have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
+ using orth by (force simp: pairwise_def orthogonal_clauses)
+ have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
+ by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
+ have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
+ by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
+ have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
+ proof
+ fix x y
+ assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
+ moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
+ using 3 by blast
+ ultimately show "x = y"
+ by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
+ qed
+ then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
+ by (metis \<open>card B = dim S\<close> card_image)
+ have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
+ by (metis "1" "4" "5" assms card_eq_dim independent_finite span_subspace)
+ show ?thesis
+ by (rule that [OF 1 2 3 4 5 6])
+qed
+
proposition orthogonal_subspace_decomp_exists:
fixes S :: "'a :: euclidean_space set"
obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
@@ -12078,6 +12351,7 @@
with assms show ?thesis by auto
qed
+subsection\<open>Parallel slices, etc.\<close>
text\<open> If we take a slice out of a set, we can do it perpendicularly,
with the normal vector to the slice parallel to the affine hull.\<close>
@@ -12139,4 +12413,167 @@
qed
qed
+lemma diffs_affine_hull_span:
+ assumes "a \<in> S"
+ shows "{x - a |x. x \<in> affine hull S} = span {x - a |x. x \<in> S}"
+proof -
+ have *: "((\<lambda>x. x - a) ` (S - {a})) = {x. x + a \<in> S} - {0}"
+ by (auto simp: algebra_simps)
+ show ?thesis
+ apply (simp add: affine_hull_span2 [OF assms] *)
+ apply (auto simp: algebra_simps)
+ done
+qed
+
+lemma aff_dim_dim_affine_diffs:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "affine S" "a \<in> S"
+ shows "aff_dim S = dim {x - a |x. x \<in> S}"
+proof -
+ obtain B where aff: "affine hull B = affine hull S"
+ and ind: "\<not> affine_dependent B"
+ and card: "of_nat (card B) = aff_dim S + 1"
+ using aff_dim_basis_exists by blast
+ then have "B \<noteq> {}" using assms
+ by (metis affine_hull_eq_empty ex_in_conv)
+ then obtain c where "c \<in> B" by auto
+ then have "c \<in> S"
+ by (metis aff affine_hull_eq \<open>affine S\<close> hull_inc)
+ have xy: "x - c = y - a \<longleftrightarrow> y = x + 1 *\<^sub>R (a - c)" for x y c and a::'a
+ by (auto simp: algebra_simps)
+ have *: "{x - c |x. x \<in> S} = {x - a |x. x \<in> S}"
+ apply safe
+ apply (simp_all only: xy)
+ using mem_affine_3_minus [OF \<open>affine S\<close>] \<open>a \<in> S\<close> \<open>c \<in> S\<close> apply blast+
+ done
+ have affS: "affine hull S = S"
+ by (simp add: \<open>affine S\<close>)
+ have "aff_dim S = of_nat (card B) - 1"
+ using card by simp
+ also have "... = dim {x - c |x. x \<in> B}"
+ by (simp add: affine_independent_card_dim_diffs [OF ind \<open>c \<in> B\<close>])
+ also have "... = dim {x - c | x. x \<in> affine hull B}"
+ by (simp add: diffs_affine_hull_span \<open>c \<in> B\<close>)
+ also have "... = dim {x - a |x. x \<in> S}"
+ by (simp add: affS aff *)
+ finally show ?thesis .
+qed
+
+lemma aff_dim_linear_image_le:
+ assumes "linear f"
+ shows "aff_dim(f ` S) \<le> aff_dim S"
+proof -
+ have "aff_dim (f ` T) \<le> aff_dim T" if "affine T" for T
+ proof (cases "T = {}")
+ case True then show ?thesis by (simp add: aff_dim_geq)
+ next
+ case False
+ then obtain a where "a \<in> T" by auto
+ have 1: "((\<lambda>x. x - f a) ` f ` T) = {x - f a |x. x \<in> f ` T}"
+ by auto
+ have 2: "{x - f a| x. x \<in> f ` T} = f ` {x - a| x. x \<in> T}"
+ by (force simp: linear_sub [OF assms])
+ have "aff_dim (f ` T) = int (dim {x - f a |x. x \<in> f ` T})"
+ by (simp add: \<open>a \<in> T\<close> hull_inc aff_dim_eq_dim [of "f a"] 1)
+ also have "... = int (dim (f ` {x - a| x. x \<in> T}))"
+ by (force simp: linear_sub [OF assms] 2)
+ also have "... \<le> int (dim {x - a| x. x \<in> T})"
+ by (simp add: dim_image_le [OF assms])
+ also have "... \<le> aff_dim T"
+ by (simp add: aff_dim_dim_affine_diffs [symmetric] \<open>a \<in> T\<close> \<open>affine T\<close>)
+ finally show ?thesis .
+ qed
+ then
+ have "aff_dim (f ` (affine hull S)) \<le> aff_dim (affine hull S)"
+ using affine_affine_hull [of S] by blast
+ then show ?thesis
+ using affine_hull_linear_image assms linear_conv_bounded_linear by fastforce
+qed
+
+lemma aff_dim_injective_linear_image [simp]:
+ assumes "linear f" "inj f"
+ shows "aff_dim (f ` S) = aff_dim S"
+proof (rule antisym)
+ show "aff_dim (f ` S) \<le> aff_dim S"
+ by (simp add: aff_dim_linear_image_le assms(1))
+next
+ obtain g where "linear g" "g \<circ> f = id"
+ using linear_injective_left_inverse assms by blast
+ then have "aff_dim S \<le> aff_dim(g ` f ` S)"
+ by (simp add: image_comp)
+ also have "... \<le> aff_dim (f ` S)"
+ by (simp add: \<open>linear g\<close> aff_dim_linear_image_le)
+ finally show "aff_dim S \<le> aff_dim (f ` S)" .
+qed
+
+text\<open>Choosing a subspace of a given dimension\<close>
+proposition choose_subspace_of_subspace:
+ fixes S :: "'n::euclidean_space set"
+ assumes "n \<le> dim S"
+ obtains T where "subspace T" "T \<subseteq> span S" "dim T = n"
+proof -
+ have "\<exists>T. subspace T \<and> T \<subseteq> span S \<and> dim T = n"
+ using assms
+ proof (induction n)
+ case 0 then show ?case by force
+ next
+ case (Suc n)
+ then obtain T where "subspace T" "T \<subseteq> span S" "dim T = n"
+ by force
+ then show ?case
+ proof (cases "span S \<subseteq> span T")
+ case True
+ have "dim S = dim T"
+ apply (rule span_eq_dim [OF subset_antisym [OF True]])
+ by (simp add: \<open>T \<subseteq> span S\<close> span_minimal subspace_span)
+ then show ?thesis
+ using Suc.prems \<open>dim T = n\<close> by linarith
+ next
+ case False
+ then obtain y where y: "y \<in> S" "y \<notin> T"
+ by (meson span_mono subsetI)
+ then have "span (insert y T) \<subseteq> span S"
+ by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_inc span_mono span_span)
+ with \<open>dim T = n\<close> \<open>subspace T\<close> span_induct y show ?thesis
+ apply (rule_tac x="span(insert y T)" in exI)
+ apply (auto simp: subspace_span dim_insert)
+ done
+ qed
+ qed
+ with that show ?thesis by blast
+qed
+
+lemma choose_affine_subset:
+ assumes "affine S" "-1 \<le> d" and dle: "d \<le> aff_dim S"
+ obtains T where "affine T" "T \<subseteq> S" "aff_dim T = d"
+proof (cases "d = -1 \<or> S={}")
+ case True with assms show ?thesis
+ by (metis aff_dim_empty affine_empty bot.extremum that eq_iff)
+next
+ case False
+ with assms obtain a where "a \<in> S" "0 \<le> d" by auto
+ with assms have ss: "subspace (op + (- a) ` S)"
+ by (simp add: affine_diffs_subspace)
+ have "nat d \<le> dim (op + (- a) ` S)"
+ by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss)
+ then obtain T where "subspace T" and Tsb: "T \<subseteq> span (op + (- a) ` S)"
+ and Tdim: "dim T = nat d"
+ using choose_subspace_of_subspace [of "nat d" "op + (- a) ` S"] by blast
+ then have "affine T"
+ using subspace_affine by blast
+ then have "affine (op + a ` T)"
+ by (metis affine_hull_eq affine_hull_translation)
+ moreover have "op + a ` T \<subseteq> S"
+ proof -
+ have "T \<subseteq> op + (- a) ` S"
+ by (metis (no_types) span_eq Tsb ss)
+ then show "op + a ` T \<subseteq> S"
+ using add_ac by auto
+ qed
+ moreover have "aff_dim (op + a ` T) = d"
+ by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq)
+ ultimately show ?thesis
+ by (rule that)
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon May 23 15:33:24 2016 +0100
@@ -110,6 +110,18 @@
lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
by (meson DIM_positive Suc_leI)
+
+lemma setsum_inner_Basis_scaleR [simp]:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
+ assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
+ by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
+ assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
+
+lemma setsum_inner_Basis_eq [simp]:
+ assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
+ by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
+ assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
+
subsection \<open>Subclass relationships\<close>
instance euclidean_space \<subseteq> perfect_space
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon May 23 15:33:24 2016 +0100
@@ -223,7 +223,7 @@
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
by (metis scaleR_minus1_left subspace_mul)
-lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
+lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
using subspace_add [of S x "- y"] by (simp add: subspace_neg)
lemma (in real_vector) subspace_setsum:
@@ -434,7 +434,7 @@
by (metis subspace_neg subspace_span)
lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
- by (metis subspace_span subspace_sub)
+ by (metis subspace_span subspace_diff)
lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
by (rule subspace_setsum [OF subspace_span])
@@ -1524,6 +1524,46 @@
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
by (simp add: orthogonal_def inner_commute)
+lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
+ by (rule ext) (simp add: orthogonal_def)
+
+lemma pairwise_ortho_scaleR:
+ "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
+ \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
+ by (auto simp: pairwise_def orthogonal_clauses)
+
+lemma orthogonal_rvsum:
+ "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (setsum f s)"
+ by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
+
+lemma orthogonal_lvsum:
+ "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (setsum f s) y"
+ by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
+
+lemma norm_add_Pythagorean:
+ assumes "orthogonal a b"
+ shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
+proof -
+ from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
+ by (simp add: algebra_simps orthogonal_def inner_commute)
+ then show ?thesis
+ by (simp add: power2_norm_eq_inner)
+qed
+
+lemma norm_setsum_Pythagorean:
+ assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
+ shows "(norm (setsum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
+using assms
+proof (induction I rule: finite_induct)
+ case empty then show ?case by simp
+next
+ case (insert x I)
+ then have "orthogonal (f x) (setsum f I)"
+ by (metis pairwise_insert orthogonal_rvsum)
+ with insert show ?case
+ by (simp add: pairwise_insert norm_add_Pythagorean)
+qed
+
subsection \<open>Bilinear functions.\<close>
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon May 23 15:33:24 2016 +0100
@@ -2109,6 +2109,79 @@
by (auto simp: closure_def)
qed
+lemma connected_disjoint_Union_open_pick:
+ assumes "pairwise disjnt B"
+ "\<And>S. S \<in> A \<Longrightarrow> connected S \<and> S \<noteq> {}"
+ "\<And>S. S \<in> B \<Longrightarrow> open S"
+ "\<Union>A \<subseteq> \<Union>B"
+ "S \<in> A"
+ obtains T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
+proof -
+ have "S \<subseteq> \<Union>B" "connected S" "S \<noteq> {}"
+ using assms \<open>S \<in> A\<close> by blast+
+ then obtain T where "T \<in> B" "S \<inter> T \<noteq> {}"
+ by (metis Sup_inf_eq_bot_iff inf.absorb_iff2 inf_commute)
+ have 1: "open T" by (simp add: \<open>T \<in> B\<close> assms)
+ have 2: "open (\<Union>(B-{T}))" using assms by blast
+ have 3: "S \<subseteq> T \<union> \<Union>(B - {T})" using \<open>S \<subseteq> \<Union>B\<close> by blast
+ have "T \<inter> \<Union>(B - {T}) = {}" using \<open>T \<in> B\<close> \<open>pairwise disjnt B\<close>
+ by (auto simp: pairwise_def disjnt_def)
+ then have 4: "T \<inter> \<Union>(B - {T}) \<inter> S = {}" by auto
+ from connectedD [OF \<open>connected S\<close> 1 2 3 4]
+ have "S \<inter> \<Union>(B-{T}) = {}"
+ by (auto simp: Int_commute \<open>S \<inter> T \<noteq> {}\<close>)
+ with \<open>T \<in> B\<close> have "S \<subseteq> T"
+ using "3" by auto
+ show ?thesis
+ using \<open>S \<inter> \<Union>(B - {T}) = {}\<close> \<open>S \<subseteq> T\<close> \<open>T \<in> B\<close> that by auto
+qed
+
+lemma connected_disjoint_Union_open_subset:
+ assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
+ and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+ and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+ and eq [simp]: "\<Union>A = \<Union>B"
+ shows "A \<subseteq> B"
+proof
+ fix S
+ assume "S \<in> A"
+ obtain T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
+ apply (rule connected_disjoint_Union_open_pick [OF B, of A])
+ using SA SB \<open>S \<in> A\<close> by auto
+ moreover obtain S' where "S' \<in> A" "T \<subseteq> S'" "T \<inter> \<Union>(A - {S'}) = {}"
+ apply (rule connected_disjoint_Union_open_pick [OF A, of B])
+ using SA SB \<open>T \<in> B\<close> by auto
+ ultimately have "S' = S"
+ by (metis A Int_subset_iff SA \<open>S \<in> A\<close> disjnt_def inf.orderE pairwise_def)
+ with \<open>T \<subseteq> S'\<close> have "T \<subseteq> S" by simp
+ with \<open>S \<subseteq> T\<close> have "S = T" by blast
+ with \<open>T \<in> B\<close> show "S \<in> B" by simp
+qed
+
+lemma connected_disjoint_Union_open_unique:
+ assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
+ and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+ and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+ and eq [simp]: "\<Union>A = \<Union>B"
+ shows "A = B"
+by (rule subset_antisym; metis connected_disjoint_Union_open_subset assms)
+
+proposition components_open_unique:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "pairwise disjnt A" "\<Union>A = S"
+ "\<And>X. X \<in> A \<Longrightarrow> open X \<and> connected X \<and> X \<noteq> {}"
+ shows "components S = A"
+proof -
+ have "open S" using assms by blast
+ show ?thesis
+ apply (rule connected_disjoint_Union_open_unique)
+ apply (simp add: components_eq disjnt_def pairwise_def)
+ using \<open>open S\<close>
+ apply (simp_all add: assms open_components in_components_connected in_components_nonempty)
+ done
+qed
+
+
subsection\<open>Existence of unbounded components\<close>
lemma cobounded_unbounded_component:
@@ -3742,14 +3815,13 @@
lemma homotopic_paths_linear:
fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
- "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
+ "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
shows "homotopic_paths s g h"
using assms
unfolding path_def
apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
- apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
- apply (intro conjI subsetI continuous_intros)
- apply (fastforce intro: continuous_intros continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])+
+ apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R (g o snd) y + (fst y) *\<^sub>R (h o snd) y)" in exI)
+ apply (intro conjI subsetI continuous_intros; force)
done
lemma homotopic_loops_linear:
@@ -5052,6 +5124,346 @@
apply (force simp: convex_Int convex_imp_path_connected)
done
+subsection\<open>Components, continuity, openin, closedin\<close>
+
+lemma continuous_openin_preimage_eq:
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply (auto simp: continuous_openin_preimage)
+apply (fastforce simp add: continuous_on_open openin_open)
+done
+
+lemma continuous_closedin_preimage_eq:
+ "continuous_on S f \<longleftrightarrow>
+ (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_closedin_preimage)
+apply (fastforce simp add: continuous_on_closed closedin_closed)
+done
+
+lemma continuous_on_components_gen:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "\<And>c. c \<in> components S \<Longrightarrow>
+ openin (subtopology euclidean S) c \<and> continuous_on c f"
+ shows "continuous_on S f"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+ fix t :: "'b set"
+ assume "open t"
+ have "{x. x \<in> S \<and> f x \<in> t} = \<Union>{{x. x \<in> c \<and> f x \<in> t} |c. c \<in> components S}"
+ apply auto
+ apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
+ using Union_components by blast
+ then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
+ using \<open>open t\<close> assms
+ by (fastforce intro: openin_trans continuous_openin_preimage)
+qed
+
+lemma continuous_on_components:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ assumes "locally connected S "
+ "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
+ shows "continuous_on S f"
+apply (rule continuous_on_components_gen)
+apply (auto simp: assms intro: openin_components_locally_connected)
+done
+
+lemma continuous_on_components_eq:
+ "locally connected S
+ \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
+by (meson continuous_on_components continuous_on_subset in_components_subset)
+
+lemma continuous_on_components_open:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S "
+ "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
+ shows "continuous_on S f"
+using continuous_on_components open_imp_locally_connected assms by blast
+
+lemma continuous_on_components_open_eq:
+ fixes S :: "'a::real_normed_vector set"
+ shows "open S \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
+using continuous_on_subset in_components_subset
+by (blast intro: continuous_on_components_open)
+
+lemma closedin_union_complement_components:
+ assumes u: "locally connected u"
+ and S: "closedin (subtopology euclidean u) S"
+ and cuS: "c \<subseteq> components(u - S)"
+ shows "closedin (subtopology euclidean u) (S \<union> \<Union>c)"
+proof -
+ have di: "(\<And>S t. S \<in> c \<and> t \<in> c' \<Longrightarrow> disjnt S t) \<Longrightarrow> disjnt (\<Union> c) (\<Union> c')" for c'
+ by (simp add: disjnt_def) blast
+ have "S \<subseteq> u"
+ using S closedin_imp_subset by blast
+ moreover have "u - S = \<Union>c \<union> \<Union>(components (u - S) - c)"
+ by (metis Diff_partition Topology_Euclidean_Space.Union_components Union_Un_distrib assms(3))
+ moreover have "disjnt (\<Union>c) (\<Union>(components (u - S) - c))"
+ apply (rule di)
+ by (metis DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE)
+ ultimately have eq: "S \<union> \<Union>c = u - (\<Union>(components(u - S) - c))"
+ by (auto simp: disjnt_def)
+ have *: "openin (subtopology euclidean u) (\<Union>(components (u - S) - c))"
+ apply (rule openin_Union)
+ apply (rule openin_trans [of "u - S"])
+ apply (simp add: u S locally_diff_closed openin_components_locally_connected)
+ apply (simp add: openin_diff S)
+ done
+ have "openin (subtopology euclidean u) (u - (u - \<Union>(components (u - S) - c)))"
+ apply (rule openin_diff, simp)
+ apply (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *)
+ done
+ then show ?thesis
+ by (force simp: eq closedin_def)
+qed
+
+lemma closed_union_complement_components:
+ fixes S :: "'a::real_normed_vector set"
+ assumes S: "closed S" and c: "c \<subseteq> components(- S)"
+ shows "closed(S \<union> \<Union> c)"
+proof -
+ have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
+ apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
+ using S apply (simp add: closed_closedin)
+ using c apply (simp add: Compl_eq_Diff_UNIV)
+ done
+ then show ?thesis
+ by (simp add: closed_closedin)
+qed
+
+lemma closedin_Un_complement_component:
+ fixes S :: "'a::real_normed_vector set"
+ assumes u: "locally connected u"
+ and S: "closedin (subtopology euclidean u) S"
+ and c: " c \<in> components(u - S)"
+ shows "closedin (subtopology euclidean u) (S \<union> c)"
+proof -
+ have "closedin (subtopology euclidean u) (S \<union> \<Union>{c})"
+ using c by (blast intro: closedin_union_complement_components [OF u S])
+ then show ?thesis
+ by simp
+qed
+
+lemma closed_Un_complement_component:
+ fixes S :: "'a::real_normed_vector set"
+ assumes S: "closed S" and c: " c \<in> components(-S)"
+ shows "closed (S \<union> c)"
+by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
+
+
+subsection\<open>Existence of isometry between subspaces of same dimension\<close>
+
+thm subspace_isomorphism
+lemma isometry_subset_subspace:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes S: "subspace S"
+ and T: "subspace T"
+ and d: "dim S \<le> dim T"
+ obtains f where "linear f" "f ` S \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+proof -
+ obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
+ and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+ and "independent B" "finite B" "card B = dim S" "span B = S"
+ by (metis orthonormal_basis_subspace [OF S] independent_finite)
+ obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
+ and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
+ and "independent C" "finite C" "card C = dim T" "span C = T"
+ by (metis orthonormal_basis_subspace [OF T] independent_finite)
+ obtain fb where "fb ` B \<subseteq> C" "inj_on fb B"
+ by (metis \<open>card B = dim S\<close> \<open>card C = dim T\<close> \<open>finite B\<close> \<open>finite C\<close> card_le_inj d)
+ then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
+ using Corth
+ apply (auto simp: pairwise_def orthogonal_clauses)
+ by (meson subsetD image_eqI inj_on_def)
+ obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
+ using linear_independent_extend \<open>independent B\<close> by fastforce
+ have "f ` S \<subseteq> T"
+ by (metis ffb \<open>fb ` B \<subseteq> C\<close> \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image span_mono)
+ have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
+ using B1 C1 \<open>fb ` B \<subseteq> C\<close> by auto
+ have "norm (f x) = norm x" if "x \<in> S" for x
+ proof -
+ obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
+ using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
+ have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
+ using linear_setsum [OF \<open>linear f\<close>] x by auto
+ also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
+ using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+ also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
+ by (simp add: ffb cong: setsum.cong)
+ finally have "norm (f x)^2 = norm (\<Sum>v\<in>B. a v *\<^sub>R fb v)^2" by simp
+ also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+ apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+ apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
+ done
+ also have "... = norm x ^2"
+ by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+ finally show ?thesis
+ by (simp add: norm_eq_sqrt_inner)
+ qed
+ then show ?thesis
+ by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
+qed
+
+proposition isometries_subspaces:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes S: "subspace S"
+ and T: "subspace T"
+ and d: "dim S = dim T"
+ obtains f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
+ "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+ "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
+ "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
+proof -
+ obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
+ and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+ and "independent B" "finite B" "card B = dim S" "span B = S"
+ by (metis orthonormal_basis_subspace [OF S] independent_finite)
+ obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
+ and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
+ and "independent C" "finite C" "card C = dim T" "span C = T"
+ by (metis orthonormal_basis_subspace [OF T] independent_finite)
+ obtain fb where "bij_betw fb B C"
+ by (metis \<open>finite B\<close> \<open>finite C\<close> bij_betw_iff_card \<open>card B = dim S\<close> \<open>card C = dim T\<close> d)
+ then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
+ using Corth
+ apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
+ by (meson subsetD image_eqI inj_on_def)
+ obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
+ using linear_independent_extend \<open>independent B\<close> by fastforce
+ define gb where "gb \<equiv> inv_into B fb"
+ then have pairwise_orth_gb: "pairwise (\<lambda>v j. orthogonal (gb v) (gb j)) C"
+ using Borth
+ apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
+ by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on bij_betw_inv_into_right inv_into_into)
+ obtain g where "linear g" and ggb: "\<And>x. x \<in> C \<Longrightarrow> g x = gb x"
+ using linear_independent_extend \<open>independent C\<close> by fastforce
+ have "f ` S \<subseteq> T"
+ by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on eq_iff ffb \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image)
+ have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
+ using B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on by fastforce
+ have f [simp]: "norm (f x) = norm x" "g (f x) = x" if "x \<in> S" for x
+ proof -
+ obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
+ using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
+ have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
+ using linear_setsum [OF \<open>linear f\<close>] x by auto
+ also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
+ using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+ also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
+ by (simp add: ffb cong: setsum.cong)
+ finally have *: "f x = (\<Sum>v\<in>B. a v *\<^sub>R fb v)" .
+ then have "(norm (f x))\<^sup>2 = (norm (\<Sum>v\<in>B. a v *\<^sub>R fb v))\<^sup>2" by simp
+ also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+ apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+ apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
+ done
+ also have "... = (norm x)\<^sup>2"
+ by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+ finally show "norm (f x) = norm x"
+ by (simp add: norm_eq_sqrt_inner)
+ have "g (f x) = g (\<Sum>v\<in>B. a v *\<^sub>R fb v)" by (simp add: *)
+ also have "... = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
+ using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
+ also have "... = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
+ by (simp add: \<open>linear g\<close> linear.scaleR)
+ also have "... = (\<Sum>v\<in>B. a v *\<^sub>R v)"
+ apply (rule setsum.cong [OF refl])
+ using \<open>bij_betw fb B C\<close> gb_def bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
+ also have "... = x"
+ using x by blast
+ finally show "g (f x) = x" .
+ qed
+ have [simp]: "\<And>x. x \<in> C \<Longrightarrow> norm (gb x) = norm x"
+ by (metis B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on gb_def inv_into_into)
+ have g [simp]: "f (g x) = x" if "x \<in> T" for x
+ proof -
+ obtain a where x: "x = (\<Sum>v \<in> C. a v *\<^sub>R v)"
+ using \<open>finite C\<close> \<open>span C = T\<close> \<open>x \<in> T\<close> span_finite by fastforce
+ have "g x = (\<Sum>v \<in> C. g (a v *\<^sub>R v))"
+ using linear_setsum [OF \<open>linear g\<close>] x by auto
+ also have "... = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
+ using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
+ also have "... = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
+ by (simp add: ggb cong: setsum.cong)
+ finally have "f (g x) = f (\<Sum>v\<in>C. a v *\<^sub>R gb v)" by simp
+ also have "... = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
+ using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+ also have "... = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
+ by (simp add: \<open>linear f\<close> linear.scaleR)
+ also have "... = (\<Sum>v\<in>C. a v *\<^sub>R v)"
+ using \<open>bij_betw fb B C\<close>
+ by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
+ also have "... = x"
+ using x by blast
+ finally show "f (g x) = x" .
+ qed
+ have gim: "g ` T = S"
+ by (metis (no_types, lifting) \<open>f ` S \<subseteq> T\<close> \<open>linear g\<close> \<open>span B = S\<close> \<open>span C = T\<close> d dim_eq_span dim_image_le f(2) image_subset_iff span_linear_image span_span subsetI)
+ have fim: "f ` S = T"
+ using \<open>g ` T = S\<close> image_iff by fastforce
+ have [simp]: "norm (g x) = norm x" if "x \<in> T" for x
+ using fim that by auto
+ show ?thesis
+ apply (rule that [OF \<open>linear f\<close> \<open>linear g\<close>])
+ apply (simp_all add: fim gim)
+ done
+qed
+
+(*REPLACE*)
+lemma isometry_subspaces:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes S: "subspace S"
+ and T: "subspace T"
+ and d: "dim S = dim T"
+ obtains f where "linear f" "f ` S = T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+using isometries_subspaces [OF assms]
+by metis
+
+lemma homeomorphic_subspaces:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes S: "subspace S"
+ and T: "subspace T"
+ and d: "dim S = dim T"
+ shows "S homeomorphic T"
+proof -
+ obtain f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
+ "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
+ by (blast intro: isometries_subspaces [OF assms])
+ then show ?thesis
+ apply (simp add: homeomorphic_def homeomorphism_def)
+ apply (rule_tac x=f in exI)
+ apply (rule_tac x=g in exI)
+ apply (auto simp: linear_continuous_on linear_conv_bounded_linear)
+ done
+qed
+
+lemma homeomorphic_affine_sets:
+ assumes "affine S" "affine T" "aff_dim S = aff_dim T"
+ shows "S homeomorphic T"
+proof (cases "S = {} \<or> T = {}")
+ case True with assms aff_dim_empty homeomorphic_empty show ?thesis
+ by metis
+next
+ case False
+ then obtain a b where ab: "a \<in> S" "b \<in> T" by auto
+ then have ss: "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+ using affine_diffs_subspace assms by blast+
+ have dd: "dim (op + (- a) ` S) = dim (op + (- b) ` T)"
+ using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def)
+ have "S homeomorphic (op + (- a) ` S)"
+ by (simp add: homeomorphic_translation)
+ also have "... homeomorphic (op + (- b) ` T)"
+ by (rule homeomorphic_subspaces [OF ss dd])
+ also have "... homeomorphic T"
+ using homeomorphic_sym homeomorphic_translation by auto
+ finally show ?thesis .
+qed
+
subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
locale Retracts =
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon May 23 15:33:24 2016 +0100
@@ -861,6 +861,11 @@
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
by (simp add: dist_norm)
+lemma mem_sphere_0 [simp]:
+ fixes x :: "'a::real_normed_vector"
+ shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
+ by (simp add: dist_norm)
+
lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
by simp
@@ -986,6 +991,22 @@
abbreviation One :: "'a::euclidean_space"
where "One \<equiv> \<Sum>Basis"
+lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
+proof -
+ have "dependent (Basis :: 'a set)"
+ apply (simp add: dependent_finite)
+ apply (rule_tac x="\<lambda>i. 1" in exI)
+ using SOME_Basis apply (auto simp: assms)
+ done
+ with independent_Basis show False by force
+qed
+
+corollary One_neq_0[iff]: "One \<noteq> 0"
+ by (metis One_non_0)
+
+corollary Zero_neq_One[iff]: "0 \<noteq> One"
+ by (metis One_non_0)
+
definition (in euclidean_space) eucl_less (infix "<e" 50)
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
@@ -5788,7 +5809,7 @@
unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
-text \<open>Half-global and completely global cases.\<close>
+subsection \<open>Half-global and completely global cases.\<close>
lemma continuous_openin_preimage:
assumes "continuous_on s f" "open t"
@@ -5874,7 +5895,7 @@
with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
qed
-text \<open>Equality of continuous functions on closure and related results.\<close>
+subsection \<open>Equality of continuous functions on closure and related results.\<close>
lemma continuous_closedin_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -7238,6 +7259,11 @@
shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
by auto
+lemma translation_Int:
+ fixes a :: "'a::ab_group_add"
+ shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
+ by auto
+
lemma closure_translation:
fixes a :: "'a::real_normed_vector"
shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
@@ -7261,6 +7287,30 @@
unfolding frontier_def translation_diff interior_translation closure_translation
by auto
+lemma sphere_translation:
+ fixes a :: "'n::euclidean_space"
+ shows "sphere (a+c) r = op+a ` sphere c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma cball_translation:
+ fixes a :: "'n::euclidean_space"
+ shows "cball (a+c) r = op+a ` cball c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma ball_translation:
+ fixes a :: "'n::euclidean_space"
+ shows "ball (a+c) r = op+a ` ball c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
subsection \<open>Separation between points and sets\<close>
@@ -8211,6 +8261,37 @@
apply auto
done
+lemma homeomorphicI [intro?]:
+ "\<lbrakk>f ` S = T; g ` T = S;
+ continuous_on S f; continuous_on T g;
+ \<And>x. x \<in> S \<Longrightarrow> g(f(x)) = x;
+ \<And>y. y \<in> T \<Longrightarrow> f(g(y)) = y\<rbrakk> \<Longrightarrow> S homeomorphic T"
+unfolding homeomorphic_def homeomorphism_def by metis
+
+lemma homeomorphism_of_subsets:
+ "\<lbrakk>homeomorphism S T f g; S' \<subseteq> S; T'' \<subseteq> T; f ` S' = T'\<rbrakk>
+ \<Longrightarrow> homeomorphism S' T' f g"
+apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+by (metis contra_subsetD imageI)
+
+lemma homeomorphism_apply1: "\<lbrakk>homeomorphism S T f g; x \<in> S\<rbrakk> \<Longrightarrow> g(f x) = x"
+ by (simp add: homeomorphism_def)
+
+lemma homeomorphism_apply2: "\<lbrakk>homeomorphism S T f g; x \<in> T\<rbrakk> \<Longrightarrow> f(g x) = x"
+ by (simp add: homeomorphism_def)
+
+lemma homeomorphism_image1: "homeomorphism S T f g \<Longrightarrow> f ` S = T"
+ by (simp add: homeomorphism_def)
+
+lemma homeomorphism_image2: "homeomorphism S T f g \<Longrightarrow> g ` T = S"
+ by (simp add: homeomorphism_def)
+
+lemma homeomorphism_cont1: "homeomorphism S T f g \<Longrightarrow> continuous_on S f"
+ by (simp add: homeomorphism_def)
+
+lemma homeomorphism_cont2: "homeomorphism S T f g \<Longrightarrow> continuous_on T g"
+ by (simp add: homeomorphism_def)
+
text \<open>Relatively weak hypotheses if a set is compact.\<close>
lemma homeomorphism_compact:
@@ -8332,7 +8413,109 @@
done
qed
-text\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
+subsection\<open>Inverse function property for open/closed maps\<close>
+
+lemma continuous_on_inverse_open_map:
+ assumes contf: "continuous_on S f"
+ and imf: "f ` S = T"
+ and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ and oo: "\<And>U. openin (subtopology euclidean S) U
+ \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+ shows "continuous_on T g"
+proof -
+ have gTS: "g ` T = S"
+ using imf injf by force
+ have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+ using imf injf by force
+ show ?thesis
+ apply (simp add: continuous_on_open [of T g] gTS)
+ apply (metis openin_imp_subset fU oo)
+ done
+qed
+
+lemma continuous_on_inverse_closed_map:
+ assumes contf: "continuous_on S f"
+ and imf: "f ` S = T"
+ and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ and oo: "\<And>U. closedin (subtopology euclidean S) U
+ \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+ shows "continuous_on T g"
+proof -
+ have gTS: "g ` T = S"
+ using imf injf by force
+ have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+ using imf injf by force
+ show ?thesis
+ apply (simp add: continuous_on_closed [of T g] gTS)
+ apply (metis closedin_imp_subset fU oo)
+ done
+qed
+
+lemma homeomorphism_injective_open_map:
+ assumes contf: "continuous_on S f"
+ and imf: "f ` S = T"
+ and injf: "inj_on f S"
+ and oo: "\<And>U. openin (subtopology euclidean S) U
+ \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+ obtains g where "homeomorphism S T f g"
+proof -
+ have "continuous_on T (inv_into S f)"
+ by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
+ then show ?thesis
+ apply (rule_tac g = "inv_into S f" in that)
+ using imf injf contf apply (auto simp: homeomorphism_def)
+ done
+qed
+
+lemma homeomorphism_injective_closed_map:
+ assumes contf: "continuous_on S f"
+ and imf: "f ` S = T"
+ and injf: "inj_on f S"
+ and oo: "\<And>U. closedin (subtopology euclidean S) U
+ \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+ obtains g where "homeomorphism S T f g"
+proof -
+ have "continuous_on T (inv_into S f)"
+ by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
+ then show ?thesis
+ apply (rule_tac g = "inv_into S f" in that)
+ using imf injf contf apply (auto simp: homeomorphism_def)
+ done
+qed
+
+lemma homeomorphism_imp_open_map:
+ assumes hom: "homeomorphism S T f g"
+ and oo: "openin (subtopology euclidean S) U"
+ shows "openin (subtopology euclidean T) (f ` U)"
+proof -
+ have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+ using assms openin_subset
+ by (fastforce simp: homeomorphism_def rev_image_eqI)
+ have "continuous_on T g"
+ using hom homeomorphism_def by blast
+ moreover have "g ` T = S"
+ by (metis hom homeomorphism_def)
+ ultimately show ?thesis
+ by (simp add: continuous_on_open oo)
+qed
+
+lemma homeomorphism_imp_closed_map:
+ assumes hom: "homeomorphism S T f g"
+ and oo: "closedin (subtopology euclidean S) U"
+ shows "closedin (subtopology euclidean T) (f ` U)"
+proof -
+ have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+ using assms closedin_subset
+ by (fastforce simp: homeomorphism_def rev_image_eqI)
+ have "continuous_on T g"
+ using hom homeomorphism_def by blast
+ moreover have "g ` T = S"
+ by (metis hom homeomorphism_def)
+ ultimately show ?thesis
+ by (simp add: continuous_on_closed oo)
+qed
+
+subsection\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
lemma cauchy_isometric:
assumes e: "e > 0"
@@ -8354,7 +8537,7 @@
fix n
assume "n\<ge>N"
have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
- using subspace_sub[OF s, of "x n" "x N"]
+ using subspace_diff[OF s, of "x n" "x N"]
using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
using normf[THEN bspec[where x="x n - x N"]]
by auto
--- a/src/HOL/Real_Vector_Spaces.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Mon May 23 15:33:24 2016 +0100
@@ -236,6 +236,18 @@
apply (simp_all add: algebra_simps)
done
+lemma vector_add_divide_simps :
+ fixes v :: "'a :: real_vector"
+ shows "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
+ "a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
+ "(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)"
+ "(a / z) *\<^sub>R v + b *\<^sub>R w = (if z = 0 then b *\<^sub>R w else (a *\<^sub>R v + (b * z) *\<^sub>R w) /\<^sub>R z)"
+ "v - (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
+ "a *\<^sub>R v - (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
+ "(a / z) *\<^sub>R v - w = (if z = 0 then -w else (a *\<^sub>R v - z *\<^sub>R w) /\<^sub>R z)"
+ "(a / z) *\<^sub>R v - b *\<^sub>R w = (if z = 0 then -b *\<^sub>R w else (a *\<^sub>R v - (b * z) *\<^sub>R w) /\<^sub>R z)"
+by (simp_all add: divide_inverse_commute scaleR_add_right real_vector.scale_right_diff_distrib)
+
lemma real_vector_affinity_eq:
fixes x :: "'a :: real_vector"
assumes m0: "m \<noteq> 0"
@@ -769,6 +781,21 @@
by (rule norm_minus_cancel)
thus ?thesis by simp
qed
+
+lemma dist_add_cancel [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "dist (a + b) (a + c) = dist b c"
+by (simp add: dist_norm)
+
+lemma dist_add_cancel2 [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "dist (b + a) (c + a) = dist b c"
+by (simp add: dist_norm)
+
+lemma dist_scaleR [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "dist (x *\<^sub>R a) (y *\<^sub>R a) = abs (x-y) * norm a"
+by (metis dist_norm norm_scaleR scaleR_left.diff)
lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
--- a/src/HOL/Set.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Set.thy Mon May 23 15:33:24 2016 +0100
@@ -1934,6 +1934,14 @@
lemma pairwise_singleton [simp]: "pairwise P {A}"
by (simp add: pairwise_def)
+lemma pairwise_insert:
+ "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
+by (force simp: pairwise_def)
+
+lemma pairwise_image:
+ "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
+by (force simp: pairwise_def)
+
lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
by blast
--- a/src/HOL/Set_Interval.thy Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Set_Interval.thy Mon May 23 15:33:24 2016 +0100
@@ -1168,19 +1168,18 @@
by (rule finite_same_card_bij) auto
lemma bij_betw_iff_card:
- assumes FIN: "finite A" and FIN': "finite B"
- shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
-using assms
-proof(auto simp add: bij_betw_same_card)
- assume *: "card A = card B"
- obtain f where "bij_betw f A {0 ..< card A}"
- using FIN ex_bij_betw_finite_nat by blast
+ assumes "finite A" "finite B"
+ shows "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
+proof
+ assume "card A = card B"
+ moreover obtain f where "bij_betw f A {0 ..< card A}"
+ using assms ex_bij_betw_finite_nat by blast
moreover obtain g where "bij_betw g {0 ..< card B} B"
- using FIN' ex_bij_betw_nat_finite by blast
+ using assms ex_bij_betw_nat_finite by blast
ultimately have "bij_betw (g o f) A B"
- using * by (auto simp add: bij_betw_trans)
+ by (auto simp: bij_betw_trans)
thus "(\<exists>f. bij_betw f A B)" by blast
-qed
+qed (auto simp: bij_betw_same_card)
lemma inj_on_iff_card_le:
assumes FIN: "finite A" and FIN': "finite B"