# HG changeset patch # User paulson # Date 1525300367 -3600 # Node ID 36209dfb981efedc434fe7b8207345491b939e91 # Parent d2daeef3ce4722d315a0574f7b0a5844d1e53d4c tidying up and using real induction methods diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed May 02 23:32:47 2018 +0100 @@ -1100,19 +1100,21 @@ { assume h:?rhs let ?P = "\(y::real ^'n). \(x::real^'m). sum (\i. (x$i) *s column i A) ?U = y" { fix y - have "?P y" - proof (rule span_induct_alt[of ?P "columns A", folded scalar_mult_eq_scaleR]) - show "\x::real ^ 'm. sum (\i. (x$i) *s column i A) ?U = 0" - by (rule exI[where x=0], simp) + have "y \ span (columns A)" + using h by auto + then have "?P y" + proof (induction rule: span_induct_alt) + case base + then show ?case + by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right) next - fix c y1 y2 - assume y1: "y1 \ columns A" and y2: "?P y2" - from y1 obtain i where i: "i \ ?U" "y1 = column i A" + case (step c y1 y2) + then obtain i where i: "i \ ?U" "y1 = column i A" unfolding columns_def by blast - from y2 obtain x:: "real ^'m" where - x: "sum (\i. (x$i) *s column i A) ?U = y2" by blast + obtain x:: "real ^'m" where x: "sum (\i. (x$i) *s column i A) ?U = y2" + using step by blast let ?x = "(\ j. if j = i then c + (x$i) else (x$j))::real^'m" - show "?P (c*s y1 + y2)" + show ?case 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) fix j have th: "\xa \ ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j) @@ -1129,9 +1131,6 @@ finally show "sum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" . qed - next - show "y \ span (columns A)" - unfolding h by blast qed } then have ?lhs unfolding lhseq .. @@ -1756,7 +1755,7 @@ proof - obtain B where "independent B" "span(rows A) \ span B" and B: "B \ span(rows A)""card B = dim (span(rows A))" - using basis_exists [of "span(rows A)"] by blast + using basis_exists [of "span(rows A)"] by metis with span_subspace have eq: "span B = span(rows A)" by auto then have inj: "inj_on (( *v) A) (span B)" diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed May 02 23:32:47 2018 +0100 @@ -1621,7 +1621,7 @@ proof - obtain d where "d \ 0" and d: "\y. f y = 0 \ d \ y = 0" using orthogonal_to_subspace_exists [OF less] orthogonal_def - by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1)) + by (metis (mono_tags, lifting) mem_Collect_eq span_superset) then obtain k where "k > 0" and k: "\e. e > 0 \ \y. y \ S - {0} \ norm y < e \ k * norm y \ \d \ y\" using lb by blast diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed May 02 23:32:47 2018 +0100 @@ -3249,10 +3249,10 @@ using assms by auto then have h0: "independent ((\x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto - then obtain B where B: + obtain B where B: "(\x. -a+x) ` (S - {a}) \ B \ B \ (\x. -a+x) ` V \ independent B \ (\x. -a+x) ` V \ span B" - using maximal_independent_subset_extend[of "(\x. -a+x) ` (S-{a})" "(\x. -a + x) ` V"] assms - by blast + using assms + by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\x. -a + x) ` V"]) define T where "T = (\x. a+x) ` insert 0 B" then have "T = insert a ((\x. a+x) ` B)" by auto @@ -3357,10 +3357,7 @@ then have "card ((\x. -a + x) ` (B - {a})) > 0" using fin by auto moreover have h1: "card ((\x. -a + x) ` (B-{a})) = card (B-{a})" - apply (rule card_image) - using translate_inj_on - apply (auto simp del: uminus_add_conv_diff) - done + by (rule card_image) (use translate_inj_on in blast) ultimately have "card (B-{a}) > 0" by auto then have *: "finite (B - {a})" using card_gt_0_iff[of "(B - {a})"] by auto @@ -3434,7 +3431,7 @@ shows "S = T" proof - obtain B where B: "B \ S" "independent B \ S \ span B" "card B = dim S" - using basis_exists[of S] by auto + using basis_exists[of S] by metis then have "span B \ S" using span_mono[of B S] span_eq[of S] assms by metis then have "span B = S" @@ -3450,7 +3447,7 @@ corollary dim_eq_span: fixes S :: "'a::euclidean_space set" shows "\S \ T; dim T \ dim S\ \ span S = span T" -by (simp add: span_mono subspace_dim_equal subspace_span) +by (simp add: span_mono subspace_dim_equal) lemma dim_eq_full: fixes S :: "'a :: euclidean_space set" @@ -6818,8 +6815,7 @@ define k where "k = Max (f ` c)" have "convex_on (convex hull c) f" apply(rule convex_on_subset[OF assms(2)]) - apply(rule subset_trans[OF _ e(1)]) - apply(rule c1) + apply(rule subset_trans[OF c1 e(1)]) done then have k: "\y\convex hull c. f y \ k" apply (rule_tac convex_on_convex_hull_bound, assumption) diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Determinants.thy Wed May 02 23:32:47 2018 +0100 @@ -421,48 +421,39 @@ fixes A :: "real^'n^'n" assumes x: "x \ span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" -proof - - let ?U = "UNIV :: 'n set" - let ?S = "{row j A |j. j \ i}" - let ?d = "\x. det (\ k. if k = i then x else row k A)" - let ?P = "\x. ?d (row i A + x) = det A" + using x +proof (induction rule: span_induct_alt) + case base { fix k have "(if k = i then row i A + 0 else row k A) = row k A" by simp } - then have P0: "?P 0" + then show ?case apply - apply (rule cong[of det, OF refl]) apply (vector row_def) done - moreover - { - fix c z y - assume zS: "z \ ?S" and Py: "?P y" - from zS obtain j where j: "z = row j A" "i \ j" - by blast - let ?w = "row i A + y" - have th0: "row i A + (c*s z + y) = ?w + c*s z" - by vector - have thz: "?d z = 0" - apply (rule det_identical_rows[OF j(2)]) - using j - apply (vector row_def) - done - have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" - unfolding th0 .. - then have "?P (c*s z + y)" - unfolding thz Py det_row_mul[of i] det_row_add[of i] - by simp - } - ultimately show ?thesis - apply - - apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR]) - apply blast - apply (rule x) +next + case (step c z y) + then obtain j where j: "z = row j A" "i \ j" + by blast + let ?w = "row i A + y" + have th0: "row i A + (c*s z + y) = ?w + c*s z" + by vector + let ?d = "\x. det (\ k. if k = i then x else row k A)" + have thz: "?d z = 0" + apply (rule det_identical_rows[OF j(2)]) + using j + apply (vector row_def) done -qed + have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" + unfolding th0 .. + then have "?d (row i A + (c*s z + y)) = det A" + unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp + then show ?case + unfolding scalar_mult_eq_scaleR . +qed lemma matrix_id [simp]: "det (matrix id) = 1" by (simp add: matrix_id_mat_1) diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Wed May 02 23:32:47 2018 +0100 @@ -963,7 +963,7 @@ then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \ x = 0} f g" by (force simp: homeomorphic_def) have "h ` (+) (- a) ` S \ T" - using heq span_clauses(1) span_linear_image by blast + using heq span_superset span_linear_image by blast then have "g ` h ` (+) (- a) ` S \ g ` {x. i \ x = 0}" using Tsub by (simp add: image_mono) also have "... \ sphere 0 1 - {i}" @@ -987,8 +987,8 @@ apply (simp add: homeomorphic_def homeomorphism_def) apply (rule_tac x="g \ h" in exI) apply (rule_tac x="k \ f" in exI) - apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp) - apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1)) + apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp) + apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset) done finally have Shom: "S homeomorphic (g \ h) ` (+) (- a) ` S" . show ?thesis diff -r d2daeef3ce47 -r 36209dfb981e src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed May 02 12:48:08 2018 +0100 +++ b/src/HOL/Analysis/Linear_Algebra.thy Wed May 02 23:32:47 2018 +0100 @@ -155,11 +155,7 @@ qed lemma linear_0: "linear f \ f 0 = 0" - unfolding linear_iff - apply clarsimp - apply (erule allE[where x="0::'a"]) - apply simp - done + unfolding linear_iff by (metis real_vector.scale_zero_left) lemma linear_cmul: "linear f \ f (c *\<^sub>R x) = c *\<^sub>R f x" by (rule linear.scaleR) @@ -284,18 +280,28 @@ lemma (in real_vector) subspace_span [iff]: "subspace (span S)" unfolding span_def - apply (rule hull_in) - apply (simp only: subspace_def Inter_iff Int_iff subset_eq) - apply auto - done - -lemma (in real_vector) span_clauses: - "a \ S \ a \ span S" - "0 \ span S" - "x\ span S \ y \ span S \ x + y \ span S" - "x \ span S \ c *\<^sub>R x \ span S" + by (rule hull_in) (auto simp: subspace_def) + +lemma (in real_vector) span_superset: "a \ S \ a \ span S" + and span_0 [simp]: "0 \ span S" + and span_add: "x \ span S \ y \ span S \ x + y \ span S" + and span_mul: "x \ span S \ c *\<^sub>R x \ span S" by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+ +lemmas (in real_vector) span_clauses = span_superset span_0 span_add span_mul + +lemma span_neg: "x \ span S \ - x \ span S" + by (metis subspace_neg subspace_span) + +lemma span_diff: "x \ span S \ y \ span S \ x - y \ span S" + by (metis subspace_span subspace_diff) + +lemma (in real_vector) span_sum: "(\x. x \ A \ f x \ span S) \ sum f A \ span S" + by (rule subspace_sum [OF subspace_span]) + +lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" + by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span) + lemma span_unique: "S \ T \ subspace T \ (\T'. S \ T' \ subspace T' \ T \ T') \ span S = T" unfolding span_def by (rule hull_unique) @@ -306,7 +312,7 @@ lemma span_UNIV [simp]: "span UNIV = UNIV" by (intro span_unique) auto -lemma (in real_vector) span_induct: +lemma (in real_vector) span_induct [consumes 1, case_names base step, induct set: span]: assumes x: "x \ span S" and P: "subspace (Collect P)" and SP: "\x. x \ S \ P x" @@ -320,10 +326,8 @@ qed lemma span_empty[simp]: "span {} = {0}" - apply (simp add: span_def) - apply (rule hull_unique) - apply (auto simp add: subspace_def) - done + unfolding span_def + by (rule hull_unique) (auto simp add: subspace_def) lemma (in real_vector) independent_empty [iff]: "independent {}" by (simp add: dependent_def) @@ -345,87 +349,53 @@ "x \ S \ z \ span_induct_alt_help S \ (c *\<^sub>R x + z) \ span_induct_alt_help S" -lemma span_induct_alt': - assumes h0: "h 0" +lemma span_induct_alt [consumes 1, case_names base step, induct set: span]: + assumes x: "x \ span S" + and h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" - shows "\x \ span S. h x" + shows "h x" proof - - { - fix x :: 'a - assume x: "x \ span_induct_alt_help S" - have "h x" - apply (rule span_induct_alt_help.induct[OF x]) - apply (rule h0) - apply (rule hS) - apply assumption - apply assumption - done - } - note th0 = this - { - fix x - assume x: "x \ span S" - have "x \ span_induct_alt_help S" - proof (rule span_induct[where x=x and S=S]) - show "x \ span S" by (rule x) - next - fix x - assume xS: "x \ S" - from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] - show "x \ span_induct_alt_help S" - by simp - next - have "0 \ span_induct_alt_help S" by (rule span_induct_alt_help_0) - moreover - { - fix x y - assume h: "x \ span_induct_alt_help S" "y \ span_induct_alt_help S" - from h have "(x + y) \ span_induct_alt_help S" - apply (induct rule: span_induct_alt_help.induct) - apply simp - unfolding add.assoc - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done - } - moreover - { - fix c x - assume xt: "x \ span_induct_alt_help S" - then have "(c *\<^sub>R x) \ span_induct_alt_help S" - apply (induct rule: span_induct_alt_help.induct) - apply (simp add: span_induct_alt_help_0) - apply (simp add: scaleR_right_distrib) - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done } - ultimately show "subspace {a. a \ span_induct_alt_help S}" - unfolding subspace_def Ball_def by blast - qed - } - with th0 show ?thesis by blast + have th0: "h x" if "x \ span_induct_alt_help S" for x + by (metis span_induct_alt_help.induct[OF that] h0 hS) + have "x \ span_induct_alt_help S" if "x \ span S" for x + using that + proof (induction x rule: span_induct) + case base + have 0: "0 \ span_induct_alt_help S" + by (rule span_induct_alt_help_0) + moreover + have "(x + y) \ span_induct_alt_help S" + if "x \ span_induct_alt_help S" "y \ span_induct_alt_help S" for x y + using that + by induct (auto simp: add.assoc span_induct_alt_help.span_induct_alt_help_S) + moreover + have "(c *\<^sub>R x) \ span_induct_alt_help S" if "x \ span_induct_alt_help S" for c x + using that + proof (induction rule: span_induct_alt_help.induct) + case span_induct_alt_help_0 + then show ?case + by (simp add: 0) + next + case (span_induct_alt_help_S x z c) + then show ?case + by (simp add: scaleR_add_right span_induct_alt_help.span_induct_alt_help_S) + qed + ultimately show ?case + unfolding subspace_def Ball_def by blast + next + case (step x) + then show ?case + using span_induct_alt_help_S[OF step span_induct_alt_help_0, of 1] + by simp + qed + with th0 x show ?thesis by blast qed -lemma span_induct_alt: - assumes h0: "h 0" - and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" - and x: "x \ span S" - shows "h x" - using span_induct_alt'[of h S] h0 hS x by blast - text \Individual closure properties.\ lemma span_span: "span (span A) = span A" unfolding span_def hull_hull .. -lemma (in real_vector) span_superset: "x \ S \ x \ span S" - by (metis span_clauses(1)) - -lemma (in real_vector) span_0 [simp]: "0 \ span S" - by (metis subspace_span subspace_0) - lemma span_inc: "S \ span S" by (metis subset_eq span_superset) @@ -437,26 +407,7 @@ assumes "0 \ A" shows "dependent A" unfolding dependent_def - using assms span_0 - by blast - -lemma (in real_vector) span_add: "x \ span S \ y \ span S \ x + y \ span S" - by (metis subspace_add subspace_span) - -lemma (in real_vector) span_mul: "x \ span S \ c *\<^sub>R x \ span S" - by (metis subspace_span subspace_mul) - -lemma span_neg: "x \ span S \ - x \ span S" - by (metis subspace_neg subspace_span) - -lemma span_diff: "x \ span S \ y \ span S \ x - y \ span S" - by (metis subspace_span subspace_diff) - -lemma (in real_vector) span_sum: "(\x. x \ A \ f x \ span S) \ sum f A \ span S" - by (rule subspace_sum [OF subspace_span]) - -lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" - by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span) + using assms span_0 by blast text \The key breakdown property.\ @@ -539,11 +490,9 @@ proof - have "span ({a} \ S) = {x. \k. (x - k *\<^sub>R a) \ span S}" unfolding span_Un span_singleton - apply safe - apply (rule_tac x=k in exI, simp) - apply (erule rev_image_eqI [OF SigmaI [OF rangeI]]) - apply auto - done + apply (auto simp: image_iff) + apply (metis add_diff_cancel_left') + by force then show ?thesis by simp qed @@ -612,30 +561,30 @@ lemma span_explicit: "span P = {y. \S u. finite S \ S \ P \ sum (\v. u v *\<^sub>R v) S = y}" - (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") + (is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") proof - - { - fix x - assume "?h x" - then obtain S u where "finite S" and "S \ P" and "sum (\v. u v *\<^sub>R v) S = x" + have "x \ span P" if "?h x" for x + proof - + from that + obtain S u where "finite S" and "S \ P" and "sum (\v. u v *\<^sub>R v) S = x" by blast - then have "x \ span P" + then show ?thesis by (auto intro: span_sum span_mul span_superset) - } + qed moreover - have "\x \ span P. ?h x" - proof (rule span_induct_alt') - show "?h 0" - by (rule exI[where x="{}"], simp) + have "?h x" if "x \ span P" for x + using that + proof (induction rule: span_induct_alt) + case base + then show ?case + by force next - fix c x y - assume x: "x \ P" - assume hy: "?h y" - from hy obtain S u where fS: "finite S" and SP: "S\P" + case (step c x y) + then obtain S u where fS: "finite S" and SP: "S\P" and u: "sum (\v. u v *\<^sub>R v) S = y" by blast let ?S = "insert x S" let ?u = "\y. if y = x then (if x \ S then u y + c else c) else u y" - from fS SP x have th0: "finite (insert x S)" "insert x S \ P" + from fS SP step have th0: "finite (insert x S)" "insert x S \ P" by blast+ have "?Q ?S ?u (c*\<^sub>R x + y)" proof cases @@ -650,16 +599,13 @@ then show ?thesis using th0 by blast next assume xS: "x \ S" - have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" + have "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" unfolding u[symmetric] - apply (rule sum.cong) - using xS - apply auto - done - show ?thesis using fS xS th0 - by (simp add: th00 add.commute cong del: if_weak_cong) + by (rule sum.cong) (use xS in auto) + then show ?thesis using fS xS th0 + by (simp add: add.commute cong del: if_weak_cong) qed - then show "?h (c*\<^sub>R x + y)" + then show ?case by fast qed ultimately show ?thesis by blast @@ -679,16 +625,13 @@ let ?v = a from aP SP have aS: "a \ S" by blast - from fS SP aP have th0: "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" + have "(\v\S. (if v = a then - 1 else u v) *\<^sub>R v) = (\v\S. u v *\<^sub>R v)" + using aS by (auto intro: sum.cong) + then have s0: "sum (\v. ?u v *\<^sub>R v) ?S = 0" + using fS aS by (simp add: ua) + moreover from fS SP aP have "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" by auto - have s0: "sum (\v. ?u v *\<^sub>R v) ?S = 0" - using fS aS - apply simp - apply (subst (2) ua[symmetric]) - apply (rule sum.cong) - apply auto - done - with th0 have ?rhs by fast + ultimately have ?rhs by fast } moreover { @@ -817,13 +760,7 @@ assume i: ?lhs then show ?rhs using False - apply simp - apply (rule conjI) - apply (rule independent_mono) - apply assumption - apply blast - apply (simp add: dependent_def) - done + using dependent_def independent_mono by fastforce next assume i: ?rhs show ?lhs @@ -868,7 +805,7 @@ lemma maximal_independent_subset_extend: assumes "S \ V" "independent S" - shows "\B. S \ B \ B \ V \ independent B \ V \ span B" + obtains B where "S \ B" "B \ V" "independent B" "V \ span B" proof - let ?C = "{B. S \ B \ independent B \ B \ V}" have "\M\?C. \X\?C. M \ X \ X = M" @@ -909,12 +846,12 @@ with \v \ span B\ have False by (auto intro: span_superset) } ultimately show ?thesis - by (auto intro!: exI[of _ B]) + by (meson that) qed lemma maximal_independent_subset: - "\B. B \ V \ independent B \ V \ span B" + obtains B where "B \ V" "independent B" "V \ span B" by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty) lemma span_finite: @@ -1043,9 +980,8 @@ lemma subspace_kernel: assumes lf: "linear f" shows "subspace {x. f x = 0}" - apply (simp add: subspace_def) - apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) - done + unfolding subspace_def + by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) lemma linear_eq_0_span: assumes x: "x \ span B" and lf: "linear f" and f0: "\x. x\B \ f x = 0" @@ -1075,7 +1011,8 @@ from span_mono[OF BA] span_mono[OF AsB] have sAB: "span A = span B" unfolding span_span by blast - { + show "A \ B" + proof fix x assume x: "x \ A" from iA have th0: "x \ span (A - {x})" @@ -1085,7 +1022,8 @@ have "A - {x} \ A" by blast then have th1: "span (A - {x}) \ span A" by (metis span_mono) - { + show "x \ B" + proof (rule ccontr) assume xB: "x \ B" from xB BA have "B \ A - {x}" by blast @@ -1093,12 +1031,10 @@ by (metis span_mono) with th1 th0 sAB have "x \ span A" by blast - with x have False + with x show False by (metis span_superset) - } - then have "x \ B" by blast - } - then show "A \ B" by blast + qed + qed qed text \Relation between bases and injectivity/surjectivity of map.\ @@ -1121,21 +1057,20 @@ and lf: "linear f" and fi: "inj_on f (span S)" shows "independent (f ` S)" -proof - - { - fix a - assume a: "a \ S" "f a \ span (f ` S - {f a})" - have eq: "f ` S - {f a} = f ` (S - {a})" - using fi \a\S\ by (auto simp add: inj_on_def span_superset) - from a have "f a \ f ` span (S - {a})" - unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast - then have "a \ span (S - {a})" - by (rule inj_on_image_mem_iff_alt[OF fi, rotated]) - (insert span_mono[of "S - {a}" S], auto intro: span_superset \a\S\) - with a(1) iS have False - by (simp add: dependent_def) - } - then show ?thesis + unfolding dependent_def +proof clarsimp + fix a + assume a: "a \ S" "f a \ span (f ` S - {f a})" + have eq: "f ` S - {f a} = f ` (S - {a})" + using fi \a\S\ by (auto simp add: inj_on_def span_superset) + from a have "f a \ f ` span (S - {a})" + unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast + then have "a \ span (S - {a})" + by (rule inj_on_image_mem_iff_alt[OF fi, rotated]) + (insert span_mono[of "S - {a}" S], auto intro: span_superset \a\S\) + with a(1) iS have False + by (simp add: dependent_def) + then show False unfolding dependent_def by blast qed @@ -1150,7 +1085,7 @@ shows "\g. range g \ span S \ linear g \ (\x\span S. g (f x) = x)" proof - obtain B where "independent B" "B \ S" "S \ span B" - using maximal_independent_subset[of S] by auto + using maximal_independent_subset[of S] . then have "span S = span B" unfolding span_eq by (auto simp: span_superset) with linear_independent_extend_subspace[OF independent_inj_on_image, OF \independent B\ lf] fi @@ -1176,14 +1111,14 @@ qed lemma linear_injective_left_inverse: "linear f \ inj f \ \g. linear g \ g \ f = id" - using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff span_UNIV) + using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff) lemma linear_surj_right_inverse: assumes lf: "linear f" and sf: "span T \ f`span S" shows "\g. range g \ span S \ linear g \ (\x\span T. f (g x) = x)" proof - obtain B where "independent B" "B \ T" "T \ span B" - using maximal_independent_subset[of T] by auto + using maximal_independent_subset[of T] . then have "span T = span B" unfolding span_eq by (auto simp: span_superset) @@ -1206,133 +1141,116 @@ lemma linear_surjective_right_inverse: "linear f \ surj f \ \g. linear g \ f \ g = id" using linear_surj_right_inverse[of f UNIV UNIV] - by (auto simp: span_UNIV fun_eq_iff) + by (auto simp: fun_eq_iff) text \The general case of the Exchange Lemma, the key to what follows.\ lemma exchange_lemma: - assumes f:"finite t" - and i: "independent s" - and sp: "s \ span t" - shows "\t'. card t' = card t \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" + assumes f: "finite T" + and i: "independent S" + and sp: "S \ span T" + shows "\t'. card t' = card T \ finite t' \ S \ t' \ t' \ S \ T \ S \ span t'" using f i sp -proof (induct "card (t - s)" arbitrary: s t rule: less_induct) +proof (induct "card (T - S)" arbitrary: S T rule: less_induct) case less - note ft = \finite t\ and s = \independent s\ and sp = \s \ span t\ - let ?P = "\t'. card t' = card t \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" - let ?ths = "\t'. ?P t'" - { - assume "s \ t" - then have ?ths - by (metis ft Un_commute sp sup_ge1) - } - moreover - { - assume st: "t \ s" - from spanning_subset_independent[OF st s sp] st ft span_mono[OF st] - have ?ths - by (metis Un_absorb sp) - } - moreover - { - assume st: "\