sandwich is back

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

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 0c6d545b8b9f5d762c6a17de39c254f8529f2747..b2411f65263a318cee22f7529a0dec08baa59a60 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -187,7 +187,7 @@ notation "[a,b]" non associative with precedence 50
 interpretation "Ordered set sergment" 'segment a b =
   (cic:/matita/dama/supremum/segment.con _ a b).
 
-notation "x \in [a,b]" non associative with precedence 50 
+notation "hvbox(x \in break [a,b])" non associative with precedence 50 
   for @{'segment2 $a $b $x}.
 interpretation "Ordered set sergment in" 'segment2 a b x=
   (cic:/matita/dama/supremum/segment.con _ a b x).
@@ -196,13 +196,13 @@ coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A
 
 definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
 
-notation < "\pi \sub 1 x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "\pi \sub 2 x" non associative with precedence 50 for @{'pi2 $x}.
+notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
+notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
 notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
 notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
 interpretation "sigma pi1" 'pi1 x = 
  (cic:/matita/dama/supremum/pi1.con _ _ x).
-
+ 
 interpretation "Type exists" 'exists \eta.x =
   (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
 
@@ -214,15 +214,14 @@ intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
 qed.
 
-notation < "{\x|\x \in [a,b]}" non associative with precedence 90 
+notation "hvbox({[a, break b]})" non associative with precedence 90 
   for @{'segment_set $a $b}.
 interpretation "Ordered set segment" 'segment_set a b = 
  (cic:/matita/dama/supremum/segment_ordered_set.con _ a b).
 
 (* Lemma 2.9 *)
 lemma segment_preserves_supremum:
-  ∀O:ordered_set.∀l,u:O.∀a:sequence (segment_ordered_set ? l u).
-    ∀x:(segment_ordered_set ? l u). 
+  ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
     (λn.fst (a n)) is_increasing ∧ 
     (fst x) is_supremum (λn.fst (a n)) → a ↑ x.
 intros; split; cases H; clear H; 
@@ -241,9 +240,17 @@ interpretation "pair pi1" 'pi1 x =
  (cic:/matita/dama/supremum/first.con _ _ x).
 interpretation "pair pi2" 'pi2 x = 
  (cic:/matita/dama/supremum/second.con _ _ x).
+
+notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
+interpretation "pair" 'pair a b = 
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b).
+ 
+notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
+interpretation "prod" 'prod a b = 
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b).
  
 lemma square_ordered_set: ordered_set → ordered_set.
-intro O; apply (mk_ordered_set (pair O O));
+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);
@@ -252,6 +259,13 @@ intro O; apply (mk_ordered_set (pair O O));
     [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 $s }.
+notation > "s 'square'" non associative with precedence 90
+  for @{ 'square $s }.
+interpretation "ordered set square" 'square s = 
+ (cic:/matita/dama/supremum/square_ordered_set.con s).
  
 definition square_segment ≝ 
   λO:ordered_set.λa,b:O.λx:square_ordered_set O.
@@ -260,7 +274,7 @@ definition square_segment ≝
    (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))).
  
 definition convex ≝
-  λO:ordered_set.λU:square_ordered_set O → Prop.
+  λO:ordered_set.λU:O square → Prop.
   ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
   
 (* Definition 2.11 *)