--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu May 03 16:17:44 2018 +0200
@@ -212,7 +212,7 @@
finally show ?thesis .
qed
-lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "real^'n^'m"
+lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
using matrix_vector_mul_linear[of A]
by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
@@ -416,128 +416,6 @@
lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
unfolding inner_simps scalar_mult_eq_scaleR by auto
-lemma matrix_left_invertible_injective:
- fixes A :: "'a::field^'n^'m"
- shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
-proof safe
- fix B
- assume B: "B ** A = mat 1"
- show "inj (( *v) A)"
- unfolding inj_on_def
- by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
-next
- assume "inj (( *v) A)"
- from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
- obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
- by blast
- have "matrix g ** A = mat 1"
- by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
- matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
- then show "\<exists>B. B ** A = mat 1"
- by metis
-qed
-
-lemma matrix_right_invertible_surjective:
- "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
-proof -
- { fix B :: "'a ^'m^'n"
- assume AB: "A ** B = mat 1"
- { fix x :: "'a ^ 'm"
- have "A *v (B *v x) = x"
- by (simp add: matrix_vector_mul_assoc AB) }
- hence "surj (( *v) A)" unfolding surj_def by metis }
- moreover
- { assume sf: "surj (( *v) A)"
- from vec.linear_surjective_right_inverse[OF _ this]
- obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
- by blast
-
- have "A ** (matrix g) = mat 1"
- unfolding matrix_eq matrix_vector_mul_lid
- matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
- using g(2) unfolding o_def fun_eq_iff id_def
- .
- hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
- }
- ultimately show ?thesis unfolding surj_def by blast
-qed
-
-lemma matrix_right_invertible_span_columns:
- "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
- vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
-proof -
- let ?U = "UNIV :: 'm set"
- have fU: "finite ?U" by simp
- have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
- unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
- by (simp add: eq_commute)
- have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
- { assume h: ?lhs
- { fix x:: "'a ^'n"
- from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
- where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
- have "x \<in> vec.span (columns A)"
- unfolding y[symmetric] scalar_mult_eq_scaleR
- proof (rule span_sum [OF span_mul])
- show "column i A \<in> span (columns A)" for i
- using columns_def span_inc by auto
- qed
- }
- then have ?rhs unfolding rhseq by blast }
- moreover
- { assume h:?rhs
- let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
- { fix y
- have "y \<in> vec.span (columns A)"
- unfolding h by blast
- then have "?P y"
- proof (induction rule: vec.span_induct_alt)
- case base
- then show ?case
- by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
- next
- case (step c y1 y2)
- then obtain i where i: "i \<in> ?U" "y1 = column i A"
- from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
- unfolding columns_def by blast
- obtain x:: "real ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
- using step by blast
- let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
- show ?case
- proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
- fix j
- have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
- else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
- using i(1) by (simp add: field_simps)
- have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
- else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
- by (rule sum.cong[OF refl]) (use th in blast)
- also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
- by (simp add: sum.distrib)
- also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
- unfolding sum.delta[OF fU]
- using i(1) by simp
- finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
- else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
- qed
- qed
- }
- then have ?lhs unfolding lhseq ..
- }
- ultimately show ?thesis by blast
-qed
-
-lemma matrix_left_invertible_span_rows_gen:
- "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
- unfolding right_invertible_transpose[symmetric]
- unfolding columns_transpose[symmetric]
- unfolding matrix_right_invertible_span_columns
- ..
-
-lemma matrix_left_invertible_span_rows:
- "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
- using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
-
text \<open>The same result in terms of square matrices.\<close>
@@ -1100,7 +978,7 @@
proof -
obtain B where "independent B" "span(rows A) \<subseteq> span B"
and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
- using basis_exists [of "span(rows A)"] by blast
+ using basis_exists [of "span(rows A)"] by metis
with span_subspace have eq: "span B = span(rows A)"
by auto
then have inj: "inj_on (( *v) A) (span B)"
--- a/src/HOL/Analysis/Cartesian_Space.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy Thu May 03 16:17:44 2018 +0200
@@ -97,6 +97,14 @@
by unfold_locales
(vector matrix_vector_mult_def sum.distrib algebra_simps)+
+lemma span_vec_eq: "vec.span X = span X"
+ and dim_vec_eq: "vec.dim X = dim X"
+ and dependent_vec_eq: "vec.dependent X = dependent X"
+ and subspace_vec_eq: "vec.subspace X = subspace X"
+ for X::"(real^'n) set"
+ unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
+ by (auto simp: scalar_mult_eq_scaleR)
+
lemma linear_componentwise:
fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
@@ -143,24 +151,44 @@
using matrix_compose_gen[of f g] assms
by (simp add: linear_def scalar_mult_eq_scaleR)
+lemma left_invertible_transpose:
+ "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
+ by (metis matrix_transpose_mul transpose_mat transpose_transpose)
+
+lemma right_invertible_transpose:
+ "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
+ by (metis matrix_transpose_mul transpose_mat transpose_transpose)
+
+lemma linear_matrix_vector_mul_eq:
+ "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
+ by (simp add: scalar_mult_eq_scaleR linear_def)
+
+lemma matrix_vector_mul[simp]:
+ "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
+ "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
+ "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
+ for f :: "real^'n \<Rightarrow> real ^'m"
+ by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
+
lemma matrix_left_invertible_injective:
- "(\<exists>B. (B::'a::field^'m^'n) ** (A::'a::field^'n^'m) = mat 1)
- \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
-proof -
- { fix B:: "'a^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
- from xy have "B*v (A *v x) = B *v (A*v y)" by simp
- hence "x = y"
- unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . }
- moreover
- { assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
- hence i: "inj (( *v) A)" unfolding inj_on_def by auto
- from vec.linear_exists_left_inverse_on[OF matrix_vector_mul_linear_gen vec.subspace_UNIV i]
- obtain g where g: "Vector_Spaces.linear ( *s) ( *s) g" "g o (( *v) A) = id" by (auto simp: id_def module_hom_iff_linear o_def)
- have "matrix g ** A = mat 1"
- unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
- using g(2) by (metis comp_apply id_apply)
- then have "\<exists>B. (B::'a::{field}^'m^'n) ** A = mat 1" by blast }
- ultimately show ?thesis by blast
+ fixes A :: "'a::field^'n^'m"
+ shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
+proof safe
+ fix B
+ assume B: "B ** A = mat 1"
+ show "inj (( *v) A)"
+ unfolding inj_on_def
+ by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
+next
+ assume "inj (( *v) A)"
+ from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
+ obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
+ by blast
+ have "matrix g ** A = mat 1"
+ by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
+ matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
+ then show "\<exists>B. B ** A = mat 1"
+ by metis
qed
lemma matrix_left_invertible_ker:
@@ -169,6 +197,31 @@
using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
by (simp add: inj_on_def)
+lemma matrix_right_invertible_surjective:
+ "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
+proof -
+ { fix B :: "'a ^'m^'n"
+ assume AB: "A ** B = mat 1"
+ { fix x :: "'a ^ 'm"
+ have "A *v (B *v x) = x"
+ by (simp add: matrix_vector_mul_assoc AB) }
+ hence "surj (( *v) A)" unfolding surj_def by metis }
+ moreover
+ { assume sf: "surj (( *v) A)"
+ from vec.linear_surjective_right_inverse[OF _ this]
+ obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
+ by blast
+
+ have "A ** (matrix g) = mat 1"
+ unfolding matrix_eq matrix_vector_mul_lid
+ matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
+ using g(2) unfolding o_def fun_eq_iff id_def
+ .
+ hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
+ }
+ ultimately show ?thesis unfolding surj_def by blast
+qed
+
lemma matrix_left_invertible_independent_columns:
fixes A :: "'a::{field}^'n^'m"
shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
@@ -196,14 +249,6 @@
ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
qed
-lemma left_invertible_transpose:
- "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
- by (metis matrix_transpose_mul transpose_mat transpose_transpose)
-
-lemma right_invertible_transpose:
- "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
- by (metis matrix_transpose_mul transpose_mat transpose_transpose)
-
lemma matrix_right_invertible_independent_rows:
fixes A :: "'a::{field}^'n^'m"
shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
@@ -212,6 +257,81 @@
matrix_left_invertible_independent_columns
by (simp add:)
+lemma matrix_right_invertible_span_columns:
+ "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
+ vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
+proof -
+ let ?U = "UNIV :: 'm set"
+ have fU: "finite ?U" by simp
+ have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
+ unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
+ by (simp add: eq_commute)
+ have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
+ { assume h: ?lhs
+ { fix x:: "'a ^'n"
+ from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
+ where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
+ have "x \<in> vec.span (columns A)"
+ unfolding y[symmetric] scalar_mult_eq_scaleR
+ proof (rule vec.span_sum [OF vec.span_scale])
+ show "column i A \<in> vec.span (columns A)" for i
+ using columns_def vec.span_superset by auto
+ qed
+ }
+ then have ?rhs unfolding rhseq by blast }
+ moreover
+ { assume h:?rhs
+ let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
+ { fix y
+ have "y \<in> vec.span (columns A)"
+ unfolding h by blast
+ then have "?P y"
+ proof (induction rule: vec.span_induct_alt)
+ case base
+ then show ?case
+ by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
+ next
+ case (step c y1 y2)
+ from step obtain i where i: "i \<in> ?U" "y1 = column i A"
+ unfolding columns_def by blast
+ obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
+ using step by blast
+ let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
+ show ?case
+ proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
+ fix j
+ have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
+ else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
+ using i(1) by (simp add: field_simps)
+ have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
+ else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
+ by (rule sum.cong[OF refl]) (use th in blast)
+ also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
+ by (simp add: sum.distrib)
+ also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
+ unfolding sum.delta[OF fU]
+ using i(1) by simp
+ finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
+ else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
+ qed
+ qed
+ }
+ then have ?lhs unfolding lhseq ..
+ }
+ ultimately show ?thesis by blast
+qed
+
+lemma matrix_left_invertible_span_rows_gen:
+ "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
+ unfolding right_invertible_transpose[symmetric]
+ unfolding columns_transpose[symmetric]
+ unfolding matrix_right_invertible_span_columns
+ ..
+
+lemma matrix_left_invertible_span_rows:
+ "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
+ using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
+
lemma matrix_left_right_inverse:
fixes A A' :: "'a::{field}^'n^'n"
shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
@@ -339,23 +459,4 @@
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
unfolding vector_space_over_itself.dimension_def by simp
-lemma linear_matrix_vector_mul_eq:
- "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
- by (simp add: scalar_mult_eq_scaleR linear_def)
-
-lemma matrix_vector_mul[simp]:
- "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
- "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
- "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
- for f :: "real^'n \<Rightarrow> real ^'m"
- by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
-
-lemma span_vec_eq: "vec.span X = span X"
- and dim_vec_eq: "vec.dim X = dim X"
- and dependent_vec_eq: "vec.dependent X = dependent X"
- and subspace_vec_eq: "vec.subspace X = subspace X"
- for X::"(real^'n) set"
- unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
- by (auto simp: scalar_mult_eq_scaleR)
-
end
\ No newline at end of file
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu May 03 16:17:44 2018 +0200
@@ -1629,7 +1629,7 @@
proof -
obtain d where "d \<noteq> 0" and d: "\<And>y. f y = 0 \<Longrightarrow> d \<bullet> y = 0"
using orthogonal_to_subspace_exists [OF less] orthogonal_def
- by (metis (mono_tags, lifting) mem_Collect_eq span_superset)
+ by (metis (mono_tags, lifting) mem_Collect_eq span_base)
then obtain k where "k > 0"
and k: "\<And>e. e > 0 \<Longrightarrow> \<exists>y. y \<in> S - {0} \<and> norm y < e \<and> k * norm y \<le> \<bar>d \<bullet> y\<bar>"
using lb by blast
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu May 03 16:17:44 2018 +0200
@@ -1630,7 +1630,7 @@
qed (use \<open>F \<subseteq> insert a S\<close> in auto)
qed
then show ?thesis
- unfolding affine_hull_explicit span_explicit by auto
+ unfolding affine_hull_explicit span_explicit by blast
qed
lemma affine_hull_insert_span:
@@ -2950,7 +2950,7 @@
have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
have "dim {x - a |x. x \<in> S - {a}} \<le> dim S"
- using \<open>a\<in>S\<close> by (auto simp: span_superset span_diff intro: subset_le_dim)
+ using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
also have "\<dots> < dim S + 1" by auto
also have "\<dots> \<le> card (S - {a})"
using assms
@@ -3353,7 +3353,7 @@
by auto
let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
- proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_inc)
+ proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset)
show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
using d inner_not_same_Basis by blast
qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
--- a/src/HOL/Analysis/Determinants.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy Thu May 03 16:17:44 2018 +0200
@@ -476,7 +476,7 @@
assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}"
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
using x
-proof (induction rule: span_induct_alt)
+proof (induction rule: vec.span_induct_alt)
case base
{
fix k
@@ -844,12 +844,12 @@
unfolding sum_cmul
using c ci
by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
- have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
+ have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
unfolding thr0
apply (rule vec.span_sum)
apply simp
- apply (rule span_mul)
- apply (rule span_superset)
+ apply (rule vec.span_scale)
+ apply (rule vec.span_base)
apply auto
done
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu May 03 16:17:44 2018 +0200
@@ -1164,7 +1164,8 @@
by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
lemma matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
- by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left sum.distrib)
+ by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
+ sum.distrib scaleR_right.sum)
lemma vector_matrix_left_distrib [algebra_simps]:
shows "(x + y) v* A = x v* A + y v* A"
--- a/src/HOL/Analysis/Homeomorphism.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu May 03 16:17:44 2018 +0200
@@ -987,8 +987,8 @@
apply (simp add: homeomorphic_def homeomorphism_def)
apply (rule_tac x="g \<circ> h" in exI)
apply (rule_tac x="k \<circ> f" in exI)
- apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp)
- apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset)
+ apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp)
+ apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base)
done
finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
show ?thesis
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu May 03 16:17:44 2018 +0200
@@ -917,7 +917,7 @@
and bg: "bilinear g"
and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
shows "f = g"
- using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
+ using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
subsection \<open>Infinity norm\<close>
--- a/src/HOL/Analysis/Polytope.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Polytope.thy Thu May 03 16:17:44 2018 +0200
@@ -1188,7 +1188,7 @@
qed
then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
- inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_superset)
+ inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_base)
then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
by (rule less.IH) (auto simp: co less.prems)
then show ?thesis
--- a/src/HOL/Analysis/Starlike.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Thu May 03 16:17:44 2018 +0200
@@ -1599,7 +1599,7 @@
fix x :: "'a::euclidean_space"
assume "x \<in> D"
then have "x \<in> span D"
- using span_superset[of _ "D"] by auto
+ using span_base[of _ "D"] by auto
then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
}
@@ -5717,9 +5717,9 @@
fixes k :: "'n::euclidean_space"
shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
apply (simp add: special_hyperplane_span)
-apply (rule Linear_Algebra.dim_unique [OF subset_refl])
+apply (rule dim_unique [OF subset_refl])
apply (auto simp: Diff_subset independent_substdbasis)
-apply (metis member_remove remove_def span_superset)
+apply (metis member_remove remove_def span_base)
done
proposition dim_hyperplane:
@@ -6750,7 +6750,7 @@
using spanU by simp
also have "... = span (insert a (S \<union> T))"
apply (rule eq_span_insert_eq)
- apply (simp add: a'_def span_neg span_sum span_superset span_mul)
+ apply (simp add: a'_def span_neg span_sum span_base span_mul)
done
also have "... = span (S \<union> insert a T)"
by simp
@@ -6922,7 +6922,7 @@
have "dim {x} < DIM('a)"
using assms by auto
then show thesis
- by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_superset that)
+ by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
qed
proposition%important orthogonal_subspace_decomp_exists:
@@ -7192,7 +7192,7 @@
have "e/2 / norm a \<noteq> 0"
using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
then show ?thesis
- by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_superset)
+ by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_base)
qed
ultimately show "?y \<in> S - U" by blast
qed
@@ -8008,7 +8008,7 @@
have "v = ?u + (v - ?u)"
by simp
moreover have "?u \<in> U"
- by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_superset span_mul)
+ by (metis (no_types, lifting) \<open>span B = U\<close> assms subspace_sum span_base span_mul)
moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
fix y
--- a/src/HOL/Modules.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Modules.thy Thu May 03 16:17:44 2018 +0200
@@ -186,7 +186,7 @@
lemma span_zero: "0 \<in> span S"
by (auto simp: span_explicit intro!: exI[of _ "{}"])
-lemma span_UNIV: "span UNIV = UNIV"
+lemma span_UNIV[simp]: "span UNIV = UNIV"
by (auto intro: span_base)
lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
--- a/src/HOL/Vector_Spaces.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy Thu May 03 16:17:44 2018 +0200
@@ -272,7 +272,8 @@
proof -
define p where "p B' \<equiv> B \<subseteq> B' \<and> independent B' \<and> span B' = UNIV" for B'
obtain B' where "p B'"
- using maximal_independent_subset_extend[OF subset_UNIV B] by (auto simp: p_def)
+ using maximal_independent_subset_extend[OF subset_UNIV B]
+ by (metis top.extremum_uniqueI p_def)
then have "p (extend_basis B)"
unfolding extend_basis_def p_def[symmetric] by (rule someI)
then show "B \<subseteq> extend_basis B" "independent (extend_basis B)" "span (extend_basis B) = UNIV"
@@ -403,7 +404,7 @@
have ab: "a \<noteq> b"
using a b by blast
have at: "a \<notin> T"
- using a ab span_superset[of a "T- {b}"] by auto
+ using a ab span_base[of a "T- {b}"] by auto
have mlt: "card ((insert a (T - {b})) - S) < card (T - S)"
using cardlt ft a b by auto
have ft': "finite (insert a (T - {b}))"
@@ -554,12 +555,12 @@
by (simp add: dim_def span_span)
lemma dim_span_eq_card_independent: "independent B \<Longrightarrow> dim (span B) = card B"
- by (simp add: dim_span dim_eq_card)
+ by (simp add: dim_eq_card)
lemma dim_le_card: assumes "V \<subseteq> span W" "finite W" shows "dim V \<le> card W"
proof -
obtain A where "independent A" "A \<subseteq> V" "V \<subseteq> span A"
- using maximal_independent_subset[of V] by auto
+ using maximal_independent_subset[of V] by force
with assms independent_span_bound[of W A] basis_card_eq_dim[of A V]
show ?thesis by auto
qed
@@ -656,11 +657,10 @@
then show ?case by auto
next
case (insert a b x)
- have fb: "finite b" using "2.prems" by simp
have th0: "f ` b \<subseteq> f ` (insert a b)"
by (simp add: subset_insertI)
have ifb: "vs2.independent (f ` b)"
- using independent_mono insert.prems(1) th0 by blast
+ using vs2.independent_mono insert.prems(1) th0 by blast
have fib: "inj_on f b"
using insert.prems(2) by blast
from vs1.span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
@@ -683,10 +683,10 @@
case False
from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
- then have "f a \<notin> span (f ` b)"
- using dependent_def insert.hyps(2) insert.prems(1) by fastforce
- moreover have "f a \<in> span (f ` b)"
- using False span_mul[OF th, of "- 1/ k"] by auto
+ then have "f a \<notin> vs2.span (f ` b)"
+ using vs2.dependent_def insert.hyps(2) insert.prems(1) by fastforce
+ moreover have "f a \<in> vs2.span (f ` b)"
+ using False vs2.span_scale[OF th, of "- 1/ k"] by auto
ultimately have False
by blast
then show ?thesis by blast
@@ -851,7 +851,8 @@
proof -
interpret linear s1 s2 f by fact
obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
- using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto
+ using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
+ by (metis antisym_conv)
have f: "inj_on f (vs1.span B)"
using f unfolding V_eq .
show ?thesis
@@ -892,9 +893,10 @@
shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>f ` V. f (g v) = v)"
proof -
obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
- using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto
+ using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
+ by (metis antisym_conv)
obtain C where C: "vs2.independent C" and fB_C: "f ` B \<subseteq> vs2.span C" "C \<subseteq> f ` B"
- using vs2.maximal_independent_subset[of "f ` B"] by auto
+ using vs2.maximal_independent_subset[of "f ` B"] by metis
then have "\<forall>v\<in>C. \<exists>b\<in>B. v = f b" by auto
then obtain g where g: "\<And>v. v \<in> C \<Longrightarrow> g v \<in> B" "\<And>v. v \<in> C \<Longrightarrow> f (g v) = v" by metis
show ?thesis
@@ -917,7 +919,8 @@
done
show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
have "vs2.span (f ` B) = vs2.span C"
- using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"] by (auto simp: vs2.subspace_span)
+ using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
+ by auto
then show "v \<in> vs2.span C"
using v linear_span_image[OF lf, of B] by (simp add: V_eq)
show "(f \<circ> p.construct C g) b = id b" if b: "b \<in> C" for b
@@ -935,7 +938,8 @@
by (auto simp: linear_iff_module_hom)
lemma linear_injective_left_inverse: "linear s1 s2 f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> g \<circ> f = id"
- using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff)
+ using linear_inj_on_left_inverse[of f UNIV]
+ by force
lemma linear_surj_right_inverse:
assumes lf: "linear s1 s2 f"
@@ -946,7 +950,7 @@
lemma linear_surjective_right_inverse: "linear s1 s2 f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> f \<circ> g = id"
using linear_surj_right_inverse[of f UNIV UNIV]
- by (auto simp: vs1.span_UNIV vs2.span_UNIV fun_eq_iff)
+ by (auto simp: fun_eq_iff)
end
@@ -1025,7 +1029,7 @@
have 2: "span (insert x S) \<subseteq> span (insert x B)"
by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
have 3: "independent (insert x B)"
- by (metis B independent_insert span_subspace subspace_span False)
+ by (metis B(1-3) independent_insert span_subspace subspace_span False)
have "dim (span (insert x S)) = Suc (dim S)"
apply (rule dim_unique [OF 1 2 3])
by (metis B False card_insert_disjoint dim_span finiteI_independent span_base span_eq span_span)
@@ -1055,7 +1059,7 @@
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)
+ by (simp add: \<open>T \<subseteq> span S\<close> span_minimal)
then show ?thesis
using Suc.prems \<open>dim T = n\<close> by linarith
next
@@ -1066,7 +1070,7 @@
by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span)
with \<open>dim T = n\<close> \<open>subspace T\<close> y show ?thesis
apply (rule_tac x="span(insert y T)" in exI)
- apply (auto simp: dim_insert dim_span subspace_span)
+ apply (auto simp: dim_insert)
using span_eq_iff by blast
qed
qed
@@ -1076,12 +1080,12 @@
lemma basis_subspace_exists:
assumes "subspace S"
obtains B where "finite B" "B \<subseteq> S" "independent B" "span B = S" "card B = dim S"
-by (metis assms span_subspace basis_exists independent_imp_finite)
+ by (metis assms span_subspace basis_exists finiteI_independent)
lemma dim_mono: assumes "V \<subseteq> span W" shows "dim V \<le> dim W"
proof -
obtain B where "independent B" "B \<subseteq> W" "W \<subseteq> span B"
- using maximal_independent_subset[of W] by auto
+ using maximal_independent_subset[of W] by force
with dim_le_card[of V B] assms independent_span_bound[of Basis B] basis_card_eq_dim[of B W]
span_mono[of B W] span_minimal[OF _ subspace_span, of W B]
show ?thesis
@@ -1093,13 +1097,10 @@
lemma dim_eq_0 [simp]:
"dim S = 0 \<longleftrightarrow> S \<subseteq> {0}"
- using basis_exists finiteI_independent
- apply safe
- subgoal by fastforce
- by (metis dim_singleton dim_subset le_0_eq)
+ by (metis basis_exists card_eq_0_iff dim_span finiteI_independent span_empty subset_empty subset_singletonD)
lemma dim_UNIV[simp]: "dim UNIV = card Basis"
- using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis span_UNIV)
+ using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis)
lemma independent_card_le_dim: assumes "B \<subseteq> V" and "independent B" shows "card B \<le> dim V"
by (subst dim_eq_card[symmetric, OF refl \<open>independent B\<close>]) (rule dim_subset[OF \<open>B \<subseteq> V\<close>])
@@ -1191,7 +1192,7 @@
corollary dim_eq_span:
shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
- by (simp add: dim_span span_mono subspace_dim_equal subspace_span)
+ by (simp add: span_mono subspace_dim_equal)
lemma dim_psubset:
"span S \<subset> span T \<Longrightarrow> dim S < dim T"
@@ -1380,7 +1381,7 @@
interpret linear s1 s2 f by fact
have *: "card (f ` B1) \<le> vs2.dim UNIV"
using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf
- by (auto simp: vs1.span_Basis vs1.span_UNIV vs1.independent_Basis eq
+ by (auto simp: vs1.span_Basis vs1.independent_Basis eq
simp del: vs2.dim_UNIV
intro!: card_image_le)
have indep_fB: "vs2.independent (f ` B1)"
@@ -1575,7 +1576,7 @@
from B(2) have fB: "finite B"
using finiteI_independent by auto
have Uspan: "UNIV \<subseteq> span (f ` B)"
- by (simp add: B(3) lf sf spanning_surjective_image)
+ by (simp add: B(3) lf linear_spanning_surjective_image sf)
have fBi: "independent (f ` B)"
proof (rule card_le_dim_spanning)
show "card (f ` B) \<le> dim ?U"
@@ -1593,7 +1594,7 @@
have "x = 0" by blast
}
then show ?thesis
- unfolding linear_injective_0[OF lf] using B(3) by blast
+ unfolding linear_inj_iff_eq_0[OF lf] using B(3) by blast
qed
lemma linear_inverse_left:
@@ -1629,7 +1630,7 @@
by blast
have "h = g"
by (metis gf h isomorphism_expand left_right_inverse_eq)
- with \<open>linear h\<close> show ?thesis by blast
+ with \<open>linear scale scale h\<close> show ?thesis by blast
qed
lemma inj_linear_imp_inv_linear:
@@ -1668,10 +1669,10 @@
proof -
from vs1.basis_exists[of S] vs1.finiteI_independent
obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" and fB: "finite B"
- by blast
+ by metis
from vs2.basis_exists[of T] vs2.finiteI_independent
obtain C where C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T" and fC: "finite C"
- by blast
+ by metis
from B(4) C(4) card_le_inj[of B C] d
obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
by auto