src/HOL/Library/Glbs.thy
changeset 29838 a562ca0c408d
child 30267 171b3bd93c90
     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.35 +by (simp add: greatestP_def)
    1.36 +
    1.37 +lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
    1.38 +by (simp add: greatestP_def)
    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.50 +apply (simp add: isLb_def)
    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.58 +by (simp add: isGlb_def)
    1.59 +
    1.60 +lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x"
    1.61 +by (simp add: isGlb_def)
    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.70 +by (simp add: isLb_def)
    1.71 +
    1.72 +lemma isLbD2a: "isLb R S x ==> x: R"
    1.73 +by (simp add: isLb_def)
    1.74 +
    1.75 +lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"
    1.76 +by (simp add: isLb_def)
    1.77 +
    1.78 +lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y"
    1.79 +apply (simp add: isGlb_def)
    1.80 +apply (blast intro!: greatestPD3)
    1.81 +done
    1.82 +
    1.83 +lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x"
    1.84 +apply (simp add: lbs_def isGlb_def)
    1.85 +apply (erule greatestPD2)
    1.86 +done
    1.87 +
    1.88 +end