1 (* Title: HOL/Cardinals/Order_Relation_More_Base.thy
2 Author: Andrei Popescu, TU Muenchen
5 Basics on order-like relations (base).
8 header {* Basics on Order-Like Relations (Base) *}
10 theory Order_Relation_More_Base
11 imports "~~/src/HOL/Library/Order_Relation"
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. *}
22 locale rel = fixes r :: "'a rel"
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"}. *}
32 subsection {* Auxiliaries *}
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)
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)
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)
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
55 lemma Total_subset_Id:
56 assumes TOT: "Total r" and SUB: "r \<le> Id"
57 shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
59 {assume "r \<noteq> {}"
60 then obtain a b where 1: "(a,b) \<in> r" by fast
61 hence "a = b" using SUB by blast
62 hence 2: "(a,a) \<in> r" using 1 by simp
63 {fix c d assume "(c,d) \<in> r"
64 hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
65 hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
66 ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
67 using TOT unfolding total_on_def by blast
68 hence "a = c \<and> a = d" using SUB by blast
70 hence "r \<le> {(a,a)}" by auto
71 with 2 have "\<exists>a. r = {(a,a)}" by blast
77 lemma Linear_order_in_diff_Id:
78 assumes LI: "Linear_order r" and
79 IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
80 shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
81 using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
84 subsection {* The upper and lower bounds operators *}
87 text{* Here we define upper (``above") and lower (``below") bounds operators.
88 We think of @{text "r"} as a {\em non-strict} relation. The suffix ``S"
89 at the names of some operators indicates that the bounds are strict -- e.g.,
90 @{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
91 Capitalization of the first letter in the name reminds that the operator acts on sets, rather
92 than on individual elements. *}
94 definition under::"'a \<Rightarrow> 'a set"
95 where "under a \<equiv> {b. (b,a) \<in> r}"
97 definition underS::"'a \<Rightarrow> 'a set"
98 where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
100 definition Under::"'a set \<Rightarrow> 'a set"
101 where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
103 definition UnderS::"'a set \<Rightarrow> 'a set"
104 where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
106 definition above::"'a \<Rightarrow> 'a set"
107 where "above a \<equiv> {b. (a,b) \<in> r}"
109 definition aboveS::"'a \<Rightarrow> 'a set"
110 where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
112 definition Above::"'a set \<Rightarrow> 'a set"
113 where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
115 definition AboveS::"'a set \<Rightarrow> 'a set"
116 where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
119 text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
120 we bounded comprehension by @{text "Field r"} in order to properly cover
121 the case of @{text "A"} being empty. *}
124 lemma UnderS_subset_Under: "UnderS A \<le> Under A"
125 by(auto simp add: UnderS_def Under_def)
128 lemma underS_subset_under: "underS a \<le> under a"
129 by(auto simp add: underS_def under_def)
132 lemma underS_notIn: "a \<notin> underS a"
133 by(simp add: underS_def)
136 lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
137 by(simp add: refl_on_def under_def)
140 lemma AboveS_disjoint: "A Int (AboveS A) = {}"
141 by(auto simp add: AboveS_def)
144 lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
145 by(auto simp add: AboveS_def underS_def)
148 lemma Refl_under_underS:
149 assumes "Refl r" "a \<in> Field r"
150 shows "under a = underS a \<union> {a}"
151 unfolding under_def underS_def
152 using assms refl_on_def[of _ r] by fastforce
155 lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
156 by (auto simp: Field_def underS_def)
159 lemma under_Field: "under a \<le> Field r"
160 by(unfold under_def Field_def, auto)
163 lemma underS_Field: "underS a \<le> Field r"
164 by(unfold underS_def Field_def, auto)
168 "a \<in> Field r \<Longrightarrow> underS a < Field r"
169 using assms underS_notIn underS_Field by blast
173 "Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
174 by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
177 lemma Under_Field: "Under A \<le> Field r"
178 by(unfold Under_def Field_def, auto)
181 lemma UnderS_Field: "UnderS A \<le> Field r"
182 by(unfold UnderS_def Field_def, auto)
185 lemma AboveS_Field: "AboveS A \<le> Field r"
186 by(unfold AboveS_def Field_def, auto)
190 assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
191 shows "under a \<le> under b"
192 proof(unfold under_def, auto)
193 fix x assume "(x,a) \<in> r"
194 with REL TRANS trans_def[of r]
195 show "(x,b) \<in> r" by blast
200 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
202 shows "underS a \<le> underS b"
203 proof(unfold underS_def, auto)
204 assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
205 with ANTISYM antisym_def[of r] REL
208 fix x assume "x \<noteq> a" "(x,a) \<in> r"
209 with REL TRANS trans_def[of r]
210 show "(x,b) \<in> r" by blast
214 lemma underS_incl_iff:
215 assumes LO: "Linear_order r" and
216 INa: "a \<in> Field r" and INb: "b \<in> Field r"
217 shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
219 assume "(a,b) \<in> r"
220 thus "underS a \<le> underS b" using LO
221 by (simp add: order_on_defs underS_incr)
223 assume *: "underS a \<le> underS b"
225 hence "(a,b) \<in> r" using assms
226 by (simp add: order_on_defs refl_on_def)
229 {assume "a \<noteq> b \<and> (b,a) \<in> r"
230 hence "b \<in> underS a" unfolding underS_def by blast
231 hence "b \<in> underS b" using * by blast
232 hence False by (simp add: underS_notIn)
235 show "(a,b) \<in> r" using assms
236 order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
240 lemma under_Under_trans:
241 assumes TRANS: "trans r" and
242 IN1: "a \<in> under b" and IN2: "b \<in> Under C"
243 shows "a \<in> Under C"
245 have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
246 using IN1 IN2 under_def Under_def by blast
247 hence "\<forall>c \<in> C. (a,c) \<in> r"
248 using TRANS trans_def[of r] by blast
250 have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
252 show ?thesis unfolding Under_def by blast
256 lemma under_UnderS_trans:
257 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
258 IN1: "a \<in> under b" and IN2: "b \<in> UnderS C"
259 shows "a \<in> UnderS C"
261 from IN2 have "b \<in> Under C"
262 using UnderS_subset_Under[of C] by blast
263 with assms under_Under_trans
264 have "a \<in> Under C" by blast
269 assume *: "a \<in> C"
270 have 1: "(a,b) \<in> r"
271 using IN1 under_def[of b] by auto
272 have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
273 using IN2 UnderS_def[of C] by blast
274 with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
275 with 1 ANTISYM antisym_def[of r]
280 show ?thesis unfolding UnderS_def Under_def by fast
284 end (* context rel *)