fixed HOL-Analysis
authorimmler
Thu May 03 16:17:44 2018 +0200 (12 months ago)
changeset 680748d50467f7555
parent 68073 fad29d2a17a5
child 68075 262b42b59151
fixed HOL-Analysis
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Modules.thy
src/HOL/Vector_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 15:07:14 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 16:17:44 2018 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "real^'n^'m"
     1.8 +lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
     1.9    using matrix_vector_mul_linear[of A]
    1.10    by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
    1.11  
    1.12 @@ -416,128 +416,6 @@
    1.13  lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
    1.14    unfolding inner_simps scalar_mult_eq_scaleR by auto
    1.15  
    1.16 -lemma matrix_left_invertible_injective:
    1.17 -  fixes A :: "'a::field^'n^'m"
    1.18 -  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
    1.19 -proof safe
    1.20 -  fix B
    1.21 -  assume B: "B ** A = mat 1"
    1.22 -  show "inj (( *v) A)"
    1.23 -    unfolding inj_on_def
    1.24 -      by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
    1.25 -next
    1.26 -  assume "inj (( *v) A)"
    1.27 -  from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
    1.28 -  obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
    1.29 -    by blast
    1.30 -  have "matrix g ** A = mat 1"
    1.31 -    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
    1.32 -        matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
    1.33 -  then show "\<exists>B. B ** A = mat 1"
    1.34 -    by metis
    1.35 -qed
    1.36 -
    1.37 -lemma matrix_right_invertible_surjective:
    1.38 -  "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
    1.39 -proof -
    1.40 -  { fix B :: "'a ^'m^'n"
    1.41 -    assume AB: "A ** B = mat 1"
    1.42 -    { fix x :: "'a ^ 'm"
    1.43 -      have "A *v (B *v x) = x"
    1.44 -        by (simp add: matrix_vector_mul_assoc AB) }
    1.45 -    hence "surj (( *v) A)" unfolding surj_def by metis }
    1.46 -  moreover
    1.47 -  { assume sf: "surj (( *v) A)"
    1.48 -    from vec.linear_surjective_right_inverse[OF _ this]
    1.49 -    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
    1.50 -      by blast
    1.51 -
    1.52 -    have "A ** (matrix g) = mat 1"
    1.53 -      unfolding matrix_eq  matrix_vector_mul_lid
    1.54 -        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
    1.55 -      using g(2) unfolding o_def fun_eq_iff id_def
    1.56 -      .
    1.57 -    hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
    1.58 -  }
    1.59 -  ultimately show ?thesis unfolding surj_def by blast
    1.60 -qed
    1.61 -
    1.62 -lemma matrix_right_invertible_span_columns:
    1.63 -  "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
    1.64 -    vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
    1.65 -proof -
    1.66 -  let ?U = "UNIV :: 'm set"
    1.67 -  have fU: "finite ?U" by simp
    1.68 -  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
    1.69 -    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
    1.70 -    by (simp add: eq_commute)
    1.71 -  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
    1.72 -  { assume h: ?lhs
    1.73 -    { fix x:: "'a ^'n"
    1.74 -      from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
    1.75 -        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
    1.76 -      have "x \<in> vec.span (columns A)"
    1.77 -        unfolding y[symmetric] scalar_mult_eq_scaleR
    1.78 -      proof (rule span_sum [OF span_mul])
    1.79 -        show "column i A \<in> span (columns A)" for i
    1.80 -          using columns_def span_inc by auto
    1.81 -      qed
    1.82 -    }
    1.83 -    then have ?rhs unfolding rhseq by blast }
    1.84 -  moreover
    1.85 -  { assume h:?rhs
    1.86 -    let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
    1.87 -    { fix y
    1.88 -      have "y \<in> vec.span (columns A)"
    1.89 -        unfolding h by blast
    1.90 -      then have "?P y"
    1.91 -      proof (induction rule: vec.span_induct_alt)
    1.92 -        case base
    1.93 -        then show ?case
    1.94 -          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
    1.95 -      next
    1.96 -        case (step c y1 y2)
    1.97 -        then obtain i where i: "i \<in> ?U" "y1 = column i A"
    1.98 -        from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
    1.99 -          unfolding columns_def by blast
   1.100 -        obtain x:: "real ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
   1.101 -          using step by blast
   1.102 -        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
   1.103 -        show ?case
   1.104 -        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
   1.105 -          fix j
   1.106 -          have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.107 -              else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
   1.108 -            using i(1) by (simp add: field_simps)
   1.109 -          have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.110 -              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"
   1.111 -            by (rule sum.cong[OF refl]) (use th in blast)
   1.112 -          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"
   1.113 -            by (simp add: sum.distrib)
   1.114 -          also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.115 -            unfolding sum.delta[OF fU]
   1.116 -            using i(1) by simp
   1.117 -          finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.118 -            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
   1.119 -        qed
   1.120 -      qed
   1.121 -    }
   1.122 -    then have ?lhs unfolding lhseq ..
   1.123 -  }
   1.124 -  ultimately show ?thesis by blast
   1.125 -qed
   1.126 -
   1.127 -lemma matrix_left_invertible_span_rows_gen:
   1.128 -  "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
   1.129 -  unfolding right_invertible_transpose[symmetric]
   1.130 -  unfolding columns_transpose[symmetric]
   1.131 -  unfolding matrix_right_invertible_span_columns
   1.132 -  ..
   1.133 -
   1.134 -lemma matrix_left_invertible_span_rows:
   1.135 -  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
   1.136 -  using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
   1.137 -
   1.138  
   1.139  text \<open>The same result in terms of square matrices.\<close>
   1.140  
   1.141 @@ -1100,7 +978,7 @@
   1.142    proof -
   1.143      obtain B where "independent B" "span(rows A) \<subseteq> span B"
   1.144                and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
   1.145 -      using basis_exists [of "span(rows A)"] by blast
   1.146 +      using basis_exists [of "span(rows A)"] by metis
   1.147      with span_subspace have eq: "span B = span(rows A)"
   1.148        by auto
   1.149      then have inj: "inj_on (( *v) A) (span B)"
     2.1 --- a/src/HOL/Analysis/Cartesian_Space.thy	Thu May 03 15:07:14 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Cartesian_Space.thy	Thu May 03 16:17:44 2018 +0200
     2.3 @@ -97,6 +97,14 @@
     2.4    by unfold_locales
     2.5      (vector matrix_vector_mult_def sum.distrib algebra_simps)+
     2.6  
     2.7 +lemma span_vec_eq: "vec.span X = span X"
     2.8 +  and dim_vec_eq: "vec.dim X = dim X"
     2.9 +  and dependent_vec_eq: "vec.dependent X = dependent X"
    2.10 +  and subspace_vec_eq: "vec.subspace X = subspace X"
    2.11 +  for X::"(real^'n) set"
    2.12 +  unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
    2.13 +  by (auto simp: scalar_mult_eq_scaleR)
    2.14 +
    2.15  lemma linear_componentwise:
    2.16    fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
    2.17    assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
    2.18 @@ -143,24 +151,44 @@
    2.19    using matrix_compose_gen[of f g] assms
    2.20    by (simp add: linear_def scalar_mult_eq_scaleR)
    2.21  
    2.22 +lemma left_invertible_transpose:
    2.23 +  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
    2.24 +  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
    2.25 +
    2.26 +lemma right_invertible_transpose:
    2.27 +  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
    2.28 +  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
    2.29 +
    2.30 +lemma linear_matrix_vector_mul_eq:
    2.31 +  "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
    2.32 +  by (simp add: scalar_mult_eq_scaleR linear_def)
    2.33 +
    2.34 +lemma matrix_vector_mul[simp]:
    2.35 +  "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
    2.36 +  "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
    2.37 +  "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
    2.38 +  for f :: "real^'n \<Rightarrow> real ^'m"
    2.39 +  by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
    2.40 +
    2.41  lemma matrix_left_invertible_injective:
    2.42 -  "(\<exists>B. (B::'a::field^'m^'n) ** (A::'a::field^'n^'m) = mat 1)
    2.43 -    \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
    2.44 -proof -
    2.45 -  { fix B:: "'a^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
    2.46 -    from xy have "B*v (A *v x) = B *v (A*v y)" by simp
    2.47 -    hence "x = y"
    2.48 -      unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . }
    2.49 -  moreover
    2.50 -  { assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
    2.51 -    hence i: "inj (( *v) A)" unfolding inj_on_def by auto
    2.52 -    from vec.linear_exists_left_inverse_on[OF matrix_vector_mul_linear_gen vec.subspace_UNIV i]
    2.53 -    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)
    2.54 -    have "matrix g ** A = mat 1"
    2.55 -      unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
    2.56 -      using g(2) by (metis comp_apply id_apply)
    2.57 -    then have "\<exists>B. (B::'a::{field}^'m^'n) ** A = mat 1" by blast }
    2.58 -  ultimately show ?thesis by blast
    2.59 +  fixes A :: "'a::field^'n^'m"
    2.60 +  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
    2.61 +proof safe
    2.62 +  fix B
    2.63 +  assume B: "B ** A = mat 1"
    2.64 +  show "inj (( *v) A)"
    2.65 +    unfolding inj_on_def
    2.66 +      by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
    2.67 +next
    2.68 +  assume "inj (( *v) A)"
    2.69 +  from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
    2.70 +  obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
    2.71 +    by blast
    2.72 +  have "matrix g ** A = mat 1"
    2.73 +    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
    2.74 +        matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
    2.75 +  then show "\<exists>B. B ** A = mat 1"
    2.76 +    by metis
    2.77  qed
    2.78  
    2.79  lemma matrix_left_invertible_ker:
    2.80 @@ -169,6 +197,31 @@
    2.81    using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
    2.82    by (simp add: inj_on_def)
    2.83  
    2.84 +lemma matrix_right_invertible_surjective:
    2.85 +  "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
    2.86 +proof -
    2.87 +  { fix B :: "'a ^'m^'n"
    2.88 +    assume AB: "A ** B = mat 1"
    2.89 +    { fix x :: "'a ^ 'm"
    2.90 +      have "A *v (B *v x) = x"
    2.91 +        by (simp add: matrix_vector_mul_assoc AB) }
    2.92 +    hence "surj (( *v) A)" unfolding surj_def by metis }
    2.93 +  moreover
    2.94 +  { assume sf: "surj (( *v) A)"
    2.95 +    from vec.linear_surjective_right_inverse[OF _ this]
    2.96 +    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
    2.97 +      by blast
    2.98 +
    2.99 +    have "A ** (matrix g) = mat 1"
   2.100 +      unfolding matrix_eq  matrix_vector_mul_lid
   2.101 +        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
   2.102 +      using g(2) unfolding o_def fun_eq_iff id_def
   2.103 +      .
   2.104 +    hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
   2.105 +  }
   2.106 +  ultimately show ?thesis unfolding surj_def by blast
   2.107 +qed
   2.108 +
   2.109  lemma matrix_left_invertible_independent_columns:
   2.110    fixes A :: "'a::{field}^'n^'m"
   2.111    shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
   2.112 @@ -196,14 +249,6 @@
   2.113    ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
   2.114  qed
   2.115  
   2.116 -lemma left_invertible_transpose:
   2.117 -  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
   2.118 -  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
   2.119 -
   2.120 -lemma right_invertible_transpose:
   2.121 -  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
   2.122 -  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
   2.123 -
   2.124  lemma matrix_right_invertible_independent_rows:
   2.125    fixes A :: "'a::{field}^'n^'m"
   2.126    shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
   2.127 @@ -212,6 +257,81 @@
   2.128      matrix_left_invertible_independent_columns
   2.129    by (simp add:)
   2.130  
   2.131 +lemma matrix_right_invertible_span_columns:
   2.132 +  "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
   2.133 +    vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
   2.134 +proof -
   2.135 +  let ?U = "UNIV :: 'm set"
   2.136 +  have fU: "finite ?U" by simp
   2.137 +  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
   2.138 +    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
   2.139 +    by (simp add: eq_commute)
   2.140 +  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
   2.141 +  { assume h: ?lhs
   2.142 +    { fix x:: "'a ^'n"
   2.143 +      from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
   2.144 +        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
   2.145 +      have "x \<in> vec.span (columns A)"
   2.146 +        unfolding y[symmetric] scalar_mult_eq_scaleR
   2.147 +      proof (rule vec.span_sum [OF vec.span_scale])
   2.148 +        show "column i A \<in> vec.span (columns A)" for i
   2.149 +          using columns_def vec.span_superset by auto
   2.150 +      qed
   2.151 +    }
   2.152 +    then have ?rhs unfolding rhseq by blast }
   2.153 +  moreover
   2.154 +  { assume h:?rhs
   2.155 +    let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
   2.156 +    { fix y
   2.157 +      have "y \<in> vec.span (columns A)"
   2.158 +        unfolding h by blast
   2.159 +      then have "?P y"
   2.160 +      proof (induction rule: vec.span_induct_alt)
   2.161 +        case base
   2.162 +        then show ?case
   2.163 +          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
   2.164 +      next
   2.165 +        case (step c y1 y2)
   2.166 +        from step obtain i where i: "i \<in> ?U" "y1 = column i A"
   2.167 +          unfolding columns_def by blast
   2.168 +        obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
   2.169 +          using step by blast
   2.170 +        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
   2.171 +        show ?case
   2.172 +        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
   2.173 +          fix j
   2.174 +          have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
   2.175 +              else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
   2.176 +            using i(1) by (simp add: field_simps)
   2.177 +          have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   2.178 +              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"
   2.179 +            by (rule sum.cong[OF refl]) (use th in blast)
   2.180 +          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"
   2.181 +            by (simp add: sum.distrib)
   2.182 +          also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   2.183 +            unfolding sum.delta[OF fU]
   2.184 +            using i(1) by simp
   2.185 +          finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   2.186 +            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
   2.187 +        qed
   2.188 +      qed
   2.189 +    }
   2.190 +    then have ?lhs unfolding lhseq ..
   2.191 +  }
   2.192 +  ultimately show ?thesis by blast
   2.193 +qed
   2.194 +
   2.195 +lemma matrix_left_invertible_span_rows_gen:
   2.196 +  "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
   2.197 +  unfolding right_invertible_transpose[symmetric]
   2.198 +  unfolding columns_transpose[symmetric]
   2.199 +  unfolding matrix_right_invertible_span_columns
   2.200 +  ..
   2.201 +
   2.202 +lemma matrix_left_invertible_span_rows:
   2.203 +  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
   2.204 +  using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
   2.205 +
   2.206  lemma matrix_left_right_inverse:
   2.207    fixes A A' :: "'a::{field}^'n^'n"
   2.208    shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
   2.209 @@ -339,23 +459,4 @@
   2.210  lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
   2.211    unfolding vector_space_over_itself.dimension_def by simp
   2.212  
   2.213 -lemma linear_matrix_vector_mul_eq:
   2.214 -  "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
   2.215 -  by (simp add: scalar_mult_eq_scaleR linear_def)
   2.216 -
   2.217 -lemma matrix_vector_mul[simp]:
   2.218 -  "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
   2.219 -  "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
   2.220 -  "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
   2.221 -  for f :: "real^'n \<Rightarrow> real ^'m"
   2.222 -  by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
   2.223 -
   2.224 -lemma span_vec_eq: "vec.span X = span X"
   2.225 -  and dim_vec_eq: "vec.dim X = dim X"
   2.226 -  and dependent_vec_eq: "vec.dependent X = dependent X"
   2.227 -  and subspace_vec_eq: "vec.subspace X = subspace X"
   2.228 -  for X::"(real^'n) set"
   2.229 -  unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
   2.230 -  by (auto simp: scalar_mult_eq_scaleR)
   2.231 -
   2.232  end
   2.233 \ No newline at end of file
     3.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu May 03 15:07:14 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu May 03 16:17:44 2018 +0200
     3.3 @@ -1629,7 +1629,7 @@
     3.4    proof -
     3.5      obtain d where "d \<noteq> 0" and d: "\<And>y. f y = 0 \<Longrightarrow> d \<bullet> y = 0"
     3.6        using orthogonal_to_subspace_exists [OF less] orthogonal_def
     3.7 -      by (metis (mono_tags, lifting) mem_Collect_eq span_superset)
     3.8 +      by (metis (mono_tags, lifting) mem_Collect_eq span_base)
     3.9      then obtain k where "k > 0"
    3.10        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>"
    3.11        using lb by blast
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 03 15:07:14 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 03 16:17:44 2018 +0200
     4.3 @@ -1630,7 +1630,7 @@
     4.4      qed (use \<open>F \<subseteq> insert a S\<close> in auto)
     4.5    qed
     4.6    then show ?thesis
     4.7 -    unfolding affine_hull_explicit span_explicit by auto
     4.8 +    unfolding affine_hull_explicit span_explicit by blast
     4.9  qed
    4.10  
    4.11  lemma affine_hull_insert_span:
    4.12 @@ -2950,7 +2950,7 @@
    4.13    have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
    4.14      by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
    4.15    have "dim {x - a |x. x \<in> S - {a}} \<le> dim S"
    4.16 -    using \<open>a\<in>S\<close> by (auto simp: span_superset span_diff intro: subset_le_dim)
    4.17 +    using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
    4.18    also have "\<dots> < dim S + 1" by auto
    4.19    also have "\<dots> \<le> card (S - {a})"
    4.20      using assms
    4.21 @@ -3353,7 +3353,7 @@
    4.22      by auto
    4.23    let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
    4.24    have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
    4.25 -  proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_inc)
    4.26 +  proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset)
    4.27      show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
    4.28        using d inner_not_same_Basis by blast
    4.29    qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
     5.1 --- a/src/HOL/Analysis/Determinants.thy	Thu May 03 15:07:14 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Determinants.thy	Thu May 03 16:17:44 2018 +0200
     5.3 @@ -476,7 +476,7 @@
     5.4    assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}"
     5.5    shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
     5.6    using x
     5.7 -proof (induction rule: span_induct_alt)
     5.8 +proof (induction rule: vec.span_induct_alt)
     5.9    case base
    5.10    {
    5.11      fix k
    5.12 @@ -844,12 +844,12 @@
    5.13        unfolding sum_cmul
    5.14        using c ci   
    5.15        by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
    5.16 -    have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
    5.17 +    have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
    5.18        unfolding thr0
    5.19        apply (rule vec.span_sum)
    5.20        apply simp
    5.21 -      apply (rule span_mul)
    5.22 -      apply (rule span_superset)
    5.23 +      apply (rule vec.span_scale)
    5.24 +      apply (rule vec.span_base)
    5.25        apply auto
    5.26        done
    5.27      let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
     6.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu May 03 15:07:14 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu May 03 16:17:44 2018 +0200
     6.3 @@ -1164,7 +1164,8 @@
     6.4    by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
     6.5  
     6.6  lemma matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
     6.7 -  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left sum.distrib)
     6.8 +  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
     6.9 +      sum.distrib scaleR_right.sum)
    6.10  
    6.11  lemma vector_matrix_left_distrib [algebra_simps]:
    6.12    shows "(x + y) v* A = x v* A + y v* A"
     7.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Thu May 03 15:07:14 2018 +0200
     7.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Thu May 03 16:17:44 2018 +0200
     7.3 @@ -987,8 +987,8 @@
     7.4      apply (simp add: homeomorphic_def homeomorphism_def)
     7.5      apply (rule_tac x="g \<circ> h" in exI)
     7.6      apply (rule_tac x="k \<circ> f" in exI)
     7.7 -    apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp)
     7.8 -    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset)
     7.9 +    apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp)
    7.10 +    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base)
    7.11      done
    7.12    finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
    7.13    show ?thesis
     8.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu May 03 15:07:14 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu May 03 16:17:44 2018 +0200
     8.3 @@ -917,7 +917,7 @@
     8.4      and bg: "bilinear g"
     8.5      and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
     8.6    shows "f = g"
     8.7 -  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
     8.8 +  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
     8.9  
    8.10  subsection \<open>Infinity norm\<close>
    8.11  
     9.1 --- a/src/HOL/Analysis/Polytope.thy	Thu May 03 15:07:14 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu May 03 16:17:44 2018 +0200
     9.3 @@ -1188,7 +1188,7 @@
     9.4      qed
     9.5      then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
     9.6        by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
     9.7 -           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_superset)
     9.8 +           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_base)
     9.9      then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
    9.10        by (rule less.IH) (auto simp: co less.prems)
    9.11      then show ?thesis
    10.1 --- a/src/HOL/Analysis/Starlike.thy	Thu May 03 15:07:14 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu May 03 16:17:44 2018 +0200
    10.3 @@ -1599,7 +1599,7 @@
    10.4          fix x :: "'a::euclidean_space"
    10.5          assume "x \<in> D"
    10.6          then have "x \<in> span D"
    10.7 -          using span_superset[of _ "D"] by auto
    10.8 +          using span_base[of _ "D"] by auto
    10.9          then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
   10.10            using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
   10.11        }
   10.12 @@ -5717,9 +5717,9 @@
   10.13    fixes k :: "'n::euclidean_space"
   10.14    shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
   10.15  apply (simp add: special_hyperplane_span)
   10.16 -apply (rule Linear_Algebra.dim_unique [OF subset_refl])
   10.17 +apply (rule dim_unique [OF subset_refl])
   10.18  apply (auto simp: Diff_subset independent_substdbasis)
   10.19 -apply (metis member_remove remove_def span_superset)
   10.20 +apply (metis member_remove remove_def span_base)
   10.21  done
   10.22  
   10.23  proposition dim_hyperplane:
   10.24 @@ -6750,7 +6750,7 @@
   10.25      using spanU by simp
   10.26    also have "... = span (insert a (S \<union> T))"
   10.27      apply (rule eq_span_insert_eq)
   10.28 -    apply (simp add: a'_def span_neg span_sum span_superset span_mul)
   10.29 +    apply (simp add: a'_def span_neg span_sum span_base span_mul)
   10.30      done
   10.31    also have "... = span (S \<union> insert a T)"
   10.32      by simp
   10.33 @@ -6922,7 +6922,7 @@
   10.34    have "dim {x} < DIM('a)"
   10.35      using assms by auto
   10.36    then show thesis
   10.37 -    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_superset that)
   10.38 +    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
   10.39  qed
   10.40  
   10.41  proposition%important orthogonal_subspace_decomp_exists:
   10.42 @@ -7192,7 +7192,7 @@
   10.43                have "e/2 / norm a \<noteq> 0"
   10.44                  using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
   10.45                then show ?thesis
   10.46 -                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_superset)
   10.47 +                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_base)
   10.48              qed
   10.49              ultimately show "?y \<in> S - U" by blast
   10.50            qed
   10.51 @@ -8008,7 +8008,7 @@
   10.52      have "v = ?u + (v - ?u)"
   10.53        by simp
   10.54      moreover have "?u \<in> U"
   10.55 -      by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_superset span_mul)
   10.56 +      by (metis (no_types, lifting) \<open>span B = U\<close> assms subspace_sum span_base span_mul)
   10.57      moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
   10.58      proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
   10.59        fix y
    11.1 --- a/src/HOL/Modules.thy	Thu May 03 15:07:14 2018 +0200
    11.2 +++ b/src/HOL/Modules.thy	Thu May 03 16:17:44 2018 +0200
    11.3 @@ -186,7 +186,7 @@
    11.4  lemma span_zero: "0 \<in> span S"
    11.5    by (auto simp: span_explicit intro!: exI[of _ "{}"])
    11.6  
    11.7 -lemma span_UNIV: "span UNIV = UNIV"
    11.8 +lemma span_UNIV[simp]: "span UNIV = UNIV"
    11.9    by (auto intro: span_base)
   11.10  
   11.11  lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
    12.1 --- a/src/HOL/Vector_Spaces.thy	Thu May 03 15:07:14 2018 +0200
    12.2 +++ b/src/HOL/Vector_Spaces.thy	Thu May 03 16:17:44 2018 +0200
    12.3 @@ -272,7 +272,8 @@
    12.4  proof -
    12.5    define p where "p B' \<equiv> B \<subseteq> B' \<and> independent B' \<and> span B' = UNIV" for B'
    12.6    obtain B' where "p B'"
    12.7 -    using maximal_independent_subset_extend[OF subset_UNIV B] by (auto simp: p_def)
    12.8 +    using maximal_independent_subset_extend[OF subset_UNIV B]
    12.9 +    by (metis top.extremum_uniqueI p_def)
   12.10    then have "p (extend_basis B)"
   12.11      unfolding extend_basis_def p_def[symmetric] by (rule someI)
   12.12    then show "B \<subseteq> extend_basis B" "independent (extend_basis B)" "span (extend_basis B) = UNIV"
   12.13 @@ -403,7 +404,7 @@
   12.14        have ab: "a \<noteq> b"
   12.15          using a b by blast
   12.16        have at: "a \<notin> T"
   12.17 -        using a ab span_superset[of a "T- {b}"] by auto
   12.18 +        using a ab span_base[of a "T- {b}"] by auto
   12.19        have mlt: "card ((insert a (T - {b})) - S) < card (T - S)"
   12.20          using cardlt ft a b by auto
   12.21        have ft': "finite (insert a (T - {b}))"
   12.22 @@ -554,12 +555,12 @@
   12.23    by (simp add: dim_def span_span)
   12.24  
   12.25  lemma dim_span_eq_card_independent: "independent B \<Longrightarrow> dim (span B) = card B"
   12.26 -  by (simp add: dim_span dim_eq_card)
   12.27 +  by (simp add: dim_eq_card)
   12.28  
   12.29  lemma dim_le_card: assumes "V \<subseteq> span W" "finite W" shows "dim V \<le> card W"
   12.30  proof -
   12.31    obtain A where "independent A" "A \<subseteq> V" "V \<subseteq> span A"
   12.32 -    using maximal_independent_subset[of V] by auto
   12.33 +    using maximal_independent_subset[of V] by force
   12.34    with assms independent_span_bound[of W A] basis_card_eq_dim[of A V]
   12.35    show ?thesis by auto
   12.36  qed
   12.37 @@ -656,11 +657,10 @@
   12.38    then show ?case by auto
   12.39  next
   12.40    case (insert a b x)
   12.41 -  have fb: "finite b" using "2.prems" by simp
   12.42    have th0: "f ` b \<subseteq> f ` (insert a b)"
   12.43      by (simp add: subset_insertI)
   12.44    have ifb: "vs2.independent (f ` b)"
   12.45 -    using independent_mono insert.prems(1) th0 by blast
   12.46 +    using vs2.independent_mono insert.prems(1) th0 by blast
   12.47    have fib: "inj_on f b"
   12.48      using insert.prems(2) by blast
   12.49    from vs1.span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
   12.50 @@ -683,10 +683,10 @@
   12.51      case False
   12.52      from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
   12.53      have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
   12.54 -    then have "f a \<notin> span (f ` b)" 
   12.55 -      using dependent_def insert.hyps(2) insert.prems(1) by fastforce
   12.56 -    moreover have "f a \<in> span (f ` b)"
   12.57 -      using False span_mul[OF th, of "- 1/ k"] by auto
   12.58 +    then have "f a \<notin> vs2.span (f ` b)" 
   12.59 +      using vs2.dependent_def insert.hyps(2) insert.prems(1) by fastforce
   12.60 +    moreover have "f a \<in> vs2.span (f ` b)"
   12.61 +      using False vs2.span_scale[OF th, of "- 1/ k"] by auto
   12.62      ultimately have False
   12.63        by blast
   12.64      then show ?thesis by blast
   12.65 @@ -851,7 +851,8 @@
   12.66  proof -
   12.67    interpret linear s1 s2 f by fact
   12.68    obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
   12.69 -    using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto
   12.70 +    using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
   12.71 +    by (metis antisym_conv)
   12.72    have f: "inj_on f (vs1.span B)"
   12.73      using f unfolding V_eq .
   12.74    show ?thesis
   12.75 @@ -892,9 +893,10 @@
   12.76    shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>f ` V. f (g v) = v)"
   12.77  proof -
   12.78    obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
   12.79 -    using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto
   12.80 +    using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
   12.81 +    by (metis antisym_conv)
   12.82    obtain C where C: "vs2.independent C" and fB_C: "f ` B \<subseteq> vs2.span C" "C \<subseteq> f ` B"
   12.83 -    using vs2.maximal_independent_subset[of "f ` B"] by auto
   12.84 +    using vs2.maximal_independent_subset[of "f ` B"] by metis
   12.85    then have "\<forall>v\<in>C. \<exists>b\<in>B. v = f b" by auto
   12.86    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
   12.87    show ?thesis
   12.88 @@ -917,7 +919,8 @@
   12.89          done
   12.90        show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
   12.91        have "vs2.span (f ` B) = vs2.span C"
   12.92 -        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)
   12.93 +        using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
   12.94 +        by auto
   12.95        then show "v \<in> vs2.span C"
   12.96          using v linear_span_image[OF lf, of B] by (simp add: V_eq)
   12.97        show "(f \<circ> p.construct C g) b = id b" if b: "b \<in> C" for b
   12.98 @@ -935,7 +938,8 @@
   12.99    by (auto simp: linear_iff_module_hom)
  12.100  
  12.101  lemma linear_injective_left_inverse: "linear s1 s2 f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> g \<circ> f = id"
  12.102 -  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff)
  12.103 +  using linear_inj_on_left_inverse[of f UNIV]
  12.104 +  by force
  12.105  
  12.106  lemma linear_surj_right_inverse:
  12.107    assumes lf: "linear s1 s2 f"
  12.108 @@ -946,7 +950,7 @@
  12.109  
  12.110  lemma linear_surjective_right_inverse: "linear s1 s2 f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> f \<circ> g = id"
  12.111    using linear_surj_right_inverse[of f UNIV UNIV]
  12.112 -  by (auto simp: vs1.span_UNIV vs2.span_UNIV fun_eq_iff)
  12.113 +  by (auto simp: fun_eq_iff)
  12.114  
  12.115  end
  12.116  
  12.117 @@ -1025,7 +1029,7 @@
  12.118      have 2: "span (insert x S) \<subseteq> span (insert x B)"
  12.119        by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
  12.120      have 3: "independent (insert x B)"
  12.121 -      by (metis B independent_insert span_subspace subspace_span False)
  12.122 +      by (metis B(1-3) independent_insert span_subspace subspace_span False)
  12.123      have "dim (span (insert x S)) = Suc (dim S)"
  12.124        apply (rule dim_unique [OF 1 2 3])
  12.125        by (metis B False card_insert_disjoint dim_span finiteI_independent span_base span_eq span_span)
  12.126 @@ -1055,7 +1059,7 @@
  12.127        case True
  12.128        have "dim S = dim T"
  12.129          apply (rule span_eq_dim [OF subset_antisym [OF True]])
  12.130 -        by (simp add: \<open>T \<subseteq> span S\<close> span_minimal subspace_span)
  12.131 +        by (simp add: \<open>T \<subseteq> span S\<close> span_minimal)
  12.132        then show ?thesis
  12.133          using Suc.prems \<open>dim T = n\<close> by linarith
  12.134      next
  12.135 @@ -1066,7 +1070,7 @@
  12.136          by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span)
  12.137        with \<open>dim T = n\<close>  \<open>subspace T\<close> y show ?thesis
  12.138          apply (rule_tac x="span(insert y T)" in exI)
  12.139 -        apply (auto simp: dim_insert dim_span subspace_span)
  12.140 +        apply (auto simp: dim_insert)
  12.141          using span_eq_iff by blast
  12.142      qed
  12.143    qed
  12.144 @@ -1076,12 +1080,12 @@
  12.145  lemma basis_subspace_exists:
  12.146    assumes "subspace S"
  12.147    obtains B where "finite B" "B \<subseteq> S" "independent B" "span B = S" "card B = dim S"
  12.148 -by (metis assms span_subspace basis_exists independent_imp_finite)
  12.149 +  by (metis assms span_subspace basis_exists finiteI_independent)
  12.150  
  12.151  lemma dim_mono: assumes "V \<subseteq> span W" shows "dim V \<le> dim W"
  12.152  proof -
  12.153    obtain B where "independent B" "B \<subseteq> W" "W \<subseteq> span B"
  12.154 -    using maximal_independent_subset[of W] by auto
  12.155 +    using maximal_independent_subset[of W] by force
  12.156    with dim_le_card[of V B] assms independent_span_bound[of Basis B] basis_card_eq_dim[of B W]
  12.157      span_mono[of B W] span_minimal[OF _ subspace_span, of W B]
  12.158    show ?thesis
  12.159 @@ -1093,13 +1097,10 @@
  12.160  
  12.161  lemma dim_eq_0 [simp]:
  12.162    "dim S = 0 \<longleftrightarrow> S \<subseteq> {0}"
  12.163 -  using basis_exists finiteI_independent
  12.164 -  apply safe
  12.165 -  subgoal by fastforce
  12.166 -  by (metis dim_singleton dim_subset le_0_eq)
  12.167 +  by (metis basis_exists card_eq_0_iff dim_span finiteI_independent span_empty subset_empty subset_singletonD)
  12.168  
  12.169  lemma dim_UNIV[simp]: "dim UNIV = card Basis"
  12.170 -  using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis span_UNIV)
  12.171 +  using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis)
  12.172  
  12.173  lemma independent_card_le_dim: assumes "B \<subseteq> V" and "independent B" shows "card B \<le> dim V"
  12.174    by (subst dim_eq_card[symmetric, OF refl \<open>independent B\<close>]) (rule dim_subset[OF \<open>B \<subseteq> V\<close>])
  12.175 @@ -1191,7 +1192,7 @@
  12.176  
  12.177  corollary dim_eq_span:
  12.178    shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
  12.179 -  by (simp add: dim_span span_mono subspace_dim_equal subspace_span)
  12.180 +  by (simp add: span_mono subspace_dim_equal)
  12.181  
  12.182  lemma dim_psubset:
  12.183    "span S \<subset> span T \<Longrightarrow> dim S < dim T"
  12.184 @@ -1380,7 +1381,7 @@
  12.185    interpret linear s1 s2 f by fact
  12.186    have *: "card (f ` B1) \<le> vs2.dim UNIV"
  12.187      using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf
  12.188 -    by (auto simp: vs1.span_Basis vs1.span_UNIV vs1.independent_Basis eq
  12.189 +    by (auto simp: vs1.span_Basis vs1.independent_Basis eq
  12.190          simp del: vs2.dim_UNIV
  12.191          intro!: card_image_le)
  12.192    have indep_fB: "vs2.independent (f ` B1)"
  12.193 @@ -1575,7 +1576,7 @@
  12.194      from B(2) have fB: "finite B"
  12.195        using finiteI_independent by auto
  12.196      have Uspan: "UNIV \<subseteq> span (f ` B)"
  12.197 -      by (simp add: B(3) lf sf spanning_surjective_image)
  12.198 +      by (simp add: B(3) lf linear_spanning_surjective_image sf)
  12.199      have fBi: "independent (f ` B)"
  12.200      proof (rule card_le_dim_spanning)
  12.201        show "card (f ` B) \<le> dim ?U"
  12.202 @@ -1593,7 +1594,7 @@
  12.203      have "x = 0" by blast
  12.204    }
  12.205    then show ?thesis
  12.206 -    unfolding linear_injective_0[OF lf] using B(3) by blast
  12.207 +    unfolding linear_inj_iff_eq_0[OF lf] using B(3) by blast
  12.208  qed
  12.209  
  12.210  lemma linear_inverse_left:
  12.211 @@ -1629,7 +1630,7 @@
  12.212      by blast
  12.213    have "h = g"
  12.214      by (metis gf h isomorphism_expand left_right_inverse_eq)
  12.215 -  with \<open>linear h\<close> show ?thesis by blast
  12.216 +  with \<open>linear scale scale h\<close> show ?thesis by blast
  12.217  qed
  12.218  
  12.219  lemma inj_linear_imp_inv_linear:
  12.220 @@ -1668,10 +1669,10 @@
  12.221  proof -
  12.222    from vs1.basis_exists[of S] vs1.finiteI_independent
  12.223    obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" and fB: "finite B"
  12.224 -    by blast
  12.225 +    by metis
  12.226    from vs2.basis_exists[of T] vs2.finiteI_independent
  12.227    obtain C where C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T" and fC: "finite C"
  12.228 -    by blast
  12.229 +    by metis
  12.230    from B(4) C(4) card_le_inj[of B C] d
  12.231    obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
  12.232      by auto