src/HOL/Analysis/Linear_Algebra.thy
changeset 68072 493b818e8e10
parent 67982 7643b005b29a
child 68073 fad29d2a17a5
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Apr 18 21:12:50 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 13:49:38 2018 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4    show "f (a + b) = f a + f b" by (rule f.add)
     1.5    show "f (a - b) = f a - f b" by (rule f.diff)
     1.6    show "f 0 = 0" by (rule f.zero)
     1.7 -  show "f (- a) = - f a" by (rule f.minus)
     1.8 -  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
     1.9 +  show "f (- a) = - f a" by (rule f.neg)
    1.10 +  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale)
    1.11  qed
    1.12  
    1.13  lemma bounded_linearI:
    1.14 @@ -34,1312 +34,6 @@
    1.15    shows "bounded_linear f"
    1.16    using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
    1.17  
    1.18 -subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
    1.19 -
    1.20 -definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
    1.21 -  where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
    1.22 -
    1.23 -lemma hull_same: "S s \<Longrightarrow> S hull s = s"
    1.24 -  unfolding hull_def by auto
    1.25 -
    1.26 -lemma hull_in: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> S (S hull s)"
    1.27 -  unfolding hull_def Ball_def by auto
    1.28 -
    1.29 -lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
    1.30 -  using hull_same[of S s] hull_in[of S s] by metis
    1.31 -
    1.32 -lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
    1.33 -  unfolding hull_def by blast
    1.34 -
    1.35 -lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
    1.36 -  unfolding hull_def by blast
    1.37 -
    1.38 -lemma hull_mono: "s \<subseteq> t \<Longrightarrow> (S hull s) \<subseteq> (S hull t)"
    1.39 -  unfolding hull_def by blast
    1.40 -
    1.41 -lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x \<Longrightarrow> (T hull s) \<subseteq> (S hull s)"
    1.42 -  unfolding hull_def by blast
    1.43 -
    1.44 -lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (S hull s) \<subseteq> t"
    1.45 -  unfolding hull_def by blast
    1.46 -
    1.47 -lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
    1.48 -  unfolding hull_def by blast
    1.49 -
    1.50 -lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
    1.51 -  unfolding hull_def by auto
    1.52 -
    1.53 -lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
    1.54 -  unfolding hull_def by auto
    1.55 -
    1.56 -lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
    1.57 -  using hull_minimal[of S "{x. P x}" Q]
    1.58 -  by (auto simp add: subset_eq)
    1.59 -
    1.60 -lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
    1.61 -  by (metis hull_subset subset_eq)
    1.62 -
    1.63 -lemma hull_Un_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
    1.64 -  unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
    1.65 -
    1.66 -lemma hull_Un:
    1.67 -  assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
    1.68 -  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
    1.69 -  apply (rule equalityI)
    1.70 -  apply (meson hull_mono hull_subset sup.mono)
    1.71 -  by (metis hull_Un_subset hull_hull hull_mono)
    1.72 -
    1.73 -lemma hull_Un_left: "P hull (S \<union> T) = P hull (P hull S \<union> T)"
    1.74 -  apply (rule equalityI)
    1.75 -   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
    1.76 -  by (metis Un_subset_iff hull_hull hull_mono hull_subset)
    1.77 -
    1.78 -lemma hull_Un_right: "P hull (S \<union> T) = P hull (S \<union> P hull T)"
    1.79 -  by (metis hull_Un_left sup.commute)
    1.80 -
    1.81 -lemma hull_insert:
    1.82 -   "P hull (insert a S) = P hull (insert a (P hull S))"
    1.83 -  by (metis hull_Un_right insert_is_Un)
    1.84 -
    1.85 -lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
    1.86 -  unfolding hull_def by blast
    1.87 -
    1.88 -lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
    1.89 -  by (metis hull_redundant_eq)
    1.90 -
    1.91 -subsection \<open>Linear functions.\<close>
    1.92 -
    1.93 -lemma%important linear_iff:
    1.94 -  "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
    1.95 -  (is "linear f \<longleftrightarrow> ?rhs")
    1.96 -proof%unimportant
    1.97 -  assume "linear f"
    1.98 -  then interpret f: linear f .
    1.99 -  show "?rhs" by (simp add: f.add f.scaleR)
   1.100 -next
   1.101 -  assume "?rhs"
   1.102 -  then show "linear f" by unfold_locales simp_all
   1.103 -qed
   1.104 -
   1.105 -lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
   1.106 -  by (simp add: linear_iff algebra_simps)
   1.107 -
   1.108 -lemma linear_compose_scaleR: "linear f \<Longrightarrow> linear (\<lambda>x. f x *\<^sub>R c)"
   1.109 -  by (simp add: linear_iff scaleR_add_left)
   1.110 -
   1.111 -lemma linear_compose_neg: "linear f \<Longrightarrow> linear (\<lambda>x. - f x)"
   1.112 -  by (simp add: linear_iff)
   1.113 -
   1.114 -lemma linear_compose_add: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x + g x)"
   1.115 -  by (simp add: linear_iff algebra_simps)
   1.116 -
   1.117 -lemma linear_compose_sub: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (\<lambda>x. f x - g x)"
   1.118 -  by (simp add: linear_iff algebra_simps)
   1.119 -
   1.120 -lemma linear_compose: "linear f \<Longrightarrow> linear g \<Longrightarrow> linear (g \<circ> f)"
   1.121 -  by (simp add: linear_iff)
   1.122 -
   1.123 -lemma linear_id: "linear id"
   1.124 -  by (simp add: linear_iff id_def)
   1.125 -
   1.126 -lemma linear_zero: "linear (\<lambda>x. 0)"
   1.127 -  by (simp add: linear_iff)
   1.128 -
   1.129 -lemma linear_uminus: "linear uminus"
   1.130 -by (simp add: linear_iff)
   1.131 -
   1.132 -lemma linear_compose_sum:
   1.133 -  assumes lS: "\<forall>a \<in> S. linear (f a)"
   1.134 -  shows "linear (\<lambda>x. sum (\<lambda>a. f a x) S)"
   1.135 -proof (cases "finite S")
   1.136 -  case True
   1.137 -  then show ?thesis
   1.138 -    using lS by induct (simp_all add: linear_zero linear_compose_add)
   1.139 -next
   1.140 -  case False
   1.141 -  then show ?thesis
   1.142 -    by (simp add: linear_zero)
   1.143 -qed
   1.144 -
   1.145 -lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
   1.146 -  unfolding linear_iff
   1.147 -  apply clarsimp
   1.148 -  apply (erule allE[where x="0::'a"])
   1.149 -  apply simp
   1.150 -  done
   1.151 -
   1.152 -lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
   1.153 -  by (rule linear.scaleR)
   1.154 -
   1.155 -lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
   1.156 -  using linear_cmul [where c="-1"] by simp
   1.157 -
   1.158 -lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
   1.159 -  by (metis linear_iff)
   1.160 -
   1.161 -lemma linear_diff: "linear f \<Longrightarrow> f (x - y) = f x - f y"
   1.162 -  using linear_add [of f x "- y"] by (simp add: linear_neg)
   1.163 -
   1.164 -lemma linear_sum:
   1.165 -  assumes f: "linear f"
   1.166 -  shows "f (sum g S) = sum (f \<circ> g) S"
   1.167 -proof (cases "finite S")
   1.168 -  case True
   1.169 -  then show ?thesis
   1.170 -    by induct (simp_all add: linear_0 [OF f] linear_add [OF f])
   1.171 -next
   1.172 -  case False
   1.173 -  then show ?thesis
   1.174 -    by (simp add: linear_0 [OF f])
   1.175 -qed
   1.176 -
   1.177 -lemma linear_sum_mul:
   1.178 -  assumes lin: "linear f"
   1.179 -  shows "f (sum (\<lambda>i. c i *\<^sub>R v i) S) = sum (\<lambda>i. c i *\<^sub>R f (v i)) S"
   1.180 -  using linear_sum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
   1.181 -  by simp
   1.182 -
   1.183 -lemma linear_injective_0:
   1.184 -  assumes lin: "linear f"
   1.185 -  shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
   1.186 -proof -
   1.187 -  have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)"
   1.188 -    by (simp add: inj_on_def)
   1.189 -  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)"
   1.190 -    by simp
   1.191 -  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
   1.192 -    by (simp add: linear_diff[OF lin])
   1.193 -  also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)"
   1.194 -    by auto
   1.195 -  finally show ?thesis .
   1.196 -qed
   1.197 -
   1.198 -lemma linear_scaleR  [simp]: "linear (\<lambda>x. scaleR c x)"
   1.199 -  by (simp add: linear_iff scaleR_add_right)
   1.200 -
   1.201 -lemma linear_scaleR_left [simp]: "linear (\<lambda>r. scaleR r x)"
   1.202 -  by (simp add: linear_iff scaleR_add_left)
   1.203 -
   1.204 -lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
   1.205 -  by (simp add: inj_on_def)
   1.206 -
   1.207 -lemma linear_add_cmul:
   1.208 -  assumes "linear f"
   1.209 -  shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
   1.210 -  using linear_add[of f] linear_cmul[of f] assms by simp
   1.211 -
   1.212 -subsection \<open>Subspaces of vector spaces\<close>
   1.213 -
   1.214 -definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
   1.215 -  where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
   1.216 -
   1.217 -definition%important (in real_vector) "span S = (subspace hull S)"
   1.218 -definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
   1.219 -abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
   1.220 -
   1.221 -text \<open>Closure properties of subspaces.\<close>
   1.222 -
   1.223 -lemma subspace_UNIV[simp]: "subspace UNIV"
   1.224 -  by (simp add: subspace_def)
   1.225 -
   1.226 -lemma (in real_vector) subspace_0: "subspace S \<Longrightarrow> 0 \<in> S"
   1.227 -  by (metis subspace_def)
   1.228 -
   1.229 -lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
   1.230 -  by (metis subspace_def)
   1.231 -
   1.232 -lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"
   1.233 -  by (metis subspace_def)
   1.234 -
   1.235 -lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
   1.236 -  by (metis scaleR_minus1_left subspace_mul)
   1.237 -
   1.238 -lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   1.239 -  using subspace_add [of S x "- y"] by (simp add: subspace_neg)
   1.240 -
   1.241 -lemma (in real_vector) subspace_sum:
   1.242 -  assumes sA: "subspace A"
   1.243 -    and f: "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
   1.244 -  shows "sum f B \<in> A"
   1.245 -proof (cases "finite B")
   1.246 -  case True
   1.247 -  then show ?thesis
   1.248 -    using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
   1.249 -qed (simp add: subspace_0 [OF sA])
   1.250 -
   1.251 -lemma subspace_trivial [iff]: "subspace {0}"
   1.252 -  by (simp add: subspace_def)
   1.253 -
   1.254 -lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
   1.255 -  by (simp add: subspace_def)
   1.256 -
   1.257 -lemma subspace_Times: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<times> B)"
   1.258 -  unfolding subspace_def zero_prod_def by simp
   1.259 -
   1.260 -lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
   1.261 -apply (simp add: subspace_def)
   1.262 -apply (intro conjI impI allI)
   1.263 -  using add.right_neutral apply blast
   1.264 - apply clarify
   1.265 - apply (metis add.assoc add.left_commute)
   1.266 -using scaleR_add_right by blast
   1.267 -
   1.268 -subsection%unimportant \<open>Properties of span\<close>
   1.269 -
   1.270 -lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
   1.271 -  by (metis span_def hull_mono)
   1.272 -
   1.273 -lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
   1.274 -  unfolding span_def
   1.275 -  apply (rule hull_in)
   1.276 -  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
   1.277 -  apply auto
   1.278 -  done
   1.279 -
   1.280 -lemma (in real_vector) span_clauses:
   1.281 -  "a \<in> S \<Longrightarrow> a \<in> span S"
   1.282 -  "0 \<in> span S"
   1.283 -  "x\<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
   1.284 -  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
   1.285 -  by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+
   1.286 -
   1.287 -lemma span_unique:
   1.288 -  "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
   1.289 -  unfolding span_def by (rule hull_unique)
   1.290 -
   1.291 -lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
   1.292 -  unfolding span_def by (rule hull_minimal)
   1.293 -
   1.294 -lemma span_UNIV [simp]: "span UNIV = UNIV"
   1.295 -  by (intro span_unique) auto
   1.296 -
   1.297 -lemma (in real_vector) span_induct:
   1.298 -  assumes x: "x \<in> span S"
   1.299 -    and P: "subspace (Collect P)"
   1.300 -    and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
   1.301 -  shows "P x"
   1.302 -proof -
   1.303 -  from SP have SP': "S \<subseteq> Collect P"
   1.304 -    by (simp add: subset_eq)
   1.305 -  from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
   1.306 -  show ?thesis
   1.307 -    using subset_eq by force
   1.308 -qed
   1.309 -
   1.310 -lemma span_empty[simp]: "span {} = {0}"
   1.311 -  apply (simp add: span_def)
   1.312 -  apply (rule hull_unique)
   1.313 -  apply (auto simp add: subspace_def)
   1.314 -  done
   1.315 -
   1.316 -lemma (in real_vector) independent_empty [iff]: "independent {}"
   1.317 -  by (simp add: dependent_def)
   1.318 -
   1.319 -lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0"
   1.320 -  unfolding dependent_def by auto
   1.321 -
   1.322 -lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
   1.323 -  apply (clarsimp simp add: dependent_def span_mono)
   1.324 -  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
   1.325 -  apply force
   1.326 -  apply (rule span_mono)
   1.327 -  apply auto
   1.328 -  done
   1.329 -
   1.330 -lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
   1.331 -  by (metis order_antisym span_def hull_minimal)
   1.332 -
   1.333 -lemma (in real_vector) span_induct':
   1.334 -  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
   1.335 -  unfolding span_def by (rule hull_induct) auto
   1.336 -
   1.337 -inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
   1.338 -where
   1.339 -  span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
   1.340 -| span_induct_alt_help_S:
   1.341 -    "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow>
   1.342 -      (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
   1.343 -
   1.344 -lemma span_induct_alt':
   1.345 -  assumes h0: "h 0"
   1.346 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
   1.347 -  shows "\<forall>x \<in> span S. h x"
   1.348 -proof -
   1.349 -  {
   1.350 -    fix x :: 'a
   1.351 -    assume x: "x \<in> span_induct_alt_help S"
   1.352 -    have "h x"
   1.353 -      apply (rule span_induct_alt_help.induct[OF x])
   1.354 -      apply (rule h0)
   1.355 -      apply (rule hS)
   1.356 -      apply assumption
   1.357 -      apply assumption
   1.358 -      done
   1.359 -  }
   1.360 -  note th0 = this
   1.361 -  {
   1.362 -    fix x
   1.363 -    assume x: "x \<in> span S"
   1.364 -    have "x \<in> span_induct_alt_help S"
   1.365 -    proof (rule span_induct[where x=x and S=S])
   1.366 -      show "x \<in> span S" by (rule x)
   1.367 -    next
   1.368 -      fix x
   1.369 -      assume xS: "x \<in> S"
   1.370 -      from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
   1.371 -      show "x \<in> span_induct_alt_help S"
   1.372 -        by simp
   1.373 -    next
   1.374 -      have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
   1.375 -      moreover
   1.376 -      {
   1.377 -        fix x y
   1.378 -        assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
   1.379 -        from h have "(x + y) \<in> span_induct_alt_help S"
   1.380 -          apply (induct rule: span_induct_alt_help.induct)
   1.381 -          apply simp
   1.382 -          unfolding add.assoc
   1.383 -          apply (rule span_induct_alt_help_S)
   1.384 -          apply assumption
   1.385 -          apply simp
   1.386 -          done
   1.387 -      }
   1.388 -      moreover
   1.389 -      {
   1.390 -        fix c x
   1.391 -        assume xt: "x \<in> span_induct_alt_help S"
   1.392 -        then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
   1.393 -          apply (induct rule: span_induct_alt_help.induct)
   1.394 -          apply (simp add: span_induct_alt_help_0)
   1.395 -          apply (simp add: scaleR_right_distrib)
   1.396 -          apply (rule span_induct_alt_help_S)
   1.397 -          apply assumption
   1.398 -          apply simp
   1.399 -          done }
   1.400 -      ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
   1.401 -        unfolding subspace_def Ball_def by blast
   1.402 -    qed
   1.403 -  }
   1.404 -  with th0 show ?thesis by blast
   1.405 -qed
   1.406 -
   1.407 -lemma span_induct_alt:
   1.408 -  assumes h0: "h 0"
   1.409 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
   1.410 -    and x: "x \<in> span S"
   1.411 -  shows "h x"
   1.412 -  using span_induct_alt'[of h S] h0 hS x by blast
   1.413 -
   1.414 -text \<open>Individual closure properties.\<close>
   1.415 -
   1.416 -lemma span_span: "span (span A) = span A"
   1.417 -  unfolding span_def hull_hull ..
   1.418 -
   1.419 -lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
   1.420 -  by (metis span_clauses(1))
   1.421 -
   1.422 -lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
   1.423 -  by (metis subspace_span subspace_0)
   1.424 -
   1.425 -lemma span_inc: "S \<subseteq> span S"
   1.426 -  by (metis subset_eq span_superset)
   1.427 -
   1.428 -lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
   1.429 -  using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
   1.430 -  by (auto simp add: span_span)
   1.431 -
   1.432 -lemma (in real_vector) dependent_0:
   1.433 -  assumes "0 \<in> A"
   1.434 -  shows "dependent A"
   1.435 -  unfolding dependent_def
   1.436 -  using assms span_0
   1.437 -  by blast
   1.438 -
   1.439 -lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
   1.440 -  by (metis subspace_add subspace_span)
   1.441 -
   1.442 -lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
   1.443 -  by (metis subspace_span subspace_mul)
   1.444 -
   1.445 -lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
   1.446 -  by (metis subspace_neg subspace_span)
   1.447 -
   1.448 -lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
   1.449 -  by (metis subspace_span subspace_diff)
   1.450 -
   1.451 -lemma (in real_vector) span_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> sum f A \<in> span S"
   1.452 -  by (rule subspace_sum [OF subspace_span])
   1.453 -
   1.454 -lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
   1.455 -  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
   1.456 -
   1.457 -text \<open>The key breakdown property.\<close>
   1.458 -
   1.459 -lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
   1.460 -proof (rule span_unique)
   1.461 -  show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
   1.462 -    by (fast intro: scaleR_one [symmetric])
   1.463 -  show "subspace (range (\<lambda>k. k *\<^sub>R x))"
   1.464 -    unfolding subspace_def
   1.465 -    by (auto intro: scaleR_add_left [symmetric])
   1.466 -next
   1.467 -  fix T
   1.468 -  assume "{x} \<subseteq> T" and "subspace T"
   1.469 -  then show "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
   1.470 -    unfolding subspace_def by auto
   1.471 -qed
   1.472 -
   1.473 -text \<open>Mapping under linear image.\<close>
   1.474 -
   1.475 -lemma subspace_linear_image:
   1.476 -  assumes lf: "linear f"
   1.477 -    and sS: "subspace S"
   1.478 -  shows "subspace (f ` S)"
   1.479 -  using lf sS linear_0[OF lf]
   1.480 -  unfolding linear_iff subspace_def
   1.481 -  apply (auto simp add: image_iff)
   1.482 -  apply (rule_tac x="x + y" in bexI)
   1.483 -  apply auto
   1.484 -  apply (rule_tac x="c *\<^sub>R x" in bexI)
   1.485 -  apply auto
   1.486 -  done
   1.487 -
   1.488 -lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
   1.489 -  by (auto simp add: subspace_def linear_iff linear_0[of f])
   1.490 -
   1.491 -lemma subspace_linear_preimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace {x. f x \<in> S}"
   1.492 -  by (auto simp add: subspace_def linear_iff linear_0[of f])
   1.493 -
   1.494 -lemma span_linear_image:
   1.495 -  assumes lf: "linear f"
   1.496 -  shows "span (f ` S) = f ` span S"
   1.497 -proof (rule span_unique)
   1.498 -  show "f ` S \<subseteq> f ` span S"
   1.499 -    by (intro image_mono span_inc)
   1.500 -  show "subspace (f ` span S)"
   1.501 -    using lf subspace_span by (rule subspace_linear_image)
   1.502 -next
   1.503 -  fix T
   1.504 -  assume "f ` S \<subseteq> T" and "subspace T"
   1.505 -  then show "f ` span S \<subseteq> T"
   1.506 -    unfolding image_subset_iff_subset_vimage
   1.507 -    by (intro span_minimal subspace_linear_vimage lf)
   1.508 -qed
   1.509 -
   1.510 -lemma spans_image:
   1.511 -  assumes lf: "linear f"
   1.512 -    and VB: "V \<subseteq> span B"
   1.513 -  shows "f ` V \<subseteq> span (f ` B)"
   1.514 -  unfolding span_linear_image[OF lf] by (metis VB image_mono)
   1.515 -
   1.516 -lemma span_Un: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
   1.517 -proof (rule span_unique)
   1.518 -  show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
   1.519 -    by safe (force intro: span_clauses)+
   1.520 -next
   1.521 -  have "linear (\<lambda>(a, b). a + b)"
   1.522 -    by (simp add: linear_iff scaleR_add_right)
   1.523 -  moreover have "subspace (span A \<times> span B)"
   1.524 -    by (intro subspace_Times subspace_span)
   1.525 -  ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
   1.526 -    by (rule subspace_linear_image)
   1.527 -next
   1.528 -  fix T
   1.529 -  assume "A \<union> B \<subseteq> T" and "subspace T"
   1.530 -  then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
   1.531 -    by (auto intro!: subspace_add elim: span_induct)
   1.532 -qed
   1.533 -
   1.534 -lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
   1.535 -proof -
   1.536 -  have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
   1.537 -    unfolding span_Un span_singleton
   1.538 -    apply safe
   1.539 -    apply (rule_tac x=k in exI, simp)
   1.540 -    apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
   1.541 -    apply auto
   1.542 -    done
   1.543 -  then show ?thesis by simp
   1.544 -qed
   1.545 -
   1.546 -lemma span_breakdown:
   1.547 -  assumes bS: "b \<in> S"
   1.548 -    and aS: "a \<in> span S"
   1.549 -  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
   1.550 -  using assms span_insert [of b "S - {b}"]
   1.551 -  by (simp add: insert_absorb)
   1.552 -
   1.553 -lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. x - k *\<^sub>R a \<in> span S)"
   1.554 -  by (simp add: span_insert)
   1.555 -
   1.556 -text \<open>Hence some "reversal" results.\<close>
   1.557 -
   1.558 -lemma in_span_insert:
   1.559 -  assumes a: "a \<in> span (insert b S)"
   1.560 -    and na: "a \<notin> span S"
   1.561 -  shows "b \<in> span (insert a S)"
   1.562 -proof -
   1.563 -  from a obtain k where k: "a - k *\<^sub>R b \<in> span S"
   1.564 -    unfolding span_insert by fast
   1.565 -  show ?thesis
   1.566 -  proof (cases "k = 0")
   1.567 -    case True
   1.568 -    with k have "a \<in> span S" by simp
   1.569 -    with na show ?thesis by simp
   1.570 -  next
   1.571 -    case False
   1.572 -    from k have "(- inverse k) *\<^sub>R (a - k *\<^sub>R b) \<in> span S"
   1.573 -      by (rule span_mul)
   1.574 -    then have "b - inverse k *\<^sub>R a \<in> span S"
   1.575 -      using \<open>k \<noteq> 0\<close> by (simp add: scaleR_diff_right)
   1.576 -    then show ?thesis
   1.577 -      unfolding span_insert by fast
   1.578 -  qed
   1.579 -qed
   1.580 -
   1.581 -lemma in_span_delete:
   1.582 -  assumes a: "a \<in> span S"
   1.583 -    and na: "a \<notin> span (S - {b})"
   1.584 -  shows "b \<in> span (insert a (S - {b}))"
   1.585 -  apply (rule in_span_insert)
   1.586 -  apply (rule set_rev_mp)
   1.587 -  apply (rule a)
   1.588 -  apply (rule span_mono)
   1.589 -  apply blast
   1.590 -  apply (rule na)
   1.591 -  done
   1.592 -
   1.593 -text \<open>Transitivity property.\<close>
   1.594 -
   1.595 -lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
   1.596 -  unfolding span_def by (rule hull_redundant)
   1.597 -
   1.598 -lemma span_trans:
   1.599 -  assumes x: "x \<in> span S"
   1.600 -    and y: "y \<in> span (insert x S)"
   1.601 -  shows "y \<in> span S"
   1.602 -  using assms by (simp only: span_redundant)
   1.603 -
   1.604 -lemma span_insert_0[simp]: "span (insert 0 S) = span S"
   1.605 -  by (simp only: span_redundant span_0)
   1.606 -
   1.607 -text \<open>An explicit expansion is sometimes needed.\<close>
   1.608 -
   1.609 -lemma span_explicit:
   1.610 -  "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
   1.611 -  (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
   1.612 -proof -
   1.613 -  {
   1.614 -    fix x
   1.615 -    assume "?h x"
   1.616 -    then obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
   1.617 -      by blast
   1.618 -    then have "x \<in> span P"
   1.619 -      by (auto intro: span_sum span_mul span_superset)
   1.620 -  }
   1.621 -  moreover
   1.622 -  have "\<forall>x \<in> span P. ?h x"
   1.623 -  proof (rule span_induct_alt')
   1.624 -    show "?h 0"
   1.625 -      by (rule exI[where x="{}"], simp)
   1.626 -  next
   1.627 -    fix c x y
   1.628 -    assume x: "x \<in> P"
   1.629 -    assume hy: "?h y"
   1.630 -    from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
   1.631 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
   1.632 -    let ?S = "insert x S"
   1.633 -    let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
   1.634 -    from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
   1.635 -      by blast+
   1.636 -    have "?Q ?S ?u (c*\<^sub>R x + y)"
   1.637 -    proof cases
   1.638 -      assume xS: "x \<in> S"
   1.639 -      have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = (\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
   1.640 -        using xS by (simp add: sum.remove [OF fS xS] insert_absorb)
   1.641 -      also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x"
   1.642 -        by (simp add: sum.remove [OF fS xS] algebra_simps)
   1.643 -      also have "\<dots> = c*\<^sub>R x + y"
   1.644 -        by (simp add: add.commute u)
   1.645 -      finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" .
   1.646 -      then show ?thesis using th0 by blast
   1.647 -    next
   1.648 -      assume xS: "x \<notin> S"
   1.649 -      have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
   1.650 -        unfolding u[symmetric]
   1.651 -        apply (rule sum.cong)
   1.652 -        using xS
   1.653 -        apply auto
   1.654 -        done
   1.655 -      show ?thesis using fS xS th0
   1.656 -        by (simp add: th00 add.commute cong del: if_weak_cong)
   1.657 -    qed
   1.658 -    then show "?h (c*\<^sub>R x + y)"
   1.659 -      by fast
   1.660 -  qed
   1.661 -  ultimately show ?thesis by blast
   1.662 -qed
   1.663 -
   1.664 -lemma dependent_explicit:
   1.665 -  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0))"
   1.666 -  (is "?lhs = ?rhs")
   1.667 -proof -
   1.668 -  {
   1.669 -    assume dP: "dependent P"
   1.670 -    then obtain a S u where aP: "a \<in> P" and fS: "finite S"
   1.671 -      and SP: "S \<subseteq> P - {a}" and ua: "sum (\<lambda>v. u v *\<^sub>R v) S = a"
   1.672 -      unfolding dependent_def span_explicit by blast
   1.673 -    let ?S = "insert a S"
   1.674 -    let ?u = "\<lambda>y. if y = a then - 1 else u y"
   1.675 -    let ?v = a
   1.676 -    from aP SP have aS: "a \<notin> S"
   1.677 -      by blast
   1.678 -    from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
   1.679 -      by auto
   1.680 -    have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
   1.681 -      using fS aS
   1.682 -      apply simp
   1.683 -      apply (subst (2) ua[symmetric])
   1.684 -      apply (rule sum.cong)
   1.685 -      apply auto
   1.686 -      done
   1.687 -    with th0 have ?rhs by fast
   1.688 -  }
   1.689 -  moreover
   1.690 -  {
   1.691 -    fix S u v
   1.692 -    assume fS: "finite S"
   1.693 -      and SP: "S \<subseteq> P"
   1.694 -      and vS: "v \<in> S"
   1.695 -      and uv: "u v \<noteq> 0"
   1.696 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S = 0"
   1.697 -    let ?a = v
   1.698 -    let ?S = "S - {v}"
   1.699 -    let ?u = "\<lambda>i. (- u i) / u v"
   1.700 -    have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P"
   1.701 -      using fS SP vS by auto
   1.702 -    have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S =
   1.703 -      sum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
   1.704 -      using fS vS uv by (simp add: sum_diff1 field_simps)
   1.705 -    also have "\<dots> = ?a"
   1.706 -      unfolding scaleR_right.sum [symmetric] u using uv by simp
   1.707 -    finally have "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
   1.708 -    with th0 have ?lhs
   1.709 -      unfolding dependent_def span_explicit
   1.710 -      apply -
   1.711 -      apply (rule bexI[where x= "?a"])
   1.712 -      apply (simp_all del: scaleR_minus_left)
   1.713 -      apply (rule exI[where x= "?S"])
   1.714 -      apply (auto simp del: scaleR_minus_left)
   1.715 -      done
   1.716 -  }
   1.717 -  ultimately show ?thesis by blast
   1.718 -qed
   1.719 -
   1.720 -lemma dependent_finite:
   1.721 -  assumes "finite S"
   1.722 -    shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = 0)"
   1.723 -           (is "?lhs = ?rhs")
   1.724 -proof
   1.725 -  assume ?lhs
   1.726 -  then obtain T u v
   1.727 -         where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *\<^sub>R v) = 0"
   1.728 -    by (force simp: dependent_explicit)
   1.729 -  with assms show ?rhs
   1.730 -    apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
   1.731 -    apply (auto simp: sum.mono_neutral_right)
   1.732 -    done
   1.733 -next
   1.734 -  assume ?rhs  with assms show ?lhs
   1.735 -    by (fastforce simp add: dependent_explicit)
   1.736 -qed
   1.737 -
   1.738 -lemma span_alt:
   1.739 -  "span B = {(\<Sum>x | f x \<noteq> 0. f x *\<^sub>R x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}"
   1.740 -  unfolding span_explicit
   1.741 -  apply safe
   1.742 -  subgoal for x S u
   1.743 -    by (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
   1.744 -        (auto intro!: sum.mono_neutral_cong_right)
   1.745 -  apply auto
   1.746 -  done
   1.747 -
   1.748 -lemma dependent_alt:
   1.749 -  "dependent B \<longleftrightarrow>
   1.750 -    (\<exists>X. finite {x. X x \<noteq> 0} \<and> {x. X x \<noteq> 0} \<subseteq> B \<and> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<and> (\<exists>x. X x \<noteq> 0))"
   1.751 -  unfolding dependent_explicit
   1.752 -  apply safe
   1.753 -  subgoal for S u v
   1.754 -    apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
   1.755 -    apply (subst sum.mono_neutral_cong_left[where T=S])
   1.756 -    apply (auto intro!: sum.mono_neutral_cong_right cong: rev_conj_cong)
   1.757 -    done
   1.758 -  apply auto
   1.759 -  done
   1.760 -
   1.761 -lemma independent_alt:
   1.762 -  "independent B \<longleftrightarrow>
   1.763 -    (\<forall>X. finite {x. X x \<noteq> 0} \<longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<longrightarrow> (\<forall>x. X x = 0))"
   1.764 -  unfolding dependent_alt by auto
   1.765 -
   1.766 -lemma independentD_alt:
   1.767 -  "independent B \<Longrightarrow> finite {x. X x \<noteq> 0} \<Longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<Longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x) = 0 \<Longrightarrow> X x = 0"
   1.768 -  unfolding independent_alt by blast
   1.769 -
   1.770 -lemma independentD_unique:
   1.771 -  assumes B: "independent B"
   1.772 -    and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B"
   1.773 -    and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B"
   1.774 -    and "(\<Sum>x | X x \<noteq> 0. X x *\<^sub>R x) = (\<Sum>x| Y x \<noteq> 0. Y x *\<^sub>R x)"
   1.775 -  shows "X = Y"
   1.776 -proof -
   1.777 -  have "X x - Y x = 0" for x
   1.778 -    using B
   1.779 -  proof (rule independentD_alt)
   1.780 -    have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}"
   1.781 -      by auto
   1.782 -    then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
   1.783 -      using X Y by (auto dest: finite_subset)
   1.784 -    then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *\<^sub>R v)"
   1.785 -      using X Y by (intro sum.mono_neutral_cong_left) auto
   1.786 -    also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
   1.787 -      by (simp add: scaleR_diff_left sum_subtractf assms)
   1.788 -    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *\<^sub>R v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *\<^sub>R v)"
   1.789 -      using X Y by (intro sum.mono_neutral_cong_right) auto
   1.790 -    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *\<^sub>R v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *\<^sub>R v)"
   1.791 -      using X Y by (intro sum.mono_neutral_cong_right) auto
   1.792 -    finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *\<^sub>R x) = 0"
   1.793 -      using assms by simp
   1.794 -  qed
   1.795 -  then show ?thesis
   1.796 -    by auto
   1.797 -qed
   1.798 -
   1.799 -text \<open>This is useful for building a basis step-by-step.\<close>
   1.800 -
   1.801 -lemma independent_insert:
   1.802 -  "independent (insert a S) \<longleftrightarrow>
   1.803 -    (if a \<in> S then independent S else independent S \<and> a \<notin> span S)"
   1.804 -  (is "?lhs \<longleftrightarrow> ?rhs")
   1.805 -proof (cases "a \<in> S")
   1.806 -  case True
   1.807 -  then show ?thesis
   1.808 -    using insert_absorb[OF True] by simp
   1.809 -next
   1.810 -  case False
   1.811 -  show ?thesis
   1.812 -  proof
   1.813 -    assume i: ?lhs
   1.814 -    then show ?rhs
   1.815 -      using False
   1.816 -      apply simp
   1.817 -      apply (rule conjI)
   1.818 -      apply (rule independent_mono)
   1.819 -      apply assumption
   1.820 -      apply blast
   1.821 -      apply (simp add: dependent_def)
   1.822 -      done
   1.823 -  next
   1.824 -    assume i: ?rhs
   1.825 -    show ?lhs
   1.826 -      using i False
   1.827 -      apply (auto simp add: dependent_def)
   1.828 -      by (metis in_span_insert insert_Diff_if insert_Diff_single insert_absorb)
   1.829 -  qed
   1.830 -qed
   1.831 -
   1.832 -lemma independent_Union_directed:
   1.833 -  assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
   1.834 -  assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c"
   1.835 -  shows "independent (\<Union>C)"
   1.836 -proof
   1.837 -  assume "dependent (\<Union>C)"
   1.838 -  then obtain u v S where S: "finite S" "S \<subseteq> \<Union>C" "v \<in> S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
   1.839 -    by (auto simp: dependent_explicit)
   1.840 -
   1.841 -  have "S \<noteq> {}"
   1.842 -    using \<open>v \<in> S\<close> by auto
   1.843 -  have "\<exists>c\<in>C. S \<subseteq> c"
   1.844 -    using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close>
   1.845 -  proof (induction rule: finite_ne_induct)
   1.846 -    case (insert i I)
   1.847 -    then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d"
   1.848 -      by blast
   1.849 -    from directed[OF cd] cd have "c \<union> d \<in> C"
   1.850 -      by (auto simp: sup.absorb1 sup.absorb2)
   1.851 -    with iI show ?case
   1.852 -      by (intro bexI[of _ "c \<union> d"]) auto
   1.853 -  qed auto
   1.854 -  then obtain c where "c \<in> C" "S \<subseteq> c"
   1.855 -    by auto
   1.856 -  have "dependent c"
   1.857 -    unfolding dependent_explicit
   1.858 -    by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+
   1.859 -  with indep[OF \<open>c \<in> C\<close>] show False
   1.860 -    by auto
   1.861 -qed
   1.862 -
   1.863 -text \<open>Hence we can create a maximal independent subset.\<close>
   1.864 -
   1.865 -lemma maximal_independent_subset_extend:
   1.866 -  assumes "S \<subseteq> V" "independent S"
   1.867 -  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   1.868 -proof -
   1.869 -  let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
   1.870 -  have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
   1.871 -  proof (rule subset_Zorn)
   1.872 -    fix C :: "'a set set" assume "subset.chain ?C C"
   1.873 -    then have C: "\<And>c. c \<in> C \<Longrightarrow> c \<subseteq> V" "\<And>c. c \<in> C \<Longrightarrow> S \<subseteq> c" "\<And>c. c \<in> C \<Longrightarrow> independent c"
   1.874 -      "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
   1.875 -      unfolding subset.chain_def by blast+
   1.876 -
   1.877 -    show "\<exists>U\<in>?C. \<forall>X\<in>C. X \<subseteq> U"
   1.878 -    proof cases
   1.879 -      assume "C = {}" with assms show ?thesis
   1.880 -        by (auto intro!: exI[of _ S])
   1.881 -    next
   1.882 -      assume "C \<noteq> {}"
   1.883 -      with C(2) have "S \<subseteq> \<Union>C"
   1.884 -        by auto
   1.885 -      moreover have "independent (\<Union>C)"
   1.886 -        by (intro independent_Union_directed C)
   1.887 -      moreover have "\<Union>C \<subseteq> V"
   1.888 -        using C by auto
   1.889 -      ultimately show ?thesis
   1.890 -        by auto
   1.891 -    qed
   1.892 -  qed
   1.893 -  then obtain B where B: "independent B" "B \<subseteq> V" "S \<subseteq> B"
   1.894 -    and max: "\<And>S. independent S \<Longrightarrow> S \<subseteq> V \<Longrightarrow> B \<subseteq> S \<Longrightarrow> S = B"
   1.895 -    by auto
   1.896 -  moreover
   1.897 -  { assume "\<not> V \<subseteq> span B"
   1.898 -    then obtain v where "v \<in> V" "v \<notin> span B"
   1.899 -      by auto
   1.900 -    with B have "independent (insert v B)"
   1.901 -      unfolding independent_insert by auto
   1.902 -    from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close>
   1.903 -    have "v \<in> B"
   1.904 -      by auto
   1.905 -    with \<open>v \<notin> span B\<close> have False
   1.906 -      by (auto intro: span_superset) }
   1.907 -  ultimately show ?thesis
   1.908 -    by (auto intro!: exI[of _ B])
   1.909 -qed
   1.910 -
   1.911 -
   1.912 -lemma maximal_independent_subset:
   1.913 -  "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   1.914 -  by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
   1.915 -
   1.916 -lemma span_finite:
   1.917 -  assumes fS: "finite S"
   1.918 -  shows "span S = {y. \<exists>u. sum (\<lambda>v. u v *\<^sub>R v) S = y}"
   1.919 -  (is "_ = ?rhs")
   1.920 -proof -
   1.921 -  {
   1.922 -    fix y
   1.923 -    assume y: "y \<in> span S"
   1.924 -    from y obtain S' u where fS': "finite S'"
   1.925 -      and SS': "S' \<subseteq> S"
   1.926 -      and u: "sum (\<lambda>v. u v *\<^sub>R v) S' = y"
   1.927 -      unfolding span_explicit by blast
   1.928 -    let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
   1.929 -    have "sum (\<lambda>v. ?u v *\<^sub>R v) S = sum (\<lambda>v. u v *\<^sub>R v) S'"
   1.930 -      using SS' fS by (auto intro!: sum.mono_neutral_cong_right)
   1.931 -    then have "sum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u)
   1.932 -    then have "y \<in> ?rhs" by auto
   1.933 -  }
   1.934 -  moreover
   1.935 -  {
   1.936 -    fix y u
   1.937 -    assume u: "sum (\<lambda>v. u v *\<^sub>R v) S = y"
   1.938 -    then have "y \<in> span S" using fS unfolding span_explicit by auto
   1.939 -  }
   1.940 -  ultimately show ?thesis by blast
   1.941 -qed
   1.942 -
   1.943 -lemma linear_independent_extend_subspace:
   1.944 -  assumes "independent B"
   1.945 -  shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = span (f`B)"
   1.946 -proof -
   1.947 -  from maximal_independent_subset_extend[OF _ \<open>independent B\<close>, of UNIV]
   1.948 -  obtain B' where "B \<subseteq> B'" "independent B'" "span B' = UNIV"
   1.949 -    by (auto simp: top_unique)
   1.950 -  have "\<forall>y. \<exists>X. {x. X x \<noteq> 0} \<subseteq> B' \<and> finite {x. X x \<noteq> 0} \<and> y = (\<Sum>x|X x \<noteq> 0. X x *\<^sub>R x)"
   1.951 -    using \<open>span B' = UNIV\<close> unfolding span_alt by auto
   1.952 -  then obtain X where X: "\<And>y. {x. X y x \<noteq> 0} \<subseteq> B'" "\<And>y. finite {x. X y x \<noteq> 0}"
   1.953 -    "\<And>y. y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R x)"
   1.954 -    unfolding choice_iff by auto
   1.955 -
   1.956 -  have X_add: "X (x + y) = (\<lambda>z. X x z + X y z)" for x y
   1.957 -    using \<open>independent B'\<close>
   1.958 -  proof (rule independentD_unique)
   1.959 -    have "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)
   1.960 -      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R z)"
   1.961 -      by (intro sum.mono_neutral_cong_left) (auto intro: X)
   1.962 -    also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
   1.963 -      by (auto simp add: scaleR_add_left sum.distrib
   1.964 -               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
   1.965 -    also have "\<dots> = x + y"
   1.966 -      by (simp add: X(3)[symmetric])
   1.967 -    also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
   1.968 -      by (rule X(3))
   1.969 -    finally show "(\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z) = (\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R z)"
   1.970 -      ..
   1.971 -    have "{z. X x z + X y z \<noteq> 0} \<subseteq> {z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}"
   1.972 -      by auto
   1.973 -    then show "finite {z. X x z + X y z \<noteq> 0}" "{xa. X x xa + X y xa \<noteq> 0} \<subseteq> B'"
   1.974 -        "finite {xa. X (x + y) xa \<noteq> 0}" "{xa. X (x + y) xa \<noteq> 0} \<subseteq> B'"
   1.975 -      using X(1) by (auto dest: finite_subset intro: X)
   1.976 -  qed
   1.977 -
   1.978 -  have X_cmult: "X (c *\<^sub>R x) = (\<lambda>z. c * X x z)" for x c
   1.979 -    using \<open>independent B'\<close>
   1.980 -  proof (rule independentD_unique)
   1.981 -    show "finite {z. X (c *\<^sub>R x) z \<noteq> 0}" "{z. X (c *\<^sub>R x) z \<noteq> 0} \<subseteq> B'"
   1.982 -      "finite {z. c * X x z \<noteq> 0}" "{z. c * X x z \<noteq> 0} \<subseteq> B' "
   1.983 -      using X(1,2) by auto
   1.984 -    show "(\<Sum>z | X (c *\<^sub>R x) z \<noteq> 0. X (c *\<^sub>R x) z *\<^sub>R z) = (\<Sum>z | c * X x z \<noteq> 0. (c * X x z) *\<^sub>R z)"
   1.985 -      unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric]
   1.986 -      by (cases "c = 0") (auto simp: X(3)[symmetric])
   1.987 -  qed
   1.988 -
   1.989 -  have X_B': "x \<in> B' \<Longrightarrow> X x = (\<lambda>z. if z = x then 1 else 0)" for x
   1.990 -    using \<open>independent B'\<close>
   1.991 -    by (rule independentD_unique[OF _ X(2) X(1)]) (auto intro: X simp: X(3)[symmetric])
   1.992 -
   1.993 -  define f' where "f' y = (if y \<in> B then f y else 0)" for y
   1.994 -  define g where "g y = (\<Sum>x|X y x \<noteq> 0. X y x *\<^sub>R f' x)" for y
   1.995 -
   1.996 -  have g_f': "x \<in> B' \<Longrightarrow> g x = f' x" for x
   1.997 -    by (auto simp: g_def X_B')
   1.998 -
   1.999 -  have "linear g"
  1.1000 -  proof
  1.1001 -    fix x y
  1.1002 -    have *: "(\<Sum>z | X x z + X y z \<noteq> 0. (X x z + X y z) *\<^sub>R f' z)
  1.1003 -      = (\<Sum>z\<in>{z. X x z \<noteq> 0} \<union> {z. X y z \<noteq> 0}. (X x z + X y z) *\<^sub>R f' z)"
  1.1004 -      by (intro sum.mono_neutral_cong_left) (auto intro: X)
  1.1005 -    show "g (x + y) = g x + g y"
  1.1006 -      unfolding g_def X_add *
  1.1007 -      by (auto simp add: scaleR_add_left sum.distrib
  1.1008 -               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
  1.1009 -  next
  1.1010 -    show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
  1.1011 -      by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
  1.1012 -  qed
  1.1013 -  moreover have "\<forall>x\<in>B. g x = f x"
  1.1014 -    using \<open>B \<subseteq> B'\<close> by (auto simp: g_f' f'_def)
  1.1015 -  moreover have "range g = span (f`B)"
  1.1016 -    unfolding \<open>span B' = UNIV\<close>[symmetric] span_linear_image[OF \<open>linear g\<close>, symmetric]
  1.1017 -  proof (rule span_subspace)
  1.1018 -    have "g ` B' \<subseteq> f`B \<union> {0}"
  1.1019 -      by (auto simp: g_f' f'_def)
  1.1020 -    also have "\<dots> \<subseteq> span (f`B)"
  1.1021 -      by (auto intro: span_superset span_0)
  1.1022 -    finally show "g ` B' \<subseteq> span (f`B)"
  1.1023 -      by auto
  1.1024 -    have "x \<in> B \<Longrightarrow> f x = g x" for x
  1.1025 -      using \<open>B \<subseteq> B'\<close> by (auto simp add: g_f' f'_def)
  1.1026 -    then show "span (f ` B) \<subseteq> span (g ` B')"
  1.1027 -      using \<open>B \<subseteq> B'\<close> by (intro span_mono) auto
  1.1028 -  qed (rule subspace_span)
  1.1029 -  ultimately show ?thesis
  1.1030 -    by auto
  1.1031 -qed
  1.1032 -
  1.1033 -lemma linear_independent_extend:
  1.1034 -  "independent B \<Longrightarrow> \<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
  1.1035 -  using linear_independent_extend_subspace[of B f] by auto
  1.1036 -
  1.1037 -text \<open>Linear functions are equal on a subspace if they are on a spanning set.\<close>
  1.1038 -
  1.1039 -lemma subspace_kernel:
  1.1040 -  assumes lf: "linear f"
  1.1041 -  shows "subspace {x. f x = 0}"
  1.1042 -  apply (simp add: subspace_def)
  1.1043 -  apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
  1.1044 -  done
  1.1045 -
  1.1046 -lemma linear_eq_0_span:
  1.1047 -  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
  1.1048 -  shows "\<forall>x \<in> span B. f x = 0"
  1.1049 -  using f0 subspace_kernel[OF lf]
  1.1050 -  by (rule span_induct')
  1.1051 -
  1.1052 -lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
  1.1053 -  using linear_eq_0_span[of f B] by auto
  1.1054 -
  1.1055 -lemma linear_eq_span:  "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
  1.1056 -  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
  1.1057 -
  1.1058 -lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
  1.1059 -  using linear_eq_span[of f g B] by auto
  1.1060 -
  1.1061 -text \<open>The degenerate case of the Exchange Lemma.\<close>
  1.1062 -
  1.1063 -lemma spanning_subset_independent:
  1.1064 -  assumes BA: "B \<subseteq> A"
  1.1065 -    and iA: "independent A"
  1.1066 -    and AsB: "A \<subseteq> span B"
  1.1067 -  shows "A = B"
  1.1068 -proof
  1.1069 -  show "B \<subseteq> A" by (rule BA)
  1.1070 -
  1.1071 -  from span_mono[OF BA] span_mono[OF AsB]
  1.1072 -  have sAB: "span A = span B" unfolding span_span by blast
  1.1073 -
  1.1074 -  {
  1.1075 -    fix x
  1.1076 -    assume x: "x \<in> A"
  1.1077 -    from iA have th0: "x \<notin> span (A - {x})"
  1.1078 -      unfolding dependent_def using x by blast
  1.1079 -    from x have xsA: "x \<in> span A"
  1.1080 -      by (blast intro: span_superset)
  1.1081 -    have "A - {x} \<subseteq> A" by blast
  1.1082 -    then have th1: "span (A - {x}) \<subseteq> span A"
  1.1083 -      by (metis span_mono)
  1.1084 -    {
  1.1085 -      assume xB: "x \<notin> B"
  1.1086 -      from xB BA have "B \<subseteq> A - {x}"
  1.1087 -        by blast
  1.1088 -      then have "span B \<subseteq> span (A - {x})"
  1.1089 -        by (metis span_mono)
  1.1090 -      with th1 th0 sAB have "x \<notin> span A"
  1.1091 -        by blast
  1.1092 -      with x have False
  1.1093 -        by (metis span_superset)
  1.1094 -    }
  1.1095 -    then have "x \<in> B" by blast
  1.1096 -  }
  1.1097 -  then show "A \<subseteq> B" by blast
  1.1098 -qed
  1.1099 -
  1.1100 -text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
  1.1101 -
  1.1102 -lemma spanning_surjective_image:
  1.1103 -  assumes us: "UNIV \<subseteq> span S"
  1.1104 -    and lf: "linear f"
  1.1105 -    and sf: "surj f"
  1.1106 -  shows "UNIV \<subseteq> span (f ` S)"
  1.1107 -proof -
  1.1108 -  have "UNIV \<subseteq> f ` UNIV"
  1.1109 -    using sf by (auto simp add: surj_def)
  1.1110 -  also have " \<dots> \<subseteq> span (f ` S)"
  1.1111 -    using spans_image[OF lf us] .
  1.1112 -  finally show ?thesis .
  1.1113 -qed
  1.1114 -
  1.1115 -lemma independent_inj_on_image:
  1.1116 -  assumes iS: "independent S"
  1.1117 -    and lf: "linear f"
  1.1118 -    and fi: "inj_on f (span S)"
  1.1119 -  shows "independent (f ` S)"
  1.1120 -proof -
  1.1121 -  {
  1.1122 -    fix a
  1.1123 -    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
  1.1124 -    have eq: "f ` S - {f a} = f ` (S - {a})"
  1.1125 -      using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
  1.1126 -    from a have "f a \<in> f ` span (S - {a})"
  1.1127 -      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
  1.1128 -    then have "a \<in> span (S - {a})"
  1.1129 -      by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
  1.1130 -         (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
  1.1131 -    with a(1) iS have False
  1.1132 -      by (simp add: dependent_def)
  1.1133 -  }
  1.1134 -  then show ?thesis
  1.1135 -    unfolding dependent_def by blast
  1.1136 -qed
  1.1137 -
  1.1138 -lemma independent_injective_image:
  1.1139 -  "independent S \<Longrightarrow> linear f \<Longrightarrow> inj f \<Longrightarrow> independent (f ` S)"
  1.1140 -  using independent_inj_on_image[of S f] by (auto simp: subset_inj_on)
  1.1141 -
  1.1142 -text \<open>Detailed theorems about left and right invertibility in general case.\<close>
  1.1143 -
  1.1144 -lemma linear_inj_on_left_inverse:
  1.1145 -  assumes lf: "linear f" and fi: "inj_on f (span S)"
  1.1146 -  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
  1.1147 -proof -
  1.1148 -  obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
  1.1149 -    using maximal_independent_subset[of S] by auto
  1.1150 -  then have "span S = span B"
  1.1151 -    unfolding span_eq by (auto simp: span_superset)
  1.1152 -  with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
  1.1153 -  obtain g where g: "linear g" "\<forall>x\<in>f ` B. g x = inv_into B f x" "range g = span (inv_into B f ` f ` B)"
  1.1154 -    by fastforce
  1.1155 -  have fB: "inj_on f B"
  1.1156 -    using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
  1.1157 -
  1.1158 -  have "\<forall>x\<in>span B. g (f x) = x"
  1.1159 -  proof (intro linear_eq_span)
  1.1160 -    show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
  1.1161 -      using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
  1.1162 -    show "\<forall>x \<in> B. g (f x) = x"
  1.1163 -      using g fi \<open>span S = span B\<close> by (auto simp: fB)
  1.1164 -  qed
  1.1165 -  moreover
  1.1166 -  have "inv_into B f ` f ` B \<subseteq> B"
  1.1167 -    by (auto simp: fB)
  1.1168 -  then have "range g \<subseteq> span S"
  1.1169 -    unfolding g \<open>span S = span B\<close> by (intro span_mono)
  1.1170 -  ultimately show ?thesis
  1.1171 -    using \<open>span S = span B\<close> \<open>linear g\<close> by auto
  1.1172 -qed
  1.1173 -
  1.1174 -lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
  1.1175 -  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
  1.1176 -
  1.1177 -lemma linear_surj_right_inverse:
  1.1178 -  assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
  1.1179 -  shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
  1.1180 -proof -
  1.1181 -  obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
  1.1182 -    using maximal_independent_subset[of T] by auto
  1.1183 -  then have "span T = span B"
  1.1184 -    unfolding span_eq by (auto simp: span_superset)
  1.1185 -
  1.1186 -  from linear_independent_extend_subspace[OF \<open>independent B\<close>, of "inv_into (span S) f"]
  1.1187 -  obtain g where g: "linear g" "\<forall>x\<in>B. g x = inv_into (span S) f x" "range g = span (inv_into (span S) f`B)"
  1.1188 -    by auto
  1.1189 -  moreover have "x \<in> B \<Longrightarrow> f (inv_into (span S) f x) = x" for x
  1.1190 -    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (intro f_inv_into_f) (auto intro: span_superset)
  1.1191 -  ultimately have "\<forall>x\<in>B. f (g x) = x"
  1.1192 -    by auto
  1.1193 -  then have "\<forall>x\<in>span B. f (g x) = x"
  1.1194 -    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
  1.1195 -    by (intro linear_eq_span) (auto simp: id_def comp_def)
  1.1196 -  moreover have "inv_into (span S) f ` B \<subseteq> span S"
  1.1197 -    using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
  1.1198 -  then have "range g \<subseteq> span S"
  1.1199 -    unfolding g by (intro span_minimal subspace_span) auto
  1.1200 -  ultimately show ?thesis
  1.1201 -    using \<open>linear g\<close> \<open>span T = span B\<close> by auto
  1.1202 -qed
  1.1203 -
  1.1204 -lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
  1.1205 -  using linear_surj_right_inverse[of f UNIV UNIV]
  1.1206 -  by (auto simp: span_UNIV fun_eq_iff)
  1.1207 -
  1.1208 -text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
  1.1209 -
  1.1210 -lemma exchange_lemma:
  1.1211 -  assumes f:"finite t"
  1.1212 -    and i: "independent s"
  1.1213 -    and sp: "s \<subseteq> span t"
  1.1214 -  shows "\<exists>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
  1.1215 -  using f i sp
  1.1216 -proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
  1.1217 -  case less
  1.1218 -  note ft = \<open>finite t\<close> and s = \<open>independent s\<close> and sp = \<open>s \<subseteq> span t\<close>
  1.1219 -  let ?P = "\<lambda>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
  1.1220 -  let ?ths = "\<exists>t'. ?P t'"
  1.1221 -  {
  1.1222 -    assume "s \<subseteq> t"
  1.1223 -    then have ?ths
  1.1224 -      by (metis ft Un_commute sp sup_ge1)
  1.1225 -  }
  1.1226 -  moreover
  1.1227 -  {
  1.1228 -    assume st: "t \<subseteq> s"
  1.1229 -    from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
  1.1230 -    have ?ths
  1.1231 -      by (metis Un_absorb sp)
  1.1232 -  }
  1.1233 -  moreover
  1.1234 -  {
  1.1235 -    assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
  1.1236 -    from st(2) obtain b where b: "b \<in> t" "b \<notin> s"
  1.1237 -      by blast
  1.1238 -    from b have "t - {b} - s \<subset> t - s"
  1.1239 -      by blast
  1.1240 -    then have cardlt: "card (t - {b} - s) < card (t - s)"
  1.1241 -      using ft by (auto intro: psubset_card_mono)
  1.1242 -    from b ft have ct0: "card t \<noteq> 0"
  1.1243 -      by auto
  1.1244 -    have ?ths
  1.1245 -    proof cases
  1.1246 -      assume stb: "s \<subseteq> span (t - {b})"
  1.1247 -      from ft have ftb: "finite (t - {b})"
  1.1248 -        by auto
  1.1249 -      from less(1)[OF cardlt ftb s stb]
  1.1250 -      obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
  1.1251 -        and fu: "finite u" by blast
  1.1252 -      let ?w = "insert b u"
  1.1253 -      have th0: "s \<subseteq> insert b u"
  1.1254 -        using u by blast
  1.1255 -      from u(3) b have "u \<subseteq> s \<union> t"
  1.1256 -        by blast
  1.1257 -      then have th1: "insert b u \<subseteq> s \<union> t"
  1.1258 -        using u b by blast
  1.1259 -      have bu: "b \<notin> u"
  1.1260 -        using b u by blast
  1.1261 -      from u(1) ft b have "card u = (card t - 1)"
  1.1262 -        by auto
  1.1263 -      then have th2: "card (insert b u) = card t"
  1.1264 -        using card_insert_disjoint[OF fu bu] ct0 by auto
  1.1265 -      from u(4) have "s \<subseteq> span u" .
  1.1266 -      also have "\<dots> \<subseteq> span (insert b u)"
  1.1267 -        by (rule span_mono) blast
  1.1268 -      finally have th3: "s \<subseteq> span (insert b u)" .
  1.1269 -      from th0 th1 th2 th3 fu have th: "?P ?w"
  1.1270 -        by blast
  1.1271 -      from th show ?thesis by blast
  1.1272 -    next
  1.1273 -      assume stb: "\<not> s \<subseteq> span (t - {b})"
  1.1274 -      from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
  1.1275 -        by blast
  1.1276 -      have ab: "a \<noteq> b"
  1.1277 -        using a b by blast
  1.1278 -      have at: "a \<notin> t"
  1.1279 -        using a ab span_superset[of a "t- {b}"] by auto
  1.1280 -      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
  1.1281 -        using cardlt ft a b by auto
  1.1282 -      have ft': "finite (insert a (t - {b}))"
  1.1283 -        using ft by auto
  1.1284 -      {
  1.1285 -        fix x
  1.1286 -        assume xs: "x \<in> s"
  1.1287 -        have t: "t \<subseteq> insert b (insert a (t - {b}))"
  1.1288 -          using b by auto
  1.1289 -        from b(1) have "b \<in> span t"
  1.1290 -          by (simp add: span_superset)
  1.1291 -        have bs: "b \<in> span (insert a (t - {b}))"
  1.1292 -          apply (rule in_span_delete)
  1.1293 -          using a sp unfolding subset_eq
  1.1294 -          apply auto
  1.1295 -          done
  1.1296 -        from xs sp have "x \<in> span t"
  1.1297 -          by blast
  1.1298 -        with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" ..
  1.1299 -        from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .
  1.1300 -      }
  1.1301 -      then have sp': "s \<subseteq> span (insert a (t - {b}))"
  1.1302 -        by blast
  1.1303 -      from less(1)[OF mlt ft' s sp'] obtain u where u:
  1.1304 -        "card u = card (insert a (t - {b}))"
  1.1305 -        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
  1.1306 -        "s \<subseteq> span u" by blast
  1.1307 -      from u a b ft at ct0 have "?P u"
  1.1308 -        by auto
  1.1309 -      then show ?thesis by blast
  1.1310 -    qed
  1.1311 -  }
  1.1312 -  ultimately show ?ths by blast
  1.1313 -qed
  1.1314 -
  1.1315 -text \<open>This implies corresponding size bounds.\<close>
  1.1316 -
  1.1317 -lemma independent_span_bound:
  1.1318 -  assumes f: "finite t"
  1.1319 -    and i: "independent s"
  1.1320 -    and sp: "s \<subseteq> span t"
  1.1321 -  shows "finite s \<and> card s \<le> card t"
  1.1322 -  by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
  1.1323 -
  1.1324  lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
  1.1325  proof -
  1.1326    have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
  1.1327 @@ -1353,51 +47,8 @@
  1.1328  
  1.1329  subsection%unimportant \<open>More interesting properties of the norm.\<close>
  1.1330  
  1.1331 -lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
  1.1332 -  by auto
  1.1333 -
  1.1334  notation inner (infix "\<bullet>" 70)
  1.1335  
  1.1336 -lemma square_bound_lemma:
  1.1337 -  fixes x :: real
  1.1338 -  shows "x < (1 + x) * (1 + x)"
  1.1339 -proof -
  1.1340 -  have "(x + 1/2)\<^sup>2 + 3/4 > 0"
  1.1341 -    using zero_le_power2[of "x+1/2"] by arith
  1.1342 -  then show ?thesis
  1.1343 -    by (simp add: field_simps power2_eq_square)
  1.1344 -qed
  1.1345 -
  1.1346 -lemma square_continuous:
  1.1347 -  fixes e :: real
  1.1348 -  shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
  1.1349 -  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
  1.1350 -  by (force simp add: power2_eq_square)
  1.1351 -
  1.1352 -
  1.1353 -lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
  1.1354 -  by simp (* TODO: delete *)
  1.1355 -
  1.1356 -lemma norm_triangle_sub:
  1.1357 -  fixes x y :: "'a::real_normed_vector"
  1.1358 -  shows "norm x \<le> norm y + norm (x - y)"
  1.1359 -  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
  1.1360 -
  1.1361 -lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> x \<bullet> x \<le> y \<bullet> y"
  1.1362 -  by (simp add: norm_eq_sqrt_inner)
  1.1363 -
  1.1364 -lemma norm_lt: "norm x < norm y \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
  1.1365 -  by (simp add: norm_eq_sqrt_inner)
  1.1366 -
  1.1367 -lemma norm_eq: "norm x = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
  1.1368 -  apply (subst order_eq_iff)
  1.1369 -  apply (auto simp: norm_le)
  1.1370 -  done
  1.1371 -
  1.1372 -lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
  1.1373 -  by (simp add: norm_eq_sqrt_inner)
  1.1374 -
  1.1375 -
  1.1376  text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
  1.1377  
  1.1378  lemma linear_componentwise:
  1.1379 @@ -1405,11 +56,11 @@
  1.1380    assumes lf: "linear f"
  1.1381    shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
  1.1382  proof -
  1.1383 +  interpret linear f by fact
  1.1384    have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
  1.1385      by (simp add: inner_sum_left)
  1.1386    then show ?thesis
  1.1387 -    unfolding linear_sum_mul[OF lf, symmetric]
  1.1388 -    unfolding euclidean_representation ..
  1.1389 +    by (simp add: euclidean_representation sum[symmetric] scale[symmetric])
  1.1390  qed
  1.1391  
  1.1392  lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
  1.1393 @@ -1607,22 +258,15 @@
  1.1394    using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
  1.1395  
  1.1396  lemma bilinear_sum:
  1.1397 -  assumes bh: "bilinear h"
  1.1398 -    and fS: "finite S"
  1.1399 -    and fT: "finite T"
  1.1400 +  assumes "bilinear h"
  1.1401    shows "h (sum f S) (sum g T) = sum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
  1.1402  proof -
  1.1403 +  interpret l: linear "\<lambda>x. h x y" for y using assms by (simp add: bilinear_def)
  1.1404 +  interpret r: linear "\<lambda>y. h x y" for x using assms by (simp add: bilinear_def)
  1.1405    have "h (sum f S) (sum g T) = sum (\<lambda>x. h (f x) (sum g T)) S"
  1.1406 -    apply (rule linear_sum[unfolded o_def])
  1.1407 -    using bh fS
  1.1408 -    apply (auto simp add: bilinear_def)
  1.1409 -    done
  1.1410 +    by (simp add: l.sum)
  1.1411    also have "\<dots> = sum (\<lambda>x. sum (\<lambda>y. h (f x) (g y)) T) S"
  1.1412 -    apply (rule sum.cong, simp)
  1.1413 -    apply (rule linear_sum[unfolded o_def])
  1.1414 -    using bh fT
  1.1415 -    apply (auto simp add: bilinear_def)
  1.1416 -    done
  1.1417 +    by (rule sum.cong) (simp_all add: r.sum)
  1.1418    finally show ?thesis
  1.1419      unfolding sum.cartesian_product .
  1.1420  qed
  1.1421 @@ -1663,6 +307,7 @@
  1.1422    assumes lf: "linear f"
  1.1423    shows "x \<bullet> adjoint f y = f x \<bullet> y"
  1.1424  proof -
  1.1425 +  interpret linear f by fact
  1.1426    have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
  1.1427    proof (intro allI exI)
  1.1428      fix y :: "'m" and x
  1.1429 @@ -1670,8 +315,7 @@
  1.1430      have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
  1.1431        by (simp add: euclidean_representation)
  1.1432      also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
  1.1433 -      unfolding linear_sum[OF lf]
  1.1434 -      by (simp add: linear_cmul[OF lf])
  1.1435 +      by (simp add: sum scale)
  1.1436      finally show "f x \<bullet> y = x \<bullet> ?w"
  1.1437        by (simp add: inner_sum_left inner_sum_right mult.commute)
  1.1438    qed
  1.1439 @@ -1847,63 +491,14 @@
  1.1440  subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
  1.1441  
  1.1442  lemma independent_Basis: "independent Basis"
  1.1443 -  unfolding dependent_def
  1.1444 -  apply (subst span_finite)
  1.1445 -  apply simp
  1.1446 -  apply clarify
  1.1447 -  apply (drule_tac f="inner a" in arg_cong)
  1.1448 -  apply (simp add: inner_Basis inner_sum_right eq_commute)
  1.1449 -  done
  1.1450 +  by (rule independent_Basis)
  1.1451  
  1.1452  lemma span_Basis [simp]: "span Basis = UNIV"
  1.1453 -  unfolding span_finite [OF finite_Basis]
  1.1454 -  by (fast intro: euclidean_representation)
  1.1455 +  by (rule span_Basis)
  1.1456  
  1.1457  lemma in_span_Basis: "x \<in> span Basis"
  1.1458    unfolding span_Basis ..
  1.1459  
  1.1460 -lemma Basis_le_norm: "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> norm x"
  1.1461 -  by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
  1.1462 -
  1.1463 -lemma norm_bound_Basis_le: "b \<in> Basis \<Longrightarrow> norm x \<le> e \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> e"
  1.1464 -  by (metis Basis_le_norm order_trans)
  1.1465 -
  1.1466 -lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>x \<bullet> b\<bar> < e"
  1.1467 -  by (metis Basis_le_norm le_less_trans)
  1.1468 -
  1.1469 -lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
  1.1470 -  apply (subst euclidean_representation[of x, symmetric])
  1.1471 -  apply (rule order_trans[OF norm_sum])
  1.1472 -  apply (auto intro!: sum_mono)
  1.1473 -  done
  1.1474 -
  1.1475 -lemma sum_norm_allsubsets_bound:
  1.1476 -  fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
  1.1477 -  assumes fP: "finite P"
  1.1478 -    and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
  1.1479 -  shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
  1.1480 -proof -
  1.1481 -  have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
  1.1482 -    by (rule sum_mono) (rule norm_le_l1)
  1.1483 -  also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
  1.1484 -    by (rule sum.swap)
  1.1485 -  also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
  1.1486 -  proof (rule sum_bounded_above)
  1.1487 -    fix i :: 'n
  1.1488 -    assume i: "i \<in> Basis"
  1.1489 -    have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
  1.1490 -      norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
  1.1491 -      by (simp add: abs_real_def sum.If_cases[OF fP] sum_negf norm_triangle_ineq4 inner_sum_left
  1.1492 -        del: real_norm_def)
  1.1493 -    also have "\<dots> \<le> e + e"
  1.1494 -      unfolding real_norm_def
  1.1495 -      by (intro add_mono norm_bound_Basis_le i fPs) auto
  1.1496 -    finally show "(\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le> 2*e" by simp
  1.1497 -  qed
  1.1498 -  also have "\<dots> = 2 * real DIM('n) * e" by simp
  1.1499 -  finally show ?thesis .
  1.1500 -qed
  1.1501 -
  1.1502  
  1.1503  subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
  1.1504  
  1.1505 @@ -1912,6 +507,7 @@
  1.1506    assumes lf: "linear f"
  1.1507    shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
  1.1508  proof
  1.1509 +  interpret linear f by fact
  1.1510    let ?B = "\<Sum>b\<in>Basis. norm (f b)"
  1.1511    show "\<forall>x. norm (f x) \<le> ?B * norm x"
  1.1512    proof
  1.1513 @@ -1920,7 +516,7 @@
  1.1514      have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
  1.1515        unfolding euclidean_representation ..
  1.1516      also have "\<dots> = norm (sum ?g Basis)"
  1.1517 -      by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
  1.1518 +      by (simp add: sum scale)
  1.1519      finally have th0: "norm (f x) = norm (sum ?g Basis)" .
  1.1520      have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
  1.1521      proof -
  1.1522 @@ -1997,15 +593,15 @@
  1.1523    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
  1.1524    assumes "linear f" "inj f"
  1.1525    obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
  1.1526 -  using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
  1.1527 +  using linear_injective_left_inverse [OF assms]
  1.1528 +    linear_invertible_bounded_below_pos assms by blast
  1.1529  
  1.1530  lemma bounded_linearI':
  1.1531    fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  1.1532    assumes "\<And>x y. f (x + y) = f x + f y"
  1.1533      and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
  1.1534    shows "bounded_linear f"
  1.1535 -  unfolding linear_conv_bounded_linear[symmetric]
  1.1536 -  by (rule linearI[OF assms])
  1.1537 +  using assms linearI linear_conv_bounded_linear by blast
  1.1538  
  1.1539  lemma bilinear_bounded:
  1.1540    fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
  1.1541 @@ -2020,7 +616,7 @@
  1.1542      apply rule
  1.1543      done
  1.1544    also have "\<dots> = norm (sum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
  1.1545 -    unfolding bilinear_sum[OF bh finite_Basis finite_Basis] ..
  1.1546 +    unfolding bilinear_sum[OF bh] ..
  1.1547    finally have th: "norm (h x y) = \<dots>" .
  1.1548    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
  1.1549      apply (auto simp add: sum_distrib_right th sum.cartesian_product)
  1.1550 @@ -2084,14 +680,14 @@
  1.1551      by (simp only: ac_simps)
  1.1552  qed
  1.1553  
  1.1554 -lemma bounded_linear_imp_has_derivative:
  1.1555 -     "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
  1.1556 -  by (simp add: has_derivative_def bounded_linear.linear linear_diff)
  1.1557 +lemma bounded_linear_imp_has_derivative: "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
  1.1558 +  by (auto simp add: has_derivative_def linear_diff linear_linear linear_def
  1.1559 +      dest: bounded_linear.linear)
  1.1560  
  1.1561  lemma linear_imp_has_derivative:
  1.1562    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  1.1563    shows "linear f \<Longrightarrow> (f has_derivative f) net"
  1.1564 -by (simp add: has_derivative_def linear_conv_bounded_linear linear_diff)
  1.1565 +  by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear)
  1.1566  
  1.1567  lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
  1.1568    using bounded_linear_imp_has_derivative differentiable_def by blast
  1.1569 @@ -2099,7 +695,7 @@
  1.1570  lemma linear_imp_differentiable:
  1.1571    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  1.1572    shows "linear f \<Longrightarrow> f differentiable net"
  1.1573 -by (metis linear_imp_has_derivative differentiable_def)
  1.1574 +  by (metis linear_imp_has_derivative differentiable_def)
  1.1575  
  1.1576  
  1.1577  subsection%unimportant \<open>We continue.\<close>
  1.1578 @@ -2107,221 +703,21 @@
  1.1579  lemma independent_bound:
  1.1580    fixes S :: "'a::euclidean_space set"
  1.1581    shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
  1.1582 -  using independent_span_bound[OF finite_Basis, of S] by auto
  1.1583 +  by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)
  1.1584 +
  1.1585 +lemmas independent_imp_finite = finiteI_independent
  1.1586  
  1.1587  corollary
  1.1588    fixes S :: "'a::euclidean_space set"
  1.1589    assumes "independent S"
  1.1590 -  shows independent_imp_finite: "finite S" and independent_card_le:"card S \<le> DIM('a)"
  1.1591 -using assms independent_bound by auto
  1.1592 -
  1.1593 -lemma independent_explicit:
  1.1594 -  fixes B :: "'a::euclidean_space set"
  1.1595 -  shows "independent B \<longleftrightarrow>
  1.1596 -         finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *\<^sub>R v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
  1.1597 -apply (cases "finite B")
  1.1598 - apply (force simp: dependent_finite)
  1.1599 -using independent_bound
  1.1600 -apply auto
  1.1601 -done
  1.1602 +  shows independent_card_le:"card S \<le> DIM('a)"
  1.1603 +  using assms independent_bound by auto
  1.1604  
  1.1605  lemma dependent_biggerset:
  1.1606    fixes S :: "'a::euclidean_space set"
  1.1607    shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
  1.1608    by (metis independent_bound not_less)
  1.1609  
  1.1610 -text \<open>Notion of dimension.\<close>
  1.1611 -
  1.1612 -definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
  1.1613 -
  1.1614 -lemma basis_exists:
  1.1615 -  "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
  1.1616 -  unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
  1.1617 -  using maximal_independent_subset[of V] independent_bound
  1.1618 -  by auto
  1.1619 -
  1.1620 -corollary dim_le_card:
  1.1621 -  fixes s :: "'a::euclidean_space set"
  1.1622 -  shows "finite s \<Longrightarrow> dim s \<le> card s"
  1.1623 -by (metis basis_exists card_mono)
  1.1624 -
  1.1625 -text \<open>Consequences of independence or spanning for cardinality.\<close>
  1.1626 -
  1.1627 -lemma independent_card_le_dim:
  1.1628 -  fixes B :: "'a::euclidean_space set"
  1.1629 -  assumes "B \<subseteq> V"
  1.1630 -    and "independent B"
  1.1631 -  shows "card B \<le> dim V"
  1.1632 -proof -
  1.1633 -  from basis_exists[of V] \<open>B \<subseteq> V\<close>
  1.1634 -  obtain B' where "independent B'"
  1.1635 -    and "B \<subseteq> span B'"
  1.1636 -    and "card B' = dim V"
  1.1637 -    by blast
  1.1638 -  with independent_span_bound[OF _ \<open>independent B\<close> \<open>B \<subseteq> span B'\<close>] independent_bound[of B']
  1.1639 -  show ?thesis by auto
  1.1640 -qed
  1.1641 -
  1.1642 -lemma span_card_ge_dim:
  1.1643 -  fixes B :: "'a::euclidean_space set"
  1.1644 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
  1.1645 -  by (metis basis_exists[of V] independent_span_bound subset_trans)
  1.1646 -
  1.1647 -lemma basis_card_eq_dim:
  1.1648 -  fixes V :: "'a::euclidean_space set"
  1.1649 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
  1.1650 -  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
  1.1651 -
  1.1652 -lemma dim_unique:
  1.1653 -  fixes B :: "'a::euclidean_space set"
  1.1654 -  shows "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
  1.1655 -  by (metis basis_card_eq_dim)
  1.1656 -
  1.1657 -text \<open>More lemmas about dimension.\<close>
  1.1658 -
  1.1659 -lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
  1.1660 -  using independent_Basis
  1.1661 -  by (intro dim_unique[of Basis]) auto
  1.1662 -
  1.1663 -lemma dim_subset:
  1.1664 -  fixes S :: "'a::euclidean_space set"
  1.1665 -  shows "S \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
  1.1666 -  using basis_exists[of T] basis_exists[of S]
  1.1667 -  by (metis independent_card_le_dim subset_trans)
  1.1668 -
  1.1669 -lemma dim_subset_UNIV:
  1.1670 -  fixes S :: "'a::euclidean_space set"
  1.1671 -  shows "dim S \<le> DIM('a)"
  1.1672 -  by (metis dim_subset subset_UNIV dim_UNIV)
  1.1673 -
  1.1674 -text \<open>Converses to those.\<close>
  1.1675 -
  1.1676 -lemma card_ge_dim_independent:
  1.1677 -  fixes B :: "'a::euclidean_space set"
  1.1678 -  assumes BV: "B \<subseteq> V"
  1.1679 -    and iB: "independent B"
  1.1680 -    and dVB: "dim V \<le> card B"
  1.1681 -  shows "V \<subseteq> span B"
  1.1682 -proof
  1.1683 -  fix a
  1.1684 -  assume aV: "a \<in> V"
  1.1685 -  {
  1.1686 -    assume aB: "a \<notin> span B"
  1.1687 -    then have iaB: "independent (insert a B)"
  1.1688 -      using iB aV BV by (simp add: independent_insert)
  1.1689 -    from aV BV have th0: "insert a B \<subseteq> V"
  1.1690 -      by blast
  1.1691 -    from aB have "a \<notin>B"
  1.1692 -      by (auto simp add: span_superset)
  1.1693 -    with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB]
  1.1694 -    have False by auto
  1.1695 -  }
  1.1696 -  then show "a \<in> span B" by blast
  1.1697 -qed
  1.1698 -
  1.1699 -lemma card_le_dim_spanning:
  1.1700 -  assumes BV: "(B:: ('a::euclidean_space) set) \<subseteq> V"
  1.1701 -    and VB: "V \<subseteq> span B"
  1.1702 -    and fB: "finite B"
  1.1703 -    and dVB: "dim V \<ge> card B"
  1.1704 -  shows "independent B"
  1.1705 -proof -
  1.1706 -  {
  1.1707 -    fix a
  1.1708 -    assume a: "a \<in> B" "a \<in> span (B - {a})"
  1.1709 -    from a fB have c0: "card B \<noteq> 0"
  1.1710 -      by auto
  1.1711 -    from a fB have cb: "card (B - {a}) = card B - 1"
  1.1712 -      by auto
  1.1713 -    from BV a have th0: "B - {a} \<subseteq> V"
  1.1714 -      by blast
  1.1715 -    {
  1.1716 -      fix x
  1.1717 -      assume x: "x \<in> V"
  1.1718 -      from a have eq: "insert a (B - {a}) = B"
  1.1719 -        by blast
  1.1720 -      from x VB have x': "x \<in> span B"
  1.1721 -        by blast
  1.1722 -      from span_trans[OF a(2), unfolded eq, OF x']
  1.1723 -      have "x \<in> span (B - {a})" .
  1.1724 -    }
  1.1725 -    then have th1: "V \<subseteq> span (B - {a})"
  1.1726 -      by blast
  1.1727 -    have th2: "finite (B - {a})"
  1.1728 -      using fB by auto
  1.1729 -    from span_card_ge_dim[OF th0 th1 th2]
  1.1730 -    have c: "dim V \<le> card (B - {a})" .
  1.1731 -    from c c0 dVB cb have False by simp
  1.1732 -  }
  1.1733 -  then show ?thesis
  1.1734 -    unfolding dependent_def by blast
  1.1735 -qed
  1.1736 -
  1.1737 -lemma card_eq_dim:
  1.1738 -  fixes B :: "'a::euclidean_space set"
  1.1739 -  shows "B \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
  1.1740 -  by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent)
  1.1741 -
  1.1742 -text \<open>More general size bound lemmas.\<close>
  1.1743 -
  1.1744 -lemma independent_bound_general:
  1.1745 -  fixes S :: "'a::euclidean_space set"
  1.1746 -  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> dim S"
  1.1747 -  by (metis independent_card_le_dim independent_bound subset_refl)
  1.1748 -
  1.1749 -lemma dependent_biggerset_general:
  1.1750 -  fixes S :: "'a::euclidean_space set"
  1.1751 -  shows "(finite S \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"
  1.1752 -  using independent_bound_general[of S] by (metis linorder_not_le)
  1.1753 -
  1.1754 -lemma dim_span [simp]:
  1.1755 -  fixes S :: "'a::euclidean_space set"
  1.1756 -  shows "dim (span S) = dim S"
  1.1757 -proof -
  1.1758 -  have th0: "dim S \<le> dim (span S)"
  1.1759 -    by (auto simp add: subset_eq intro: dim_subset span_superset)
  1.1760 -  from basis_exists[of S]
  1.1761 -  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
  1.1762 -    by blast
  1.1763 -  from B have fB: "finite B" "card B = dim S"
  1.1764 -    using independent_bound by blast+
  1.1765 -  have bSS: "B \<subseteq> span S"
  1.1766 -    using B(1) by (metis subset_eq span_inc)
  1.1767 -  have sssB: "span S \<subseteq> span B"
  1.1768 -    using span_mono[OF B(3)] by (simp add: span_span)
  1.1769 -  from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis
  1.1770 -    using fB(2) by arith
  1.1771 -qed
  1.1772 -
  1.1773 -lemma subset_le_dim:
  1.1774 -  fixes S :: "'a::euclidean_space set"
  1.1775 -  shows "S \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"
  1.1776 -  by (metis dim_span dim_subset)
  1.1777 -
  1.1778 -lemma span_eq_dim:
  1.1779 -  fixes S :: "'a::euclidean_space set"
  1.1780 -  shows "span S = span T \<Longrightarrow> dim S = dim T"
  1.1781 -  by (metis dim_span)
  1.1782 -
  1.1783 -lemma dim_image_le:
  1.1784 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  1.1785 -  assumes lf: "linear f"
  1.1786 -  shows "dim (f ` S) \<le> dim (S)"
  1.1787 -proof -
  1.1788 -  from basis_exists[of S] obtain B where
  1.1789 -    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
  1.1790 -  from B have fB: "finite B" "card B = dim S"
  1.1791 -    using independent_bound by blast+
  1.1792 -  have "dim (f ` S) \<le> card (f ` B)"
  1.1793 -    apply (rule span_card_ge_dim)
  1.1794 -    using lf B fB
  1.1795 -    apply (auto simp add: span_linear_image spans_image subset_image_iff)
  1.1796 -    done
  1.1797 -  also have "\<dots> \<le> dim S"
  1.1798 -    using card_image_le[OF fB(1)] fB by simp
  1.1799 -  finally show ?thesis .
  1.1800 -qed
  1.1801 -
  1.1802  text \<open>Picking an orthogonal replacement for a spanning set.\<close>
  1.1803  
  1.1804  lemma vector_sub_project_orthogonal:
  1.1805 @@ -2367,10 +763,10 @@
  1.1806      have "x - k *\<^sub>R (a - (\<Sum>x\<in>C. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x)) \<in> span C \<longleftrightarrow> x - k *\<^sub>R a \<in> span C"
  1.1807        apply (simp only: scaleR_right_diff_distrib th0)
  1.1808        apply (rule span_add_eq)
  1.1809 -      apply (rule span_mul)
  1.1810 +      apply (rule span_scale)
  1.1811        apply (rule span_sum)
  1.1812 -      apply (rule span_mul)
  1.1813 -      apply (rule span_superset)
  1.1814 +      apply (rule span_scale)
  1.1815 +      apply (rule span_base)
  1.1816        apply assumption
  1.1817        done
  1.1818    }
  1.1819 @@ -2402,7 +798,8 @@
  1.1820  
  1.1821  lemma orthogonal_basis_exists:
  1.1822    fixes V :: "('a::euclidean_space) set"
  1.1823 -  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (card B = dim V) \<and> pairwise orthogonal B"
  1.1824 +  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and>
  1.1825 +  (card B = dim V) \<and> pairwise orthogonal B"
  1.1826  proof -
  1.1827    from basis_exists[of V] obtain B where
  1.1828      B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
  1.1829 @@ -2413,7 +810,7 @@
  1.1830      C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C"
  1.1831      by blast
  1.1832    from C B have CSV: "C \<subseteq> span V"
  1.1833 -    by (metis span_inc span_mono subset_trans)
  1.1834 +    by (metis span_superset span_mono subset_trans)
  1.1835    from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
  1.1836      by (simp add: span_span)
  1.1837    from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
  1.1838 @@ -2423,7 +820,7 @@
  1.1839      by simp
  1.1840    moreover have "dim V \<le> card C"
  1.1841      using span_card_ge_dim[OF CSV SVC C(1)]
  1.1842 -    by (simp add: dim_span)
  1.1843 +    by simp
  1.1844    ultimately have CdV: "card C = dim V"
  1.1845      using C(1) by simp
  1.1846    from C B CSV CdV iC show ?thesis
  1.1847 @@ -2440,7 +837,8 @@
  1.1848    from sU obtain a where a: "a \<notin> span S"
  1.1849      by blast
  1.1850    from orthogonal_basis_exists obtain B where
  1.1851 -    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B"
  1.1852 +    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B"
  1.1853 +    "card B = dim S" "pairwise orthogonal B"
  1.1854      by blast
  1.1855    from B have fB: "finite B" "card B = dim S"
  1.1856      using independent_bound by auto
  1.1857 @@ -2451,8 +849,8 @@
  1.1858    have "sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
  1.1859      unfolding sSB
  1.1860      apply (rule span_sum)
  1.1861 -    apply (rule span_mul)
  1.1862 -    apply (rule span_superset)
  1.1863 +    apply (rule span_scale)
  1.1864 +    apply (rule span_base)
  1.1865      apply assumption
  1.1866      done
  1.1867    with a have a0:"?a  \<noteq> 0"
  1.1868 @@ -2504,7 +902,7 @@
  1.1869      then have "dim (span S) = dim (UNIV :: ('a) set)"
  1.1870        by simp
  1.1871      then have "dim S = DIM('a)"
  1.1872 -      by (simp add: dim_span dim_UNIV)
  1.1873 +      by (metis Euclidean_Space.dim_UNIV dim_span)
  1.1874      with d have False by arith
  1.1875    }
  1.1876    then have th: "span S \<noteq> UNIV"
  1.1877 @@ -2512,132 +910,15 @@
  1.1878    from span_not_univ_subset_hyperplane[OF th] show ?thesis .
  1.1879  qed
  1.1880  
  1.1881 -text \<open>We can extend a linear basis-basis injection to the whole set.\<close>
  1.1882 -
  1.1883 -lemma linear_indep_image_lemma:
  1.1884 -  assumes lf: "linear f"
  1.1885 -    and fB: "finite B"
  1.1886 -    and ifB: "independent (f ` B)"
  1.1887 -    and fi: "inj_on f B"
  1.1888 -    and xsB: "x \<in> span B"
  1.1889 -    and fx: "f x = 0"
  1.1890 -  shows "x = 0"
  1.1891 -  using fB ifB fi xsB fx
  1.1892 -proof (induct arbitrary: x rule: finite_induct[OF fB])
  1.1893 -  case 1
  1.1894 -  then show ?case by auto
  1.1895 -next
  1.1896 -  case (2 a b x)
  1.1897 -  have fb: "finite b" using "2.prems" by simp
  1.1898 -  have th0: "f ` b \<subseteq> f ` (insert a b)"
  1.1899 -    apply (rule image_mono)
  1.1900 -    apply blast
  1.1901 -    done
  1.1902 -  from independent_mono[ OF "2.prems"(2) th0]
  1.1903 -  have ifb: "independent (f ` b)"  .
  1.1904 -  have fib: "inj_on f b"
  1.1905 -    apply (rule subset_inj_on [OF "2.prems"(3)])
  1.1906 -    apply blast
  1.1907 -    done
  1.1908 -  from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
  1.1909 -  obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
  1.1910 -    by blast
  1.1911 -  have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
  1.1912 -    unfolding span_linear_image[OF lf]
  1.1913 -    apply (rule imageI)
  1.1914 -    using k span_mono[of "b - {a}" b]
  1.1915 -    apply blast
  1.1916 -    done
  1.1917 -  then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
  1.1918 -    by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
  1.1919 -  then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
  1.1920 -    using "2.prems"(5) by simp
  1.1921 -  have xsb: "x \<in> span b"
  1.1922 -  proof (cases "k = 0")
  1.1923 -    case True
  1.1924 -    with k have "x \<in> span (b - {a})" by simp
  1.1925 -    then show ?thesis using span_mono[of "b - {a}" b]
  1.1926 -      by blast
  1.1927 -  next
  1.1928 -    case False
  1.1929 -    with span_mul[OF th, of "- 1/ k"]
  1.1930 -    have th1: "f a \<in> span (f ` b)"
  1.1931 -      by auto
  1.1932 -    from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
  1.1933 -    have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
  1.1934 -    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
  1.1935 -    have "f a \<notin> span (f ` b)" using tha
  1.1936 -      using "2.hyps"(2)
  1.1937 -      "2.prems"(3) by auto
  1.1938 -    with th1 have False by blast
  1.1939 -    then show ?thesis by blast
  1.1940 -  qed
  1.1941 -  from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
  1.1942 -qed
  1.1943 -
  1.1944 -text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
  1.1945 -
  1.1946 -lemma subspace_isomorphism:
  1.1947 -  fixes S :: "'a::euclidean_space set"
  1.1948 -    and T :: "'b::euclidean_space set"
  1.1949 -  assumes s: "subspace S"
  1.1950 -    and t: "subspace T"
  1.1951 -    and d: "dim S = dim T"
  1.1952 -  shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"
  1.1953 -proof -
  1.1954 -  from basis_exists[of S] independent_bound
  1.1955 -  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B"
  1.1956 -    by blast
  1.1957 -  from basis_exists[of T] independent_bound
  1.1958 -  obtain C where C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C"
  1.1959 -    by blast
  1.1960 -  from B(4) C(4) card_le_inj[of B C] d
  1.1961 -  obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
  1.1962 -    by auto
  1.1963 -  from linear_independent_extend[OF B(2)]
  1.1964 -  obtain g where g: "linear g" "\<forall>x\<in> B. g x = f x"
  1.1965 -    by blast
  1.1966 -  from inj_on_iff_eq_card[OF fB, of f] f(2) have "card (f ` B) = card B"
  1.1967 -    by simp
  1.1968 -  with B(4) C(4) have ceq: "card (f ` B) = card C"
  1.1969 -    using d by simp
  1.1970 -  have "g ` B = f ` B"
  1.1971 -    using g(2) by (auto simp add: image_iff)
  1.1972 -  also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
  1.1973 -  finally have gBC: "g ` B = C" .
  1.1974 -  have gi: "inj_on g B"
  1.1975 -    using f(2) g(2) by (auto simp add: inj_on_def)
  1.1976 -  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
  1.1977 -  {
  1.1978 -    fix x y
  1.1979 -    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
  1.1980 -    from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
  1.1981 -      by blast+
  1.1982 -    from gxy have th0: "g (x - y) = 0"
  1.1983 -      by (simp add: linear_diff[OF g(1)])
  1.1984 -    have th1: "x - y \<in> span B"
  1.1985 -      using x' y' by (metis span_diff)
  1.1986 -    have "x = y"
  1.1987 -      using g0[OF th1 th0] by simp
  1.1988 -  }
  1.1989 -  then have giS: "inj_on g S"
  1.1990 -    unfolding inj_on_def by blast
  1.1991 -  from span_subspace[OF B(1,3) s] have "g ` S = span (g ` B)"
  1.1992 -    by (simp add: span_linear_image[OF g(1)])
  1.1993 -  also have "\<dots> = span C" unfolding gBC ..
  1.1994 -  also have "\<dots> = T" using span_subspace[OF C(1,3) t] .
  1.1995 -  finally have gS: "g ` S = T" .
  1.1996 -  from g(1) gS giS show ?thesis
  1.1997 -    by blast
  1.1998 -qed
  1.1999 -
  1.2000  lemma linear_eq_stdbasis:
  1.2001    fixes f :: "'a::euclidean_space \<Rightarrow> _"
  1.2002    assumes lf: "linear f"
  1.2003      and lg: "linear g"
  1.2004 -    and fg: "\<forall>b\<in>Basis. f b = g b"
  1.2005 +    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
  1.2006    shows "f = g"
  1.2007 -  using linear_eq[OF lf lg, of _ Basis] fg by auto
  1.2008 +  using linear_eq_on_span[OF lf lg, of Basis] fg
  1.2009 +  by auto
  1.2010 +
  1.2011  
  1.2012  text \<open>Similar results for bilinear functions.\<close>
  1.2013  
  1.2014 @@ -2652,7 +933,8 @@
  1.2015    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
  1.2016    from bf bg have sp: "subspace ?P"
  1.2017      unfolding bilinear_def linear_iff subspace_def bf bg
  1.2018 -    by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
  1.2019 +    by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
  1.2020 +        span_add Ball_def
  1.2021        intro: bilinear_ladd[OF bf])
  1.2022  
  1.2023    have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
  1.2024 @@ -2662,7 +944,8 @@
  1.2025      apply (simp add: fg)
  1.2026      apply (auto simp add: subspace_def)
  1.2027      using bf bg unfolding bilinear_def linear_iff
  1.2028 -    apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
  1.2029 +      apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg]
  1.2030 +        span_add Ball_def
  1.2031        intro: bilinear_ladd[OF bf])
  1.2032      done
  1.2033    then show ?thesis
  1.2034 @@ -2677,234 +960,6 @@
  1.2035    shows "f = g"
  1.2036    using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
  1.2037  
  1.2038 -text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
  1.2039 -
  1.2040 -lemma linear_injective_imp_surjective:
  1.2041 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2042 -  assumes lf: "linear f"
  1.2043 -    and fi: "inj f"
  1.2044 -  shows "surj f"
  1.2045 -proof -
  1.2046 -  let ?U = "UNIV :: 'a set"
  1.2047 -  from basis_exists[of ?U] obtain B
  1.2048 -    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "card B = dim ?U"
  1.2049 -    by blast
  1.2050 -  from B(4) have d: "dim ?U = card B"
  1.2051 -    by simp
  1.2052 -  have th: "?U \<subseteq> span (f ` B)"
  1.2053 -    apply (rule card_ge_dim_independent)
  1.2054 -    apply blast
  1.2055 -    apply (rule independent_injective_image[OF B(2) lf fi])
  1.2056 -    apply (rule order_eq_refl)
  1.2057 -    apply (rule sym)
  1.2058 -    unfolding d
  1.2059 -    apply (rule card_image)
  1.2060 -    apply (rule subset_inj_on[OF fi])
  1.2061 -    apply blast
  1.2062 -    done
  1.2063 -  from th show ?thesis
  1.2064 -    unfolding span_linear_image[OF lf] surj_def
  1.2065 -    using B(3) by blast
  1.2066 -qed
  1.2067 -
  1.2068 -text \<open>And vice versa.\<close>
  1.2069 -
  1.2070 -lemma surjective_iff_injective_gen:
  1.2071 -  assumes fS: "finite S"
  1.2072 -    and fT: "finite T"
  1.2073 -    and c: "card S = card T"
  1.2074 -    and ST: "f ` S \<subseteq> T"
  1.2075 -  shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
  1.2076 -  (is "?lhs \<longleftrightarrow> ?rhs")
  1.2077 -proof
  1.2078 -  assume h: "?lhs"
  1.2079 -  {
  1.2080 -    fix x y
  1.2081 -    assume x: "x \<in> S"
  1.2082 -    assume y: "y \<in> S"
  1.2083 -    assume f: "f x = f y"
  1.2084 -    from x fS have S0: "card S \<noteq> 0"
  1.2085 -      by auto
  1.2086 -    have "x = y"
  1.2087 -    proof (rule ccontr)
  1.2088 -      assume xy: "\<not> ?thesis"
  1.2089 -      have th: "card S \<le> card (f ` (S - {y}))"
  1.2090 -        unfolding c
  1.2091 -        apply (rule card_mono)
  1.2092 -        apply (rule finite_imageI)
  1.2093 -        using fS apply simp
  1.2094 -        using h xy x y f unfolding subset_eq image_iff
  1.2095 -        apply auto
  1.2096 -        apply (case_tac "xa = f x")
  1.2097 -        apply (rule bexI[where x=x])
  1.2098 -        apply auto
  1.2099 -        done
  1.2100 -      also have " \<dots> \<le> card (S - {y})"
  1.2101 -        apply (rule card_image_le)
  1.2102 -        using fS by simp
  1.2103 -      also have "\<dots> \<le> card S - 1" using y fS by simp
  1.2104 -      finally show False using S0 by arith
  1.2105 -    qed
  1.2106 -  }
  1.2107 -  then show ?rhs
  1.2108 -    unfolding inj_on_def by blast
  1.2109 -next
  1.2110 -  assume h: ?rhs
  1.2111 -  have "f ` S = T"
  1.2112 -    apply (rule card_subset_eq[OF fT ST])
  1.2113 -    unfolding card_image[OF h]
  1.2114 -    apply (rule c)
  1.2115 -    done
  1.2116 -  then show ?lhs by blast
  1.2117 -qed
  1.2118 -
  1.2119 -lemma linear_surjective_imp_injective:
  1.2120 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2121 -  assumes lf: "linear f"
  1.2122 -    and sf: "surj f"
  1.2123 -  shows "inj f"
  1.2124 -proof -
  1.2125 -  let ?U = "UNIV :: 'a set"
  1.2126 -  from basis_exists[of ?U] obtain B
  1.2127 -    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U"
  1.2128 -    by blast
  1.2129 -  {
  1.2130 -    fix x
  1.2131 -    assume x: "x \<in> span B"
  1.2132 -    assume fx: "f x = 0"
  1.2133 -    from B(2) have fB: "finite B"
  1.2134 -      using independent_bound by auto
  1.2135 -    have fBi: "independent (f ` B)"
  1.2136 -      apply (rule card_le_dim_spanning[of "f ` B" ?U])
  1.2137 -      apply blast
  1.2138 -      using sf B(3)
  1.2139 -      unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
  1.2140 -      apply blast
  1.2141 -      using fB apply blast
  1.2142 -      unfolding d[symmetric]
  1.2143 -      apply (rule card_image_le)
  1.2144 -      apply (rule fB)
  1.2145 -      done
  1.2146 -    have th0: "dim ?U \<le> card (f ` B)"
  1.2147 -      apply (rule span_card_ge_dim)
  1.2148 -      apply blast
  1.2149 -      unfolding span_linear_image[OF lf]
  1.2150 -      apply (rule subset_trans[where B = "f ` UNIV"])
  1.2151 -      using sf unfolding surj_def
  1.2152 -      apply blast
  1.2153 -      apply (rule image_mono)
  1.2154 -      apply (rule B(3))
  1.2155 -      apply (metis finite_imageI fB)
  1.2156 -      done
  1.2157 -    moreover have "card (f ` B) \<le> card B"
  1.2158 -      by (rule card_image_le, rule fB)
  1.2159 -    ultimately have th1: "card B = card (f ` B)"
  1.2160 -      unfolding d by arith
  1.2161 -    have fiB: "inj_on f B"
  1.2162 -      unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
  1.2163 -      by blast
  1.2164 -    from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
  1.2165 -    have "x = 0" by blast
  1.2166 -  }
  1.2167 -  then show ?thesis
  1.2168 -    unfolding linear_injective_0[OF lf]
  1.2169 -    using B(3)
  1.2170 -    by blast
  1.2171 -qed
  1.2172 -
  1.2173 -text \<open>Hence either is enough for isomorphism.\<close>
  1.2174 -
  1.2175 -lemma left_right_inverse_eq:
  1.2176 -  assumes fg: "f \<circ> g = id"
  1.2177 -    and gh: "g \<circ> h = id"
  1.2178 -  shows "f = h"
  1.2179 -proof -
  1.2180 -  have "f = f \<circ> (g \<circ> h)"
  1.2181 -    unfolding gh by simp
  1.2182 -  also have "\<dots> = (f \<circ> g) \<circ> h"
  1.2183 -    by (simp add: o_assoc)
  1.2184 -  finally show "f = h"
  1.2185 -    unfolding fg by simp
  1.2186 -qed
  1.2187 -
  1.2188 -lemma isomorphism_expand:
  1.2189 -  "f \<circ> g = id \<and> g \<circ> f = id \<longleftrightarrow> (\<forall>x. f (g x) = x) \<and> (\<forall>x. g (f x) = x)"
  1.2190 -  by (simp add: fun_eq_iff o_def id_def)
  1.2191 -
  1.2192 -lemma linear_injective_isomorphism:
  1.2193 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2194 -  assumes lf: "linear f"
  1.2195 -    and fi: "inj f"
  1.2196 -  shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
  1.2197 -  unfolding isomorphism_expand[symmetric]
  1.2198 -  using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]]
  1.2199 -    linear_injective_left_inverse[OF lf fi]
  1.2200 -  by (metis left_right_inverse_eq)
  1.2201 -
  1.2202 -lemma linear_surjective_isomorphism:
  1.2203 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2204 -  assumes lf: "linear f"
  1.2205 -    and sf: "surj f"
  1.2206 -  shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
  1.2207 -  unfolding isomorphism_expand[symmetric]
  1.2208 -  using linear_surjective_right_inverse[OF lf sf]
  1.2209 -    linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]
  1.2210 -  by (metis left_right_inverse_eq)
  1.2211 -
  1.2212 -text \<open>Left and right inverses are the same for
  1.2213 -  @{typ "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"}.\<close>
  1.2214 -
  1.2215 -lemma linear_inverse_left:
  1.2216 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2217 -  assumes lf: "linear f"
  1.2218 -    and lf': "linear f'"
  1.2219 -  shows "f \<circ> f' = id \<longleftrightarrow> f' \<circ> f = id"
  1.2220 -proof -
  1.2221 -  {
  1.2222 -    fix f f':: "'a \<Rightarrow> 'a"
  1.2223 -    assume lf: "linear f" "linear f'"
  1.2224 -    assume f: "f \<circ> f' = id"
  1.2225 -    from f have sf: "surj f"
  1.2226 -      apply (auto simp add: o_def id_def surj_def)
  1.2227 -      apply metis
  1.2228 -      done
  1.2229 -    from linear_surjective_isomorphism[OF lf(1) sf] lf f
  1.2230 -    have "f' \<circ> f = id"
  1.2231 -      unfolding fun_eq_iff o_def id_def by metis
  1.2232 -  }
  1.2233 -  then show ?thesis
  1.2234 -    using lf lf' by metis
  1.2235 -qed
  1.2236 -
  1.2237 -text \<open>Moreover, a one-sided inverse is automatically linear.\<close>
  1.2238 -
  1.2239 -lemma left_inverse_linear:
  1.2240 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2241 -  assumes lf: "linear f"
  1.2242 -    and gf: "g \<circ> f = id"
  1.2243 -  shows "linear g"
  1.2244 -proof -
  1.2245 -  from gf have fi: "inj f"
  1.2246 -    apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
  1.2247 -    apply metis
  1.2248 -    done
  1.2249 -  from linear_injective_isomorphism[OF lf fi]
  1.2250 -  obtain h :: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
  1.2251 -    by blast
  1.2252 -  have "h = g"
  1.2253 -    apply (rule ext) using gf h(2,3)
  1.2254 -    apply (simp add: o_def id_def fun_eq_iff)
  1.2255 -    apply metis
  1.2256 -    done
  1.2257 -  with h(1) show ?thesis by blast
  1.2258 -qed
  1.2259 -
  1.2260 -lemma inj_linear_imp_inv_linear:
  1.2261 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  1.2262 -  assumes "linear f" "inj f" shows "linear (inv f)"
  1.2263 -using assms inj_iff left_inverse_linear by blast
  1.2264 -
  1.2265 -
  1.2266  subsection \<open>Infinity norm\<close>
  1.2267  
  1.2268  definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
  1.2269 @@ -3181,7 +1236,7 @@
  1.2270    qed
  1.2271    then show ?thesis
  1.2272      apply (clarsimp simp: collinear_def)
  1.2273 -    by (metis real_vector.scale_zero_right vector_fraction_eq_iff)
  1.2274 +    by (metis scaleR_zero_right vector_fraction_eq_iff)
  1.2275  qed
  1.2276  
  1.2277  lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"