author huffman Tue, 18 Mar 2014 09:39:07 -0700 changeset 56196 32b7eafc5a52 parent 56195 c7dfd924a165 child 56211 3250d70c8d0b
remove unnecessary finiteness assumptions from lemmas about setsum
```--- 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"
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 @@

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])
-  done
+proof (cases "finite S")
+  case True
+  then show ?thesis

lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
unfolding linear_iff
@@ -278,30 +277,18 @@

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
+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"
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]
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])
+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_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
-```