1.1 --- a/src/HOL/ex/ROOT.ML Wed Feb 17 09:51:46 2010 +0100
1.2 +++ b/src/HOL/ex/ROOT.ML Wed Feb 17 10:43:20 2010 +0100
1.3 @@ -66,7 +66,8 @@
1.4 "Refute_Examples",
1.5 "Quickcheck_Examples",
1.6 "Landau",
1.7 - "Execute_Choice"
1.8 + "Execute_Choice",
1.9 + "Summation"
1.10 ];
1.11
1.12 HTML.with_charset "utf-8" (no_document use_thys)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/ex/Summation.thy Wed Feb 17 10:43:20 2010 +0100
2.3 @@ -0,0 +1,107 @@
2.4 +(* Author: Florian Haftmann, TU Muenchen *)
2.5 +
2.6 +header {* Some basic facts about discrete summation *}
2.7 +
2.8 +theory Summation
2.9 +imports Main
2.10 +begin
2.11 +
2.12 +text {* Auxiliary. *}
2.13 +
2.14 +lemma add_setsum_orient:
2.15 + "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
2.16 + by (fact plus.commute)
2.17 +
2.18 +lemma add_setsum_int:
2.19 + fixes j k l :: int
2.20 + shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
2.21 + by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
2.22 +
2.23 +text {* The shift operator. *}
2.24 +
2.25 +definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
2.26 + "\<Delta> f k = f (k + 1) - f k"
2.27 +
2.28 +lemma \<Delta>_shift:
2.29 + "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
2.30 + by (simp add: \<Delta>_def expand_fun_eq)
2.31 +
2.32 +lemma \<Delta>_same_shift:
2.33 + assumes "\<Delta> f = \<Delta> g"
2.34 + shows "\<exists>l. (op +) l \<circ> f = g"
2.35 +proof -
2.36 + fix k
2.37 + from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
2.38 + then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
2.39 + by (simp add: \<Delta>_def algebra_simps)
2.40 + then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
2.41 + by blast
2.42 + then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
2.43 + by simp
2.44 + have "\<And>k. f k - g k = f 0 - g 0"
2.45 + proof -
2.46 + fix k
2.47 + show "f k - g k = f 0 - g 0"
2.48 + by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
2.49 + qed
2.50 + then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
2.51 + by (simp add: algebra_simps)
2.52 + then have "(op +) (g 0 - f 0) \<circ> f = g" ..
2.53 + then show ?thesis ..
2.54 +qed
2.55 +
2.56 +text {* The formal sum operator. *}
2.57 +
2.58 +definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
2.59 + "\<Sigma> f j l = (if j < l then setsum f {j..<l}
2.60 + else if j > l then - setsum f {l..<j}
2.61 + else 0)"
2.62 +
2.63 +lemma \<Sigma>_same [simp]:
2.64 + "\<Sigma> f j j = 0"
2.65 + by (simp add: \<Sigma>_def)
2.66 +
2.67 +lemma \<Sigma>_positive:
2.68 + "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
2.69 + by (simp add: \<Sigma>_def)
2.70 +
2.71 +lemma \<Sigma>_negative:
2.72 + "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
2.73 + by (simp add: \<Sigma>_def)
2.74 +
2.75 +lemma add_\<Sigma>:
2.76 + "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
2.77 + by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
2.78 + (simp_all add: add_setsum_orient [of f k j l]
2.79 + add_setsum_orient [of f j l k]
2.80 + add_setsum_orient [of f j k l] add_setsum_int)
2.81 +
2.82 +lemma \<Sigma>_incr_upper:
2.83 + "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
2.84 +proof -
2.85 + have "{l..<l+1} = {l}" by auto
2.86 + then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
2.87 + moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
2.88 + ultimately show ?thesis by simp
2.89 +qed
2.90 +
2.91 +text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
2.92 +
2.93 +lemma \<Delta>_\<Sigma>:
2.94 + "\<Delta> (\<Sigma> f j) = f"
2.95 +proof
2.96 + fix k
2.97 + show "\<Delta> (\<Sigma> f j) k = f k"
2.98 + by (simp add: \<Delta>_def \<Sigma>_incr_upper)
2.99 +qed
2.100 +
2.101 +lemma \<Sigma>_\<Delta>:
2.102 + "\<Sigma> (\<Delta> f) j l = f l - f j"
2.103 +proof -
2.104 + from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
2.105 + then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
2.106 + then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
2.107 + then show ?thesis by simp
2.108 +qed
2.109 +
2.110 +end