equal
deleted
inserted
replaced
1993 from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto |
1993 from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto |
1994 also have "F g \<dots> = g (Suc n) \<^bold>* F g {m..n}" by simp |
1994 also have "F g \<dots> = g (Suc n) \<^bold>* F g {m..n}" by simp |
1995 finally show ?thesis . |
1995 finally show ?thesis . |
1996 qed |
1996 qed |
1997 |
1997 |
|
1998 lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}" |
|
1999 proof (induction n) |
|
2000 case 0 |
|
2001 show ?case |
|
2002 by (cases "m=0") auto |
|
2003 next |
|
2004 case (Suc n) |
|
2005 then show ?case |
|
2006 by (auto simp: assoc split: if_split_asm) |
|
2007 qed |
|
2008 |
|
2009 lemma in_pairs_0: "F g {..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}" |
|
2010 using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) |
|
2011 |
1998 end |
2012 end |
1999 |
2013 |
2000 lemma sum_natinterval_diff: |
2014 lemma sum_natinterval_diff: |
2001 fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" |
2015 fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" |
2002 shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} = |
2016 shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} = |