author paulson Wed May 02 23:32:47 2018 +0100 (12 months ago) changeset 68069 36209dfb981e parent 68065 d2daeef3ce47 child 68070 8dc792d440b9
tidying up and using real induction methods
 src/HOL/Analysis/Cartesian_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Change_Of_Vars.thy file | annotate | diff | revisions src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Determinants.thy file | annotate | diff | revisions src/HOL/Analysis/Homeomorphism.thy file | annotate | diff | revisions src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | revisions src/HOL/Analysis/Polytope.thy file | annotate | diff | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed May 02 12:48:08 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed May 02 23:32:47 2018 +0100
1.3 @@ -1100,19 +1100,21 @@
1.4    { assume h:?rhs
1.5      let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). sum (\<lambda>i. (x\$i) *s column i A) ?U = y"
1.6      { fix y
1.7 -      have "?P y"
1.8 -      proof (rule span_induct_alt[of ?P "columns A", folded scalar_mult_eq_scaleR])
1.9 -        show "\<exists>x::real ^ 'm. sum (\<lambda>i. (x\$i) *s column i A) ?U = 0"
1.10 -          by (rule exI[where x=0], simp)
1.11 +      have "y \<in> span (columns A)"
1.12 +        using h by auto
1.13 +      then have "?P y"
1.14 +      proof (induction rule: span_induct_alt)
1.15 +        case base
1.16 +        then show ?case
1.17 +          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
1.18        next
1.19 -        fix c y1 y2
1.20 -        assume y1: "y1 \<in> columns A" and y2: "?P y2"
1.21 -        from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
1.22 +        case (step c y1 y2)
1.23 +        then obtain i where i: "i \<in> ?U" "y1 = column i A"
1.24            unfolding columns_def by blast
1.25 -        from y2 obtain x:: "real ^'m" where
1.26 -          x: "sum (\<lambda>i. (x\$i) *s column i A) ?U = y2" by blast
1.27 +        obtain x:: "real ^'m" where x: "sum (\<lambda>i. (x\$i) *s column i A) ?U = y2"
1.28 +          using step by blast
1.29          let ?x = "(\<chi> j. if j = i then c + (x\$i) else (x\$j))::real^'m"
1.30 -        show "?P (c*s y1 + y2)"
1.31 +        show ?case
1.32          proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong)
1.33            fix j
1.34            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j)
1.35 @@ -1129,9 +1131,6 @@
1.36            finally show "sum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
1.37              else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + sum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U" .
1.38          qed
1.39 -      next
1.40 -        show "y \<in> span (columns A)"
1.41 -          unfolding h by blast
1.42        qed
1.43      }
1.44      then have ?lhs unfolding lhseq ..
1.45 @@ -1756,7 +1755,7 @@
1.46    proof -
1.47      obtain B where "independent B" "span(rows A) \<subseteq> span B"
1.48                and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
1.49 -      using basis_exists [of "span(rows A)"] by blast
1.50 +      using basis_exists [of "span(rows A)"] by metis
1.51      with span_subspace have eq: "span B = span(rows A)"
1.52        by auto
1.53      then have inj: "inj_on (( *v) A) (span B)"
```
```     2.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed May 02 12:48:08 2018 +0100
2.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed May 02 23:32:47 2018 +0100
2.3 @@ -1621,7 +1621,7 @@
2.4    proof -
2.5      obtain d where "d \<noteq> 0" and d: "\<And>y. f y = 0 \<Longrightarrow> d \<bullet> y = 0"
2.6        using orthogonal_to_subspace_exists [OF less] orthogonal_def
2.7 -      by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1))
2.8 +      by (metis (mono_tags, lifting) mem_Collect_eq span_superset)
2.9      then obtain k where "k > 0"
2.10        and k: "\<And>e. e > 0 \<Longrightarrow> \<exists>y. y \<in> S - {0} \<and> norm y < e \<and> k * norm y \<le> \<bar>d \<bullet> y\<bar>"
2.11        using lb by blast
```
```     3.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed May 02 12:48:08 2018 +0100
3.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed May 02 23:32:47 2018 +0100
3.3 @@ -3249,10 +3249,10 @@
3.4      using assms by auto
3.5    then have h0: "independent  ((\<lambda>x. -a + x) ` (S-{a}))"
3.6      using affine_dependent_iff_dependent2 assms by auto
3.7 -  then obtain B where B:
3.8 +  obtain B where B:
3.9      "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B"
3.10 -     using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms
3.11 -     by blast
3.12 +    using assms
3.13 +    by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\<lambda>x. -a + x) ` V"])
3.14    define T where "T = (\<lambda>x. a+x) ` insert 0 B"
3.15    then have "T = insert a ((\<lambda>x. a+x) ` B)"
3.16      by auto
3.17 @@ -3357,10 +3357,7 @@
3.18      then have "card ((\<lambda>x. -a + x) ` (B - {a})) > 0"
3.19        using fin by auto
3.20      moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
3.21 -       apply (rule card_image)
3.22 -       using translate_inj_on
3.23 -       apply (auto simp del: uminus_add_conv_diff)
3.24 -       done
3.25 +      by (rule card_image) (use translate_inj_on in blast)
3.26      ultimately have "card (B-{a}) > 0" by auto
3.27      then have *: "finite (B - {a})"
3.28        using card_gt_0_iff[of "(B - {a})"] by auto
3.29 @@ -3434,7 +3431,7 @@
3.30    shows "S = T"
3.31  proof -
3.32    obtain B where B: "B \<le> S" "independent B \<and> S \<subseteq> span B" "card B = dim S"
3.33 -    using basis_exists[of S] by auto
3.34 +    using basis_exists[of S] by metis
3.35    then have "span B \<subseteq> S"
3.36      using span_mono[of B S] span_eq[of S] assms by metis
3.37    then have "span B = S"
3.38 @@ -3450,7 +3447,7 @@
3.39  corollary dim_eq_span:
3.40    fixes S :: "'a::euclidean_space set"
3.41    shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
3.42 -by (simp add: span_mono subspace_dim_equal subspace_span)
3.43 +by (simp add: span_mono subspace_dim_equal)
3.44
3.45  lemma dim_eq_full:
3.46      fixes S :: "'a :: euclidean_space set"
3.47 @@ -6818,8 +6815,7 @@
3.48    define k where "k = Max (f ` c)"
3.49    have "convex_on (convex hull c) f"
3.50      apply(rule convex_on_subset[OF assms(2)])
3.51 -    apply(rule subset_trans[OF _ e(1)])
3.52 -    apply(rule c1)
3.53 +    apply(rule subset_trans[OF c1 e(1)])
3.54      done
3.55    then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
3.56      apply (rule_tac convex_on_convex_hull_bound, assumption)
```
```     4.1 --- a/src/HOL/Analysis/Determinants.thy	Wed May 02 12:48:08 2018 +0100
4.2 +++ b/src/HOL/Analysis/Determinants.thy	Wed May 02 23:32:47 2018 +0100
4.3 @@ -421,48 +421,39 @@
4.4    fixes A :: "real^'n^'n"
4.5    assumes x: "x \<in> span {row j A |j. j \<noteq> i}"
4.6    shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
4.7 -proof -
4.8 -  let ?U = "UNIV :: 'n set"
4.9 -  let ?S = "{row j A |j. j \<noteq> i}"
4.10 -  let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"
4.11 -  let ?P = "\<lambda>x. ?d (row i A + x) = det A"
4.12 +  using x
4.13 +proof (induction rule: span_induct_alt)
4.14 +  case base
4.15    {
4.16      fix k
4.17      have "(if k = i then row i A + 0 else row k A) = row k A"
4.18        by simp
4.19    }
4.20 -  then have P0: "?P 0"
4.21 +  then show ?case
4.22      apply -
4.23      apply (rule cong[of det, OF refl])
4.24      apply (vector row_def)
4.25      done
4.26 -  moreover
4.27 -  {
4.28 -    fix c z y
4.29 -    assume zS: "z \<in> ?S" and Py: "?P y"
4.30 -    from zS obtain j where j: "z = row j A" "i \<noteq> j"
4.31 -      by blast
4.32 -    let ?w = "row i A + y"
4.33 -    have th0: "row i A + (c*s z + y) = ?w + c*s z"
4.34 -      by vector
4.35 -    have thz: "?d z = 0"
4.36 -      apply (rule det_identical_rows[OF j(2)])
4.37 -      using j
4.38 -      apply (vector row_def)
4.39 -      done
4.40 -    have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)"
4.41 -      unfolding th0 ..
4.42 -    then have "?P (c*s z + y)"
4.43 -      unfolding thz Py det_row_mul[of i] det_row_add[of i]
4.44 -      by simp
4.45 -  }
4.46 -  ultimately show ?thesis
4.47 -    apply -
4.48 -    apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR])
4.49 -    apply blast
4.50 -    apply (rule x)
4.51 +next
4.52 +  case (step c z y)
4.53 +  then obtain j where j: "z = row j A" "i \<noteq> j"
4.54 +    by blast
4.55 +  let ?w = "row i A + y"
4.56 +  have th0: "row i A + (c*s z + y) = ?w + c*s z"
4.57 +    by vector
4.58 +  let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"
4.59 +  have thz: "?d z = 0"
4.60 +    apply (rule det_identical_rows[OF j(2)])
4.61 +    using j
4.62 +    apply (vector row_def)
4.63      done
4.64 -qed
4.65 +  have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)"
4.66 +    unfolding th0 ..
4.67 +  then have "?d (row i A + (c*s z + y)) = det A"
4.68 +    unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp
4.69 +  then show ?case
4.70 +    unfolding scalar_mult_eq_scaleR .
4.71 +qed
4.72
4.73  lemma matrix_id [simp]: "det (matrix id) = 1"
4.74    by (simp add: matrix_id_mat_1)
```
```     5.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Wed May 02 12:48:08 2018 +0100
5.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Wed May 02 23:32:47 2018 +0100
5.3 @@ -963,7 +963,7 @@
5.4    then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g"
5.5      by (force simp: homeomorphic_def)
5.6    have "h ` (+) (- a) ` S \<subseteq> T"
5.7 -    using heq span_clauses(1) span_linear_image by blast
5.8 +    using heq span_superset span_linear_image by blast
5.9    then have "g ` h ` (+) (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
5.10      using Tsub by (simp add: image_mono)
5.11    also have "... \<subseteq> sphere 0 1 - {i}"
5.12 @@ -987,8 +987,8 @@
5.13      apply (simp add: homeomorphic_def homeomorphism_def)
5.14      apply (rule_tac x="g \<circ> h" in exI)
5.15      apply (rule_tac x="k \<circ> f" in exI)
5.16 -    apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp)
5.17 -    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1))
5.18 +    apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp)
5.19 +    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset)
5.20      done
5.21    finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
5.22    show ?thesis
```
```     6.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 12:48:08 2018 +0100
6.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 23:32:47 2018 +0100
6.3 @@ -155,11 +155,7 @@
6.4  qed
6.5
6.6  lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
6.7 -  unfolding linear_iff
6.8 -  apply clarsimp
6.9 -  apply (erule allE[where x="0::'a"])
6.10 -  apply simp
6.11 -  done
6.12 +  unfolding linear_iff  by (metis real_vector.scale_zero_left)
6.13
6.14  lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
6.15    by (rule linear.scaleR)
6.16 @@ -284,18 +280,28 @@
6.17
6.18  lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
6.19    unfolding span_def
6.20 -  apply (rule hull_in)
6.21 -  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
6.22 -  apply auto
6.23 -  done
6.24 -
6.25 -lemma (in real_vector) span_clauses:
6.26 -  "a \<in> S \<Longrightarrow> a \<in> span S"
6.27 -  "0 \<in> span S"
6.28 -  "x\<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
6.29 -  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
6.30 +  by (rule hull_in) (auto simp: subspace_def)
6.31 +
6.32 +lemma (in real_vector) span_superset: "a \<in> S \<Longrightarrow> a \<in> span S"
6.33 +        and span_0 [simp]: "0 \<in> span S"
6.34 +        and span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
6.35 +        and span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
6.36    by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+
6.37
6.38 +lemmas (in real_vector) span_clauses = span_superset span_0 span_add span_mul
6.39 +
6.40 +lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
6.41 +  by (metis subspace_neg subspace_span)
6.42 +
6.43 +lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
6.44 +  by (metis subspace_span subspace_diff)
6.45 +
6.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"
6.47 +  by (rule subspace_sum [OF subspace_span])
6.48 +
6.49 +lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
6.50 +  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
6.51 +
6.52  lemma span_unique:
6.53    "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
6.54    unfolding span_def by (rule hull_unique)
6.55 @@ -306,7 +312,7 @@
6.56  lemma span_UNIV [simp]: "span UNIV = UNIV"
6.57    by (intro span_unique) auto
6.58
6.59 -lemma (in real_vector) span_induct:
6.60 +lemma (in real_vector) span_induct [consumes 1, case_names base step, induct set: span]:
6.61    assumes x: "x \<in> span S"
6.62      and P: "subspace (Collect P)"
6.63      and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
6.64 @@ -320,10 +326,8 @@
6.65  qed
6.66
6.67  lemma span_empty[simp]: "span {} = {0}"
6.68 -  apply (simp add: span_def)
6.69 -  apply (rule hull_unique)
6.70 -  apply (auto simp add: subspace_def)
6.71 -  done
6.72 +  unfolding span_def
6.73 +  by (rule hull_unique) (auto simp add: subspace_def)
6.74
6.75  lemma (in real_vector) independent_empty [iff]: "independent {}"
6.76    by (simp add: dependent_def)
6.77 @@ -345,87 +349,53 @@
6.78      "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow>
6.79        (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
6.80
6.81 -lemma span_induct_alt':
6.82 -  assumes h0: "h 0"
6.83 +lemma span_induct_alt [consumes 1, case_names base step, induct set: span]:
6.84 +  assumes x: "x \<in> span S"
6.85 +    and h0: "h 0"
6.86      and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
6.87 -  shows "\<forall>x \<in> span S. h x"
6.88 +  shows "h x"
6.89  proof -
6.90 -  {
6.91 -    fix x :: 'a
6.92 -    assume x: "x \<in> span_induct_alt_help S"
6.93 -    have "h x"
6.94 -      apply (rule span_induct_alt_help.induct[OF x])
6.95 -      apply (rule h0)
6.96 -      apply (rule hS)
6.97 -      apply assumption
6.98 -      apply assumption
6.99 -      done
6.100 -  }
6.101 -  note th0 = this
6.102 -  {
6.103 -    fix x
6.104 -    assume x: "x \<in> span S"
6.105 -    have "x \<in> span_induct_alt_help S"
6.106 -    proof (rule span_induct[where x=x and S=S])
6.107 -      show "x \<in> span S" by (rule x)
6.108 -    next
6.109 -      fix x
6.110 -      assume xS: "x \<in> S"
6.111 -      from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
6.112 -      show "x \<in> span_induct_alt_help S"
6.113 -        by simp
6.114 -    next
6.115 -      have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
6.116 -      moreover
6.117 -      {
6.118 -        fix x y
6.119 -        assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
6.120 -        from h have "(x + y) \<in> span_induct_alt_help S"
6.121 -          apply (induct rule: span_induct_alt_help.induct)
6.122 -          apply simp
6.123 -          unfolding add.assoc
6.124 -          apply (rule span_induct_alt_help_S)
6.125 -          apply assumption
6.126 -          apply simp
6.127 -          done
6.128 -      }
6.129 -      moreover
6.130 -      {
6.131 -        fix c x
6.132 -        assume xt: "x \<in> span_induct_alt_help S"
6.133 -        then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
6.134 -          apply (induct rule: span_induct_alt_help.induct)
6.135 -          apply (simp add: span_induct_alt_help_0)
6.136 -          apply (simp add: scaleR_right_distrib)
6.137 -          apply (rule span_induct_alt_help_S)
6.138 -          apply assumption
6.139 -          apply simp
6.140 -          done }
6.141 -      ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
6.142 -        unfolding subspace_def Ball_def by blast
6.143 -    qed
6.144 -  }
6.145 -  with th0 show ?thesis by blast
6.146 +  have th0: "h x" if "x \<in> span_induct_alt_help S" for x
6.147 +    by (metis span_induct_alt_help.induct[OF that] h0 hS)
6.148 +  have "x \<in> span_induct_alt_help S" if "x \<in> span S" for x
6.149 +    using that
6.150 +  proof (induction x rule: span_induct)
6.151 +    case base
6.152 +    have 0: "0 \<in> span_induct_alt_help S"
6.153 +      by (rule span_induct_alt_help_0)
6.154 +    moreover
6.155 +    have "(x + y) \<in> span_induct_alt_help S"
6.156 +      if "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S" for x y
6.157 +      using that
6.158 +      by induct (auto simp: add.assoc span_induct_alt_help.span_induct_alt_help_S)
6.159 +    moreover
6.160 +    have "(c *\<^sub>R x) \<in> span_induct_alt_help S" if "x \<in> span_induct_alt_help S" for c x
6.161 +      using that
6.162 +      proof (induction rule: span_induct_alt_help.induct)
6.163 +        case span_induct_alt_help_0
6.164 +        then show ?case
6.165 +          by (simp add: 0)
6.166 +      next
6.167 +        case (span_induct_alt_help_S x z c)
6.168 +        then show ?case
6.169 +          by (simp add: scaleR_add_right span_induct_alt_help.span_induct_alt_help_S)
6.170 +      qed
6.171 +    ultimately show ?case
6.172 +      unfolding subspace_def Ball_def by blast
6.173 +  next
6.174 +    case (step x)
6.175 +    then show ?case
6.176 +      using span_induct_alt_help_S[OF step span_induct_alt_help_0, of 1]
6.177 +      by simp
6.178 +  qed
6.179 +  with th0 x show ?thesis by blast
6.180  qed
6.181
6.182 -lemma span_induct_alt:
6.183 -  assumes h0: "h 0"
6.184 -    and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)"
6.185 -    and x: "x \<in> span S"
6.186 -  shows "h x"
6.187 -  using span_induct_alt'[of h S] h0 hS x by blast
6.188 -
6.189  text \<open>Individual closure properties.\<close>
6.190
6.191  lemma span_span: "span (span A) = span A"
6.192    unfolding span_def hull_hull ..
6.193
6.194 -lemma (in real_vector) span_superset: "x \<in> S \<Longrightarrow> x \<in> span S"
6.195 -  by (metis span_clauses(1))
6.196 -
6.197 -lemma (in real_vector) span_0 [simp]: "0 \<in> span S"
6.198 -  by (metis subspace_span subspace_0)
6.199 -
6.200  lemma span_inc: "S \<subseteq> span S"
6.201    by (metis subset_eq span_superset)
6.202
6.203 @@ -437,26 +407,7 @@
6.204    assumes "0 \<in> A"
6.205    shows "dependent A"
6.206    unfolding dependent_def
6.207 -  using assms span_0
6.208 -  by blast
6.209 -
6.210 -lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
6.211 -  by (metis subspace_add subspace_span)
6.212 -
6.213 -lemma (in real_vector) span_mul: "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
6.214 -  by (metis subspace_span subspace_mul)
6.215 -
6.216 -lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
6.217 -  by (metis subspace_neg subspace_span)
6.218 -
6.219 -lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
6.220 -  by (metis subspace_span subspace_diff)
6.221 -
6.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"
6.223 -  by (rule subspace_sum [OF subspace_span])
6.224 -
6.225 -lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
6.226 -  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
6.227 +  using assms span_0 by blast
6.228
6.229  text \<open>The key breakdown property.\<close>
6.230
6.231 @@ -539,11 +490,9 @@
6.232  proof -
6.233    have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
6.234      unfolding span_Un span_singleton
6.235 -    apply safe
6.236 -    apply (rule_tac x=k in exI, simp)
6.237 -    apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
6.238 -    apply auto
6.239 -    done
6.240 +    apply (auto simp: image_iff)
6.241 +    apply (metis add_diff_cancel_left')
6.242 +    by force
6.243    then show ?thesis by simp
6.244  qed
6.245
6.246 @@ -612,30 +561,30 @@
6.247
6.248  lemma span_explicit:
6.249    "span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
6.250 -  (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
6.251 +  (is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
6.252  proof -
6.253 -  {
6.254 -    fix x
6.255 -    assume "?h x"
6.256 -    then obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
6.257 +  have "x \<in> span P" if "?h x" for x
6.258 +  proof -
6.259 +    from that
6.260 +    obtain S u where "finite S" and "S \<subseteq> P" and "sum (\<lambda>v. u v *\<^sub>R v) S = x"
6.261        by blast
6.262 -    then have "x \<in> span P"
6.263 +    then show ?thesis
6.264        by (auto intro: span_sum span_mul span_superset)
6.265 -  }
6.266 +  qed
6.267    moreover
6.268 -  have "\<forall>x \<in> span P. ?h x"
6.269 -  proof (rule span_induct_alt')
6.270 -    show "?h 0"
6.271 -      by (rule exI[where x="{}"], simp)
6.272 +  have "?h x" if "x \<in> span P" for x
6.273 +    using that
6.274 +  proof (induction rule: span_induct_alt)
6.275 +    case base
6.276 +    then show ?case
6.277 +      by force
6.278    next
6.279 -    fix c x y
6.280 -    assume x: "x \<in> P"
6.281 -    assume hy: "?h y"
6.282 -    from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
6.283 +    case (step c x y)
6.284 +    then obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
6.285        and u: "sum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
6.286      let ?S = "insert x S"
6.287      let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y"
6.288 -    from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P"
6.289 +    from fS SP step have th0: "finite (insert x S)" "insert x S \<subseteq> P"
6.290        by blast+
6.291      have "?Q ?S ?u (c*\<^sub>R x + y)"
6.292      proof cases
6.293 @@ -650,16 +599,13 @@
6.294        then show ?thesis using th0 by blast
6.295      next
6.296        assume xS: "x \<notin> S"
6.297 -      have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
6.298 +      have "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y"
6.299          unfolding u[symmetric]
6.300 -        apply (rule sum.cong)
6.301 -        using xS
6.302 -        apply auto
6.303 -        done
6.304 -      show ?thesis using fS xS th0
6.305 -        by (simp add: th00 add.commute cong del: if_weak_cong)
6.306 +        by (rule sum.cong) (use xS in auto)
6.307 +      then show ?thesis using fS xS th0
6.308 +        by (simp add: add.commute cong del: if_weak_cong)
6.309      qed
6.310 -    then show "?h (c*\<^sub>R x + y)"
6.311 +    then show ?case
6.312        by fast
6.313    qed
6.314    ultimately show ?thesis by blast
6.315 @@ -679,16 +625,13 @@
6.316      let ?v = a
6.317      from aP SP have aS: "a \<notin> S"
6.318        by blast
6.319 -    from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
6.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)"
6.321 +      using aS by (auto intro: sum.cong)
6.322 +    then have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
6.323 +      using fS aS by (simp add: ua)
6.324 +    moreover from fS SP aP have "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0"
6.325        by auto
6.326 -    have s0: "sum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0"
6.327 -      using fS aS
6.328 -      apply simp
6.329 -      apply (subst (2) ua[symmetric])
6.330 -      apply (rule sum.cong)
6.331 -      apply auto
6.332 -      done
6.333 -    with th0 have ?rhs by fast
6.334 +    ultimately have ?rhs by fast
6.335    }
6.336    moreover
6.337    {
6.338 @@ -817,13 +760,7 @@
6.339      assume i: ?lhs
6.340      then show ?rhs
6.341        using False
6.342 -      apply simp
6.343 -      apply (rule conjI)
6.344 -      apply (rule independent_mono)
6.345 -      apply assumption
6.346 -      apply blast
6.347 -      apply (simp add: dependent_def)
6.348 -      done
6.349 +      using dependent_def independent_mono by fastforce
6.350    next
6.351      assume i: ?rhs
6.352      show ?lhs
6.353 @@ -868,7 +805,7 @@
6.354
6.355  lemma maximal_independent_subset_extend:
6.356    assumes "S \<subseteq> V" "independent S"
6.357 -  shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
6.358 +  obtains B where "S \<subseteq> B" "B \<subseteq> V" "independent B" "V \<subseteq> span B"
6.359  proof -
6.360    let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}"
6.361    have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M"
6.362 @@ -909,12 +846,12 @@
6.363      with \<open>v \<notin> span B\<close> have False
6.364        by (auto intro: span_superset) }
6.365    ultimately show ?thesis
6.366 -    by (auto intro!: exI[of _ B])
6.367 +    by (meson that)
6.368  qed
6.369
6.370
6.371  lemma maximal_independent_subset:
6.372 -  "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
6.373 +  obtains B where "B \<subseteq> V" "independent B" "V \<subseteq> span B"
6.374    by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
6.375
6.376  lemma span_finite:
6.377 @@ -1043,9 +980,8 @@
6.378  lemma subspace_kernel:
6.379    assumes lf: "linear f"
6.380    shows "subspace {x. f x = 0}"
6.381 -  apply (simp add: subspace_def)
6.382 -  apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
6.383 -  done
6.384 +  unfolding subspace_def
6.385 +  by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
6.386
6.387  lemma linear_eq_0_span:
6.388    assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
6.389 @@ -1075,7 +1011,8 @@
6.390    from span_mono[OF BA] span_mono[OF AsB]
6.391    have sAB: "span A = span B" unfolding span_span by blast
6.392
6.393 -  {
6.394 +  show "A \<subseteq> B"
6.395 +  proof
6.396      fix x
6.397      assume x: "x \<in> A"
6.398      from iA have th0: "x \<notin> span (A - {x})"
6.399 @@ -1085,7 +1022,8 @@
6.400      have "A - {x} \<subseteq> A" by blast
6.401      then have th1: "span (A - {x}) \<subseteq> span A"
6.402        by (metis span_mono)
6.403 -    {
6.404 +    show "x \<in> B"
6.405 +    proof (rule ccontr)
6.406        assume xB: "x \<notin> B"
6.407        from xB BA have "B \<subseteq> A - {x}"
6.408          by blast
6.409 @@ -1093,12 +1031,10 @@
6.410          by (metis span_mono)
6.411        with th1 th0 sAB have "x \<notin> span A"
6.412          by blast
6.413 -      with x have False
6.414 +      with x show False
6.415          by (metis span_superset)
6.416 -    }
6.417 -    then have "x \<in> B" by blast
6.418 -  }
6.419 -  then show "A \<subseteq> B" by blast
6.420 +    qed
6.421 +  qed
6.422  qed
6.423
6.424  text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
6.425 @@ -1121,21 +1057,20 @@
6.426      and lf: "linear f"
6.427      and fi: "inj_on f (span S)"
6.428    shows "independent (f ` S)"
6.429 -proof -
6.430 -  {
6.431 -    fix a
6.432 -    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
6.433 -    have eq: "f ` S - {f a} = f ` (S - {a})"
6.434 -      using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
6.435 -    from a have "f a \<in> f ` span (S - {a})"
6.436 -      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
6.437 -    then have "a \<in> span (S - {a})"
6.438 -      by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
6.439 -         (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
6.440 -    with a(1) iS have False
6.441 -      by (simp add: dependent_def)
6.442 -  }
6.443 -  then show ?thesis
6.444 +  unfolding dependent_def
6.445 +proof clarsimp
6.446 +  fix a
6.447 +  assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
6.448 +  have eq: "f ` S - {f a} = f ` (S - {a})"
6.449 +    using fi \<open>a\<in>S\<close> by (auto simp add: inj_on_def span_superset)
6.450 +  from a have "f a \<in> f ` span (S - {a})"
6.451 +    unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
6.452 +  then have "a \<in> span (S - {a})"
6.453 +    by (rule inj_on_image_mem_iff_alt[OF fi, rotated])
6.454 +      (insert span_mono[of "S - {a}" S], auto intro: span_superset \<open>a\<in>S\<close>)
6.455 +  with a(1) iS have False
6.456 +    by (simp add: dependent_def)
6.457 +  then show False
6.458      unfolding dependent_def by blast
6.459  qed
6.460
6.461 @@ -1150,7 +1085,7 @@
6.462    shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span S. g (f x) = x)"
6.463  proof -
6.464    obtain B where "independent B" "B \<subseteq> S" "S \<subseteq> span B"
6.465 -    using maximal_independent_subset[of S] by auto
6.466 +    using maximal_independent_subset[of S] .
6.467    then have "span S = span B"
6.468      unfolding span_eq by (auto simp: span_superset)
6.469    with linear_independent_extend_subspace[OF independent_inj_on_image, OF \<open>independent B\<close> lf] fi
6.470 @@ -1176,14 +1111,14 @@
6.471  qed
6.472
6.473  lemma linear_injective_left_inverse: "linear f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear g \<and> g \<circ> f = id"
6.474 -  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV)
6.475 +  using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff)
6.476
6.477  lemma linear_surj_right_inverse:
6.478    assumes lf: "linear f" and sf: "span T \<subseteq> f`span S"
6.479    shows "\<exists>g. range g \<subseteq> span S \<and> linear g \<and> (\<forall>x\<in>span T. f (g x) = x)"
6.480  proof -
6.481    obtain B where "independent B" "B \<subseteq> T" "T \<subseteq> span B"
6.482 -    using maximal_independent_subset[of T] by auto
6.483 +    using maximal_independent_subset[of T] .
6.484    then have "span T = span B"
6.485      unfolding span_eq by (auto simp: span_superset)
6.486
6.487 @@ -1206,133 +1141,116 @@
6.488
6.489  lemma linear_surjective_right_inverse: "linear f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear g \<and> f \<circ> g = id"
6.490    using linear_surj_right_inverse[of f UNIV UNIV]
6.491 -  by (auto simp: span_UNIV fun_eq_iff)
6.492 +  by (auto simp: fun_eq_iff)
6.493
6.494  text \<open>The general case of the Exchange Lemma, the key to what follows.\<close>
6.495
6.496  lemma exchange_lemma:
6.497 -  assumes f:"finite t"
6.498 -    and i: "independent s"
6.499 -    and sp: "s \<subseteq> span t"
6.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'"
6.501 +  assumes f: "finite T"
6.502 +    and i: "independent S"
6.503 +    and sp: "S \<subseteq> span T"
6.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'"
6.505    using f i sp
6.506 -proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
6.507 +proof (induct "card (T - S)" arbitrary: S T rule: less_induct)
6.508    case less
6.509 -  note ft = \<open>finite t\<close> and s = \<open>independent s\<close> and sp = \<open>s \<subseteq> span t\<close>
6.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'"
6.511 -  let ?ths = "\<exists>t'. ?P t'"
6.512 -  {
6.513 -    assume "s \<subseteq> t"
6.514 -    then have ?ths
6.515 -      by (metis ft Un_commute sp sup_ge1)
6.516 -  }
6.517 -  moreover
6.518 -  {
6.519 -    assume st: "t \<subseteq> s"
6.520 -    from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
6.521 -    have ?ths
6.522 -      by (metis Un_absorb sp)
6.523 -  }
6.524 -  moreover
6.525 -  {
6.526 -    assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
6.527 -    from st(2) obtain b where b: "b \<in> t" "b \<notin> s"
6.528 +  note ft = \<open>finite T\<close> and S = \<open>independent S\<close> and sp = \<open>S \<subseteq> span T\<close>
6.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'"
6.530 +  show ?case
6.531 +  proof (cases "S \<subseteq> T \<or> T \<subseteq> S")
6.532 +    case True
6.533 +    then show ?thesis
6.534 +    proof
6.535 +      assume "S \<subseteq> T" then show ?thesis
6.536 +        by (metis ft Un_commute sp sup_ge1)
6.537 +    next
6.538 +      assume "T \<subseteq> S" then show ?thesis
6.539 +        by (metis Un_absorb sp spanning_subset_independent[OF _ S sp] ft)
6.540 +    qed
6.541 +  next
6.542 +    case False
6.543 +    then have st: "\<not> S \<subseteq> T" "\<not> T \<subseteq> S"
6.544 +      by auto
6.545 +    from st(2) obtain b where b: "b \<in> T" "b \<notin> S"
6.546        by blast
6.547 -    from b have "t - {b} - s \<subset> t - s"
6.548 +    from b have "T - {b} - S \<subset> T - S"
6.549        by blast
6.550 -    then have cardlt: "card (t - {b} - s) < card (t - s)"
6.551 +    then have cardlt: "card (T - {b} - S) < card (T - S)"
6.552        using ft by (auto intro: psubset_card_mono)
6.553 -    from b ft have ct0: "card t \<noteq> 0"
6.554 +    from b ft have ct0: "card T \<noteq> 0"
6.555        by auto
6.556 -    have ?ths
6.557 -    proof cases
6.558 -      assume stb: "s \<subseteq> span (t - {b})"
6.559 -      from ft have ftb: "finite (t - {b})"
6.560 +    show ?thesis
6.561 +    proof (cases "S \<subseteq> span (T - {b})")
6.562 +      case True
6.563 +      from ft have ftb: "finite (T - {b})"
6.564          by auto
6.565 -      from less(1)[OF cardlt ftb s stb]
6.566 -      obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
6.567 -        and fu: "finite u" by blast
6.568 -      let ?w = "insert b u"
6.569 -      have th0: "s \<subseteq> insert b u"
6.570 -        using u by blast
6.571 -      from u(3) b have "u \<subseteq> s \<union> t"
6.572 -        by blast
6.573 -      then have th1: "insert b u \<subseteq> s \<union> t"
6.574 -        using u b by blast
6.575 -      have bu: "b \<notin> u"
6.576 -        using b u by blast
6.577 -      from u(1) ft b have "card u = (card t - 1)"
6.578 +      from less(1)[OF cardlt ftb S True]
6.579 +      obtain U where U: "card U = card (T - {b})" "S \<subseteq> U" "U \<subseteq> S \<union> (T - {b})" "S \<subseteq> span U"
6.580 +        and fu: "finite U" by blast
6.581 +      let ?w = "insert b U"
6.582 +      have th0: "S \<subseteq> insert b U"
6.583 +        using U by blast
6.584 +      have th1: "insert b U \<subseteq> S \<union> T"
6.585 +        using U b by blast
6.586 +      have bu: "b \<notin> U"
6.587 +        using b U by blast
6.588 +      from U(1) ft b have "card U = (card T - 1)"
6.589          by auto
6.590 -      then have th2: "card (insert b u) = card t"
6.591 +      then have th2: "card (insert b U) = card T"
6.592          using card_insert_disjoint[OF fu bu] ct0 by auto
6.593 -      from u(4) have "s \<subseteq> span u" .
6.594 -      also have "\<dots> \<subseteq> span (insert b u)"
6.595 +      from U(4) have "S \<subseteq> span U" .
6.596 +      also have "\<dots> \<subseteq> span (insert b U)"
6.597          by (rule span_mono) blast
6.598 -      finally have th3: "s \<subseteq> span (insert b u)" .
6.599 +      finally have th3: "S \<subseteq> span (insert b U)" .
6.600        from th0 th1 th2 th3 fu have th: "?P ?w"
6.601          by blast
6.602        from th show ?thesis by blast
6.603      next
6.604 -      assume stb: "\<not> s \<subseteq> span (t - {b})"
6.605 -      from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
6.606 +      case False
6.607 +      then obtain a where a: "a \<in> S" "a \<notin> span (T - {b})"
6.608          by blast
6.609        have ab: "a \<noteq> b"
6.610          using a b by blast
6.611 -      have at: "a \<notin> t"
6.612 -        using a ab span_superset[of a "t- {b}"] by auto
6.613 -      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
6.614 +      have at: "a \<notin> T"
6.615 +        using a ab span_superset[of a "T- {b}"] by auto
6.616 +      have mlt: "card ((insert a (T - {b})) - S) < card (T - S)"
6.617          using cardlt ft a b by auto
6.618 -      have ft': "finite (insert a (t - {b}))"
6.619 +      have ft': "finite (insert a (T - {b}))"
6.620          using ft by auto
6.621 -      {
6.622 +      have sp': "S \<subseteq> span (insert a (T - {b}))"
6.623 +      proof
6.624          fix x
6.625 -        assume xs: "x \<in> s"
6.626 -        have t: "t \<subseteq> insert b (insert a (t - {b}))"
6.627 +        assume xs: "x \<in> S"
6.628 +        have T: "T \<subseteq> insert b (insert a (T - {b}))"
6.629            using b by auto
6.630 -        from b(1) have "b \<in> span t"
6.631 -          by (simp add: span_superset)
6.632 -        have bs: "b \<in> span (insert a (t - {b}))"
6.633 -          apply (rule in_span_delete)
6.634 -          using a sp unfolding subset_eq
6.635 -          apply auto
6.636 -          done
6.637 -        from xs sp have "x \<in> span t"
6.638 +        have bs: "b \<in> span (insert a (T - {b}))"
6.639 +          by (rule in_span_delete) (use a sp in auto)
6.640 +        from xs sp have "x \<in> span T"
6.641            by blast
6.642 -        with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" ..
6.643 -        from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .
6.644 -      }
6.645 -      then have sp': "s \<subseteq> span (insert a (t - {b}))"
6.646 -        by blast
6.647 -      from less(1)[OF mlt ft' s sp'] obtain u where u:
6.648 -        "card u = card (insert a (t - {b}))"
6.649 -        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
6.650 -        "s \<subseteq> span u" by blast
6.651 -      from u a b ft at ct0 have "?P u"
6.652 +        with span_mono[OF T] have x: "x \<in> span (insert b (insert a (T - {b})))" ..
6.653 +        from span_trans[OF bs x] show "x \<in> span (insert a (T - {b}))" .
6.654 +      qed
6.655 +      from less(1)[OF mlt ft' S sp'] obtain U where U:
6.656 +        "card U = card (insert a (T - {b}))"
6.657 +        "finite U" "S \<subseteq> U" "U \<subseteq> S \<union> insert a (T - {b})"
6.658 +        "S \<subseteq> span U" by blast
6.659 +      from U a b ft at ct0 have "?P U"
6.660          by auto
6.661        then show ?thesis by blast
6.662      qed
6.663 -  }
6.664 -  ultimately show ?ths by blast
6.665 +  qed
6.666  qed
6.667
6.668  text \<open>This implies corresponding size bounds.\<close>
6.669
6.670  lemma independent_span_bound:
6.671 -  assumes f: "finite t"
6.672 -    and i: "independent s"
6.673 -    and sp: "s \<subseteq> span t"
6.674 -  shows "finite s \<and> card s \<le> card t"
6.675 +  assumes f: "finite T"
6.676 +    and i: "independent S"
6.677 +    and sp: "S \<subseteq> span T"
6.678 +  shows "finite S \<and> card S \<le> card T"
6.679    by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
6.680
6.681 -lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
6.682 -proof -
6.683 -  have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
6.684 -    by auto
6.685 -  show ?thesis unfolding eq
6.686 -    apply (rule finite_imageI)
6.687 -    apply (rule finite)
6.688 -    done
6.689 -qed
6.690 +lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
6.691 +  using finite finite_image_set by blast
6.692
6.693
6.694  subsection%unimportant \<open>More interesting properties of the norm.\<close>
6.695 @@ -1358,10 +1276,6 @@
6.696    using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
6.697    by (force simp add: power2_eq_square)
6.698
6.699 -
6.700 -lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
6.701 -  by simp (* TODO: delete *)
6.702 -
6.703  lemma norm_triangle_sub:
6.704    fixes x y :: "'a::real_normed_vector"
6.705    shows "norm x \<le> norm y + norm (x - y)"
6.706 @@ -1456,10 +1370,8 @@
6.707  lemma sum_group:
6.708    assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
6.709    shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
6.710 -  apply (subst sum_image_gen[OF fS, of g f])
6.711 -  apply (rule sum.mono_neutral_right[OF fT fST])
6.712 -  apply (auto intro: sum.neutral)
6.713 -  done
6.714 +  unfolding sum_image_gen[OF fS, of g f]
6.715 +  by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
6.716
6.717  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
6.718  proof
6.719 @@ -1691,12 +1603,7 @@
6.720    assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
6.721      and "\<forall>n \<ge> m. e n \<le> e m"
6.722    shows "\<forall>n \<ge> m. d n < e m"
6.723 -  using assms
6.724 -  apply auto
6.725 -  apply (erule_tac x="n" in allE)
6.726 -  apply (erule_tac x="n" in allE)
6.727 -  apply auto
6.728 -  done
6.729 +  using assms by force
6.730
6.731  lemma infinite_enumerate:
6.732    assumes fS: "infinite S"
6.733 @@ -1808,10 +1715,7 @@
6.734  next
6.735    case False
6.736    with y x1 show ?thesis
6.737 -    apply auto
6.738 -    apply (rule exI[where x=1])
6.739 -    apply auto
6.740 -    done
6.741 +    by (metis less_le_trans not_less power_one_right)
6.742  qed
6.743
6.744  lemma forall_pos_mono:
6.745 @@ -1910,11 +1814,7 @@
6.746      proof -
6.747        from Basis_le_norm[OF that, of x]
6.748        show "norm (?g i) \<le> norm (f i) * norm x"
6.749 -        unfolding norm_scaleR
6.750 -        apply (subst mult.commute)
6.751 -        apply (rule mult_mono)
6.752 -        apply (auto simp add: field_simps)
6.753 -        done
6.754 +        unfolding norm_scaleR  by (metis mult.commute mult_left_mono norm_ge_zero)
6.755      qed
6.756      from sum_norm_le[of _ ?g, OF th]
6.757      show "norm (f x) \<le> ?B * norm x"
6.758 @@ -1999,23 +1899,17 @@
6.759    fix x :: 'm
6.760    fix y :: 'n
6.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))"
6.762 -    apply (subst euclidean_representation[where 'a='m])
6.763 -    apply (subst euclidean_representation[where 'a='n])
6.764 -    apply rule
6.765 -    done
6.766 +    by (simp add: euclidean_representation)
6.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))"
6.768      unfolding bilinear_sum[OF bh finite_Basis finite_Basis] ..
6.769    finally have th: "norm (h x y) = \<dots>" .
6.770 -  show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
6.771 -    apply (auto simp add: sum_distrib_right th sum.cartesian_product)
6.772 -    apply (rule sum_norm_le)
6.773 -    apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
6.774 -      field_simps simp del: scaleR_scaleR)
6.775 -    apply (rule mult_mono)
6.776 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
6.777 -    apply (rule mult_mono)
6.778 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
6.779 -    done
6.780 +  have "\<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk>
6.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))"
6.782 +    by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono)
6.783 +  then show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
6.784 +    unfolding sum_distrib_right th sum.cartesian_product
6.785 +    by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
6.786 +      field_simps simp del: scaleR_scaleR intro!: sum_norm_le)
6.787  qed
6.788
6.789  lemma bilinear_conv_bounded_bilinear:
6.790 @@ -2033,15 +1927,9 @@
6.791      show "h x (y + z) = h x y + h x z"
6.792        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
6.793    next
6.794 -    fix r x y
6.795 -    show "h (scaleR r x) y = scaleR r (h x y)"
6.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
6.797        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
6.798 -      by simp
6.799 -  next
6.800 -    fix r x y
6.801 -    show "h x (scaleR r y) = scaleR r (h x y)"
6.802 -      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
6.803 -      by simp
6.804 +      by simp_all
6.805    next
6.806      have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
6.807        using \<open>bilinear h\<close> by (rule bilinear_bounded)
6.808 @@ -2119,11 +2007,16 @@
6.809  definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = n)"
6.810
6.811  lemma basis_exists:
6.812 -  "\<exists>B. (B :: ('a::euclidean_space) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
6.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)"]
6.814 -  using maximal_independent_subset[of V] independent_bound
6.815 -  by auto
6.816 -
6.817 +  obtains B :: "'a::euclidean_space set"
6.818 +  where "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
6.819 +proof -
6.820 +  obtain B :: "'a set" where "B \<subseteq> V" "independent B" "V \<subseteq> span B"
6.821 +    by (meson maximal_independent_subset[of V])
6.822 +  then show ?thesis
6.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)"]
6.824 +    unfolding dim_def by blast
6.825 +qed
6.826 +
6.827  corollary dim_le_card:
6.828    fixes s :: "'a::euclidean_space set"
6.829    shows "finite s \<Longrightarrow> dim s \<le> card s"
6.830 @@ -2138,10 +2031,8 @@
6.831    shows "card B \<le> dim V"
6.832  proof -
6.833    from basis_exists[of V] \<open>B \<subseteq> V\<close>
6.834 -  obtain B' where "independent B'"
6.835 -    and "B \<subseteq> span B'"
6.836 -    and "card B' = dim V"
6.837 -    by blast
6.838 +  obtain B' where "independent B'" "B \<subseteq> span B'" "card B' = dim V"
6.839 +    by force
6.840    with independent_span_bound[OF _ \<open>independent B\<close> \<open>B \<subseteq> span B'\<close>] independent_bound[of B']
6.841    show ?thesis by auto
6.842  qed
6.843 @@ -2562,10 +2453,10 @@
6.844  proof -
6.845    from basis_exists[of S] independent_bound
6.846    obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B"
6.847 -    by blast
6.848 +    by metis
6.849    from basis_exists[of T] independent_bound
6.850    obtain C where C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C"
6.851 -    by blast
6.852 +    by metis
6.853    from B(4) C(4) card_le_inj[of B C] d
6.854    obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close>
6.855      by auto
```
```     7.1 --- a/src/HOL/Analysis/Polytope.thy	Wed May 02 12:48:08 2018 +0100
7.2 +++ b/src/HOL/Analysis/Polytope.thy	Wed May 02 23:32:47 2018 +0100
7.3 @@ -1189,7 +1189,7 @@
7.4      qed
7.5      then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
7.6        by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
7.7 -           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_clauses(1))
7.8 +           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_superset)
7.9      then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
7.10        by (rule less.IH) (auto simp: co less.prems)
7.11      then show ?thesis
```
```     8.1 --- a/src/HOL/Analysis/Starlike.thy	Wed May 02 12:48:08 2018 +0100
8.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed May 02 23:32:47 2018 +0100
8.3 @@ -1622,7 +1622,7 @@
8.4  next
8.5    case False
8.6    obtain B where B: "independent B \<and> B \<le> S \<and> S \<le> span B \<and> card B = dim S"
8.7 -    using basis_exists[of S] by auto
8.8 +    using basis_exists[of S] by metis
8.9    then have "B \<noteq> {}"
8.10      using B assms \<open>S \<noteq> {0}\<close> span_empty by auto
8.11    have "insert 0 B \<le> span B"
8.12 @@ -5713,7 +5713,7 @@
8.13  apply (simp add: special_hyperplane_span)
8.14  apply (rule Linear_Algebra.dim_unique [OF subset_refl])
8.15  apply (auto simp: Diff_subset independent_substdbasis)
8.16 -apply (metis member_remove remove_def span_clauses(1))
8.17 +apply (metis member_remove remove_def span_superset)
8.18  done
8.19
8.20  proposition dim_hyperplane:
8.21 @@ -6564,11 +6564,9 @@
8.22
8.23  lemma basis_subspace_exists:
8.24    fixes S :: "'a::euclidean_space set"
8.25 -  shows
8.26 -   "subspace S
8.27 -        \<Longrightarrow> \<exists>b. finite b \<and> b \<subseteq> S \<and>
8.28 -                independent b \<and> span b = S \<and> card b = dim S"
8.29 -by (metis span_subspace basis_exists independent_imp_finite)
8.30 +  assumes "subspace S"
8.31 +  obtains B where "finite B" "B \<subseteq> S" "independent B" "span B = S" "card B = dim S"
8.32 +by (metis assms span_subspace basis_exists independent_imp_finite)
8.33
8.34  lemma affine_hyperplane_sums_eq_UNIV_0:
8.35    fixes S :: "'a :: euclidean_space set"
8.36 @@ -6658,7 +6656,7 @@
8.37    obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
8.38               and indB: "independent B"
8.39               and cardB: "card B = dim (S \<inter> T)"
8.40 -    using basis_exists by blast
8.41 +    using basis_exists by metis
8.42    then obtain C D where "B \<subseteq> C" "C \<subseteq> S" "independent C" "S \<subseteq> span C"
8.43                      and "B \<subseteq> D" "D \<subseteq> T" "independent D" "T \<subseteq> span D"
8.44      using maximal_independent_subset_extend
8.45 @@ -6975,14 +6973,12 @@
8.46      using spanU by simp
8.47    also have "... = span (insert a (S \<union> T))"
8.48      apply (rule eq_span_insert_eq)
8.49 -    apply (simp add: a'_def span_neg span_sum span_clauses(1) span_mul)
8.50 +    apply (simp add: a'_def span_neg span_sum span_superset span_mul)
8.51      done
8.52    also have "... = span (S \<union> insert a T)"
8.53      by simp
8.54    finally show ?case
8.55 -    apply (rule_tac x="insert a' U" in exI)
8.56 -    using orthU apply auto
8.57 -    done
8.58 +    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
8.59  qed
8.60
8.61
8.62 @@ -6992,7 +6988,7 @@
8.63    obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
8.64  proof%unimportant -
8.65    obtain B where "finite B" "span B = span T"
8.66 -    using basis_subspace_exists [of "span T"] subspace_span by auto
8.67 +    using basis_subspace_exists [of "span T"] subspace_span by metis
8.68    with orthogonal_extension_aux [of B S]
8.69    obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
8.70      using assms pairwise_orthogonal_imp_finite by auto
8.71 @@ -7060,7 +7056,7 @@
8.72               and "independent B" "card B = dim S" "span B = S"
8.73      by (blast intro: orthogonal_basis_subspace [OF assms])
8.74    have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
8.75 -    using \<open>span B = S\<close> span_clauses(1) span_mul by fastforce
8.76 +    using \<open>span B = S\<close> span_superset span_mul by fastforce
8.77    have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
8.78      using orth by (force simp: pairwise_def orthogonal_clauses)
8.79    have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
8.80 @@ -7145,7 +7141,7 @@
8.81    have "dim {x} < DIM('a)"
8.82      using assms by auto
8.83    then show thesis
8.84 -    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
8.85 +    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_superset that)
8.86  qed
8.87
8.88  proposition%important orthogonal_subspace_decomp_exists:
8.89 @@ -7407,7 +7403,7 @@
8.90                have "e/2 / norm a \<noteq> 0"
8.91                  using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
8.92                then show ?thesis
8.93 -                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_clauses(1))
8.94 +                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_superset)
8.95              qed
8.96              ultimately show "?y \<in> S - U" by blast
8.97            qed
8.98 @@ -8260,7 +8256,7 @@
8.99      have "v = ?u + (v - ?u)"
8.100        by simp
8.101      moreover have "?u \<in> U"
8.102 -      by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_clauses(1) span_mul)
8.103 +      by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_superset span_mul)
8.104      moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
8.105      proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
8.106        fix y
```