author haftmann Thu Apr 24 10:33:17 2014 +0200 (2014-04-24) changeset 56680 4e2a0d4e7a82 parent 56679 5545bfdfefcc child 56681 e8d5d60d655e
now covered by AFP 3ddac3e572cf
 src/HOL/ROOT file | annotate | diff | revisions src/HOL/ex/Summation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/ROOT	Thu Apr 24 00:23:38 2014 +0200
1.2 +++ b/src/HOL/ROOT	Thu Apr 24 10:33:17 2014 +0200
1.3 @@ -560,7 +560,6 @@
1.4      HarmonicSeries
1.5      Refute_Examples
1.6      Execute_Choice
1.7 -    Summation
1.8      Gauge_Integration
1.9      Dedekind_Real
1.10      Quicksort
```
```     2.1 --- a/src/HOL/ex/Summation.thy	Thu Apr 24 00:23:38 2014 +0200
2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,107 +0,0 @@
2.4 -(* Author: Florian Haftmann, TU Muenchen *)
2.5 -
2.7 -
2.8 -theory Summation
2.9 -imports Main
2.10 -begin
2.11 -
2.12 -text {* Auxiliary. *}
2.13 -
2.15 -  "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
2.17 -
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 fun_eq_iff)
2.31 -
2.32 -lemma \<Delta>_same_shift:
2.33 -  assumes "\<Delta> f = \<Delta> g"
2.34 -  shows "\<exists>l. plus 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. (plus (g 0 - f 0) \<circ> f) k = g k"
2.51 -    by (simp add: algebra_simps)
2.52 -  then have "plus (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.76 -  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
2.79 -      add_setsum_orient [of f j l k]
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 "plus 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: fun_eq_iff)
2.107 -  then show ?thesis by simp
2.108 -qed
2.109 -
2.110 -end
```