equal
deleted
inserted
replaced
42 lemma setprod_lessThan_Suc[simp]: |
42 lemma setprod_lessThan_Suc[simp]: |
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
44 by (simp add:lessThan_Suc mult_ac) |
44 by (simp add:lessThan_Suc mult_ac) |
45 |
45 |
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
47 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
47 sum f {..<n} + sum f {n..p} = sum f {..p::nat}" |
48 apply(subst setsum.union_disjoint[symmetric]) |
48 apply(subst sum.union_disjoint[symmetric]) |
49 apply(auto simp add: ivl_disj_un_one) |
49 apply(auto simp add: ivl_disj_un_one) |
50 done |
50 done |
51 |
51 |
52 lemma setsum_eq_zero [simp]: |
52 lemma setsum_eq_zero [simp]: |
53 fixes f::"nat \<Rightarrow> nat" |
53 fixes f::"nat \<Rightarrow> nat" |
131 shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" |
131 shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" |
132 proof - |
132 proof - |
133 have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" |
133 have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" |
134 using h2 by auto |
134 using h2 by auto |
135 have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)" |
135 have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)" |
136 using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) |
136 using h1 by (metis atLeast0LessThan le0 sum_add_nat_ivl) |
137 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
137 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
138 finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp |
138 finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp |
139 qed |
139 qed |
140 |
140 |
141 lemma setsum_cut_off_le: |
141 lemma setsum_cut_off_le: |