X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDerivativeOps.ma;h=bd3023428163bad18c54c7728273d3492d9ab5f0;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=18b016072917303391bb2b1cdca933b445751759;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma b/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma index 18b016072..bd3023428 100644 --- a/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma +++ b/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma @@ -16,14 +16,14 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/DerivativeOps". +include "CoRN.ma". + (* $Id: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *) -(* INCLUDE -Derivative -*) +include "ftc/Derivative.ma". (* UNEXPORTED -Section Lemmas. +Section Lemmas *) (*#* **Algebraic Operations @@ -38,36 +38,36 @@ context.%}.% We begin with some technical stuff that will be necessary for division. *) -inline cic:/CoRN/ftc/DerivativeOps/a.var. +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var". -inline cic:/CoRN/ftc/DerivativeOps/b.var. +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var". -inline cic:/CoRN/ftc/DerivativeOps/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/DerivativeOps/I.con. +inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/I.con" "Lemmas__". (* end hide *) -inline cic:/CoRN/ftc/DerivativeOps/F.var. +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var". (* begin hide *) -inline cic:/CoRN/ftc/DerivativeOps/P.con. +inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/P.con" "Lemmas__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/DerivativeOps/Fbnd.var. +alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var". (* end show *) -inline cic:/CoRN/ftc/DerivativeOps/bnd_away_zero_square.con. +inline "cic:/CoRN/ftc/DerivativeOps/bnd_away_zero_square.con". (* UNEXPORTED -End Lemmas. +End Lemmas *) (* UNEXPORTED @@ -75,7 +75,7 @@ Hint Resolve bnd_away_zero_square: included. *) (* UNEXPORTED -Section Local_Results. +Section Local_Results *) (*#* **Local Results @@ -83,41 +83,41 @@ Section Local_Results. We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative. *) -inline cic:/CoRN/ftc/DerivativeOps/a.var. +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var". -inline cic:/CoRN/ftc/DerivativeOps/b.var. +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var". -inline cic:/CoRN/ftc/DerivativeOps/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/DerivativeOps/Hab.con. +inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab.con" "Local_Results__". -inline cic:/CoRN/ftc/DerivativeOps/I.con. +inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/I.con" "Local_Results__". (* end hide *) -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con". -inline cic:/CoRN/ftc/DerivativeOps/F.var. +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var". -inline cic:/CoRN/ftc/DerivativeOps/F'.var. +alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var". -inline cic:/CoRN/ftc/DerivativeOps/G.var. +alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var". -inline cic:/CoRN/ftc/DerivativeOps/G'.var. +alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var". -inline cic:/CoRN/ftc/DerivativeOps/derF.var. +alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var". -inline cic:/CoRN/ftc/DerivativeOps/derG.var. +alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_inv.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_inv.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_mult.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_mult.con". (*#* As was the case for continuity, the rule for the reciprocal function has a side condition. @@ -125,14 +125,14 @@ As was the case for continuity, the rule for the reciprocal function has a side (* begin show *) -inline cic:/CoRN/ftc/DerivativeOps/Fbnd.var. +alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var". (* end show *) -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_recip.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_recip.con". (* UNEXPORTED -End Local_Results. +End Local_Results *) (* UNEXPORTED @@ -145,51 +145,51 @@ Hint Resolve Derivative_I_const Derivative_I_id Derivative_I_plus *) (* UNEXPORTED -Section Corolaries. +Section Corolaries *) -inline cic:/CoRN/ftc/DerivativeOps/a.var. +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var". -inline cic:/CoRN/ftc/DerivativeOps/b.var. +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var". -inline cic:/CoRN/ftc/DerivativeOps/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/DerivativeOps/Hab.con. +inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab.con" "Corolaries__". -inline cic:/CoRN/ftc/DerivativeOps/I.con. +inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/I.con" "Corolaries__". (* end hide *) -inline cic:/CoRN/ftc/DerivativeOps/F.var. +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var". -inline cic:/CoRN/ftc/DerivativeOps/F'.var. +alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var". -inline cic:/CoRN/ftc/DerivativeOps/G.var. +alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var". -inline cic:/CoRN/ftc/DerivativeOps/G'.var. +alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var". -inline cic:/CoRN/ftc/DerivativeOps/derF.var. +alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var". -inline cic:/CoRN/ftc/DerivativeOps/derG.var. +alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var". (*#* From this lemmas the rules for the other algebraic operations follow directly. *) -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_minus.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_minus.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con". -inline cic:/CoRN/ftc/DerivativeOps/Gbnd.var. +alias id "Gbnd" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con". (* UNEXPORTED -End Corolaries. +End Corolaries *) (* UNEXPORTED @@ -198,35 +198,35 @@ Hint Resolve Derivative_I_minus Derivative_I_nth Derivative_I_scal *) (* UNEXPORTED -Section Derivative_Sums. +Section Derivative_Sums *) (*#* The derivation rules for families of functions are easily proved by induction using the constant and addition rules. *) -inline cic:/CoRN/ftc/DerivativeOps/a.var. +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var". -inline cic:/CoRN/ftc/DerivativeOps/b.var. +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var". -inline cic:/CoRN/ftc/DerivativeOps/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var". -inline cic:/CoRN/ftc/DerivativeOps/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/DerivativeOps/I.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/I.con" "Derivative_Sums__". (* end hide *) -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum0.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum0.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con". -inline cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con. +inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con". (* UNEXPORTED -End Derivative_Sums. +End Derivative_Sums *) (* UNEXPORTED