renamed listsum -> sum_list, listprod ~> prod_list
authornipkow
Thu Sep 15 11:48:20 2016 +0200 (2016-09-15)
changeset 63882018998c00003
parent 63876 fd73c5dbaad2
child 63883 41b5d9f3778a
renamed listsum -> sum_list, listprod ~> prod_list
NEWS
src/HOL/Binomial.thy
src/HOL/GCD.thy
src/HOL/Groups_List.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_FPS.thy
src/HOL/Nitpick.thy
src/HOL/Nominal/Examples/Standardization.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Probability/PMF_Impl.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Proofs/Lambda/ListApplication.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Random.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/ex/Gauge_Integration.thy
src/HOL/ex/Parallel_Example.thy
src/HOL/ex/Perm_Fragments.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Wed Sep 14 22:07:11 2016 +0200
     1.2 +++ b/NEWS	Thu Sep 15 11:48:20 2016 +0200
     1.3 @@ -251,6 +251,10 @@
     1.4  * Theory Set_Interval.thy: substantial new theorems on indexed sums
     1.5  and products.
     1.6  
     1.7 +* Theory List.thy:
     1.8 +  listsum ~> sum_list
     1.9 +  listprod ~> prod_list
    1.10 +
    1.11  * Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
    1.12  equations in functional programming style: variables present on the
    1.13  left-hand but not on the righ-hand side are replaced by underscores.
     2.1 --- a/src/HOL/Binomial.thy	Wed Sep 14 22:07:11 2016 +0200
     2.2 +++ b/src/HOL/Binomial.thy	Thu Sep 15 11:48:20 2016 +0200
     2.3 @@ -1521,28 +1521,28 @@
     2.4  qed
     2.5  
     2.6  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>
     2.7 -lemma card_length_listsum_rec:
     2.8 +lemma card_length_sum_list_rec:
     2.9    assumes "m \<ge> 1"
    2.10 -  shows "card {l::nat list. length l = m \<and> listsum l = N} =
    2.11 -      card {l. length l = (m - 1) \<and> listsum l = N} +
    2.12 -      card {l. length l = m \<and> listsum l + 1 = N}"
    2.13 +  shows "card {l::nat list. length l = m \<and> sum_list l = N} =
    2.14 +      card {l. length l = (m - 1) \<and> sum_list l = N} +
    2.15 +      card {l. length l = m \<and> sum_list l + 1 = N}"
    2.16      (is "card ?C = card ?A + card ?B")
    2.17  proof -
    2.18 -  let ?A' = "{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
    2.19 -  let ?B' = "{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
    2.20 +  let ?A' = "{l. length l = m \<and> sum_list l = N \<and> hd l = 0}"
    2.21 +  let ?B' = "{l. length l = m \<and> sum_list l = N \<and> hd l \<noteq> 0}"
    2.22    let ?f = "\<lambda>l. 0 # l"
    2.23    let ?g = "\<lambda>l. (hd l + 1) # tl l"
    2.24    have 1: "xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" for x xs
    2.25      by simp
    2.26 -  have 2: "xs \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs" for xs :: "nat list"
    2.27 +  have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
    2.28      by (auto simp add: neq_Nil_conv)
    2.29    have f: "bij_betw ?f ?A ?A'"
    2.30      apply (rule bij_betw_byWitness[where f' = tl])
    2.31      using assms
    2.32      apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
    2.33      done
    2.34 -  have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs" for xs :: "nat list"
    2.35 -    by (metis 1 listsum_simps(2) 2)
    2.36 +  have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
    2.37 +    by (metis 1 sum_list_simps(2) 2)
    2.38    have g: "bij_betw ?g ?B ?B'"
    2.39      apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
    2.40      using assms
    2.41 @@ -1552,10 +1552,10 @@
    2.42      using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
    2.43    have fin_A: "finite ?A" using fin[of _ "N+1"]
    2.44      by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"])
    2.45 -      (auto simp: member_le_listsum_nat less_Suc_eq_le)
    2.46 +      (auto simp: member_le_sum_list_nat less_Suc_eq_le)
    2.47    have fin_B: "finite ?B"
    2.48      by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"])
    2.49 -      (auto simp: member_le_listsum_nat less_Suc_eq_le fin)
    2.50 +      (auto simp: member_le_sum_list_nat less_Suc_eq_le fin)
    2.51    have uni: "?C = ?A' \<union> ?B'"
    2.52      by auto
    2.53    have disj: "?A' \<inter> ?B' = {}"
    2.54 @@ -1569,7 +1569,7 @@
    2.55    finally show ?thesis .
    2.56  qed
    2.57  
    2.58 -lemma card_length_listsum: "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
    2.59 +lemma card_length_sum_list: "card {l::nat list. size l = m \<and> sum_list l = N} = (N + m - 1) choose N"
    2.60    \<comment> "by Holden Lee, tidied by Tobias Nipkow"
    2.61  proof (cases m)
    2.62    case 0
    2.63 @@ -1590,7 +1590,7 @@
    2.64        by simp
    2.65    next
    2.66      case (Suc k)
    2.67 -    have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} = (N + (m - 1) - 1) choose N"
    2.68 +    have c1: "card {l::nat list. size l = (m - 1) \<and> sum_list l =  N} = (N + (m - 1) - 1) choose N"
    2.69      proof (cases "m = 1")
    2.70        case True
    2.71        with Suc.hyps have "N \<ge> 1"
    2.72 @@ -1602,23 +1602,23 @@
    2.73        then show ?thesis
    2.74          using Suc by fastforce
    2.75      qed
    2.76 -    from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
    2.77 +    from Suc have c2: "card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
    2.78        (if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
    2.79      proof -
    2.80        have *: "n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" for m n
    2.81          by arith
    2.82        from Suc have "N > 0 \<Longrightarrow>
    2.83 -        card {l::nat list. size l = m \<and> listsum l + 1 = N} =
    2.84 +        card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
    2.85            ((N - 1) + m - 1) choose (N - 1)"
    2.86          by (simp add: *)
    2.87        then show ?thesis
    2.88          by auto
    2.89      qed
    2.90 -    from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
    2.91 -          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
    2.92 +    from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> sum_list l = N} +
    2.93 +          card {l::nat list. size l = m \<and> sum_list l + 1 = N}) = (N + m - 1) choose N"
    2.94        by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
    2.95      then show ?case
    2.96 -      using card_length_listsum_rec[OF Suc.prems] by auto
    2.97 +      using card_length_sum_list_rec[OF Suc.prems] by auto
    2.98    qed
    2.99  qed
   2.100  
     3.1 --- a/src/HOL/GCD.thy	Wed Sep 14 22:07:11 2016 +0200
     3.2 +++ b/src/HOL/GCD.thy	Thu Sep 15 11:48:20 2016 +0200
     3.3 @@ -865,7 +865,7 @@
     3.4      apply (auto simp add: gcd_mult_cancel)
     3.5    done
     3.6  
     3.7 -lemma listprod_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
     3.8 +lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
     3.9    by (induct xs) (simp_all add: gcd_mult_cancel)
    3.10  
    3.11  lemma coprime_divisors:
     4.1 --- a/src/HOL/Groups_List.thy	Wed Sep 14 22:07:11 2016 +0200
     4.2 +++ b/src/HOL/Groups_List.thy	Thu Sep 15 11:48:20 2016 +0200
     4.3 @@ -55,32 +55,32 @@
     4.4  context monoid_add
     4.5  begin
     4.6  
     4.7 -sublocale listsum: monoid_list plus 0
     4.8 +sublocale sum_list: monoid_list plus 0
     4.9  defines
    4.10 -  listsum = listsum.F ..
    4.11 +  sum_list = sum_list.F ..
    4.12   
    4.13  end
    4.14  
    4.15  context comm_monoid_add
    4.16  begin
    4.17  
    4.18 -sublocale listsum: comm_monoid_list plus 0
    4.19 +sublocale sum_list: comm_monoid_list plus 0
    4.20  rewrites
    4.21 -  "monoid_list.F plus 0 = listsum"
    4.22 +  "monoid_list.F plus 0 = sum_list"
    4.23  proof -
    4.24    show "comm_monoid_list plus 0" ..
    4.25 -  then interpret listsum: comm_monoid_list plus 0 .
    4.26 -  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    4.27 +  then interpret sum_list: comm_monoid_list plus 0 .
    4.28 +  from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
    4.29  qed
    4.30  
    4.31  sublocale setsum: comm_monoid_list_set plus 0
    4.32  rewrites
    4.33 -  "monoid_list.F plus 0 = listsum"
    4.34 +  "monoid_list.F plus 0 = sum_list"
    4.35    and "comm_monoid_set.F plus 0 = setsum"
    4.36  proof -
    4.37    show "comm_monoid_list_set plus 0" ..
    4.38    then interpret setsum: comm_monoid_list_set plus 0 .
    4.39 -  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    4.40 +  from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
    4.41    from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
    4.42  qed
    4.43  
    4.44 @@ -88,39 +88,39 @@
    4.45  
    4.46  text \<open>Some syntactic sugar for summing a function over a list:\<close>
    4.47  syntax (ASCII)
    4.48 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    4.49 +  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    4.50  syntax
    4.51 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.52 +  "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.53  translations \<comment> \<open>Beware of argument permutation!\<close>
    4.54 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)"
    4.55 +  "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
    4.56  
    4.57  text \<open>TODO duplicates\<close>
    4.58 -lemmas listsum_simps = listsum.Nil listsum.Cons
    4.59 -lemmas listsum_append = listsum.append
    4.60 -lemmas listsum_rev = listsum.rev
    4.61 +lemmas sum_list_simps = sum_list.Nil sum_list.Cons
    4.62 +lemmas sum_list_append = sum_list.append
    4.63 +lemmas sum_list_rev = sum_list.rev
    4.64  
    4.65 -lemma (in monoid_add) fold_plus_listsum_rev:
    4.66 -  "fold plus xs = plus (listsum (rev xs))"
    4.67 +lemma (in monoid_add) fold_plus_sum_list_rev:
    4.68 +  "fold plus xs = plus (sum_list (rev xs))"
    4.69  proof
    4.70    fix x
    4.71 -  have "fold plus xs x = listsum (rev xs @ [x])"
    4.72 -    by (simp add: foldr_conv_fold listsum.eq_foldr)
    4.73 -  also have "\<dots> = listsum (rev xs) + x"
    4.74 +  have "fold plus xs x = sum_list (rev xs @ [x])"
    4.75 +    by (simp add: foldr_conv_fold sum_list.eq_foldr)
    4.76 +  also have "\<dots> = sum_list (rev xs) + x"
    4.77      by simp
    4.78 -  finally show "fold plus xs x = listsum (rev xs) + x"
    4.79 +  finally show "fold plus xs x = sum_list (rev xs) + x"
    4.80      .
    4.81  qed
    4.82  
    4.83 -lemma (in comm_monoid_add) listsum_map_remove1:
    4.84 -  "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
    4.85 +lemma (in comm_monoid_add) sum_list_map_remove1:
    4.86 +  "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
    4.87    by (induct xs) (auto simp add: ac_simps)
    4.88  
    4.89 -lemma (in monoid_add) size_list_conv_listsum:
    4.90 -  "size_list f xs = listsum (map f xs) + size xs"
    4.91 +lemma (in monoid_add) size_list_conv_sum_list:
    4.92 +  "size_list f xs = sum_list (map f xs) + size xs"
    4.93    by (induct xs) auto
    4.94  
    4.95  lemma (in monoid_add) length_concat:
    4.96 -  "length (concat xss) = listsum (map length xss)"
    4.97 +  "length (concat xss) = sum_list (map length xss)"
    4.98    by (induct xss) simp_all
    4.99  
   4.100  lemma (in monoid_add) length_product_lists:
   4.101 @@ -129,96 +129,96 @@
   4.102    case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
   4.103  qed simp
   4.104  
   4.105 -lemma (in monoid_add) listsum_map_filter:
   4.106 +lemma (in monoid_add) sum_list_map_filter:
   4.107    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
   4.108 -  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
   4.109 +  shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
   4.110    using assms by (induct xs) auto
   4.111  
   4.112 -lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
   4.113 -  "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
   4.114 +lemma (in comm_monoid_add) distinct_sum_list_conv_Setsum:
   4.115 +  "distinct xs \<Longrightarrow> sum_list xs = Setsum (set xs)"
   4.116    by (induct xs) simp_all
   4.117  
   4.118 -lemma listsum_upt[simp]:
   4.119 -  "m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}"
   4.120 -by(simp add: distinct_listsum_conv_Setsum)
   4.121 +lemma sum_list_upt[simp]:
   4.122 +  "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
   4.123 +by(simp add: distinct_sum_list_conv_Setsum)
   4.124  
   4.125 -lemma listsum_eq_0_nat_iff_nat [simp]:
   4.126 -  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
   4.127 +lemma sum_list_eq_0_nat_iff_nat [simp]:
   4.128 +  "sum_list ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
   4.129    by (induct ns) simp_all
   4.130  
   4.131 -lemma member_le_listsum_nat:
   4.132 -  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
   4.133 +lemma member_le_sum_list_nat:
   4.134 +  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns"
   4.135    by (induct ns) auto
   4.136  
   4.137 -lemma elem_le_listsum_nat:
   4.138 -  "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
   4.139 -  by (rule member_le_listsum_nat) simp
   4.140 +lemma elem_le_sum_list_nat:
   4.141 +  "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns::nat list)"
   4.142 +  by (rule member_le_sum_list_nat) simp
   4.143  
   4.144 -lemma listsum_update_nat:
   4.145 -  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
   4.146 +lemma sum_list_update_nat:
   4.147 +  "k < size ns \<Longrightarrow> sum_list (ns[k := (n::nat)]) = sum_list ns + n - ns ! k"
   4.148  apply(induct ns arbitrary:k)
   4.149   apply (auto split:nat.split)
   4.150 -apply(drule elem_le_listsum_nat)
   4.151 +apply(drule elem_le_sum_list_nat)
   4.152  apply arith
   4.153  done
   4.154  
   4.155 -lemma (in monoid_add) listsum_triv:
   4.156 +lemma (in monoid_add) sum_list_triv:
   4.157    "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   4.158    by (induct xs) (simp_all add: distrib_right)
   4.159  
   4.160 -lemma (in monoid_add) listsum_0 [simp]:
   4.161 +lemma (in monoid_add) sum_list_0 [simp]:
   4.162    "(\<Sum>x\<leftarrow>xs. 0) = 0"
   4.163    by (induct xs) (simp_all add: distrib_right)
   4.164  
   4.165  text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
   4.166 -lemma (in ab_group_add) uminus_listsum_map:
   4.167 -  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
   4.168 +lemma (in ab_group_add) uminus_sum_list_map:
   4.169 +  "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)"
   4.170    by (induct xs) simp_all
   4.171  
   4.172 -lemma (in comm_monoid_add) listsum_addf:
   4.173 -  "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
   4.174 +lemma (in comm_monoid_add) sum_list_addf:
   4.175 +  "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)"
   4.176    by (induct xs) (simp_all add: algebra_simps)
   4.177  
   4.178 -lemma (in ab_group_add) listsum_subtractf:
   4.179 -  "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
   4.180 +lemma (in ab_group_add) sum_list_subtractf:
   4.181 +  "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)"
   4.182    by (induct xs) (simp_all add: algebra_simps)
   4.183  
   4.184 -lemma (in semiring_0) listsum_const_mult:
   4.185 +lemma (in semiring_0) sum_list_const_mult:
   4.186    "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
   4.187    by (induct xs) (simp_all add: algebra_simps)
   4.188  
   4.189 -lemma (in semiring_0) listsum_mult_const:
   4.190 +lemma (in semiring_0) sum_list_mult_const:
   4.191    "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
   4.192    by (induct xs) (simp_all add: algebra_simps)
   4.193  
   4.194 -lemma (in ordered_ab_group_add_abs) listsum_abs:
   4.195 -  "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
   4.196 +lemma (in ordered_ab_group_add_abs) sum_list_abs:
   4.197 +  "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)"
   4.198    by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
   4.199  
   4.200 -lemma listsum_mono:
   4.201 +lemma sum_list_mono:
   4.202    fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
   4.203    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)"
   4.204    by (induct xs) (simp, simp add: add_mono)
   4.205  
   4.206 -lemma (in monoid_add) listsum_distinct_conv_setsum_set:
   4.207 -  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
   4.208 +lemma (in monoid_add) sum_list_distinct_conv_setsum_set:
   4.209 +  "distinct xs \<Longrightarrow> sum_list (map f xs) = setsum f (set xs)"
   4.210    by (induct xs) simp_all
   4.211  
   4.212 -lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
   4.213 -  "listsum (map f [m..<n]) = setsum f (set [m..<n])"
   4.214 -  by (simp add: listsum_distinct_conv_setsum_set)
   4.215 +lemma (in monoid_add) interv_sum_list_conv_setsum_set_nat:
   4.216 +  "sum_list (map f [m..<n]) = setsum f (set [m..<n])"
   4.217 +  by (simp add: sum_list_distinct_conv_setsum_set)
   4.218  
   4.219 -lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
   4.220 -  "listsum (map f [k..l]) = setsum f (set [k..l])"
   4.221 -  by (simp add: listsum_distinct_conv_setsum_set)
   4.222 +lemma (in monoid_add) interv_sum_list_conv_setsum_set_int:
   4.223 +  "sum_list (map f [k..l]) = setsum f (set [k..l])"
   4.224 +  by (simp add: sum_list_distinct_conv_setsum_set)
   4.225  
   4.226 -text \<open>General equivalence between @{const listsum} and @{const setsum}\<close>
   4.227 -lemma (in monoid_add) listsum_setsum_nth:
   4.228 -  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   4.229 -  using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
   4.230 +text \<open>General equivalence between @{const sum_list} and @{const setsum}\<close>
   4.231 +lemma (in monoid_add) sum_list_setsum_nth:
   4.232 +  "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   4.233 +  using interv_sum_list_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
   4.234  
   4.235 -lemma listsum_map_eq_setsum_count:
   4.236 -  "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
   4.237 +lemma sum_list_map_eq_setsum_count:
   4.238 +  "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
   4.239  proof(induction xs)
   4.240    case (Cons x xs)
   4.241    show ?case (is "?l = ?r")
   4.242 @@ -236,9 +236,9 @@
   4.243    qed
   4.244  qed simp
   4.245  
   4.246 -lemma listsum_map_eq_setsum_count2:
   4.247 +lemma sum_list_map_eq_setsum_count2:
   4.248  assumes "set xs \<subseteq> X" "finite X"
   4.249 -shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
   4.250 +shows "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
   4.251  proof-
   4.252    let ?F = "\<lambda>x. count_list xs x * f x"
   4.253    have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
   4.254 @@ -246,23 +246,23 @@
   4.255    also have "\<dots> = setsum ?F (set xs)"
   4.256      using assms(2)
   4.257      by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
   4.258 -  finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
   4.259 +  finally show ?thesis by(simp add:sum_list_map_eq_setsum_count)
   4.260  qed
   4.261  
   4.262 -lemma listsum_nonneg: 
   4.263 -    "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
   4.264 +lemma sum_list_nonneg: 
   4.265 +    "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
   4.266    by (induction xs) simp_all
   4.267  
   4.268 -lemma (in monoid_add) listsum_map_filter':
   4.269 -  "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
   4.270 +lemma (in monoid_add) sum_list_map_filter':
   4.271 +  "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)"
   4.272    by (induction xs) simp_all
   4.273  
   4.274 -lemma listsum_cong [fundef_cong]:
   4.275 +lemma sum_list_cong [fundef_cong]:
   4.276    assumes "xs = ys"
   4.277    assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
   4.278 -  shows    "listsum (map f xs) = listsum (map g ys)"
   4.279 +  shows    "sum_list (map f xs) = sum_list (map g ys)"
   4.280  proof -
   4.281 -  from assms(2) have "listsum (map f xs) = listsum (map g xs)"
   4.282 +  from assms(2) have "sum_list (map f xs) = sum_list (map g xs)"
   4.283      by (induction xs) simp_all
   4.284    with assms(1) show ?thesis by simp
   4.285  qed
   4.286 @@ -271,7 +271,7 @@
   4.287  subsection \<open>Further facts about @{const List.n_lists}\<close>
   4.288  
   4.289  lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   4.290 -  by (induct n) (auto simp add: comp_def length_concat listsum_triv)
   4.291 +  by (induct n) (auto simp add: comp_def length_concat sum_list_triv)
   4.292  
   4.293  lemma distinct_n_lists:
   4.294    assumes "distinct xs"
   4.295 @@ -300,20 +300,20 @@
   4.296  
   4.297  lemmas setsum_code = setsum.set_conv_list
   4.298  
   4.299 -lemma setsum_set_upto_conv_listsum_int [code_unfold]:
   4.300 -  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
   4.301 -  by (simp add: interv_listsum_conv_setsum_set_int)
   4.302 +lemma setsum_set_upto_conv_sum_list_int [code_unfold]:
   4.303 +  "setsum f (set [i..j::int]) = sum_list (map f [i..j])"
   4.304 +  by (simp add: interv_sum_list_conv_setsum_set_int)
   4.305  
   4.306 -lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
   4.307 -  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   4.308 -  by (simp add: interv_listsum_conv_setsum_set_nat)
   4.309 +lemma setsum_set_upt_conv_sum_list_nat [code_unfold]:
   4.310 +  "setsum f (set [m..<n]) = sum_list (map f [m..<n])"
   4.311 +  by (simp add: interv_sum_list_conv_setsum_set_nat)
   4.312  
   4.313 -lemma listsum_transfer[transfer_rule]:
   4.314 +lemma sum_list_transfer[transfer_rule]:
   4.315    includes lifting_syntax
   4.316    assumes [transfer_rule]: "A 0 0"
   4.317    assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
   4.318 -  shows "(list_all2 A ===> A) listsum listsum"
   4.319 -  unfolding listsum.eq_foldr [abs_def]
   4.320 +  shows "(list_all2 A ===> A) sum_list sum_list"
   4.321 +  unfolding sum_list.eq_foldr [abs_def]
   4.322    by transfer_prover
   4.323  
   4.324  
   4.325 @@ -322,58 +322,58 @@
   4.326  context monoid_mult
   4.327  begin
   4.328  
   4.329 -sublocale listprod: monoid_list times 1
   4.330 +sublocale prod_list: monoid_list times 1
   4.331  defines
   4.332 -  listprod = listprod.F ..
   4.333 +  prod_list = prod_list.F ..
   4.334  
   4.335  end
   4.336  
   4.337  context comm_monoid_mult
   4.338  begin
   4.339  
   4.340 -sublocale listprod: comm_monoid_list times 1
   4.341 +sublocale prod_list: comm_monoid_list times 1
   4.342  rewrites
   4.343 -  "monoid_list.F times 1 = listprod"
   4.344 +  "monoid_list.F times 1 = prod_list"
   4.345  proof -
   4.346    show "comm_monoid_list times 1" ..
   4.347 -  then interpret listprod: comm_monoid_list times 1 .
   4.348 -  from listprod_def show "monoid_list.F times 1 = listprod" by simp
   4.349 +  then interpret prod_list: comm_monoid_list times 1 .
   4.350 +  from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
   4.351  qed
   4.352  
   4.353  sublocale setprod: comm_monoid_list_set times 1
   4.354  rewrites
   4.355 -  "monoid_list.F times 1 = listprod"
   4.356 +  "monoid_list.F times 1 = prod_list"
   4.357    and "comm_monoid_set.F times 1 = setprod"
   4.358  proof -
   4.359    show "comm_monoid_list_set times 1" ..
   4.360    then interpret setprod: comm_monoid_list_set times 1 .
   4.361 -  from listprod_def show "monoid_list.F times 1 = listprod" by simp
   4.362 +  from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
   4.363    from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
   4.364  qed
   4.365  
   4.366  end
   4.367  
   4.368 -lemma listprod_cong [fundef_cong]:
   4.369 +lemma prod_list_cong [fundef_cong]:
   4.370    assumes "xs = ys"
   4.371    assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
   4.372 -  shows    "listprod (map f xs) = listprod (map g ys)"
   4.373 +  shows    "prod_list (map f xs) = prod_list (map g ys)"
   4.374  proof -
   4.375 -  from assms(2) have "listprod (map f xs) = listprod (map g xs)"
   4.376 +  from assms(2) have "prod_list (map f xs) = prod_list (map g xs)"
   4.377      by (induction xs) simp_all
   4.378    with assms(1) show ?thesis by simp
   4.379  qed
   4.380  
   4.381 -lemma listprod_zero_iff: 
   4.382 -  "listprod xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
   4.383 +lemma prod_list_zero_iff: 
   4.384 +  "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
   4.385    by (induction xs) simp_all
   4.386  
   4.387  text \<open>Some syntactic sugar:\<close>
   4.388  
   4.389  syntax (ASCII)
   4.390 -  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
   4.391 +  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
   4.392  syntax
   4.393 -  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
   4.394 +  "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
   4.395  translations \<comment> \<open>Beware of argument permutation!\<close>
   4.396 -  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)"
   4.397 +  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
   4.398  
   4.399  end
     5.1 --- a/src/HOL/IMP/Abs_Int0.thy	Wed Sep 14 22:07:11 2016 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Thu Sep 15 11:48:20 2016 +0200
     5.3 @@ -329,14 +329,14 @@
     5.4  by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)
     5.5  
     5.6  definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
     5.7 -"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
     5.8 +"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
     5.9  
    5.10  text{* Upper complexity bound: *}
    5.11  lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
    5.12  proof-
    5.13    let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
    5.14    have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
    5.15 -    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
    5.16 +    by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
    5.17    also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    5.18      apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
    5.19    also have "\<dots> = ?a * (h * ?n + 1)" by simp
    5.20 @@ -455,7 +455,7 @@
    5.21           < (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
    5.22      apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
    5.23    thus ?thesis
    5.24 -    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
    5.25 +    by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
    5.26  qed
    5.27  
    5.28  end
     6.1 --- a/src/HOL/IMP/Abs_Int1.thy	Wed Sep 14 22:07:11 2016 +0200
     6.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Thu Sep 15 11:48:20 2016 +0200
     6.3 @@ -118,14 +118,14 @@
     6.4  by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
     6.5  
     6.6  definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
     6.7 -"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
     6.8 +"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
     6.9  
    6.10  text{* Upper complexity bound: *}
    6.11  lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
    6.12  proof-
    6.13    let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
    6.14    have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
    6.15 -    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
    6.16 +    by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
    6.17    also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    6.18      apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
    6.19    also have "\<dots> = ?a * (h * ?n + 1)" by simp
    6.20 @@ -239,7 +239,7 @@
    6.21           < (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
    6.22      apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
    6.23    thus ?thesis
    6.24 -    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
    6.25 +    by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
    6.26  qed
    6.27  
    6.28  end
     7.1 --- a/src/HOL/IMP/Abs_Int3.thy	Wed Sep 14 22:07:11 2016 +0200
     7.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Thu Sep 15 11:48:20 2016 +0200
     7.3 @@ -390,7 +390,7 @@
     7.4  lemma m_c_widen:
     7.5    "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
     7.6     \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
     7.7 -apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
     7.8 +apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]sum_list_setsum_nth)
     7.9  apply(subgoal_tac "length(annos C2) = length(annos C1)")
    7.10   prefer 2 apply (simp add: size_annos_same2)
    7.11  apply (auto)
    7.12 @@ -437,7 +437,7 @@
    7.13  
    7.14  
    7.15  definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
    7.16 -"n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
    7.17 +"n\<^sub>c C = sum_list (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
    7.18  
    7.19  lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
    7.20    (\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
    7.21 @@ -446,7 +446,7 @@
    7.22  lemma n_c_narrow: "strip C1 = strip C2
    7.23    \<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
    7.24    \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1"
    7.25 -apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth)
    7.26 +apply(auto simp: n_c_def narrow_acom_def sum_list_setsum_nth)
    7.27  apply(subgoal_tac "length(annos C2) = length(annos C1)")
    7.28  prefer 2 apply (simp add: size_annos_same2)
    7.29  apply (auto)
     8.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Sep 14 22:07:11 2016 +0200
     8.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Sep 15 11:48:20 2016 +0200
     8.3 @@ -951,16 +951,16 @@
     8.4  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)"
     8.5    by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
     8.6  
     8.7 -lemma listsum_ennreal[simp]:
     8.8 +lemma sum_list_ennreal[simp]:
     8.9    assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
    8.10 -  shows   "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
    8.11 +  shows   "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
    8.12  using assms
    8.13  proof (induction xs)
    8.14    case (Cons x xs)
    8.15 -  from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))"
    8.16 +  from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
    8.17      by simp
    8.18 -  also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))"
    8.19 -    by (intro ennreal_plus [symmetric] listsum_nonneg) auto
    8.20 +  also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
    8.21 +    by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
    8.22    finally show ?case by simp
    8.23  qed simp_all
    8.24  
     9.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Sep 14 22:07:11 2016 +0200
     9.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 15 11:48:20 2016 +0200
     9.3 @@ -771,7 +771,7 @@
     9.4    then show ?thesis by simp
     9.5  qed
     9.6  
     9.7 -lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
     9.8 +lemma sum_list_ereal [simp]: "sum_list (map (\<lambda>x. ereal (f x)) xs) = ereal (sum_list (map f xs))"
     9.9    by (induction xs) simp_all
    9.10  
    9.11  lemma setsum_Pinfty:
    10.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Sep 14 22:07:11 2016 +0200
    10.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Sep 15 11:48:20 2016 +0200
    10.3 @@ -2107,7 +2107,7 @@
    10.4  subsubsection \<open>Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
    10.5    finite product of FPS, also the relvant instance of powers of a FPS\<close>
    10.6  
    10.7 -definition "natpermute n k = {l :: nat list. length l = k \<and> listsum l = n}"
    10.8 +definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"
    10.9  
   10.10  lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
   10.11    apply (auto simp add: natpermute_def)
   10.12 @@ -2117,14 +2117,14 @@
   10.13  
   10.14  lemma append_natpermute_less_eq:
   10.15    assumes "xs @ ys \<in> natpermute n k"
   10.16 -  shows "listsum xs \<le> n"
   10.17 -    and "listsum ys \<le> n"
   10.18 +  shows "sum_list xs \<le> n"
   10.19 +    and "sum_list ys \<le> n"
   10.20  proof -
   10.21 -  from assms have "listsum (xs @ ys) = n"
   10.22 +  from assms have "sum_list (xs @ ys) = n"
   10.23      by (simp add: natpermute_def)
   10.24 -  then have "listsum xs + listsum ys = n"
   10.25 +  then have "sum_list xs + sum_list ys = n"
   10.26      by simp
   10.27 -  then show "listsum xs \<le> n" and "listsum ys \<le> n"
   10.28 +  then show "sum_list xs \<le> n" and "sum_list ys \<le> n"
   10.29      by simp_all
   10.30  qed
   10.31  
   10.32 @@ -2142,9 +2142,9 @@
   10.33        and xs: "xs \<in> natpermute m h"
   10.34        and ys: "ys \<in> natpermute (n - m) (k - h)"
   10.35        and leq: "l = xs@ys" by blast
   10.36 -    from xs have xs': "listsum xs = m"
   10.37 +    from xs have xs': "sum_list xs = m"
   10.38        by (simp add: natpermute_def)
   10.39 -    from ys have ys': "listsum ys = n - m"
   10.40 +    from ys have ys': "sum_list ys = n - m"
   10.41        by (simp add: natpermute_def)
   10.42      show "l \<in> ?L" using leq xs ys h
   10.43        apply (clarsimp simp add: natpermute_def)
   10.44 @@ -2160,12 +2160,12 @@
   10.45      assume l: "l \<in> natpermute n k"
   10.46      let ?xs = "take h l"
   10.47      let ?ys = "drop h l"
   10.48 -    let ?m = "listsum ?xs"
   10.49 -    from l have ls: "listsum (?xs @ ?ys) = n"
   10.50 +    let ?m = "sum_list ?xs"
   10.51 +    from l have ls: "sum_list (?xs @ ?ys) = n"
   10.52        by (simp add: natpermute_def)
   10.53      have xs: "?xs \<in> natpermute ?m h" using l assms
   10.54        by (simp add: natpermute_def)
   10.55 -    have l_take_drop: "listsum l = listsum (take h l @ drop h l)"
   10.56 +    have l_take_drop: "sum_list l = sum_list (take h l @ drop h l)"
   10.57        by simp
   10.58      then have ys: "?ys \<in> natpermute (n - ?m) (k - h)"
   10.59        using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
   10.60 @@ -2230,7 +2230,7 @@
   10.61        using i by auto
   10.62      from H have "n = setsum (nth xs) {0..k}"
   10.63        apply (simp add: natpermute_def)
   10.64 -      apply (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth)
   10.65 +      apply (auto simp add: atLeastLessThanSuc_atLeastAtMost sum_list_setsum_nth)
   10.66        done
   10.67      also have "\<dots> = n + setsum (nth xs) ({0..k} - {i})"
   10.68        unfolding setsum.union_disjoint[OF f d, unfolded eqs] using i by simp
   10.69 @@ -2265,8 +2265,8 @@
   10.70        done
   10.71      have xsl: "length xs = k + 1"
   10.72        by (simp only: xs length_replicate length_list_update)
   10.73 -    have "listsum xs = setsum (nth xs) {0..<k+1}"
   10.74 -      unfolding listsum_setsum_nth xsl ..
   10.75 +    have "sum_list xs = setsum (nth xs) {0..<k+1}"
   10.76 +      unfolding sum_list_setsum_nth xsl ..
   10.77      also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
   10.78        by (rule setsum.cong) (simp_all add: xs del: replicate.simps)
   10.79      also have "\<dots> = n" using i by (simp add: setsum.delta)
   10.80 @@ -2421,9 +2421,9 @@
   10.81        by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
   10.82      then guess j by (elim exE conjE) note j = this
   10.83      
   10.84 -    from v have "k = listsum v" by (simp add: A_def natpermute_def)
   10.85 +    from v have "k = sum_list v" by (simp add: A_def natpermute_def)
   10.86      also have "\<dots> = (\<Sum>i=0..m. v ! i)"
   10.87 -      by (simp add: listsum_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
   10.88 +      by (simp add: sum_list_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
   10.89      also from j have "{0..m} = insert j ({0..m}-{j})" by auto
   10.90      also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
   10.91        by (subst setsum.insert) simp_all
   10.92 @@ -2469,7 +2469,7 @@
   10.93                  g $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h g" using assms 
   10.94          by (simp add: mult_ac del: power_Suc of_nat_Suc)
   10.95        also have "v ! i < k" if "v \<in> {v\<in>natpermute k (m+1). k \<notin> set v}" "i \<le> m" for v i
   10.96 -        using that elem_le_listsum_nat[of i v] unfolding natpermute_def
   10.97 +        using that elem_le_sum_list_nat[of i v] unfolding natpermute_def
   10.98          by (auto simp: set_conv_nth dest!: spec[of _ i])
   10.99        hence "?h f = ?h g"
  10.100          by (intro setsum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
  10.101 @@ -2599,10 +2599,10 @@
  10.102          by auto
  10.103        have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
  10.104          using i by auto
  10.105 -      from xs have "Suc n = listsum xs"
  10.106 +      from xs have "Suc n = sum_list xs"
  10.107          by (simp add: natpermute_def)
  10.108        also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
  10.109 -        by (simp add: natpermute_def listsum_setsum_nth)
  10.110 +        by (simp add: natpermute_def sum_list_setsum_nth)
  10.111        also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
  10.112          unfolding eqs  setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
  10.113          unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
  10.114 @@ -2853,10 +2853,10 @@
  10.115                by auto
  10.116              have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
  10.117                using i by auto
  10.118 -            from xs have "n = listsum xs"
  10.119 +            from xs have "n = sum_list xs"
  10.120                by (simp add: natpermute_def)
  10.121              also have "\<dots> = setsum (nth xs) {0..<Suc k}"
  10.122 -              using xs by (simp add: natpermute_def listsum_setsum_nth)
  10.123 +              using xs by (simp add: natpermute_def sum_list_setsum_nth)
  10.124              also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
  10.125                unfolding eqs  setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
  10.126                unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
    11.1 --- a/src/HOL/Library/ListVector.thy	Wed Sep 14 22:07:11 2016 +0200
    11.2 +++ b/src/HOL/Library/ListVector.thy	Thu Sep 15 11:48:20 2016 +0200
    11.3 @@ -119,7 +119,7 @@
    11.4  done
    11.5  
    11.6  lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
    11.7 -by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
    11.8 +by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
    11.9  
   11.10  lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
   11.11  apply(induct xs arbitrary: ys zs)
    12.1 --- a/src/HOL/Library/Multiset.thy	Wed Sep 14 22:07:11 2016 +0200
    12.2 +++ b/src/HOL/Library/Multiset.thy	Thu Sep 15 11:48:20 2016 +0200
    12.3 @@ -3188,7 +3188,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -lemma [code]: "sum_mset (mset xs) = listsum xs"
    12.8 +lemma [code]: "sum_mset (mset xs) = sum_list xs"
    12.9    by (induct xs) simp_all
   12.10  
   12.11  lemma [code]: "prod_mset (mset xs) = fold times xs 1"
    13.1 --- a/src/HOL/Library/Polynomial.thy	Wed Sep 14 22:07:11 2016 +0200
    13.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Sep 15 11:48:20 2016 +0200
    13.3 @@ -2946,7 +2946,7 @@
    13.4  lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
    13.5    unfolding lead_coeff_def by auto
    13.6  
    13.7 -lemma coeff_0_listprod: "coeff (listprod xs) 0 = listprod (map (\<lambda>p. coeff p 0) xs)"
    13.8 +lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
    13.9    by (induction xs) (simp_all add: coeff_mult)
   13.10  
   13.11  lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
   13.12 @@ -3214,9 +3214,9 @@
   13.13       setprod (\<lambda>x. reflect_poly (f x)) A"
   13.14    by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
   13.15  
   13.16 -lemma reflect_poly_listprod:
   13.17 -  "reflect_poly (listprod (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) = 
   13.18 -     listprod (map reflect_poly xs)"
   13.19 +lemma reflect_poly_prod_list:
   13.20 +  "reflect_poly (prod_list (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) = 
   13.21 +     prod_list (map reflect_poly xs)"
   13.22    by (induction xs) (simp_all add: reflect_poly_mult)
   13.23  
   13.24  lemma reflect_poly_Poly_nz: 
   13.25 @@ -3225,7 +3225,7 @@
   13.26  
   13.27  lemmas reflect_poly_simps = 
   13.28    reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
   13.29 -  reflect_poly_power reflect_poly_setprod reflect_poly_listprod
   13.30 +  reflect_poly_power reflect_poly_setprod reflect_poly_prod_list
   13.31  
   13.32  
   13.33  subsection \<open>Derivatives of univariate polynomials\<close>
    14.1 --- a/src/HOL/Library/Polynomial_FPS.thy	Wed Sep 14 22:07:11 2016 +0200
    14.2 +++ b/src/HOL/Library/Polynomial_FPS.thy	Thu Sep 15 11:48:20 2016 +0200
    14.3 @@ -64,13 +64,13 @@
    14.4  lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\<lambda>x. fps_of_poly (f x)) A"
    14.5    by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add)
    14.6  
    14.7 -lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)"
    14.8 +lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
    14.9    by (induction xs) (simp_all add: fps_of_poly_add)
   14.10    
   14.11  lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
   14.12    by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
   14.13    
   14.14 -lemma fps_of_poly_listprod: "fps_of_poly (listprod xs) = listprod (map fps_of_poly xs)"
   14.15 +lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
   14.16    by (induction xs) (simp_all add: fps_of_poly_mult)
   14.17  
   14.18  lemma fps_of_poly_pCons: 
   14.19 @@ -144,7 +144,7 @@
   14.20  lemmas fps_of_poly_simps =
   14.21    fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
   14.22    fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
   14.23 -  fps_of_poly_setsum fps_of_poly_listsum fps_of_poly_setprod fps_of_poly_listprod
   14.24 +  fps_of_poly_setsum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
   14.25    fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
   14.26    fps_of_poly_divide_numeral
   14.27  
    15.1 --- a/src/HOL/Nitpick.thy	Wed Sep 14 22:07:11 2016 +0200
    15.2 +++ b/src/HOL/Nitpick.thy	Thu Sep 15 11:48:20 2016 +0200
    15.3 @@ -73,7 +73,7 @@
    15.4    "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
    15.5  
    15.6  definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
    15.7 -  "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    15.8 +  "setsum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    15.9  
   15.10  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
   15.11    "fold_graph' f z {} z" |
    16.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Wed Sep 14 22:07:11 2016 +0200
    16.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Thu Sep 15 11:48:20 2016 +0200
    16.3 @@ -213,8 +213,8 @@
    16.4      prefer 2
    16.5      apply (erule allE, erule impE, rule refl, erule spec)
    16.6      apply simp
    16.7 -    apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
    16.8 -    apply (fastforce simp add: listsum_map_remove1)
    16.9 +    apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
   16.10 +    apply (fastforce simp add: sum_list_map_remove1)
   16.11    apply clarify
   16.12    apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
   16.13     prefer 2
   16.14 @@ -235,8 +235,8 @@
   16.15     prefer 2
   16.16     apply blast
   16.17    apply simp
   16.18 -  apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
   16.19 -  apply (fastforce simp add: listsum_map_remove1)
   16.20 +  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
   16.21 +  apply (fastforce simp add: sum_list_map_remove1)
   16.22    done
   16.23  
   16.24  theorem Apps_lam_induct:
    17.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Sep 14 22:07:11 2016 +0200
    17.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 15 11:48:20 2016 +0200
    17.3 @@ -306,14 +306,14 @@
    17.4  lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
    17.5    by (auto simp: sparsify_def set_zip)
    17.6  
    17.7 -lemma listsum_sparsify[simp]:
    17.8 +lemma sum_list_sparsify[simp]:
    17.9    fixes v :: "('a :: semiring_0) list"
   17.10    assumes "length w = length v"
   17.11    shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
   17.12      (is "(\<Sum>x\<leftarrow>_. ?f x) = _")
   17.13    unfolding sparsify_def scalar_product_def
   17.14 -  using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
   17.15 -  by (simp add: listsum_setsum)
   17.16 +  using assms sum_list_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
   17.17 +  by (simp add: sum_list_setsum)
   17.18  *)
   17.19  definition [simp]: "unzip w = (map fst w, map snd w)"
   17.20  
   17.21 @@ -338,7 +338,7 @@
   17.22    "jad = apsnd transpose o length_permutate o map sparsify"
   17.23  
   17.24  definition
   17.25 -  "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
   17.26 +  "jad_mv v = inflate o case_prod zip o apsnd (map sum_list o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
   17.27  
   17.28  lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
   17.29  quickcheck[tester = smart_exhaustive, size = 6]
    18.1 --- a/src/HOL/Probability/PMF_Impl.thy	Wed Sep 14 22:07:11 2016 +0200
    18.2 +++ b/src/HOL/Probability/PMF_Impl.thy	Thu Sep 15 11:48:20 2016 +0200
    18.3 @@ -396,10 +396,10 @@
    18.4  
    18.5  
    18.6  lemma mapping_of_pmf_pmf_of_list:
    18.7 -  assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "listsum (map snd xs) = 1"
    18.8 +  assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "sum_list (map snd xs) = 1"
    18.9    shows   "mapping_of_pmf (pmf_of_list xs) = 
   18.10               Mapping.tabulate (remdups (map fst xs)) 
   18.11 -               (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
   18.12 +               (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
   18.13  proof -
   18.14    from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force
   18.15    with assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
   18.16 @@ -413,7 +413,7 @@
   18.17    defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
   18.18    shows   "mapping_of_pmf (pmf_of_list xs) = 
   18.19               Mapping.tabulate (remdups (map fst xs')) 
   18.20 -               (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs") 
   18.21 +               (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs") 
   18.22  proof -
   18.23    have wf: "pmf_of_list_wf xs'" unfolding xs'_def by (rule pmf_of_list_remove_zeros) fact
   18.24    have pos: "\<forall>x\<in>snd`set xs'. x > 0" using assms(1) unfolding xs'_def
   18.25 @@ -426,7 +426,7 @@
   18.26  qed
   18.27  
   18.28  lemma pmf_of_list_wf_code [code]:
   18.29 -  "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> listsum (map snd xs) = 1"
   18.30 +  "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> sum_list (map snd xs) = 1"
   18.31    by (auto simp add: pmf_of_list_wf_def list_all_def)
   18.32  
   18.33  lemma pmf_of_list_code [code abstract]:
   18.34 @@ -434,7 +434,7 @@
   18.35       if pmf_of_list_wf xs then
   18.36         let xs' = filter (\<lambda>z. snd z \<noteq> 0) xs
   18.37         in  Mapping.tabulate (remdups (map fst xs')) 
   18.38 -             (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))
   18.39 +             (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))
   18.40       else
   18.41         Code.abort (STR ''Invalid list for pmf_of_list'') (\<lambda>_. mapping_of_pmf (pmf_of_list xs)))"
   18.42    using mapping_of_pmf_pmf_of_list'[of xs] by (simp add: Let_def)
    19.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Sep 14 22:07:11 2016 +0200
    19.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 11:48:20 2016 +0200
    19.3 @@ -1843,13 +1843,13 @@
    19.4  subsection \<open>PMFs from assiciation lists\<close>
    19.5  
    19.6  definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
    19.7 -  "pmf_of_list xs = embed_pmf (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
    19.8 +  "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
    19.9  
   19.10  definition pmf_of_list_wf where
   19.11 -  "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> listsum (map snd xs) = 1"
   19.12 +  "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> sum_list (map snd xs) = 1"
   19.13  
   19.14  lemma pmf_of_list_wfI:
   19.15 -  "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
   19.16 +  "(\<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"
   19.17    unfolding pmf_of_list_wf_def by simp
   19.18  
   19.19  context
   19.20 @@ -1857,12 +1857,12 @@
   19.21  
   19.22  private lemma pmf_of_list_aux:
   19.23    assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
   19.24 -  assumes "listsum (map snd xs) = 1"
   19.25 -  shows "(\<integral>\<^sup>+ x. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
   19.26 +  assumes "sum_list (map snd xs) = 1"
   19.27 +  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
   19.28  proof -
   19.29 -  have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
   19.30 -            (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
   19.31 -    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter') (auto intro: listsum_cong)
   19.32 +  have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
   19.33 +            (\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
   19.34 +    by (intro nn_integral_cong ennreal_cong, subst sum_list_map_filter') (auto intro: sum_list_cong)
   19.35    also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
   19.36      using assms(1)
   19.37    proof (induction xs)
   19.38 @@ -1874,11 +1874,11 @@
   19.39              (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + 
   19.40              ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
   19.41        by (intro nn_integral_cong, subst ennreal_plus [symmetric]) 
   19.42 -         (auto simp: case_prod_unfold indicator_def intro!: listsum_nonneg)
   19.43 +         (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
   19.44      also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) + 
   19.45                        (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
   19.46        by (intro nn_integral_add)
   19.47 -         (force intro!: listsum_nonneg AE_I2 intro: Cons simp: indicator_def)+
   19.48 +         (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
   19.49      also have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV) =
   19.50                 (\<Sum>(x', p)\<leftarrow>xs. (\<integral>\<^sup>+ y. ennreal (indicator {x'} y * p) \<partial>count_space UNIV))"
   19.51        using Cons(1) by (intro Cons) simp_all
   19.52 @@ -1886,19 +1886,19 @@
   19.53    qed simp
   19.54    also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
   19.55      using assms(1)
   19.56 -    by (intro listsum_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
   19.57 +    by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
   19.58         (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
   19.59               simp del: times_ereal.simps)+
   19.60 -  also from assms have "\<dots> = listsum (map snd xs)" by (simp add: case_prod_unfold listsum_ennreal)
   19.61 +  also from assms have "\<dots> = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal)
   19.62    also have "\<dots> = 1" using assms(2) by simp
   19.63    finally show ?thesis .
   19.64  qed
   19.65  
   19.66  lemma pmf_pmf_of_list:
   19.67    assumes "pmf_of_list_wf xs"
   19.68 -  shows   "pmf (pmf_of_list xs) x = listsum (map snd (filter (\<lambda>z. fst z = x) xs))"
   19.69 +  shows   "pmf (pmf_of_list xs) x = sum_list (map snd (filter (\<lambda>z. fst z = x) xs))"
   19.70    using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def
   19.71 -  by (subst pmf_embed_pmf) (auto intro!: listsum_nonneg)
   19.72 +  by (subst pmf_embed_pmf) (auto intro!: sum_list_nonneg)
   19.73  
   19.74  end
   19.75  
   19.76 @@ -1930,16 +1930,16 @@
   19.77  
   19.78  lemma emeasure_pmf_of_list:
   19.79    assumes "pmf_of_list_wf xs"
   19.80 -  shows   "emeasure (pmf_of_list xs) A = ennreal (listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
   19.81 +  shows   "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
   19.82  proof -
   19.83    have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
   19.84      by simp
   19.85    also from assms 
   19.86 -    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])))"
   19.87 +    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
   19.88      by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
   19.89    also from assms 
   19.90 -    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. listsum (map snd [z\<leftarrow>xs . fst z = x]))"
   19.91 -    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: listsum_nonneg)
   19.92 +    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
   19.93 +    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
   19.94    also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. 
   19.95        indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
   19.96      using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
   19.97 @@ -1948,13 +1948,13 @@
   19.98    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
   19.99      using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
  19.100    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * 
  19.101 -                      listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
  19.102 +                      sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
  19.103      using assms by (simp add: pmf_pmf_of_list)
  19.104 -  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). listsum (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
  19.105 +  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)))"
  19.106      by (intro setsum.cong) (auto simp: indicator_def)
  19.107    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
  19.108                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  19.109 -    by (intro setsum.cong refl, subst listsum_map_filter', subst listsum_setsum_nth) simp
  19.110 +    by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
  19.111    also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
  19.112                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  19.113      by (rule setsum.commute)
  19.114 @@ -1963,30 +1963,30 @@
  19.115      by (auto intro!: setsum.cong setsum.neutral)
  19.116    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
  19.117      by (intro setsum.cong refl) (simp_all add: setsum.delta)
  19.118 -  also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  19.119 -    by (subst listsum_map_filter', subst listsum_setsum_nth) simp_all
  19.120 +  also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  19.121 +    by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
  19.122    finally show ?thesis . 
  19.123  qed
  19.124  
  19.125  lemma measure_pmf_of_list:
  19.126    assumes "pmf_of_list_wf xs"
  19.127 -  shows   "measure (pmf_of_list xs) A = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  19.128 +  shows   "measure (pmf_of_list xs) A = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  19.129    using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
  19.130 -  by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
  19.131 +  by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: sum_list_nonneg)
  19.132  
  19.133  (* TODO Move? *)
  19.134 -lemma listsum_nonneg_eq_zero_iff:
  19.135 +lemma sum_list_nonneg_eq_zero_iff:
  19.136    fixes xs :: "'a :: linordered_ab_group_add list"
  19.137 -  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
  19.138 +  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
  19.139  proof (induction xs)
  19.140    case (Cons x xs)
  19.141 -  from Cons.prems have "listsum (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> listsum xs = 0"
  19.142 -    unfolding listsum_simps by (subst add_nonneg_eq_0_iff) (auto intro: listsum_nonneg)
  19.143 +  from Cons.prems have "sum_list (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> sum_list xs = 0"
  19.144 +    unfolding sum_list_simps by (subst add_nonneg_eq_0_iff) (auto intro: sum_list_nonneg)
  19.145    with Cons.IH Cons.prems show ?case by simp
  19.146  qed simp_all
  19.147  
  19.148 -lemma listsum_filter_nonzero:
  19.149 -  "listsum (filter (\<lambda>x. x \<noteq> 0) xs) = listsum xs"
  19.150 +lemma sum_list_filter_nonzero:
  19.151 +  "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
  19.152    by (induction xs) simp_all
  19.153  (* END MOVE *)
  19.154    
  19.155 @@ -1997,11 +1997,11 @@
  19.156    {
  19.157      fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
  19.158      then obtain y where y: "(x, y) \<in> set xs" by auto
  19.159 -    from B have "listsum (map snd [z\<leftarrow>xs. fst z = x]) = 0"
  19.160 +    from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
  19.161        by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
  19.162      moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
  19.163      ultimately have "y = 0" using assms(1) 
  19.164 -      by (subst (asm) listsum_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
  19.165 +      by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
  19.166      with assms(2) y have False by force
  19.167    }
  19.168    thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
  19.169 @@ -2015,8 +2015,8 @@
  19.170    have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
  19.171      by (induction xs) simp_all
  19.172    with assms(1) show wf: "pmf_of_list_wf xs'"
  19.173 -    by (auto simp: pmf_of_list_wf_def xs'_def listsum_filter_nonzero)
  19.174 -  have "listsum (map snd [z\<leftarrow>xs' . fst z = i]) = listsum (map snd [z\<leftarrow>xs . fst z = i])" for i
  19.175 +    by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
  19.176 +  have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
  19.177      unfolding xs'_def by (induction xs) simp_all
  19.178    with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
  19.179      by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
    20.1 --- a/src/HOL/Proofs/Lambda/ListApplication.thy	Wed Sep 14 22:07:11 2016 +0200
    20.2 +++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Sep 15 11:48:20 2016 +0200
    20.3 @@ -110,8 +110,8 @@
    20.4      prefer 2
    20.5      apply (erule allE, erule mp, rule refl)
    20.6     apply simp
    20.7 -   apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
    20.8 -   apply (fastforce simp add: listsum_map_remove1)
    20.9 +   apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
   20.10 +   apply (fastforce simp add: sum_list_map_remove1)
   20.11    apply clarify
   20.12    apply (rule assms)
   20.13     apply (erule allE, erule impE)
   20.14 @@ -126,8 +126,8 @@
   20.15    apply (rule le_imp_less_Suc)
   20.16    apply (rule trans_le_add1)
   20.17    apply (rule trans_le_add2)
   20.18 -  apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
   20.19 -  apply (simp add: member_le_listsum_nat)
   20.20 +  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
   20.21 +  apply (simp add: member_le_sum_list_nat)
   20.22    done
   20.23  
   20.24  theorem Apps_dB_induct:
    21.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Sep 14 22:07:11 2016 +0200
    21.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 15 11:48:20 2016 +0200
    21.3 @@ -204,7 +204,7 @@
    21.4  oops
    21.5  
    21.6  lemma
    21.7 -  "ns ! k < length ns ==> k <= listsum ns"
    21.8 +  "ns ! k < length ns ==> k <= sum_list ns"
    21.9  quickcheck[random, iterations = 10000, finite_types = false, quiet]
   21.10  quickcheck[exhaustive, finite_types = false, expect = counterexample]
   21.11  oops
    22.1 --- a/src/HOL/Random.thy	Wed Sep 14 22:07:11 2016 +0200
    22.2 +++ b/src/HOL/Random.thy	Thu Sep 15 11:48:20 2016 +0200
    22.3 @@ -79,7 +79,7 @@
    22.4    "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
    22.5  
    22.6  lemma pick_member:
    22.7 -  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
    22.8 +  "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
    22.9    by (induct xs arbitrary: i) (simp_all add: less_natural_def)
   22.10  
   22.11  lemma pick_drop_zero:
   22.12 @@ -95,17 +95,17 @@
   22.13  qed
   22.14  
   22.15  definition select_weight :: "(natural \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   22.16 -  "select_weight xs = range (listsum (map fst xs))
   22.17 +  "select_weight xs = range (sum_list (map fst xs))
   22.18     \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
   22.19  
   22.20  lemma select_weight_member:
   22.21 -  assumes "0 < listsum (map fst xs)"
   22.22 +  assumes "0 < sum_list (map fst xs)"
   22.23    shows "fst (select_weight xs s) \<in> set (map snd xs)"
   22.24  proof -
   22.25    from range assms
   22.26 -    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
   22.27 +    have "fst (range (sum_list (map fst xs)) s) < sum_list (map fst xs)" .
   22.28    with pick_member
   22.29 -    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
   22.30 +    have "pick xs (fst (range (sum_list (map fst xs)) s)) \<in> set (map snd xs)" .
   22.31    then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
   22.32  qed
   22.33  
   22.34 @@ -116,7 +116,7 @@
   22.35  lemma select_weight_drop_zero:
   22.36    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
   22.37  proof -
   22.38 -  have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
   22.39 +  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
   22.40      by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
   22.41    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
   22.42  qed
   22.43 @@ -127,7 +127,7 @@
   22.44  proof -
   22.45    have less: "\<And>s. fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)"
   22.46      using assms by (intro range) (simp add: less_natural_def)
   22.47 -  moreover have "listsum (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
   22.48 +  moreover have "sum_list (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
   22.49      by (induct xs) simp_all
   22.50    ultimately show ?thesis
   22.51      by (auto simp add: select_weight_def select_def scomp_def split_def
    23.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Sep 14 22:07:11 2016 +0200
    23.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Sep 15 11:48:20 2016 +0200
    23.3 @@ -14,7 +14,7 @@
    23.4  
    23.5  abbreviation (input) tokens :: "nat list \<Rightarrow> nat"
    23.6  where
    23.7 -  "tokens \<equiv> listsum"
    23.8 +  "tokens \<equiv> sum_list"
    23.9  
   23.10  abbreviation (input)
   23.11    "bag_of \<equiv> mset"
    24.1 --- a/src/HOL/ex/Gauge_Integration.thy	Wed Sep 14 22:07:11 2016 +0200
    24.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Thu Sep 15 11:48:20 2016 +0200
    24.3 @@ -204,7 +204,7 @@
    24.4    ultimately show ?case by simp
    24.5  qed auto
    24.6  
    24.7 -lemma fine_listsum_eq_diff:
    24.8 +lemma fine_sum_list_eq_diff:
    24.9    fixes f :: "real \<Rightarrow> real"
   24.10    shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
   24.11  by (induct set: fine) simp_all
   24.12 @@ -249,7 +249,7 @@
   24.13  by (induct D, auto simp add: algebra_simps)
   24.14  
   24.15  lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
   24.16 -unfolding rsum_def map_append listsum_append ..
   24.17 +unfolding rsum_def map_append sum_list_append ..
   24.18  
   24.19  
   24.20  subsection \<open>Gauge integrability (definite)\<close>
   24.21 @@ -594,22 +594,22 @@
   24.22      proof (clarify)
   24.23        fix D assume D: "fine \<delta> (a, b) D"
   24.24        hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
   24.25 -        by (rule fine_listsum_eq_diff)
   24.26 +        by (rule fine_sum_list_eq_diff)
   24.27        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>"
   24.28          by simp
   24.29        also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
   24.30          by (rule abs_minus_commute)
   24.31        also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
   24.32 -        by (simp only: rsum_def listsum_subtractf split_def)
   24.33 +        by (simp only: rsum_def sum_list_subtractf split_def)
   24.34        also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
   24.35 -        by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
   24.36 +        by (rule ord_le_eq_trans [OF sum_list_abs], simp add: o_def split_def)
   24.37        also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
   24.38 -        apply (rule listsum_mono, clarify, rename_tac u x v)
   24.39 +        apply (rule sum_list_mono, clarify, rename_tac u x v)
   24.40          using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
   24.41          done
   24.42        also have "\<dots> = e"
   24.43 -        using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
   24.44 -        unfolding split_def listsum_const_mult
   24.45 +        using fine_sum_list_eq_diff [OF D, where f="\<lambda>x. x"]
   24.46 +        unfolding split_def sum_list_const_mult
   24.47          using \<open>a < b\<close> by simp
   24.48        finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
   24.49      qed
    25.1 --- a/src/HOL/ex/Parallel_Example.thy	Wed Sep 14 22:07:11 2016 +0200
    25.2 +++ b/src/HOL/ex/Parallel_Example.thy	Thu Sep 15 11:48:20 2016 +0200
    25.3 @@ -9,7 +9,7 @@
    25.4  subsubsection \<open>Fragments of the harmonic series\<close>
    25.5  
    25.6  definition harmonic :: "nat \<Rightarrow> rat" where
    25.7 -  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
    25.8 +  "harmonic n = sum_list (map (\<lambda>n. 1 / of_nat n) [1..<n])"
    25.9  
   25.10  
   25.11  subsubsection \<open>The sieve of Erathostenes\<close>
    26.1 --- a/src/HOL/ex/Perm_Fragments.thy	Wed Sep 14 22:07:11 2016 +0200
    26.2 +++ b/src/HOL/ex/Perm_Fragments.thy	Thu Sep 15 11:48:20 2016 +0200
    26.3 @@ -11,8 +11,8 @@
    26.4  
    26.5  text \<open>On cycles\<close>
    26.6  
    26.7 -lemma cycle_listprod:
    26.8 -  "\<langle>a # as\<rangle> = listprod (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
    26.9 +lemma cycle_prod_list:
   26.10 +  "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
   26.11    by (induct as) simp_all
   26.12  
   26.13  lemma cycle_append [simp]:
    27.1 --- a/src/HOL/ex/Primrec.thy	Wed Sep 14 22:07:11 2016 +0200
    27.2 +++ b/src/HOL/ex/Primrec.thy	Thu Sep 15 11:48:20 2016 +0200
    27.3 @@ -224,16 +224,16 @@
    27.4  
    27.5  text \<open>MAIN RESULT\<close>
    27.6  
    27.7 -lemma SC_case: "SC l < ack 1 (listsum l)"
    27.8 +lemma SC_case: "SC l < ack 1 (sum_list l)"
    27.9  apply (unfold SC_def)
   27.10  apply (induct l)
   27.11  apply (simp_all add: le_add1 le_imp_less_Suc)
   27.12  done
   27.13  
   27.14 -lemma CONSTANT_case: "CONSTANT k l < ack k (listsum l)"
   27.15 +lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)"
   27.16  by simp
   27.17  
   27.18 -lemma PROJ_case: "PROJ i l < ack 0 (listsum l)"
   27.19 +lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)"
   27.20  apply (simp add: PROJ_def)
   27.21  apply (induct l arbitrary:i)
   27.22   apply (auto simp add: drop_Cons split: nat.split)
   27.23 @@ -243,8 +243,8 @@
   27.24  
   27.25  text \<open>@{term COMP} case\<close>
   27.26  
   27.27 -lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
   27.28 -  ==> \<exists>k. \<forall>l. listsum (map (\<lambda>f. f l) fs) < ack k (listsum l)"
   27.29 +lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
   27.30 +  ==> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)"
   27.31  apply (induct fs)
   27.32   apply (rule_tac x = 0 in exI)
   27.33   apply simp
   27.34 @@ -253,9 +253,9 @@
   27.35  done
   27.36  
   27.37  lemma COMP_case:
   27.38 -  "\<forall>l. g l < ack kg (listsum l) ==>
   27.39 -  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
   27.40 -  ==> \<exists>k. \<forall>l. COMP g fs  l < ack k (listsum l)"
   27.41 +  "\<forall>l. g l < ack kg (sum_list l) ==>
   27.42 +  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
   27.43 +  ==> \<exists>k. \<forall>l. COMP g fs  l < ack k (sum_list l)"
   27.44  apply (unfold COMP_def)
   27.45  apply (drule COMP_map_aux)
   27.46  apply (meson ack_less_mono2 ack_nest_bound less_trans)
   27.47 @@ -265,9 +265,9 @@
   27.48  text \<open>@{term PREC} case\<close>
   27.49  
   27.50  lemma PREC_case_aux:
   27.51 -  "\<forall>l. f l + listsum l < ack kf (listsum l) ==>
   27.52 -    \<forall>l. g l + listsum l < ack kg (listsum l) ==>
   27.53 -    PREC f g l + listsum l < ack (Suc (kf + kg)) (listsum l)"
   27.54 +  "\<forall>l. f l + sum_list l < ack kf (sum_list l) ==>
   27.55 +    \<forall>l. g l + sum_list l < ack kg (sum_list l) ==>
   27.56 +    PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)"
   27.57  apply (unfold PREC_def)
   27.58  apply (case_tac l)
   27.59   apply simp_all
   27.60 @@ -290,12 +290,12 @@
   27.61  done
   27.62  
   27.63  lemma PREC_case:
   27.64 -  "\<forall>l. f l < ack kf (listsum l) ==>
   27.65 -    \<forall>l. g l < ack kg (listsum l) ==>
   27.66 -    \<exists>k. \<forall>l. PREC f g l < ack k (listsum l)"
   27.67 +  "\<forall>l. f l < ack kf (sum_list l) ==>
   27.68 +    \<forall>l. g l < ack kg (sum_list l) ==>
   27.69 +    \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)"
   27.70  by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2)
   27.71  
   27.72 -lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (listsum l)"
   27.73 +lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (sum_list l)"
   27.74  apply (erule PRIMREC.induct)
   27.75      apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
   27.76  done
    28.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Wed Sep 14 22:07:11 2016 +0200
    28.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Sep 15 11:48:20 2016 +0200
    28.3 @@ -116,7 +116,7 @@
    28.4  text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
    28.5    method to help generate transfer rules.\<close>
    28.6  
    28.7 -lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
    28.8 +lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list"
    28.9    by transfer_prover
   28.10  
   28.11  end
   28.12 @@ -178,8 +178,8 @@
   28.13  
   28.14  lemma
   28.15    assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
   28.16 -    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   28.17 -  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   28.18 +    sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   28.19 +  shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   28.20  apply transfer
   28.21  apply fact
   28.22  done
   28.23 @@ -189,8 +189,8 @@
   28.24  
   28.25  lemma
   28.26    assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
   28.27 -    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
   28.28 -  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
   28.29 +    (sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs"
   28.30 +  shows "sum_list xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
   28.31  apply transfer
   28.32  apply fact
   28.33  done
   28.34 @@ -200,8 +200,8 @@
   28.35  
   28.36  lemma
   28.37    assumes "\<And>xs::int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
   28.38 -    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
   28.39 -  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
   28.40 +    sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)"
   28.41 +  shows "xs \<noteq> [] \<Longrightarrow> sum_list xs < sum_list (map Suc xs)"
   28.42  apply transfer
   28.43  apply fact
   28.44  done