author chaieb Mon Feb 09 16:19:46 2009 +0000 (2009-02-09) changeset 29838 a562ca0c408d parent 29837 eb7e62c0f53c child 29839 018ac1fa1ed3
A theory of greatest lower bounds
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Glbs.thy	Mon Feb 09 16:19:46 2009 +0000
1.3 @@ -0,0 +1,85 @@
1.4 +(* Title:      Glbs
1.5 +   ID:         \$Id:
1.6 +   Author:     Amine Chaieb, University of Cambridge
1.7 +*)
1.8 +
1.9 +header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
1.10 +
1.11 +theory Glbs
1.12 +imports Lubs
1.13 +begin
1.14 +
1.15 +definition
1.16 +  greatestP      :: "['a =>bool,'a::ord] => bool" where
1.17 +  "greatestP P x = (P x & Collect P *<=  x)"
1.18 +
1.19 +definition
1.20 +  isLb        :: "['a set, 'a set, 'a::ord] => bool" where
1.21 +  "isLb R S x = (x <=* S & x: R)"
1.22 +
1.23 +definition
1.24 +  isGlb       :: "['a set, 'a set, 'a::ord] => bool" where
1.25 +  "isGlb R S x = greatestP (isLb R S) x"
1.26 +
1.27 +definition
1.28 +  lbs         :: "['a set, 'a::ord set] => 'a set" where
1.29 +  "lbs R S = Collect (isLb R S)"
1.30 +
1.31 +subsection{*Rules about the Operators @{term greatestP}, @{term isLb}
1.32 +    and @{term isGlb}*}
1.33 +
1.34 +lemma leastPD1: "greatestP P x ==> P x"
1.36 +
1.37 +lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
1.39 +
1.40 +lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y"
1.41 +by (blast dest!: greatestPD2 setleD)
1.42 +
1.43 +lemma isGlbD1: "isGlb R S x ==> x <=* S"
1.44 +by (simp add: isGlb_def isLb_def greatestP_def)
1.45 +
1.46 +lemma isGlbD1a: "isGlb R S x ==> x: R"
1.47 +by (simp add: isGlb_def isLb_def greatestP_def)
1.48 +
1.49 +lemma isGlb_isLb: "isGlb R S x ==> isLb R S x"
1.51 +apply (blast dest: isGlbD1 isGlbD1a)
1.52 +done
1.53 +
1.54 +lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x"
1.55 +by (blast dest!: isGlbD1 setgeD)
1.56 +
1.57 +lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x"
1.59 +
1.60 +lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x"
1.62 +
1.63 +lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x"
1.64 +by (simp add: isGlb_def greatestP_def)
1.65 +
1.66 +lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x"
1.67 +by (simp add: isLb_def setge_def)
1.68 +
1.69 +lemma isLbD2: "isLb R S x ==> x <=* S "
1.71 +
1.72 +lemma isLbD2a: "isLb R S x ==> x: R"
1.74 +
1.75 +lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"