author nipkow Thu, 03 Aug 2017 09:30:09 +0200 changeset 66311 037aaa0b6daf parent 66309 ca985e87c123 child 66312 9a4c049f8997
 src/HOL/Binomial.thy file | annotate | diff | comparison | revisions src/HOL/Computational_Algebra/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/Groups_List.thy file | annotate | diff | comparison | revisions src/HOL/Proofs/Lambda/ListApplication.thy file | annotate | diff | comparison | revisions
```--- 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}"

-  "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-by (induct ns) simp_all
+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)"
+
+end
+
+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)"
+
+lemma member_le_sum_list:
+  "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs"

-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)

```--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Aug 03 07:31:25 2017 +0200