# HG changeset patch # User immler # Date 1525357064 -7200 # Node ID 8d50467f7555e00e7768b7e77fa5b8905c7530ae # Parent fad29d2a17a55e66bc8e90ed134d42f612b1ddc5 fixed HOL-Analysis diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- 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) \ (x - ((b \ x) / (b \ 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 "(\B. B ** A = mat 1) \ 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 \ ( *v) A = id" - by blast - have "matrix g ** A = mat 1" - by (metis matrix_vector_mul_linear_gen \Vector_Spaces.linear ( *s) ( *s) g\ g matrix_compose_gen - matrix_eq matrix_id_mat_1 matrix_vector_mul(1)) - then show "\B. B ** A = mat 1" - by metis -qed - -lemma matrix_right_invertible_surjective: - "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\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 \ 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \ 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 "\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: - "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \ - vec.span (columns A) = UNIV" (is "?lhs = ?rhs") -proof - - let ?U = "UNIV :: 'm set" - have fU: "finite ?U" by simp - have lhseq: "?lhs \ (\y. \(x::'a^'m). sum (\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 \ (\x. x \ 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 (\i. (y$i) *s column i A) ?U = x" by blast - have "x \ vec.span (columns A)" - unfolding y[symmetric] scalar_mult_eq_scaleR - proof (rule span_sum [OF span_mul]) - show "column i A \ 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 = "\(y::'a ^'n). \(x::'a^'m). sum (\i. (x$i) *s column i A) ?U = y" - { fix y - have "y \ 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 \ ?U" "y1 = column i A" - from y1 obtain i where i: "i \ ?U" "y1 = column i A" - unfolding columns_def by blast - obtain x:: "real ^'m" where x: "sum (\i. (x$i) *s column i A) ?U = y2" - using step by blast - let ?x = "(\ 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: "\xa \ ?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 (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) - else (x$xa) * ((column xa A$j))) ?U = sum (\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 "\ = sum (\xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" - by (simp add: sum.distrib) - also have "\ = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" - unfolding sum.delta[OF fU] - using i(1) by simp - finally show "sum (\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 (\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: - "(\(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \ 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: - "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" - using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq) - text \The same result in terms of square matrices.\ @@ -1100,7 +978,7 @@ proof - obtain B where "independent B" "span(rows A) \ span B" and B: "B \ 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)" diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Cartesian_Space.thy --- 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 \ '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: + "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" + by (metis matrix_transpose_mul transpose_mat transpose_transpose) + +lemma right_invertible_transpose: + "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(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 \ linear (f :: real^'n \ real ^'m)" + by (simp add: scalar_mult_eq_scaleR linear_def) + +lemma matrix_vector_mul[simp]: + "Vector_Spaces.linear ( *s) ( *s) g \ (\y. matrix g *v y) = g" + "linear f \ (\x. matrix f *v x) = f" + "bounded_linear f \ (\x. matrix f *v x) = f" + for f :: "real^'n \ real ^'m" + by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear) + lemma matrix_left_invertible_injective: - "(\B. (B::'a::field^'m^'n) ** (A::'a::field^'n^'m) = mat 1) - \ (\x y. A *v x = A *v y \ 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: "\x y. A *v x = A *v y \ 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 "\B. (B::'a::{field}^'m^'n) ** A = mat 1" by blast } - ultimately show ?thesis by blast + fixes A :: "'a::field^'n^'m" + shows "(\B. B ** A = mat 1) \ 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 \ ( *v) A = id" + by blast + have "matrix g ** A = mat 1" + by (metis matrix_vector_mul_linear_gen \Vector_Spaces.linear ( *s) ( *s) g\ g matrix_compose_gen + matrix_eq matrix_id_mat_1 matrix_vector_mul(1)) + then show "\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: + "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\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 \ 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \ 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 "\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 "(\(B::'a ^'m^'n). B ** A = mat 1) \ @@ -196,14 +249,6 @@ ultimately show ?thesis unfolding matrix_left_invertible_ker by auto qed -lemma left_invertible_transpose: - "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" - by (metis matrix_transpose_mul transpose_mat transpose_transpose) - -lemma right_invertible_transpose: - "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(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 "(\(B::'a^'m^'n). A ** B = mat 1) \ @@ -212,6 +257,81 @@ matrix_left_invertible_independent_columns by (simp add:) +lemma matrix_right_invertible_span_columns: + "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \ + vec.span (columns A) = UNIV" (is "?lhs = ?rhs") +proof - + let ?U = "UNIV :: 'm set" + have fU: "finite ?U" by simp + have lhseq: "?lhs \ (\y. \(x::'a^'m). sum (\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 \ (\x. x \ 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 (\i. (y$i) *s column i A) ?U = x" by blast + have "x \ vec.span (columns A)" + unfolding y[symmetric] scalar_mult_eq_scaleR + proof (rule vec.span_sum [OF vec.span_scale]) + show "column i A \ 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 = "\(y::'a ^'n). \(x::'a^'m). sum (\i. (x$i) *s column i A) ?U = y" + { fix y + have "y \ 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 \ ?U" "y1 = column i A" + unfolding columns_def by blast + obtain x:: "'a ^'m" where x: "sum (\i. (x$i) *s column i A) ?U = y2" + using step by blast + let ?x = "(\ 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: "\xa \ ?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 (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) + else (x$xa) * ((column xa A$j))) ?U = sum (\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 "\ = sum (\xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" + by (simp add: sum.distrib) + also have "\ = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" + unfolding sum.delta[OF fU] + using i(1) by simp + finally show "sum (\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 (\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: + "(\(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \ 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: + "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ 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 \ 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 \ linear (f :: real^'n \ real ^'m)" - by (simp add: scalar_mult_eq_scaleR linear_def) - -lemma matrix_vector_mul[simp]: - "Vector_Spaces.linear ( *s) ( *s) g \ (\y. matrix g *v y) = g" - "linear f \ (\x. matrix f *v x) = f" - "bounded_linear f \ (\x. matrix f *v x) = f" - for f :: "real^'n \ 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 diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Change_Of_Vars.thy --- 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 \ 0" and d: "\y. f y = 0 \ d \ 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: "\e. e > 0 \ \y. y \ S - {0} \ norm y < e \ k * norm y \ \d \ y\" using lb by blast diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Convex_Euclidean_Space.thy --- 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 \F \ insert a S\ 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 \ S - {a}} = card (S - {a})" by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def) have "dim {x - a |x. x \ S - {a}} \ dim S" - using \a\S\ by (auto simp: span_superset span_diff intro: subset_le_dim) + using \a\S\ by (auto simp: span_base span_diff intro: subset_le_dim) also have "\ < dim S + 1" by auto also have "\ \ card (S - {a})" using assms @@ -3353,7 +3353,7 @@ by auto let ?t = "{x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0}" have "\f. linear f \ f ` B = d \ f ` span B = ?t \ 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 \ {x. \i\Basis. i \ d \ x \ i = 0}" using d inner_not_same_Basis by blast qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms) diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Determinants.thy --- 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 \ vec.span {row j A |j. j \ i}" shows "det (\ 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 \ span {row j A| j. j \ i}" + have thr: "- row i A \ vec.span {row j A| j. j \ 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 = "(\ k. if k = i then 0 else row k A) :: 'a^'n^'n" diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Finite_Cartesian_Product.thy --- 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 (\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" diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Homeomorphism.thy --- 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 \ h" in exI) apply (rule_tac x="k \ 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 \ h) ` (+) (- a) ` S" . show ?thesis diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Linear_Algebra.thy --- 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: "\i j. i \ Basis \ j \ Basis \ 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 \Infinity norm\ diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Polytope.thy --- 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 \ {x. a \ x = 0}) < n" by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff - inf_le1 \dim S = n\ not_le rel_interior_subset span_0 span_superset) + inf_le1 \dim S = n\ not_le rel_interior_subset span_0 span_base) then have "0 \ convex hull {x. x extreme_point_of (S \ {x. a \ x = 0})}" by (rule less.IH) (auto simp: co less.prems) then show ?thesis diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Analysis/Starlike.thy --- 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 \ D" then have "x \ 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)) \ 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 \ Basis \ dim {x. k \ 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 \ 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 \ 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 \ 0" using \0 < e\ \a \ 0\ by auto then show ?thesis - by (metis True \a \ 0\ a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_superset) + by (metis True \a \ 0\ a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_base) qed ultimately show "?y \ S - U" by blast qed @@ -8008,7 +8008,7 @@ have "v = ?u + (v - ?u)" by simp moreover have "?u \ U" - by (metis (no_types, lifting) \span B = U\ assms real_vector_class.subspace_sum span_superset span_mul) + by (metis (no_types, lifting) \span B = U\ assms subspace_sum span_base span_mul) moreover have "(v - ?u) \ U\<^sup>\" proof (clarsimp simp: orthogonal_comp_def orthogonal_def) fix y diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Modules.thy --- 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 \ 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 \ span S \ y \ span S \ x + y \ span S" diff -r fad29d2a17a5 -r 8d50467f7555 src/HOL/Vector_Spaces.thy --- 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' \ B \ B' \ independent B' \ 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 \ extend_basis B" "independent (extend_basis B)" "span (extend_basis B) = UNIV" @@ -403,7 +404,7 @@ have ab: "a \ b" using a b by blast have at: "a \ 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 \ 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 \ span W" "finite W" shows "dim V \ card W" proof - obtain A where "independent A" "A \ V" "V \ 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 \ 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 \ span (f ` b)" - using dependent_def insert.hyps(2) insert.prems(1) by fastforce - moreover have "f a \ span (f ` b)" - using False span_mul[OF th, of "- 1/ k"] by auto + then have "f a \ vs2.span (f ` b)" + using vs2.dependent_def insert.hyps(2) insert.prems(1) by fastforce + moreover have "f a \ 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 _ \vs1.subspace V\] by auto + using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \vs1.subspace V\] + by (metis antisym_conv) have f: "inj_on f (vs1.span B)" using f unfolding V_eq . show ?thesis @@ -892,9 +893,10 @@ shows "\g\UNIV \ V. linear s2 s1 g \ (\v\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 _ \vs1.subspace V\] by auto + using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \vs1.subspace V\] + by (metis antisym_conv) obtain C where C: "vs2.independent C" and fB_C: "f ` B \ vs2.span C" "C \ f ` B" - using vs2.maximal_independent_subset[of "f ` B"] by auto + using vs2.maximal_independent_subset[of "f ` B"] by metis then have "\v\C. \b\B. v = f b" by auto then obtain g where g: "\v. v \ C \ g v \ B" "\v. v \ C \ 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 \ vs2.span C" using v linear_span_image[OF lf, of B] by (simp add: V_eq) show "(f \ p.construct C g) b = id b" if b: "b \ C" for b @@ -935,7 +938,8 @@ by (auto simp: linear_iff_module_hom) lemma linear_injective_left_inverse: "linear s1 s2 f \ inj f \ \g. linear s2 s1 g \ g \ 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 \ surj f \ \g. linear s2 s1 g \ f \ 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) \ span (insert x B)" by (metis \B \ span S\ \span S \ span B\ 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: \T \ span S\ span_minimal subspace_span) + by (simp add: \T \ span S\ span_minimal) then show ?thesis using Suc.prems \dim T = n\ by linarith next @@ -1066,7 +1070,7 @@ by (metis (no_types) \T \ span S\ subsetD insert_subset span_superset span_mono span_span) with \dim T = n\ \subspace T\ 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 \ 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 \ span W" shows "dim V \ dim W" proof - obtain B where "independent B" "B \ W" "W \ 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 \ S \ {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 \ V" and "independent B" shows "card B \ dim V" by (subst dim_eq_card[symmetric, OF refl \independent B\]) (rule dim_subset[OF \B \ V\]) @@ -1191,7 +1192,7 @@ corollary dim_eq_span: shows "\S \ T; dim T \ dim S\ \ 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 \ span T \ dim S < dim T" @@ -1380,7 +1381,7 @@ interpret linear s1 s2 f by fact have *: "card (f ` B1) \ 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 \ 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) \ 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 \linear h\ show ?thesis by blast + with \linear scale scale h\ 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 \ S" "vs1.independent B" "S \ 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 \ T" "vs2.independent C" "T \ 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 \ C" "inj_on f B" using \finite B\ \finite C\ by auto