1 (* Title: HOL/Lubs.thy |
|
2 Author: Jacques D. Fleuriot, University of Cambridge |
|
3 *) |
|
4 |
|
5 header {* Definitions of Upper Bounds and Least Upper Bounds *} |
|
6 |
|
7 theory Lubs |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text {* Thanks to suggestions by James Margetson *} |
|
12 |
|
13 definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70) |
|
14 where "S *<= x = (ALL y: S. y \<le> x)" |
|
15 |
|
16 definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70) |
|
17 where "x <=* S = (ALL y: S. x \<le> y)" |
|
18 |
|
19 definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
|
20 where "leastP P x = (P x \<and> x <=* Collect P)" |
|
21 |
|
22 definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
|
23 where "isUb R S x = (S *<= x \<and> x: R)" |
|
24 |
|
25 definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
|
26 where "isLub R S x = leastP (isUb R S) x" |
|
27 |
|
28 definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
|
29 where "ubs R S = Collect (isUb R S)" |
|
30 |
|
31 |
|
32 subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *} |
|
33 |
|
34 lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x" |
|
35 by (simp add: setle_def) |
|
36 |
|
37 lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x" |
|
38 by (simp add: setle_def) |
|
39 |
|
40 lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S" |
|
41 by (simp add: setge_def) |
|
42 |
|
43 lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y" |
|
44 by (simp add: setge_def) |
|
45 |
|
46 |
|
47 subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *} |
|
48 |
|
49 lemma leastPD1: "leastP P x \<Longrightarrow> P x" |
|
50 by (simp add: leastP_def) |
|
51 |
|
52 lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P" |
|
53 by (simp add: leastP_def) |
|
54 |
|
55 lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y" |
|
56 by (blast dest!: leastPD2 setgeD) |
|
57 |
|
58 lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x" |
|
59 by (simp add: isLub_def isUb_def leastP_def) |
|
60 |
|
61 lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R" |
|
62 by (simp add: isLub_def isUb_def leastP_def) |
|
63 |
|
64 lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x" |
|
65 unfolding isUb_def by (blast dest: isLubD1 isLubD1a) |
|
66 |
|
67 lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
|
68 by (blast dest!: isLubD1 setleD) |
|
69 |
|
70 lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x" |
|
71 by (simp add: isLub_def) |
|
72 |
|
73 lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x" |
|
74 by (simp add: isLub_def) |
|
75 |
|
76 lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x" |
|
77 by (simp add: isLub_def leastP_def) |
|
78 |
|
79 lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
|
80 by (simp add: isUb_def setle_def) |
|
81 |
|
82 lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x" |
|
83 by (simp add: isUb_def) |
|
84 |
|
85 lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R" |
|
86 by (simp add: isUb_def) |
|
87 |
|
88 lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x" |
|
89 by (simp add: isUb_def) |
|
90 |
|
91 lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y" |
|
92 unfolding isLub_def by (blast intro!: leastPD3) |
|
93 |
|
94 lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S" |
|
95 unfolding ubs_def isLub_def by (rule leastPD2) |
|
96 |
|
97 lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)" |
|
98 apply (frule isLub_isUb) |
|
99 apply (frule_tac x = y in isLub_isUb) |
|
100 apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
|
101 done |
|
102 |
|
103 end |
|