Library/rstc.ml

   1 (* ========================================================================= *)
   2 (* All you wanted to know about reflexive symmetric and transitive closures. *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 let RULE_INDUCT_TAC =
   8   MATCH_MP_TAC o DISCH_ALL o SPEC_ALL o UNDISCH o SPEC_ALL;;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Little lemmas about equivalent forms of symmetry and transitivity.        *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let SYM_ALT = prove
  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);;
  20
  21 let TRANS_ALT = prove
  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[]);;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* Reflexive closure                                                         *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let RC_RULES,RC_INDUCT,RC_CASES = new_inductive_definition
  33   `(!x y. R x y ==> RC R x y) /\
  34    (!x:A. RC R x x)`;;
  35
  36 let RC_INC = prove
  37  (`!(R:A->A->bool) x y. R x y ==> RC R x y`,
  38   REWRITE_TAC[RC_RULES]);;
  39
  40 let RC_REFL = prove
  41  (`!(R:A->A->bool) x. RC R x x`,
  42   REWRITE_TAC[RC_RULES]);;
  43
  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]);;
  47
  48 let RC_MONO = prove
  49  (`!(R:A->A->bool) S.
  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]);;
  53
  54 let RC_CLOSED = prove
  55  (`!R:A->A->bool. (RC R = R) <=> !x. R x x`,
  56   REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT] THEN MESON_TAC[]);;
  57
  58 let RC_IDEMP = prove
  59  (`!R:A->A->bool. RC(RC R) = RC R`,
  60   REWRITE_TAC[RC_CLOSED; RC_REFL]);;
  61
  62 let RC_SYM = prove
  63  (`!R:A->A->bool.
  64         (!x y. R x y ==> R y x) ==> (!x y. RC R x y ==> RC R y x)`,
  65   MESON_TAC[RC_CASES]);;
  66
  67 let RC_TRANS = prove
  68  (`!R:A->A->bool.
  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[]);;
  72
  73 (* ------------------------------------------------------------------------- *)
  74 (* Symmetric closure                                                         *)
  75 (* ------------------------------------------------------------------------- *)
  76
  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)`;;
  80
  81 let SC_INC = prove
  82  (`!(R:A->A->bool) x y. R x y ==> SC R x y`,
  83   REWRITE_TAC[SC_RULES]);;
  84
  85 let SC_SYM = prove
  86  (`!(R:A->A->bool) x y. SC R x y ==> SC R y x`,
  87   REWRITE_TAC[SC_RULES]);;
  88
  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]]);;
  93
  94 let SC_MONO = prove
  95  (`!(R:A->A->bool) S.
  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]);;
  99
 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[]);;
 103
 104 let SC_IDEMP = prove
 105  (`!R:A->A->bool. SC(SC R) = SC R`,
 106   REWRITE_TAC[SC_CLOSED; SC_SYM]);;
 107
 108 let SC_REFL = prove
 109  (`!R:A->A->bool. (!x. R x x) ==> (!x. SC R x x)`,
 110   MESON_TAC[SC_EXPLICIT]);;
 111
 112 (* ------------------------------------------------------------------------- *)
 113 (* Transitive closure                                                        *)
 114 (* ------------------------------------------------------------------------- *)
 115
 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)`;;
 119
 120 let TC_INC = prove
 121  (`!(R:A->A->bool) x y. R x y ==> TC R x y`,
 122   REWRITE_TAC[TC_RULES]);;
 123
 124 let TC_TRANS = prove
 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]);;
 127
 128 let TC_MONO = prove
 129  (`!(R:A->A->bool) S.
 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]);;
 134
 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]);;
 141
 142 let TC_IDEMP = prove
 143  (`!R:A->A->bool. TC(TC R) = TC R`,
 144   REWRITE_TAC[TC_CLOSED; TC_TRANS]);;
 145
 146 let TC_REFL = prove
 147  (`!R:A->A->bool. (!x. R x x) ==> (!x. TC R x x)`,
 148   MESON_TAC[TC_INC]);;
 149
 150 let TC_SYM = prove
 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]);;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Commutativity properties of the three basic closure operations            *)
 157 (* ------------------------------------------------------------------------- *)
 158
 159 let RC_SC = prove
 160  (`!R:A->A->bool. RC(SC R) = SC(RC R)`,
 161   REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT; SC_EXPLICIT] THEN MESON_TAC[]);;
 162
 163 let SC_RC = prove
 164  (`!R:A->A->bool. SC(RC R) = RC(SC R)`,
 165   REWRITE_TAC[RC_SC]);;
 166
 167 let RC_TC = prove
 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]]);;
 172
 173 let TC_RC = prove
 174  (`!R:A->A->bool. TC(RC R) = RC(TC R)`,
 175   REWRITE_TAC[RC_TC]);;
 176
 177 let TC_SC = prove
 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]);;
 181
 182 let SC_TC = prove
 183  (`!(R:A->A->bool) x y. SC(TC R) x y ==> TC(SC R) x y`,
 184   REWRITE_TAC[TC_SC]);;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* Left and right variants of TC.                                            *)
 188 (* ------------------------------------------------------------------------- *)
 189
 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]);;
 193
 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]);;
 197
 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]]);;
 202
 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]]);;
 207
 208 let TC_INDUCT_L = prove
 209  (`!(R:A->A->bool) P.
 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]]);;
 216
 217 let TC_INDUCT_R = prove
 218  (`!(R:A->A->bool) P.
 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]]);;
 225
 226 (* ------------------------------------------------------------------------- *)
 227 (* Reflexive symmetric closure                                               *)
 228 (* ------------------------------------------------------------------------- *)
 229
 230 let RSC = new_definition
 231   `RSC(R:A->A->bool) = RC(SC R)`;;
 232
 233 let RSC_INC = prove
 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]);;
 236
 237 let RSC_REFL = prove
 238  (`!(R:A->A->bool) x. RSC R x x`,
 239   REWRITE_TAC[RSC; RC_REFL]);;
 240
 241 let RSC_SYM = prove
 242  (`!(R:A->A->bool) x y. RSC R x y ==> RSC R y x`,
 243   REWRITE_TAC[RSC; RC_SC; SC_SYM]);;
 244
 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]);;
 248
 249 let RSC_INDUCT = prove
 250  (`!(R:A->A->bool) P.
 251         (!x y. R x y ==> P x y) /\
 252         (!x. P x x) /\
 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[]);;
 256
 257 let RSC_MONO = prove
 258  (`!(R:A->A->bool) S.
 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]);;
 262
 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[]);;
 266
 267 let RSC_IDEMP = prove
 268  (`!R:A->A->bool. RSC(RSC R) = RSC R`,
 269   REWRITE_TAC[RSC_CLOSED; RSC_REFL; RSC_SYM]);;
 270
 271 (* ------------------------------------------------------------------------- *)
 272 (* Reflexive transitive closure                                              *)
 273 (* ------------------------------------------------------------------------- *)
 274
 275 let RTC = new_definition
 276   `RTC(R:A->A->bool) = RC(TC R)`;;
 277
 278 let RTC_INC = prove
 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]);;
 281
 282 let RTC_REFL = prove
 283  (`!(R:A->A->bool) x. RTC R x x`,
 284   REWRITE_TAC[RTC; RC_REFL]);;
 285
 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]);;
 289
 290 let RTC_RULES = prove
 291  (`!(R:A->A->bool).
 292         (!x y. R x y ==> RTC R x y) /\
 293         (!x. RTC R x x) /\
 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]);;
 296
 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]);;
 300
 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]);;
 304
 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]);;
 308
 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]);;
 312
 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]);;
 316
 317 let RTC_INDUCT = prove
 318  (`!(R:A->A->bool) P.
 319         (!x y. R x y ==> P x y) /\
 320         (!x. P x x) /\
 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[]);;
 325
 326 let RTC_INDUCT_L = prove
 327  (`!(R:A->A->bool) P.
 328         (!x. P x x) /\
 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
 333   ASM_MESON_TAC[]);;
 334
 335 let RTC_INDUCT_R = prove
 336  (`!(R:A->A->bool) P.
 337         (!x. P x x) /\
 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
 342   ASM_MESON_TAC[]);;
 343
 344 let RTC_MONO = prove
 345  (`!(R:A->A->bool) S.
 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]);;
 349
 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]);;
 355
 356 let RTC_IDEMP = prove
 357  (`!R:A->A->bool. RTC(RTC R) = RTC R`,
 358   REWRITE_TAC[RTC_CLOSED; RTC_REFL; RTC_TRANS]);;
 359
 360 let RTC_SYM = prove
 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]);;
 363
 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[]);;
 369
 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]);;
 373
 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]);;
 377
 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]);;
 381
 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]);;
 385
 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]);;
 391
 392 (* ------------------------------------------------------------------------- *)
 393 (* Symmetric transitive closure                                              *)
 394 (* ------------------------------------------------------------------------- *)
 395
 396 let STC = new_definition
 397   `STC(R:A->A->bool) = TC(SC R)`;;
 398
 399 let STC_INC = prove
 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]);;
 402
 403 let STC_SYM = prove
 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]);;
 406
 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]);;
 410
 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]);;
 414
 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]);;
 418
 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]);;
 423
 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]);;
 428
 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]);;
 433
 434 let STC_INDUCT = prove
 435  (`!(R:A->A->bool) P.
 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]);;
 442
 443 let STC_MONO = prove
 444  (`!(R:A->A->bool) S.
 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]);;
 448
 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[]]);;
 455
 456 let STC_IDEMP = prove
 457  (`!R:A->A->bool. STC(STC R) = STC R`,
 458   REWRITE_TAC[STC_CLOSED; STC_SYM; STC_TRANS]);;
 459
 460 let STC_REFL = prove
 461  (`!R:A->A->bool. (!x. R x x) ==> !x. STC R x x`,
 462   MESON_TAC[STC_INC]);;
 463
 464 (* ------------------------------------------------------------------------- *)
 465 (* Reflexive symmetric transitive closure (smallest equivalence relation)    *)
 466 (* ------------------------------------------------------------------------- *)
 467
 468 let RSTC = new_definition
 469   `RSTC(R:A->A->bool) = RC(TC(SC R))`;;
 470
 471 let RSTC_INC = prove
 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]);;
 474
 475 let RSTC_REFL = prove
 476  (`!(R:A->A->bool) x. RSTC R x x`,
 477   REWRITE_TAC[RSTC; RC_REFL]);;
 478
 479 let RSTC_SYM = prove
 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]);;
 482
 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]);;
 486
 487 let RSTC_RULES = prove
 488  (`!(R:A->A->bool).
 489         (!x y. R x y ==> RSTC R x y) /\
 490         (!x. RSTC R x x) /\
 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]);;
 494
 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]);;
 498
 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]);;
 502
 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]);;
 508
 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]);;
 514
 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]);;
 520
 521 let RSTC_INDUCT = prove
 522  (`!(R:A->A->bool) P.
 523         (!x y. R x y ==> P x y) /\
 524         (!x. P x x) /\
 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[]);;
 531
 532 let RSTC_MONO = prove
 533  (`!(R:A->A->bool) S.
 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]);;
 537
 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]);;
 544
 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]);;
 548
 549 (* ------------------------------------------------------------------------- *)
 550 (* Finally, we prove the inclusion properties for composite closures         *)
 551 (* ------------------------------------------------------------------------- *)
 552
 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]);;
 556
 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]);;
 560
 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]);;
 564
 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]);;
 568
 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]);;
 572
 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]);;
 576
 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]);;
 580
 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]);;
 584
 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]);;
 588
 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]);;
 592
 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]);;
 596
 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]);;
 600
 601 (* ------------------------------------------------------------------------- *)
 602 (* Handy things about reverse relations.                                     *)
 603 (* ------------------------------------------------------------------------- *)
 604
 605 let INV = new_definition
 606   `INV R (x:A) (y:B) <=> R y x`;;
 607
 608 let RC_INV = prove
 609  (`RC(INV R) = INV(RC R)`,
 610   REWRITE_TAC[FUN_EQ_THM; RC_EXPLICIT; INV; EQ_SYM_EQ]);;
 611
 612 let SC_INV = prove
 613  (`SC(INV R) = INV(SC R)`,
 614   REWRITE_TAC[FUN_EQ_THM; SC_EXPLICIT; INV; DISJ_SYM]);;
 615
 616 let SC_INV_STRONG = prove
 617  (`SC(INV R) = SC R`,
 618   REWRITE_TAC[FUN_EQ_THM; SC_EXPLICIT; INV; DISJ_SYM]);;
 619
 620 let TC_INV = prove
 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]);;
 624
 625 let RSC_INV = prove
 626  (`RSC(INV R) = INV(RSC R)`,
 627   REWRITE_TAC[RSC; RC_INV; SC_INV]);;
 628
 629 let RTC_INV = prove
 630  (`RTC(INV R) = INV(RTC R)`,
 631   REWRITE_TAC[RTC; RC_INV; TC_INV]);;
 632
 633 let STC_INV = prove
 634  (`STC(INV R) = INV(STC R)`,
 635   REWRITE_TAC[STC; SC_INV; TC_INV]);;
 636
 637 let RSTC_INV = prove
 638  (`RSTC(INV R) = INV(RSTC R)`,
 639   REWRITE_TAC[RSTC; RC_INV; SC_INV; TC_INV]);;
 640
 641 (* ------------------------------------------------------------------------- *)
 642 (* An iterative version of (R)TC.                                            *)
 643 (* ------------------------------------------------------------------------- *)
 644
 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)`;;
 648
 649 let RELPOW_R = prove
 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]);;
 655
 656 let RELPOW_M = prove
 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
 659   MESON_TAC[]);;
 660
 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]]);;
 668
 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
 674   MESON_TAC[]);;
 675
 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[];
 682       MESON_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
 688         ASM_MESON_TAC[];
 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
 699         ASM_REWRITE_TAC[];
 700         ASM_MESON_TAC[]]]]);;