src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 64267 b9a1486e79be
parent 63945 444eafb6e864
child 66447 a1f5c5c26fa6
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -12,18 +12,18 @@
     1.4    by simp
     1.5  
     1.6  (*move up?*)
     1.7 -lemma setsum_UNIV_sum:
     1.8 +lemma sum_UNIV_sum:
     1.9    fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
    1.10    shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
    1.11    apply (subst UNIV_Plus_UNIV [symmetric])
    1.12 -  apply (subst setsum.Plus)
    1.13 +  apply (subst sum.Plus)
    1.14    apply simp_all
    1.15    done
    1.16  
    1.17 -lemma setsum_mult_product:
    1.18 -  "setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
    1.19 -  unfolding setsum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
    1.20 -proof (rule setsum.cong, simp, rule setsum.reindex_cong)
    1.21 +lemma sum_mult_product:
    1.22 +  "sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
    1.23 +  unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
    1.24 +proof (rule sum.cong, simp, rule sum.reindex_cong)
    1.25    fix i
    1.26    show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
    1.27    show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"
    1.28 @@ -108,19 +108,19 @@
    1.29  
    1.30  subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
    1.31  
    1.32 -lemma setsum_cong_aux:
    1.33 -  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
    1.34 -  by (auto intro: setsum.cong)
    1.35 +lemma sum_cong_aux:
    1.36 +  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
    1.37 +  by (auto intro: sum.cong)
    1.38  
    1.39 -hide_fact (open) setsum_cong_aux
    1.40 +hide_fact (open) sum_cong_aux
    1.41  
    1.42  method_setup vector = \<open>
    1.43  let
    1.44    val ss1 =
    1.45      simpset_of (put_simpset HOL_basic_ss @{context}
    1.46 -      addsimps [@{thm setsum.distrib} RS sym,
    1.47 -      @{thm setsum_subtractf} RS sym, @{thm setsum_distrib_left},
    1.48 -      @{thm setsum_distrib_right}, @{thm setsum_negf} RS sym])
    1.49 +      addsimps [@{thm sum.distrib} RS sym,
    1.50 +      @{thm sum_subtractf} RS sym, @{thm sum_distrib_left},
    1.51 +      @{thm sum_distrib_right}, @{thm sum_negf} RS sym])
    1.52    val ss2 =
    1.53      simpset_of (@{context} addsimps
    1.54               [@{thm plus_vec_def}, @{thm times_vec_def},
    1.55 @@ -130,8 +130,8 @@
    1.56                @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
    1.57    fun vector_arith_tac ctxt ths =
    1.58      simp_tac (put_simpset ss1 ctxt)
    1.59 -    THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.setsum_cong_aux} i
    1.60 -         ORELSE resolve_tac ctxt @{thms setsum.neutral} i
    1.61 +    THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.sum_cong_aux} i
    1.62 +         ORELSE resolve_tac ctxt @{thms sum.neutral} i
    1.63           ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i)
    1.64      (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    1.65      THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths)
    1.66 @@ -152,9 +152,9 @@
    1.67  lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
    1.68  lemma vec_neg: "vec(- x) = - vec x " by vector
    1.69  
    1.70 -lemma vec_setsum:
    1.71 +lemma vec_sum:
    1.72    assumes "finite S"
    1.73 -  shows "vec(setsum f S) = setsum (vec \<circ> f) S"
    1.74 +  shows "vec(sum f S) = sum (vec \<circ> f) S"
    1.75    using assms
    1.76  proof induct
    1.77    case empty
    1.78 @@ -299,8 +299,8 @@
    1.79  lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
    1.80    by (metis component_le_norm_cart le_less_trans)
    1.81  
    1.82 -lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
    1.83 -  by (simp add: norm_vec_def setL2_le_setsum)
    1.84 +lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
    1.85 +  by (simp add: norm_vec_def setL2_le_sum)
    1.86  
    1.87  lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
    1.88    unfolding scaleR_vec_def vector_scalar_mult_def by simp
    1.89 @@ -309,9 +309,9 @@
    1.90    unfolding dist_norm scalar_mult_eq_scaleR
    1.91    unfolding scaleR_right_diff_distrib[symmetric] by simp
    1.92  
    1.93 -lemma setsum_component [simp]:
    1.94 +lemma sum_component [simp]:
    1.95    fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
    1.96 -  shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
    1.97 +  shows "(sum f S)$i = sum (\<lambda>x. (f x)$i) S"
    1.98  proof (cases "finite S")
    1.99    case True
   1.100    then show ?thesis by induct simp_all
   1.101 @@ -320,19 +320,19 @@
   1.102    then show ?thesis by simp
   1.103  qed
   1.104  
   1.105 -lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
   1.106 +lemma sum_eq: "sum f S = (\<chi> i. sum (\<lambda>x. (f x)$i ) S)"
   1.107    by (simp add: vec_eq_iff)
   1.108  
   1.109 -lemma setsum_cmul:
   1.110 +lemma sum_cmul:
   1.111    fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
   1.112 -  shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
   1.113 -  by (simp add: vec_eq_iff setsum_distrib_left)
   1.114 +  shows "sum (\<lambda>x. c *s f x) S = c *s sum f S"
   1.115 +  by (simp add: vec_eq_iff sum_distrib_left)
   1.116  
   1.117 -lemma setsum_norm_allsubsets_bound_cart:
   1.118 +lemma sum_norm_allsubsets_bound_cart:
   1.119    fixes f:: "'a \<Rightarrow> real ^'n"
   1.120 -  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
   1.121 -  shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
   1.122 -  using setsum_norm_allsubsets_bound[OF assms]
   1.123 +  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
   1.124 +  shows "sum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
   1.125 +  using sum_norm_allsubsets_bound[OF assms]
   1.126    by simp
   1.127  
   1.128  subsection\<open>Closures and interiors of halfspaces\<close>
   1.129 @@ -475,15 +475,15 @@
   1.130  
   1.131  definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
   1.132      (infixl "**" 70)
   1.133 -  where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
   1.134 +  where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
   1.135  
   1.136  definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"
   1.137      (infixl "*v" 70)
   1.138 -  where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
   1.139 +  where "m *v x \<equiv> (\<chi> i. sum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
   1.140  
   1.141  definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
   1.142      (infixl "v*" 70)
   1.143 -  where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
   1.144 +  where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
   1.145  
   1.146  definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
   1.147  definition transpose where
   1.148 @@ -495,14 +495,14 @@
   1.149  
   1.150  lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
   1.151  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
   1.152 -  by (vector matrix_matrix_mult_def setsum.distrib[symmetric] field_simps)
   1.153 +  by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
   1.154  
   1.155  lemma matrix_mul_lid:
   1.156    fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   1.157    shows "mat 1 ** A = A"
   1.158    apply (simp add: matrix_matrix_mult_def mat_def)
   1.159    apply vector
   1.160 -  apply (auto simp only: if_distrib cond_application_beta setsum.delta'[OF finite]
   1.161 +  apply (auto simp only: if_distrib cond_application_beta sum.delta'[OF finite]
   1.162      mult_1_left mult_zero_left if_True UNIV_I)
   1.163    done
   1.164  
   1.165 @@ -512,26 +512,26 @@
   1.166    shows "A ** mat 1 = A"
   1.167    apply (simp add: matrix_matrix_mult_def mat_def)
   1.168    apply vector
   1.169 -  apply (auto simp only: if_distrib cond_application_beta setsum.delta[OF finite]
   1.170 +  apply (auto simp only: if_distrib cond_application_beta sum.delta[OF finite]
   1.171      mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
   1.172    done
   1.173  
   1.174  lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
   1.175 -  apply (vector matrix_matrix_mult_def setsum_distrib_left setsum_distrib_right mult.assoc)
   1.176 -  apply (subst setsum.commute)
   1.177 +  apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
   1.178 +  apply (subst sum.commute)
   1.179    apply simp
   1.180    done
   1.181  
   1.182  lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
   1.183    apply (vector matrix_matrix_mult_def matrix_vector_mult_def
   1.184 -    setsum_distrib_left setsum_distrib_right mult.assoc)
   1.185 -  apply (subst setsum.commute)
   1.186 +    sum_distrib_left sum_distrib_right mult.assoc)
   1.187 +  apply (subst sum.commute)
   1.188    apply simp
   1.189    done
   1.190  
   1.191  lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
   1.192    apply (vector matrix_vector_mult_def mat_def)
   1.193 -  apply (simp add: if_distrib cond_application_beta setsum.delta' cong del: if_weak_cong)
   1.194 +  apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong)
   1.195    done
   1.196  
   1.197  lemma matrix_transpose_mul:
   1.198 @@ -548,15 +548,15 @@
   1.199    apply (erule_tac x="axis ia 1" in allE)
   1.200    apply (erule_tac x="i" in allE)
   1.201    apply (auto simp add: if_distrib cond_application_beta axis_def
   1.202 -    setsum.delta[OF finite] cong del: if_weak_cong)
   1.203 +    sum.delta[OF finite] cong del: if_weak_cong)
   1.204    done
   1.205  
   1.206  lemma matrix_vector_mul_component: "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
   1.207    by (simp add: matrix_vector_mult_def inner_vec_def)
   1.208  
   1.209  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
   1.210 -  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_distrib_right setsum_distrib_left ac_simps)
   1.211 -  apply (subst setsum.commute)
   1.212 +  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
   1.213 +  apply (subst sum.commute)
   1.214    apply simp
   1.215    done
   1.216  
   1.217 @@ -588,27 +588,27 @@
   1.218    by (simp add: matrix_vector_mult_def inner_vec_def)
   1.219  
   1.220  lemma matrix_mult_vsum:
   1.221 -  "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   1.222 +  "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   1.223    by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
   1.224  
   1.225  lemma vector_componentwise:
   1.226    "(x::'a::ring_1^'n) = (\<chi> j. \<Sum>i\<in>UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)"
   1.227 -  by (simp add: axis_def if_distrib setsum.If_cases vec_eq_iff)
   1.228 +  by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff)
   1.229  
   1.230 -lemma basis_expansion: "setsum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
   1.231 -  by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong)
   1.232 +lemma basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
   1.233 +  by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong)
   1.234  
   1.235  lemma linear_componentwise_expansion:
   1.236    fixes f:: "real ^'m \<Rightarrow> real ^ _"
   1.237    assumes lf: "linear f"
   1.238 -  shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
   1.239 +  shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
   1.240  proof -
   1.241    let ?M = "(UNIV :: 'm set)"
   1.242    let ?N = "(UNIV :: 'n set)"
   1.243 -  have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j"
   1.244 -    unfolding setsum_component by simp
   1.245 +  have "?rhs = (sum (\<lambda>i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j"
   1.246 +    unfolding sum_component by simp
   1.247    then show ?thesis
   1.248 -    unfolding linear_setsum_mul[OF lf, symmetric]
   1.249 +    unfolding linear_sum_mul[OF lf, symmetric]
   1.250      unfolding scalar_mult_eq_scaleR[symmetric]
   1.251      unfolding basis_expansion
   1.252      by simp
   1.253 @@ -630,7 +630,7 @@
   1.254  
   1.255  lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
   1.256    by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
   1.257 -      field_simps setsum_distrib_left setsum.distrib)
   1.258 +      field_simps sum_distrib_left sum.distrib)
   1.259  
   1.260  lemma matrix_works:
   1.261    assumes lf: "linear f"
   1.262 @@ -652,14 +652,14 @@
   1.263    by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
   1.264  
   1.265  lemma matrix_vector_column:
   1.266 -  "(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   1.267 +  "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   1.268    by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
   1.269  
   1.270  lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
   1.271    apply (rule adjoint_unique)
   1.272    apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
   1.273 -    setsum_distrib_right setsum_distrib_left)
   1.274 -  apply (subst setsum.commute)
   1.275 +    sum_distrib_right sum_distrib_left)
   1.276 +  apply (subst sum.commute)
   1.277    apply (auto simp add: ac_simps)
   1.278    done
   1.279  
   1.280 @@ -758,13 +758,13 @@
   1.281  lemma matrix_left_invertible_independent_columns:
   1.282    fixes A :: "real^'n^'m"
   1.283    shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
   1.284 -      (\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
   1.285 +      (\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
   1.286      (is "?lhs \<longleftrightarrow> ?rhs")
   1.287  proof -
   1.288    let ?U = "UNIV :: 'n set"
   1.289    { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
   1.290      { fix c i
   1.291 -      assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
   1.292 +      assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
   1.293        let ?x = "\<chi> i. c i"
   1.294        have th0:"A *v ?x = 0"
   1.295          using c
   1.296 @@ -786,7 +786,7 @@
   1.297  lemma matrix_right_invertible_independent_rows:
   1.298    fixes A :: "real^'n^'m"
   1.299    shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow>
   1.300 -    (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
   1.301 +    (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
   1.302    unfolding left_invertible_transpose[symmetric]
   1.303      matrix_left_invertible_independent_columns
   1.304    by (simp add: column_transpose)
   1.305 @@ -797,7 +797,7 @@
   1.306  proof -
   1.307    let ?U = "UNIV :: 'm set"
   1.308    have fU: "finite ?U" by simp
   1.309 -  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y)"
   1.310 +  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
   1.311      unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
   1.312      apply (subst eq_commute)
   1.313      apply rule
   1.314 @@ -806,10 +806,10 @@
   1.315    { assume h: ?lhs
   1.316      { fix x:: "real ^'n"
   1.317        from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m"
   1.318 -        where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
   1.319 +        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
   1.320        have "x \<in> span (columns A)"
   1.321          unfolding y[symmetric]
   1.322 -        apply (rule span_setsum)
   1.323 +        apply (rule span_sum)
   1.324          unfolding scalar_mult_eq_scaleR
   1.325          apply (rule span_mul)
   1.326          apply (rule span_superset)
   1.327 @@ -820,11 +820,11 @@
   1.328      then have ?rhs unfolding rhseq by blast }
   1.329    moreover
   1.330    { assume h:?rhs
   1.331 -    let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y"
   1.332 +    let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
   1.333      { fix y
   1.334        have "?P y"
   1.335        proof (rule span_induct_alt[of ?P "columns A", folded scalar_mult_eq_scaleR])
   1.336 -        show "\<exists>x::real ^ 'm. setsum (\<lambda>i. (x$i) *s column i A) ?U = 0"
   1.337 +        show "\<exists>x::real ^ 'm. sum (\<lambda>i. (x$i) *s column i A) ?U = 0"
   1.338            by (rule exI[where x=0], simp)
   1.339        next
   1.340          fix c y1 y2
   1.341 @@ -832,7 +832,7 @@
   1.342          from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
   1.343            unfolding columns_def by blast
   1.344          from y2 obtain x:: "real ^'m" where
   1.345 -          x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
   1.346 +          x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
   1.347          let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
   1.348          show "?P (c*s y1 + y2)"
   1.349          proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong)
   1.350 @@ -840,18 +840,18 @@
   1.351            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.352                else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
   1.353              using i(1) by (simp add: field_simps)
   1.354 -          have "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.355 -              else (x$xa) * ((column xa A$j))) ?U = setsum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
   1.356 -            apply (rule setsum.cong[OF refl])
   1.357 +          have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.358 +              else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
   1.359 +            apply (rule sum.cong[OF refl])
   1.360              using th apply blast
   1.361              done
   1.362 -          also have "\<dots> = setsum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.363 -            by (simp add: setsum.distrib)
   1.364 -          also have "\<dots> = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.365 -            unfolding setsum.delta[OF fU]
   1.366 +          also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.367 +            by (simp add: sum.distrib)
   1.368 +          also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.369 +            unfolding sum.delta[OF fU]
   1.370              using i(1) by simp
   1.371 -          finally show "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.372 -            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
   1.373 +          finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.374 +            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
   1.375          qed
   1.376        next
   1.377          show "y \<in> span (columns A)"
   1.378 @@ -984,9 +984,9 @@
   1.379      { fix n
   1.380        assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
   1.381        have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
   1.382 -        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum)
   1.383 +        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum)
   1.384        also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
   1.385 -        by (rule setsum_strict_mono) (simp_all add: n)
   1.386 +        by (rule sum_strict_mono) (simp_all add: n)
   1.387        finally have "dist (f (r n)) l < e" by simp
   1.388      }
   1.389      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
   1.390 @@ -1235,7 +1235,7 @@
   1.391      where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
   1.392  proof -
   1.393    from assms obtain s where "finite s"
   1.394 -    and "cbox (x - setsum (op *\<^sub>R d) Basis) (x + setsum (op *\<^sub>R d) Basis) = convex hull s"
   1.395 +    and "cbox (x - sum (op *\<^sub>R d) Basis) (x + sum (op *\<^sub>R d) Basis) = convex hull s"
   1.396      by (rule cube_convex_hull)
   1.397    with that[of s] show thesis
   1.398      by (simp add: const_vector_cart)
   1.399 @@ -1314,13 +1314,13 @@
   1.400  lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
   1.401    using exhaust_3 by auto
   1.402  
   1.403 -lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
   1.404 +lemma sum_1: "sum f (UNIV::1 set) = f 1"
   1.405    unfolding UNIV_1 by simp
   1.406  
   1.407 -lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
   1.408 +lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
   1.409    unfolding UNIV_2 by simp
   1.410  
   1.411 -lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
   1.412 +lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
   1.413    unfolding UNIV_3 by (simp add: ac_simps)
   1.414  
   1.415  instantiation num1 :: cart_one