tidying up and using real induction methods
authorpaulson <lp15@cam.ac.uk>
Wed May 02 23:32:47 2018 +0100 (12 months ago)
changeset 6806936209dfb981e
parent 68065 d2daeef3ce47
child 68070 8dc792d440b9
tidying up and using real induction methods
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Starlike.thy
     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