author nipkow Thu, 15 Sep 2016 17:05:34 +0200 changeset 63883 41b5d9f3778a parent 63881 b746b19197bd (current diff) parent 63882 018998c00003 (diff) child 63884 d588f684ccaf
merged
```--- a/NEWS	Thu Sep 15 15:48:37 2016 +0100
+++ b/NEWS	Thu Sep 15 17:05:34 2016 +0200
@@ -251,6 +251,10 @@
* Theory Set_Interval.thy: substantial new theorems on indexed sums
and products.

+* Theory List.thy:
+  listsum ~> sum_list
+  listprod ~> prod_list
+
* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
equations in functional programming style: variables present on the
left-hand but not on the righ-hand side are replaced by underscores.```
```--- a/src/HOL/Binomial.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Binomial.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -1521,28 +1521,28 @@
qed

text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is @{term "(N + m - 1) choose N"}:\<close>
-lemma card_length_listsum_rec:
+lemma card_length_sum_list_rec:
assumes "m \<ge> 1"
-  shows "card {l::nat list. length l = m \<and> listsum l = N} =
-      card {l. length l = (m - 1) \<and> listsum l = N} +
-      card {l. length l = m \<and> listsum l + 1 = N}"
+  shows "card {l::nat list. length l = m \<and> sum_list l = N} =
+      card {l. length l = (m - 1) \<and> sum_list l = N} +
+      card {l. length l = m \<and> sum_list l + 1 = N}"
(is "card ?C = card ?A + card ?B")
proof -
-  let ?A' = "{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
-  let ?B' = "{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
+  let ?A' = "{l. length l = m \<and> sum_list l = N \<and> hd l = 0}"
+  let ?B' = "{l. length l = m \<and> sum_list l = N \<and> hd l \<noteq> 0}"
let ?f = "\<lambda>l. 0 # l"
let ?g = "\<lambda>l. (hd l + 1) # tl l"
have 1: "xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" for x xs
by simp
-  have 2: "xs \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs" for xs :: "nat list"
+  have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
have f: "bij_betw ?f ?A ?A'"
apply (rule bij_betw_byWitness[where f' = tl])
using assms
apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
done
-  have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs" for xs :: "nat list"
-    by (metis 1 listsum_simps(2) 2)
+  have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
+    by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
using assms
@@ -1552,10 +1552,10 @@
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]
by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"])
-      (auto simp: member_le_listsum_nat less_Suc_eq_le)
+      (auto simp: member_le_sum_list_nat less_Suc_eq_le)
have fin_B: "finite ?B"
by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"])
-      (auto simp: member_le_listsum_nat less_Suc_eq_le fin)
+      (auto simp: member_le_sum_list_nat less_Suc_eq_le fin)
have uni: "?C = ?A' \<union> ?B'"
by auto
have disj: "?A' \<inter> ?B' = {}"
@@ -1569,7 +1569,7 @@
finally show ?thesis .
qed

-lemma card_length_listsum: "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
+lemma card_length_sum_list: "card {l::nat list. size l = m \<and> sum_list l = N} = (N + m - 1) choose N"
\<comment> "by Holden Lee, tidied by Tobias Nipkow"
proof (cases m)
case 0
@@ -1590,7 +1590,7 @@
by simp
next
case (Suc k)
-    have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} = (N + (m - 1) - 1) choose N"
+    have c1: "card {l::nat list. size l = (m - 1) \<and> sum_list l =  N} = (N + (m - 1) - 1) choose N"
proof (cases "m = 1")
case True
with Suc.hyps have "N \<ge> 1"
@@ -1602,23 +1602,23 @@
then show ?thesis
using Suc by fastforce
qed
-    from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
+    from Suc have c2: "card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
(if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
proof -
have *: "n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" for m n
by arith
from Suc have "N > 0 \<Longrightarrow>
-        card {l::nat list. size l = m \<and> listsum l + 1 = N} =
+        card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
((N - 1) + m - 1) choose (N - 1)"
then show ?thesis
by auto
qed
-    from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
-          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
+    from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> sum_list l = N} +
+          card {l::nat list. size l = m \<and> sum_list l + 1 = N}) = (N + m - 1) choose N"
by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
then show ?case
-      using card_length_listsum_rec[OF Suc.prems] by auto
+      using card_length_sum_list_rec[OF Suc.prems] by auto
qed
qed
```
```--- a/src/HOL/GCD.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/GCD.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -865,7 +865,7 @@
done

-lemma listprod_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
+lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
by (induct xs) (simp_all add: gcd_mult_cancel)

lemma coprime_divisors:```
```--- a/src/HOL/Groups_List.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Groups_List.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -55,32 +55,32 @@
begin

-sublocale listsum: monoid_list plus 0
+sublocale sum_list: monoid_list plus 0
defines
-  listsum = listsum.F ..
+  sum_list = sum_list.F ..

end

begin

-sublocale listsum: comm_monoid_list plus 0
+sublocale sum_list: comm_monoid_list plus 0
rewrites
-  "monoid_list.F plus 0 = listsum"
+  "monoid_list.F plus 0 = sum_list"
proof -
show "comm_monoid_list plus 0" ..
-  then interpret listsum: comm_monoid_list plus 0 .
-  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
+  then interpret sum_list: comm_monoid_list plus 0 .
+  from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
qed

sublocale setsum: comm_monoid_list_set plus 0
rewrites
-  "monoid_list.F plus 0 = listsum"
+  "monoid_list.F plus 0 = sum_list"
and "comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_list_set plus 0" ..
then interpret setsum: comm_monoid_list_set plus 0 .
-  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
+  from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
qed

@@ -88,39 +88,39 @@

text \<open>Some syntactic sugar for summing a function over a list:\<close>
syntax (ASCII)
-  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
+  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax
-  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
-  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)"
+  "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"

text \<open>TODO duplicates\<close>
-lemmas listsum_simps = listsum.Nil listsum.Cons
-lemmas listsum_append = listsum.append
-lemmas listsum_rev = listsum.rev
+lemmas sum_list_simps = sum_list.Nil sum_list.Cons
+lemmas sum_list_append = sum_list.append
+lemmas sum_list_rev = sum_list.rev

-  "fold plus xs = plus (listsum (rev xs))"
+  "fold plus xs = plus (sum_list (rev xs))"
proof
fix x
-  have "fold plus xs x = listsum (rev xs @ [x])"
-    by (simp add: foldr_conv_fold listsum.eq_foldr)
-  also have "\<dots> = listsum (rev xs) + x"
+  have "fold plus xs x = sum_list (rev xs @ [x])"
+    by (simp add: foldr_conv_fold sum_list.eq_foldr)
+  also have "\<dots> = sum_list (rev xs) + x"
by simp
-  finally show "fold plus xs x = listsum (rev xs) + x"
+  finally show "fold plus xs x = sum_list (rev xs) + x"
.
qed

-  "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
+  "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)

-  "size_list f xs = listsum (map f xs) + size xs"
+  "size_list f xs = sum_list (map f xs) + size xs"
by (induct xs) auto

-  "length (concat xss) = listsum (map length xss)"
+  "length (concat xss) = sum_list (map length xss)"
by (induct xss) simp_all

@@ -129,96 +129,96 @@
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
qed simp

assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
-  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
+  shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
using assms by (induct xs) auto

-  "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
+  "distinct xs \<Longrightarrow> sum_list xs = Setsum (set xs)"
by (induct xs) simp_all

-lemma listsum_upt[simp]:
-  "m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}"
+lemma sum_list_upt[simp]:
+  "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"

-lemma listsum_eq_0_nat_iff_nat [simp]:
-  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
+lemma sum_list_eq_0_nat_iff_nat [simp]:
+  "sum_list ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
by (induct ns) simp_all

-lemma member_le_listsum_nat:
-  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
+lemma member_le_sum_list_nat:
+  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns"
by (induct ns) auto

-lemma elem_le_listsum_nat:
-  "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
-  by (rule member_le_listsum_nat) simp
+lemma elem_le_sum_list_nat:
+  "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns::nat list)"
+  by (rule member_le_sum_list_nat) simp

-lemma listsum_update_nat:
-  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
+lemma sum_list_update_nat:
+  "k < size ns \<Longrightarrow> sum_list (ns[k := (n::nat)]) = sum_list ns + n - ns ! k"
apply(induct ns arbitrary:k)
apply (auto split:nat.split)
-apply(drule elem_le_listsum_nat)
+apply(drule elem_le_sum_list_nat)
apply arith
done

"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
by (induct xs) (simp_all add: distrib_right)

"(\<Sum>x\<leftarrow>xs. 0) = 0"
by (induct xs) (simp_all add: distrib_right)

text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
-  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
+  "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)"
by (induct xs) simp_all

-  "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+  "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)

-  "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+  "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)

-lemma (in semiring_0) listsum_const_mult:
+lemma (in semiring_0) sum_list_const_mult:
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
by (induct xs) (simp_all add: algebra_simps)

-lemma (in semiring_0) listsum_mult_const:
+lemma (in semiring_0) sum_list_mult_const:
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
by (induct xs) (simp_all add: algebra_simps)

-  "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+  "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)"
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])

-lemma listsum_mono:
+lemma sum_list_mono:
shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"

-  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
+  "distinct xs \<Longrightarrow> sum_list (map f xs) = setsum f (set xs)"
by (induct xs) simp_all

-  "listsum (map f [m..<n]) = setsum f (set [m..<n])"
+  "sum_list (map f [m..<n]) = setsum f (set [m..<n])"

-  "listsum (map f [k..l]) = setsum f (set [k..l])"
+  "sum_list (map f [k..l]) = setsum f (set [k..l])"

-text \<open>General equivalence between @{const listsum} and @{const setsum}\<close>
-  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
-  using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
+text \<open>General equivalence between @{const sum_list} and @{const setsum}\<close>
+  "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
+  using interv_sum_list_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)

-lemma listsum_map_eq_setsum_count:
-  "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
+lemma sum_list_map_eq_setsum_count:
+  "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
proof(induction xs)
case (Cons x xs)
show ?case (is "?l = ?r")
@@ -236,9 +236,9 @@
qed
qed simp

-lemma listsum_map_eq_setsum_count2:
+lemma sum_list_map_eq_setsum_count2:
assumes "set xs \<subseteq> X" "finite X"
-shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
+shows "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
proof-
let ?F = "\<lambda>x. count_list xs x * f x"
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
@@ -246,23 +246,23 @@
also have "\<dots> = setsum ?F (set xs)"
using assms(2)
by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
-  finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
+  finally show ?thesis by(simp add:sum_list_map_eq_setsum_count)
qed

-lemma listsum_nonneg:
-    "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
+lemma sum_list_nonneg:
+    "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
by (induction xs) simp_all

-  "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
+  "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)"
by (induction xs) simp_all

-lemma listsum_cong [fundef_cong]:
+lemma sum_list_cong [fundef_cong]:
assumes "xs = ys"
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
-  shows    "listsum (map f xs) = listsum (map g ys)"
+  shows    "sum_list (map f xs) = sum_list (map g ys)"
proof -
-  from assms(2) have "listsum (map f xs) = listsum (map g xs)"
+  from assms(2) have "sum_list (map f xs) = sum_list (map g xs)"
by (induction xs) simp_all
with assms(1) show ?thesis by simp
qed
@@ -271,7 +271,7 @@
subsection \<open>Further facts about @{const List.n_lists}\<close>

lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
-  by (induct n) (auto simp add: comp_def length_concat listsum_triv)
+  by (induct n) (auto simp add: comp_def length_concat sum_list_triv)

lemma distinct_n_lists:
assumes "distinct xs"
@@ -300,20 +300,20 @@

lemmas setsum_code = setsum.set_conv_list

-lemma setsum_set_upto_conv_listsum_int [code_unfold]:
-  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
+lemma setsum_set_upto_conv_sum_list_int [code_unfold]:
+  "setsum f (set [i..j::int]) = sum_list (map f [i..j])"

-lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
-  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
+lemma setsum_set_upt_conv_sum_list_nat [code_unfold]:
+  "setsum f (set [m..<n]) = sum_list (map f [m..<n])"

-lemma listsum_transfer[transfer_rule]:
+lemma sum_list_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "A 0 0"
assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
-  shows "(list_all2 A ===> A) listsum listsum"
-  unfolding listsum.eq_foldr [abs_def]
+  shows "(list_all2 A ===> A) sum_list sum_list"
+  unfolding sum_list.eq_foldr [abs_def]
by transfer_prover

@@ -322,58 +322,58 @@
context monoid_mult
begin

-sublocale listprod: monoid_list times 1
+sublocale prod_list: monoid_list times 1
defines
-  listprod = listprod.F ..
+  prod_list = prod_list.F ..

end

context comm_monoid_mult
begin

-sublocale listprod: comm_monoid_list times 1
+sublocale prod_list: comm_monoid_list times 1
rewrites
-  "monoid_list.F times 1 = listprod"
+  "monoid_list.F times 1 = prod_list"
proof -
show "comm_monoid_list times 1" ..
-  then interpret listprod: comm_monoid_list times 1 .
-  from listprod_def show "monoid_list.F times 1 = listprod" by simp
+  then interpret prod_list: comm_monoid_list times 1 .
+  from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
qed

sublocale setprod: comm_monoid_list_set times 1
rewrites
-  "monoid_list.F times 1 = listprod"
+  "monoid_list.F times 1 = prod_list"
and "comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_list_set times 1" ..
then interpret setprod: comm_monoid_list_set times 1 .
-  from listprod_def show "monoid_list.F times 1 = listprod" by simp
+  from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
qed

end

-lemma listprod_cong [fundef_cong]:
+lemma prod_list_cong [fundef_cong]:
assumes "xs = ys"
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
-  shows    "listprod (map f xs) = listprod (map g ys)"
+  shows    "prod_list (map f xs) = prod_list (map g ys)"
proof -
-  from assms(2) have "listprod (map f xs) = listprod (map g xs)"
+  from assms(2) have "prod_list (map f xs) = prod_list (map g xs)"
by (induction xs) simp_all
with assms(1) show ?thesis by simp
qed

-lemma listprod_zero_iff:
-  "listprod xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
+lemma prod_list_zero_iff:
+  "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
by (induction xs) simp_all

text \<open>Some syntactic sugar:\<close>

syntax (ASCII)
-  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
+  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax
-  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
-  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)"
+  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"

end```
```--- a/src/HOL/IMP/Abs_Int0.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -329,14 +329,14 @@
by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)

definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
-"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
+"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"

text{* Upper complexity bound: *}
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
-    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
+    by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
@@ -455,7 +455,7 @@
< (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
-    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
+    by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed

end```
```--- a/src/HOL/IMP/Abs_Int1.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -118,14 +118,14 @@
by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)

definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
-"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
+"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"

text{* Upper complexity bound: *}
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
-    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
+    by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
@@ -239,7 +239,7 @@
< (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
-    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
+    by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed

end```
```--- a/src/HOL/IMP/Abs_Int3.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -390,7 +390,7 @@
lemma m_c_widen:
"strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
\<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
-apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
+apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]sum_list_setsum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
@@ -437,7 +437,7 @@

definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
-"n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
+"n\<^sub>c C = sum_list (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"

lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
@@ -446,7 +446,7 @@
lemma n_c_narrow: "strip C1 = strip C2
\<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
\<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1"
-apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth)
+apply(auto simp: n_c_def narrow_acom_def sum_list_setsum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)```
```--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -951,16 +951,16 @@
lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)

-lemma listsum_ennreal[simp]:
+lemma sum_list_ennreal[simp]:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
-  shows   "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
+  shows   "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
using assms
proof (induction xs)
case (Cons x xs)
-  from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))"
+  from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
by simp
-  also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))"
-    by (intro ennreal_plus [symmetric] listsum_nonneg) auto
+  also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
+    by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
finally show ?case by simp
qed simp_all
```
```--- a/src/HOL/Library/Extended_Real.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -771,7 +771,7 @@
then show ?thesis by simp
qed

-lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
+lemma sum_list_ereal [simp]: "sum_list (map (\<lambda>x. ereal (f x)) xs) = ereal (sum_list (map f xs))"
by (induction xs) simp_all

lemma setsum_Pinfty:```
```--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -2107,7 +2107,7 @@
subsubsection \<open>Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
finite product of FPS, also the relvant instance of powers of a FPS\<close>

-definition "natpermute n k = {l :: nat list. length l = k \<and> listsum l = n}"
+definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"

lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
@@ -2117,14 +2117,14 @@

lemma append_natpermute_less_eq:
assumes "xs @ ys \<in> natpermute n k"
-  shows "listsum xs \<le> n"
-    and "listsum ys \<le> n"
+  shows "sum_list xs \<le> n"
+    and "sum_list ys \<le> n"
proof -
-  from assms have "listsum (xs @ ys) = n"
+  from assms have "sum_list (xs @ ys) = n"
-  then have "listsum xs + listsum ys = n"
+  then have "sum_list xs + sum_list ys = n"
by simp
-  then show "listsum xs \<le> n" and "listsum ys \<le> n"
+  then show "sum_list xs \<le> n" and "sum_list ys \<le> n"
by simp_all
qed

@@ -2142,9 +2142,9 @@
and xs: "xs \<in> natpermute m h"
and ys: "ys \<in> natpermute (n - m) (k - h)"
and leq: "l = xs@ys" by blast
-    from xs have xs': "listsum xs = m"
+    from xs have xs': "sum_list xs = m"
-    from ys have ys': "listsum ys = n - m"
+    from ys have ys': "sum_list ys = n - m"
show "l \<in> ?L" using leq xs ys h
@@ -2160,12 +2160,12 @@
assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
let ?ys = "drop h l"
-    let ?m = "listsum ?xs"
-    from l have ls: "listsum (?xs @ ?ys) = n"
+    let ?m = "sum_list ?xs"
+    from l have ls: "sum_list (?xs @ ?ys) = n"
have xs: "?xs \<in> natpermute ?m h" using l assms
-    have l_take_drop: "listsum l = listsum (take h l @ drop h l)"
+    have l_take_drop: "sum_list l = sum_list (take h l @ drop h l)"
by simp
then have ys: "?ys \<in> natpermute (n - ?m) (k - h)"
using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
@@ -2230,7 +2230,7 @@
using i by auto
from H have "n = setsum (nth xs) {0..k}"
-      apply (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth)
+      apply (auto simp add: atLeastLessThanSuc_atLeastAtMost sum_list_setsum_nth)
done
also have "\<dots> = n + setsum (nth xs) ({0..k} - {i})"
unfolding setsum.union_disjoint[OF f d, unfolded eqs] using i by simp
@@ -2265,8 +2265,8 @@
done
have xsl: "length xs = k + 1"
by (simp only: xs length_replicate length_list_update)
-    have "listsum xs = setsum (nth xs) {0..<k+1}"
-      unfolding listsum_setsum_nth xsl ..
+    have "sum_list xs = setsum (nth xs) {0..<k+1}"
+      unfolding sum_list_setsum_nth xsl ..
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
by (rule setsum.cong) (simp_all add: xs del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum.delta)
@@ -2421,9 +2421,9 @@
by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
then guess j by (elim exE conjE) note j = this

-    from v have "k = listsum v" by (simp add: A_def natpermute_def)
+    from v have "k = sum_list v" by (simp add: A_def natpermute_def)
also have "\<dots> = (\<Sum>i=0..m. v ! i)"
-      by (simp add: listsum_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
+      by (simp add: sum_list_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
also from j have "{0..m} = insert j ({0..m}-{j})" by auto
also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
by (subst setsum.insert) simp_all
@@ -2469,7 +2469,7 @@
g \$ k * (of_nat (Suc m) * (f \$ 0) ^ m) + ?h g" using assms
by (simp add: mult_ac del: power_Suc of_nat_Suc)
also have "v ! i < k" if "v \<in> {v\<in>natpermute k (m+1). k \<notin> set v}" "i \<le> m" for v i
-        using that elem_le_listsum_nat[of i v] unfolding natpermute_def
+        using that elem_le_sum_list_nat[of i v] unfolding natpermute_def
by (auto simp: set_conv_nth dest!: spec[of _ i])
hence "?h f = ?h g"
by (intro setsum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
@@ -2599,10 +2599,10 @@
by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
using i by auto
-      from xs have "Suc n = listsum xs"
+      from xs have "Suc n = sum_list xs"
also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
-        by (simp add: natpermute_def listsum_setsum_nth)
+        by (simp add: natpermute_def sum_list_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs  setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
@@ -2853,10 +2853,10 @@
by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
using i by auto
-            from xs have "n = listsum xs"
+            from xs have "n = sum_list xs"
also have "\<dots> = setsum (nth xs) {0..<Suc k}"
-              using xs by (simp add: natpermute_def listsum_setsum_nth)
+              using xs by (simp add: natpermute_def sum_list_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs  setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]```
```--- a/src/HOL/Library/ListVector.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/ListVector.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -119,7 +119,7 @@
done

lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
-by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
+by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)

lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
apply(induct xs arbitrary: ys zs)```
```--- a/src/HOL/Library/Multiset.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -3188,7 +3188,7 @@

end

-lemma [code]: "sum_mset (mset xs) = listsum xs"
+lemma [code]: "sum_mset (mset xs) = sum_list xs"
by (induct xs) simp_all

lemma [code]: "prod_mset (mset xs) = fold times xs 1"```
```--- a/src/HOL/Library/Polynomial.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -2946,7 +2946,7 @@

-lemma coeff_0_listprod: "coeff (listprod xs) 0 = listprod (map (\<lambda>p. coeff p 0) xs)"
+lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
by (induction xs) (simp_all add: coeff_mult)

lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
@@ -3214,9 +3214,9 @@
setprod (\<lambda>x. reflect_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)

-lemma reflect_poly_listprod:
-  "reflect_poly (listprod (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) =
-     listprod (map reflect_poly xs)"
+lemma reflect_poly_prod_list:
+  "reflect_poly (prod_list (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) =
+     prod_list (map reflect_poly xs)"
by (induction xs) (simp_all add: reflect_poly_mult)

lemma reflect_poly_Poly_nz:
@@ -3225,7 +3225,7 @@

lemmas reflect_poly_simps =
reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
-  reflect_poly_power reflect_poly_setprod reflect_poly_listprod
+  reflect_poly_power reflect_poly_setprod reflect_poly_prod_list

subsection \<open>Derivatives of univariate polynomials\<close>```
```--- a/src/HOL/Library/Polynomial_FPS.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Library/Polynomial_FPS.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -64,13 +64,13 @@
lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\<lambda>x. fps_of_poly (f x)) A"

-lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)"
+lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"

lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)

-lemma fps_of_poly_listprod: "fps_of_poly (listprod xs) = listprod (map fps_of_poly xs)"
+lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
by (induction xs) (simp_all add: fps_of_poly_mult)

lemma fps_of_poly_pCons:
@@ -144,7 +144,7 @@
lemmas fps_of_poly_simps =
fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
-  fps_of_poly_setsum fps_of_poly_listsum fps_of_poly_setprod fps_of_poly_listprod
+  fps_of_poly_setsum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
fps_of_poly_divide_numeral
```
```--- a/src/HOL/Nitpick.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Nitpick.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -73,7 +73,7 @@
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"

definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
-  "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+  "setsum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"

inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |```
```--- a/src/HOL/Nominal/Examples/Standardization.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -213,8 +213,8 @@
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
-    apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
-    apply (fastforce simp add: listsum_map_remove1)
+    apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+    apply (fastforce simp add: sum_list_map_remove1)
apply clarify
apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
prefer 2
@@ -235,8 +235,8 @@
prefer 2
apply blast
apply simp
-  apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
-  apply (fastforce simp add: listsum_map_remove1)
+  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+  apply (fastforce simp add: sum_list_map_remove1)
done

theorem Apps_lam_induct:```
```--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -306,14 +306,14 @@
lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
by (auto simp: sparsify_def set_zip)

-lemma listsum_sparsify[simp]:
+lemma sum_list_sparsify[simp]:
fixes v :: "('a :: semiring_0) list"
assumes "length w = length v"
shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
(is "(\<Sum>x\<leftarrow>_. ?f x) = _")
unfolding sparsify_def scalar_product_def
-  using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
+  using assms sum_list_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
*)
definition [simp]: "unzip w = (map fst w, map snd w)"

@@ -338,7 +338,7 @@
"jad = apsnd transpose o length_permutate o map sparsify"

definition
-  "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
+  "jad_mv v = inflate o case_prod zip o apsnd (map sum_list o transpose o map (map (\<lambda> (i, x). v ! i * x)))"

lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
quickcheck[tester = smart_exhaustive, size = 6]```
```--- a/src/HOL/Probability/PMF_Impl.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Probability/PMF_Impl.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -396,10 +396,10 @@

lemma mapping_of_pmf_pmf_of_list:
-  assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "listsum (map snd xs) = 1"
+  assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "sum_list (map snd xs) = 1"
shows   "mapping_of_pmf (pmf_of_list xs) =
Mapping.tabulate (remdups (map fst xs))
-               (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+               (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
proof -
from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force
with assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
@@ -413,7 +413,7 @@
defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
shows   "mapping_of_pmf (pmf_of_list xs) =
Mapping.tabulate (remdups (map fst xs'))
-               (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs")
+               (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs")
proof -
have wf: "pmf_of_list_wf xs'" unfolding xs'_def by (rule pmf_of_list_remove_zeros) fact
have pos: "\<forall>x\<in>snd`set xs'. x > 0" using assms(1) unfolding xs'_def
@@ -426,7 +426,7 @@
qed

