13356
|
1 |
(* Title: ZF/Trancl.thy
|
1478
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
3 |
Copyright 1992 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
60770
|
6 |
section\<open>Relations: Their General Properties and Transitive Closure\<close>
|
13356
|
7 |
|
16417
|
8 |
theory Trancl imports Fixedpt Perm begin
|
13239
|
9 |
|
24893
|
10 |
definition
|
|
11 |
refl :: "[i,i]=>o" where
|
46820
|
12 |
"refl(A,r) == (\<forall>x\<in>A. <x,x> \<in> r)"
|
13239
|
13 |
|
24893
|
14 |
definition
|
|
15 |
irrefl :: "[i,i]=>o" where
|
46820
|
16 |
"irrefl(A,r) == \<forall>x\<in>A. <x,x> \<notin> r"
|
13239
|
17 |
|
24893
|
18 |
definition
|
|
19 |
sym :: "i=>o" where
|
46820
|
20 |
"sym(r) == \<forall>x y. <x,y>: r \<longrightarrow> <y,x>: r"
|
13239
|
21 |
|
24893
|
22 |
definition
|
|
23 |
asym :: "i=>o" where
|
46820
|
24 |
"asym(r) == \<forall>x y. <x,y>:r \<longrightarrow> ~ <y,x>:r"
|
13239
|
25 |
|
24893
|
26 |
definition
|
|
27 |
antisym :: "i=>o" where
|
46820
|
28 |
"antisym(r) == \<forall>x y.<x,y>:r \<longrightarrow> <y,x>:r \<longrightarrow> x=y"
|
13239
|
29 |
|
24893
|
30 |
definition
|
|
31 |
trans :: "i=>o" where
|
46820
|
32 |
"trans(r) == \<forall>x y z. <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
|
13239
|
33 |
|
24893
|
34 |
definition
|
69587
|
35 |
trans_on :: "[i,i]=>o" (\<open>trans[_]'(_')\<close>) where
|
46820
|
36 |
"trans[A](r) == \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A.
|
|
37 |
<x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
|
13239
|
38 |
|
24893
|
39 |
definition
|
69587
|
40 |
rtrancl :: "i=>i" (\<open>(_^*)\<close> [100] 100) (*refl/transitive closure*) where
|
46820
|
41 |
"r^* == lfp(field(r)*field(r), %s. id(field(r)) \<union> (r O s))"
|
13239
|
42 |
|
24893
|
43 |
definition
|
69587
|
44 |
trancl :: "i=>i" (\<open>(_^+)\<close> [100] 100) (*transitive closure*) where
|
13239
|
45 |
"r^+ == r O r^*"
|
|
46 |
|
24893
|
47 |
definition
|
|
48 |
equiv :: "[i,i]=>o" where
|
46820
|
49 |
"equiv(A,r) == r \<subseteq> A*A & refl(A,r) & sym(r) & trans(r)"
|
14653
|
50 |
|
|
51 |
|
60770
|
52 |
subsection\<open>General properties of relations\<close>
|
13239
|
53 |
|
60770
|
54 |
subsubsection\<open>irreflexivity\<close>
|
13239
|
55 |
|
|
56 |
lemma irreflI:
|
46953
|
57 |
"[| !!x. x \<in> A ==> <x,x> \<notin> r |] ==> irrefl(A,r)"
|
46820
|
58 |
by (simp add: irrefl_def)
|
13239
|
59 |
|
46953
|
60 |
lemma irreflE: "[| irrefl(A,r); x \<in> A |] ==> <x,x> \<notin> r"
|
13240
|
61 |
by (simp add: irrefl_def)
|
13239
|
62 |
|
60770
|
63 |
subsubsection\<open>symmetry\<close>
|
13239
|
64 |
|
|
65 |
lemma symI:
|
|
66 |
"[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
|
46820
|
67 |
by (unfold sym_def, blast)
|
13239
|
68 |
|
13534
|
69 |
lemma symE: "[| sym(r); <x,y>: r |] ==> <y,x>: r"
|
13240
|
70 |
by (unfold sym_def, blast)
|
13239
|
71 |
|
60770
|
72 |
subsubsection\<open>antisymmetry\<close>
|
13239
|
73 |
|
|
74 |
lemma antisymI:
|
|
75 |
"[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> antisym(r)"
|
46820
|
76 |
by (simp add: antisym_def, blast)
|
13239
|
77 |
|
|
78 |
lemma antisymE: "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y"
|
13240
|
79 |
by (simp add: antisym_def, blast)
|
13239
|
80 |
|
60770
|
81 |
subsubsection\<open>transitivity\<close>
|
13239
|
82 |
|
|
83 |
lemma transD: "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r"
|
13240
|
84 |
by (unfold trans_def, blast)
|
13239
|
85 |
|
46820
|
86 |
lemma trans_onD:
|
46953
|
87 |
"[| trans[A](r); <a,b>:r; <b,c>:r; a \<in> A; b \<in> A; c \<in> A |] ==> <a,c>:r"
|
13243
|
88 |
by (unfold trans_on_def, blast)
|
|
89 |
|
|
90 |
lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
|
|
91 |
by (unfold trans_def trans_on_def, blast)
|
13239
|
92 |
|
58860
|
93 |
lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)"
|
13248
|
94 |
by (simp add: trans_on_def trans_def, blast)
|
|
95 |
|
|
96 |
|
60770
|
97 |
subsection\<open>Transitive closure of a relation\<close>
|
13239
|
98 |
|
|
99 |
lemma rtrancl_bnd_mono:
|
46820
|
100 |
"bnd_mono(field(r)*field(r), %s. id(field(r)) \<union> (r O s))"
|
13248
|
101 |
by (rule bnd_monoI, blast+)
|
13239
|
102 |
|
46820
|
103 |
lemma rtrancl_mono: "r<=s ==> r^* \<subseteq> s^*"
|
13239
|
104 |
apply (unfold rtrancl_def)
|
|
105 |
apply (rule lfp_mono)
|
|
106 |
apply (rule rtrancl_bnd_mono)+
|
46820
|
107 |
apply blast
|
13239
|
108 |
done
|
|
109 |
|
46820
|
110 |
(* @{term"r^* = id(field(r)) \<union> ( r O r^* )"} *)
|
13239
|
111 |
lemmas rtrancl_unfold =
|
45602
|
112 |
rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]]
|
13239
|
113 |
|
|
114 |
(** The relation rtrancl **)
|
|
115 |
|
46820
|
116 |
(* @{term"r^* \<subseteq> field(r) * field(r)"} *)
|
45602
|
117 |
lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset]
|
13239
|
118 |
|
13248
|
119 |
lemma relation_rtrancl: "relation(r^*)"
|
46820
|
120 |
apply (simp add: relation_def)
|
|
121 |
apply (blast dest: rtrancl_type [THEN subsetD])
|
13248
|
122 |
done
|
|
123 |
|
13239
|
124 |
(*Reflexivity of rtrancl*)
|
46953
|
125 |
lemma rtrancl_refl: "[| a \<in> field(r) |] ==> <a,a> \<in> r^*"
|
13239
|
126 |
apply (rule rtrancl_unfold [THEN ssubst])
|
|
127 |
apply (erule idI [THEN UnI1])
|
|
128 |
done
|
|
129 |
|
|
130 |
(*Closure under composition with r *)
|
46820
|
131 |
lemma rtrancl_into_rtrancl: "[| <a,b> \<in> r^*; <b,c> \<in> r |] ==> <a,c> \<in> r^*"
|
13239
|
132 |
apply (rule rtrancl_unfold [THEN ssubst])
|
13269
|
133 |
apply (rule compI [THEN UnI2], assumption, assumption)
|
13239
|
134 |
done
|
|
135 |
|
|
136 |
(*rtrancl of r contains all pairs in r *)
|
46820
|
137 |
lemma r_into_rtrancl: "<a,b> \<in> r ==> <a,b> \<in> r^*"
|
13240
|
138 |
by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)
|
13239
|
139 |
|
|
140 |
(*The premise ensures that r consists entirely of pairs*)
|
46820
|
141 |
lemma r_subset_rtrancl: "relation(r) ==> r \<subseteq> r^*"
|
13248
|
142 |
by (simp add: relation_def, blast intro: r_into_rtrancl)
|
13239
|
143 |
|
|
144 |
lemma rtrancl_field: "field(r^*) = field(r)"
|
13240
|
145 |
by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
|
13239
|
146 |
|
|
147 |
|
|
148 |
(** standard induction rule **)
|
|
149 |
|
13534
|
150 |
lemma rtrancl_full_induct [case_names initial step, consumes 1]:
|
46820
|
151 |
"[| <a,b> \<in> r^*;
|
46953
|
152 |
!!x. x \<in> field(r) ==> P(<x,x>);
|
46820
|
153 |
!!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |]
|
13239
|
154 |
==> P(<a,b>)"
|
46820
|
155 |
by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast)
|
13239
|
156 |
|
|
157 |
(*nice induction rule.
|
46953
|
158 |
Tried adding the typing hypotheses y,z \<in> field(r), but these
|
13239
|
159 |
caused expensive case splits!*)
|
13534
|
160 |
lemma rtrancl_induct [case_names initial step, induct set: rtrancl]:
|
46820
|
161 |
"[| <a,b> \<in> r^*;
|
|
162 |
P(a);
|
|
163 |
!!y z.[| <a,y> \<in> r^*; <y,z> \<in> r; P(y) |] ==> P(z)
|
13239
|
164 |
|] ==> P(b)"
|
|
165 |
(*by induction on this formula*)
|
46820
|
166 |
apply (subgoal_tac "\<forall>y. <a,b> = <a,y> \<longrightarrow> P (y) ")
|
13239
|
167 |
(*now solve first subgoal: this formula is sufficient*)
|
|
168 |
apply (erule spec [THEN mp], rule refl)
|
|
169 |
(*now do the induction*)
|
13240
|
170 |
apply (erule rtrancl_full_induct, blast+)
|
13239
|
171 |
done
|
|
172 |
|
|
173 |
(*transitivity of transitive closure!! -- by induction.*)
|
|
174 |
lemma trans_rtrancl: "trans(r^*)"
|
|
175 |
apply (unfold trans_def)
|
|
176 |
apply (intro allI impI)
|
13784
|
177 |
apply (erule_tac b = z in rtrancl_induct, assumption)
|
46820
|
178 |
apply (blast intro: rtrancl_into_rtrancl)
|
13239
|
179 |
done
|
|
180 |
|
45602
|
181 |
lemmas rtrancl_trans = trans_rtrancl [THEN transD]
|
13239
|
182 |
|
|
183 |
(*elimination of rtrancl -- by induction on a special formula*)
|
|
184 |
lemma rtranclE:
|
46820
|
185 |
"[| <a,b> \<in> r^*; (a=b) ==> P;
|
|
186 |
!!y.[| <a,y> \<in> r^*; <y,b> \<in> r |] ==> P |]
|
13239
|
187 |
==> P"
|
46820
|
188 |
apply (subgoal_tac "a = b | (\<exists>y. <a,y> \<in> r^* & <y,b> \<in> r) ")
|
13239
|
189 |
(*see HOL/trancl*)
|
46820
|
190 |
apply blast
|
13240
|
191 |
apply (erule rtrancl_induct, blast+)
|
13239
|
192 |
done
|
|
193 |
|
|
194 |
|
|
195 |
(**** The relation trancl ****)
|
|
196 |
|
|
197 |
(*Transitivity of r^+ is proved by transitivity of r^* *)
|
|
198 |
lemma trans_trancl: "trans(r^+)"
|
|
199 |
apply (unfold trans_def trancl_def)
|
|
200 |
apply (blast intro: rtrancl_into_rtrancl
|
|
201 |
trans_rtrancl [THEN transD, THEN compI])
|
|
202 |
done
|
|
203 |
|
13243
|
204 |
lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
|
|
205 |
|
45602
|
206 |
lemmas trancl_trans = trans_trancl [THEN transD]
|
13239
|
207 |
|
|
208 |
(** Conversions between trancl and rtrancl **)
|
0
|
209 |
|
46820
|
210 |
lemma trancl_into_rtrancl: "<a,b> \<in> r^+ ==> <a,b> \<in> r^*"
|
13239
|
211 |
apply (unfold trancl_def)
|
|
212 |
apply (blast intro: rtrancl_into_rtrancl)
|
|
213 |
done
|
|
214 |
|
|
215 |
(*r^+ contains all pairs in r *)
|
46820
|
216 |
lemma r_into_trancl: "<a,b> \<in> r ==> <a,b> \<in> r^+"
|
13239
|
217 |
apply (unfold trancl_def)
|
|
218 |
apply (blast intro!: rtrancl_refl)
|
|
219 |
done
|
|
220 |
|
|
221 |
(*The premise ensures that r consists entirely of pairs*)
|
46820
|
222 |
lemma r_subset_trancl: "relation(r) ==> r \<subseteq> r^+"
|
13248
|
223 |
by (simp add: relation_def, blast intro: r_into_trancl)
|
|
224 |
|
13239
|
225 |
|
|
226 |
(*intro rule by definition: from r^* and r *)
|
46820
|
227 |
lemma rtrancl_into_trancl1: "[| <a,b> \<in> r^*; <b,c> \<in> r |] ==> <a,c> \<in> r^+"
|
13240
|
228 |
by (unfold trancl_def, blast)
|
13239
|
229 |
|
|
230 |
(*intro rule from r and r^* *)
|
|
231 |
lemma rtrancl_into_trancl2:
|
46820
|
232 |
"[| <a,b> \<in> r; <b,c> \<in> r^* |] ==> <a,c> \<in> r^+"
|
13239
|
233 |
apply (erule rtrancl_induct)
|
|
234 |
apply (erule r_into_trancl)
|
46820
|
235 |
apply (blast intro: r_into_trancl trancl_trans)
|
13239
|
236 |
done
|
|
237 |
|
|
238 |
(*Nice induction rule for trancl*)
|
13534
|
239 |
lemma trancl_induct [case_names initial step, induct set: trancl]:
|
46820
|
240 |
"[| <a,b> \<in> r^+;
|
|
241 |
!!y. [| <a,y> \<in> r |] ==> P(y);
|
|
242 |
!!y z.[| <a,y> \<in> r^+; <y,z> \<in> r; P(y) |] ==> P(z)
|
13239
|
243 |
|] ==> P(b)"
|
|
244 |
apply (rule compEpair)
|
|
245 |
apply (unfold trancl_def, assumption)
|
|
246 |
(*by induction on this formula*)
|
46820
|
247 |
apply (subgoal_tac "\<forall>z. <y,z> \<in> r \<longrightarrow> P (z) ")
|
13239
|
248 |
(*now solve first subgoal: this formula is sufficient*)
|
|
249 |
apply blast
|
|
250 |
apply (erule rtrancl_induct)
|
|
251 |
apply (blast intro: rtrancl_into_trancl1)+
|
|
252 |
done
|
|
253 |
|
|
254 |
(*elimination of r^+ -- NOT an induction rule*)
|
|
255 |
lemma tranclE:
|
46820
|
256 |
"[| <a,b> \<in> r^+;
|
|
257 |
<a,b> \<in> r ==> P;
|
|
258 |
!!y.[| <a,y> \<in> r^+; <y,b> \<in> r |] ==> P
|
13239
|
259 |
|] ==> P"
|
46820
|
260 |
apply (subgoal_tac "<a,b> \<in> r | (\<exists>y. <a,y> \<in> r^+ & <y,b> \<in> r) ")
|
|
261 |
apply blast
|
13239
|
262 |
apply (rule compEpair)
|
|
263 |
apply (unfold trancl_def, assumption)
|
|
264 |
apply (erule rtranclE)
|
|
265 |
apply (blast intro: rtrancl_into_trancl1)+
|
|
266 |
done
|
|
267 |
|
46820
|
268 |
lemma trancl_type: "r^+ \<subseteq> field(r)*field(r)"
|
13239
|
269 |
apply (unfold trancl_def)
|
|
270 |
apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
|
|
271 |
done
|
|
272 |
|
13248
|
273 |
lemma relation_trancl: "relation(r^+)"
|
46820
|
274 |
apply (simp add: relation_def)
|
|
275 |
apply (blast dest: trancl_type [THEN subsetD])
|
13248
|
276 |
done
|
|
277 |
|
13243
|
278 |
lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A"
|
|
279 |
by (insert trancl_type [of r], blast)
|
|
280 |
|
46820
|
281 |
lemma trancl_mono: "r<=s ==> r^+ \<subseteq> s^+"
|
13239
|
282 |
by (unfold trancl_def, intro comp_mono rtrancl_mono)
|
|
283 |
|
13248
|
284 |
lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r"
|
|
285 |
apply (rule equalityI)
|
46820
|
286 |
prefer 2 apply (erule r_subset_trancl, clarify)
|
|
287 |
apply (frule trancl_type [THEN subsetD], clarify)
|
13248
|
288 |
apply (erule trancl_induct, assumption)
|
46820
|
289 |
apply (blast dest: transD)
|
13248
|
290 |
done
|
|
291 |
|
13239
|
292 |
|
|
293 |
(** Suggested by Sidi Ould Ehmety **)
|
|
294 |
|
|
295 |
lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
|
13240
|
296 |
apply (rule equalityI, auto)
|
13239
|
297 |
prefer 2
|
|
298 |
apply (frule rtrancl_type [THEN subsetD])
|
46820
|
299 |
apply (blast intro: r_into_rtrancl )
|
60770
|
300 |
txt\<open>converse direction\<close>
|
46820
|
301 |
apply (frule rtrancl_type [THEN subsetD], clarify)
|
13239
|
302 |
apply (erule rtrancl_induct)
|
|
303 |
apply (simp add: rtrancl_refl rtrancl_field)
|
|
304 |
apply (blast intro: rtrancl_trans)
|
|
305 |
done
|
|
306 |
|
46820
|
307 |
lemma rtrancl_subset: "[| R \<subseteq> S; S \<subseteq> R^* |] ==> S^* = R^*"
|
13239
|
308 |
apply (drule rtrancl_mono)
|
13269
|
309 |
apply (drule rtrancl_mono, simp_all, blast)
|
13239
|
310 |
done
|
|
311 |
|
|
312 |
lemma rtrancl_Un_rtrancl:
|
46820
|
313 |
"[| relation(r); relation(s) |] ==> (r^* \<union> s^*)^* = (r \<union> s)^*"
|
13239
|
314 |
apply (rule rtrancl_subset)
|
|
315 |
apply (blast dest: r_subset_rtrancl)
|
|
316 |
apply (blast intro: rtrancl_mono [THEN subsetD])
|
|
317 |
done
|
|
318 |
|
|
319 |
(*** "converse" laws by Sidi Ould Ehmety ***)
|
|
320 |
|
|
321 |
(** rtrancl **)
|
|
322 |
|
|
323 |
lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"
|
|
324 |
apply (rule converseI)
|
|
325 |
apply (frule rtrancl_type [THEN subsetD])
|
|
326 |
apply (erule rtrancl_induct)
|
|
327 |
apply (blast intro: rtrancl_refl)
|
|
328 |
apply (blast intro: r_into_rtrancl rtrancl_trans)
|
|
329 |
done
|
|
330 |
|
|
331 |
lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"
|
|
332 |
apply (drule converseD)
|
|
333 |
apply (frule rtrancl_type [THEN subsetD])
|
|
334 |
apply (erule rtrancl_induct)
|
|
335 |
apply (blast intro: rtrancl_refl)
|
|
336 |
apply (blast intro: r_into_rtrancl rtrancl_trans)
|
|
337 |
done
|
|
338 |
|
|
339 |
lemma rtrancl_converse: "converse(r)^* = converse(r^*)"
|
|
340 |
apply (safe intro!: equalityI)
|
|
341 |
apply (frule rtrancl_type [THEN subsetD])
|
|
342 |
apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)
|
|
343 |
done
|
|
344 |
|
|
345 |
(** trancl **)
|
|
346 |
|
|
347 |
lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"
|
|
348 |
apply (erule trancl_induct)
|
|
349 |
apply (auto intro: r_into_trancl trancl_trans)
|
|
350 |
done
|
|
351 |
|
|
352 |
lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"
|
|
353 |
apply (drule converseD)
|
|
354 |
apply (erule trancl_induct)
|
|
355 |
apply (auto intro: r_into_trancl trancl_trans)
|
|
356 |
done
|
|
357 |
|
|
358 |
lemma trancl_converse: "converse(r)^+ = converse(r^+)"
|
|
359 |
apply (safe intro!: equalityI)
|
|
360 |
apply (frule trancl_type [THEN subsetD])
|
|
361 |
apply (safe dest!: trancl_converseD intro!: trancl_converseI)
|
|
362 |
done
|
|
363 |
|
13534
|
364 |
lemma converse_trancl_induct [case_names initial step, consumes 1]:
|
46820
|
365 |
"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);
|
|
366 |
!!y z. [| <y, z> \<in> r; <z, b> \<in> r^+; P(z) |] ==> P(y) |]
|
13239
|
367 |
==> P(a)"
|
|
368 |
apply (drule converseI)
|
|
369 |
apply (simp (no_asm_use) add: trancl_converse [symmetric])
|
|
370 |
apply (erule trancl_induct)
|
|
371 |
apply (auto simp add: trancl_converse)
|
|
372 |
done
|
|
373 |
|
0
|
374 |
end
|