# HG changeset patch # User huffman # Date 1395160747 25200 # Node ID 32b7eafc5a52490c8e831eeb06052a4c14372788 # Parent c7dfd924a1658cd45ec10cd820c0d81c121b70bf remove unnecessary finiteness assumptions from lemmas about setsum diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 18 11:58:30 2014 -0700 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Mar 18 09:39:07 2014 -0700 @@ -467,11 +467,10 @@ proof - let ?M = "(UNIV :: 'm set)" let ?N = "(UNIV :: 'n set)" - have fM: "finite ?M" by simp have "?rhs = (setsum (\i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j" unfolding setsum_component by simp then show ?thesis - unfolding linear_setsum_mul[OF lf fM, symmetric] + unfolding linear_setsum_mul[OF lf, symmetric] unfolding scalar_mult_eq_scaleR[symmetric] unfolding basis_expansion by simp @@ -674,7 +673,7 @@ where y: "setsum (\i. (y$i) *s column i A) ?U = x" by blast have "x \ span (columns A)" unfolding y[symmetric] - apply (rule span_setsum[OF fU]) + apply (rule span_setsum) apply clarify unfolding scalar_mult_eq_scaleR apply (rule span_mul) diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Mar 18 11:58:30 2014 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Mar 18 09:39:07 2014 -0700 @@ -7057,10 +7057,7 @@ fix i assume "i \ Basis" and "i \ d" have "?a \ span d" - apply (rule span_setsum[of d "(\b. b /\<^sub>R (2 * real (card d)))" d]) - using finite_subset[OF assms(2) finite_Basis] - apply blast - proof - + proof (rule span_setsum[of d "(\b. b /\<^sub>R (2 * real (card d)))" d]) { fix x :: "'a::euclidean_space" assume "x \ d" diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 18 11:58:30 2014 -0700 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 18 09:39:07 2014 -0700 @@ -544,16 +544,14 @@ subsection {* The traditional Rolle theorem in one dimension *} lemma linear_componentwise: - fixes f:: "'a::euclidean_space \ 'b::euclidean_space" + fixes f:: "'a::euclidean_space \ 'b::real_inner" assumes lf: "linear f" shows "(f x) \ j = (\i\Basis. (x\i) * (f i\j))" (is "?lhs = ?rhs") proof - - have fA: "finite Basis" - by simp have "?rhs = (\i\Basis. (x\i) *\<^sub>R (f i))\j" by (simp add: inner_setsum_left) then show ?thesis - unfolding linear_setsum_mul[OF lf fA, symmetric] + unfolding linear_setsum_mul[OF lf, symmetric] unfolding euclidean_representation .. qed diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 18 11:58:30 2014 -0700 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 18 09:39:07 2014 -0700 @@ -964,7 +964,7 @@ by simp have thd0: "det (\ i. if i = k then row k A + (\i \ ?Uk. x $ i *s row i A) else row i A) = det A" apply (rule det_row_span) - apply (rule span_setsum[OF fUk]) + apply (rule span_setsum) apply (rule ballI) apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ apply (rule span_superset) diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Mar 18 11:58:30 2014 -0700 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Mar 18 09:39:07 2014 -0700 @@ -157,8 +157,7 @@ lemma setsum_norm_bound: fixes f :: "'a \ 'b::real_normed_vector" - assumes fS: "finite S" - and K: "\x \ S. norm (f x) \ K" + assumes K: "\x \ S. norm (f x) \ K" shows "norm (setsum f S) \ of_nat (card S) * K" using setsum_norm_le[OF K] setsum_constant[symmetric] by simp @@ -250,13 +249,13 @@ by (simp add: linear_iff) lemma linear_compose_setsum: - assumes fS: "finite S" - and lS: "\a \ S. linear (f a)" + assumes lS: "\a \ S. linear (f a)" shows "linear (\x. setsum (\a. f a x) S)" - using lS - apply (induct rule: finite_induct[OF fS]) - apply (auto simp add: linear_zero intro: linear_compose_add) - done +proof (cases "finite S") + case True + then show ?thesis + using lS by induct (simp_all add: linear_zero linear_compose_add) +qed (simp add: linear_zero) lemma linear_0: "linear f \ f 0 = 0" unfolding linear_iff @@ -278,30 +277,18 @@ using linear_add [of f x "- y"] by (simp add: linear_neg) lemma linear_setsum: - assumes lin: "linear f" - and fin: "finite S" + assumes f: "linear f" shows "f (setsum g S) = setsum (f \ g) S" - using fin -proof induct - case empty - then show ?case - by (simp add: linear_0[OF lin]) -next - case (insert x F) - have "f (setsum g (insert x F)) = f (g x + setsum g F)" - using insert.hyps by simp - also have "\ = f (g x) + f (setsum g F)" - using linear_add[OF lin] by simp - also have "\ = setsum (f \ g) (insert x F)" - using insert.hyps by simp - finally show ?case . -qed +proof (cases "finite S") + case True + then show ?thesis + by induct (simp_all add: linear_0 [OF f] linear_add [OF f]) +qed (simp add: linear_0 [OF f]) lemma linear_setsum_mul: assumes lin: "linear f" - and fin: "finite S" 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 lin fin, of "\i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin] + using linear_setsum[OF lin, of "\i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin] by simp lemma linear_injective_0: @@ -425,7 +412,7 @@ have "f x \ y = f (\i\Basis. (x \ i) *\<^sub>R i) \ y" by (simp add: euclidean_representation) also have "\ = (\i\Basis. (x \ i) *\<^sub>R f i) \ y" - unfolding linear_setsum[OF lf finite_Basis] + unfolding linear_setsum[OF lf] by (simp add: linear_cmul[OF lf]) finally show "f x \ y = x \ ?w" by (simp add: inner_setsum_left inner_setsum_right mult_commute) @@ -706,12 +693,13 @@ lemma (in real_vector) subspace_setsum: assumes sA: "subspace A" - and fB: "finite B" - and f: "\x\ B. f x \ A" + and f: "\x\B. f x \ A" shows "setsum f B \ A" - using fB f sA - by (induct rule: finite_induct[OF fB]) - (simp add: subspace_def sA, auto simp add: sA subspace_add) +proof (cases "finite B") + case True + then show ?thesis + using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA]) +qed (simp add: subspace_0 [OF sA]) lemma subspace_linear_image: assumes lf: "linear f" @@ -921,8 +909,8 @@ lemma span_sub: "x \ span S \ y \ span S \ x - y \ span S" by (metis subspace_span subspace_sub) -lemma (in real_vector) span_setsum: "finite A \ \x \ A. f x \ span S \ setsum f A \ span S" - by (rule subspace_setsum, rule subspace_span) +lemma (in real_vector) span_setsum: "\x\A. f x \ span S \ setsum f A \ span S" + by (rule subspace_setsum [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) @@ -1943,7 +1931,7 @@ apply (simp only: scaleR_right_diff_distrib th0) apply (rule span_add_eq) apply (rule span_mul) - apply (rule span_setsum[OF C(1)]) + apply (rule span_setsum) apply clarify apply (rule span_mul) apply (rule span_superset) @@ -2030,7 +2018,7 @@ let ?a = "a - setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" have "setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" unfolding sSB - apply (rule span_setsum[OF fB(1)]) + apply (rule span_setsum) apply clarsimp apply (rule span_mul) apply (rule span_superset) @@ -3030,4 +3018,3 @@ done end -