Examples/reduct.ml

   1 (* ========================================================================= *)
   2 (* General "reduction" properties of binary relations,                       *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/rstc.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Field of a binary relation.                                               *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let FL = new_definition
  12   `FL(R) x <=> (?y:A. R x y) \/ (?y. R y x)`;;
  13
  14 (* ------------------------------------------------------------------------ *)
  15 (* Normality of a term w.r.t. a reduction relation                          *)
  16 (* ------------------------------------------------------------------------ *)
  17
  18 let NORMAL = new_definition
  19   `NORMAL(R:A->A->bool) x <=> ~(?y. R x y)`;;
  20
  21 (* ------------------------------------------------------------------------ *)
  22 (* Full Church-Rosser property.                                             *)
  23 (*                                                                          *)
  24 (* Note that we deviate from most term rewriting literature which call this *)
  25 (* the "diamond property" and calls a relation "Church-Rosser" iff its RTC  *)
  26 (* has the diamond property. But this seems simpler and more natural.       *)
  27 (* ------------------------------------------------------------------------ *)
  28
  29 let CR = new_definition
  30   `CR(R:A->A->bool) <=> !x y1 y2. R x y1 /\ R x y2 ==> ?z. R y1 z /\ R y2 z`;;
  31
  32 (* ------------------------------------------------------------------------ *)
  33 (* Weak Church-Rosser property, i.e. the rejoining may take several steps.  *)
  34 (* ------------------------------------------------------------------------ *)
  35
  36 let WCR = new_definition
  37   `WCR(R:A->A->bool) <=>
  38    !x y1 y2. R x y1 /\ R x y2 ==> ?z. RTC R y1 z /\ RTC R y2 z`;;
  39
  40 (* ------------------------------------------------------------------------ *)
  41 (* (Weak) normalization: every term has a normal form.                      *)
  42 (* ------------------------------------------------------------------------ *)
  43
  44 let WN = new_definition
  45   `WN(R:A->A->bool) <=> !x. ?y. RTC R x y /\ NORMAL(R) y`;;
  46
  47 (* ------------------------------------------------------------------------ *)
  48 (* Strong normalization: every reduction sequence terminates (Noetherian)   *)
  49 (* ------------------------------------------------------------------------ *)
  50
  51 let SN = new_definition
  52   `SN(R:A->A->bool) <=> ~(?seq. !n. R (seq n) (seq (SUC n)))`;;
  53
  54 (* ------------------------------------------------------------------------- *)
  55 (* Definition of a tree.                                                     *)
  56 (* ------------------------------------------------------------------------- *)
  57
  58 let TREE = new_definition
  59   `TREE(R:A->A->bool) <=>
  60         (!y. ~(TC R y y)) /\
  61         ?a. a IN FL(R) /\
  62             !y. y IN FL(R) ==> (y = a) \/ TC R a y /\ ?!x. R x y`;;
  63
  64 (* ------------------------------------------------------------------------- *)
  65 (* Local finiteness (finitely branching).                                    *)
  66 (* ------------------------------------------------------------------------- *)
  67
  68 let LF = new_definition
  69   `LF(R:A->A->bool) <=> !x. FINITE {y | R x y}`;;
  70
  71 (* ------------------------------------------------------------------------- *)
  72 (* Wellfoundedness apparatus for SN relations.                               *)
  73 (* ------------------------------------------------------------------------- *)
  74
  75 let SN_WF = prove
  76  (`!R:A->A->bool. SN(R) <=> WF(INV R)`,
  77   REWRITE_TAC[SN; WF_DCHAIN; INV]);;
  78
  79 let SN_PRESERVE = prove
  80  (`!R:A->A->bool. SN(R) <=> !P. (!x. P x ==> ?y. P y /\ R x y) ==> ~(?x. P x)`,
  81   REWRITE_TAC[SN_WF; WF; INV] THEN MESON_TAC[]);;
  82
  83 let SN_NOETHERIAN = prove
  84  (`!R:A->A->bool. SN(R) <=> !P. (!x. (!y. R x y ==> P y) ==> P x) ==> !x. P x`,
  85   REWRITE_TAC[WF_IND; SN_WF; INV]);;
  86
  87 (* ------------------------------------------------------------------------ *)
  88 (* Normality and weak normalization is preserved by transitive closure.     *)
  89 (* ------------------------------------------------------------------------ *)
  90
  91 let NORMAL_TC = prove
  92  (`!R:A->A->bool. NORMAL(TC R) x <=> NORMAL(R) x`,
  93   REWRITE_TAC[NORMAL] THEN MESON_TAC[TC_CASES_R; TC_INC]);;
  94
  95 let NORMAL_RTC = prove
  96  (`!R:A->A->bool. NORMAL(R) x ==> !y. RTC R x y <=> (x = y)`,
  97   ONCE_REWRITE_TAC[GSYM NORMAL_TC] THEN
  98   REWRITE_TAC[NORMAL; RTC; RC_EXPLICIT] THEN MESON_TAC[]);;
  99
 100 let WN_TC = prove
 101  (`!R:A->A->bool. WN(TC R) <=> WN R`,
 102   REWRITE_TAC[WN; NORMAL_TC; RTC; TC_IDEMP]);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* Wellfoundedness and strong normalization are too.                         *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let WF_TC = prove
 109  (`!R:A->A->bool. WF(TC R) <=> WF(R)`,
 110   GEN_TAC THEN EQ_TAC THENL
 111    [MESON_TAC[WF_SUBSET; TC_INC];
 112     REWRITE_TAC[WF] THEN DISCH_TAC THEN X_GEN_TAC `P:A->bool` THEN
 113     FIRST_X_ASSUM(MP_TAC o SPEC `\y:A. ?z. P z /\ TC(R) z y`) THEN
 114     REWRITE_TAC[] THEN MESON_TAC[TC_CASES_L]]);;
 115
 116 (******************* Alternative --- intuitionistic --- proof
 117
 118 let WF_TC = prove
 119  (`!R:A->A->bool. WF(TC R) <=> WF(R)`,
 120   GEN_TAC THEN EQ_TAC THENL
 121    [MESON_TAC[WF_SUBSET; TC_INC];
 122     REWRITE_TAC[WF_IND]] THEN
 123   DISCH_TAC THEN GEN_TAC THEN
 124   FIRST_ASSUM(MP_TAC o SPEC `\z:A. !u:A. TC(R) u z ==> P(u)`) THEN
 125   REWRITE_TAC[] THEN MESON_TAC[TC_CASES_L]);;
 126
 127 let WF_TC_EXPLICIT = prove
 128  (`!R:A->A->bool. WF(R) ==> WF(TC(R))`,
 129   GEN_TAC THEN REWRITE_TAC[WF_IND] THEN DISCH_TAC THEN
 130   GEN_TAC THEN DISCH_TAC THEN
 131   FIRST_X_ASSUM(MP_TAC o SPEC `\z:A. !u:A. TC(R) u z ==> P(u)`) THEN
 132   REWRITE_TAC[] THEN STRIP_TAC THEN X_GEN_TAC `z:A` THEN
 133   FIRST_ASSUM MATCH_MP_TAC THEN SPEC_TAC(`z:A`,`z:A`) THEN
 134   FIRST_ASSUM MATCH_MP_TAC THEN
 135   GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o REDEPTH_CONV)
 136    [RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
 137   DISCH_TAC THEN X_GEN_TAC `u:A` THEN
 138   ONCE_REWRITE_TAC[TC_CASES_L] THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
 139    [DISCH_TAC THEN
 140     MATCH_MP_TAC(ASSUME `!x:A. (!y. TC R y x ==> P y) ==> P x`) THEN
 141     X_GEN_TAC `v:A` THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 142     EXISTS_TAC `u:A` THEN CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC;
 143     DISCH_THEN(X_CHOOSE_THEN `w:A` STRIP_ASSUME_TAC) THEN
 144     FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `w:A` THEN
 145     CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC]);;
 146
 147 ***********************)
 148
 149 let SN_TC = prove
 150  (`!R:A->A->bool. SN(TC R) <=> SN R`,
 151   GEN_TAC THEN REWRITE_TAC[SN_WF; GSYM TC_INV; WF_TC]);;
 152
 153 (* ------------------------------------------------------------------------ *)
 154 (* Strong normalization implies normalization                               *)
 155 (* ------------------------------------------------------------------------ *)
 156
 157 let SN_WN = prove
 158  (`!R:A->A->bool. SN(R) ==> WN(R)`,
 159   GEN_TAC THEN REWRITE_TAC[SN_WF; WF; WN] THEN DISCH_TAC THEN
 160   X_GEN_TAC `a:A` THEN POP_ASSUM(MP_TAC o SPEC `\y:A. RTC R a y`) THEN
 161   REWRITE_TAC[INV; NORMAL] THEN MESON_TAC[RTC_REFL; RTC_TRANS_L]);;
 162
 163 (* ------------------------------------------------------------------------ *)
 164 (* Reflexive closure preserves Church-Rosser property (pretty trivial)      *)
 165 (* ------------------------------------------------------------------------ *)
 166
 167 let RC_CR = prove
 168  (`!R:A->A->bool. CR(R) ==> CR(RC R)`,
 169   REWRITE_TAC[CR; RC_EXPLICIT] THEN MESON_TAC[]);;
 170
 171 (* ------------------------------------------------------------------------ *)
 172 (* The strip lemma leads us halfway to the fact that transitive        x    *)
 173 (* closure preserves the Church-Rosser property. It's no harder       / \   *)
 174 (* to prove it for two separate reduction relations. This then       /   y2 *)
 175 (* allows us to prove the desired theorem simply by using the       /    /  *)
 176 (* strip lemma twice with a bit of conjunct-swapping.              y1   /   *)
 177 (*                                                                   \ /    *)
 178 (* The diagram on the right shows the use of the variables.           z     *)
 179 (* ------------------------------------------------------------------------ *)
 180
 181 let STRIP_LEMMA = prove
 182  (`!R S. (!x y1 y2.    R x y1 /\ S x y2 ==> ?z:A. S y1 z /\    R y2 z) ==>
 183          (!x y1 y2. TC R x y1 /\ S x y2 ==> ?z:A. S y1 z /\ TC R y2 z)`,
 184   REPEAT GEN_TAC THEN DISCH_TAC THEN
 185   REWRITE_TAC[TAUT `a /\ b ==> c <=> a ==> (b ==> c)`] THEN
 186   REWRITE_TAC[GSYM RIGHT_IMP_FORALL_THM] THEN
 187   MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC[TC_INC; TC_TRANS]);;
 188
 189 (* ------------------------------------------------------------------------ *)
 190 (* Transitive closure preserves Church-Rosser property.                     *)
 191 (* ------------------------------------------------------------------------ *)
 192
 193 let TC_CR = prove
 194  (`!R:A->A->bool. CR(R) ==> CR(TC R)`,
 195   GEN_TAC THEN REWRITE_TAC[CR] THEN DISCH_TAC THEN
 196   MATCH_MP_TAC STRIP_LEMMA THEN REPEAT GEN_TAC THEN
 197   ONCE_REWRITE_TAC[CONJ_SYM] THEN
 198   RULE_INDUCT_TAC STRIP_LEMMA THEN ASM_REWRITE_TAC[]);;
 199
 200 (* ------------------------------------------------------------------------ *)
 201 (* Reflexive transitive closure preserves Church-Rosser property.           *)
 202 (* ------------------------------------------------------------------------ *)
 203
 204 let RTC_CR = prove
 205  (`!R:A->A->bool. CR(R) ==> CR(RTC R)`,
 206   REWRITE_TAC[RTC] THEN MESON_TAC[RC_CR; TC_CR]);;
 207
 208 (* ------------------------------------------------------------------------ *)
 209 (* Equivalent `Church-Rosser` property for the equivalence relation.        *)
 210 (* ------------------------------------------------------------------------ *)
 211
 212 let STC_CR = prove
 213  (`!R:A->A->bool. CR(RTC R) <=>
 214         !x y. RSTC R x y ==> ?z:A. RTC R x z /\ RTC R y z`,
 215   GEN_TAC THEN REWRITE_TAC[CR] THEN EQ_TAC THENL
 216    [DISCH_TAC THEN MATCH_MP_TAC RSTC_INDUCT THEN
 217     ASM_MESON_TAC[RTC_REFL; RTC_INC; RTC_TRANS];
 218     MESON_TAC[RSTC_INC_RTC; RSTC_SYM; RSTC_TRANS]]);;
 219
 220 (* ------------------------------------------------------------------------ *)
 221 (* Under normalization, Church-Rosser is equivalent to uniqueness of NF     *)
 222 (* ------------------------------------------------------------------------ *)
 223
 224 let NORM_CR = prove
 225  (`!R:A->A->bool. WN(R) ==>
 226      (CR(RTC R) <=> (!x y1 y2. RTC R x y1 /\ NORMAL(R) y1 /\
 227                                RTC R x y2 /\ NORMAL(R) y2 ==> (y1 = y2)))`,
 228   GEN_TAC THEN REWRITE_TAC[CR; WN] THEN DISCH_TAC THEN EQ_TAC THENL
 229    [MESON_TAC[NORMAL_RTC]; ASM_MESON_TAC[RTC_TRANS]]);;
 230
 231 (* ------------------------------------------------------------------------ *)
 232 (* Normalizing and Church-Rosser iff every term has a unique normal form    *)
 233 (* ------------------------------------------------------------------------ *)
 234
 235 let CR_NORM = prove
 236  (`!R:A->A->bool. WN(R) /\ CR(RTC R) <=> !x. ?!y. RTC R x y /\ NORMAL(R) y`,
 237   GEN_TAC THEN ONCE_REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 238   REWRITE_TAC[FORALL_AND_THM; GSYM WN] THEN
 239   MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
 240   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP NORM_CR th]) THEN
 241   REWRITE_TAC[CONJ_ASSOC]);;
 242
 243 (* ------------------------------------------------------------------------ *)
 244 (* Newman's lemma: weak Church-Rosser plus                   x              *)
 245 (* strong normalization implies full Church-                / \             *)
 246 (* Rosser. By the above (and SN ==> WN) it                 z1 z2            *)
 247 (* is sufficient to show normal forms are                 / | | \           *)
 248 (* unique. We use the Noetherian induction               /  \ /  \          *)
 249 (* form of SN, so we need only prove that if            /    z    \         *)
 250 (* some term has multiple normal forms, so             /     |     \        *)
 251 (* does a `successor`. See the diagram on the         /      |      \       *)
 252 (* right for the use of variables.                   y1      w       y2     *)
 253 (* ------------------------------------------------------------------------ *)
 254
 255 let NEWMAN_LEMMA = prove
 256  (`!R:A->A->bool. SN(R) /\ WCR(R) ==> CR(RTC R)`,
 257   GEN_TAC THEN STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP SN_WN) THEN
 258   DISCH_THEN(fun th -> ASSUME_TAC(REWRITE_RULE[WN] th) THEN MP_TAC th) THEN
 259   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP NORM_CR th]) THEN
 260   FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND; SN_WF]) THEN
 261   REWRITE_TAC[INV] THEN X_GEN_TAC `x:A` THEN REPEAT STRIP_TAC THEN
 262   MAP_EVERY UNDISCH_TAC [`RTC R (x:A) y1`; `RTC R (x:A) y2`] THEN
 263   ONCE_REWRITE_TAC[RTC_CASES_R] THEN
 264   DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (X_CHOOSE_TAC `z2:A`)) THEN
 265   DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (X_CHOOSE_TAC `z1:A`)) THENL
 266    [ASM_MESON_TAC[];ASM_MESON_TAC[NORMAL];ASM_MESON_TAC[NORMAL]; ALL_TAC] THEN
 267   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [WCR]) THEN
 268   ASM_MESON_TAC[RTC_TRANS]);;
 269
 270 (* ------------------------------------------------------------------------- *)
 271 (* A variant of Koenig's lemma.                                              *)
 272 (* ------------------------------------------------------------------------- *)
 273
 274 let LF_TC_FINITE = prove
 275  (`!R. LF(R) /\ SN(R) ==> !x:A. FINITE {y | TC(R) x y}`,
 276   GEN_TAC THEN REWRITE_TAC[LF] THEN STRIP_TAC THEN
 277   FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND; SN_WF; INV]) THEN
 278   GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN
 279     `{y:A | TC(R) x y} = {y | R x y} UNION
 280                          (UNIONS { s | ?z. R x z /\ (s = {y | TC(R) z y})})`
 281   SUBST1_TAC THENL
 282    [REWRITE_TAC[EXTENSION; IN_UNION; IN_UNIONS] THEN
 283     REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[IN] THEN
 284     GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [TC_CASES_R] THEN
 285     AP_TERM_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 286     ASM_MESON_TAC[]; ALL_TAC] THEN
 287   ASM_REWRITE_TAC[FINITE_UNION; FINITE_UNIONS] THEN CONJ_TAC THENL
 288    [MP_TAC(ISPECL [`\z:A. {y | TC R z y}`; `{z | (R:A->A->bool) x z}`]
 289                   FINITE_IMAGE_EXPAND) THEN
 290     ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN; IN_ELIM_THM];
 291     GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [IN_ELIM_THM] THEN
 292     REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 293     FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC]);;
 294
 295 let SN_NOLOOP = prove
 296  (`!R:A->A->bool. SN(R) ==> !z. ~(TC(R) z z)`,
 297   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM SN_TC] THEN
 298   SPEC_TAC(`TC(R:A->A->bool)`,`R:A->A->bool`) THEN
 299   GEN_TAC THEN REWRITE_TAC[SN_WF; INV; WF] THEN
 300   DISCH_THEN(fun th -> GEN_TAC THEN MP_TAC th) THEN
 301   DISCH_THEN(MP_TAC o SPEC `\x:A. x = z`) THEN
 302   REWRITE_TAC[] THEN MESON_TAC[]);;
 303
 304 let RELPOW_RTC = prove
 305  (`!R:A->A->bool. !n x y. RELPOW n R x y ==> RTC(R) x y`,
 306   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[RELPOW] THEN
 307   ASM_MESON_TAC[RTC_REFL; RTC_TRANS_L]);;
 308
 309 let RTC_TC_LEMMA = prove
 310  (`!R x:A. {y:A | RTC(R) x y} = x INSERT {y:A | TC(R) x y}`,
 311   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT] THEN
 312   REWRITE_TAC[RTC; RC_EXPLICIT; DISJ_ACI; EQ_SYM_EQ]);;
 313
 314 let HAS_SIZE_SUBSET = prove
 315  (`!s:A->bool t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ s SUBSET t ==> m <= n`,
 316   REWRITE_TAC[HAS_SIZE] THEN MESON_TAC[CARD_SUBSET]);;
 317
 318 let FC_FINITE_BOUND_LEMMA = prove
 319  (`!R. (!z. ~(TC R z z))
 320        ==> !n. {y:A | RTC(R) x y} HAS_SIZE n
 321                ==> !m y. RELPOW m R x y ==> m <= n`,
 322   REPEAT STRIP_TAC THEN
 323   FIRST_ASSUM(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC o
 324     REWRITE_RULE[RELPOW_SEQUENCE]) THEN
 325   SUBGOAL_THEN `!i. i <= m ==> RELPOW i R (x:A) (f i)` ASSUME_TAC THENL
 326    [INDUCT_TAC THEN ASM_REWRITE_TAC[RELPOW] THEN
 327     REWRITE_TAC[LE_SUC_LT] THEN ASM_MESON_TAC[LT_IMP_LE]; ALL_TAC] THEN
 328   SUBGOAL_THEN `{z:A | ?i:num. i < m /\ (z = f i)} SUBSET {y | RTC R x y}`
 329   ASSUME_TAC THENL
 330    [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[RELPOW_RTC; LT_IMP_LE];
 331     ALL_TAC] THEN
 332   SUBGOAL_THEN `!p. p <= m ==> {z:A | ?i. i < p /\ (z = f i)} HAS_SIZE p`
 333   (fun th -> ASSUME_TAC(MATCH_MP th (SPEC `m:num` LE_REFL))) THENL
 334    [ALL_TAC;
 335     MATCH_MP_TAC HAS_SIZE_SUBSET THEN
 336     EXISTS_TAC `{z:A | ?i. i < m /\ (z = f i)}` THEN
 337     EXISTS_TAC `{y:A | RTC(R) x y}` THEN ASM_REWRITE_TAC[]] THEN
 338   INDUCT_TAC THEN DISCH_TAC THENL
 339    [REWRITE_TAC[HAS_SIZE_0; EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM; LT];
 340     ALL_TAC] THEN
 341   SUBGOAL_THEN `{z:A | ?i. i < SUC p /\ (z = f i)} =
 342                 f(p) INSERT {z | ?i. i < p /\ (z = f i)}`
 343   SUBST1_TAC THENL
 344    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_ELIM_THM] THEN
 345     REWRITE_TAC[LT] THEN MESON_TAC[]; ALL_TAC] THEN
 346   REWRITE_TAC[HAS_SIZE; CARD_CLAUSES; SUC_INJ] THEN
 347   SUBGOAL_THEN `{z:A | ?i. i < p /\ (z = f i)} HAS_SIZE p` MP_TAC THENL
 348    [FIRST_ASSUM MATCH_MP_TAC THEN UNDISCH_TAC `SUC p <= m` THEN ARITH_TAC;
 349     ALL_TAC] THEN
 350   REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC THEN
 351   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP (CONJUNCT2 CARD_CLAUSES) th]) THEN
 352   COND_CASES_TAC THEN ASM_REWRITE_TAC[FINITE_INSERT] THEN
 353   UNDISCH_TAC `f p IN {z:A | ?i:num. i < p /\ (z = f i)}` THEN
 354   CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN
 355   REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM] THEN
 356   X_GEN_TAC `q:num` THEN
 357   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 358   SUBGOAL_THEN `TC(R) ((f:num->A) q) (f p)` (fun th -> ASM_MESON_TAC[th]) THEN
 359   UNDISCH_TAC `SUC p <= m` THEN UNDISCH_TAC `q < p` THEN
 360   REWRITE_TAC[LT_EXISTS] THEN
 361   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 362   SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THENL
 363    [REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN
 364     MATCH_MP_TAC TC_INC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 365     UNDISCH_TAC `SUC (SUC q) <= m` THEN ARITH_TAC;
 366     DISCH_TAC THEN MATCH_MP_TAC TC_TRANS_L THEN
 367     EXISTS_TAC `(f:num->A)(q + SUC d)` THEN CONJ_TAC THENL
 368      [ALL_TAC; REWRITE_TAC[ADD_CLAUSES]] THEN
 369     FIRST_ASSUM MATCH_MP_TAC THEN
 370     UNDISCH_TAC `SUC (q + SUC (SUC d)) <= m` THEN ARITH_TAC]);;
 371
 372 let FC_FINITE_BOUND = prove
 373  (`!R (x:A). FINITE {y | RTC(R) x y} /\
 374              (!z. ~(TC R z z))
 375              ==> ?N. !n y. RELPOW n R x y ==> n <= N`,
 376   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 377   DISCH_TAC THEN EXISTS_TAC `CARD {y:A | RTC(R) x y}` THEN
 378   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP FC_FINITE_BOUND_LEMMA) THEN
 379   ASM_REWRITE_TAC[HAS_SIZE]);;
 380
 381 let BOUND_SN = prove
 382  (`!R. (!x:A. ?N. !n y. RELPOW n R x y ==> n <= N) ==> SN(R)`,
 383   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SN_WF; WF_DCHAIN; INV] THEN
 384   DISCH_THEN(X_CHOOSE_TAC `f:num->A`) THEN
 385   FIRST_X_ASSUM(MP_TAC o SPEC `(f:num->A) 0`) THEN
 386   DISCH_THEN(X_CHOOSE_THEN `N:num`
 387    (MP_TAC o SPECL [`SUC N`; `f(SUC N):A`])) THEN
 388   REWRITE_TAC[GSYM NOT_LT; LT] THEN
 389   SUBGOAL_THEN `!n. RELPOW n R (f 0 :A) (f n)` (fun th -> REWRITE_TAC[th]) THEN
 390   INDUCT_TAC THEN ASM_REWRITE_TAC[RELPOW] THEN ASM_MESON_TAC[]);;
 391
 392 let LF_SN_BOUND = prove
 393  (`!R. LF(R) ==> (SN(R) <=> !x:A. ?N. !n y. RELPOW n R x y ==> n <= N)`,
 394   GEN_TAC THEN DISCH_TAC THEN EQ_TAC THEN REWRITE_TAC[BOUND_SN] THEN
 395   DISCH_TAC THEN GEN_TAC THEN MATCH_MP_TAC FC_FINITE_BOUND THEN CONJ_TAC THENL
 396    [SPEC_TAC(`x:A`,`x:A`) THEN REWRITE_TAC[RTC_TC_LEMMA; FINITE_INSERT] THEN
 397     MATCH_MP_TAC LF_TC_FINITE THEN ASM_REWRITE_TAC[];
 398     MATCH_MP_TAC SN_NOLOOP THEN ASM_REWRITE_TAC[]]);;
 399
 400 (* ------------------------------------------------------------------------- *)
 401 (* Koenig's lemma.                                                           *)
 402 (* ------------------------------------------------------------------------- *)
 403
 404 let TREE_FL = prove
 405  (`!R. TREE(R) ==> ?a:A. FL(R) = {y | RTC(R) a y}`,
 406   GEN_TAC THEN REWRITE_TAC[TREE] THEN
 407   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
 408    (X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC)) THEN
 409   EXISTS_TAC `a:A` THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 410   X_GEN_TAC `x:A` THEN EQ_TAC THENL
 411    [DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[RTC; RC_EXPLICIT] THEN
 412     MESON_TAC[]; ONCE_REWRITE_TAC[RTC_CASES_L] THEN ASM_MESON_TAC[IN; FL]]);;
 413
 414 let KOENIG_LEMMA = prove
 415  (`!R:A->A->bool. TREE(R) /\ LF(R) /\ SN(R) ==> FINITE (FL R)`,
 416   GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
 417   DISCH_THEN(X_CHOOSE_THEN `a:A` SUBST1_TAC o MATCH_MP TREE_FL) THEN
 418   REWRITE_TAC[RTC_TC_LEMMA; FINITE_INSERT] THEN
 419   SPEC_TAC(`a:A`,`a:A`) THEN MATCH_MP_TAC LF_TC_FINITE THEN
 420   ASM_REWRITE_TAC[]);;
 421
 422 (* ------------------------------------------------------------------------- *)
 423 (* Rephrasing in terms of joinability.                                       *)
 424 (* ------------------------------------------------------------------------- *)
 425
 426 let JOINABLE = new_definition
 427   `JOINABLE R s t <=> ?u. RTC R s u /\ RTC R t u`;;
 428
 429 let JOINABLE_REFL = prove
 430  (`!R t. JOINABLE R t t`,
 431   REWRITE_TAC[JOINABLE] THEN MESON_TAC[RTC_CASES]);;
 432
 433 let JOINABLE_SYM = prove
 434  (`!R s t. JOINABLE R s t <=> JOINABLE R t s`,
 435   REWRITE_TAC[JOINABLE] THEN MESON_TAC[]);;
 436
 437 let JOINABLE_TRANS_R = prove
 438  (`!R s t u. R s t /\ JOINABLE R t u ==> JOINABLE R s u`,
 439   REWRITE_TAC[JOINABLE] THEN MESON_TAC[RTC_CASES_R]);;
 440
 441 let CR_RSTC_JOINABLE = prove
 442  (`!R. CR(RTC R) ==> !x:A y. RSTC(R) x y <=> JOINABLE(R) x y`,
 443   GEN_TAC THEN REWRITE_TAC[STC_CR; JOINABLE] THEN
 444   ASM_MESON_TAC[RSTC_TRANS; RSTC_SYM; RSTC_INC_RTC]);;
 445
 446 (* ------------------------------------------------------------------------- *)
 447 (* CR is equivalent to transitivity of joinability.                          *)
 448 (* ------------------------------------------------------------------------- *)
 449
 450 let JOINABLE_TRANS = prove
 451  (`!R. CR(RTC R) <=>
 452        !x y z. JOINABLE(R) x y /\ JOINABLE(R) y z ==> JOINABLE(R) x z`,
 453   REWRITE_TAC[CR; JOINABLE] THEN MESON_TAC[RTC_REFL; RTC_TRANS; RTC_SYM]);;