lemma pmf_of_list_wf_code [code]:
-  "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> listsum (map snd xs) = 1"
+  "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> sum_list (map snd xs) = 1"
by (auto simp add: pmf_of_list_wf_def list_all_def)

lemma pmf_of_list_code [code abstract]:
@@ -434,7 +434,7 @@
if pmf_of_list_wf xs then
let xs' = filter (\<lambda>z. snd z \<noteq> 0) xs
in  Mapping.tabulate (remdups (map fst xs'))
-             (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))
+             (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))
else
Code.abort (STR ''Invalid list for pmf_of_list'') (\<lambda>_. mapping_of_pmf (pmf_of_list xs)))"
using mapping_of_pmf_pmf_of_list'[of xs] by (simp add: Let_def)```
```--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -1843,13 +1843,13 @@
subsection \<open>PMFs from assiciation lists\<close>

definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
-  "pmf_of_list xs = embed_pmf (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+  "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"

definition pmf_of_list_wf where
-  "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> listsum (map snd xs) = 1"
+  "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> sum_list (map snd xs) = 1"

lemma pmf_of_list_wfI:
-  "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
+  "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> sum_list (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
unfolding pmf_of_list_wf_def by simp

context
@@ -1857,12 +1857,12 @@

private lemma pmf_of_list_aux:
assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
-  assumes "listsum (map snd xs) = 1"
-  shows "(\<integral>\<^sup>+ x. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
+  assumes "sum_list (map snd xs) = 1"
+  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
proof -
-  have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
-            (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
-    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter') (auto intro: listsum_cong)
+  have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
+            (\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
+    by (intro nn_integral_cong ennreal_cong, subst sum_list_map_filter') (auto intro: sum_list_cong)
also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
using assms(1)
proof (induction xs)
@@ -1874,11 +1874,11 @@
(\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
by (intro nn_integral_cong, subst ennreal_plus [symmetric])
-         (auto simp: case_prod_unfold indicator_def intro!: listsum_nonneg)
+         (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
-         (force intro!: listsum_nonneg AE_I2 intro: Cons simp: indicator_def)+
+         (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
also have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV) =
(\<Sum>(x', p)\<leftarrow>xs. (\<integral>\<^sup>+ y. ennreal (indicator {x'} y * p) \<partial>count_space UNIV))"
using Cons(1) by (intro Cons) simp_all
@@ -1886,19 +1886,19 @@
qed simp
also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
using assms(1)
-    by (intro listsum_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
+    by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
(auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
simp del: times_ereal.simps)+
-  also from assms have "\<dots> = listsum (map snd xs)" by (simp add: case_prod_unfold listsum_ennreal)
+  also from assms have "\<dots> = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal)
also have "\<dots> = 1" using assms(2) by simp
finally show ?thesis .
qed

lemma pmf_pmf_of_list:
assumes "pmf_of_list_wf xs"
-  shows   "pmf (pmf_of_list xs) x = listsum (map snd (filter (\<lambda>z. fst z = x) xs))"
+  shows   "pmf (pmf_of_list xs) x = sum_list (map snd (filter (\<lambda>z. fst z = x) xs))"
using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def
-  by (subst pmf_embed_pmf) (auto intro!: listsum_nonneg)
+  by (subst pmf_embed_pmf) (auto intro!: sum_list_nonneg)

end

@@ -1930,16 +1930,16 @@

lemma emeasure_pmf_of_list:
assumes "pmf_of_list_wf xs"
-  shows   "emeasure (pmf_of_list xs) A = ennreal (listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
+  shows   "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
proof -
have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
by simp
also from assms
-    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])))"
+    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
also from assms
-    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. listsum (map snd [z\<leftarrow>xs . fst z = x]))"
-    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: listsum_nonneg)
+    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
+    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
@@ -1948,13 +1948,13 @@
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
-                      listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+                      sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
using assms by (simp add: pmf_pmf_of_list)
-  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). listsum (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
+  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
by (intro setsum.cong) (auto simp: indicator_def)
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
-    by (intro setsum.cong refl, subst listsum_map_filter', subst listsum_setsum_nth) simp
+    by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
by (rule setsum.commute)
@@ -1963,30 +1963,30 @@
by (auto intro!: setsum.cong setsum.neutral)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
by (intro setsum.cong refl) (simp_all add: setsum.delta)
-  also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
-    by (subst listsum_map_filter', subst listsum_setsum_nth) simp_all
+  also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+    by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
finally show ?thesis .
qed

lemma measure_pmf_of_list:
assumes "pmf_of_list_wf xs"
-  shows   "measure (pmf_of_list xs) A = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+  shows   "measure (pmf_of_list xs) A = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
-  by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
+  by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: sum_list_nonneg)

(* TODO Move? *)
-lemma listsum_nonneg_eq_zero_iff:
+lemma sum_list_nonneg_eq_zero_iff:
fixes xs :: "'a :: linordered_ab_group_add list"
-  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
+  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
proof (induction xs)
case (Cons x xs)
-  from Cons.prems have "listsum (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> listsum xs = 0"
-    unfolding listsum_simps by (subst add_nonneg_eq_0_iff) (auto intro: listsum_nonneg)
+  from Cons.prems have "sum_list (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> sum_list xs = 0"
+    unfolding sum_list_simps by (subst add_nonneg_eq_0_iff) (auto intro: sum_list_nonneg)
with Cons.IH Cons.prems show ?case by simp
qed simp_all

-lemma listsum_filter_nonzero:
-  "listsum (filter (\<lambda>x. x \<noteq> 0) xs) = listsum xs"
+lemma sum_list_filter_nonzero:
+  "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
by (induction xs) simp_all
(* END MOVE *)

@@ -1997,11 +1997,11 @@
{
fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
then obtain y where y: "(x, y) \<in> set xs" by auto
-    from B have "listsum (map snd [z\<leftarrow>xs. fst z = x]) = 0"
+    from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
ultimately have "y = 0" using assms(1)
-      by (subst (asm) listsum_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
+      by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
with assms(2) y have False by force
}
thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
@@ -2015,8 +2015,8 @@
have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
by (induction xs) simp_all
with assms(1) show wf: "pmf_of_list_wf xs'"
-    by (auto simp: pmf_of_list_wf_def xs'_def listsum_filter_nonzero)
-  have "listsum (map snd [z\<leftarrow>xs' . fst z = i]) = listsum (map snd [z\<leftarrow>xs . fst z = i])" for i
+    by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
+  have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
unfolding xs'_def by (induction xs) simp_all
with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)```
```--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -110,8 +110,8 @@
prefer 2
apply (erule allE, erule mp, rule refl)
apply simp
-   apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
-   apply (fastforce simp add: listsum_map_remove1)
+   apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+   apply (fastforce simp add: sum_list_map_remove1)
apply clarify
apply (rule assms)
apply (erule allE, erule impE)
@@ -126,8 +126,8 @@
apply (rule le_imp_less_Suc)
-  apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
+  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
done

theorem Apps_dB_induct:```
```--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -204,7 +204,7 @@
oops

lemma
-  "ns ! k < length ns ==> k <= listsum ns"
+  "ns ! k < length ns ==> k <= sum_list ns"
quickcheck[random, iterations = 10000, finite_types = false, quiet]
quickcheck[exhaustive, finite_types = false, expect = counterexample]
oops```
```--- a/src/HOL/Random.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/Random.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -79,7 +79,7 @@
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"

lemma pick_member:
-  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
+  "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
by (induct xs arbitrary: i) (simp_all add: less_natural_def)

lemma pick_drop_zero:
@@ -95,17 +95,17 @@
qed

definition select_weight :: "(natural \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  "select_weight xs = range (listsum (map fst xs))
+  "select_weight xs = range (sum_list (map fst xs))
\<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"

lemma select_weight_member:
-  assumes "0 < listsum (map fst xs)"
+  assumes "0 < sum_list (map fst xs)"
shows "fst (select_weight xs s) \<in> set (map snd xs)"
proof -
from range assms
-    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
+    have "fst (range (sum_list (map fst xs)) s) < sum_list (map fst xs)" .
with pick_member
-    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
+    have "pick xs (fst (range (sum_list (map fst xs)) s)) \<in> set (map snd xs)" .
then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed

@@ -116,7 +116,7 @@
lemma select_weight_drop_zero:
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
-  have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
+  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
@@ -127,7 +127,7 @@
proof -
have less: "\<And>s. fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)"
using assms by (intro range) (simp add: less_natural_def)
-  moreover have "listsum (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
+  moreover have "sum_list (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
by (induct xs) simp_all
ultimately show ?thesis
by (auto simp add: select_weight_def select_def scomp_def split_def```
```--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -14,7 +14,7 @@

abbreviation (input) tokens :: "nat list \<Rightarrow> nat"
where
-  "tokens \<equiv> listsum"
+  "tokens \<equiv> sum_list"

abbreviation (input)
"bag_of \<equiv> mset"```
```--- a/src/HOL/ex/Gauge_Integration.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -204,7 +204,7 @@
ultimately show ?case by simp
qed auto

-lemma fine_listsum_eq_diff:
+lemma fine_sum_list_eq_diff:
fixes f :: "real \<Rightarrow> real"
shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
by (induct set: fine) simp_all
@@ -249,7 +249,7 @@
by (induct D, auto simp add: algebra_simps)

lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
-unfolding rsum_def map_append listsum_append ..
+unfolding rsum_def map_append sum_list_append ..

subsection \<open>Gauge integrability (definite)\<close>
@@ -594,22 +594,22 @@
proof (clarify)
fix D assume D: "fine \<delta> (a, b) D"
hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
-        by (rule fine_listsum_eq_diff)
+        by (rule fine_sum_list_eq_diff)
hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
by simp
also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
by (rule abs_minus_commute)
also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
-        by (simp only: rsum_def listsum_subtractf split_def)
+        by (simp only: rsum_def sum_list_subtractf split_def)
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
-        by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
+        by (rule ord_le_eq_trans [OF sum_list_abs], simp add: o_def split_def)
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
-        apply (rule listsum_mono, clarify, rename_tac u x v)
+        apply (rule sum_list_mono, clarify, rename_tac u x v)
using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
done
also have "\<dots> = e"
-        using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
-        unfolding split_def listsum_const_mult
+        using fine_sum_list_eq_diff [OF D, where f="\<lambda>x. x"]
+        unfolding split_def sum_list_const_mult
using \<open>a < b\<close> by simp
finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
qed```
```--- a/src/HOL/ex/Parallel_Example.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/ex/Parallel_Example.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -9,7 +9,7 @@
subsubsection \<open>Fragments of the harmonic series\<close>

definition harmonic :: "nat \<Rightarrow> rat" where
-  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
+  "harmonic n = sum_list (map (\<lambda>n. 1 / of_nat n) [1..<n])"

subsubsection \<open>The sieve of Erathostenes\<close>```
```--- a/src/HOL/ex/Perm_Fragments.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -11,8 +11,8 @@

text \<open>On cycles\<close>

-lemma cycle_listprod:
-  "\<langle>a # as\<rangle> = listprod (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
+lemma cycle_prod_list:
+  "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
by (induct as) simp_all

lemma cycle_append [simp]:```
```--- a/src/HOL/ex/Primrec.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/ex/Primrec.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -224,16 +224,16 @@

text \<open>MAIN RESULT\<close>

-lemma SC_case: "SC l < ack 1 (listsum l)"
+lemma SC_case: "SC l < ack 1 (sum_list l)"
apply (unfold SC_def)
apply (induct l)
done

-lemma CONSTANT_case: "CONSTANT k l < ack k (listsum l)"
+lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)"
by simp

-lemma PROJ_case: "PROJ i l < ack 0 (listsum l)"
+lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)"
apply (induct l arbitrary:i)
apply (auto simp add: drop_Cons split: nat.split)
@@ -243,8 +243,8 @@

text \<open>@{term COMP} case\<close>

-lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
-  ==> \<exists>k. \<forall>l. listsum (map (\<lambda>f. f l) fs) < ack k (listsum l)"
+lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
+  ==> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)"
apply (induct fs)
apply (rule_tac x = 0 in exI)
apply simp
@@ -253,9 +253,9 @@
done

lemma COMP_case:
-  "\<forall>l. g l < ack kg (listsum l) ==>
-  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
-  ==> \<exists>k. \<forall>l. COMP g fs  l < ack k (listsum l)"
+  "\<forall>l. g l < ack kg (sum_list l) ==>
+  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
+  ==> \<exists>k. \<forall>l. COMP g fs  l < ack k (sum_list l)"
apply (unfold COMP_def)
apply (drule COMP_map_aux)
apply (meson ack_less_mono2 ack_nest_bound less_trans)
@@ -265,9 +265,9 @@
text \<open>@{term PREC} case\<close>

lemma PREC_case_aux:
-  "\<forall>l. f l + listsum l < ack kf (listsum l) ==>
-    \<forall>l. g l + listsum l < ack kg (listsum l) ==>
-    PREC f g l + listsum l < ack (Suc (kf + kg)) (listsum l)"
+  "\<forall>l. f l + sum_list l < ack kf (sum_list l) ==>
+    \<forall>l. g l + sum_list l < ack kg (sum_list l) ==>
+    PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)"
apply (unfold PREC_def)
apply (case_tac l)
apply simp_all
@@ -290,12 +290,12 @@
done

lemma PREC_case:
-  "\<forall>l. f l < ack kf (listsum l) ==>
-    \<forall>l. g l < ack kg (listsum l) ==>
-    \<exists>k. \<forall>l. PREC f g l < ack k (listsum l)"
+  "\<forall>l. f l < ack kf (sum_list l) ==>
+    \<forall>l. g l < ack kg (sum_list l) ==>
+    \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)"

-lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (listsum l)"
+lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (sum_list l)"
apply (erule PRIMREC.induct)
apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
done```
```--- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Sep 15 15:48:37 2016 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Sep 15 17:05:34 2016 +0200
@@ -116,7 +116,7 @@
text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
method to help generate transfer rules.\<close>

-lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
+lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list"
by transfer_prover

end
@@ -178,8 +178,8 @@

lemma
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
-    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
-  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+    sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+  shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
apply transfer
apply fact
done
@@ -189,8 +189,8 @@

lemma
assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
-    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
-  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
+    (sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs"
+  shows "sum_list xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
apply transfer
apply fact
done
@@ -200,8 +200,8 @@

lemma
assumes "\<And>xs::int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
-    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
-  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
+    sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)"
+  shows "xs \<noteq> [] \<Longrightarrow> sum_list xs < sum_list (map Suc xs)"
apply transfer
apply fact
done```