src/HOL/Cardinals/Order_Relation_More.thy
 author wenzelm Thu May 26 17:51:22 2016 +0200 (2016-05-26) changeset 63167 0909deb8059b parent 60585 48fdff264eb2 permissions -rw-r--r--
isabelle update_cartouches -c -t;
1 (*  Title:      HOL/Cardinals/Order_Relation_More.thy
2     Author:     Andrei Popescu, TU Muenchen
5 Basics on order-like relations.
6 *)
8 section \<open>Basics on Order-Like Relations\<close>
10 theory Order_Relation_More
11 imports Main
12 begin
14 subsection \<open>The upper and lower bounds operators\<close>
16 lemma aboveS_subset_above: "aboveS r a \<le> above r a"
17 by(auto simp add: aboveS_def above_def)
19 lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
20 by(auto simp add: AboveS_def Above_def)
22 lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
23 by(auto simp add: UnderS_def)
25 lemma aboveS_notIn: "a \<notin> aboveS r a"
26 by(auto simp add: aboveS_def)
28 lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
29 by(auto simp add: refl_on_def above_def)
31 lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
32 by(auto simp add: Above_def under_def)
34 lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
35 by(auto simp add: Under_def above_def)
37 lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
38 by(auto simp add: UnderS_def aboveS_def)
40 lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
41 by(auto simp add: UnderS_def Under_def)
43 lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
44 by(auto simp add: Above_def Under_def)
46 lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
47 by(auto simp add: Under_def Above_def)
49 lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
50 by(auto simp add: AboveS_def UnderS_def)
52 lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
53 by(auto simp add: UnderS_def AboveS_def)
55 lemma Under_Above_Galois:
56 "\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
57 by(unfold Above_def Under_def, blast)
59 lemma UnderS_AboveS_Galois:
60 "\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
61 by(unfold AboveS_def UnderS_def, blast)
63 lemma Refl_above_aboveS:
64   assumes REFL: "Refl r" and IN: "a \<in> Field r"
65   shows "above r a = aboveS r a \<union> {a}"
66 proof(unfold above_def aboveS_def, auto)
67   show "(a,a) \<in> r" using REFL IN refl_on_def[of _ r] by blast
68 qed
70 lemma Linear_order_under_aboveS_Field:
71   assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
72   shows "Field r = under r a \<union> aboveS r a"
73 proof(unfold under_def aboveS_def, auto)
74   assume "a \<in> Field r" "(a, a) \<notin> r"
75   with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
76   show False by auto
77 next
78   fix b assume "b \<in> Field r" "(b, a) \<notin> r"
79   with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
80   have "(a,b) \<in> r \<or> a = b" by blast
81   thus "(a,b) \<in> r"
82   using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
83 next
84   fix b assume "(b, a) \<in> r"
85   thus "b \<in> Field r"
86   using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
87 next
88   fix b assume "b \<noteq> a" "(a, b) \<in> r"
89   thus "b \<in> Field r"
90   using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
91 qed
93 lemma Linear_order_underS_above_Field:
94 assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
95 shows "Field r = underS r a \<union> above r a"
96 proof(unfold underS_def above_def, auto)
97   assume "a \<in> Field r" "(a, a) \<notin> r"
98   with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
99   show False by metis
100 next
101   fix b assume "b \<in> Field r" "(a, b) \<notin> r"
102   with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
103   have "(b,a) \<in> r \<or> b = a" by blast
104   thus "(b,a) \<in> r"
105   using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
106 next
107   fix b assume "b \<noteq> a" "(b, a) \<in> r"
108   thus "b \<in> Field r"
109   using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
110 next
111   fix b assume "(a, b) \<in> r"
112   thus "b \<in> Field r"
113   using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
114 qed
116 lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
117 unfolding Field_def under_def by auto
119 lemma Under_Field: "Under r A \<le> Field r"
120 by(unfold Under_def Field_def, auto)
122 lemma UnderS_Field: "UnderS r A \<le> Field r"
123 by(unfold UnderS_def Field_def, auto)
125 lemma above_Field: "above r a \<le> Field r"
126 by(unfold above_def Field_def, auto)
128 lemma aboveS_Field: "aboveS r a \<le> Field r"
129 by(unfold aboveS_def Field_def, auto)
131 lemma Above_Field: "Above r A \<le> Field r"
132 by(unfold Above_def Field_def, auto)
134 lemma Refl_under_Under:
135 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
136 shows "Under r A = (\<Inter>a \<in> A. under r a)"
137 proof
138   show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
139   by(unfold Under_def under_def, auto)
140 next
141   show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
142   proof(auto)
143     fix x
144     assume *: "\<forall>xa \<in> A. x \<in> under r xa"
145     hence "\<forall>xa \<in> A. (x,xa) \<in> r"
146     by (simp add: under_def)
147     moreover
148     {from NE obtain a where "a \<in> A" by blast
149      with * have "x \<in> under r a" by simp
150      hence "x \<in> Field r"
151      using under_Field[of r a] by auto
152     }
153     ultimately show "x \<in> Under r A"
154     unfolding Under_def by auto
155   qed
156 qed
158 lemma Refl_underS_UnderS:
159 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
160 shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
161 proof
162   show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
163   by(unfold UnderS_def underS_def, auto)
164 next
165   show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
166   proof(auto)
167     fix x
168     assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
169     hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
170     by (auto simp add: underS_def)
171     moreover
172     {from NE obtain a where "a \<in> A" by blast
173      with * have "x \<in> underS r a" by simp
174      hence "x \<in> Field r"
175      using underS_Field[of _ r a] by auto
176     }
177     ultimately show "x \<in> UnderS r A"
178     unfolding UnderS_def by auto
179   qed
180 qed
182 lemma Refl_above_Above:
183 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
184 shows "Above r A = (\<Inter>a \<in> A. above r a)"
185 proof
186   show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
187   by(unfold Above_def above_def, auto)
188 next
189   show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
190   proof(auto)
191     fix x
192     assume *: "\<forall>xa \<in> A. x \<in> above r xa"
193     hence "\<forall>xa \<in> A. (xa,x) \<in> r"
194     by (simp add: above_def)
195     moreover
196     {from NE obtain a where "a \<in> A" by blast
197      with * have "x \<in> above r a" by simp
198      hence "x \<in> Field r"
199      using above_Field[of r a] by auto
200     }
201     ultimately show "x \<in> Above r A"
202     unfolding Above_def by auto
203   qed
204 qed
206 lemma Refl_aboveS_AboveS:
207 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
208 shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
209 proof
210   show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
211   by(unfold AboveS_def aboveS_def, auto)
212 next
213   show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
214   proof(auto)
215     fix x
216     assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
217     hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
218     by (auto simp add: aboveS_def)
219     moreover
220     {from NE obtain a where "a \<in> A" by blast
221      with * have "x \<in> aboveS r a" by simp
222      hence "x \<in> Field r"
223      using aboveS_Field[of r a] by auto
224     }
225     ultimately show "x \<in> AboveS r A"
226     unfolding AboveS_def by auto
227   qed
228 qed
230 lemma under_Under_singl: "under r a = Under r {a}"
231 by(unfold Under_def under_def, auto simp add: Field_def)
233 lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
234 by(unfold UnderS_def underS_def, auto simp add: Field_def)
236 lemma above_Above_singl: "above r a = Above r {a}"
237 by(unfold Above_def above_def, auto simp add: Field_def)
239 lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
240 by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
242 lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
243 by(unfold Under_def, auto)
245 lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
246 by(unfold UnderS_def, auto)
248 lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
249 by(unfold Above_def, auto)
251 lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
252 by(unfold AboveS_def, auto)
254 lemma under_incl_iff:
255 assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
256 shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
257 proof
258   assume "(a,b) \<in> r"
259   thus "under r a \<le> under r b" using TRANS
260   by (auto simp add: under_incr)
261 next
262   assume "under r a \<le> under r b"
263   moreover
264   have "a \<in> under r a" using REFL IN
265   by (auto simp add: Refl_under_in)
266   ultimately show "(a,b) \<in> r"
267   by (auto simp add: under_def)
268 qed
270 lemma above_decr:
271 assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
272 shows "above r b \<le> above r a"
273 proof(unfold above_def, auto)
274   fix x assume "(b,x) \<in> r"
275   with REL TRANS trans_def[of r]
276   show "(a,x) \<in> r" by blast
277 qed
279 lemma aboveS_decr:
280 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
281         REL: "(a,b) \<in> r"
282 shows "aboveS r b \<le> aboveS r a"
283 proof(unfold aboveS_def, auto)
284   assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
285   with ANTISYM antisym_def[of r] REL
286   show False by auto
287 next
288   fix x assume "x \<noteq> b" "(b,x) \<in> r"
289   with REL TRANS trans_def[of r]
290   show "(a,x) \<in> r" by blast
291 qed
293 lemma under_trans:
294 assumes TRANS: "trans r" and
295         IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
296 shows "a \<in> under r c"
297 proof-
298   have "(a,b) \<in> r \<and> (b,c) \<in> r"
299   using IN1 IN2 under_def by fastforce
300   hence "(a,c) \<in> r"
301   using TRANS trans_def[of r] by blast
302   thus ?thesis unfolding under_def by simp
303 qed
305 lemma under_underS_trans:
306 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
307         IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
308 shows "a \<in> underS r c"
309 proof-
310   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
311   using IN1 IN2 under_def underS_def by fastforce
312   hence 1: "(a,c) \<in> r"
313   using TRANS trans_def[of r] by blast
314   have 2: "b \<noteq> c" using IN2 underS_def by force
315   have 3: "a \<noteq> c"
316   proof
317     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
318     show False by auto
319   qed
320   from 1 3 show ?thesis unfolding underS_def by simp
321 qed
323 lemma underS_under_trans:
324 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
325         IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
326 shows "a \<in> underS r c"
327 proof-
328   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
329   using IN1 IN2 under_def underS_def by fast
330   hence 1: "(a,c) \<in> r"
331   using TRANS trans_def[of r] by fast
332   have 2: "a \<noteq> b" using IN1 underS_def by force
333   have 3: "a \<noteq> c"
334   proof
335     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
336     show False by auto
337   qed
338   from 1 3 show ?thesis unfolding underS_def by simp
339 qed
341 lemma underS_underS_trans:
342 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
343         IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
344 shows "a \<in> underS r c"
345 proof-
346   have "a \<in> under r b"
347   using IN1 underS_subset_under by fast
348   with assms under_underS_trans show ?thesis by fast
349 qed
351 lemma above_trans:
352 assumes TRANS: "trans r" and
353         IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
354 shows "c \<in> above r a"
355 proof-
356   have "(a,b) \<in> r \<and> (b,c) \<in> r"
357   using IN1 IN2 above_def by fast
358   hence "(a,c) \<in> r"
359   using TRANS trans_def[of r] by blast
360   thus ?thesis unfolding above_def by simp
361 qed
363 lemma above_aboveS_trans:
364 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
365         IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
366 shows "c \<in> aboveS r a"
367 proof-
368   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
369   using IN1 IN2 above_def aboveS_def by fast
370   hence 1: "(a,c) \<in> r"
371   using TRANS trans_def[of r] by blast
372   have 2: "b \<noteq> c" using IN2 aboveS_def by force
373   have 3: "a \<noteq> c"
374   proof
375     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
376     show False by auto
377   qed
378   from 1 3 show ?thesis unfolding aboveS_def by simp
379 qed
381 lemma aboveS_above_trans:
382 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
383         IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
384 shows "c \<in> aboveS r a"
385 proof-
386   have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
387   using IN1 IN2 above_def aboveS_def by fast
388   hence 1: "(a,c) \<in> r"
389   using TRANS trans_def[of r] by blast
390   have 2: "a \<noteq> b" using IN1 aboveS_def by force
391   have 3: "a \<noteq> c"
392   proof
393     assume "a = c" with 0 2 ANTISYM antisym_def[of r]
394     show False by auto
395   qed
396   from 1 3 show ?thesis unfolding aboveS_def by simp
397 qed
399 lemma aboveS_aboveS_trans:
400 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
401         IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
402 shows "c \<in> aboveS r a"
403 proof-
404   have "b \<in> above r a"
405   using IN1 aboveS_subset_above by fast
406   with assms above_aboveS_trans show ?thesis by fast
407 qed
409 lemma under_Under_trans:
410 assumes TRANS: "trans r" and
411         IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
412 shows "a \<in> Under r C"
413 proof-
414   have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
415     using IN2 Under_def by force
416   hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
417     using IN1 under_def by fast
418   hence "\<forall>c \<in> C. (a,c) \<in> r"
419   using TRANS trans_def[of r] by blast
420   moreover
421   have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
422   ultimately
423   show ?thesis unfolding Under_def by blast
424 qed
426 lemma underS_Under_trans:
427 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
428         IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
429 shows "a \<in> UnderS r C"
430 proof-
431   from IN1 have "a \<in> under r b"
432   using underS_subset_under[of r b] by fast
433   with assms under_Under_trans
434   have "a \<in> Under r C" by fast
435   (*  *)
436   moreover
437   have "a \<notin> C"
438   proof
439     assume *: "a \<in> C"
440     have 1: "b \<noteq> a \<and> (a,b) \<in> r"
441     using IN1 underS_def[of r b] by auto
442     have "\<forall>c \<in> C. (b,c) \<in> r"
443     using IN2 Under_def[of r C] by auto
444     with * have "(b,a) \<in> r" by simp
445     with 1 ANTISYM antisym_def[of r]
446     show False by blast
447   qed
448   (*  *)
449   ultimately
450   show ?thesis unfolding UnderS_def
451   using Under_def by force
452 qed
454 lemma underS_UnderS_trans:
455 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
456         IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
457 shows "a \<in> UnderS r C"
458 proof-
459   from IN2 have "b \<in> Under r C"
460   using UnderS_subset_Under[of r C] by blast
461   with underS_Under_trans assms
462   show ?thesis by force
463 qed
465 lemma above_Above_trans:
466 assumes TRANS: "trans r" and
467         IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
468 shows "a \<in> Above r C"
469 proof-
470   have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
471     using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
472   hence "\<forall>c \<in> C. (c,a) \<in> r"
473   using TRANS trans_def[of r] by blast
474   moreover
475   have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
476   ultimately
477   show ?thesis unfolding Above_def by auto
478 qed
480 lemma aboveS_Above_trans:
481 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
482         IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
483 shows "a \<in> AboveS r C"
484 proof-
485   from IN1 have "a \<in> above r b"
486   using aboveS_subset_above[of r b] by blast
487   with assms above_Above_trans
488   have "a \<in> Above r C" by fast
489   (*  *)
490   moreover
491   have "a \<notin> C"
492   proof
493     assume *: "a \<in> C"
494     have 1: "b \<noteq> a \<and> (b,a) \<in> r"
495     using IN1 aboveS_def[of r b] by auto
496     have "\<forall>c \<in> C. (c,b) \<in> r"
497     using IN2 Above_def[of r C] by auto
498     with * have "(a,b) \<in> r" by simp
499     with 1 ANTISYM antisym_def[of r]
500     show False by blast
501   qed
502   (*  *)
503   ultimately
504   show ?thesis unfolding AboveS_def
505   using Above_def by force
506 qed
508 lemma above_AboveS_trans:
509 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
510         IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
511 shows "a \<in> AboveS r C"
512 proof-
513   from IN2 have "b \<in> Above r C"
514   using AboveS_subset_Above[of r C] by blast
515   with assms above_Above_trans
516   have "a \<in> Above r C" by force
517   (*  *)
518   moreover
519   have "a \<notin> C"
520   proof
521     assume *: "a \<in> C"
522     have 1: "(b,a) \<in> r"
523     using IN1 above_def[of r b] by auto
524     have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
525     using IN2 AboveS_def[of r C] by auto
526     with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
527     with 1 ANTISYM antisym_def[of r]
528     show False by blast
529   qed
530   (*  *)
531   ultimately
532   show ?thesis unfolding AboveS_def
533   using Above_def by force
534 qed
536 lemma aboveS_AboveS_trans:
537 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
538         IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
539 shows "a \<in> AboveS r C"
540 proof-
541   from IN2 have "b \<in> Above r C"
542   using AboveS_subset_Above[of r C] by blast
543   with aboveS_Above_trans assms
544   show ?thesis by force
545 qed
547 lemma under_UnderS_trans:
548 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
549         IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
550 shows "a \<in> UnderS r C"
551 proof-
552   from IN2 have "b \<in> Under r C"
553   using UnderS_subset_Under[of r C] by blast
554   with assms under_Under_trans
555   have "a \<in> Under r C" by force
556   (*  *)
557   moreover
558   have "a \<notin> C"
559   proof
560     assume *: "a \<in> C"
561     have 1: "(a,b) \<in> r"
562     using IN1 under_def[of r b] by auto
563     have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
564     using IN2 UnderS_def[of r C] by blast
565     with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
566     with 1 ANTISYM antisym_def[of r]
567     show False by blast
568   qed
569   (*  *)
570   ultimately
571   show ?thesis unfolding UnderS_def Under_def by fast
572 qed
575 subsection \<open>Properties depending on more than one relation\<close>
577 lemma under_incr2:
578 "r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
579 unfolding under_def by blast
581 lemma underS_incr2:
582 "r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
583 unfolding underS_def by blast
585 (* FIXME: r \<leadsto> r'
586 lemma Under_incr:
587 "r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
588 unfolding Under_def by blast
590 lemma UnderS_incr:
591 "r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
592 unfolding UnderS_def by blast
594 lemma Under_incr_decr:
595 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Under r A \<le> Under r A'"
596 unfolding Under_def by blast
598 lemma UnderS_incr_decr:
599 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> UnderS r A \<le> UnderS r A'"
600 unfolding UnderS_def by blast
601 *)
603 lemma above_incr2:
604 "r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
605 unfolding above_def by blast
607 lemma aboveS_incr2:
608 "r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
609 unfolding aboveS_def by blast
611 (* FIXME
612 lemma Above_incr:
613 "r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
614 unfolding Above_def by blast
616 lemma AboveS_incr:
617 "r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
618 unfolding AboveS_def by blast
620 lemma Above_incr_decr:
621 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
622 unfolding Above_def by blast
624 lemma AboveS_incr_decr:
625 "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
626 unfolding AboveS_def by blast
627 *)
629 end