From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 theories/Sets/Cpo.v | 105 ++++++++++++++++++++++++++--------------------------
 1 file changed, 53 insertions(+), 52 deletions(-)

(limited to 'theories/Sets/Cpo.v')

diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 0b2cf3e3..1e1b70d5 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,86 +24,87 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Cpo.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Cpo.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Partial_Order.
 
 Section Bounds.
-Variable U : Type.
-Variable D : PO U.
+  Variable U : Type.
+  Variable D : PO U.
 
-Let C := Carrier_of U D.
+  Let C := Carrier_of U D.
+  
+  Let R := Rel_of U D.
 
-Let R := Rel_of U D.
-
-Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
+  Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
     Upper_Bound_definition :
-      In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
+    In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
 
-Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
+  Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
     Lower_Bound_definition :
-      In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
-
-Inductive Lub (B:Ensemble U) (x:U) : Prop :=
+    In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
+  
+  Inductive Lub (B:Ensemble U) (x:U) : Prop :=
     Lub_definition :
-      Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
+    Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
 
-Inductive Glb (B:Ensemble U) (x:U) : Prop :=
+  Inductive Glb (B:Ensemble U) (x:U) : Prop :=
     Glb_definition :
-      Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
+    Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
 
-Inductive Bottom (bot:U) : Prop :=
+  Inductive Bottom (bot:U) : Prop :=
     Bottom_definition :
-      In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
-
-Inductive Totally_ordered (B:Ensemble U) : Prop :=
+    In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
+  
+  Inductive Totally_ordered (B:Ensemble U) : Prop :=
     Totally_ordered_definition :
-      (Included U B C ->
-       forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
-      Totally_ordered B.
+    (Included U B C ->
+      forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
+    Totally_ordered B.
 
-Definition Compatible : Relation U :=
-  fun x y:U =>
-    In U C x ->
-    In U C y ->  exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
-	
-Inductive Directed (X:Ensemble U) : Prop :=
-    Definition_of_Directed :
-      Included U X C ->
-      Inhabited U X ->
-      (forall x1 x2:U,
-         Included U (Couple U x1 x2) X ->
-          exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
-      Directed X.
+  Definition Compatible : Relation U :=
+    fun x y:U =>
+      In U C x ->
+      In U C y ->  exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
 
-Inductive Complete : Prop :=
+  Inductive Directed (X:Ensemble U) : Prop :=
+    Definition_of_Directed :
+    Included U X C ->
+    Inhabited U X ->
+    (forall x1 x2:U,
+      Included U (Couple U x1 x2) X ->
+      exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
+    Directed X.
+  
+  Inductive Complete : Prop :=
     Definition_of_Complete :
-      (exists bot : _, Bottom bot) ->
-      (forall X:Ensemble U, Directed X ->  exists bsup : _, Lub X bsup) ->
-      Complete.
+    (exists bot : _, Bottom bot) ->
+    (forall X:Ensemble U, Directed X ->  exists bsup : _, Lub X bsup) ->
+    Complete.
 
-Inductive Conditionally_complete : Prop :=
+  Inductive Conditionally_complete : Prop :=
     Definition_of_Conditionally_complete :
-      (forall X:Ensemble U,
-         Included U X C ->
-         (exists maj : _, Upper_Bound X maj) ->
-          exists bsup : _, Lub X bsup) -> Conditionally_complete.
+    (forall X:Ensemble U,
+      Included U X C ->
+      (exists maj : _, Upper_Bound X maj) ->
+      exists bsup : _, Lub X bsup) -> Conditionally_complete.
 End Bounds.
+
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
   Definition_of_Complete Definition_of_Complete
   Definition_of_Conditionally_complete.
 
 Section Specific_orders.
-Variable U : Type.
-
-Record Cpo : Type := Definition_of_cpo
-  {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
-
-Record Chain : Type := Definition_of_chain
-  {PO_of_chain : PO U;
-   Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
+  Variable U : Type.
+
+  Record Cpo : Type := Definition_of_cpo
+    {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
+  
+  Record Chain : Type := Definition_of_chain
+    {PO_of_chain : PO U;
+    Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
 
 End Specific_orders.
\ No newline at end of file
-- 
cgit v1.2.3