1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 11:58:30 2014 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 09:39:07 2014 -0700
     1.3 @@ -467,11 +467,10 @@
     1.4  proof -
     1.5    let ?M = "(UNIV :: 'm set)"
     1.6    let ?N = "(UNIV :: 'n set)"
     1.7 -  have fM: "finite ?M" by simp
     1.8    have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j"
     1.9      unfolding setsum_component by simp
    1.10    then show ?thesis
    1.11 -    unfolding linear_setsum_mul[OF lf fM, symmetric]
    1.12 +    unfolding linear_setsum_mul[OF lf, symmetric]
    1.13      unfolding scalar_mult_eq_scaleR[symmetric]
    1.14      unfolding basis_expansion
    1.15      by simp
    1.16 @@ -674,7 +673,7 @@
    1.17          where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
    1.18        have "x \<in> span (columns A)"
    1.19          unfolding y[symmetric]
    1.20 -        apply (rule span_setsum[OF fU])
    1.21 +        apply (rule span_setsum)
    1.22          apply clarify
    1.23          unfolding scalar_mult_eq_scaleR
    1.24          apply (rule span_mul)

     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 11:58:30 2014 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 09:39:07 2014 -0700
     2.3 @@ -7057,10 +7057,7 @@
     2.4      fix i
     2.5      assume "i \<in> Basis" and "i \<notin> d"
     2.6      have "?a \<in> span d"
     2.7 -      apply (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d])
     2.8 -      using finite_subset[OF assms(2) finite_Basis]
     2.9 -      apply blast
    2.10 -    proof -
    2.11 +    proof (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d])
    2.12        {
    2.13          fix x :: "'a::euclidean_space"
    2.14          assume "x \<in> d"

     3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 18 11:58:30 2014 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 18 09:39:07 2014 -0700
     3.3 @@ -544,16 +544,14 @@
     3.4  subsection {* The traditional Rolle theorem in one dimension *}
     3.5  
     3.6  lemma linear_componentwise:
     3.7 -  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     3.8 +  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
     3.9    assumes lf: "linear f"
    3.10    shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
    3.11  proof -
    3.12 -  have fA: "finite Basis"
    3.13 -    by simp
    3.14    have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
    3.15      by (simp add: inner_setsum_left)
    3.16    then show ?thesis
    3.17 -    unfolding linear_setsum_mul[OF lf fA, symmetric]
    3.18 +    unfolding linear_setsum_mul[OF lf, symmetric]
    3.19      unfolding euclidean_representation ..
    3.20  qed
    3.21  

     4.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Mar 18 11:58:30 2014 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Mar 18 09:39:07 2014 -0700
     4.3 @@ -964,7 +964,7 @@
     4.4      by simp
     4.5    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"
     4.6      apply (rule det_row_span)
     4.7 -    apply (rule span_setsum[OF fUk])
     4.8 +    apply (rule span_setsum)
     4.9      apply (rule ballI)
    4.10      apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
    4.11      apply (rule span_superset)

     5.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 18 11:58:30 2014 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 18 09:39:07 2014 -0700
     5.3 @@ -157,8 +157,7 @@
     5.4  
     5.5  lemma setsum_norm_bound:
     5.6    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     5.7 -  assumes fS: "finite S"
     5.8 -    and K: "\<forall>x \<in> S. norm (f x) \<le> K"
     5.9 +  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
    5.10    shows "norm (setsum f S) \<le> of_nat (card S) * K"
    5.11    using setsum_norm_le[OF K] setsum_constant[symmetric]
    5.12    by simp
    5.13 @@ -250,13 +249,13 @@
    5.14    by (simp add: linear_iff)
    5.15  
    5.16  lemma linear_compose_setsum:
    5.17 -  assumes fS: "finite S"
    5.18 -    and lS: "\<forall>a \<in> S. linear (f a)"
    5.19 +  assumes lS: "\<forall>a \<in> S. linear (f a)"
    5.20    shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
    5.21 -  using lS
    5.22 -  apply (induct rule: finite_induct[OF fS])
    5.23 -  apply (auto simp add: linear_zero intro: linear_compose_add)
    5.24 -  done
    5.25 +proof (cases "finite S")
    5.26 +  case True
    5.27 +  then show ?thesis
    5.28 +    using lS by induct (simp_all add: linear_zero linear_compose_add)
    5.29 +qed (simp add: linear_zero)
    5.30  
    5.31  lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
    5.32    unfolding linear_iff
    5.33 @@ -278,30 +277,18 @@
    5.34    using linear_add [of f x "- y"] by (simp add: linear_neg)
    5.35  
    5.36  lemma linear_setsum:
    5.37 -  assumes lin: "linear f"
    5.38 -    and fin: "finite S"
    5.39 +  assumes f: "linear f"
    5.40    shows "f (setsum g S) = setsum (f \<circ> g) S"
    5.41 -  using fin
    5.42 -proof induct
    5.43 -  case empty
    5.44 -  then show ?case
    5.45 -    by (simp add: linear_0[OF lin])
    5.46 -next
    5.47 -  case (insert x F)
    5.48 -  have "f (setsum g (insert x F)) = f (g x + setsum g F)"
    5.49 -    using insert.hyps by simp
    5.50 -  also have "\<dots> = f (g x) + f (setsum g F)"
    5.51 -    using linear_add[OF lin] by simp
    5.52 -  also have "\<dots> = setsum (f \<circ> g) (insert x F)"
    5.53 -    using insert.hyps by simp
    5.54 -  finally show ?case .
    5.55 -qed
    5.56 +proof (cases "finite S")
    5.57 +  case True
    5.58 +  then show ?thesis
    5.59 +    by induct (simp_all add: linear_0 [OF f] linear_add [OF f])
    5.60 +qed (simp add: linear_0 [OF f])
    5.61  
    5.62  lemma linear_setsum_mul:
    5.63    assumes lin: "linear f"
    5.64 -    and fin: "finite S"
    5.65    shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
    5.66 -  using linear_setsum[OF lin fin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
    5.67 +  using linear_setsum[OF lin, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lin]
    5.68    by simp
    5.69  
    5.70  lemma linear_injective_0:
    5.71 @@ -425,7 +412,7 @@
    5.72      have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
    5.73        by (simp add: euclidean_representation)
    5.74      also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
    5.75 -      unfolding linear_setsum[OF lf finite_Basis]
    5.76 +      unfolding linear_setsum[OF lf]
    5.77        by (simp add: linear_cmul[OF lf])
    5.78      finally show "f x \<bullet> y = x \<bullet> ?w"
    5.79        by (simp add: inner_setsum_left inner_setsum_right mult_commute)
    5.80 @@ -706,12 +693,13 @@
    5.81  
    5.82  lemma (in real_vector) subspace_setsum:
    5.83    assumes sA: "subspace A"
    5.84 -    and fB: "finite B"
    5.85 -    and f: "\<forall>x\<in> B. f x \<in> A"
    5.86 +    and f: "\<forall>x\<in>B. f x \<in> A"
    5.87    shows "setsum f B \<in> A"
    5.88 -  using  fB f sA
    5.89 -  by (induct rule: finite_induct[OF fB])
    5.90 -    (simp add: subspace_def sA, auto simp add: sA subspace_add)
    5.91 +proof (cases "finite B")
    5.92 +  case True
    5.93 +  then show ?thesis
    5.94 +    using f by induct (simp_all add: subspace_0 [OF sA] subspace_add [OF sA])
    5.95 +qed (simp add: subspace_0 [OF sA])
    5.96  
    5.97  lemma subspace_linear_image:
    5.98    assumes lf: "linear f"
    5.99 @@ -921,8 +909,8 @@
   5.100  lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
   5.101    by (metis subspace_span subspace_sub)
   5.102  
   5.103 -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"
   5.104 -  by (rule subspace_setsum, rule subspace_span)
   5.105 +lemma (in real_vector) span_setsum: "\<forall>x\<in>A. f x \<in> span S \<Longrightarrow> setsum f A \<in> span S"
   5.106 +  by (rule subspace_setsum [OF subspace_span])
   5.107  
   5.108  lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
   5.109    by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
   5.110 @@ -1943,7 +1931,7 @@
   5.111        apply (simp only: scaleR_right_diff_distrib th0)
   5.112        apply (rule span_add_eq)
   5.113        apply (rule span_mul)
   5.114 -      apply (rule span_setsum[OF C(1)])
   5.115 +      apply (rule span_setsum)
   5.116        apply clarify
   5.117        apply (rule span_mul)
   5.118        apply (rule span_superset)
   5.119 @@ -2030,7 +2018,7 @@
   5.120    let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
   5.121    have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
   5.122      unfolding sSB
   5.123 -    apply (rule span_setsum[OF fB(1)])
   5.124 +    apply (rule span_setsum)
   5.125      apply clarsimp
   5.126      apply (rule span_mul)
   5.127      apply (rule span_superset)
   5.128 @@ -3030,4 +3018,3 @@
   5.129    done
   5.130  
   5.131  end
   5.132 -