wf.ml

   1 (* ========================================================================= *)
   2 (* Theory of wellfounded relations.                                          *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "arith.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Definition of wellfoundedness for arbitrary (infix) relation <<           *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 parse_as_infix("<<",(12,"right"));;
  17
  18 let WF = new_definition
  19   `WF(<<) <=> !P:A->bool. (?x. P(x)) ==> (?x. P(x) /\ !y. y << x ==> ~P(y))`;;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Strengthen it to equality.                                                *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let WF_EQ = prove
  26  (`WF(<<) <=> !P:A->bool. (?x. P(x)) <=> (?x. P(x) /\ !y. y << x ==> ~P(y))`,
  27   REWRITE_TAC[WF] THEN MESON_TAC[]);;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Equivalence of wellfounded induction.                                     *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let WF_IND = prove
  34  (`WF(<<) <=> !P:A->bool. (!x. (!y. y << x ==> P(y)) ==> P(x)) ==> !x. P(x)`,
  35   REWRITE_TAC[WF] THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THEN
  36   POP_ASSUM(MP_TAC o SPEC `\x:A. ~P(x)`) THEN REWRITE_TAC[] THEN MESON_TAC[]);;
  37
  38 (* ------------------------------------------------------------------------- *)
  39 (* Equivalence of the "infinite descending chains" version.                  *)
  40 (* ------------------------------------------------------------------------- *)
  41
  42 let WF_DCHAIN = prove
  43  (`WF(<<) <=> ~(?s:num->A. !n. s(SUC n) << s(n))`,
  44   REWRITE_TAC[WF; TAUT `(a <=> ~b) <=> (~a <=> b)`; NOT_FORALL_THM] THEN
  45   EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
  46    [POP_ASSUM(MP_TAC o REWRITE_RULE[NOT_IMP]) THEN
  47     DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:A`) ASSUME_TAC) THEN
  48     SUBGOAL_THEN `!x:A. ?y. P(x) ==> P(y) /\ y << x` MP_TAC THENL
  49      [ASM_MESON_TAC[]; REWRITE_TAC[SKOLEM_THM]] THEN
  50     DISCH_THEN(X_CHOOSE_THEN `f:A->A` STRIP_ASSUME_TAC) THEN
  51     CHOOSE_TAC(prove_recursive_functions_exist num_RECURSION
  52      `(s(0) = a:A) /\ (!n. s(SUC n) = f(s n))`) THEN
  53     EXISTS_TAC `s:num->A` THEN ASM_REWRITE_TAC[] THEN
  54     SUBGOAL_THEN `!n. P(s n) /\ s(SUC n):A << s(n)`
  55       (fun th -> ASM_MESON_TAC[th]) THEN
  56     INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
  57     EXISTS_TAC `\y:A. ?n:num. y = s(n)` THEN REWRITE_TAC[] THEN
  58     ASM_MESON_TAC[]]);;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* Equivalent to just *uniqueness* part of recursion.                        *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 let WF_UREC = prove
  65  (`WF(<<) ==>
  66        !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
  67             ==> !(f:A->B) g. (!x. f x = H f x) /\ (!x. g x = H g x)
  68                               ==> (f = g)`,
  69   REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
  70   FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
  71   DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[]);;
  72
  73 let WF_UREC_WF = prove
  74  (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
  75         ==> !(f:A->bool) g. (!x. f x = H f x) /\ (!x. g x = H g x)
  76                           ==> (f = g))
  77    ==> WF(<<)`,
  78   REWRITE_TAC[WF_IND] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
  79   FIRST_X_ASSUM(MP_TAC o SPEC `\f x. P(x:A) \/ !z:A. z << x ==> f(z)`) THEN
  80   REWRITE_TAC[] THEN
  81   W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
  82    [MESON_TAC[]; DISCH_THEN(MP_TAC o SPECL [`P:A->bool`; `\x:A. T`]) THEN
  83     REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]]);;
  84
  85 (* ------------------------------------------------------------------------- *)
  86 (* Stronger form of recursion with "inductive invariant" (Krstic/Matthews).  *)
  87 (* ------------------------------------------------------------------------- *)
  88
  89 let WF_REC_INVARIANT = prove
  90  (`WF(<<)
  91    ==> !H S. (!f g x. (!z. z << x ==> (f z = g z) /\ S z (f z))
  92                       ==> (H f x = H g x) /\ S x (H f x))
  93              ==> ?f:A->B. !x. (f x = H f x)`,
  94   let lemma = prove_inductive_relations_exist
  95     `!f:A->B x. (!z. z << x ==> R z (f z)) ==> R x (H f x)` in
  96   REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
  97   X_CHOOSE_THEN `R:A->B->bool` STRIP_ASSUME_TAC lemma THEN
  98   SUBGOAL_THEN `!x:A. ?!y:B. R x y` (fun th -> ASM_MESON_TAC[th]) THEN
  99   FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT STRIP_TAC THEN
 100   FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [th]) THEN
 101   SUBGOAL_THEN `!x:A y:B. R x y ==> S x y` MP_TAC THEN ASM_MESON_TAC[]);;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* Equivalent to just *existence* part of recursion.                         *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 let WF_REC = prove
 108  (`WF(<<)
 109    ==> !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
 110            ==> ?f:A->B. !x. f x = H f x`,
 111   REPEAT STRIP_TAC THEN
 112   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC_INVARIANT) THEN
 113   EXISTS_TAC `\x:A y:B. T` THEN ASM_REWRITE_TAC[]);;
 114
 115 let WF_REC_WF = prove
 116  (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
 117                  ==> ?f:A->num. !x. f x = H f x)
 118    ==> WF(<<)`,
 119   DISCH_TAC THEN REWRITE_TAC[WF_DCHAIN] THEN
 120   DISCH_THEN(X_CHOOSE_TAC `x:num->A`) THEN
 121   SUBGOAL_THEN `!n. (x:num->A)(@m. x(m) << x(n)) << x(n)` ASSUME_TAC THENL
 122    [CONV_TAC(BINDER_CONV SELECT_CONV) THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 123   FIRST_ASSUM(MP_TAC o SPEC
 124    `\f:A->num. \y:A. if ?p:num. y = x(p)
 125                      then SUC(f(x(@m. x(m) << y)))
 126                      else 0`) THEN
 127   REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
 128    [REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
 129     FIRST_ASSUM(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
 130     AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 131     FIRST_ASSUM MATCH_ACCEPT_TAC; ALL_TAC] THEN
 132   DISCH_THEN(X_CHOOSE_THEN `f:A->num` MP_TAC) THEN
 133   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `(x:num->A) n`) THEN
 134   SUBGOAL_THEN `!n. ?p. (x:num->A) n = x p` (fun th -> REWRITE_TAC[th]) THENL
 135    [MESON_TAC[]; DISCH_TAC] THEN
 136   SUBGOAL_THEN `!n:num. ?k. f(x(k):A) < f(x(n))` ASSUME_TAC THENL
 137    [GEN_TAC THEN EXISTS_TAC `@m:num. x(m):A << x(n)` THEN
 138     FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [th]) THEN REWRITE_TAC[LT];
 139     MP_TAC(SPEC `\n:num. ?i:num. n = f(x(i):A)` num_WOP) THEN
 140     REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;
 141
 142 (* ------------------------------------------------------------------------- *)
 143 (* Combine the two versions of the recursion theorem.                        *)
 144 (* ------------------------------------------------------------------------- *)
 145
 146 let WF_EREC = prove
 147  (`WF(<<) ==>
 148        !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
 149             ==> ?!f:A->B. !x. f x = H f x`,
 150   MESON_TAC[WF_REC; WF_UREC]);;
 151
 152 (* ------------------------------------------------------------------------- *)
 153 (* Some preservation theorems for wellfoundedness.                           *)
 154 (* ------------------------------------------------------------------------- *)
 155
 156 parse_as_infix("<<<",(12,"right"));;
 157
 158 let WF_SUBSET = prove
 159  (`(!(x:A) y. x << y ==> x <<< y) /\ WF(<<<) ==> WF(<<)`,
 160   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[WF] THEN
 161   DISCH_TAC THEN GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 162   UNDISCH_TAC `!(x:A) (y:A). x << y ==> x <<< y` THEN MESON_TAC[]);;
 163
 164 let WF_MEASURE_GEN = prove
 165  (`!m:A->B. WF(<<) ==> WF(\x x'. m x << m x')`,
 166   GEN_TAC THEN REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
 167   FIRST_ASSUM(MP_TAC o SPEC `\y:B. !x:A. (m(x) = y) ==> P x`) THEN
 168   UNDISCH_TAC `!x. (!y. (m:A->B) y << m x ==> P y) ==> P x` THEN
 169   REWRITE_TAC[] THEN MESON_TAC[]);;
 170
 171 let WF_LEX_DEPENDENT = prove
 172  (`!R:A->A->bool S:A->B->B->bool. WF(R) /\ (!a. WF(S a))
 173          ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S r1 s1 s2)`,
 174   REPEAT GEN_TAC THEN REWRITE_TAC[WF] THEN STRIP_TAC THEN
 175   X_GEN_TAC `P:A#B->bool` THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 176   GEN_REWRITE_TAC I [FORALL_PAIR_THM] THEN
 177   MAP_EVERY X_GEN_TAC [`a0:A`; `b0:B`] THEN DISCH_TAC THEN
 178   FIRST_X_ASSUM(MP_TAC o SPEC `\a:A. ?b:B. P(a,b)`) THEN
 179   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 180   DISCH_THEN(MP_TAC o SPECL [`a0:A`; `b0:B`]) THEN ASM_REWRITE_TAC[] THEN
 181   DISCH_THEN(X_CHOOSE_THEN `a:A` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
 182   DISCH_THEN(X_CHOOSE_TAC `b1:B`) THEN
 183   FIRST_X_ASSUM(MP_TAC o SPECL [`a:A`; `\b. (P:A#B->bool) (a,b)`]) THEN
 184   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 185   DISCH_THEN(MP_TAC o SPEC `b1:B`) THEN ASM_REWRITE_TAC[] THEN
 186   DISCH_THEN(X_CHOOSE_THEN `b:B` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
 187   DISCH_TAC THEN EXISTS_TAC `(a:A,b:B)` THEN ASM_REWRITE_TAC[] THEN
 188   REWRITE_TAC[FORALL_PAIR_THM] THEN ASM_MESON_TAC[]);;
 189
 190 let WF_LEX = prove
 191  (`!R:A->A->bool S:B->B->bool. WF(R) /\ WF(S)
 192          ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S s1 s2)`,
 193   SIMP_TAC[WF_LEX_DEPENDENT; ETA_AX]);;
 194
 195 let WF_POINTWISE = prove
 196  (`WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool)
 197    ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)`,
 198   STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL WF_SUBSET) THEN EXISTS_TAC
 199    `\(x1,y1) (x2,y2). x1 << x2 \/ (x1:A = x2) /\ (y1:B) <<< (y2:B)` THEN
 200   CONJ_TAC THENL
 201    [REWRITE_TAC[FORALL_PAIR_THM] THEN CONV_TAC TAUT;
 202     MATCH_MP_TAC WF_LEX THEN ASM_REWRITE_TAC[]]);;
 203
 204 (* ------------------------------------------------------------------------- *)
 205 (* Wellfoundedness properties of natural numbers.                            *)
 206 (* ------------------------------------------------------------------------- *)
 207
 208 let WF_num = prove
 209  (`WF(<)`,
 210   REWRITE_TAC[WF_IND; num_WF]);;
 211
 212 let WF_REC_num = prove
 213  (`!H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
 214         ==> ?f:num->A. !n. f n = H f n`,
 215   MATCH_ACCEPT_TAC(MATCH_MP WF_REC WF_num));;
 216
 217 (* ------------------------------------------------------------------------- *)
 218 (* Natural number measures (useful in program verification).                 *)
 219 (* ------------------------------------------------------------------------- *)
 220
 221 let MEASURE = new_definition
 222   `MEASURE m = \x y. m(x) < m(y)`;;
 223
 224 let WF_MEASURE = prove
 225  (`!m:A->num. WF(MEASURE m)`,
 226   REPEAT GEN_TAC THEN REWRITE_TAC[MEASURE] THEN
 227   MATCH_MP_TAC WF_MEASURE_GEN THEN
 228   MATCH_ACCEPT_TAC WF_num);;
 229
 230 let MEASURE_LE = prove
 231  (`(!y. MEASURE m y a ==> MEASURE m y b) <=> m(a) <= m(b)`,
 232     REWRITE_TAC[MEASURE] THEN MESON_TAC[NOT_LE; LTE_TRANS; LT_REFL]);;
 233
 234 (* ------------------------------------------------------------------------- *)
 235 (* Trivially, a WF relation is irreflexive.                                  *)
 236 (* ------------------------------------------------------------------------- *)
 237
 238 let WF_REFL = prove
 239  (`!x:A. WF(<<) ==> ~(x << x)`,
 240   GEN_TAC THEN REWRITE_TAC[WF] THEN
 241   DISCH_THEN(MP_TAC o SPEC `\y:A. y = x`) THEN
 242   REWRITE_TAC[] THEN MESON_TAC[]);;
 243
 244 (* ------------------------------------------------------------------------- *)
 245 (* Even more trivially, the everywhere-false relation is wellfounded.        *)
 246 (* ------------------------------------------------------------------------- *)
 247
 248 let WF_FALSE = prove
 249  (`WF(\x y:A. F)`,
 250   REWRITE_TAC[WF]);;
 251
 252 (* ------------------------------------------------------------------------- *)
 253 (* Tail recursion.                                                           *)
 254 (* ------------------------------------------------------------------------- *)
 255
 256 let WF_REC_TAIL = prove
 257  (`!P g h. ?f:A->B. !x. f x = if P(x) then f(g x) else h x`,
 258   let lemma1 = prove
 259    (`~(P 0) ==> ((?n. P(SUC n)) <=> (?n. P(n)))`,
 260     MESON_TAC[num_CASES; NOT_SUC])
 261   and lemma2 = prove
 262    (`(P 0) ==> ((!m. m < n ==> P(SUC m)) <=> (!m. m < SUC n ==> P(m)))`,
 263     REPEAT(DISCH_TAC ORELSE EQ_TAC) THEN INDUCT_TAC THEN
 264     ASM_MESON_TAC[LT_SUC; LT_0]) in
 265   REPEAT GEN_TAC THEN
 266   MP_TAC(GEN `x:A` (ISPECL [`x:A`; `\y:A n:num. g(y):A`] num_RECURSION)) THEN
 267   REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
 268   DISCH_THEN(X_CHOOSE_THEN `s:A->num->A` STRIP_ASSUME_TAC) THEN
 269   EXISTS_TAC `\x:A. if ?n:num. ~P(s x n)
 270                     then (h:A->B)(@y. ?n. (y = s x n) /\ ~P(s x n) /\
 271                                           !m. m < n ==> P(s x m))
 272                     else something_arbitrary:B` THEN
 273   X_GEN_TAC `x:A` THEN
 274   SUBGOAL_THEN `!n x:A. s (g x) n :A = s x (SUC n)` ASSUME_TAC THENL
 275    [INDUCT_TAC THEN ASM_REWRITE_TAC[];
 276     UNDISCH_THEN `!x:A n. s x (SUC n) :A = g (s x n)` (K ALL_TAC)] THEN
 277   ASM_CASES_TAC `(P:A->bool) x` THEN ASM_REWRITE_TAC[] THENL
 278    [ASM_SIMP_TAC[lemma1] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 279     CONV_TAC SYM_CONV THEN ASM_SIMP_TAC[lemma2; lemma1];
 280     COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 281     AP_TERM_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 282     REWRITE_TAC[] THEN X_GEN_TAC `y:A` THEN EQ_TAC THENL
 283      [SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 284       INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LT_0];
 285       ASM_MESON_TAC[LT]]]);;
 286
 287 (* ------------------------------------------------------------------------- *)
 288 (* A more general mix of tail and wellfounded recursion.                     *)
 289 (* ------------------------------------------------------------------------- *)
 290
 291 let WF_REC_TAIL_GENERAL = prove
 292  (`!P G H. WF(<<) /\
 293            (!f g x. (!z. z << x ==> (f z = g z))
 294                     ==> (P f x <=> P g x) /\ G f x = G g x /\ H f x = H g x) /\
 295            (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x)) /\
 296            (!f x y. P f x /\ y << G f x ==> y << x)
 297            ==> ?f:A->B. !x. f x = if P f x then f(G f x) else H f x`,
 298   REPEAT STRIP_TAC THEN
 299   CHOOSE_THEN MP_TAC
 300    (prove_inductive_relations_exist
 301      `(!x:A. ~(P f x) ==> terminates f x) /\
 302       (!x. P (f:A->B) x /\ terminates f (G f x) ==> terminates f x)`) THEN
 303   REWRITE_TAC[FORALL_AND_THM] THEN
 304   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 305   SUBGOAL_THEN
 306    `?while. !f:A->B x:A. while f x = if P f x then while f (G f x) else x`
 307    (STRIP_ASSUME_TAC o GSYM)
 308   THENL [REWRITE_TAC[GSYM SKOLEM_THM; WF_REC_TAIL]; ALL_TAC] THEN
 309   SUBGOAL_THEN
 310    `?f:A->B. !x. f x = if terminates f x then H f (while f x :A) else anything`
 311   MP_TAC THENL
 312    [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC) THEN
 313     REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[]
 314      `(a = b) /\ (a /\ b ==> (x = y) /\ (f x = g x))
 315       ==> ((if a then f x else d) = (if b then g y else d))`) THEN
 316     REPEAT STRIP_TAC THENL
 317      [SUBGOAL_THEN
 318        `!f g x.
 319            (!x y. P f x /\ y << G (f:A->B) x ==> y << x) /\
 320            (!y:A. (!z:A. z << y ==> z << x)
 321                   ==> (P f y = P g y) /\ (G f y = G g y))
 322                ==> terminates f x ==> terminates g x`
 323        (fun th -> EQ_TAC THEN MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
 324       GEN_TAC THEN GEN_TAC THEN
 325       REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN DISCH_TAC THEN
 326       ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
 327       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
 328       SUBGOAL_THEN
 329        `!x:A. terminates (f:A->B) x /\
 330               (!y:A. (!z:A. z << y ==> z << x)
 331                      ==> (P f y <=> P g y) /\ (G f y :A = G g y))
 332               ==> (while f x :A = while g x)`
 333        (fun th -> MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
 334       REWRITE_TAC[IMP_CONJ] THEN
 335       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
 336       FIRST_X_ASSUM MATCH_MP_TAC THEN
 337       SUBGOAL_THEN
 338        `!f:A->B. (!x:A y:A. P f x /\ y << G f x ==> y << x)
 339          ==> !x. terminates f x ==> !y. y << while f x ==> y << x`
 340        (fun th -> ASM_MESON_TAC[th]) THEN
 341       GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 342       ASM_MESON_TAC[]];
 343     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
 344     DISCH_THEN(fun th -> ASSUME_TAC(GSYM th) THEN MP_TAC th) THEN
 345     MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:A` THEN
 346     ASM_CASES_TAC `P (f:A->B) (x:A) :bool` THEN ASM_MESON_TAC[]]);;
 347
 348 (* ------------------------------------------------------------------------- *)
 349 (* Tactic to apply WF induction on a free "measured" term in the goal.       *)
 350 (* ------------------------------------------------------------------------- *)
 351
 352 let WF_INDUCT_TAC =
 353   let qqconv =
 354     let pth = prove
 355      (`(!x. P x ==> !y. Q x y) <=> !y x. P x ==> Q x y`, MESON_TAC[]) in
 356     GEN_REWRITE_CONV I [pth]
 357   and eqconv =
 358     let pth = prove
 359      (`(!m. P m ==> (m = e) ==> Q) <=> (P e ==> Q)`, MESON_TAC[]) in
 360     REWR_CONV pth in
 361   let rec qqconvs tm =
 362     try (qqconv THENC BINDER_CONV qqconvs) tm
 363     with Failure _ -> eqconv tm in
 364   fun tm (asl,w as gl) ->
 365     let fvs = frees tm
 366     and gv = genvar(type_of tm) in
 367     let pat = list_mk_forall(gv::fvs,mk_imp(mk_eq(gv,tm),w)) in
 368     let th0 = UNDISCH(PART_MATCH rand num_WF pat) in
 369     let th1 = MP (SPECL (tm::fvs) th0) (REFL tm) in
 370     let th2 = CONV_RULE(LAND_CONV qqconvs) (DISCH_ALL th1) in
 371     (MATCH_MP_TAC th2 THEN MAP_EVERY X_GEN_TAC fvs THEN
 372      CONV_TAC(LAND_CONV qqconvs) THEN DISCH_THEN ASSUME_TAC) gl;;