diff -r fd73c5dbaad2 -r 018998c00003 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Binomial.thy	Thu Sep 15 11:48:20 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"
     by (auto simp add: neq_Nil_conv)
   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)"
         by (simp add: *)
       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