helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var".
  40
  41 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var".
  42
  43 alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var".
  44
  45 (* begin hide *)
  46
  47 inline procedural "cic:/CoRN/ftc/DerivativeOps/Lemmas/I.con" "Lemmas__".
  48
  49 (* end hide *)
  50
  51 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var".
  52
  53 (* begin hide *)
  54
  55 inline procedural "cic:/CoRN/ftc/DerivativeOps/Lemmas/P.con" "Lemmas__".
  56
  57 (* end hide *)
  58
  59 (* begin show *)
  60
  61 alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var".
  62
  63 (* end show *)
  64
  65 inline procedural "cic:/CoRN/ftc/DerivativeOps/bnd_away_zero_square.con".
  66
  67 (* UNEXPORTED
  68 End Lemmas
  69 *)
  70
  71 (* UNEXPORTED
  72 Hint Resolve bnd_away_zero_square: included.
  73 *)
  74
  75 (* UNEXPORTED
  76 Section Local_Results
  77 *)
  78
  79 (*#* **Local Results
  80
  81 We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative.
  82 *)
  83
  84 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var".
  85
  86 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var".
  87
  88 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var".
  89
  90 (* begin hide *)
  91
  92 inline procedural "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab.con" "Local_Results__".
  93
  94 inline procedural "cic:/CoRN/ftc/DerivativeOps/Local_Results/I.con" "Local_Results__".
  95
  96 (* end hide *)
  97
  98 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con".
  99
 100 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con".
 101
 102 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var".
 103
 104 alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var".
 105
 106 alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var".
 107
 108 alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var".
 109
 110 alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var".
 111
 112 alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var".
 113
 114 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con".
 115
 116 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_inv.con".
 117
 118 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_mult.con".
 119
 120 (*#*
 121 As was the case for continuity, the rule for the reciprocal function has a side condition.
 122 *)
 123
 124 (* begin show *)
 125
 126 alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var".
 127
 128 (* end show *)
 129
 130 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_recip.con".
 131
 132 (* UNEXPORTED
 133 End Local_Results
 134 *)
 135
 136 (* UNEXPORTED
 137 Hint Immediate derivative_imp_inc derivative_imp_inc': included.
 138 *)
 139
 140 (* UNEXPORTED
 141 Hint Resolve Derivative_I_const Derivative_I_id Derivative_I_plus
 142   Derivative_I_inv Derivative_I_mult Derivative_I_recip: derivate.
 143 *)
 144
 145 (* UNEXPORTED
 146 Section Corolaries
 147 *)
 148
 149 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var".
 150
 151 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var".
 152
 153 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var".
 154
 155 (* begin hide *)
 156
 157 inline procedural "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab.con" "Corolaries__".
 158
 159 inline procedural "cic:/CoRN/ftc/DerivativeOps/Corolaries/I.con" "Corolaries__".
 160
 161 (* end hide *)
 162
 163 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var".
 164
 165 alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var".
 166
 167 alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var".
 168
 169 alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var".
 170
 171 alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var".
 172
 173 alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var".
 174
 175 (*#*
 176 From this lemmas the rules for the other algebraic operations follow directly.
 177 *)
 178
 179 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_minus.con".
 180
 181 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con".
 182
 183 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con".
 184
 185 alias id "Gbnd" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var".
 186
 187 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con".
 188
 189 (* UNEXPORTED
 190 End Corolaries
 191 *)
 192
 193 (* UNEXPORTED
 194 Hint Resolve Derivative_I_minus Derivative_I_nth Derivative_I_scal
 195   Derivative_I_div: derivate.
 196 *)
 197
 198 (* UNEXPORTED
 199 Section Derivative_Sums
 200 *)
 201
 202 (*#* The derivation rules for families of functions are easily proved by
 203 induction using the constant and addition rules.
 204 *)
 205
 206 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var".
 207
 208 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var".
 209
 210 alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var".
 211
 212 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var".
 213
 214 (* begin hide *)
 215
 216 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/I.con" "Derivative_Sums__".
 217
 218 (* end hide *)
 219
 220 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum0.con".
 221
 222 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con".
 223
 224 inline procedural "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con".
 225
 226 (* UNEXPORTED
 227 End Derivative_Sums
 228 *)
 229
 230 (* UNEXPORTED
 231 Hint Resolve Derivative_I_Sum0 Derivative_I_Sum Derivative_I_Sumx: derivate.
 232 *)
 233