Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntervals.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntervals.mma
index 83214c0b511817f3abacbe77b389d08d917ac215..68c9aeadf9e66be2f7ee094d108217854ac6b0b8 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntervals.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntervals.mma
@@ -105,7 +105,7 @@ inline procedural "cic:/CoRN/ftc/MoreIntervals/interval.ind".
 To each interval a predicate (set) is assigned by the following map:
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop.con" as definition.
 
 (* begin hide *)
 
@@ -123,67 +123,67 @@ We now define what it means for an interval to be nonvoid, proper,
 finite and compact in the obvious way.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/finite.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/finite.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_.con" as definition.
 
 (*#* Finite intervals have a left end and a right end. *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/left_end.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/left_end.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/right_end.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/right_end.con" as definition.
 
 (*#*
 Some trivia: compact intervals are finite; proper intervals are nonvoid; an interval is nonvoid iff it contains some point.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_finite.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_finite.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con" as lemma.
 
 (*#*
 For practical reasons it helps to define left end and right end of compact intervals.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Rend.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Rend.con" as definition.
 
 (*#* In a compact interval, the left end is always less than or equal
 to the right end.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con" as lemma.
 
 (*#*
 Some nice characterizations of inclusion:
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_included.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_included.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval.con" as lemma.
 
 (*#*
 A weirder inclusion result.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included3_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included3_interval.con" as lemma.
 
 (*#*
 Finally, all intervals are characterized by well defined predicates.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con" as lemma.
 
 (* UNEXPORTED
 End Intervals
@@ -224,17 +224,17 @@ alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact
 
 alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var".
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single.con" as definition.
 
 (*#*
 This interval contains [x] and only (elements equal to) [x]; furthermore, for every (well-defined) [P], if $x\in P$#x∈P# then $[x,x]\subseteq P$#[x,x]⊆P#.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con" as lemma.
 
 (* UNEXPORTED
 End Single_Compact_Interval
@@ -244,7 +244,7 @@ End Single_Compact_Interval
 The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con" as definition.
 
 (*#*
 Now for more interesting and important results.
@@ -260,49 +260,49 @@ Section Proper_Compact_with_One_or_Two_Points
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con" as lemma.
 
 (*#*
 If [x [=] y] then the construction yields the same interval whether we
@@ -311,43 +311,43 @@ stage, which is why we formalized this result as a functional
 definition rather than as an existential formula.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con" as lemma.
 
 (*#*
 We can make an analogous construction for two points.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con" as lemma.
 
 (* UNEXPORTED
 End Proper_Compact_with_One_or_Two_Points
@@ -357,9 +357,9 @@ End Proper_Compact_with_One_or_Two_Points
 Compact intervals are exactly compact intervals(!).
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con" as lemma.
 
 (*#*
 A generalization of the previous results: if $[a,b]\subseteq J$#[a,b]⊆J#
@@ -367,7 +367,7 @@ and [J] is proper, then we can find a proper interval [[a',b']] such that
 $[a,b]\subseteq[a',b']\subseteq J$#[a,b]⊆[a',b']⊆J#.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con" as lemma.
 
 (* UNEXPORTED
 End Compact_Constructions
@@ -393,15 +393,15 @@ alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var".
 
 alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var".
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con" as definition.
 
 (* UNEXPORTED
 End Functions
@@ -415,17 +415,17 @@ Section Reflexivity_Properties
 In the case of compact intervals, this definitions collapse to the old ones.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con" as lemma.
 
 (* UNEXPORTED
 End Reflexivity_Properties
@@ -439,11 +439,11 @@ Section Lemmas
 Interestingly, inclusion and equality in an interval are also characterizable in a similar way:
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con".
+inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con" as lemma.
 
 (* UNEXPORTED
 End Lemmas