# HG changeset patch # User huffman # Date 1272566464 25200 # Node ID fb69c8cd27bdf4ea1dc786961254c5f06498b45f # Parent eacded3b05f71fa9160e013789940d68c3c351eb define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general diff -r eacded3b05f7 -r fb69c8cd27bd src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 29 09:29:47 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 29 11:41:04 2010 -0700 @@ -1090,7 +1090,7 @@ show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule) fix x' y z::"real^'m" and c::real note lin = assms(2)[rule_format,OF `x\s`,THEN derivative_linear] - show "g' x (c *s x') = c *s g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially]) + show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially]) apply(rule lem3[rule_format]) unfolding smult_conv_scaleR unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format] apply(rule Lim_cmul) by(rule lem3[rule_format]) diff -r eacded3b05f7 -r fb69c8cd27bd src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Thu Apr 29 09:29:47 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Thu Apr 29 11:41:04 2010 -0700 @@ -421,7 +421,7 @@ qed lemma det_row_span: - fixes A :: "'a:: linordered_idom^'n^'n" + 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- @@ -450,7 +450,7 @@ ultimately show ?thesis apply - - apply (rule span_induct_alt[of ?P ?S, OF P0]) + apply (rule span_induct_alt[of ?P ?S, OF P0, folded smult_conv_scaleR]) apply blast apply (rule x) done @@ -462,7 +462,7 @@ (* ------------------------------------------------------------------------- *) lemma det_dependent_rows: - fixes A:: "'a::linordered_idom^'n^'n" + fixes A:: "real^'n^'n" assumes d: "dependent (rows A)" shows "det A = 0" proof- @@ -483,12 +483,12 @@ from det_row_span[OF th0] have "det A = det (\ k. if k = i then 0 *s 1 else row k A)" unfolding right_minus vector_smult_lzero .. - with det_row_mul[of i "0::'a" "\i. 1"] + with det_row_mul[of i "0::real" "\i. 1"] have "det A = 0" by simp} ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::linordered_idom^'n^'n))" shows "det A = 0" +lemma det_dependent_columns: assumes d: "dependent(columns (A::real^'n^'n))" shows "det A = 0" by (metis d det_dependent_rows rows_transpose det_transpose) (* ------------------------------------------------------------------------- *) @@ -744,7 +744,7 @@ apply (rule span_setsum) apply simp apply (rule ballI) - apply (rule span_mul)+ + apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ apply (rule span_superset) apply auto done @@ -761,9 +761,9 @@ (* ------------------------------------------------------------------------- *) lemma cramer_lemma_transpose: - fixes A:: "'a::linordered_idom^'n^'n" and x :: "'a ^'n" + fixes A:: "real^'n^'n" and x :: "real^'n" shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) - else row i A)::'a^'n^'n) = x$k * det A" + else row i A)::real^'n^'n) = x$k * det A" (is "?lhs = ?rhs") proof- let ?U = "UNIV :: 'n set" @@ -780,7 +780,7 @@ apply (rule det_row_span) apply (rule span_setsum[OF fUk]) apply (rule ballI) - apply (rule span_mul) + apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ apply (rule span_superset) apply auto done @@ -797,8 +797,8 @@ qed lemma cramer_lemma: - fixes A :: "'a::linordered_idom ^'n^'n" - shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" + fixes A :: "real^'n^'n" + shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A" proof- let ?U = "UNIV :: 'n set" have stupid: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" diff -r eacded3b05f7 -r fb69c8cd27bd src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Apr 29 09:29:47 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Apr 29 11:41:04 2010 -0700 @@ -753,6 +753,13 @@ "setsum (\i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) +lemma smult_conv_scaleR: "c *s x = scaleR c x" + unfolding vector_scalar_mult_def vector_scaleR_def by simp + +lemma basis_expansion': + "setsum (\i. (x$i) *\<^sub>R basis i) UNIV = x" + by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR]) + lemma basis_expansion_unique: "setsum (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n) \ (\i. f i = x$i)" by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong) @@ -824,64 +831,63 @@ subsection{* Linear functions. *} -definition "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *s x) = c *s f x)" - -lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *s x) = c *s f x" +definition + linear :: "('a::real_vector \ 'b::real_vector) \ bool" where + "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" + +lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "linear f" using assms unfolding linear_def by auto -lemma linear_compose_cmul: "linear f ==> linear (\x. (c::'a::comm_semiring) *s f x)" - by (vector linear_def Cart_eq field_simps) - -lemma linear_compose_neg: "linear (f :: 'a ^'n \ 'a::comm_ring ^'m) ==> linear (\x. -(f(x)))" by (vector linear_def Cart_eq) - -lemma linear_compose_add: "linear (f :: 'a ^'n \ 'a::semiring_1 ^'m) \ linear g ==> linear (\x. f(x) + g(x))" - by (vector linear_def Cart_eq field_simps) - -lemma linear_compose_sub: "linear (f :: 'a ^'n \ 'a::ring_1 ^'m) \ linear g ==> linear (\x. f x - g x)" - by (vector linear_def Cart_eq field_simps) +lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_neg: "linear f ==> linear (\x. -(f(x)))" + by (simp add: linear_def) + +lemma linear_compose_add: "linear f \ linear g ==> linear (\x. f(x) + g(x))" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_sub: "linear f \ linear g ==> linear (\x. f x - g x)" + by (simp add: linear_def algebra_simps) lemma linear_compose: "linear f \ linear g ==> linear (g o f)" by (simp add: linear_def) lemma linear_id: "linear id" by (simp add: linear_def id_def) -lemma linear_zero: "linear (\x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def) +lemma linear_zero: "linear (\x. 0)" by (simp add: linear_def) lemma linear_compose_setsum: - assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n \ 'a ^'m)" - shows "linear(\x. setsum (\a. f a x :: 'a::semiring_1 ^'m) S)" + assumes fS: "finite S" and lS: "\a \ S. linear (f a)" + shows "linear(\x. setsum (\a. f a x) S)" using lS apply (induct rule: finite_induct[OF fS]) by (auto simp add: linear_zero intro: linear_compose_add) lemma linear_vmul_component: - fixes f:: "'a::semiring_1^'m \ 'a^'n" assumes lf: "linear f" - shows "linear (\x. f x $ k *s v)" + shows "linear (\x. f x $ k *\<^sub>R v)" using lf - apply (auto simp add: linear_def ) - by (vector field_simps)+ - -lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)" + by (auto simp add: linear_def algebra_simps) + +lemma linear_0: "linear f ==> f 0 = 0" unfolding linear_def apply clarsimp apply (erule allE[where x="0::'a"]) apply simp done -lemma linear_cmul: "linear f ==> f(c*s x) = c *s f x" by (simp add: linear_def) - -lemma linear_neg: "linear (f :: 'a::ring_1 ^'n \ _) ==> f (-x) = - f x" - unfolding vector_sneg_minus1 - using linear_cmul[of f] by auto +lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) + +lemma linear_neg: "linear f ==> f (-x) = - f x" + using linear_cmul [where c="-1"] by simp lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) -lemma linear_sub: "linear (f::'a::ring_1 ^'n \ _) ==> f(x - y) = f x - f y" +lemma linear_sub: "linear f ==> f(x - y) = f x - f y" by (simp add: diff_def linear_add linear_neg) lemma linear_setsum: - fixes f:: "'a::semiring_1^'n \ _" assumes lf: "linear f" and fS: "finite S" shows "f (setsum g S) = setsum (f o g) S" proof (induct rule: finite_induct[OF fS]) @@ -896,14 +902,13 @@ qed lemma linear_setsum_mul: - fixes f:: "'a ^'n \ 'a::semiring_1^'m" assumes lf: "linear f" and fS: "finite S" - shows "f (setsum (\i. c i *s v i) S) = setsum (\i. c i *s f (v i)) S" - using linear_setsum[OF lf fS, of "\i. c i *s v i" , unfolded o_def] + shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" + using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lf] by simp lemma linear_injective_0: - assumes lf: "linear (f:: 'a::ring_1 ^ 'n \ _)" + assumes lf: "linear f" shows "inj f \ (\x. f x = 0 \ x = 0)" proof- have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) @@ -923,22 +928,22 @@ let ?B = "setsum (\i. norm(f(basis i))) ?S" have fS: "finite ?S" by simp {fix x:: "real ^ 'm" - let ?g = "(\i. (x$i) *s (basis i) :: real ^ 'm)" - have "norm (f x) = norm (f (setsum (\i. (x$i) *s (basis i)) ?S))" - by (simp only: basis_expansion) - also have "\ = norm (setsum (\i. (x$i) *s f (basis i))?S)" + let ?g = "(\i. (x$i) *\<^sub>R (basis i) :: real ^ 'm)" + have "norm (f x) = norm (f (setsum (\i. (x$i) *\<^sub>R (basis i)) ?S))" + by (simp add: basis_expansion') + also have "\ = norm (setsum (\i. (x$i) *\<^sub>R f (basis i))?S)" using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto - finally have th0: "norm (f x) = norm (setsum (\i. (x$i) *s f (basis i))?S)" . + finally have th0: "norm (f x) = norm (setsum (\i. (x$i) *\<^sub>R f (basis i))?S)" . {fix i assume i: "i \ ?S" from component_le_norm[of x i] - have "norm ((x$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" - unfolding norm_mul + have "norm ((x$i) *\<^sub>R f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" + unfolding norm_scaleR apply (simp only: mult_commute) apply (rule mult_mono) by (auto simp add: field_simps) } - then have th: "\i\ ?S. norm ((x$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" by metis - from setsum_norm_le[OF fS, of "\i. (x$i) *s (f (basis i))", OF th] + then have th: "\i\ ?S. norm ((x$i) *\<^sub>R f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" by metis + from setsum_norm_le[OF fS, of "\i. (x$i) *\<^sub>R (f (basis i))", OF th] have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} then show ?thesis by blast qed @@ -969,9 +974,6 @@ then show ?thesis using Kp by blast qed -lemma smult_conv_scaleR: "c *s x = scaleR c x" - unfolding vector_scalar_mult_def vector_scaleR_def by simp - lemma linear_conv_bounded_linear: fixes f :: "real ^ _ \ real ^ _" shows "linear f \ bounded_linear f" @@ -1000,7 +1002,7 @@ qed lemma bounded_linearI': fixes f::"real^'n \ real^'m" - assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *s x) = c *s f x" + assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] by(rule linearI[OF assms]) @@ -1013,39 +1015,38 @@ lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" by (simp add: bilinear_def linear_def) -lemma bilinear_lmul: "bilinear h ==> h (c *s x) y = c *s (h x y)" +lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" by (simp add: bilinear_def linear_def) -lemma bilinear_rmul: "bilinear h ==> h x (c *s y) = c *s (h x y)" +lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" by (simp add: bilinear_def linear_def) -lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n)) y = -(h x y)" - by (simp only: vector_sneg_minus1 bilinear_lmul) - -lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n)) = - h x y" - by (simp only: vector_sneg_minus1 bilinear_rmul) +lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)" + by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) + +lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y" + by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul) lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" using add_imp_eq[of x y 0] by auto lemma bilinear_lzero: - fixes h :: "'a::ring^'n \ _" assumes bh: "bilinear h" shows "h 0 x = 0" + assumes bh: "bilinear h" shows "h 0 x = 0" using bilinear_ladd[OF bh, of 0 0 x] by (simp add: eq_add_iff field_simps) lemma bilinear_rzero: - fixes h :: "'a::ring^_ \ _" assumes bh: "bilinear h" shows "h x 0 = 0" + assumes bh: "bilinear h" shows "h x 0 = 0" using bilinear_radd[OF bh, of x 0 0 ] by (simp add: eq_add_iff field_simps) -lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ _)) z = h x z - h y z" +lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" by (simp add: diff_def bilinear_ladd bilinear_lneg) -lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ _)) = h z x - h z y" +lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y" by (simp add: diff_def bilinear_radd bilinear_rneg) lemma bilinear_setsum: - fixes h:: "'a ^_ \ 'a::semiring_1^_\ 'a ^ _" assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " proof- @@ -1069,15 +1070,15 @@ let ?B = "setsum (\(i,j). norm (h (basis i) (basis j))) (?M \ ?N)" have fM: "finite ?M" and fN: "finite ?N" by simp_all {fix x:: "real ^ 'm" and y :: "real^'n" - have "norm (h x y) = norm (h (setsum (\i. (x$i) *s basis i) ?M) (setsum (\i. (y$i) *s basis i) ?N))" unfolding basis_expansion .. - also have "\ = norm (setsum (\ (i,j). h ((x$i) *s basis i) ((y$j) *s basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. + have "norm (h x y) = norm (h (setsum (\i. (x$i) *\<^sub>R basis i) ?M) (setsum (\i. (y$i) *\<^sub>R basis i) ?N))" unfolding basis_expansion' .. + also have "\ = norm (setsum (\ (i,j). h ((x$i) *\<^sub>R basis i) ((y$j) *\<^sub>R basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. finally have th: "norm (h x y) = \" . have "norm (h x y) \ ?B * norm x * norm y" apply (simp add: setsum_left_distrib th) apply (rule setsum_norm_le) using fN fM apply simp - apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps) + apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR) apply (rule mult_mono) apply (auto simp add: zero_le_mult_iff component_le_norm) apply (rule mult_mono) @@ -1148,6 +1149,11 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis +text {* TODO: The following lemmas about adjoints should hold for any +Hilbert space (i.e. complete inner product space). +(see http://en.wikipedia.org/wiki/Hermitian_adjoint) +*} + lemma adjoint_works_lemma: fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" @@ -1160,9 +1166,9 @@ {fix y:: "real ^ 'm" let ?w = "(\ i. (f (basis i) \ y)) :: real ^ 'n" {fix x - have "f x \ y = f (setsum (\i. (x$i) *s basis i) ?N) \ y" - by (simp only: basis_expansion) - also have "\ = (setsum (\i. (x$i) *s f (basis i)) ?N) \ y" + have "f x \ y = f (setsum (\i. (x$i) *\<^sub>R basis i) ?N) \ y" + by (simp only: basis_expansion') + also have "\ = (setsum (\i. (x$i) *\<^sub>R f (basis i)) ?N) \ y" unfolding linear_setsum[OF lf fN] by (simp add: linear_cmul[OF lf]) finally have "f x \ y = x \ ?w" @@ -1326,18 +1332,18 @@ by (vector Cart_eq setsum_component) lemma linear_componentwise: - fixes f:: "'a::ring_1 ^'m \ 'a ^ _" + fixes f:: "real ^'m \ real ^ _" assumes lf: "linear f" shows "(f x)$j = setsum (\i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") proof- let ?M = "(UNIV :: 'm set)" let ?N = "(UNIV :: 'n set)" have fM: "finite ?M" by simp - have "?rhs = (setsum (\i.(x$i) *s f (basis i) ) ?M)$j" - unfolding vector_smult_component[symmetric] - unfolding setsum_component[of "(\i.(x$i) *s f (basis i :: 'a^'m))" ?M] + have "?rhs = (setsum (\i.(x$i) *\<^sub>R f (basis i) ) ?M)$j" + unfolding vector_smult_component[symmetric] smult_conv_scaleR + unfolding setsum_component[of "(\i.(x$i) *\<^sub>R f (basis i :: real^'m))" ?M] .. - then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion .. + then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' .. qed text{* Inverse matrices (not necessarily square) *} @@ -1352,23 +1358,23 @@ definition matrix:: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" where "matrix f = (\ i j. (f(basis j))$i)" -lemma matrix_vector_mul_linear: "linear(\x. A *v (x::'a::comm_semiring_1 ^ _))" +lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" by (simp add: linear_def matrix_vector_mult_def Cart_eq field_simps setsum_right_distrib setsum_addf) -lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)" +lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)" apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute) apply clarify apply (rule linear_componentwise[OF lf, symmetric]) done -lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works) - -lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A" +lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works) + +lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: real ^ 'n)) = A" by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) lemma matrix_compose: - assumes lf: "linear (f::'a::comm_ring_1^'n \ 'a^'m)" - and lg: "linear (g::'a::comm_ring_1^'m \ 'a^_)" + assumes lf: "linear (f::real^'n \ real^'m)" + and lg: "linear (g::real^'m \ real^_)" shows "matrix (g o f) = matrix g ** matrix f" using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) @@ -1718,7 +1724,10 @@ subsection{* A bit of linear algebra. *} -definition "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *s x \S )" +definition + subspace :: "'a::real_vector set \ bool" where + "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" + definition "span S = (subspace hull S)" definition "dependent S \ (\a \ S. a \ span(S - {a}))" abbreviation "independent s == ~(dependent s)" @@ -1732,13 +1741,13 @@ lemma subspace_add: "subspace S \ x \ S \ y \ S ==> x + y \ S" by (metis subspace_def) -lemma subspace_mul: "subspace S \ x \ S \ c *s x \ S" +lemma subspace_mul: "subspace S \ x \ S \ c *\<^sub>R x \ S" by (metis subspace_def) -lemma subspace_neg: "subspace S \ (x::'a::ring_1^_) \ S \ - x \ S" - by (metis vector_sneg_minus1 subspace_mul) - -lemma subspace_sub: "subspace S \ (x::'a::ring_1^_) \ S \ y \ S \ x - y \ S" +lemma subspace_neg: "subspace S \ x \ S \ - x \ S" + by (metis scaleR_minus1_left subspace_mul) + +lemma subspace_sub: "subspace S \ x \ S \ y \ S \ x - y \ S" by (metis diff_def subspace_add subspace_neg) lemma subspace_setsum: @@ -1750,19 +1759,19 @@ by (simp add: subspace_def sA, auto simp add: sA subspace_add) lemma subspace_linear_image: - assumes lf: "linear (f::'a::semiring_1^_ \ _)" and sS: "subspace S" + assumes lf: "linear f" and sS: "subspace S" shows "subspace(f ` S)" using lf sS linear_0[OF lf] unfolding linear_def subspace_def apply (auto simp add: image_iff) apply (rule_tac x="x + y" in bexI, auto) - apply (rule_tac x="c*s x" in bexI, auto) + apply (rule_tac x="c *\<^sub>R x" in bexI, auto) done -lemma subspace_linear_preimage: "linear (f::'a::semiring_1^_ \ _) ==> subspace S ==> subspace {x. f x \ S}" +lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \ S}" by (auto simp add: subspace_def linear_def linear_0[of f]) -lemma subspace_trivial: "subspace {0::'a::semiring_1 ^_}" +lemma subspace_trivial: "subspace {0}" by (simp add: subspace_def) lemma subspace_inter: "subspace A \ subspace B ==> subspace (A \ B)" @@ -1798,7 +1807,7 @@ "a \ S ==> a \ span S" "0 \ span S" "x\ span S \ y \ span S ==> x + y \ span S" - "x \ span S \ c *s x \ span S" + "x \ span S \ c *\<^sub>R x \ span S" by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+ @@ -1811,11 +1820,11 @@ show "P x" by (metis mem_def subset_eq) qed -lemma span_empty: "span {} = {(0::'a::semiring_0 ^ _)}" +lemma span_empty: "span {} = {0}" apply (simp add: span_def) apply (rule hull_unique) apply (auto simp add: mem_def subspace_def) - unfolding mem_def[of "0::'a^_", symmetric] + unfolding mem_def[of "0::'a", symmetric] apply simp done @@ -1837,15 +1846,15 @@ and P: "subspace P" shows "\x \ span S. P x" using span_induct SP P by blast -inductive span_induct_alt_help for S:: "'a::semiring_1^_ \ bool" +inductive span_induct_alt_help for S:: "'a::real_vector \ bool" where span_induct_alt_help_0: "span_induct_alt_help S 0" - | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *s x + z)" + | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *\<^sub>R x + z)" lemma span_induct_alt': - assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\c x y. x \ S \ h y \ h (c*s x + y)" shows "\x \ span S. h x" + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" proof- - {fix x:: "'a^'n" assume x: "span_induct_alt_help S x" + {fix x:: "'a" assume x: "span_induct_alt_help S x" have "h x" apply (rule span_induct_alt_help.induct[OF x]) apply (rule h0) @@ -1876,10 +1885,10 @@ done} moreover {fix c x assume xt: "span_induct_alt_help S x" - then have "span_induct_alt_help S (c*s x)" + then have "span_induct_alt_help S (c *\<^sub>R x)" apply (induct rule: span_induct_alt_help.induct) apply (simp add: span_induct_alt_help_0) - apply (simp add: vector_smult_assoc vector_add_ldistrib) + apply (simp add: scaleR_right_distrib) apply (rule span_induct_alt_help_S) apply assumption apply simp @@ -1892,7 +1901,7 @@ qed lemma span_induct_alt: - assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\c x y. x \ S \ h y \ h (c*s x + y)" and x: "x \ span S" + 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 @@ -1905,26 +1914,26 @@ lemma span_add: "x \ span S \ y \ span S ==> x + y \ span S" by (metis subspace_add subspace_span) -lemma span_mul: "x \ span S ==> (c *s x) \ span S" +lemma span_mul: "x \ span S ==> (c *\<^sub>R x) \ span S" by (metis subspace_span subspace_mul) -lemma span_neg: "x \ span S ==> - (x::'a::ring_1^_) \ span S" +lemma span_neg: "x \ span S ==> - x \ span S" by (metis subspace_neg subspace_span) -lemma span_sub: "(x::'a::ring_1^_) \ span S \ y \ span S ==> x - y \ span S" +lemma span_sub: "x \ span S \ y \ span S ==> x - y \ span S" by (metis subspace_span subspace_sub) lemma span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" by (rule subspace_setsum, rule subspace_span) -lemma span_add_eq: "(x::'a::ring_1^_) \ span S \ x + y \ span S \ y \ span S" +lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" apply (auto simp only: span_add span_sub) apply (subgoal_tac "(x + y) - x \ span S", simp) by (simp only: span_add span_sub) (* Mapping under linear image. *) -lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ _ => _)" +lemma span_linear_image: assumes lf: "linear f" shows "span (f ` S) = f ` (span S)" proof- {fix x @@ -1957,8 +1966,8 @@ (* The key breakdown property. *) lemma span_breakdown: - assumes bS: "(b::'a::ring_1 ^ _) \ S" and aS: "a \ span S" - shows "\k. a - k*s b \ span (S - {b})" (is "?P a") + assumes bS: "b \ S" and aS: "a \ span S" + shows "\k. a - k *\<^sub>R b \ span (S - {b})" (is "?P a") proof- {fix x assume xS: "x \ S" {assume ab: "x = b" @@ -1983,23 +1992,23 @@ apply (simp add: mem_def) apply (clarsimp simp add: mem_def) apply (rule_tac x="k + ka" in exI) - apply (subgoal_tac "x + y - (k + ka) *s b = (x - k*s b) + (y - ka *s b)") + apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)") apply (simp only: ) apply (rule span_add[unfolded mem_def]) apply assumption+ - apply (vector field_simps) + apply (simp add: algebra_simps) apply (clarsimp simp add: mem_def) apply (rule_tac x= "c*k" in exI) - apply (subgoal_tac "c *s x - (c * k) *s b = c*s (x - k*s b)") + apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)") apply (simp only: ) apply (rule span_mul[unfolded mem_def]) apply assumption - by (vector field_simps) + by (simp add: algebra_simps) ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis qed lemma span_breakdown_eq: - "(x::'a::ring_1^_) \ span (insert a S) \ (\k. (x - k *s a) \ span S)" (is "?lhs \ ?rhs") + "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" (is "?lhs \ ?rhs") proof- {assume x: "x \ span (insert a S)" from x span_breakdown[of "a" "insert a S" "x"] @@ -2011,9 +2020,9 @@ apply blast done} moreover - { fix k assume k: "x - k *s a \ span S" - have eq: "x = (x - k *s a) + k *s a" by vector - have "(x - k *s a) + k *s a \ span (insert a S)" + { fix k assume k: "x - k *\<^sub>R a \ span S" + have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by vector + have "(x - k *\<^sub>R a) + k *\<^sub>R a \ span (insert a S)" apply (rule span_add) apply (rule set_rev_mp[of _ "span S" _]) apply (rule k) @@ -2030,11 +2039,11 @@ (* Hence some "reversal" results.*) lemma in_span_insert: - assumes a: "(a::'a::field^_) \ span (insert b S)" and na: "a \ span S" + assumes a: "a \ span (insert b S)" and na: "a \ span S" shows "b \ span (insert a S)" proof- from span_breakdown[of b "insert b S" a, OF insertI1 a] - obtain k where k: "a - k*s b \ span (S - {b})" by auto + obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto {assume k0: "k = 0" with k have "a \ span S" apply (simp) @@ -2046,12 +2055,12 @@ with na have ?thesis by blast} moreover {assume k0: "k \ 0" - have eq: "b = (1/k) *s a - ((1/k) *s a - b)" by vector - from k0 have eq': "(1/k) *s (a - k*s b) = (1/k) *s a - b" - by (vector field_simps) - from k have "(1/k) *s (a - k*s b) \ span (S - {b})" + have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by vector + from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" + by (simp add: algebra_simps) + from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \ span (S - {b})" by (rule span_mul) - hence th: "(1/k) *s a - b \ span (S - {b})" + hence th: "(1/k) *\<^sub>R a - b \ span (S - {b})" unfolding eq' . from k @@ -2069,7 +2078,7 @@ qed lemma in_span_delete: - assumes a: "(a::'a::field^_) \ span S" + assumes a: "a \ span S" and na: "a \ span (S-{b})" shows "b \ span (insert a (S - {b}))" apply (rule in_span_insert) @@ -2083,12 +2092,12 @@ (* Transitivity property. *) lemma span_trans: - assumes x: "(x::'a::ring_1^_) \ span S" and y: "y \ span (insert x S)" + assumes x: "x \ span S" and y: "y \ span (insert x S)" shows "y \ span S" proof- from span_breakdown[of x "insert x S" y, OF insertI1 y] - obtain k where k: "y -k*s x \ span (S - {x})" by auto - have eq: "y = (y - k *s x) + k *s x" by vector + obtain k where k: "y -k*\<^sub>R x \ span (S - {x})" by auto + have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by vector show ?thesis apply (subst eq) apply (rule span_add) @@ -2105,11 +2114,11 @@ (* ------------------------------------------------------------------------- *) lemma span_explicit: - "span P = {y::'a::semiring_1^_. \S u. finite S \ S \ P \ setsum (\v. u v *s v) S = y}" + "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") proof- {fix x assume x: "x \ ?E" - then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *s v) S = x" + then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" by blast have "x \ span P" unfolding u[symmetric] @@ -2126,7 +2135,7 @@ fix c x y assume x: "x \ P" and hy: "?h y" from hy obtain S u where fS: "finite S" and SP: "S\P" - and u: "setsum (\v. u v *s v) S = y" by blast + and u: "setsum (\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" @@ -2134,28 +2143,28 @@ {assume xS: "x \ S" have S1: "S = (S - {x}) \ {x}" and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto - have "setsum (\v. ?u v *s v) ?S =(\v\