From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 7 Jun 2008 16:25:03 +0000 (+0000)
Subject: exhaustivity defined
X-Git-Tag: make_still_working~5065
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b284579a0c4d45bc8483f295434a465ca685f444;p=helm.git

exhaustivity defined
---

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index b56309c6f..128afd683 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,15 +1,16 @@
+sandwich.ma ordered_uniform.ma
+property_sigma.ma ordered_uniform.ma
+uniform.ma supremum.ma
 bishop_set.ma ordered_set.ma
-extra.ma bishop_set_rewrite.ma
-ordered_set.ma cprop_connectives.ma
-cprop_connectives.ma logic/equality.ma
-bishop_set_rewrite.ma bishop_set.ma
 sequence.ma nat/nat.ma
-uniform.ma supremum.ma
+ordered_uniform.ma uniform.ma
 supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
+property_exhaustivity.ma ordered_uniform.ma
+bishop_set_rewrite.ma bishop_set.ma
+cprop_connectives.ma logic/equality.ma
 nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
-property_sigma.ma ordered_uniform.ma
-ordered_uniform.ma uniform.ma
-sandwich.ma ordered_uniform.ma
+ordered_set.ma cprop_connectives.ma
+extra.ma bishop_set_rewrite.ma
 logic/equality.ma 
 nat/compare.ma 
 nat/nat.ma 
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
new file mode 100644
index 000000000..00f8cb259
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ordered_uniform.ma".
+
+(* Definition 3.7 *)
+definition exhaustivity ≝
+  λC:ordered_uniform_space.
+   ∀a,b:sequence C.
+     (a is_increasing → a is_upper_located → a is_cauchy) ∧
+     (b is_decreasing → b is_lower_located → b is_cauchy).
+     
+(* Lemma 3.8 *)
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a4df77806..b99323140 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -292,15 +292,40 @@ definition convex ≝
 definition upper_located ≝
   λO:ordered_set.λa:sequence O.∀x,y:O. y ≰ x → 
     (∃i:nat.a i ≰ x) ∨ (∃b:O.y≰b ∧ ∀i:nat.a i ≤ b).
+
+definition lower_located ≝
+  λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y → 
+    (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i).
+
+notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 
+  for @{'upper_located $s}.
+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).
+
+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).
     
 (* Lemma 2.12 *)    
-lemma uparrow_located:
-  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → upper_located ? a.
+lemma uparrow_upperlocated:
+  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → a is_upper_located.
 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
 cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
 [2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
 |1: right; exists [apply u]; split; [apply W|apply H4]]
 qed. 
 
+lemma downarrow_lowerlocated:
+  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↓ u → a is_lower_located.
+intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
+cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
+[1: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+|2: right; exists [apply u]; split; [apply W|apply H4]]
+qed. 
      
     
\ No newline at end of file