X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fordered_set.ma;h=91e77bb62d3acbda167154cb9dd731ad9fa7f1df;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=890164ea950d405fd295ad26e0227d62b68d42e7;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/ordered_set.ma b/helm/software/matita/library/dama/ordered_set.ma
index 890164ea9..91e77bb62 100644
--- a/helm/software/matita/library/dama/ordered_set.ma
+++ b/helm/software/matita/library/dama/ordered_set.ma
@@ -20,8 +20,8 @@ include "logic/cprop_connectives.ma".
 notation "''" non associative with precedence 90 for @{'}.
 notation "''" non associative with precedence 90 for @{'}.
 
-interpretation "" ' = ( (os_l _)).
-interpretation "" ' = ( (os_r _)).
+interpretation "" ' = ( (os_l ?)).
+interpretation "" ' = ( (os_r ?)).
 *)
 
 (* Definition 2.1 *)
@@ -69,31 +69,31 @@ coercion Type_of_ordered_set_dual.
 coercion Type_of_ordered_set.
 
 notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
-interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
+interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess ? a b).
 
-interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
-interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
+interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r ?) a b).
+interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l ?) a b).
 
 notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
 notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
 
-interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l _))).
-interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r _))).
+interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l ?))).
+interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r ?))).
 
 notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
 notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
 
-interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l _))).
-interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r _))).
+interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l ?))).
+interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r ?))).
 
 (* Definition 2.2 (3) *)
 definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
 
 notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
-interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le _ a b)).
+interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le ? a b)).
 
-interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r _) a b)).
-interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l _) a b)).
+interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r ?) a b)).
+interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l ?) a b)).
 
 lemma hle_reflexive: ∀E.reflexive ? (le E).
 unfold reflexive; intros 3; apply (hos_coreflexive ? x H);
@@ -102,8 +102,8 @@ qed.
 notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
 notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
 
-interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
-interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
+interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l ?)).
+interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r ?)).
 
 (* DUALITY TESTS 
 lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
@@ -124,8 +124,8 @@ qed.
 notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
 notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
 
-interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
-interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
+interpretation "le transitive" 'le_transitive = (hle_transitive (os_l ?)).
+interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r ?)).
 
 (* Lemma 2.3 *)
 lemma exc_hle_variance: 
@@ -139,8 +139,8 @@ qed.
 notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
 notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
 
-interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
-interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
+interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l ?)).
+interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r ?)).
 
 definition square_exc ≝
  λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
@@ -177,5 +177,5 @@ interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 
 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
-interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b). 
+interpretation "ordered set subset" 'subseteq a b = (os_subset ? a b).