--- 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 (\<lambda>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 (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
have "x \<in> 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)
--- 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 \<in> Basis" and "i \<notin> d"
have "?a \<in> span d"
- apply (rule span_setsum[of d "(\<lambda>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 "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d])
{
fix x :: "'a::euclidean_space"
assume "x \<in> d"
--- 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 \<Rightarrow> 'b::euclidean_space"
+ fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes lf: "linear f"
shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
proof -
- have fA: "finite Basis"
- by simp
have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>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
--- 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 (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?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)
--- 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 \<Rightarrow> 'b::real_normed_vector"
- assumes fS: "finite S"
- and K: "\<forall>x \<in> S. norm (f x) \<le> K"
+ assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
shows "norm (setsum f S) \<le> 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: "\<forall>a \<in> S. linear (f a)"
+ assumes lS: "\<forall>a \<in> S. linear (f a)"
shows "linear (\<lambda>x. setsum (\<lambda>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 \<Longrightarrow> 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 \<circ> 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 "\<dots> = f (g x) + f (setsum g F)"
- using linear_add[OF lin] by simp
- also have "\<dots> = setsum (f \<circ> 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 (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
- using linear_setsum[OF lin fin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
+ using linear_setsum[OF lin, of "\<lambda>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 \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
by (simp add: euclidean_representation)
also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
- unfolding linear_setsum[OF lf finite_Basis]
+ unfolding linear_setsum[OF lf]
by (simp add: linear_cmul[OF lf])
finally show "f x \<bullet> y = x \<bullet> ?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: "\<forall>x\<in> B. f x \<in> A"
+ and f: "\<forall>x\<in>B. f x \<in> A"
shows "setsum f B \<in> 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 \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
by (metis subspace_span subspace_sub)
-lemma (in real_vector) span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S \<Longrightarrow> setsum f A \<in> span S"
- by (rule subspace_setsum, rule subspace_span)
+lemma (in real_vector) span_setsum: "\<forall>x\<in>A. f x \<in> span S \<Longrightarrow> setsum f A \<in> span S"
+ by (rule subspace_setsum [OF subspace_span])
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> 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 (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> 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
-