helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
  20
  21 (*#* printing Sum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
  22
  23 (*#* printing Sum1 %\ensuremath{\sum_1}% #&sum;<sub>1</sub># *)
  24
  25 (*#* printing Sum2 %\ensuremath{\sum_2}% #&sum;<sub>2</sub># *)
  26
  27 (*#* printing Sum %\ensuremath{\sum}% #&sum;# *)
  28
  29 (*#* printing Sumx %\ensuremath{\sum'}% #&sum;'&*)
  30
  31 include "algebra/CAbGroups.ma".
  32
  33 (*#* * Sums
  34
  35 %\begin{convention}% Let [G] be an abelian group.
  36 %\end{convention}%
  37 *)
  38
  39 (* UNEXPORTED
  40 Section Sums
  41 *)
  42
  43 alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var".
  44
  45 (* Sum1 and Sum use subtraction *)
  46
  47 inline procedural "cic:/CoRN/algebra/CSums/Sumlist.con" as definition.
  48
  49 inline procedural "cic:/CoRN/algebra/CSums/Sumx.con" as definition.
  50
  51 (*#*
  52 It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
  53 #{0, ... i-1}# as a function on the natural numbers which evaluates to
  54 [Zero] when the input is greater than or equal to [i].
  55 *)
  56
  57 inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con" as definition.
  58
  59 inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con" as lemma.
  60
  61 inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con" as lemma.
  62
  63 (*#* [Sum0] defines the sum for [i=0..(n-1)] *)
  64
  65 inline procedural "cic:/CoRN/algebra/CSums/Sum0.con" as definition.
  66
  67 (*#* [Sum1] defines the sum for [i=m..(n-1)] *)
  68
  69 inline procedural "cic:/CoRN/algebra/CSums/Sum1.con" as definition.
  70
  71 inline procedural "cic:/CoRN/algebra/CSums/Sum.con" as definition.
  72
  73 (* Sum i=m..n *)
  74
  75 (*#* [Sum2] is similar to [Sum1], but does not require the summand to be
  76 defined outside where it is being added. *)
  77
  78 inline procedural "cic:/CoRN/algebra/CSums/Sum2.con" as definition.
  79
  80 inline procedural "cic:/CoRN/algebra/CSums/Sum_one.con" as lemma.
  81
  82 (* UNEXPORTED
  83 Hint Resolve Sum_one: algebra.
  84 *)
  85
  86 inline procedural "cic:/CoRN/algebra/CSums/Sum_empty.con" as lemma.
  87
  88 (* UNEXPORTED
  89 Hint Resolve Sum_empty: algebra.
  90 *)
  91
  92 inline procedural "cic:/CoRN/algebra/CSums/Sum_Sum.con" as lemma.
  93
  94 (* UNEXPORTED
  95 Hint Resolve Sum_Sum: algebra.
  96 *)
  97
  98 inline procedural "cic:/CoRN/algebra/CSums/Sum_first.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/algebra/CSums/Sum_last.con" as lemma.
 101
 102 (* UNEXPORTED
 103 Hint Resolve Sum_last: algebra.
 104 *)
 105
 106 inline procedural "cic:/CoRN/algebra/CSums/Sum_last'.con" as lemma.
 107
 108 (*#*
 109 We add some extensionality results which will be quite useful
 110 when working with integration.
 111 *)
 112
 113 inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext.con" as lemma.
 114
 115 inline procedural "cic:/CoRN/algebra/CSums/Sum_strext.con" as lemma.
 116
 117 inline procedural "cic:/CoRN/algebra/CSums/Sumx_strext.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext'.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/algebra/CSums/Sum_strext'.con" as lemma.
 122
 123 inline procedural "cic:/CoRN/algebra/CSums/Sum0_wd.con" as lemma.
 124
 125 inline procedural "cic:/CoRN/algebra/CSums/Sum_wd.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/algebra/CSums/Sumx_wd.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/algebra/CSums/Sum_wd'.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/algebra/CSums/Sum2_wd.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con" as lemma.
 134
 135 (* UNEXPORTED
 136 Hint Resolve Sum0_plus_Sum0: algebra.
 137 *)
 138
 139 inline procedural "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con" as lemma.
 140
 141 inline procedural "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con" as lemma.
 142
 143 inline procedural "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con" as lemma.
 144
 145 inline procedural "cic:/CoRN/algebra/CSums/inv_Sum0.con" as lemma.
 146
 147 (* UNEXPORTED
 148 Hint Resolve inv_Sum0: algebra.
 149 *)
 150
 151 inline procedural "cic:/CoRN/algebra/CSums/inv_Sum.con" as lemma.
 152
 153 (* UNEXPORTED
 154 Hint Resolve inv_Sum: algebra.
 155 *)
 156
 157 inline procedural "cic:/CoRN/algebra/CSums/inv_Sumx.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/algebra/CSums/inv_Sum2.con" as lemma.
 160
 161 inline procedural "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con" as lemma.
 162
 163 (* UNEXPORTED
 164 Hint Resolve Sum_minus_Sum: algebra.
 165 *)
 166
 167 inline procedural "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con" as lemma.
 168
 169 inline procedural "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con" as lemma.
 170
 171 inline procedural "cic:/CoRN/algebra/CSums/Sum_apzero.con" as lemma.
 172
 173 inline procedural "cic:/CoRN/algebra/CSums/Sum_zero.con" as lemma.
 174
 175 inline procedural "cic:/CoRN/algebra/CSums/Sum_term.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/algebra/CSums/Sum0_shift.con" as lemma.
 178
 179 (* UNEXPORTED
 180 Hint Resolve Sum0_shift: algebra.
 181 *)
 182
 183 inline procedural "cic:/CoRN/algebra/CSums/Sum_shift.con" as lemma.
 184
 185 inline procedural "cic:/CoRN/algebra/CSums/Sum_big_shift.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/algebra/CSums/Sumx_Sum0.con" as lemma.
 188
 189 (* UNEXPORTED
 190 End Sums
 191 *)
 192
 193 (* UNEXPORTED
 194 Implicit Arguments Sum [G].
 195 *)
 196
 197 (* UNEXPORTED
 198 Implicit Arguments Sum0 [G].
 199 *)
 200
 201 (* UNEXPORTED
 202 Implicit Arguments Sumx [G n].
 203 *)
 204
 205 (* UNEXPORTED
 206 Implicit Arguments Sum2 [G m n].
 207 *)
 208
 209 (*#*
 210 The next results are useful for calculating some special sums,
 211 often referred to as ``Mengolli Sums''.
 212 %\begin{convention}% Let [G] be an abelian group.
 213 %\end{convention}%
 214 *)
 215
 216 (* UNEXPORTED
 217 Section More_Sums
 218 *)
 219
 220 alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var".
 221
 222 inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum.con" as lemma.
 223
 224 inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con" as lemma.
 225
 226 inline procedural "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con" as lemma.
 227
 228 inline procedural "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con" as lemma.
 229
 230 (* UNEXPORTED
 231 End More_Sums
 232 *)
 233
 234 (* UNEXPORTED
 235 Hint Resolve Sum_one Sum_Sum Sum_first Sum_last Sum_last' Sum_wd
 236   Sum_plus_Sum: algebra.
 237 *)
 238
 239 (* UNEXPORTED
 240 Hint Resolve Sum_minus_Sum inv_Sum inv_Sum0: algebra.
 241 *)
 242