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