Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / Partitions.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/Partitions.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/Partitions.mma
index 0e224f38edef55325074b023657fdee34c7c1e5e..5488ba0e75407425269fba5eea373007bd472e94 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/Partitions.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/Partitions.mma
@@ -58,9 +58,9 @@ cic:/matita/CoRN-Procedural/ftc/Partitions/Pts.con
 [i < j] and that [ai] is in [[a,b]] for all [i].
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_mon.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_mon.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_in_compact.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_in_compact.con" as lemma.
 
 (*#*
 Each partition of [[a,b]] implies a partition of the interval
@@ -69,9 +69,9 @@ important role in much of our future work, so we take some care to
 define it.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/part_pred_lemma.con".
+inline procedural "cic:/CoRN/ftc/Partitions/part_pred_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_Dom.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_Dom.con" as definition.
 
 (*#*
 The mesh of a partition is the greatest distance between two
@@ -85,11 +85,11 @@ of defining the minimum and maximum of the empty list to be [0] actually
 helps us in this case.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh.con".
+inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh.con" as definition.
 
 (*#*
 Even partitions (partitions where all the points are evenly spaced)
@@ -97,11 +97,11 @@ will also play a central role in our work; the first two lemmas are
 presented simply to make the definition of even partition lighter.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/even_part_1.con".
+inline procedural "cic:/CoRN/ftc/Partitions/even_part_1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/even_part_2.con".
+inline procedural "cic:/CoRN/ftc/Partitions/even_part_2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition.con" as definition.
 
 (* UNEXPORTED
 Section Refinements
@@ -126,9 +126,9 @@ We now define what it means for a partition [Q] to be a refinement of
 [P] and prove the main property of refinements.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Refinement.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Refinement.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Refinement_prop.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Refinement_prop.con" as lemma.
 
 (*#*
 We will also need to consider arbitrary sums %of the form
@@ -139,11 +139,11 @@ For this, we again need a choice function [x] which has to satisfy
 some condition.  We define the condition and the sum for a fixed [P]:
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Points_in_Partition.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Points_in_Partition.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_Sum.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_Sum.con" as definition.
 
 (* UNEXPORTED
 End Refinements
@@ -173,7 +173,7 @@ alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Hab.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__".
+inline procedural "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__" as definition.
 
 (* end hide *)
 
@@ -194,11 +194,11 @@ alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/m.var".
 
 alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/Q.var".
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con" as lemma.
 
 (* UNEXPORTED
 End Getting_Points
@@ -212,7 +212,7 @@ alias id "F" = "cic:/CoRN/ftc/Partitions/Definitions/F.var".
 
 alias id "contF" = "cic:/CoRN/ftc/Partitions/Definitions/contF.var".
 
-inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con" as definition.
 
 (* UNEXPORTED
 End Definitions
@@ -275,21 +275,21 @@ Section Lemmas
 If a partition has more than one point then its mesh list is nonempty.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con".
+inline procedural "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con" as lemma.
 
 (*#*
 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con" as lemma.
 
 (*#*
 Mesh and antimesh are always nonnegative.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con".
+inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con" as lemma.
 
 (*#*
 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
@@ -306,7 +306,7 @@ alias id "b" = "cic:/CoRN/ftc/Partitions/Lemmas/b.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__".
+inline procedural "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__" as definition.
 
 (* end hide *)
 
@@ -316,11 +316,11 @@ alias id "n" = "cic:/CoRN/ftc/Partitions/Lemmas/n.var".
 
 alias id "P" = "cic:/CoRN/ftc/Partitions/Lemmas/P.var".
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh_lemma.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con".
+inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh_leEq.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh_leEq.con" as lemma.
 
 (* UNEXPORTED
 End Lemmas
@@ -333,15 +333,15 @@ Section Even_Partitions
 (*#* More technical stuff.  Two equal partitions have the same mesh.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd'.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd'.con" as lemma.
 
 (*#*
 The mesh of an even partition is easily calculated.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con".
+inline procedural "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con" as lemma.
 
 (*#* ** Miscellaneous
 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
@@ -354,7 +354,7 @@ alias id "b" = "cic:/CoRN/ftc/Partitions/Even_Partitions/b.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__".
+inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__" as definition.
 
 (* end hide *)
 
@@ -364,9 +364,9 @@ alias id "Hab" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hab.var".
 An interesting property: in a partition, if [ai [<] aj] then [i < j].
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con".
+inline procedural "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con" as lemma.
 
 (*#*
 %\begin{convention}% Assume [m,n] are positive natural numbers and
@@ -387,13 +387,13 @@ alias id "Hn" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hn.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__".
+inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__".
+inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/even_partition_refinement.con".
+inline procedural "cic:/CoRN/ftc/Partitions/even_partition_refinement.con" as lemma.
 
 (* UNEXPORTED
 End Even_Partitions
@@ -414,7 +414,7 @@ alias id "b" = "cic:/CoRN/ftc/Partitions/More_Definitions/b.var".
 
 alias id "Hab" = "cic:/CoRN/ftc/Partitions/More_Definitions/Hab.var".
 
-inline procedural "cic:/CoRN/ftc/Partitions/_Separated.con".
+inline procedural "cic:/CoRN/ftc/Partitions/_Separated.con" as definition.
 
 (*#*
 Two partitions are said to be (mutually) separated if they are both
@@ -434,7 +434,7 @@ alias id "P" = "cic:/CoRN/ftc/Partitions/More_Definitions/P.var".
 
 alias id "Q" = "cic:/CoRN/ftc/Partitions/More_Definitions/Q.var".
 
-inline procedural "cic:/CoRN/ftc/Partitions/Separated.con".
+inline procedural "cic:/CoRN/ftc/Partitions/Separated.con" as definition.
 
 (* UNEXPORTED
 End More_Definitions
@@ -458,7 +458,7 @@ alias id "b" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/b.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__".
+inline procedural "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__" as definition.
 
 (* end hide *)
 
@@ -468,7 +468,7 @@ alias id "Hab" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/Hab.var".
 The antimesh of a separated partition is always positive.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con".
+inline procedural "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con" as lemma.
 
 (*#*
 A partition can have only one point iff the endpoints of the interval
@@ -476,11 +476,11 @@ are the same; moreover, if the partition is separated and the
 endpoints of the interval are the same then it must have one point.
 *)
 
-inline procedural "cic:/CoRN/ftc/Partitions/partition_length_zero.con".
+inline procedural "cic:/CoRN/ftc/Partitions/partition_length_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con".
+inline procedural "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con".
+inline procedural "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con" as lemma.
 
 (* UNEXPORTED
 End Sep_Partitions