src/HOL/ex/Summation.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 39302 d7728f65b353 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
 haftmann@35163 ` 1` ```(* Author: Florian Haftmann, TU Muenchen *) ``` haftmann@35163 ` 2` haftmann@35163 ` 3` ```header {* Some basic facts about discrete summation *} ``` haftmann@35163 ` 4` haftmann@35163 ` 5` ```theory Summation ``` haftmann@35163 ` 6` ```imports Main ``` haftmann@35163 ` 7` ```begin ``` haftmann@35163 ` 8` haftmann@35163 ` 9` ```text {* Auxiliary. *} ``` haftmann@35163 ` 10` haftmann@35163 ` 11` ```lemma add_setsum_orient: ``` haftmann@35163 ` 12` ``` "setsum f {k.. k < l \ setsum f {j.. :: "(int \ 'a\ab_group_add) \ int \ 'a" where ``` haftmann@35163 ` 23` ``` "\ f k = f (k + 1) - f k" ``` haftmann@35163 ` 24` haftmann@35163 ` 25` ```lemma \_shift: ``` haftmann@35163 ` 26` ``` "\ (\k. l + f k) = \ f" ``` nipkow@39302 ` 27` ``` by (simp add: \_def fun_eq_iff) ``` haftmann@35163 ` 28` haftmann@35163 ` 29` ```lemma \_same_shift: ``` haftmann@35163 ` 30` ``` assumes "\ f = \ g" ``` haftmann@35267 ` 31` ``` shows "\l. plus l \ f = g" ``` haftmann@35163 ` 32` ```proof - ``` haftmann@35163 ` 33` ``` fix k ``` haftmann@35163 ` 34` ``` from assms have "\k. \ f k = \ g k" by simp ``` haftmann@35163 ` 35` ``` then have k_incr: "\k. f (k + 1) - g (k + 1) = f k - g k" ``` haftmann@35163 ` 36` ``` by (simp add: \_def algebra_simps) ``` haftmann@35163 ` 37` ``` then have "\k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)" ``` haftmann@35163 ` 38` ``` by blast ``` haftmann@35163 ` 39` ``` then have k_decr: "\k. f (k - 1) - g (k - 1) = f k - g k" ``` haftmann@35163 ` 40` ``` by simp ``` haftmann@35163 ` 41` ``` have "\k. f k - g k = f 0 - g 0" ``` haftmann@35163 ` 42` ``` proof - ``` haftmann@35163 ` 43` ``` fix k ``` haftmann@35163 ` 44` ``` show "f k - g k = f 0 - g 0" ``` haftmann@36811 ` 45` ``` by (induct k rule: int_induct) (simp_all add: k_incr k_decr) ``` haftmann@35163 ` 46` ``` qed ``` haftmann@35267 ` 47` ``` then have "\k. (plus (g 0 - f 0) \ f) k = g k" ``` haftmann@35163 ` 48` ``` by (simp add: algebra_simps) ``` haftmann@35267 ` 49` ``` then have "plus (g 0 - f 0) \ f = g" .. ``` haftmann@35163 ` 50` ``` then show ?thesis .. ``` haftmann@35163 ` 51` ```qed ``` haftmann@35163 ` 52` haftmann@35163 ` 53` ```text {* The formal sum operator. *} ``` haftmann@35163 ` 54` haftmann@35163 ` 55` ```definition \ :: "(int \ 'a\ab_group_add) \ int \ int \ 'a" where ``` haftmann@35163 ` 56` ``` "\ f j l = (if j < l then setsum f {j.. l then - setsum f {l.._same [simp]: ``` haftmann@35163 ` 61` ``` "\ f j j = 0" ``` haftmann@35163 ` 62` ``` by (simp add: \_def) ``` haftmann@35163 ` 63` haftmann@35163 ` 64` ```lemma \_positive: ``` haftmann@35163 ` 65` ``` "j < l \ \ f j l = setsum f {j.._def) ``` haftmann@35163 ` 67` haftmann@35163 ` 68` ```lemma \_negative: ``` haftmann@35163 ` 69` ``` "j > l \ \ f j l = - \ f l j" ``` haftmann@35163 ` 70` ``` by (simp add: \_def) ``` haftmann@35163 ` 71` haftmann@35163 ` 72` ```lemma add_\: ``` haftmann@35163 ` 73` ``` "\ f j k + \ f k l = \ f j l" ``` haftmann@35163 ` 74` ``` by (simp add: \_def algebra_simps add_setsum_int) ``` haftmann@35163 ` 75` ``` (simp_all add: add_setsum_orient [of f k j l] ``` haftmann@35163 ` 76` ``` add_setsum_orient [of f j l k] ``` haftmann@35163 ` 77` ``` add_setsum_orient [of f j k l] add_setsum_int) ``` haftmann@35163 ` 78` haftmann@35163 ` 79` ```lemma \_incr_upper: ``` haftmann@35163 ` 80` ``` "\ f j (l + 1) = \ f j l + f l" ``` haftmann@35163 ` 81` ```proof - ``` haftmann@35163 ` 82` ``` have "{l.. f l (l + 1) = f l" by (simp add: \_def) ``` haftmann@35163 ` 84` ``` moreover have "\ f j (l + 1) = \ f j l + \ f l (l + 1)" by (simp add: add_\) ``` haftmann@35163 ` 85` ``` ultimately show ?thesis by simp ``` haftmann@35163 ` 86` ```qed ``` haftmann@35163 ` 87` haftmann@35163 ` 88` ```text {* Fundamental lemmas: The relation between @{term \} and @{term \}. *} ``` haftmann@35163 ` 89` haftmann@35163 ` 90` ```lemma \_\: ``` haftmann@35163 ` 91` ``` "\ (\ f j) = f" ``` haftmann@35163 ` 92` ```proof ``` haftmann@35163 ` 93` ``` fix k ``` haftmann@35163 ` 94` ``` show "\ (\ f j) k = f k" ``` haftmann@35163 ` 95` ``` by (simp add: \_def \_incr_upper) ``` haftmann@35163 ` 96` ```qed ``` haftmann@35163 ` 97` haftmann@35163 ` 98` ```lemma \_\: ``` haftmann@35163 ` 99` ``` "\ (\ f) j l = f l - f j" ``` haftmann@35163 ` 100` ```proof - ``` haftmann@35163 ` 101` ``` from \_\ have "\ (\ (\ f) j) = \ f" . ``` haftmann@35267 ` 102` ``` then obtain k where "plus k \ \ (\ f) j = f" by (blast dest: \_same_shift) ``` nipkow@39302 ` 103` ``` then have "\q. f q = k + \ (\ f) j q" by (simp add: fun_eq_iff) ``` haftmann@35163 ` 104` ``` then show ?thesis by simp ``` haftmann@35163 ` 105` ```qed ``` haftmann@35163 ` 106` haftmann@35163 ` 107` ```end ```