src/HOL/Lubs.thy
 changeset 28952 15a4b2cf8c34 parent 27368 9f90ac19e32b child 29654 24e73987bfe2
1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Lubs.thy	Wed Dec 03 15:58:44 2008 +0100
1.3 @@ -0,0 +1,113 @@
1.4 +(*  Title       : Lubs.thy
1.5 +    ID          : \$Id\$
1.6 +    Author      : Jacques D. Fleuriot
1.7 +    Copyright   : 1998  University of Cambridge
1.8 +*)
1.9 +
1.10 +header{*Definitions of Upper Bounds and Least Upper Bounds*}
1.11 +
1.12 +theory Lubs
1.13 +imports Plain
1.14 +begin
1.15 +
1.16 +text{*Thanks to suggestions by James Margetson*}
1.17 +
1.18 +definition
1.19 +  setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
1.20 +  "S *<= x = (ALL y: S. y <= x)"
1.21 +
1.22 +definition
1.23 +  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
1.24 +  "x <=* S = (ALL y: S. x <= y)"
1.25 +
1.26 +definition
1.27 +  leastP      :: "['a =>bool,'a::ord] => bool" where
1.28 +  "leastP P x = (P x & x <=* Collect P)"
1.29 +
1.30 +definition
1.31 +  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
1.32 +  "isUb R S x = (S *<= x & x: R)"
1.33 +
1.34 +definition
1.35 +  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
1.36 +  "isLub R S x = leastP (isUb R S) x"
1.37 +
1.38 +definition
1.39 +  ubs         :: "['a set, 'a::ord set] => 'a set" where
1.40 +  "ubs R S = Collect (isUb R S)"
1.41 +
1.42 +
1.43 +
1.44 +subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
1.45 +
1.46 +lemma setleI: "ALL y: S. y <= x ==> S *<= x"
1.48 +
1.49 +lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
1.51 +
1.52 +lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
1.54 +
1.55 +lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
1.57 +
1.58 +
1.59 +subsection{*Rules about the Operators @{term leastP}, @{term ub}
1.60 +    and @{term lub}*}
1.61 +
1.62 +lemma leastPD1: "leastP P x ==> P x"
1.64 +
1.65 +lemma leastPD2: "leastP P x ==> x <=* Collect P"
1.67 +
1.68 +lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
1.69 +by (blast dest!: leastPD2 setgeD)
1.70 +
1.71 +lemma isLubD1: "isLub R S x ==> S *<= x"
1.72 +by (simp add: isLub_def isUb_def leastP_def)
1.73 +
1.74 +lemma isLubD1a: "isLub R S x ==> x: R"
1.75 +by (simp add: isLub_def isUb_def leastP_def)
1.76 +
1.77 +lemma isLub_isUb: "isLub R S x ==> isUb R S x"
1.79 +apply (blast dest: isLubD1 isLubD1a)
1.80 +done
1.81 +
1.82 +lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
1.83 +by (blast dest!: isLubD1 setleD)
1.84 +
1.85 +lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
1.87 +
1.88 +lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
1.90 +
1.91 +lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
1.92 +by (simp add: isLub_def leastP_def)
1.93 +
1.94 +lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
1.95 +by (simp add: isUb_def setle_def)
1.96 +
1.97 +lemma isUbD2: "isUb R S x ==> S *<= x"
1.99 +
1.100 +lemma isUbD2a: "isUb R S x ==> x: R"