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..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
haftmann@35732
    13
  by (fact add.commute)
haftmann@35163
    14
haftmann@35163
    15
lemma add_setsum_int:
haftmann@35163
    16
  fixes j k l :: int
haftmann@35163
    17
  shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
haftmann@35163
    18
  by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
haftmann@35163
    19
haftmann@35163
    20
text {* The shift operator. *}
haftmann@35163
    21
haftmann@35163
    22
definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
haftmann@35163
    23
  "\<Delta> f k = f (k + 1) - f k"
haftmann@35163
    24
haftmann@35163
    25
lemma \<Delta>_shift:
haftmann@35163
    26
  "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
nipkow@39302
    27
  by (simp add: \<Delta>_def fun_eq_iff)
haftmann@35163
    28
haftmann@35163
    29
lemma \<Delta>_same_shift:
haftmann@35163
    30
  assumes "\<Delta> f = \<Delta> g"
haftmann@35267
    31
  shows "\<exists>l. plus l \<circ> f = g"
haftmann@35163
    32
proof -
haftmann@35163
    33
  fix k
haftmann@35163
    34
  from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
haftmann@35163
    35
  then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
haftmann@35163
    36
    by (simp add: \<Delta>_def algebra_simps)
haftmann@35163
    37
  then have "\<And>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: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
haftmann@35163
    40
    by simp
haftmann@35163
    41
  have "\<And>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 "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
haftmann@35163
    48
    by (simp add: algebra_simps)
haftmann@35267
    49
  then have "plus (g 0 - f 0) \<circ> 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 \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
haftmann@35163
    56
  "\<Sigma> f j l = (if j < l then setsum f {j..<l}
haftmann@35163
    57
    else if j > l then - setsum f {l..<j}
haftmann@35163
    58
    else 0)"
haftmann@35163
    59
haftmann@35163
    60
lemma \<Sigma>_same [simp]:
haftmann@35163
    61
  "\<Sigma> f j j = 0"
haftmann@35163
    62
  by (simp add: \<Sigma>_def)
haftmann@35163
    63
haftmann@35163
    64
lemma \<Sigma>_positive:
haftmann@35163
    65
  "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
haftmann@35163
    66
  by (simp add: \<Sigma>_def)
haftmann@35163
    67
haftmann@35163
    68
lemma \<Sigma>_negative:
haftmann@35163
    69
  "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
haftmann@35163
    70
  by (simp add: \<Sigma>_def)
haftmann@35163
    71
haftmann@35163
    72
lemma add_\<Sigma>:
haftmann@35163
    73
  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
haftmann@35163
    74
  by (simp add: \<Sigma>_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 \<Sigma>_incr_upper:
haftmann@35163
    80
  "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
haftmann@35163
    81
proof -
haftmann@35163
    82
  have "{l..<l+1} = {l}" by auto
haftmann@35163
    83
  then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
haftmann@35163
    84
  moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
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 \<Delta>} and @{term \<Sigma>}. *}
haftmann@35163
    89
haftmann@35163
    90
lemma \<Delta>_\<Sigma>:
haftmann@35163
    91
  "\<Delta> (\<Sigma> f j) = f"
haftmann@35163
    92
proof
haftmann@35163
    93
  fix k
haftmann@35163
    94
  show "\<Delta> (\<Sigma> f j) k = f k"
haftmann@35163
    95
    by (simp add: \<Delta>_def \<Sigma>_incr_upper)
haftmann@35163
    96
qed
haftmann@35163
    97
haftmann@35163
    98
lemma \<Sigma>_\<Delta>:
haftmann@35163
    99
  "\<Sigma> (\<Delta> f) j l = f l - f j"
haftmann@35163
   100
proof -
haftmann@35163
   101
  from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
haftmann@35267
   102
  then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
nipkow@39302
   103
  then have "\<And>q. f q = k + \<Sigma> (\<Delta> 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