src/HOL/Library/Glbs.thy
author haftmann
Mon Mar 23 08:14:23 2009 +0100 (2009-03-23)
changeset 30661 54858c8ad226
parent 30267 171b3bd93c90
child 46509 c4b2ec379fdd
permissions -rw-r--r--
tuned header
     1 (* Author: Amine Chaieb, University of Cambridge *)
     2 
     3 header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
     4 
     5 theory Glbs
     6 imports Lubs
     7 begin
     8 
     9 definition
    10   greatestP      :: "['a =>bool,'a::ord] => bool" where
    11   "greatestP P x = (P x & Collect P *<=  x)"
    12 
    13 definition
    14   isLb        :: "['a set, 'a set, 'a::ord] => bool" where
    15   "isLb R S x = (x <=* S & x: R)"
    16 
    17 definition
    18   isGlb       :: "['a set, 'a set, 'a::ord] => bool" where
    19   "isGlb R S x = greatestP (isLb R S) x"
    20 
    21 definition
    22   lbs         :: "['a set, 'a::ord set] => 'a set" where
    23   "lbs R S = Collect (isLb R S)"
    24 
    25 subsection{*Rules about the Operators @{term greatestP}, @{term isLb}
    26     and @{term isGlb}*}
    27 
    28 lemma leastPD1: "greatestP P x ==> P x"
    29 by (simp add: greatestP_def)
    30 
    31 lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
    32 by (simp add: greatestP_def)
    33 
    34 lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y"
    35 by (blast dest!: greatestPD2 setleD)
    36 
    37 lemma isGlbD1: "isGlb R S x ==> x <=* S"
    38 by (simp add: isGlb_def isLb_def greatestP_def)
    39 
    40 lemma isGlbD1a: "isGlb R S x ==> x: R"
    41 by (simp add: isGlb_def isLb_def greatestP_def)
    42 
    43 lemma isGlb_isLb: "isGlb R S x ==> isLb R S x"
    44 apply (simp add: isLb_def)
    45 apply (blast dest: isGlbD1 isGlbD1a)
    46 done
    47 
    48 lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x"
    49 by (blast dest!: isGlbD1 setgeD)
    50 
    51 lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x"
    52 by (simp add: isGlb_def)
    53 
    54 lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x"
    55 by (simp add: isGlb_def)
    56 
    57 lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x"
    58 by (simp add: isGlb_def greatestP_def)
    59 
    60 lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x"
    61 by (simp add: isLb_def setge_def)
    62 
    63 lemma isLbD2: "isLb R S x ==> x <=* S "
    64 by (simp add: isLb_def)
    65 
    66 lemma isLbD2a: "isLb R S x ==> x: R"
    67 by (simp add: isLb_def)
    68 
    69 lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"
    70 by (simp add: isLb_def)
    71 
    72 lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y"
    73 apply (simp add: isGlb_def)
    74 apply (blast intro!: greatestPD3)
    75 done
    76 
    77 lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x"
    78 apply (simp add: lbs_def isGlb_def)
    79 apply (erule greatestPD2)
    80 done
    81 
    82 end