src/HOL/ex/Summation.thy
 changeset 35163 2e0966d6f951 child 35267 8dfd816713c6
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Summation.thy	Wed Feb 17 10:43:20 2010 +0100
1.3 @@ -0,0 +1,107 @@
1.4 +(* Author: Florian Haftmann, TU Muenchen *)
1.5 +
1.6 +header {* Some basic facts about discrete summation *}
1.7 +
1.8 +theory Summation
1.9 +imports Main
1.10 +begin
1.11 +
1.12 +text {* Auxiliary. *}
1.13 +
1.15 +  "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
1.16 +  by (fact plus.commute)
1.17 +
1.19 +  fixes j k l :: int
1.20 +  shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
1.21 +  by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
1.22 +
1.23 +text {* The shift operator. *}
1.24 +
1.25 +definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
1.26 +  "\<Delta> f k = f (k + 1) - f k"
1.27 +
1.28 +lemma \<Delta>_shift:
1.29 +  "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
1.30 +  by (simp add: \<Delta>_def expand_fun_eq)
1.31 +
1.32 +lemma \<Delta>_same_shift:
1.33 +  assumes "\<Delta> f = \<Delta> g"
1.34 +  shows "\<exists>l. (op +) l \<circ> f = g"
1.35 +proof -
1.36 +  fix k
1.37 +  from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
1.38 +  then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
1.39 +    by (simp add: \<Delta>_def algebra_simps)
1.40 +  then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
1.41 +    by blast
1.42 +  then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
1.43 +    by simp
1.44 +  have "\<And>k. f k - g k = f 0 - g 0"
1.45 +  proof -
1.46 +    fix k
1.47 +    show "f k - g k = f 0 - g 0"
1.48 +      by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
1.49 +  qed
1.50 +  then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
1.51 +    by (simp add: algebra_simps)
1.52 +  then have "(op +) (g 0 - f 0) \<circ> f = g" ..
1.53 +  then show ?thesis ..
1.54 +qed
1.55 +
1.56 +text {* The formal sum operator. *}
1.57 +
1.58 +definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
1.59 +  "\<Sigma> f j l = (if j < l then setsum f {j..<l}
1.60 +    else if j > l then - setsum f {l..<j}
1.61 +    else 0)"
1.62 +
1.63 +lemma \<Sigma>_same [simp]:
1.64 +  "\<Sigma> f j j = 0"
1.65 +  by (simp add: \<Sigma>_def)
1.66 +
1.67 +lemma \<Sigma>_positive:
1.68 +  "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
1.69 +  by (simp add: \<Sigma>_def)
1.70 +
1.71 +lemma \<Sigma>_negative:
1.72 +  "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
1.73 +  by (simp add: \<Sigma>_def)
1.74 +
1.76 +  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
1.77 +  by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
1.78 +   (simp_all add: add_setsum_orient [of f k j l]
1.79 +      add_setsum_orient [of f j l k]
1.80 +      add_setsum_orient [of f j k l] add_setsum_int)
1.81 +
1.82 +lemma \<Sigma>_incr_upper:
1.83 +  "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
1.84 +proof -
1.85 +  have "{l..<l+1} = {l}" by auto
1.86 +  then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
1.87 +  moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
1.88 +  ultimately show ?thesis by simp
1.89 +qed
1.90 +
1.91 +text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
1.92 +
1.93 +lemma \<Delta>_\<Sigma>:
1.94 +  "\<Delta> (\<Sigma> f j) = f"
1.95 +proof
1.96 +  fix k
1.97 +  show "\<Delta> (\<Sigma> f j) k = f k"
1.98 +    by (simp add: \<Delta>_def \<Sigma>_incr_upper)
1.99 +qed
1.100 +
1.101 +lemma \<Sigma>_\<Delta>:
1.102 +  "\<Sigma> (\<Delta> f) j l = f l - f j"
1.103 +proof -
1.104 +  from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
1.105 +  then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
1.106 +  then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
1.107 +  then show ?thesis by simp
1.108 +qed
1.109 +
1.110 +end
```