src/HOL/Lubs.thy
 author haftmann Wed Jan 28 11:03:16 2009 +0100 (2009-01-28) changeset 29654 24e73987bfe2 parent 28952 15a4b2cf8c34 child 30738 0842e906300c permissions -rw-r--r--
Plain, Main form meeting points in import hierarchy
1 (*  Title       : Lubs.thy
2     Author      : Jacques D. Fleuriot
3     Copyright   : 1998  University of Cambridge
4 *)
6 header{*Definitions of Upper Bounds and Least Upper Bounds*}
8 theory Lubs
9 imports Plain Main
10 begin
12 text{*Thanks to suggestions by James Margetson*}
14 definition
15   setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
16   "S *<= x = (ALL y: S. y <= x)"
18 definition
19   setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
20   "x <=* S = (ALL y: S. x <= y)"
22 definition
23   leastP      :: "['a =>bool,'a::ord] => bool" where
24   "leastP P x = (P x & x <=* Collect P)"
26 definition
27   isUb        :: "['a set, 'a set, 'a::ord] => bool" where
28   "isUb R S x = (S *<= x & x: R)"
30 definition
31   isLub       :: "['a set, 'a set, 'a::ord] => bool" where
32   "isLub R S x = leastP (isUb R S) x"
34 definition
35   ubs         :: "['a set, 'a::ord set] => 'a set" where
36   "ubs R S = Collect (isUb R S)"
40 subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
42 lemma setleI: "ALL y: S. y <= x ==> S *<= x"
45 lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
48 lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
51 lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
55 subsection{*Rules about the Operators @{term leastP}, @{term ub}
56     and @{term lub}*}
58 lemma leastPD1: "leastP P x ==> P x"
61 lemma leastPD2: "leastP P x ==> x <=* Collect P"
64 lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
65 by (blast dest!: leastPD2 setgeD)
67 lemma isLubD1: "isLub R S x ==> S *<= x"
68 by (simp add: isLub_def isUb_def leastP_def)
70 lemma isLubD1a: "isLub R S x ==> x: R"
71 by (simp add: isLub_def isUb_def leastP_def)
73 lemma isLub_isUb: "isLub R S x ==> isUb R S x"
75 apply (blast dest: isLubD1 isLubD1a)
76 done
78 lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
79 by (blast dest!: isLubD1 setleD)
81 lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
84 lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
87 lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
88 by (simp add: isLub_def leastP_def)
90 lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
91 by (simp add: isUb_def setle_def)
93 lemma isUbD2: "isUb R S x ==> S *<= x"