# HG changeset patch
# User nipkow
# Date 1501753135 -7200
# Node ID 9a4c049f899735e5aee85948dce71558bf994fbe
# Parent  e8d2862ec203087e67f157503f172d37bf1919cc# Parent  037aaa0b6dafc731a56776621dfc66b9a4f840bb
merged

diff -r e8d2862ec203 -r 9a4c049f8997 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Aug 02 20:33:39 2017 +0200
+++ b/src/HOL/Binomial.thy	Thu Aug 03 11:38:55 2017 +0200
@@ -1177,10 +1177,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_sum_list_nat less_Suc_eq_le)
+      (auto simp: member_le_sum_list 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_sum_list_nat less_Suc_eq_le fin)
+      (auto simp: member_le_sum_list less_Suc_eq_le fin)
   have uni: "?C = ?A' \<union> ?B'"
     by auto
   have disj: "?A' \<inter> ?B' = {}" by blast
diff -r e8d2862ec203 -r 9a4c049f8997 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Aug 02 20:33:39 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Aug 03 11:38:55 2017 +0200
@@ -2487,7 +2487,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_sum_list_nat[of i v] unfolding natpermute_def
+        using that elem_le_sum_list[of i v] unfolding natpermute_def
         by (auto simp: set_conv_nth dest!: spec[of _ i])
       hence "?h f = ?h g"
         by (intro sum.cong refl prod.cong less lessI) (auto simp: natpermute_def)
diff -r e8d2862ec203 -r 9a4c049f8997 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Aug 02 20:33:39 2017 +0200
+++ b/src/HOL/Groups_List.thy	Thu Aug 03 11:38:55 2017 +0200
@@ -142,25 +142,44 @@
   "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
 by(simp add: distinct_sum_list_conv_Sum)
 
-lemma (in canonically_ordered_monoid_add) sum_list_eq_0_iff [simp]:
-  "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-by (induct ns) simp_all
+context ordered_comm_monoid_add
+begin
+
+lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs"
+by (induction xs) auto
+
+lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0"
+by (induction xs) (auto simp: add_nonpos_nonpos)
 
-lemma member_le_sum_list_nat:
-  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns"
-  by (induct ns) auto
+lemma sum_list_nonneg_eq_0_iff:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)"
+by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
+
+end
+
+context canonically_ordered_monoid_add
+begin
 
-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 sum_list_eq_0_iff [simp]:
+  "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
+by (simp add: sum_list_nonneg_eq_0_iff)
+
+lemma member_le_sum_list:
+  "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs"
+by (induction xs) (auto simp: add_increasing add_increasing2)
 
-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_sum_list_nat)
-apply arith
-done
+lemma elem_le_sum_list:
+  "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)"
+by (rule member_le_sum_list) simp
+
+end
+
+lemma (in ordered_cancel_comm_monoid_diff) sum_list_update:
+  "k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k"
+apply(induction xs arbitrary:k)
+ apply (auto simp: add_ac split: nat.split)
+apply(drule elem_le_sum_list)
+by (simp add: local.add_diff_assoc local.add_increasing)
 
 lemma (in monoid_add) sum_list_triv:
   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
diff -r e8d2862ec203 -r 9a4c049f8997 src/HOL/Proofs/Lambda/ListApplication.thy
--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Wed Aug 02 20:33:39 2017 +0200
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Aug 03 11:38:55 2017 +0200
@@ -127,7 +127,7 @@
   apply (rule trans_le_add1)
   apply (rule trans_le_add2)
   apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
-  apply (simp add: member_le_sum_list_nat)
+  apply (simp add: member_le_sum_list)
   done
 
 theorem Apps_dB_induct: