From 9f064ffe2834ae91f306b44f79bfbfb68a4631c5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Jun 2008 15:58:54 +0000
Subject: [PATCH] bla bla bla

---
 .../contribs/dama/dama/models/uniformnat.ma   | 80 ++++++++++++++++++-
 .../contribs/dama/dama/nat_ordered_set.ma     | 14 +++-
 2 files changed, 92 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
index 314977675..c65299ad6 100644
--- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
+++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
@@ -45,6 +45,84 @@ intro C; apply (mk_uniform_space C);
         lapply (H6 H4) as H7; apply eq_sym; apply H7;]] 
 qed.        
 
+
+notation "\naturals" non associative with precedence 99 for @{'nat}.
+
+interpretation "naturals" 'nat = nat.
+interpretation "Ordered set N" 'nat = nat_ordered_set.
+
+lemma nat_dedekind_sigma_complete:
+  ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
+    ∀x.x is_supremum a → ∃i.∀j.i ≤ j → x ≈ a j.
+intros 5; cases x; clear x; intros;
+cases H2; 
+letin m ≝ (
+  let rec aux i ≝
+    match i with
+    [ O ⇒ match eqb (fst (a O)) x1 with
+            [ true ⇒ O
+            | false ⇒ match H4 (a O) ? with
+                      [ ex_introT n _ ⇒ n]]
+    | S m ⇒ let pred ≝ aux m in 
+            match eqb (fst (a pred)) x1 with
+            [ true ⇒ pred
+            | false ⇒ match H4 (a pred) ? with
+                      [ ex_introT n _ ⇒ n]]]
+   in aux
+   :
+   ∀i:nat.∃j.a j = x1 ∨ a i < a j);  
+        
+cases (∀n.a n = x1 ∨ x1 ≰ a n);
+
+ elim x1 in H1 ⊢ % 0; 
+[1: intro H2; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) O H2); intros;
+    fold unfold X X in H1 ⊢ %;
+    exists [apply O] cases H1; intros; apply le_le_eq;[2: apply H3;]
+    intro; alias symbol "pi1" = "sigma pi1".
+    change in H6 with (fst (a j) < O);
+    apply (not_le_Sn_O (fst (a j))); apply H6;
+|2: intros 3; letin S_X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) (S n) H2); intros;
+    fold unfold S_X S_X in H3 ⊢ %;
+    generalize in match (leb_to_Prop l n); elim (leb l n); simplify in H4;
+    [1: cut (n ≤ u); [2: cases H2; normalize in H5 ⊢ %;
+          apply le_S_S_to_le; lapply (not_lt_to_le ?? H5) as XX;
+          apply le_S; apply XX;]
+        cases H1; [2:split; apply nat_le_to_os_le; assumption|3:simplify;
+    
+    elim (or_lt_le (S n) l); 
+      [ cases (?:l = S n ∨ l < S n);[ 
+          unfold lt; cases H2; normalize in H5; 
+        apply (Right (eq nat n (S n)) (lt n (S n)) ?).apply (not_le_to_lt (S n) n ?).apply (not_le_Sn_n n).]
+        [ destruct H4;
+
+  
+  ∀x.∃i.x ≰ a i ∨ x ≤ a i.
+intros; elim x;
+
+
 definition nat_uniform_space: uniform_space.
-apply (discrete_uniform_space_of_bishop_set nat_ordered_set);
+apply (discrete_uniform_space_of_bishop_set ℕ);
 qed.
+
+interpretation "Uniform space N" 'nat = nat_uniform_space.
+
+include "ordered_uniform.ma".
+
+definition nat_ordered_uniform_space:ordered_uniform_space.
+apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
+simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
+cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
+lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
+[1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
+|2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
+qed. 
+
+interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
+
+lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
+intros 4; split; intros 3; cases H; cases H3; clear H3 H;
+cases (H5 (a i));
+cases (H10 (sig_in ?? x1 H2)); 
+
+exists [1,3:apply x1]
+intros; apply H6;
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index e7dfec461..6ecbe5424 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -15,7 +15,7 @@
 include "ordered_set.ma".
 
 include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "cprop_connectives.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -49,3 +49,15 @@ apply (mk_ordered_set ? nat_excess);
 [1: intro x; intro; apply (not_le_Sn_n ? H);
 |2: apply nat_excess_cotransitive]
 qed.
+
+alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+lemma os_le_to_nat_le:
+  ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
+intros; normalize in H; apply (not_lt_to_le ?? H);
+qed.
+ 
+lemma nat_le_to_os_le:
+  ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
+intros 3; apply (le_to_not_lt a b);assumption;
+qed.
+  
\ No newline at end of file
-- 
2.39.2