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.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.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.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.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.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
```