1 (* Title: HOL/Transitive_Closure.thy |
1 (* Title: HOL/Transitive_Closure.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
|
6 Relfexive and Transitive closure of a relation |
|
7 |
|
8 rtrancl is reflexive/transitive closure; |
|
9 trancl is transitive closure |
|
10 reflcl is reflexive closure |
|
11 |
|
12 These postfix operators have MAXIMUM PRIORITY, forcing their operands |
|
13 to be atomic. |
|
14 *) |
5 *) |
15 |
6 |
16 theory Transitive_Closure = Inductive |
7 header {* Reflexive and Transitive closure of a relation *} |
17 files ("Transitive_Closure_lemmas.ML"): |
8 |
|
9 theory Transitive_Closure = Inductive: |
|
10 |
|
11 text {* |
|
12 @{text rtrancl} is reflexive/transitive closure, |
|
13 @{text trancl} is transitive closure, |
|
14 @{text reflcl} is reflexive closure. |
|
15 |
|
16 These postfix operators have \emph{maximum priority}, forcing their |
|
17 operands to be atomic. |
|
18 *} |
18 |
19 |
19 consts |
20 consts |
20 rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999) |
21 rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^*)" [1000] 999) |
21 |
22 |
22 inductive "r^*" |
23 inductive "r^*" |
23 intros |
24 intros |
24 rtrancl_refl [intro!, simp]: "(a, a) : r^*" |
25 rtrancl_refl [intro!, simp]: "(a, a) : r^*" |
25 rtrancl_into_rtrancl: "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*" |
26 rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" |
26 |
27 |
27 constdefs |
28 constdefs |
28 trancl :: "('a * 'a) set => ('a * 'a) set" ("(_^+)" [1000] 999) |
29 trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^+)" [1000] 999) |
29 "r^+ == r O rtrancl r" |
30 "r^+ == r O rtrancl r" |
30 |
31 |
31 syntax |
32 syntax |
32 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_^=)" [1000] 999) |
33 "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) |
33 translations |
34 translations |
34 "r^=" == "r Un Id" |
35 "r^=" == "r \<union> Id" |
35 |
36 |
36 syntax (xsymbols) |
37 syntax (xsymbols) |
37 rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) |
38 rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\\<^sup>*)" [1000] 999) |
38 trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) |
39 trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\\<^sup>+)" [1000] 999) |
39 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
40 "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\\<^sup>=)" [1000] 999) |
40 |
41 |
41 use "Transitive_Closure_lemmas.ML" |
42 |
42 |
43 subsection {* Reflexive-transitive closure *} |
|
44 |
|
45 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
|
46 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
|
47 apply (simp only: split_tupled_all) |
|
48 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
|
49 done |
|
50 |
|
51 lemma rtrancl_mono: "r \<subseteq> s ==> r^* \<subseteq> s^*" |
|
52 -- {* monotonicity of @{text rtrancl} *} |
|
53 apply (rule subsetI) |
|
54 apply (simp only: split_tupled_all) |
|
55 apply (erule rtrancl.induct) |
|
56 apply (rule_tac [2] rtrancl_into_rtrancl) |
|
57 apply blast+ |
|
58 done |
|
59 |
|
60 theorem rtrancl_induct [consumes 1]: |
|
61 (assumes a: "(a, b) : r^*" |
|
62 and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z") |
|
63 "P b" |
|
64 proof - |
|
65 from a have "a = a --> P b" |
|
66 by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct) |
|
67 (rules intro: cases)+ |
|
68 thus ?thesis by rules |
|
69 qed |
|
70 |
|
71 ML_setup {* |
|
72 bind_thm ("rtrancl_induct2", split_rule |
|
73 (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct"))); |
|
74 *} |
|
75 |
|
76 lemma trans_rtrancl: "trans(r^*)" |
|
77 -- {* transitivity of transitive closure!! -- by induction *} |
|
78 apply (unfold trans_def) |
|
79 apply safe |
|
80 apply (erule_tac b = z in rtrancl_induct) |
|
81 apply (blast intro: rtrancl_into_rtrancl)+ |
|
82 done |
|
83 |
|
84 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] |
|
85 |
|
86 lemma rtranclE: |
|
87 "[| (a::'a,b) : r^*; (a = b) ==> P; |
|
88 !!y.[| (a,y) : r^*; (y,b) : r |] ==> P |
|
89 |] ==> P" |
|
90 -- {* elimination of @{text rtrancl} -- by induction on a special formula *} |
|
91 proof - |
|
92 assume major: "(a::'a,b) : r^*" |
|
93 case rule_context |
|
94 show ?thesis |
|
95 apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)") |
|
96 apply (rule_tac [2] major [THEN rtrancl_induct]) |
|
97 prefer 2 apply (blast!) |
|
98 prefer 2 apply (blast!) |
|
99 apply (erule asm_rl exE disjE conjE prems)+ |
|
100 done |
|
101 qed |
|
102 |
|
103 lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard] |
|
104 |
|
105 text {* |
|
106 \medskip More @{term "r^*"} equations and inclusions. |
|
107 *} |
|
108 |
|
109 lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" |
|
110 apply auto |
|
111 apply (erule rtrancl_induct) |
|
112 apply (rule rtrancl_refl) |
|
113 apply (blast intro: rtrancl_trans) |
|
114 done |
|
115 |
|
116 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" |
|
117 apply (rule set_ext) |
|
118 apply (simp only: split_tupled_all) |
|
119 apply (blast intro: rtrancl_trans) |
|
120 done |
|
121 |
|
122 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
|
123 apply (drule rtrancl_mono) |
|
124 apply simp |
|
125 done |
|
126 |
|
127 lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*" |
|
128 apply (drule rtrancl_mono) |
|
129 apply (drule rtrancl_mono) |
|
130 apply simp |
|
131 apply blast |
|
132 done |
|
133 |
|
134 lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*" |
|
135 by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) |
|
136 |
|
137 lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*" |
|
138 by (blast intro!: rtrancl_subset intro: r_into_rtrancl) |
|
139 |
|
140 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" |
|
141 apply (rule sym) |
|
142 apply (rule rtrancl_subset) |
|
143 apply blast |
|
144 apply clarify |
|
145 apply (rename_tac a b) |
|
146 apply (case_tac "a = b") |
|
147 apply blast |
|
148 apply (blast intro!: r_into_rtrancl) |
|
149 done |
|
150 |
|
151 lemma rtrancl_converseD: "(x, y) \<in> (r^-1)^* ==> (y, x) \<in> r^*" |
|
152 apply (erule rtrancl_induct) |
|
153 apply (rule rtrancl_refl) |
|
154 apply (blast intro: rtrancl_trans) |
|
155 done |
|
156 |
|
157 lemma rtrancl_converseI: "(y, x) \<in> r^* ==> (x, y) \<in> (r^-1)^*" |
|
158 apply (erule rtrancl_induct) |
|
159 apply (rule rtrancl_refl) |
|
160 apply (blast intro: rtrancl_trans) |
|
161 done |
|
162 |
|
163 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" |
|
164 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
|
165 |
|
166 lemma converse_rtrancl_induct: |
|
167 "[| (a,b) : r^*; P(b); |
|
168 !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] |
|
169 ==> P(a)" |
|
170 proof - |
|
171 assume major: "(a,b) : r^*" |
|
172 case rule_context |
|
173 show ?thesis |
|
174 apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct]) |
|
175 apply assumption |
|
176 apply (blast! dest!: rtrancl_converseD) |
|
177 done |
|
178 qed |
|
179 |
|
180 ML_setup {* |
|
181 bind_thm ("converse_rtrancl_induct2", split_rule |
|
182 (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct"))); |
|
183 *} |
|
184 |
|
185 lemma converse_rtranclE: |
|
186 "[| (x,z):r^*; |
|
187 x=z ==> P; |
|
188 !!y. [| (x,y):r; (y,z):r^* |] ==> P |
|
189 |] ==> P" |
|
190 proof - |
|
191 assume major: "(x,z):r^*" |
|
192 case rule_context |
|
193 show ?thesis |
|
194 apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)") |
|
195 apply (rule_tac [2] major [THEN converse_rtrancl_induct]) |
|
196 prefer 2 apply (blast!) |
|
197 prefer 2 apply (blast!) |
|
198 apply (erule asm_rl exE disjE conjE prems)+ |
|
199 done |
|
200 qed |
|
201 |
|
202 ML_setup {* |
|
203 bind_thm ("converse_rtranclE2", split_rule |
|
204 (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE"))); |
|
205 *} |
|
206 |
|
207 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" |
|
208 by (blast elim: rtranclE converse_rtranclE |
|
209 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
|
210 |
|
211 |
|
212 subsection {* Transitive closure *} |
|
213 |
|
214 lemma trancl_mono: "p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" |
|
215 apply (unfold trancl_def) |
|
216 apply (blast intro: rtrancl_mono [THEN subsetD]) |
|
217 done |
|
218 |
|
219 text {* |
|
220 \medskip Conversions between @{text trancl} and @{text rtrancl}. |
|
221 *} |
|
222 |
|
223 lemma trancl_into_rtrancl: "!!p. p \<in> r^+ ==> p \<in> r^*" |
|
224 apply (unfold trancl_def) |
|
225 apply (simp only: split_tupled_all) |
|
226 apply (erule rel_compEpair) |
|
227 apply (assumption | rule rtrancl_into_rtrancl)+ |
|
228 done |
|
229 |
|
230 lemma r_into_trancl [intro]: "!!p. p \<in> r ==> p \<in> r^+" |
|
231 -- {* @{text "r^+"} contains @{text r} *} |
|
232 apply (unfold trancl_def) |
|
233 apply (simp only: split_tupled_all) |
|
234 apply (assumption | rule rel_compI rtrancl_refl)+ |
|
235 done |
|
236 |
|
237 lemma rtrancl_into_trancl1: "(a, b) \<in> r^* ==> (b, c) \<in> r ==> (a, c) \<in> r^+" |
|
238 -- {* intro rule by definition: from @{text rtrancl} and @{text r} *} |
|
239 by (auto simp add: trancl_def) |
|
240 |
|
241 lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+" |
|
242 -- {* intro rule from @{text r} and @{text rtrancl} *} |
|
243 apply (erule rtranclE) |
|
244 apply (blast intro: r_into_trancl) |
|
245 apply (rule rtrancl_trans [THEN rtrancl_into_trancl1]) |
|
246 apply (assumption | rule r_into_rtrancl)+ |
|
247 done |
|
248 |
|
249 lemma trancl_induct: |
|
250 "[| (a,b) : r^+; |
|
251 !!y. [| (a,y) : r |] ==> P(y); |
|
252 !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) |
|
253 |] ==> P(b)" |
|
254 -- {* Nice induction rule for @{text trancl} *} |
|
255 proof - |
|
256 assume major: "(a, b) : r^+" |
|
257 case rule_context |
|
258 show ?thesis |
|
259 apply (rule major [unfolded trancl_def, THEN rel_compEpair]) |
|
260 txt {* by induction on this formula *} |
|
261 apply (subgoal_tac "ALL z. (y,z) : r --> P (z)") |
|
262 txt {* now solve first subgoal: this formula is sufficient *} |
|
263 apply blast |
|
264 apply (erule rtrancl_induct) |
|
265 apply (blast intro: rtrancl_into_trancl1 prems)+ |
|
266 done |
|
267 qed |
|
268 |
|
269 lemma trancl_trans_induct: |
|
270 "[| (x,y) : r^+; |
|
271 !!x y. (x,y) : r ==> P x y; |
|
272 !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z |
|
273 |] ==> P x y" |
|
274 -- {* Another induction rule for trancl, incorporating transitivity *} |
|
275 proof - |
|
276 assume major: "(x,y) : r^+" |
|
277 case rule_context |
|
278 show ?thesis |
|
279 by (blast intro: r_into_trancl major [THEN trancl_induct] prems) |
|
280 qed |
|
281 |
|
282 lemma tranclE: |
|
283 "[| (a::'a,b) : r^+; |
|
284 (a,b) : r ==> P; |
|
285 !!y.[| (a,y) : r^+; (y,b) : r |] ==> P |
|
286 |] ==> P" |
|
287 -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *} |
|
288 proof - |
|
289 assume major: "(a::'a,b) : r^+" |
|
290 case rule_context |
|
291 show ?thesis |
|
292 apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)") |
|
293 apply (erule asm_rl disjE exE conjE prems)+ |
|
294 apply (rule major [unfolded trancl_def, THEN rel_compEpair]) |
|
295 apply (erule rtranclE) |
|
296 apply blast |
|
297 apply (blast intro!: rtrancl_into_trancl1) |
|
298 done |
|
299 qed |
|
300 |
|
301 lemma trans_trancl: "trans(r^+)" |
|
302 -- {* Transitivity of @{term "r^+"} *} |
|
303 -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *} |
|
304 apply (unfold trancl_def) |
|
305 apply (rule transI) |
|
306 apply (erule rel_compEpair)+ |
|
307 apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]]) |
|
308 apply assumption+ |
|
309 done |
|
310 |
|
311 lemmas trancl_trans = trans_trancl [THEN transD, standard] |
|
312 |
|
313 lemma rtrancl_trancl_trancl: "(x, y) \<in> r^* ==> (y, z) \<in> r^+ ==> (x, z) \<in> r^+" |
|
314 apply (unfold trancl_def) |
|
315 apply (blast intro: rtrancl_trans) |
|
316 done |
|
317 |
|
318 lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+" |
|
319 by (erule transD [OF trans_trancl r_into_trancl]) |
|
320 |
|
321 lemma trancl_insert: |
|
322 "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" |
|
323 -- {* primitive recursion for @{text trancl} over finite relations *} |
|
324 apply (rule equalityI) |
|
325 apply (rule subsetI) |
|
326 apply (simp only: split_tupled_all) |
|
327 apply (erule trancl_induct) |
|
328 apply blast |
|
329 apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) |
|
330 apply (rule subsetI) |
|
331 apply (blast intro: trancl_mono rtrancl_mono |
|
332 [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
|
333 done |
|
334 |
|
335 lemma trancl_converse: "(r^-1)^+ = (r^+)^-1" |
|
336 apply (unfold trancl_def) |
|
337 apply (simp add: rtrancl_converse converse_rel_comp) |
|
338 apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq) |
|
339 done |
|
340 |
|
341 lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x,y) \<in> (r^-1)^+" |
|
342 by (simp add: trancl_converse) |
|
343 |
|
344 lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1" |
|
345 by (simp add: trancl_converse) |
|
346 |
|
347 lemma converse_trancl_induct: |
|
348 "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); |
|
349 !!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y) |] |
|
350 ==> P(a)" |
|
351 proof - |
|
352 assume major: "(a,b) : r^+" |
|
353 case rule_context |
|
354 show ?thesis |
|
355 apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]]) |
|
356 apply (rule prems) |
|
357 apply (erule converseD) |
|
358 apply (blast intro: prems dest!: trancl_converseD) |
|
359 done |
|
360 qed |
|
361 |
|
362 lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*" |
|
363 apply (erule converse_trancl_induct) |
|
364 apply auto |
|
365 apply (blast intro: rtrancl_trans) |
|
366 done |
|
367 |
|
368 lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+" |
|
369 apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y") |
|
370 apply fast |
|
371 apply (intro strip) |
|
372 apply (erule trancl_induct) |
|
373 apply (auto intro: r_into_trancl) |
|
374 done |
|
375 |
|
376 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y" |
|
377 by (blast dest: r_into_trancl) |
|
378 |
|
379 lemma trancl_subset_Sigma_aux: |
|
380 "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A" |
|
381 apply (erule rtrancl_induct) |
|
382 apply auto |
|
383 done |
|
384 |
|
385 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A" |
|
386 apply (unfold trancl_def) |
|
387 apply (blast dest!: trancl_subset_Sigma_aux) |
|
388 done |
43 |
389 |
44 lemma reflcl_trancl [simp]: "(r^+)^= = r^*" |
390 lemma reflcl_trancl [simp]: "(r^+)^= = r^*" |
45 apply safe |
391 apply safe |
46 apply (erule trancl_into_rtrancl) |
392 apply (erule trancl_into_rtrancl) |
47 apply (blast elim: rtranclE dest: rtrancl_into_trancl1) |
393 apply (blast elim: rtranclE dest: rtrancl_into_trancl1) |
48 done |
394 done |
49 |
395 |
50 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" |
396 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" |
51 apply safe |
397 apply safe |
89 |
435 |
90 lemma trancl_range [simp]: "Range (r^+) = Range r" |
436 lemma trancl_range [simp]: "Range (r^+) = Range r" |
91 by (simp add: Range_def trancl_converse [symmetric]) |
437 by (simp add: Range_def trancl_converse [symmetric]) |
92 |
438 |
93 lemma Not_Domain_rtrancl: |
439 lemma Not_Domain_rtrancl: |
94 "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" |
440 "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" |
95 apply (auto) |
441 apply auto |
96 by (erule rev_mp, erule rtrancl_induct, auto) |
442 by (erule rev_mp, erule rtrancl_induct, auto) |
97 |
443 |
98 (* more about converse rtrancl and trancl, should be merged with main body *) |
444 |
99 |
445 text {* More about converse @{text rtrancl} and @{text trancl}, should |
100 lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+" |
446 be merged with main body. *} |
|
447 |
|
448 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+" |
101 by (fast intro: trancl_trans) |
449 by (fast intro: trancl_trans) |
102 |
450 |
103 lemma trancl_into_trancl [rule_format]: |
451 lemma trancl_into_trancl [rule_format]: |
104 "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+" |
452 "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+" |
105 apply (erule trancl_induct) |
453 apply (erule trancl_induct) |
106 apply (fast intro: r_r_into_trancl) |
454 apply (fast intro: r_r_into_trancl) |
107 apply (fast intro: r_r_into_trancl trancl_trans) |
455 apply (fast intro: r_r_into_trancl trancl_trans) |
108 done |
456 done |
109 |
457 |
110 lemma trancl_rtrancl_trancl: |
458 lemma trancl_rtrancl_trancl: |
111 "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+" |
459 "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r\<^sup>* ==> (a, c) \<in> r\<^sup>+" |
112 apply (drule tranclD) |
460 apply (drule tranclD) |
113 apply (erule exE, erule conjE) |
461 apply (erule exE, erule conjE) |
114 apply (drule rtrancl_trans, assumption) |
462 apply (drule rtrancl_trans, assumption) |
115 apply (drule rtrancl_into_trancl2, assumption) |
463 apply (drule rtrancl_into_trancl2, assumption) |
116 apply assumption |
464 apply assumption |
117 done |
465 done |
118 |
466 |
119 lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans |
467 lemmas transitive_closure_trans [trans] = |
120 trancl_into_trancl trancl_into_trancl2 |
468 r_r_into_trancl trancl_trans rtrancl_trans |
121 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
469 trancl_into_trancl trancl_into_trancl2 |
122 rtrancl_trancl_trancl trancl_rtrancl_trancl |
470 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
|
471 rtrancl_trancl_trancl trancl_rtrancl_trancl |
123 |
472 |
124 declare trancl_into_rtrancl [elim] |
473 declare trancl_into_rtrancl [elim] |
125 |
474 |
126 declare rtrancl_induct [induct set: rtrancl] |
475 declare rtrancl_induct [induct set: rtrancl] |
127 declare rtranclE [cases set: rtrancl] |
476 declare rtranclE [cases set: rtrancl] |