X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=50b1ebedae5d64b9f1a8842fea85e20c440410af;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=a3aa83d6af7d6bec3e5bb71ca0b112240cbf83d0;hpb=3cd093c8c3f5454514802e5d3ae5edc150dbbf72;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index a3aa83d6a..50b1ebeda 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -53,18 +53,12 @@ notation > "x 'is_supremum' s" non associative with precedence 50 notation > "x 'is_infimum' s" non associative with precedence 50 for @{'infimum $s $x}. -interpretation "Ordered set upper bound" 'upper_bound s x = - (cic:/matita/dama/supremum/upper_bound.con _ s x). -interpretation "Ordered set lower bound" 'lower_bound s x = - (cic:/matita/dama/supremum/lower_bound.con _ s x). -interpretation "Ordered set increasing" 'increasing s = - (cic:/matita/dama/supremum/increasing.con _ s). -interpretation "Ordered set decreasing" 'decreasing s = - (cic:/matita/dama/supremum/decreasing.con _ s). -interpretation "Ordered set strong sup" 'supremum s x = - (cic:/matita/dama/supremum/supremum.con _ s x). -interpretation "Ordered set strong inf" 'infimum s x = - (cic:/matita/dama/supremum/infimum.con _ s x). +interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound _ s x). +interpretation "Ordered set lower bound" 'lower_bound s x = (lower_bound _ s x). +interpretation "Ordered set increasing" 'increasing s = (increasing _ s). +interpretation "Ordered set decreasing" 'decreasing s = (decreasing _ s). +interpretation "Ordered set strong sup" 'supremum s x = (supremum _ s x). +interpretation "Ordered set strong inf" 'infimum s x = (infimum _ s x). include "bishop_set.ma". @@ -97,24 +91,24 @@ notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 notation > "s 'is_strictly_increasing'" non associative with precedence 50 for @{'strictly_increasing $s}. interpretation "Ordered set strict increasing" 'strictly_increasing s = - (cic:/matita/dama/supremum/strictly_increasing.con _ s). + (strictly_increasing _ s). notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50 for @{'strictly_decreasing $s}. notation > "s 'is_strictly_decreasing'" non associative with precedence 50 for @{'strictly_decreasing $s}. interpretation "Ordered set strict decreasing" 'strictly_decreasing s = - (cic:/matita/dama/supremum/strictly_decreasing.con _ s). + (strictly_decreasing _ s). notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}. interpretation "Ordered set supremum of increasing" 'sup_inc s u = (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) - (cic:/matita/dama/supremum/increasing.con _ s) - (cic:/matita/dama/supremum/supremum.con _ s u)). + (increasing _ s) + (supremum _ s u)). notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}. interpretation "Ordered set supremum of increasing" 'inf_dec s u = (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) - (cic:/matita/dama/supremum/decreasing.con _ s) - (cic:/matita/dama/supremum/infimum.con _ s u)). + (decreasing _ s) + (infimum _ s u)). include "nat/plus.ma". include "nat_ordered_set.ma". @@ -185,8 +179,7 @@ notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associati for @{'order_converge $a $x}. notation > "a 'order_converges' x" non associative with precedence 50 for @{'order_converge $a $x}. -interpretation "Order convergence" 'order_converge s u = - (cic:/matita/dama/supremum/order_converge.con _ s u). +interpretation "Order convergence" 'order_converge s u = (order_converge _ s u). (* Definition 2.8 *) @@ -195,13 +188,11 @@ definition segment ≝ λO:ordered_set.λa,b:O.λx:O. notation "[a,b]" non associative with precedence 50 for @{'segment $a $b}. -interpretation "Ordered set sergment" 'segment a b = - (cic:/matita/dama/supremum/segment.con _ a b). +interpretation "Ordered set sergment" 'segment a b = (segment _ a b). 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). +interpretation "Ordered set sergment in" 'segment2 a b x= (segment _ a b x). coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P. @@ -211,8 +202,7 @@ 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 "sigma pi1" 'pi1 x = (pi1 _ _ x). interpretation "Type exists" 'exists \eta.x = (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x). @@ -228,7 +218,7 @@ qed. 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). + (segment_ordered_set _ a b). (* Lemma 2.9 *) lemma segment_preserves_supremum: @@ -247,18 +237,14 @@ coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x]. definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y]. -interpretation "pair pi1" 'pi1 x = - (cic:/matita/dama/supremum/first.con _ _ x). -interpretation "pair pi2" 'pi2 x = - (cic:/matita/dama/supremum/second.con _ _ x). +interpretation "pair pi1" 'pi1 x = (first _ _ x). +interpretation "pair pi2" 'pi2 x = (second _ _ 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). +interpretation "pair" 'pair a b = (prod _ _ 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). +interpretation "prod" 'prod a b = (pair a b). lemma square_ordered_set: ordered_set → ordered_set. intro O; apply (mk_ordered_set (O × O)); @@ -275,8 +261,7 @@ 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). +interpretation "ordered set square" 'square s = (square_ordered_set s). definition square_segment ≝ λO:ordered_set.λa,b:O.λx:square_ordered_set O. @@ -302,14 +287,14 @@ notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 notation > "s 'is_upper_located'" non associative with precedence 50 for @{'upper_located $s}. interpretation "Ordered set upper locatedness" 'upper_located s = - (cic:/matita/dama/supremum/upper_located.con _ s). + (upper_located _ s). notation < "s \nbsp 'is_lower_located'" non associative with precedence 50 for @{'lower_located $s}. notation > "s 'is_lower_located'" non associative with precedence 50 for @{'lower_located $s}. interpretation "Ordered set lower locatedness" 'lower_located s = - (cic:/matita/dama/supremum/lower_located.con _ s). + (lower_located _ s). (* Lemma 2.12 *) lemma uparrow_upperlocated: @@ -328,4 +313,4 @@ cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W); |2: right; exists [apply u]; split; [apply W|apply H4]] qed. - \ No newline at end of file +