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=25a674c2624e4da9df5dd9b56a5bd8e39aaaab79;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma b/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma index 25a674c26..bd3023428 100644 --- a/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma +++ b/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma @@ -23,7 +23,7 @@ include "CoRN.ma". 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". (* 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,17 +83,17 @@ 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 *) @@ -101,17 +101,17 @@ inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.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". @@ -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". (* UNEXPORTED -End Local_Results. +End Local_Results *) (* UNEXPORTED @@ -145,34 +145,34 @@ 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. @@ -184,12 +184,12 @@ inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.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". (* UNEXPORTED -End Corolaries. +End Corolaries *) (* UNEXPORTED @@ -198,24 +198,24 @@ 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 *) @@ -226,7 +226,7 @@ inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con". inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con". (* UNEXPORTED -End Derivative_Sums. +End Derivative_Sums *) (* UNEXPORTED