equal
deleted
inserted
replaced
140 |
140 |
141 lemma sum_list_upt[simp]: |
141 lemma sum_list_upt[simp]: |
142 "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" |
142 "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" |
143 by(simp add: distinct_sum_list_conv_Sum) |
143 by(simp add: distinct_sum_list_conv_Sum) |
144 |
144 |
145 lemma sum_list_eq_0_nat_iff_nat [simp]: |
145 lemma (in canonically_ordered_monoid_add) sum_list_eq_0_iff [simp]: |
146 "sum_list ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" |
146 "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" |
147 by (induct ns) simp_all |
147 by (induct ns) simp_all |
148 |
148 |
149 lemma member_le_sum_list_nat: |
149 lemma member_le_sum_list_nat: |
150 "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns" |
150 "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns" |
151 by (induct ns) auto |
151 by (induct ns) auto |
152 |
152 |