src/HOL/Real/Lubs.thy
changeset 5078 7b5ea59c0275
child 7219 4e3f386c2e37
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/Lubs.thy	Thu Jun 25 13:57:34 1998 +0200
@@ -0,0 +1,38 @@
+(*  Title       : Lubs.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : Upper bounds, lubs definitions
+                  suggested by James Margetson
+*) 
+
+
+Lubs = Set +
+
+consts
+    
+    "*<=" :: ['a set, 'a] => bool     (infixl 70)
+    "<=*" :: ['a, 'a set] => bool     (infixl 70)
+
+constdefs
+    leastP      :: ['a =>bool,'a] => bool
+    "leastP P x == (P x & x <=* Collect P)"
+
+    isLub       :: ['a set, 'a set, 'a] => bool    
+    "isLub R S x  == leastP (isUb R S) x"
+
+    isUb        :: ['a set, 'a set, 'a] => bool     
+    "isUb R S x   == S *<= x & x: R"
+
+    ubs         :: ['a set, 'a set] => 'a set
+    "ubs R S      == Collect (isUb R S)"
+
+defs
+    setle_def
+    "S *<= x    == (ALL y: S. y <= x)"
+
+    setge_def
+    "x <=* S    == (ALL y: S. x <= y)"
+
+end                    
+
+