1 (* ========================================================================= *)
2 (* All you wanted to know about reflexive symmetric and transitive closures. *)
3 (* ========================================================================= *)
8 MATCH_MP_TAC o DISCH_ALL o SPEC_ALL o UNDISCH o SPEC_ALL;;
10 (* ------------------------------------------------------------------------- *)
11 (* Little lemmas about equivalent forms of symmetry and transitivity. *)
12 (* ------------------------------------------------------------------------- *)
15 (`!R:A->A->bool. (!x y. R x y ==> R y x) <=> (!x y. R x y <=> R y x)`,
16 GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
17 [EQ_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC;
18 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [th])] THEN
19 FIRST_ASSUM MATCH_ACCEPT_TAC);;
22 (`!(R:A->A->bool) (S:A->A->bool) U.
23 (!x z. (?y. R x y /\ S y z) ==> U x z) <=>
24 (!x y z. R x y /\ S y z ==> U x z)`,
25 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
26 EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
28 (* ------------------------------------------------------------------------- *)
29 (* Reflexive closure *)
30 (* ------------------------------------------------------------------------- *)
32 let RC_RULES,RC_INDUCT,RC_CASES = new_inductive_definition
33 `(!x y. R x y ==> RC R x y) /\
37 (`!(R:A->A->bool) x y. R x y ==> RC R x y`,
38 REWRITE_TAC[RC_RULES]);;
41 (`!(R:A->A->bool) x. RC R x x`,
42 REWRITE_TAC[RC_RULES]);;
44 let RC_EXPLICIT = prove
45 (`!(R:A->A->bool) x y. RC R x y <=> R x y \/ (x = y)`,
46 REWRITE_TAC[RC_CASES; EQ_SYM_EQ]);;
50 (!x y. R x y ==> S x y) ==>
51 (!x y. RC R x y ==> RC S x y)`,
52 MESON_TAC[RC_CASES]);;
55 (`!R:A->A->bool. (RC R = R) <=> !x. R x x`,
56 REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT] THEN MESON_TAC[]);;
59 (`!R:A->A->bool. RC(RC R) = RC R`,
60 REWRITE_TAC[RC_CLOSED; RC_REFL]);;
64 (!x y. R x y ==> R y x) ==> (!x y. RC R x y ==> RC R y x)`,
65 MESON_TAC[RC_CASES]);;
69 (!x y z. R x y /\ R y z ==> R x z) ==>
70 (!x y z. RC R x y /\ RC R y z ==> RC R x z)`,
71 REWRITE_TAC[RC_CASES] THEN MESON_TAC[]);;
73 (* ------------------------------------------------------------------------- *)
74 (* Symmetric closure *)
75 (* ------------------------------------------------------------------------- *)
77 let SC_RULES,SC_INDUCT,SC_CASES = new_inductive_definition
78 `(!x y. R x y ==> SC R x y) /\
79 (!x:A y. SC R x y ==> SC R y x)`;;
82 (`!(R:A->A->bool) x y. R x y ==> SC R x y`,
83 REWRITE_TAC[SC_RULES]);;
86 (`!(R:A->A->bool) x y. SC R x y ==> SC R y x`,
87 REWRITE_TAC[SC_RULES]);;
89 let SC_EXPLICIT = prove
90 (`!R:A->A->bool. SC(R) x y <=> R x y \/ R y x`,
91 GEN_TAC THEN EQ_TAC THENL
92 [RULE_INDUCT_TAC SC_INDUCT THEN MESON_TAC[]; MESON_TAC[SC_CASES]]);;
96 (!x y. R x y ==> S x y) ==>
97 (!x y. SC R x y ==> SC S x y)`,
98 MESON_TAC[SC_EXPLICIT]);;
100 let SC_CLOSED = prove
101 (`!R:A->A->bool. (SC R = R) <=> !x y. R x y ==> R y x`,
102 REWRITE_TAC[FUN_EQ_THM; SC_EXPLICIT] THEN MESON_TAC[]);;
105 (`!R:A->A->bool. SC(SC R) = SC R`,
106 REWRITE_TAC[SC_CLOSED; SC_SYM]);;
109 (`!R:A->A->bool. (!x. R x x) ==> (!x. SC R x x)`,
110 MESON_TAC[SC_EXPLICIT]);;
112 (* ------------------------------------------------------------------------- *)
113 (* Transitive closure *)
114 (* ------------------------------------------------------------------------- *)
116 let TC_RULES,TC_INDUCT,TC_CASES = new_inductive_definition
117 `(!x y. R x y ==> TC R x y) /\
118 (!(x:A) y z. TC R x y /\ TC R y z ==> TC R x z)`;;
121 (`!(R:A->A->bool) x y. R x y ==> TC R x y`,
122 REWRITE_TAC[TC_RULES]);;
125 (`!(R:A->A->bool) x y z. TC R x y /\ TC R y z ==> TC R x z`,
126 REWRITE_TAC[TC_RULES]);;
130 (!x y. R x y ==> S x y) ==>
131 (!x y. TC R x y ==> TC S x y)`,
132 REPEAT GEN_TAC THEN STRIP_TAC THEN
133 MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC[TC_RULES]);;
135 let TC_CLOSED = prove
136 (`!R:A->A->bool. (TC R = R) <=> !x y z. R x y /\ R y z ==> R x z`,
137 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL
138 [MESON_TAC[TC_RULES]; REPEAT STRIP_TAC] THEN
139 EQ_TAC THENL [RULE_INDUCT_TAC TC_INDUCT; ALL_TAC] THEN
140 ASM_MESON_TAC[TC_RULES]);;
143 (`!R:A->A->bool. TC(TC R) = TC R`,
144 REWRITE_TAC[TC_CLOSED; TC_TRANS]);;
147 (`!R:A->A->bool. (!x. R x x) ==> (!x. TC R x x)`,
151 (`!R:A->A->bool. (!x y. R x y ==> R y x) ==> (!x y. TC R x y ==> TC R y x)`,
152 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC TC_INDUCT THEN
153 ASM_MESON_TAC[TC_RULES]);;
155 (* ------------------------------------------------------------------------- *)
156 (* Commutativity properties of the three basic closure operations *)
157 (* ------------------------------------------------------------------------- *)
160 (`!R:A->A->bool. RC(SC R) = SC(RC R)`,
161 REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT; SC_EXPLICIT] THEN MESON_TAC[]);;
164 (`!R:A->A->bool. SC(RC R) = RC(SC R)`,
165 REWRITE_TAC[RC_SC]);;
168 (`!R:A->A->bool. RC(TC R) = TC(RC R)`,
169 REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN EQ_TAC THENL
170 [RULE_INDUCT_TAC RC_INDUCT THEN MESON_TAC[TC_RULES; RC_RULES; TC_MONO];
171 RULE_INDUCT_TAC TC_INDUCT THEN MESON_TAC[RC_TRANS; TC_RULES; RC_MONO]]);;
174 (`!R:A->A->bool. TC(RC R) = RC(TC R)`,
175 REWRITE_TAC[RC_TC]);;
178 (`!(R:A->A->bool) x y. SC(TC R) x y ==> TC(SC R) x y`,
179 GEN_TAC THEN MATCH_MP_TAC SC_INDUCT THEN
180 MESON_TAC[TC_MONO; TC_SYM; SC_RULES]);;
183 (`!(R:A->A->bool) x y. SC(TC R) x y ==> TC(SC R) x y`,
184 REWRITE_TAC[TC_SC]);;
186 (* ------------------------------------------------------------------------- *)
187 (* Left and right variants of TC. *)
188 (* ------------------------------------------------------------------------- *)
190 let TC_TRANS_L = prove
191 (`!(R:A->A->bool) x y z. TC R x y /\ R y z ==> TC R x z`,
192 MESON_TAC[TC_RULES]);;
194 let TC_TRANS_R = prove
195 (`!(R:A->A->bool) x y z. R x y /\ TC R y z ==> TC R x z`,
196 MESON_TAC[TC_RULES]);;
198 let TC_CASES_L = prove
199 (`!(R:A->A->bool) x z. TC R x z <=> R x z \/ (?y. TC R x y /\ R y z)`,
200 REPEAT GEN_TAC THEN EQ_TAC THENL
201 [RULE_INDUCT_TAC TC_INDUCT THEN MESON_TAC[TC_RULES]; MESON_TAC[TC_RULES]]);;
203 let TC_CASES_R = prove
204 (`!(R:A->A->bool) x z. TC R x z <=> R x z \/ (?y. R x y /\ TC R y z)`,
205 REPEAT GEN_TAC THEN EQ_TAC THENL
206 [RULE_INDUCT_TAC TC_INDUCT THEN MESON_TAC[TC_RULES]; MESON_TAC[TC_RULES]]);;
208 let TC_INDUCT_L = prove
210 (!x y. R x y ==> P x y) /\
211 (!x y z. P x y /\ R y z ==> P x z) ==>
212 (!x y. TC R x y ==> P x y)`,
213 REPEAT GEN_TAC THEN STRIP_TAC THEN
214 SUBGOAL_THEN `!y:A z. TC(R) y z ==> !x:A. P x y ==> P x z` MP_TAC THENL
215 [MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC[]; ASM_MESON_TAC[TC_CASES_R]]);;
217 let TC_INDUCT_R = prove
219 (!x y. R x y ==> P x y) /\
220 (!x z. (?y. R x y /\ P y z) ==> P x z) ==>
221 (!x y. TC R x y ==> P x y)`,
222 REPEAT GEN_TAC THEN STRIP_TAC THEN
223 SUBGOAL_THEN `!x:A y. TC(R) x y ==> !z:A. P y z ==> P x z` MP_TAC THENL
224 [MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC[]; ASM_MESON_TAC[TC_CASES_L]]);;
226 (* ------------------------------------------------------------------------- *)
227 (* Reflexive symmetric closure *)
228 (* ------------------------------------------------------------------------- *)
230 let RSC = new_definition
231 `RSC(R:A->A->bool) = RC(SC R)`;;
234 (`!(R:A->A->bool) x y. R x y ==> RSC R x y`,
235 REWRITE_TAC[RSC] THEN MESON_TAC[RC_INC; SC_INC]);;
238 (`!(R:A->A->bool) x. RSC R x x`,
239 REWRITE_TAC[RSC; RC_REFL]);;
242 (`!(R:A->A->bool) x y. RSC R x y ==> RSC R y x`,
243 REWRITE_TAC[RSC; RC_SC; SC_SYM]);;
245 let RSC_CASES = prove
246 (`!(R:A->A->bool) x y. RSC R x y <=> (x = y) \/ R x y \/ R y x`,
247 REWRITE_TAC[RSC; RC_EXPLICIT; SC_EXPLICIT; DISJ_ACI]);;
249 let RSC_INDUCT = prove
251 (!x y. R x y ==> P x y) /\
253 (!x y. P x y ==> P y x)
254 ==> !x y. RSC R x y ==> P x y`,
255 REWRITE_TAC[RSC; RC_EXPLICIT; SC_EXPLICIT] THEN MESON_TAC[]);;
259 (!x y. R x y ==> S x y) ==>
260 (!x y. RSC R x y ==> RSC S x y)`,
261 REWRITE_TAC[RSC] THEN MESON_TAC[SC_MONO; RC_MONO]);;
263 let RSC_CLOSED = prove
264 (`!R:A->A->bool. (RSC R = R) <=> (!x. R x x) /\ (!x y. R x y ==> R y x)`,
265 REWRITE_TAC[FUN_EQ_THM; RSC; RC_EXPLICIT; SC_EXPLICIT] THEN MESON_TAC[]);;
267 let RSC_IDEMP = prove
268 (`!R:A->A->bool. RSC(RSC R) = RSC R`,
269 REWRITE_TAC[RSC_CLOSED; RSC_REFL; RSC_SYM]);;
271 (* ------------------------------------------------------------------------- *)
272 (* Reflexive transitive closure *)
273 (* ------------------------------------------------------------------------- *)
275 let RTC = new_definition
276 `RTC(R:A->A->bool) = RC(TC R)`;;
279 (`!(R:A->A->bool) x y. R x y ==> RTC R x y`,
280 REWRITE_TAC[RTC] THEN MESON_TAC[RC_INC; TC_INC]);;
283 (`!(R:A->A->bool) x. RTC R x x`,
284 REWRITE_TAC[RTC; RC_REFL]);;
286 let RTC_TRANS = prove
287 (`!(R:A->A->bool) x y z. RTC R x y /\ RTC R y z ==> RTC R x z`,
288 REWRITE_TAC[RTC; RC_TC; TC_TRANS]);;
290 let RTC_RULES = prove
292 (!x y. R x y ==> RTC R x y) /\
294 (!x y z. RTC R x y /\ RTC R y z ==> RTC R x z)`,
295 REWRITE_TAC[RTC_INC; RTC_REFL; RTC_TRANS]);;
297 let RTC_TRANS_L = prove
298 (`!(R:A->A->bool) x y z. RTC R x y /\ R y z ==> RTC R x z`,
299 REWRITE_TAC[RTC; RC_TC] THEN MESON_TAC[TC_TRANS_L; RC_INC]);;
301 let RTC_TRANS_R = prove
302 (`!(R:A->A->bool) x y z. R x y /\ RTC R y z ==> RTC R x z`,
303 REWRITE_TAC[RTC; RC_TC] THEN MESON_TAC[TC_TRANS_R; RC_INC]);;
305 let RTC_CASES = prove
306 (`!(R:A->A->bool) x z. RTC R x z <=> (x = z) \/ ?y. RTC R x y /\ RTC R y z`,
307 REWRITE_TAC[RTC; RC_EXPLICIT] THEN MESON_TAC[TC_TRANS]);;
309 let RTC_CASES_L = prove
310 (`!(R:A->A->bool) x z. RTC R x z <=> (x = z) \/ ?y. RTC R x y /\ R y z`,
311 REWRITE_TAC[RTC; RC_EXPLICIT] THEN MESON_TAC[TC_CASES_L; TC_TRANS_L]);;
313 let RTC_CASES_R = prove
314 (`!(R:A->A->bool) x z. RTC R x z <=> (x = z) \/ ?y. R x y /\ RTC R y z`,
315 REWRITE_TAC[RTC; RC_EXPLICIT] THEN MESON_TAC[TC_CASES_R; TC_TRANS_R]);;
317 let RTC_INDUCT = prove
319 (!x y. R x y ==> P x y) /\
321 (!x y z. P x y /\ P y z ==> P x z)
322 ==> !x y. RTC R x y ==> P x y`,
323 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RTC; RC_TC] THEN
324 MATCH_MP_TAC TC_INDUCT THEN REWRITE_TAC[RC_EXPLICIT] THEN ASM_MESON_TAC[]);;
326 let RTC_INDUCT_L = prove
329 (!x y z. P x y /\ R y z ==> P x z)
330 ==> !x y. RTC R x y ==> P x y`,
331 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RTC; RC_TC] THEN
332 MATCH_MP_TAC TC_INDUCT_L THEN REWRITE_TAC[RC_EXPLICIT] THEN
335 let RTC_INDUCT_R = prove
338 (!x y z. R x y /\ P y z ==> P x z)
339 ==> !x y. RTC R x y ==> P x y`,
340 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[RTC; RC_TC] THEN
341 MATCH_MP_TAC TC_INDUCT_R THEN REWRITE_TAC[RC_EXPLICIT] THEN
346 (!x y. R x y ==> S x y) ==>
347 (!x y. RTC R x y ==> RTC S x y)`,
348 REWRITE_TAC[RTC] THEN MESON_TAC[RC_MONO; TC_MONO]);;
350 let RTC_CLOSED = prove
351 (`!R:A->A->bool. (RTC R = R) <=> (!x. R x x) /\
352 (!x y z. R x y /\ R y z ==> R x z)`,
353 REWRITE_TAC[FUN_EQ_THM; RTC; RC_EXPLICIT] THEN
354 MESON_TAC[TC_CLOSED; TC_RULES]);;
356 let RTC_IDEMP = prove
357 (`!R:A->A->bool. RTC(RTC R) = RTC R`,
358 REWRITE_TAC[RTC_CLOSED; RTC_REFL; RTC_TRANS]);;
361 (`!R:A->A->bool. (!x y. R x y ==> R y x) ==> (!x y. RTC R x y ==> RTC R y x)`,
362 REWRITE_TAC[RTC] THEN MESON_TAC[RC_SYM; TC_SYM]);;
364 let RTC_STUTTER = prove
365 (`RTC R = RTC (\x y. R x y /\ ~(x = y))`,
366 REWRITE_TAC[RC_TC; RTC] THEN
367 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
368 REWRITE_TAC[RC_CASES] THEN MESON_TAC[]);;
370 let TC_RTC_CASES_L = prove
371 (`TC R x z <=> ?y. RTC R x y /\ R y z`,
372 REWRITE_TAC[RTC; RC_CASES] THEN MESON_TAC[TC_CASES_L; TC_INC]);;
374 let TC_RTC_CASES_R = prove
375 (`!R x z. TC R x z <=> ?y. R x y /\ RTC R y z`,
376 REWRITE_TAC[RTC; RC_CASES] THEN MESON_TAC[TC_CASES_R; TC_INC]);;
378 let TC_TC_RTC_CASES = prove
379 (`!R x z. TC R x z <=> ?y. TC R x y /\ RTC R y z`,
380 REWRITE_TAC[RTC; RC_CASES] THEN MESON_TAC[TC_TRANS]);;
382 let TC_RTC_TC_CASES = prove
383 (`!R x z. TC R x z <=> ?y. RTC R x y /\ TC R y z`,
384 REWRITE_TAC[RTC; RC_CASES] THEN MESON_TAC[TC_TRANS]);;
386 let RTC_NE_IMP_TC = prove
387 (`!R x y. RTC R x y /\ ~(x = y) ==> TC R x y`,
388 GEN_TAC THEN ONCE_REWRITE_TAC[GSYM IMP_IMP] THEN
389 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[] THEN
390 MESON_TAC[TC_INC; TC_CASES]);;
392 (* ------------------------------------------------------------------------- *)
393 (* Symmetric transitive closure *)
394 (* ------------------------------------------------------------------------- *)
396 let STC = new_definition
397 `STC(R:A->A->bool) = TC(SC R)`;;
400 (`!(R:A->A->bool) x y. R x y ==> STC R x y`,
401 REWRITE_TAC[STC] THEN MESON_TAC[SC_INC; TC_INC]);;
404 (`!(R:A->A->bool) x y. STC R x y ==> STC R y x`,
405 REWRITE_TAC[STC] THEN MESON_TAC[TC_SYM; SC_SYM]);;
407 let STC_TRANS = prove
408 (`!(R:A->A->bool) x y z. STC R x y /\ STC R y z ==> STC R x z`,
409 REWRITE_TAC[STC; TC_TRANS]);;
411 let STC_TRANS_L = prove
412 (`!(R:A->A->bool) x y z. STC R x y /\ R y z ==> STC R x z`,
413 REWRITE_TAC[STC] THEN MESON_TAC[TC_TRANS_L; SC_INC]);;
415 let STC_TRANS_R = prove
416 (`!(R:A->A->bool) x y z. R x y /\ STC R y z ==> STC R x z`,
417 REWRITE_TAC[STC] THEN MESON_TAC[TC_TRANS_R; SC_INC]);;
419 let STC_CASES = prove
420 (`!(R:A->A->bool) x z. STC R x z <=> R x z \/ STC R z x \/
421 ?y. STC R x y /\ STC R y z`,
422 REWRITE_TAC[STC] THEN MESON_TAC[SC_SYM; TC_SYM; TC_INC; TC_TRANS; SC_INC]);;
424 let STC_CASES_L = prove
425 (`!(R:A->A->bool) x z. STC R x z <=> R x z \/ STC R z x \/
426 ?y. STC R x y /\ R y z`,
427 REWRITE_TAC[STC] THEN MESON_TAC[SC_SYM; TC_SYM; TC_INC; TC_TRANS; SC_INC]);;
429 let STC_CASES_R = prove
430 (`!(R:A->A->bool) x z. STC R x z <=> R x z \/ STC R z x \/
431 ?y. R x y /\ STC R y z`,
432 REWRITE_TAC[STC] THEN MESON_TAC[SC_SYM; TC_SYM; TC_INC; TC_TRANS; SC_INC]);;
434 let STC_INDUCT = prove
436 (!x y. R x y ==> P x y) /\
437 (!x y. P x y ==> P y x) /\
438 (!x y z. P x y /\ P y z ==> P x z) ==>
439 !x y. STC R x y ==> P x y`,
440 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[STC] THEN
441 MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC[SC_EXPLICIT]);;
445 (!x y. R x y ==> S x y) ==>
446 (!x y. STC R x y ==> STC S x y)`,
447 REWRITE_TAC[STC] THEN MESON_TAC[SC_MONO; TC_MONO]);;
449 let STC_CLOSED = prove
450 (`!R:A->A->bool. (STC R = R) <=> (!x y. R x y ==> R y x) /\
451 (!x y z. R x y /\ R y z ==> R x z)`,
452 GEN_TAC THEN REWRITE_TAC[STC; SC_EXPLICIT] THEN EQ_TAC THENL
453 [DISCH_THEN(SUBST1_TAC o SYM) THEN MESON_TAC[TC_TRANS; TC_SYM; SC_SYM];
454 REWRITE_TAC[GSYM SC_CLOSED; GSYM TC_CLOSED] THEN MESON_TAC[]]);;
456 let STC_IDEMP = prove
457 (`!R:A->A->bool. STC(STC R) = STC R`,
458 REWRITE_TAC[STC_CLOSED; STC_SYM; STC_TRANS]);;
461 (`!R:A->A->bool. (!x. R x x) ==> !x. STC R x x`,
462 MESON_TAC[STC_INC]);;
464 (* ------------------------------------------------------------------------- *)
465 (* Reflexive symmetric transitive closure (smallest equivalence relation) *)
466 (* ------------------------------------------------------------------------- *)
468 let RSTC = new_definition
469 `RSTC(R:A->A->bool) = RC(TC(SC R))`;;
472 (`!(R:A->A->bool) x y. R x y ==> RSTC R x y`,
473 REWRITE_TAC[RSTC] THEN MESON_TAC[RC_INC; TC_INC; SC_INC]);;
475 let RSTC_REFL = prove
476 (`!(R:A->A->bool) x. RSTC R x x`,
477 REWRITE_TAC[RSTC; RC_REFL]);;
480 (`!(R:A->A->bool) x y. RSTC R x y ==> RSTC R y x`,
481 REWRITE_TAC[RSTC] THEN MESON_TAC[SC_SYM; TC_SYM; RC_SYM]);;
483 let RSTC_TRANS = prove
484 (`!(R:A->A->bool) x y z. RSTC R x y /\ RSTC R y z ==> RSTC R x z`,
485 REWRITE_TAC[RSTC; RC_TC; TC_TRANS]);;
487 let RSTC_RULES = prove
489 (!x y. R x y ==> RSTC R x y) /\
491 (!x y. RSTC R x y ==> RSTC R y x) /\
492 (!x y z. RSTC R x y /\ RSTC R y z ==> RSTC R x z)`,
493 REWRITE_TAC[RSTC_INC; RSTC_REFL; RSTC_SYM; RSTC_TRANS]);;
495 let RSTC_TRANS_L = prove
496 (`!(R:A->A->bool) x y z. RSTC R x y /\ R y z ==> RSTC R x z`,
497 REWRITE_TAC[RSTC; RC_TC] THEN MESON_TAC[TC_TRANS_L; RC_INC; SC_INC]);;
499 let RSTC_TRANS_R = prove
500 (`!(R:A->A->bool) x y z. R x y /\ RSTC R y z ==> RSTC R x z`,
501 REWRITE_TAC[RSTC; RC_TC] THEN MESON_TAC[TC_TRANS_R; RC_INC; SC_INC]);;
503 let RSTC_CASES = prove
504 (`!(R:A->A->bool) x z. RSTC R x z <=> (x = z) \/ R x z \/ RSTC R z x \/
505 ?y. RSTC R x y /\ RSTC R y z`,
506 REWRITE_TAC[RSTC; RC_TC; RC_SC] THEN REWRITE_TAC[GSYM STC] THEN
507 MESON_TAC[STC_CASES; RC_CASES]);;
509 let RSTC_CASES_L = prove
510 (`!(R:A->A->bool) x z. RSTC R x z <=> (x = z) \/ R x z \/ RSTC R z x \/
511 ?y. RSTC R x y /\ R y z`,
512 REWRITE_TAC[RSTC; RC_TC; RC_SC] THEN REWRITE_TAC[GSYM STC] THEN
513 MESON_TAC[STC_CASES_L; RC_CASES]);;
515 let RSTC_CASES_R = prove
516 (`!(R:A->A->bool) x z. RSTC R x z <=> (x = z) \/ R x z \/ RSTC R z x \/
517 ?y. R x y /\ RSTC R y z`,
518 REWRITE_TAC[RSTC; RC_TC; RC_SC] THEN REWRITE_TAC[GSYM STC] THEN
519 MESON_TAC[STC_CASES_R; RC_CASES]);;
521 let RSTC_INDUCT = prove
523 (!x y. R x y ==> P x y) /\
525 (!x y. P x y ==> P y x) /\
526 (!x y z. P x y /\ P y z ==> P x z)
527 ==> !x y. RSTC R x y ==> P x y`,
528 REPEAT GEN_TAC THEN STRIP_TAC THEN
529 REWRITE_TAC[RSTC; RC_TC; RC_SC] THEN REWRITE_TAC[GSYM STC] THEN
530 MATCH_MP_TAC STC_INDUCT THEN REWRITE_TAC[RC_EXPLICIT] THEN ASM_MESON_TAC[]);;
532 let RSTC_MONO = prove
534 (!x y. R x y ==> S x y) ==>
535 (!x y. RSTC R x y ==> RSTC S x y)`,
536 REWRITE_TAC[RSTC] THEN MESON_TAC[RC_MONO; SC_MONO; TC_MONO]);;
538 let RSTC_CLOSED = prove
539 (`!R:A->A->bool. (RSTC R = R) <=> (!x. R x x) /\
540 (!x y. R x y ==> R y x) /\
541 (!x y z. R x y /\ R y z ==> R x z)`,
542 REWRITE_TAC[RSTC] THEN REWRITE_TAC[GSYM STC; GSYM STC_CLOSED] THEN
543 REWRITE_TAC[RC_EXPLICIT; FUN_EQ_THM] THEN MESON_TAC[STC_INC]);;
545 let RSTC_IDEMP = prove
546 (`!R:A->A->bool. RSTC(RSTC R) = RSTC R`,
547 REWRITE_TAC[RSTC_CLOSED; RSTC_REFL; RSTC_SYM; RSTC_TRANS]);;
549 (* ------------------------------------------------------------------------- *)
550 (* Finally, we prove the inclusion properties for composite closures *)
551 (* ------------------------------------------------------------------------- *)
553 let RSC_INC_RC = prove
554 (`!R:A->A->bool. !x y. RC R x y ==> RSC R x y`,
555 REWRITE_TAC[RSC; RC_SC; SC_INC]);;
557 let RSC_INC_SC = prove
558 (`!R:A->A->bool. !x y. SC R x y ==> RSC R x y`,
559 REWRITE_TAC[RSC; RC_INC]);;
561 let RTC_INC_RC = prove
562 (`!R:A->A->bool. !x y. RC R x y ==> RTC R x y`,
563 REWRITE_TAC[RTC; RC_TC; TC_INC]);;
565 let RTC_INC_TC = prove
566 (`!R:A->A->bool. !x y. TC R x y ==> RTC R x y`,
567 REWRITE_TAC[RTC; RC_INC]);;
569 let STC_INC_SC = prove
570 (`!R:A->A->bool. !x y. SC R x y ==> STC R x y`,
571 REWRITE_TAC[STC; TC_INC]);;
573 let STC_INC_TC = prove
574 (`!R:A->A->bool. !x y. TC R x y ==> STC R x y`,
575 REWRITE_TAC[STC] THEN MESON_TAC[TC_MONO; SC_INC]);;
577 let RSTC_INC_RC = prove
578 (`!R:A->A->bool. !x y. RC R x y ==> RSTC R x y`,
579 REWRITE_TAC[RSTC; RC_TC; RC_SC; GSYM STC; STC_INC]);;
581 let RSTC_INC_SC = prove
582 (`!R:A->A->bool. !x y. SC R x y ==> RSTC R x y`,
583 REWRITE_TAC[RSTC; GSYM RTC; RTC_INC]);;
585 let RSTC_INC_TC = prove
586 (`!R:A->A->bool. !x y. TC R x y ==> RSTC R x y`,
587 REWRITE_TAC[RSTC; RC_TC; GSYM RSC] THEN MESON_TAC[TC_MONO; RSC_INC]);;
589 let RSTC_INC_RSC = prove
590 (`!R:A->A->bool. !x y. RSC R x y ==> RSTC R x y`,
591 REWRITE_TAC[RSC; RSTC; RC_TC; TC_INC]);;
593 let RSTC_INC_RTC = prove
594 (`!R:A->A->bool. !x y. RTC R x y ==> RSTC R x y`,
595 REWRITE_TAC[GSYM RTC; RSTC] THEN MESON_TAC[RTC_MONO; SC_INC]);;
597 let RSTC_INC_STC = prove
598 (`!R:A->A->bool. !x y. STC R x y ==> RSTC R x y`,
599 REWRITE_TAC[GSYM STC; RSTC; RC_INC]);;
601 (* ------------------------------------------------------------------------- *)
602 (* Handy things about reverse relations. *)
603 (* ------------------------------------------------------------------------- *)
605 let INV = new_definition
606 `INV R (x:A) (y:B) <=> R y x`;;
609 (`RC(INV R) = INV(RC R)`,
610 REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT; INV; EQ_SYM_EQ]);;
613 (`SC(INV R) = INV(SC R)`,
614 REWRITE_TAC[FUN_EQ_THM; SC_EXPLICIT; INV; DISJ_SYM]);;
616 let SC_INV_STRONG = prove
618 REWRITE_TAC[FUN_EQ_THM; SC_EXPLICIT; INV; DISJ_SYM]);;
621 (`TC(INV R) = INV(TC R)`,
622 REWRITE_TAC[FUN_EQ_THM; INV] THEN REPEAT GEN_TAC THEN EQ_TAC THEN
623 RULE_INDUCT_TAC TC_INDUCT THEN MESON_TAC[INV; TC_RULES]);;
626 (`RSC(INV R) = INV(RSC R)`,
627 REWRITE_TAC[RSC; RC_INV; SC_INV]);;
630 (`RTC(INV R) = INV(RTC R)`,
631 REWRITE_TAC[RTC; RC_INV; TC_INV]);;
634 (`STC(INV R) = INV(STC R)`,
635 REWRITE_TAC[STC; SC_INV; TC_INV]);;
638 (`RSTC(INV R) = INV(RSTC R)`,
639 REWRITE_TAC[RSTC; RC_INV; SC_INV; TC_INV]);;
641 (* ------------------------------------------------------------------------- *)
642 (* An iterative version of (R)TC. *)
643 (* ------------------------------------------------------------------------- *)
645 let RELPOW = new_recursive_definition num_RECURSION
646 `(RELPOW 0 (R:A->A->bool) x y <=> (x = y)) /\
647 (RELPOW (SUC n) R x y <=> ?z. RELPOW n R x z /\ R z y)`;;
650 (`(RELPOW 0 (R:A->A->bool) x y <=> (x = y)) /\
651 (RELPOW (SUC n) R x y <=> ?z. R x z /\ RELPOW n R z y)`,
652 CONJ_TAC THENL [REWRITE_TAC[RELPOW]; ALL_TAC] THEN
653 MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`x:A`; `y:A`; `n:num`] THEN
654 INDUCT_TAC THEN ASM_MESON_TAC[RELPOW]);;
657 (`!m n x:A y. RELPOW (m + n) R x y <=> ?z. RELPOW m R x z /\ RELPOW n R z y`,
658 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; RELPOW_R; UNWIND_THM1] THEN
661 let RTC_RELPOW = prove
662 (`!R (x:A) y. RTC R x y <=> ?n. RELPOW n R x y`,
663 REPEAT GEN_TAC THEN EQ_TAC THENL
664 [RULE_INDUCT_TAC RTC_INDUCT_L THEN MESON_TAC[RELPOW];
665 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN SPEC_TAC(`y:A`,`y:A`) THEN
666 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THEN
667 REWRITE_TAC[RELPOW] THEN ASM_MESON_TAC[RTC_REFL; RTC_TRANS_L]]);;
669 let TC_RELPOW = prove
670 (`!R (x:A) y. TC R x y <=> ?n. RELPOW (SUC n) R x y`,
671 REWRITE_TAC[RELPOW] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
672 REWRITE_TAC[LEFT_EXISTS_AND_THM; GSYM RTC_RELPOW] THEN
673 ONCE_REWRITE_TAC[TC_CASES_L] THEN REWRITE_TAC[RTC; RC_EXPLICIT] THEN
676 let RELPOW_SEQUENCE = prove
677 (`!R n x y. RELPOW n R x y <=> ?f. (f(0) = x:A) /\ (f(n) = y) /\
678 !i. i < n ==> R (f i) (f(SUC i))`,
679 GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LT; RELPOW] THENL
680 [REPEAT GEN_TAC THEN EQ_TAC THENL
681 [DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `\n:num. y:A` THEN REWRITE_TAC[];
683 REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
684 [DISJ_CASES_TAC(ARITH_RULE `(n = 0) \/ 0 < n`) THENL
685 [EXISTS_TAC `\i. if i = 0 then x else y:A` THEN
686 ASM_REWRITE_TAC[ARITH; LT] THEN
687 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_SUC] THEN
689 EXISTS_TAC `\i. if i <= n then f(i) else (y:A)` THEN
690 ASM_REWRITE_TAC[LE_0; ARITH_RULE `~(SUC n <= n)`] THEN
691 REPEAT STRIP_TAC THEN
692 ASM_REWRITE_TAC[LE_REFL; ARITH_RULE `~(SUC n <= n)`] THEN
693 ASM_REWRITE_TAC[LE_SUC_LT] THEN
694 ASM_REWRITE_TAC[LE_LT] THEN
695 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
696 EXISTS_TAC `(f:num->A) n` THEN CONJ_TAC THENL
697 [EXISTS_TAC `f:num->A` THEN ASM_REWRITE_TAC[] THEN
698 REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
700 ASM_MESON_TAC[]]]]);;