src/HOL/Library/Glbs.thy
 author hoelzl Tue Mar 05 15:43:13 2013 +0100 (2013-03-05) changeset 51342 763c6872bd10 parent 46509 c4b2ec379fdd permissions -rw-r--r--
generalized isGlb_unique
```     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 greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    10   where "greatestP P x = (P x \<and> Collect P *<=  x)"
```
```    11
```
```    12 definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    13   where "isLb R S x = (x <=* S \<and> x: R)"
```
```    14
```
```    15 definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
```
```    16   where "isGlb R S x = greatestP (isLb R S) x"
```
```    17
```
```    18 definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
```
```    19   where "lbs R S = Collect (isLb R S)"
```
```    20
```
```    21
```
```    22 subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
```
```    23   and @{term isGlb} *}
```
```    24
```
```    25 lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
```
```    26   by (simp add: greatestP_def)
```
```    27
```
```    28 lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
```
```    29   by (simp add: greatestP_def)
```
```    30
```
```    31 lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
```
```    32   by (blast dest!: greatestPD2 setleD)
```
```    33
```
```    34 lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
```
```    35   by (simp add: isGlb_def isLb_def greatestP_def)
```
```    36
```
```    37 lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
```
```    38   by (simp add: isGlb_def isLb_def greatestP_def)
```
```    39
```
```    40 lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
```
```    41   unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
```
```    42
```
```    43 lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
```
```    44   by (blast dest!: isGlbD1 setgeD)
```
```    45
```
```    46 lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
```
```    47   by (simp add: isGlb_def)
```
```    48
```
```    49 lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
```
```    50   by (simp add: isGlb_def)
```
```    51
```
```    52 lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
```
```    53   by (simp add: isGlb_def greatestP_def)
```
```    54
```
```    55 lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
```
```    56   by (simp add: isLb_def setge_def)
```
```    57
```
```    58 lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
```
```    59   by (simp add: isLb_def)
```
```    60
```
```    61 lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
```
```    62   by (simp add: isLb_def)
```
```    63
```
```    64 lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
```
```    65   by (simp add: isLb_def)
```
```    66
```
```    67 lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
```
```    68   unfolding isGlb_def by (blast intro!: greatestPD3)
```
```    69
```
```    70 lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
```
```    71   unfolding lbs_def isGlb_def by (rule greatestPD2)
```
```    72
```
```    73 lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
```
```    74   apply (frule isGlb_isLb)
```
```    75   apply (frule_tac x = y in isGlb_isLb)
```
```    76   apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
```
```    77   done
```
```    78
```
```    79 end
```