src/HOL/Real/Lubs.thy
 changeset 21404 eb85850d3eb7 parent 19765 dfe940911617 child 27368 9f90ac19e32b
```--- a/src/HOL/Real/Lubs.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Real/Lubs.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -13,23 +13,27 @@
text{*Thanks to suggestions by James Margetson*}

definition
-
-  setle :: "['a set, 'a::ord] => bool"     (infixl "*<=" 70)
+  setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
"S *<= x = (ALL y: S. y <= x)"

-  setge :: "['a::ord, 'a set] => bool"     (infixl "<=*" 70)
+definition
+  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
"x <=* S = (ALL y: S. x <= y)"

-  leastP      :: "['a =>bool,'a::ord] => bool"
+definition
+  leastP      :: "['a =>bool,'a::ord] => bool" where
"leastP P x = (P x & x <=* Collect P)"

-  isUb        :: "['a set, 'a set, 'a::ord] => bool"
+definition
+  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
"isUb R S x = (S *<= x & x: R)"

-  isLub       :: "['a set, 'a set, 'a::ord] => bool"
+definition
+  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
"isLub R S x = leastP (isUb R S) x"

-  ubs         :: "['a set, 'a::ord set] => 'a set"
+definition
+  ubs         :: "['a set, 'a::ord set] => 'a set" where
"ubs R S = Collect (isUb R S)"

```