...

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index b877e094cd63d26dfc68045622e576a6c31b0d52..1c68695d3038dbc8806519257c1ae3d867330f02 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -72,3 +72,6 @@ intros 5 (E x y Lxy Lyx); intro H;
 cases H; [apply Lxy;|apply Lyx] assumption;
 qed.
 
+lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
+intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
+qed.

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index dd9a395d6c182d8b0d49c2cb019c7a369d24c969..3e255f79263ca5eb5785a2a1e6a8e347ca98ada0 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -3,4 +3,7 @@ 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
+supremum.ma ordered_set.ma sequence.ma
 logic/equality.ma 
+nat/nat.ma 

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
new file mode 100644 (file)
index 0000000..3bcb691
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "nat/nat.ma".
+
+definition sequence := λO:Type.nat → O.
+
+definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x.
+
+coercion cic:/matita/dama/sequence/fun_of_sequence.con 1.

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
new file mode 100644 (file)
index 0000000..757de3e
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "sequence.ma".
+include "ordered_set.ma".
+
+(* Definition 2.4 *)
+definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
+
+definition strong_sup ≝
+  λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
+
+definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
+
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 
+  for @{'upper_bound $s $x}.
+notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 
+  for @{'increasing $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 
+  for @{'strong_sup $s $x}.
+
+notation > "x 'is_upper_bound' s" non associative with precedence 50 
+  for @{'upper_bound $s $x}.
+notation > "s 'is_increasing'"    non associative with precedence 50 
+  for @{'increasing $s}.
+notation > "x 'is_strong_sup' s"  non associative with precedence 50 
+  for @{'strong_sup $s $x}.
+
+interpretation "Ordered set upper bound" 'upper_bound s x = 
+  (cic:/matita/dama/supremum/upper_bound.con _ s x).
+interpretation "Ordered set increasing"  'increasing s    = 
+  (cic:/matita/dama/supremum/increasing.con _ s).
+interpretation "Ordered set strong sup"  'strong_sup s x  = 
+  (cic:/matita/dama/supremum/strong_sup.con _ s x).
+
+include "bishop_set.ma".  
+  
+lemma uniq_supremum: 
+  ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
+    t1 is_upper_bound s → t2 is_upper_bound s → t1 ≈ t2.
+intros (O s t1 t2 Ht1 Ht2); apply le_le_eq; cases Ht1; cases Ht2;
+