src/HOL/Analysis/Linear_Algebra.thy
 changeset 68069 36209dfb981e parent 68062 ee88c0fccbae child 68073 fad29d2a17a5
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 12:48:08 2018 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 23:32:47 2018 +0100
1.3 @@ -155,11 +155,7 @@
1.4  qed
1.5
1.6  lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
1.7 -  unfolding linear_iff
1.8 -  apply clarsimp
1.9 -  apply (erule allE[where x="0::'a"])
1.10 -  apply simp
1.11 -  done
1.12 +  unfolding linear_iff  by (metis real_vector.scale_zero_left)
1.13
1.14  lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
1.15    by (rule linear.scaleR)
1.16 @@ -284,18 +280,28 @@
1.17
1.18  lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
1.19    unfolding span_def
1.20 -  apply (rule hull_in)
1.21 -  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
1.22 -  apply auto
1.23 -  done
1.24 -
1.25 -lemma (in real_vector) span_clauses:
1.26 -  "a \<in> S \<Longrightarrow> a \<in> span S"
1.27 -  "0 \<in> span S"
1.28 -  "x\<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
1.29 -  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
1.30 +  by (rule hull_in) (auto simp: subspace_def)
1.31 +
1.32 +lemma (in real_vector) span_superset: "a \<in> S \<Longrightarrow> a \<in> span S"
1.33 +        and span_0 [simp]: "0 \<in> span S"
1.34 +        and span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
1.35 +        and span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
1.36    by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+
1.37
1.38 +lemmas (in real_vector) span_clauses = span_superset span_0 span_add span_mul
1.39 +
1.40 +lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
1.41 +  by (metis subspace_neg subspace_span)
1.42 +
1.43 +lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
1.44 +  by (metis subspace_span subspace_diff)
1.45 +
1.46 +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.47 +  by (rule subspace_sum [OF subspace_span])
1.48 +
1.49 +lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
1.50 +  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
1.51 +
1.52  lemma span_unique:
1.53    "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
1.54    unfolding span_def by (rule hull_unique)
1.55 @@ -306,7 +312,7 @@
1.56  lemma span_UNIV [simp]: "span UNIV = UNIV"
1.57    by (intro span_unique) auto
1.58
1.59 -lemma (in real_vector) span_induct:
1.60 +lemma (in real_vector) span_induct [consumes 1, case_names base step, induct set: span]:
1.61    assumes x: "x \<in> span S"
1.62      and P: "subspace (Collect P)"
1.63      and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
1.64 @@ -320,10 +326,8 @@
1.65  qed
1.66
1.67  lemma span_empty[simp]: "span {} = {0}"
1.68 -  apply (simp add: span_def)
1.69 -  apply (rule hull_unique)
1.70 -  apply (auto simp add: subspace_def)
1.71 -  done
1.72 +  unfolding span_def
1.73 +  by (rule hull_unique) (auto simp add: subspace_def)
1.74
1.75  lemma (in real_vector) independent_empty [iff]: "independent {}"
1.77 @@ -345,87 +349,53 @@
1.78      "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow>
1.79        (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
1.80
1.81 -lemma span_induct_alt':
1.82 -  assumes h0: "h 0"
1.83 +lemma span_induct_alt [consumes 1, case_names base step, induct set: span]:
1.84 +  assumes x: "x \<in> span S"
1.85 +    and h0: "h 0"
1.86      and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
1.87 -  shows "\<forall>x \<in> span S. h x"
1.88 +  shows "h x"
1.89  proof -
1.90 -  {
1.91 -    fix x :: 'a
1.92 -    assume x: "x \<in> span_induct_alt_help S"
1.93 -    have "h x"
1.94 -      apply (rule span_induct_alt_help.induct[OF x])
1.95 -      apply (rule h0)
1.96 -      apply (rule hS)
1.97 -      apply assumption
1.98 -      apply assumption
1.99 -      done
1.100 -  }
1.101 -  note th0 = this
1.102 -  {
1.103 -    fix x
1.104 -    assume x: "x \<in> span S"
1.105 -    have "x \<in> span_induct_alt_help S"
1.106 -    proof (rule span_induct[where x=x and S=S])
1.107 -      show "x \<in> span S" by (rule x)
1.108 -    next
1.109 -      fix x
1.110 -      assume xS: "x \<in> S"
1.111 -      from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
1.112 -      show "x \<in> span_induct_alt_help S"
1.113 -        by simp
1.114 -    next
1.115 -      have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
1.116 -      moreover
1.117 -      {
1.118 -        fix x y
1.119 -        assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
1.120 -        from h have "(x + y) \<in> span_induct_alt_help S"
1.121 -          apply (induct rule: span_induct_alt_help.induct)
1.122 -          apply simp
1.124 -          apply (rule span_induct_alt_help_S)
1.125 -          apply assumption
1.126 -          apply simp
1.127 -          done
1.128 -      }
1.129 -      moreover
1.130 -      {
1.131 -        fix c x
1.132 -        assume xt: "x \<in> span_induct_alt_help S"
1.133 -        then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
1.134 -          apply (induct rule: span_induct_alt_help.induct)
1.135 -          apply (simp add: span_induct_alt_help_0)
1.136 -          apply (simp add: scaleR_right_distrib)
1.137 -          apply (rule span_induct_alt_help_S)
1.138 -          apply assumption
1.139 -          apply simp
1.140 -          done }
1.141 -      ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
1.142 -        unfolding subspace_def Ball_def by blast
1.143 -    qed
1.144 -  }
1.145 -  with th0 show ?thesis by blast
1.146 +  have th0: "h x" if "x \<in> span_induct_alt_help S" for x
1.147 +    by (metis span_induct_alt_help.induct[OF that] h0 hS)
1.148 +  have "x \<in> span_induct_alt_help S" if "x \<in> span S" for x
1.149 +    using that
1.150 +  proof (induction x rule: span_induct)
1.151 +    case base
1.152 +    have 0: "0 \<in> span_induct_alt_help S"
1.153 +      by (rule span_induct_alt_help_0)
1.154 +    moreover
1.155 +    have "(x + y) \<in> span_induct_alt_help S"
1.156 +      if "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S" for x y
1.157 +      using that
1.158 +      by induct (auto simp: add.assoc span_induct_alt_help.span_induct_alt_help_S)
1.159 +    moreover
1.160 +    have "(c *\<^sub>R x) \<in> span_induct_alt_help S" if "x \<in> span_induct_alt_help S" for c x
1.161 +      using that
1.162 +      proof (induction rule: span_induct_alt_help.induct)
1.163 +        case span_induct_alt_help_0
1.164 +        then show ?case
1.165 +          by (simp add: 0)
1.166 +      next
1.167 +        case (span_induct_alt_help_S x z c)
1.168 +        then show ?case
1.170 +      qed
1.171 +    ultimately show ?case
1.172 +      unfolding subspace_def Ball_def by blast
1.173 +  next
1.174 +    case (step x)
1.175 +    then show ?case
1.176 +      using span_induct_alt_help_S[OF step span_induct_alt_help_0, of 1]
1.177 +      by simp
1.178 +  qed
1.179 +  with th0 x show ?thesis by blast
1.180  qed
1.181
1.182 -lemma span_induct_alt:
1.183 -  assumes h0: "h 0"
1.184 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
1.185 -    and x: "x \<in> span S"
1.186 -  shows "h x"
1.187 -  using span_induct_alt'[of h S] h0 hS x by blast
1.188 -
1.189  text \<open>Individual closure properties.\<close>
1.190
1.191  lemma span_span: "span (span A) = span A"
1.192    unfolding span_def hull_hull ..
1.193
1.194 -lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
1.195 -  by (metis span_clauses(1))
1.196 -
1.197 -lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
1.198 -  by (metis subspace_span subspace_0)
1.199 -
1.200  lemma span_inc: "S \<subseteq> span S"
1.201    by (metis subset_eq span_superset)
1.202
1.203 @@ -437,26 +407,7 @@
1.204    assumes "0 \<in> A"
1.205    shows "dependent A"
1.206    unfolding dependent_def
1.207 -  using assms span_0
1.208 -  by blast
1.209 -
1.210 -lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
1.211 -  by (metis subspace_add subspace_span)
1.212 -
1.213 -lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
1.214 -  by (metis subspace_span subspace_mul)
1.215 -
1.216 -lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
1.217 -  by (metis subspace_neg subspace_span)
1.218 -
1.219 -lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
1.220 -  by (metis subspace_span subspace_diff)
1.221 -
1.222 -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.223 -  by (rule subspace_sum [OF subspace_span])
1.224 -
1.225 -lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
1.226 -  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
1.227 +  using assms span_0 by blast
1.228
1.229  text \<open>The key breakdown property.\<close>
1.230
1.231 @@ -539,11 +490,9 @@
1.232  proof -
1.233    have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
1.234      unfolding span_Un span_singleton
1.235 -    apply safe
1.236 -    apply (rule_tac x=k in exI, simp)
1.237 -    apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
1.238 -    apply auto
1.239 -    done
1.240 +    apply (auto simp: image_iff)
1.242 +    by force
1.243    then show ?thesis by simp
1.244  qed
1.245
1.246 @@ -612,30 +561,30 @@
1.247
1.248  lemma span_explicit:
1.249    "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
1.250 -  (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
1.251 +  (is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
1.252  proof -
1.253 -  {
1.254 -    fix x
1.255 -    assume "?h x"
1.256 -    then obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
1.257 +  have "x \<in> span P" if "?h x" for x
1.258 +  proof -
1.259 +    from that
1.260 +    obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
1.261        by blast
1.262 -    then have "x \<in> span P"
1.263 +    then show ?thesis
1.264        by (auto intro: span_sum span_mul span_superset)
1.265 -  }
1.266 +  qed
1.267    moreover
1.268 -  have "\<forall>x \<in> span P. ?h x"
1.269 -  proof (rule span_induct_alt')
1.270 -    show "?h 0"
1.271 -      by (rule exI[where x="{}"], simp)
1.272 +  have "?h x" if "x \<in> span P" for x
1.273 +    using that
1.274 +  proof (induction rule: span_induct_alt)
1.275 +    case base
1.276 +    then show ?case
1.277 +      by force
1.278    next
1.279 -    fix c x y
1.280 -    assume x: "x \<in> P"
1.281 -    assume hy: "?h y"
1.282 -    from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
1.283 +    case (step c x y)
1.284 +    then obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
1.285        and u: "sum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
1.286      let ?S = "insert x S"
1.287      let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
1.288 -    from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
1.289 +    from fS SP step have th0: "finite (insert x S)" "insert x S \<subseteq> P"
1.290        by blast+
1.291      have "?Q ?S ?u (c*\<^sub>R x + y)"
1.292      proof cases
1.293 @@ -650,16 +599,13 @@
1.294        then show ?thesis using th0 by blast
1.295      next
1.296        assume xS: "x \<notin> S"
1.297 -      have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
1.298 +      have "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
1.299          unfolding u[symmetric]
1.300 -        apply (rule sum.cong)
1.301 -        using xS
1.302 -        apply auto
1.303 -        done
1.304 -      show ?thesis using fS xS th0
1.306 +        by (rule sum.cong) (use xS in auto)
1.307 +      then show ?thesis using fS xS th0
1.309      qed
1.310 -    then show "?h (c*\<^sub>R x + y)"
1.311 +    then show ?case
1.312        by fast
1.313    qed
1.314    ultimately show ?thesis by blast
1.315 @@ -679,16 +625,13 @@
1.316      let ?v = a
1.317      from aP SP have aS: "a \<notin> S"
1.318        by blast
1.319 -    from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
1.320 +    have "(\<Sum>v\<in>S. (if v = a then - 1 else u v) *\<^sub>R v) = (\<Sum>v\<in>S. u v *\<^sub>R v)"
1.321 +      using aS by (auto intro: sum.cong)
1.322 +    then have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
1.323 +      using fS aS by (simp add: ua)
1.324 +    moreover from fS SP aP have "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
1.325        by auto
1.326 -    have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
1.327 -      using fS aS
1.328 -      apply simp
1.329 -      apply (subst (2) ua[symmetric])
1.330 -      apply (rule sum.cong)
1.331 -      apply auto
1.332 -      done
1.333 -    with th0 have ?rhs by fast
1.334 +    ultimately have ?rhs by fast
1.335    }
1.336    moreover
1.337    {
1.338 @@ -817,13 +760,7 @@
1.339      assume i: ?lhs
1.340      then show ?rhs
1.341        using False
1.342 -      apply simp
1.343 -      apply (rule conjI)
1.344 -      apply (rule independent_mono)
1.345 -      apply assumption
1.346 -      apply blast
1.347 -      apply (simp add: dependent_def)
1.348 -      done
1.349 +      using dependent_def independent_mono by fastforce
1.350    next
1.351      assume i: ?rhs
1.352      show ?lhs
1.353 @@ -868,7 +805,7 @@
1.354
1.355  lemma maximal_independent_subset_extend:
1.356    assumes "S \<subseteq> V" "independent S"
1.357 -  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
1.358 +  obtains B where "S \<subseteq> B" "B \<subseteq> V" "independent B" "V \<subseteq> span B"
1.359  proof -
1.360    let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
1.361    have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
1.362 @@ -909,12 +846,12 @@
1.363      with \<open>v \<notin> span B\<close> have False
1.364        by (auto intro: span_superset) }
1.365    ultimately show ?thesis
1.366 -    by (auto intro!: exI[of _ B])
1.367 +    by (meson that)
1.368  qed
1.369
1.370
1.371  lemma maximal_independent_subset:
1.372 -  "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
1.373 +  obtains B where "B \<subseteq> V" "independent B" "V \<subseteq> span B"
1.374    by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
1.375
1.376  lemma span_finite:
1.377 @@ -1043,9 +980,8 @@
1.378  lemma subspace_kernel:
1.379    assumes lf: "linear f"
1.380    shows "subspace {x. f x = 0}"
1.381 -  apply (simp add: subspace_def)
1.383 -  done
1.384 +  unfolding subspace_def
1.386
1.387  lemma linear_eq_0_span:
1.388    assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
1.389 @@ -1075,7 +1011,8 @@
1.390    from span_mono[OF BA] span_mono[OF AsB]
1.391    have sAB: "span A = span B" unfolding span_span by blast
1.392
1.393 -  {
1.394 +  show "A \<subseteq> B"
1.395 +  proof
1.396      fix x
1.397      assume x: "x \<in> A"
1.398      from iA have th0: "x \<notin> span (A - {x})"
1.399 @@ -1085,7 +1022,8 @@
1.400      have "A - {x} \<subseteq> A" by blast
1.401      then have th1: "span (A - {x}) \<subseteq> span A"
1.402        by (metis span_mono)
1.403 -    {
1.404 +    show "x \<in> B"
1.405 +    proof (rule ccontr)
1.406        assume xB: "x \<notin> B"
1.407        from xB BA have "B \<subseteq> A - {x}"
1.408          by blast
1.409 @@ -1093,12 +1031,10 @@
1.410          by (metis span_mono)
1.411        with th1 th0 sAB have "x \<notin> span A"
1.412          by blast
1.413 -      with x have False
1.414 +      with x show False
1.415          by (metis span_superset)
1.416 -    }
1.417 -    then have "x \<in> B" by blast
1.418 -  }
1.419 -  then show "A \<subseteq> B" by blast
1.420 +    qed
1.421 +  qed
1.422  qed
1.423
1.424  text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
1.425 @@ -1121,21 +1057,20 @@
1.426      and lf: "linear f"
1.427      and fi: "inj_on f (span S)"
1.428    shows "independent (f ` S)"
1.429 -proof -
1.430 -  {
1.431 -    fix a
1.432 -    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
1.433 -    have eq: "f ` S - {f a} = f ` (S - {a})"
1.434 -      using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
1.435 -    from a have "f a \<in> f ` span (S - {a})"
1.436 -      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
1.437 -    then have "a \<in> span (S - {a})"
1.438 -      by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
1.439 -         (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
1.440 -    with a(1) iS have False
1.441 -      by (simp add: dependent_def)
1.442 -  }
1.443 -  then show ?thesis
1.444 +  unfolding dependent_def
1.445 +proof clarsimp
1.446 +  fix a
1.447 +  assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
1.448 +  have eq: "f ` S - {f a} = f ` (S - {a})"
1.449 +    using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
1.450 +  from a have "f a \<in> f ` span (S - {a})"
1.451 +    unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
1.452 +  then have "a \<in> span (S - {a})"
1.453 +    by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
1.454 +      (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
1.455 +  with a(1) iS have False
1.456 +    by (simp add: dependent_def)
1.457 +  then show False
1.458      unfolding dependent_def by blast
1.459  qed
1.460
1.461 @@ -1150,7 +1085,7 @@
1.462    shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
1.463  proof -
1.464    obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
1.465 -    using maximal_independent_subset[of S] by auto
1.466 +    using maximal_independent_subset[of S] .
1.467    then have "span S = span B"
1.468      unfolding span_eq by (auto simp: span_superset)
1.469    with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
1.470 @@ -1176,14 +1111,14 @@
1.471  qed
1.472
1.473  lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
1.474 -  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
1.475 +  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff)
1.476
1.477  lemma linear_surj_right_inverse:
1.478    assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
1.479    shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
1.480  proof -
1.481    obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
1.482 -    using maximal_independent_subset[of T] by auto
1.483 +    using maximal_independent_subset[of T] .
1.484    then have "span T = span B"
1.485      unfolding span_eq by (auto simp: span_superset)
1.486
1.487 @@ -1206,133 +1141,116 @@
1.488
1.489  lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
1.490    using linear_surj_right_inverse[of f UNIV UNIV]
1.491 -  by (auto simp: span_UNIV fun_eq_iff)
1.492 +  by (auto simp: fun_eq_iff)
1.493
1.494  text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
1.495
1.496  lemma exchange_lemma:
1.497 -  assumes f:"finite t"
1.498 -    and i: "independent s"
1.499 -    and sp: "s \<subseteq> span t"
1.500 -  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.501 +  assumes f: "finite T"
1.502 +    and i: "independent S"
1.503 +    and sp: "S \<subseteq> span T"
1.504 +  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.505    using f i sp
1.506 -proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
1.507 +proof (induct "card (T - S)" arbitrary: S T rule: less_induct)
1.508    case less
1.509 -  note ft = \<open>finite t\<close> and s = \<open>independent s\<close> and sp = \<open>s \<subseteq> span t\<close>
1.510 -  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.511 -  let ?ths = "\<exists>t'. ?P t'"
1.512 -  {
1.513 -    assume "s \<subseteq> t"
1.514 -    then have ?ths
1.515 -      by (metis ft Un_commute sp sup_ge1)
1.516 -  }
1.517 -  moreover
1.518 -  {
1.519 -    assume st: "t \<subseteq> s"
1.520 -    from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
1.521 -    have ?ths
1.522 -      by (metis Un_absorb sp)
1.523 -  }
1.524 -  moreover
1.525 -  {
1.526 -    assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
1.527 -    from st(2) obtain b where b: "b \<in> t" "b \<notin> s"
1.528 +  note ft = \<open>finite T\<close> and S = \<open>independent S\<close> and sp = \<open>S \<subseteq> span T\<close>
1.529 +  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.530 +  show ?case
1.531 +  proof (cases "S \<subseteq> T \<or> T \<subseteq> S")
1.532 +    case True
1.533 +    then show ?thesis
1.534 +    proof
1.535 +      assume "S \<subseteq> T" then show ?thesis
1.536 +        by (metis ft Un_commute sp sup_ge1)
1.537 +    next
1.538 +      assume "T \<subseteq> S" then show ?thesis
1.539 +        by (metis Un_absorb sp spanning_subset_independent[OF _ S sp] ft)
1.540 +    qed
1.541 +  next
1.542 +    case False
1.543 +    then have st: "\<not> S \<subseteq> T" "\<not> T \<subseteq> S"
1.544 +      by auto
1.545 +    from st(2) obtain b where b: "b \<in> T" "b \<notin> S"
1.546        by blast
1.547 -    from b have "t - {b} - s \<subset> t - s"
1.548 +    from b have "T - {b} - S \<subset> T - S"
1.549        by blast
1.550 -    then have cardlt: "card (t - {b} - s) < card (t - s)"
1.551 +    then have cardlt: "card (T - {b} - S) < card (T - S)"
1.552        using ft by (auto intro: psubset_card_mono)
1.553 -    from b ft have ct0: "card t \<noteq> 0"
1.554 +    from b ft have ct0: "card T \<noteq> 0"
1.555        by auto
1.556 -    have ?ths
1.557 -    proof cases
1.558 -      assume stb: "s \<subseteq> span (t - {b})"
1.559 -      from ft have ftb: "finite (t - {b})"
1.560 +    show ?thesis
1.561 +    proof (cases "S \<subseteq> span (T - {b})")
1.562 +      case True
1.563 +      from ft have ftb: "finite (T - {b})"
1.564          by auto
1.565 -      from less(1)[OF cardlt ftb s stb]
1.566 -      obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
1.567 -        and fu: "finite u" by blast
1.568 -      let ?w = "insert b u"
1.569 -      have th0: "s \<subseteq> insert b u"
1.570 -        using u by blast
1.571 -      from u(3) b have "u \<subseteq> s \<union> t"
1.572 -        by blast
1.573 -      then have th1: "insert b u \<subseteq> s \<union> t"
1.574 -        using u b by blast
1.575 -      have bu: "b \<notin> u"
1.576 -        using b u by blast
1.577 -      from u(1) ft b have "card u = (card t - 1)"
1.578 +      from less(1)[OF cardlt ftb S True]
1.579 +      obtain U where U: "card U = card (T - {b})" "S \<subseteq> U" "U \<subseteq> S \<union> (T - {b})" "S \<subseteq> span U"
1.580 +        and fu: "finite U" by blast
1.581 +      let ?w = "insert b U"
1.582 +      have th0: "S \<subseteq> insert b U"
1.583 +        using U by blast
1.584 +      have th1: "insert b U \<subseteq> S \<union> T"
1.585 +        using U b by blast
1.586 +      have bu: "b \<notin> U"
1.587 +        using b U by blast
1.588 +      from U(1) ft b have "card U = (card T - 1)"
1.589          by auto
1.590 -      then have th2: "card (insert b u) = card t"
1.591 +      then have th2: "card (insert b U) = card T"
1.592          using card_insert_disjoint[OF fu bu] ct0 by auto
1.593 -      from u(4) have "s \<subseteq> span u" .
1.594 -      also have "\<dots> \<subseteq> span (insert b u)"
1.595 +      from U(4) have "S \<subseteq> span U" .
1.596 +      also have "\<dots> \<subseteq> span (insert b U)"
1.597          by (rule span_mono) blast
1.598 -      finally have th3: "s \<subseteq> span (insert b u)" .
1.599 +      finally have th3: "S \<subseteq> span (insert b U)" .
1.600        from th0 th1 th2 th3 fu have th: "?P ?w"
1.601          by blast
1.602        from th show ?thesis by blast
1.603      next
1.604 -      assume stb: "\<not> s \<subseteq> span (t - {b})"
1.605 -      from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
1.606 +      case False
1.607 +      then obtain a where a: "a \<in> S" "a \<notin> span (T - {b})"
1.608          by blast
1.609        have ab: "a \<noteq> b"
1.610          using a b by blast
1.611 -      have at: "a \<notin> t"
1.612 -        using a ab span_superset[of a "t- {b}"] by auto
1.613 -      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
1.614 +      have at: "a \<notin> T"
1.615 +        using a ab span_superset[of a "T- {b}"] by auto
1.616 +      have mlt: "card ((insert a (T - {b})) - S) < card (T - S)"
1.617          using cardlt ft a b by auto
1.618 -      have ft': "finite (insert a (t - {b}))"
1.619 +      have ft': "finite (insert a (T - {b}))"
1.620          using ft by auto
1.621 -      {
1.622 +      have sp': "S \<subseteq> span (insert a (T - {b}))"
1.623 +      proof
1.624          fix x
1.625 -        assume xs: "x \<in> s"
1.626 -        have t: "t \<subseteq> insert b (insert a (t - {b}))"
1.627 +        assume xs: "x \<in> S"
1.628 +        have T: "T \<subseteq> insert b (insert a (T - {b}))"
1.629            using b by auto
1.630 -        from b(1) have "b \<in> span t"
1.631 -          by (simp add: span_superset)
1.632 -        have bs: "b \<in> span (insert a (t - {b}))"
1.633 -          apply (rule in_span_delete)
1.634 -          using a sp unfolding subset_eq
1.635 -          apply auto
1.636 -          done
1.637 -        from xs sp have "x \<in> span t"
1.638 +        have bs: "b \<in> span (insert a (T - {b}))"
1.639 +          by (rule in_span_delete) (use a sp in auto)
1.640 +        from xs sp have "x \<in> span T"
1.641            by blast
1.642 -        with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" ..
1.643 -        from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .
1.644 -      }
1.645 -      then have sp': "s \<subseteq> span (insert a (t - {b}))"
1.646 -        by blast
1.647 -      from less(1)[OF mlt ft' s sp'] obtain u where u:
1.648 -        "card u = card (insert a (t - {b}))"
1.649 -        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
1.650 -        "s \<subseteq> span u" by blast
1.651 -      from u a b ft at ct0 have "?P u"
1.652 +        with span_mono[OF T] have x: "x \<in> span (insert b (insert a (T - {b})))" ..
1.653 +        from span_trans[OF bs x] show "x \<in> span (insert a (T - {b}))" .
1.654 +      qed
1.655 +      from less(1)[OF mlt ft' S sp'] obtain U where U:
1.656 +        "card U = card (insert a (T - {b}))"
1.657 +        "finite U" "S \<subseteq> U" "U \<subseteq> S \<union> insert a (T - {b})"
1.658 +        "S \<subseteq> span U" by blast
1.659 +      from U a b ft at ct0 have "?P U"
1.660          by auto
1.661        then show ?thesis by blast
1.662      qed
1.663 -  }
1.664 -  ultimately show ?ths by blast
1.665 +  qed
1.666  qed
1.667
1.668  text \<open>This implies corresponding size bounds.\<close>
1.669
1.670  lemma independent_span_bound:
1.671 -  assumes f: "finite t"
1.672 -    and i: "independent s"
1.673 -    and sp: "s \<subseteq> span t"
1.674 -  shows "finite s \<and> card s \<le> card t"
1.675 +  assumes f: "finite T"
1.676 +    and i: "independent S"
1.677 +    and sp: "S \<subseteq> span T"
1.678 +  shows "finite S \<and> card S \<le> card T"
1.679    by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
1.680
1.681 -lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
1.682 -proof -
1.683 -  have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
1.684 -    by auto
1.685 -  show ?thesis unfolding eq
1.686 -    apply (rule finite_imageI)
1.687 -    apply (rule finite)
1.688 -    done
1.689 -qed
1.690 +lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
1.691 +  using finite finite_image_set by blast
1.692
1.693
1.694  subsection%unimportant \<open>More interesting properties of the norm.\<close>
1.695 @@ -1358,10 +1276,6 @@
1.696    using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
1.697    by (force simp add: power2_eq_square)
1.698
1.699 -
1.700 -lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
1.701 -  by simp (* TODO: delete *)
1.702 -
1.703  lemma norm_triangle_sub:
1.704    fixes x y :: "'a::real_normed_vector"
1.705    shows "norm x \<le> norm y + norm (x - y)"
1.706 @@ -1456,10 +1370,8 @@
1.707  lemma sum_group:
1.708    assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
1.709    shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
1.710 -  apply (subst sum_image_gen[OF fS, of g f])
1.711 -  apply (rule sum.mono_neutral_right[OF fT fST])
1.712 -  apply (auto intro: sum.neutral)
1.713 -  done
1.714 +  unfolding sum_image_gen[OF fS, of g f]
1.715 +  by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
1.716
1.717  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
1.718  proof
1.719 @@ -1691,12 +1603,7 @@
1.720    assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
1.721      and "\<forall>n \<ge> m. e n \<le> e m"
1.722    shows "\<forall>n \<ge> m. d n < e m"
1.723 -  using assms
1.724 -  apply auto
1.725 -  apply (erule_tac x="n" in allE)
1.726 -  apply (erule_tac x="n" in allE)
1.727 -  apply auto
1.728 -  done
1.729 +  using assms by force
1.730
1.731  lemma infinite_enumerate:
1.732    assumes fS: "infinite S"
1.733 @@ -1808,10 +1715,7 @@
1.734  next
1.735    case False
1.736    with y x1 show ?thesis
1.737 -    apply auto
1.738 -    apply (rule exI[where x=1])
1.739 -    apply auto
1.740 -    done
1.741 +    by (metis less_le_trans not_less power_one_right)
1.742  qed
1.743
1.744  lemma forall_pos_mono:
1.745 @@ -1910,11 +1814,7 @@
1.746      proof -
1.747        from Basis_le_norm[OF that, of x]
1.748        show "norm (?g i) \<le> norm (f i) * norm x"
1.749 -        unfolding norm_scaleR
1.750 -        apply (subst mult.commute)
1.751 -        apply (rule mult_mono)
1.752 -        apply (auto simp add: field_simps)
1.753 -        done
1.754 +        unfolding norm_scaleR  by (metis mult.commute mult_left_mono norm_ge_zero)
1.755      qed
1.756      from sum_norm_le[of _ ?g, OF th]
1.757      show "norm (f x) \<le> ?B * norm x"
1.758 @@ -1999,23 +1899,17 @@
1.759    fix x :: 'm
1.760    fix y :: 'n
1.761    have "norm (h x y) = norm (h (sum (\<lambda>i. (x \<bullet> i) *\<^sub>R i) Basis) (sum (\<lambda>i. (y \<bullet> i) *\<^sub>R i) Basis))"
1.762 -    apply (subst euclidean_representation[where 'a='m])
1.763 -    apply (subst euclidean_representation[where 'a='n])
1.764 -    apply rule
1.765 -    done
1.766 +    by (simp add: euclidean_representation)
1.767    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.768      unfolding bilinear_sum[OF bh finite_Basis finite_Basis] ..
1.769    finally have th: "norm (h x y) = \<dots>" .
1.770 -  show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
1.771 -    apply (auto simp add: sum_distrib_right th sum.cartesian_product)
1.772 -    apply (rule sum_norm_le)
1.773 -    apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
1.774 -      field_simps simp del: scaleR_scaleR)
1.775 -    apply (rule mult_mono)
1.776 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
1.777 -    apply (rule mult_mono)
1.778 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
1.779 -    done
1.780 +  have "\<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk>
1.781 +           \<Longrightarrow> \<bar>x \<bullet> i\<bar> * (\<bar>y \<bullet> j\<bar> * norm (h i j)) \<le> norm x * (norm y * norm (h i j))"
1.782 +    by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono)
1.783 +  then show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
1.784 +    unfolding sum_distrib_right th sum.cartesian_product
1.785 +    by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
1.786 +      field_simps simp del: scaleR_scaleR intro!: sum_norm_le)
1.787  qed
1.788
1.789  lemma bilinear_conv_bounded_bilinear:
1.790 @@ -2033,15 +1927,9 @@
1.791      show "h x (y + z) = h x y + h x z"
1.792        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
1.793    next
1.794 -    fix r x y
1.795 -    show "h (scaleR r x) y = scaleR r (h x y)"
1.796 +    show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y
1.797        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
1.798 -      by simp
1.799 -  next
1.800 -    fix r x y
1.801 -    show "h x (scaleR r y) = scaleR r (h x y)"
1.802 -      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
1.803 -      by simp
1.804 +      by simp_all
1.805    next
1.806      have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
1.807        using \<open>bilinear h\<close> by (rule bilinear_bounded)
1.808 @@ -2119,11 +2007,16 @@
1.809  definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
1.810
1.811  lemma basis_exists:
1.812 -  "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
1.813 -  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.814 -  using maximal_independent_subset[of V] independent_bound
1.815 -  by auto
1.816 -
1.817 +  obtains B :: "'a::euclidean_space set"
1.818 +  where "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
1.819 +proof -
1.820 +  obtain B :: "'a set" where "B \<subseteq> V" "independent B" "V \<subseteq> span B"
1.821 +    by (meson maximal_independent_subset[of V])
1.822 +  then show ?thesis
1.823 +    using that some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
1.824 +    unfolding dim_def by blast
1.825 +qed
1.826 +
1.827  corollary dim_le_card:
1.828    fixes s :: "'a::euclidean_space set"
1.829    shows "finite s \<Longrightarrow> dim s \<le> card s"
1.830 @@ -2138,10 +2031,8 @@
1.831    shows "card B \<le> dim V"
1.832  proof -
1.833    from basis_exists[of V] \<open>B \<subseteq> V\<close>
1.834 -  obtain B' where "independent B'"
1.835 -    and "B \<subseteq> span B'"
1.836 -    and "card B' = dim V"
1.837 -    by blast
1.838 +  obtain B' where "independent B'" "B \<subseteq> span B'" "card B' = dim V"
1.839 +    by force
1.840    with independent_span_bound[OF _ \<open>independent B\<close> \<open>B \<subseteq> span B'\<close>] independent_bound[of B']
1.841    show ?thesis by auto
1.842  qed
1.843 @@ -2562,10 +2453,10 @@
1.844  proof -
1.845    from basis_exists[of S] independent_bound
1.846    obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B"
1.847 -    by blast
1.848 +    by metis
1.849    from basis_exists[of T] independent_bound
1.850    obtain C where C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C"
1.851 -    by blast
1.852 +    by metis
1.853    from B(4) C(4) card_le_inj[of B C] d
1.854    obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
1.855      by auto
```