helm/software/matita/contribs/procedural/CoRN/ftc/DerivativeOps.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: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 include "ftc/Derivative.ma".
  22
  23 (* UNEXPORTED
  24 Section Lemmas
  25 *)
  26
  27 (*#* **Algebraic Operations
  28
  29 We will now prove the main results about deriving functions built from
  30 the algebraic operators#. #%\footnote{%Composition presents some
  31 tricky questions, and is therefore discussed in a separated
  32 context.%}.%
  33
  34 [F'] and [G'] will be the derivatives, respectively, of [F] and [G].
  35
  36 We begin with some technical stuff that will be necessary for division.
  37 *)
  38
  39 (* UNEXPORTED
  40 cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var
  41 *)
  42
  43 (* UNEXPORTED
  44 cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var
  45 *)
  46
  47 (* UNEXPORTED
  48 cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var
  49 *)
  50
  51 (* begin hide *)
  52
  53 inline procedural "cic:/CoRN/ftc/DerivativeOps/Lemmas/I.con" "Lemmas__" as definition.
  54
  55 (* end hide *)
  56
  57 (* UNEXPORTED
  58 cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var
  59 *)
  60
  61 (* begin hide *)
  62
  63 inline procedural "cic:/CoRN/ftc/DerivativeOps/Lemmas/P.con" "Lemmas__" as definition.
  64
  65 (* end hide *)
  66
  67 (* begin show *)
  68
  69 (* UNEXPORTED
  70 cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var
  71 *)
  72
  73 (* end show *)
  74
  75 inline procedural "cic:/CoRN/ftc/DerivativeOps/bnd_away_zero_square.con" as lemma.
  76
  77 (* UNEXPORTED
  78 End Lemmas
  79 *)
  80
  81 (* UNEXPORTED
  82 Hint Resolve bnd_away_zero_square: included.
  83 *)
  84
  85 (* UNEXPORTED
  86 Section Local_Results
  87 *)
  88
  89 (*#* **Local Results
  90
  91 We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative.
  92 *)
  93
  94 (* UNEXPORTED
  95 cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var
  96 *)
  97
  98 (* UNEXPORTED
  99 cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var
 100 *)
 101
 102 (* UNEXPORTED
 103 cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var
 104 *)
 105
 106 (* begin hide *)
 107
 108 inline procedural "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab.con" "Local_Results__" as definition.
 109
 110 inline procedural "cic:/CoRN/ftc/DerivativeOps/Local_Results/I.con" "Local_Results__" as definition.
 111
 112 (* end hide *)
 113
 114 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con" as lemma.
 115
 116 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con" as lemma.
 117
 118 (* UNEXPORTED
 119 cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var
 120 *)
 121
 122 (* UNEXPORTED
 123 cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var
 124 *)
 125
 126 (* UNEXPORTED
 127 cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var
 128 *)
 129
 130 (* UNEXPORTED
 131 cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var
 132 *)
 133
 134 (* UNEXPORTED
 135 cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var
 136 *)
 137
 138 (* UNEXPORTED
 139 cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var
 140 *)
 141
 142 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con" as lemma.
 143
 144 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_inv.con" as lemma.
 145
 146 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_mult.con" as lemma.
 147
 148 (*#*
 149 As was the case for continuity, the rule for the reciprocal function has a side condition.
 150 *)
 151
 152 (* begin show *)
 153
 154 (* UNEXPORTED
 155 cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var
 156 *)
 157
 158 (* end show *)
 159
 160 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_recip.con" as lemma.
 161
 162 (* UNEXPORTED
 163 End Local_Results
 164 *)
 165
 166 (* UNEXPORTED
 167 Hint Immediate derivative_imp_inc derivative_imp_inc': included.
 168 *)
 169
 170 (* UNEXPORTED
 171 Hint Resolve Derivative_I_const Derivative_I_id Derivative_I_plus
 172   Derivative_I_inv Derivative_I_mult Derivative_I_recip: derivate.
 173 *)
 174
 175 (* UNEXPORTED
 176 Section Corolaries
 177 *)
 178
 179 (* UNEXPORTED
 180 cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var
 181 *)
 182
 183 (* UNEXPORTED
 184 cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var
 185 *)
 186
 187 (* UNEXPORTED
 188 cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var
 189 *)
 190
 191 (* begin hide *)
 192
 193 inline procedural "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab.con" "Corolaries__" as definition.
 194
 195 inline procedural "cic:/CoRN/ftc/DerivativeOps/Corolaries/I.con" "Corolaries__" as definition.
 196
 197 (* end hide *)
 198
 199 (* UNEXPORTED
 200 cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var
 213 *)
 214
 215 (* UNEXPORTED
 216 cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var
 217 *)
 218
 219 (* UNEXPORTED
 220 cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var
 221 *)
 222
 223 (*#*
 224 From this lemmas the rules for the other algebraic operations follow directly.
 225 *)
 226
 227 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_minus.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con" as lemma.
 232
 233 (* UNEXPORTED
 234 cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var
 235 *)
 236
 237 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con" as lemma.
 238
 239 (* UNEXPORTED
 240 End Corolaries
 241 *)
 242
 243 (* UNEXPORTED
 244 Hint Resolve Derivative_I_minus Derivative_I_nth Derivative_I_scal
 245   Derivative_I_div: derivate.
 246 *)
 247
 248 (* UNEXPORTED
 249 Section Derivative_Sums
 250 *)
 251
 252 (*#* The derivation rules for families of functions are easily proved by
 253 induction using the constant and addition rules.
 254 *)
 255
 256 (* UNEXPORTED
 257 cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var
 258 *)
 259
 260 (* UNEXPORTED
 261 cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var
 262 *)
 263
 264 (* UNEXPORTED
 265 cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var
 266 *)
 267
 268 (* UNEXPORTED
 269 cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var
 270 *)
 271
 272 (* begin hide *)
 273
 274 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/I.con" "Derivative_Sums__" as definition.
 275
 276 (* end hide *)
 277
 278 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum0.con" as lemma.
 279
 280 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con" as lemma.
 281
 282 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con" as lemma.
 283
 284 (* UNEXPORTED
 285 End Derivative_Sums
 286 *)
 287
 288 (* UNEXPORTED
 289 Hint Resolve Derivative_I_Sum0 Derivative_I_Sum Derivative_I_Sumx: derivate.
 290 *)
 291