|
1 (* Title: HOL/Cardinals/Order_Relation_More_Base.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Basics on order-like relations (base). |
|
6 *) |
|
7 |
|
8 header {* Basics on Order-Like Relations (Base) *} |
|
9 |
|
10 theory Order_Relation_More_Base |
|
11 imports "~~/src/HOL/Library/Order_Relation" |
|
12 begin |
|
13 |
|
14 |
|
15 text{* In this section, we develop basic concepts and results pertaining |
|
16 to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or |
|
17 total relations. The development is placed on top of the definitions |
|
18 from the theory @{text "Order_Relation"}. We also |
|
19 further define upper and lower bounds operators. *} |
|
20 |
|
21 |
|
22 locale rel = fixes r :: "'a rel" |
|
23 |
|
24 text{* The following context encompasses all this section, except |
|
25 for its last subsection. In other words, for the rest of this section except its last |
|
26 subsection, we consider a fixed relation @{text "r"}. *} |
|
27 |
|
28 context rel |
|
29 begin |
|
30 |
|
31 |
|
32 subsection {* Auxiliaries *} |
|
33 |
|
34 |
|
35 lemma refl_on_domain: |
|
36 "\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A" |
|
37 by(auto simp add: refl_on_def) |
|
38 |
|
39 |
|
40 corollary well_order_on_domain: |
|
41 "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A" |
|
42 by(simp add: refl_on_domain order_on_defs) |
|
43 |
|
44 |
|
45 lemma well_order_on_Field: |
|
46 "well_order_on A r \<Longrightarrow> A = Field r" |
|
47 by(auto simp add: refl_on_def Field_def order_on_defs) |
|
48 |
|
49 |
|
50 lemma well_order_on_Well_order: |
|
51 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r" |
|
52 using well_order_on_Field by simp |
|
53 |
|
54 |
|
55 lemma Total_Id_Field: |
|
56 assumes TOT: "Total r" and NID: "\<not> (r <= Id)" |
|
57 shows "Field r = Field(r - Id)" |
|
58 using mono_Field[of "r - Id" r] Diff_subset[of r Id] |
|
59 proof(auto) |
|
60 have "r \<noteq> {}" using NID by fast |
|
61 then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast |
|
62 hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) |
|
63 (* *) |
|
64 fix a assume *: "a \<in> Field r" |
|
65 obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" |
|
66 using * 1 by blast |
|
67 hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT |
|
68 by (simp add: total_on_def) |
|
69 thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast |
|
70 qed |
|
71 |
|
72 |
|
73 lemma Total_subset_Id: |
|
74 assumes TOT: "Total r" and SUB: "r \<le> Id" |
|
75 shows "r = {} \<or> (\<exists>a. r = {(a,a)})" |
|
76 proof- |
|
77 {assume "r \<noteq> {}" |
|
78 then obtain a b where 1: "(a,b) \<in> r" by fast |
|
79 hence "a = b" using SUB by blast |
|
80 hence 2: "(a,a) \<in> r" using 1 by simp |
|
81 {fix c d assume "(c,d) \<in> r" |
|
82 hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast |
|
83 hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and> |
|
84 ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)" |
|
85 using TOT unfolding total_on_def by blast |
|
86 hence "a = c \<and> a = d" using SUB by blast |
|
87 } |
|
88 hence "r \<le> {(a,a)}" by auto |
|
89 with 2 have "\<exists>a. r = {(a,a)}" by blast |
|
90 } |
|
91 thus ?thesis by blast |
|
92 qed |
|
93 |
|
94 |
|
95 lemma Linear_order_in_diff_Id: |
|
96 assumes LI: "Linear_order r" and |
|
97 IN1: "a \<in> Field r" and IN2: "b \<in> Field r" |
|
98 shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)" |
|
99 using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force |
|
100 |
|
101 |
|
102 subsection {* The upper and lower bounds operators *} |
|
103 |
|
104 |
|
105 text{* Here we define upper (``above") and lower (``below") bounds operators. |
|
106 We think of @{text "r"} as a {\em non-strict} relation. The suffix ``S" |
|
107 at the names of some operators indicates that the bounds are strict -- e.g., |
|
108 @{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}). |
|
109 Capitalization of the first letter in the name reminds that the operator acts on sets, rather |
|
110 than on individual elements. *} |
|
111 |
|
112 definition under::"'a \<Rightarrow> 'a set" |
|
113 where "under a \<equiv> {b. (b,a) \<in> r}" |
|
114 |
|
115 definition underS::"'a \<Rightarrow> 'a set" |
|
116 where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}" |
|
117 |
|
118 definition Under::"'a set \<Rightarrow> 'a set" |
|
119 where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}" |
|
120 |
|
121 definition UnderS::"'a set \<Rightarrow> 'a set" |
|
122 where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}" |
|
123 |
|
124 definition above::"'a \<Rightarrow> 'a set" |
|
125 where "above a \<equiv> {b. (a,b) \<in> r}" |
|
126 |
|
127 definition aboveS::"'a \<Rightarrow> 'a set" |
|
128 where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}" |
|
129 |
|
130 definition Above::"'a set \<Rightarrow> 'a set" |
|
131 where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}" |
|
132 |
|
133 definition AboveS::"'a set \<Rightarrow> 'a set" |
|
134 where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}" |
|
135 (* *) |
|
136 |
|
137 text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"}, |
|
138 we bounded comprehension by @{text "Field r"} in order to properly cover |
|
139 the case of @{text "A"} being empty. *} |
|
140 |
|
141 |
|
142 lemma UnderS_subset_Under: "UnderS A \<le> Under A" |
|
143 by(auto simp add: UnderS_def Under_def) |
|
144 |
|
145 |
|
146 lemma underS_subset_under: "underS a \<le> under a" |
|
147 by(auto simp add: underS_def under_def) |
|
148 |
|
149 |
|
150 lemma underS_notIn: "a \<notin> underS a" |
|
151 by(simp add: underS_def) |
|
152 |
|
153 |
|
154 lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a" |
|
155 by(simp add: refl_on_def under_def) |
|
156 |
|
157 |
|
158 lemma AboveS_disjoint: "A Int (AboveS A) = {}" |
|
159 by(auto simp add: AboveS_def) |
|
160 |
|
161 |
|
162 lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)" |
|
163 by(auto simp add: AboveS_def underS_def) |
|
164 |
|
165 |
|
166 lemma Refl_under_underS: |
|
167 assumes "Refl r" "a \<in> Field r" |
|
168 shows "under a = underS a \<union> {a}" |
|
169 unfolding under_def underS_def |
|
170 using assms refl_on_def[of _ r] by fastforce |
|
171 |
|
172 |
|
173 lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}" |
|
174 by (auto simp: Field_def underS_def) |
|
175 |
|
176 |
|
177 lemma under_Field: "under a \<le> Field r" |
|
178 by(unfold under_def Field_def, auto) |
|
179 |
|
180 |
|
181 lemma underS_Field: "underS a \<le> Field r" |
|
182 by(unfold underS_def Field_def, auto) |
|
183 |
|
184 |
|
185 lemma underS_Field2: |
|
186 "a \<in> Field r \<Longrightarrow> underS a < Field r" |
|
187 using assms underS_notIn underS_Field by blast |
|
188 |
|
189 |
|
190 lemma underS_Field3: |
|
191 "Field r \<noteq> {} \<Longrightarrow> underS a < Field r" |
|
192 by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty) |
|
193 |
|
194 |
|
195 lemma Under_Field: "Under A \<le> Field r" |
|
196 by(unfold Under_def Field_def, auto) |
|
197 |
|
198 |
|
199 lemma UnderS_Field: "UnderS A \<le> Field r" |
|
200 by(unfold UnderS_def Field_def, auto) |
|
201 |
|
202 |
|
203 lemma AboveS_Field: "AboveS A \<le> Field r" |
|
204 by(unfold AboveS_def Field_def, auto) |
|
205 |
|
206 |
|
207 lemma under_incr: |
|
208 assumes TRANS: "trans r" and REL: "(a,b) \<in> r" |
|
209 shows "under a \<le> under b" |
|
210 proof(unfold under_def, auto) |
|
211 fix x assume "(x,a) \<in> r" |
|
212 with REL TRANS trans_def[of r] |
|
213 show "(x,b) \<in> r" by blast |
|
214 qed |
|
215 |
|
216 |
|
217 lemma underS_incr: |
|
218 assumes TRANS: "trans r" and ANTISYM: "antisym r" and |
|
219 REL: "(a,b) \<in> r" |
|
220 shows "underS a \<le> underS b" |
|
221 proof(unfold underS_def, auto) |
|
222 assume *: "b \<noteq> a" and **: "(b,a) \<in> r" |
|
223 with ANTISYM antisym_def[of r] REL |
|
224 show False by blast |
|
225 next |
|
226 fix x assume "x \<noteq> a" "(x,a) \<in> r" |
|
227 with REL TRANS trans_def[of r] |
|
228 show "(x,b) \<in> r" by blast |
|
229 qed |
|
230 |
|
231 |
|
232 lemma underS_incl_iff: |
|
233 assumes LO: "Linear_order r" and |
|
234 INa: "a \<in> Field r" and INb: "b \<in> Field r" |
|
235 shows "(underS a \<le> underS b) = ((a,b) \<in> r)" |
|
236 proof |
|
237 assume "(a,b) \<in> r" |
|
238 thus "underS a \<le> underS b" using LO |
|
239 by (simp add: order_on_defs underS_incr) |
|
240 next |
|
241 assume *: "underS a \<le> underS b" |
|
242 {assume "a = b" |
|
243 hence "(a,b) \<in> r" using assms |
|
244 by (simp add: order_on_defs refl_on_def) |
|
245 } |
|
246 moreover |
|
247 {assume "a \<noteq> b \<and> (b,a) \<in> r" |
|
248 hence "b \<in> underS a" unfolding underS_def by blast |
|
249 hence "b \<in> underS b" using * by blast |
|
250 hence False by (simp add: underS_notIn) |
|
251 } |
|
252 ultimately |
|
253 show "(a,b) \<in> r" using assms |
|
254 order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast |
|
255 qed |
|
256 |
|
257 |
|
258 lemma under_Under_trans: |
|
259 assumes TRANS: "trans r" and |
|
260 IN1: "a \<in> under b" and IN2: "b \<in> Under C" |
|
261 shows "a \<in> Under C" |
|
262 proof- |
|
263 have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)" |
|
264 using IN1 IN2 under_def Under_def by blast |
|
265 hence "\<forall>c \<in> C. (a,c) \<in> r" |
|
266 using TRANS trans_def[of r] by blast |
|
267 moreover |
|
268 have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast |
|
269 ultimately |
|
270 show ?thesis unfolding Under_def by blast |
|
271 qed |
|
272 |
|
273 |
|
274 lemma under_UnderS_trans: |
|
275 assumes TRANS: "trans r" and ANTISYM: "antisym r" and |
|
276 IN1: "a \<in> under b" and IN2: "b \<in> UnderS C" |
|
277 shows "a \<in> UnderS C" |
|
278 proof- |
|
279 from IN2 have "b \<in> Under C" |
|
280 using UnderS_subset_Under[of C] by blast |
|
281 with assms under_Under_trans |
|
282 have "a \<in> Under C" by blast |
|
283 (* *) |
|
284 moreover |
|
285 have "a \<notin> C" |
|
286 proof |
|
287 assume *: "a \<in> C" |
|
288 have 1: "(a,b) \<in> r" |
|
289 using IN1 under_def[of b] by auto |
|
290 have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r" |
|
291 using IN2 UnderS_def[of C] by blast |
|
292 with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast |
|
293 with 1 ANTISYM antisym_def[of r] |
|
294 show False by blast |
|
295 qed |
|
296 (* *) |
|
297 ultimately |
|
298 show ?thesis unfolding UnderS_def Under_def by fast |
|
299 qed |
|
300 |
|
301 |
|
302 end (* context rel *) |
|
303 |
|
304 end |