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