a) update with upstream version

[helm.git] / helm / software / matita / contribs / dama / dama / ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 4c72cfd98d35dbbbc4c0f57134b6a88dc70b0866..45a8a1b379c1e4d866dd48a6d1c575bce6edb971 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 (* Definition 2.1 *)
 record ordered_set: Type ≝ {
@@ -22,17 +22,14 @@ record ordered_set: Type ≝ {
   os_cotransitive: cotransitive ? os_excess 
 }.
 
-interpretation "Ordered set excess" 'nleq a b = 
-  (cic:/matita/dama/ordered_set/os_excess.con _ a b). 
+interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b). 
 
 (* Definition 2.2 (3) *)
 definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
 
-interpretation "Ordered set greater or equal than" 'geq a b = 
- (cic:/matita/dama/ordered_set/le.con _ b a).
+interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
 
-interpretation "Ordered set less or equal than" 'leq a b = 
- (cic:/matita/dama/ordered_set/le.con _ a b).
+interpretation "Ordered set less or equal than" 'leq a b = (le _ a b).
 
 lemma le_reflexive: ∀E.reflexive ? (le E).
 unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
@@ -51,3 +48,27 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
+
+lemma square_ordered_set: ordered_set → ordered_set.
+intro O;
+apply (mk_ordered_set (O × O));
+[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
+|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
+    cases H (X X); apply (os_coreflexive ?? X);
+|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
+    clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
+    [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
+    |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+qed.
+
+notation "s 2 \atop \nleq" non associative with precedence 90
+  for @{ 'square_os $s }.
+notation > "s 'square'" non associative with precedence 90
+  for @{ 'square $s }.
+interpretation "ordered set square" 'square s = (square_ordered_set s). 
+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). 
+