X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Fftc%2FIntegral.mma;h=adfac8d026b3e2bdc95e908210ded75662de7762;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=1fa68f3856580adfbd6972baa9c8bde2eba4842f;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/Integral.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/Integral.mma
index 1fa68f385..adfac8d02 100644
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/Integral.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/Integral.mma
@@ -30,9 +30,9 @@ include "ftc/RefLemma.ma".
 Section Lemmas
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__".
+inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
+inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Lemmas
@@ -65,13 +65,13 @@ alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.
 
 alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
 
 alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
 
-inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.
 
 (* end hide *)
 
@@ -79,11 +79,11 @@ inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
 Section Darboux_Sum
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
+inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.
 
 (* UNEXPORTED
 End Darboux_Sum
@@ -114,7 +114,7 @@ alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.
 
 (* end hide *)
 
@@ -128,7 +128,7 @@ alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var".
 
 alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var".
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.
 
 (* UNEXPORTED
 End Integral_Thm
@@ -154,7 +154,7 @@ alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__".
+inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.
 
 (* end hide *)
 
@@ -174,13 +174,13 @@ alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/con
 
 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.
 
 (* UNEXPORTED
 End Well_Definedness
@@ -198,7 +198,7 @@ Opaque Even_Partition.
 The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#&int;<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#&int;<sub>a</sub><sup>a</sup>=0#.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_one.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.
 
 alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
 
@@ -208,15 +208,15 @@ alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monoto
 
 alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.
 
 (* UNEXPORTED
 Transparent Even_Partition.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.
 
 (* UNEXPORTED
 End Linearity_and_Monotonicity
@@ -246,19 +246,19 @@ alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monoton
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__".
+inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.
 
 (* end hide *)
 
 alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
 
-inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.
 
 (* UNEXPORTED
 Opaque nring.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.
 
 (* UNEXPORTED
 Transparent nring.
@@ -284,21 +284,21 @@ alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.va
 As corollaries we can calculate integrals of group operations applied to functions.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_const.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.
 
 (*#*
 We can also bound integrals by bounding the integrated functions.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.
 
 (* UNEXPORTED
 End Corollaries
@@ -357,31 +357,31 @@ alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_J
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.
 
 (* end hide *)
 
@@ -404,25 +404,25 @@ alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partitio
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.
 
 (* UNEXPORTED
 Opaque partition_join.
@@ -448,9 +448,9 @@ Opaque minus.
 Transparent minus.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.
 
 (* UNEXPORTED
 End Partition_Join
@@ -464,7 +464,7 @@ With these results in mind, the following is a trivial consequence:
 Opaque Even_Partition.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.
 
 (* UNEXPORTED
 End Integral_Sum
@@ -482,11 +482,11 @@ End Basic_Properties
 The following are simple consequences of this result and of previous ones.
 *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.
 
 (* end hide *)