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 |
|