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