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.76    by (simp add: dependent_def)
    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.123 -          unfolding add.assoc
   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.169 +          by (simp add: scaleR_add_right span_induct_alt_help.span_induct_alt_help_S)
   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.241 +    apply (metis add_diff_cancel_left')
   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.305 -        by (simp add: th00 add.commute cong del: if_weak_cong)
   1.306 +        by (rule sum.cong) (use xS in auto)
   1.307 +      then show ?thesis using fS xS th0
   1.308 +        by (simp add: add.commute cong del: if_weak_cong)
   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.382 -  apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
   1.383 -  done
   1.384 +  unfolding subspace_def
   1.385 +  by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
   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