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