src/HOL/Lubs.thy
 author wenzelm Mon Mar 22 20:58:52 2010 +0100 (2010-03-22) changeset 35898 c890a3835d15 parent 30738 0842e906300c child 46509 c4b2ec379fdd permissions -rw-r--r--
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 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"
43 by (simp add: setle_def)
45 lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
46 by (simp add: setle_def)
48 lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
49 by (simp add: setge_def)
51 lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
52 by (simp add: setge_def)
55 subsection{*Rules about the Operators @{term leastP}, @{term ub}
56     and @{term lub}*}
58 lemma leastPD1: "leastP P x ==> P x"
59 by (simp add: leastP_def)
61 lemma leastPD2: "leastP P x ==> x <=* Collect P"
62 by (simp add: leastP_def)
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"
74 apply (simp add: isUb_def)
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"
82 by (simp add: isLub_def)
84 lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
85 by (simp add: isLub_def)
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"
94 by (simp add: isUb_def)
96 lemma isUbD2a: "isUb R S x ==> x: R"
97 by (simp add: isUb_def)
99 lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
100 by (simp add: isUb_def)
102 lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
103 apply (simp add: isLub_def)
104 apply (blast intro!: leastPD3)
105 done
107 lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
108 apply (simp add: ubs_def isLub_def)
109 apply (erule leastPD2)
110 done
112 end