src/HOL/Library/Glbs.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 30661 54858c8ad226 child 46509 c4b2ec379fdd permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
```     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
```