X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fsupremum.ma;h=aba4730bcf614fa9fcadcbce36154a1f1ce3e2e7;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=0de61b292fcaca3e40f5b7bddfa7ba0b88d27398;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index 0de61b292..aba4730bc 100644
--- a/helm/software/matita/library/dama/supremum.ma
+++ b/helm/software/matita/library/dama/supremum.ma
@@ -15,8 +15,8 @@
 
 include "datatypes/constructors.ma".
 include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/sequence.ma".
 
 (* Definition 2.4 *)
 definition upper_bound ≝ 
@@ -54,14 +54,14 @@ notation > "x 'is_supremum' s"  non associative with precedence 45
 notation > "x 'is_infimum' s"  non associative with precedence 45 
   for @{'infimum $s $x}.
 
-interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
-interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
+interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l ?) s x).
+interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r ?) s x).
 
-interpretation "Ordered set increasing"  'increasing s = (increasing (os_l _) s).
-interpretation "Ordered set decreasing"  'decreasing s = (increasing (os_r _) s).
+interpretation "Ordered set increasing"  'increasing s = (increasing (os_l ?) s).
+interpretation "Ordered set decreasing"  'decreasing s = (increasing (os_r ?) s).
 
-interpretation "Ordered set strong sup"  'supremum s x = (supremum (os_l _) s x).
-interpretation "Ordered set strong inf"  'infimum s x = (supremum (os_r _) s x).
+interpretation "Ordered set strong sup"  'supremum s x = (supremum (os_l ?) s x).
+interpretation "Ordered set strong inf"  'infimum s x = (supremum (os_r ?) s x).
   
 (* Fact 2.5 *)
 lemma h_supremum_is_upper_bound: 
@@ -74,8 +74,8 @@ qed.
 notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
 notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
 
-interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
-interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
+interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l ?)).
+interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r ?)).
 
 (* Lemma 2.6 *)
 definition strictly_increasing ≝ 
@@ -86,21 +86,21 @@ notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
 notation > "s 'is_strictly_increasing'" non associative with precedence 45 
   for @{'strictly_increasing $s}.
 interpretation "Ordered set strict increasing"  'strictly_increasing s    = 
-  (strictly_increasing (os_l _) s).
+  (strictly_increasing (os_l ?) s).
   
 notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
 notation > "s 'is_strictly_decreasing'" non associative with precedence 45 
   for @{'strictly_decreasing $s}.
 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    = 
-  (strictly_increasing (os_r _) s).
+  (strictly_increasing (os_r ?) s).
 
 definition uparrow ≝
   λC:half_ordered_set.λs:sequence C.λu:C.
    increasing ? s ∧ supremum ? s u.
 
-interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
-interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
+interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l ?) s u).
+interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r ?) s u).
 
 lemma h_trans_increasing: 
   ∀C:half_ordered_set.∀a:sequence C.increasing ? a → 
@@ -117,11 +117,11 @@ qed.
 notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
 notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
 
-interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
-interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
+interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l ?)).
+interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r ?)).
 
 lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
    hos_carr (os_l (nat_ordered_set)).
 intros; assumption;
 qed.
@@ -144,8 +144,8 @@ qed.
 notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
 notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
 
-interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
-interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
+interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l ?)).
+interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r ?)).
 
 alias symbol "exists" = "CProp exists".
 lemma nat_strictly_increasing_reaches: 
@@ -180,8 +180,8 @@ qed.
 notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
 notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
 
-interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
-interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
+interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l ?)).
+interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r ?)).
 
 (* Definition 2.7 *)
 definition order_converge ≝
@@ -194,7 +194,7 @@ notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associativ
   for @{'order_converge $a $x}.
 notation > "a 'order_converges' x" non associative with precedence 45 
   for @{'order_converge $a $x}.
-interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
+interpretation "Order convergence" 'order_converge s u = (order_converge ? s u).   
     
 (* Definition 2.8 *)
 record segment (O : Type) : Type ≝ {
@@ -202,9 +202,9 @@ record segment (O : Type) : Type ≝ {
    seg_u_ : O
 }.
 
-notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation > "𝕦_ term 90 s" non associative with precedence 90 for @{'upp $s}.
 notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}. 
-notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation > "𝕝_ term 90 s" non associative with precedence 90 for @{'low $s}.
 notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}. 
  
 definition seg_u ≝
@@ -214,10 +214,10 @@ definition seg_l ≝
  λO:half_ordered_set.λs:segment O.
    wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s). 
  
-interpretation "uppper" 'upp s = (seg_u (os_l _) s).
-interpretation "lower" 'low s = (seg_l (os_l _) s).
-interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
-interpretation "lower dual" 'low s = (seg_u (os_r _) s).
+interpretation "uppper" 'upp s = (seg_u (os_l ?) s).
+interpretation "lower" 'low s = (seg_l (os_l ?) s).
+interpretation "uppper dual" 'upp s = (seg_l (os_r ?) s).
+interpretation "lower dual" 'low s = (seg_u (os_r ?) s).
  
 definition in_segment ≝ 
   λO:half_ordered_set.λs:segment O.λx:O.
@@ -226,7 +226,7 @@ definition in_segment ≝
 notation "‡O" non associative with precedence 90 for @{'segment $O}.
 interpretation "Ordered set sergment" 'segment x = (segment x).
 
-interpretation "Ordered set sergment in" 'mem x s = (in_segment _ s x).
+interpretation "Ordered set sergment in" 'mem x s = (in_segment ? s x).
 
 definition segment_ordered_set_carr ≝
   λO:half_ordered_set.λs:‡O.∃x.x ∈ s.
@@ -268,7 +268,7 @@ apply half2full; apply (half_segment_ordered_set (os_l O) s);
 qed.
 
 notation "{[ term 19 s ]}" non associative with precedence 90 for @{'segset $s}.
-interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s). 
+interpretation "Ordered set segment" 'segset s = (segment_ordered_set ? s). 
 
 (* test :
  ∀O:ordered_set.∀s: segment (os_l O).∀x:O.
@@ -376,8 +376,8 @@ qed.
 notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
 notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
 
-interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
-interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
+interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l ?)).
+interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r ?)).
 
 (*
 test segment_preserves_infimum2:
@@ -417,14 +417,14 @@ notation < "s \nbsp 'is_upper_located'" non associative with precedence 45
 notation > "s 'is_upper_located'" non associative with precedence 45 
   for @{'upper_located $s}.
 interpretation "Ordered set upper locatedness" 'upper_located s = 
-  (upper_located (os_l _) s).
+  (upper_located (os_l ?) s).
 
 notation < "s \nbsp 'is_lower_located'" non associative with precedence 45 
   for @{'lower_located $s}.
 notation > "s 'is_lower_located'" non associative with precedence 45
   for @{'lower_located $s}.
 interpretation "Ordered set lower locatedness" 'lower_located s = 
-  (upper_located (os_r _) s).
+  (upper_located (os_r ?) s).
       
 (* Lemma 2.12 *)    
 lemma h_uparrow_upperlocated:
@@ -438,5 +438,5 @@ qed.
 notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
 notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
 
-interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
-interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).
+interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l ?)).
+interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r ?)).