--- a/src/HOL/Binomial.thy Thu Aug 03 07:31:25 2017 +0200
+++ b/src/HOL/Binomial.thy Thu Aug 03 09:30:09 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
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Aug 03 07:31:25 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Aug 03 09:30:09 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)
--- a/src/HOL/Groups_List.thy Thu Aug 03 07:31:25 2017 +0200
+++ b/src/HOL/Groups_List.thy Thu Aug 03 09:30:09 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"
--- a/src/HOL/Proofs/Lambda/ListApplication.thy Thu Aug 03 07:31:25 2017 +0200
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy Thu Aug 03 09:30:09 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: