Arithmetic/derived.ml

   1 (* ========================================================================= *)
   2 (* Derived properties of provability.                                        *)
   3 (* ========================================================================= *)
   4
   5 let negativef = new_definition
   6   `negativef p = ?q. p = q --> False`;;
   7
   8 let negatef = new_definition
   9   `negatef p = if negativef p then @q. p = q --> False else p --> False`;;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* The primitive basis, separated into its named components.                 *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let axiom_addimp = prove
  16  (`!A p q. A |-- p --> (q --> p)`,
  17   MESON_TAC[proves_RULES; axiom_RULES]);;
  18
  19 let axiom_distribimp = prove
  20  (`!A p q r. A |-- (p --> q --> r) --> (p --> q) --> (p --> r)`,
  21   MESON_TAC[proves_RULES; axiom_RULES]);;
  22
  23 let axiom_doubleneg = prove
  24  (`!A p. A |-- ((p --> False) --> False) --> p`,
  25   MESON_TAC[proves_RULES; axiom_RULES]);;
  26
  27 let axiom_allimp = prove
  28  (`!A x p q. A |-- (!!x (p --> q)) --> (!!x p) --> (!!x q)`,
  29   MESON_TAC[proves_RULES; axiom_RULES]);;
  30
  31 let axiom_impall = prove
  32  (`!A x p. ~(x IN FV p) ==> A |-- p --> !!x p`,
  33   MESON_TAC[proves_RULES; axiom_RULES]);;
  34
  35 let axiom_existseq = prove
  36  (`!A x t. ~(x IN FVT t) ==> A |-- ??x (V x === t)`,
  37   MESON_TAC[proves_RULES; axiom_RULES]);;
  38
  39 let axiom_eqrefl = prove
  40  (`!A t. A |-- t === t`,
  41   MESON_TAC[proves_RULES; axiom_RULES]);;
  42
  43 let axiom_funcong = prove
  44  (`(!A s t. A |-- s === t --> Suc s === Suc t) /\
  45    (!A s t u v. A |-- s === t --> u === v --> s ++ u === t ++ v) /\
  46    (!A s t u v. A |-- s === t --> u === v --> s ** u === t ** v)`,
  47   MESON_TAC[proves_RULES; axiom_RULES]);;
  48
  49 let axiom_predcong = prove
  50  (`(!A s t u v. A |-- s === t --> u === v --> s === u --> t === v) /\
  51    (!A s t u v. A |-- s === t --> u === v --> s << u --> t << v) /\
  52    (!A s t u v. A |-- s === t --> u === v --> s <<= u --> t <<= v)`,
  53   MESON_TAC[proves_RULES; axiom_RULES]);;
  54
  55 let axiom_iffimp1 = prove
  56  (`!A p q. A |-- (p <-> q) --> p --> q`,
  57   MESON_TAC[proves_RULES; axiom_RULES]);;
  58
  59 let axiom_iffimp2 = prove
  60  (`!A p q. A |-- (p <-> q) --> q --> p`,
  61   MESON_TAC[proves_RULES; axiom_RULES]);;
  62
  63 let axiom_impiff = prove
  64  (`!A p q. A |-- (p --> q) --> (q --> p) --> (p <-> q)`,
  65   MESON_TAC[proves_RULES; axiom_RULES]);;
  66
  67 let axiom_true = prove
  68  (`A |-- True <-> (False --> False)`,
  69   MESON_TAC[proves_RULES; axiom_RULES]);;
  70
  71 let axiom_not = prove
  72  (`!A p. A |-- Not p <-> (p --> False)`,
  73   MESON_TAC[proves_RULES; axiom_RULES]);;
  74
  75 let axiom_and = prove
  76  (`!A p q. A |-- (p && q) <-> (p --> q --> False) --> False`,
  77   MESON_TAC[proves_RULES; axiom_RULES]);;
  78
  79 let axiom_or = prove
  80  (`!A p q. A |-- (p || q) <-> Not(Not p && Not q)`,
  81   MESON_TAC[proves_RULES; axiom_RULES]);;
  82
  83 let axiom_exists = prove
  84  (`!A x p. A |-- (??x p) <-> Not(!!x (Not p))`,
  85   MESON_TAC[proves_RULES; axiom_RULES]);;
  86
  87 let assume = prove
  88  (`!A p. p IN A ==> A |-- p`,
  89   MESON_TAC[proves_RULES]);;
  90
  91 let modusponens = prove
  92  (`!A p. A |-- (p --> q) /\ A |-- p ==> A |-- q`,
  93   MESON_TAC[proves_RULES]);;
  94
  95 let gen = prove
  96  (`!A p x. A |-- p ==> A |-- !!x p`,
  97   MESON_TAC[proves_RULES]);;
  98
  99 (* ------------------------------------------------------------------------- *)
 100 (* Some purely propositional schemas and derived rules.                      *)
 101 (* ------------------------------------------------------------------------- *)
 102
 103 let iff_imp1 = prove
 104  (`!A p q. A |-- p <-> q ==> A |-- p --> q`,
 105   MESON_TAC[modusponens; axiom_iffimp1]);;
 106
 107 let iff_imp2 = prove
 108  (`!A p q. A |-- p <-> q ==> A |-- q --> p`,
 109   MESON_TAC[modusponens; axiom_iffimp2]);;
 110
 111 let imp_antisym = prove
 112  (`!A p q. A |-- p --> q /\ A |-- q --> p ==> A |-- p <-> q`,
 113   MESON_TAC[modusponens; axiom_impiff]);;
 114
 115 let add_assum = prove
 116  (`!A p q. A |-- q ==> A |-- p --> q`,
 117   MESON_TAC[modusponens; axiom_addimp]);;
 118
 119 let imp_refl = prove
 120  (`!A p. A |-- p --> p`,
 121   MESON_TAC[modusponens; axiom_distribimp; axiom_addimp]);;
 122
 123 let imp_add_assum = prove
 124  (`!A p q r. A |-- q --> r ==> A |-- (p --> q) --> (p --> r)`,
 125   MESON_TAC[modusponens; axiom_distribimp; add_assum]);;
 126
 127 let imp_unduplicate = prove
 128  (`!A p q. A |-- p --> p --> q ==> A |-- p --> q`,
 129   MESON_TAC[modusponens; axiom_distribimp; imp_refl]);;
 130
 131 let imp_trans = prove
 132  (`!A p q. A |-- p --> q /\ A |-- q --> r ==> A |-- p --> r`,
 133   MESON_TAC[modusponens; imp_add_assum]);;
 134
 135 let imp_swap = prove
 136  (`!A p q r. A |-- p --> q --> r ==> A |-- q --> p --> r`,
 137   MESON_TAC[imp_trans; axiom_addimp; modusponens; axiom_distribimp]);;
 138
 139 let imp_trans_chain_2 = prove
 140  (`!A p q1 q2 r. A |-- p --> q1 /\ A |-- p --> q2 /\ A |-- q1 --> q2 --> r
 141                  ==> A |-- p --> r`,
 142   ASM_MESON_TAC[imp_trans; imp_swap; imp_unduplicate]);;
 143
 144 let imp_trans_th = prove
 145  (`!A p q r. A |-- (q --> r) --> (p --> q) --> (p --> r)`,
 146   MESON_TAC[imp_trans; axiom_addimp; axiom_distribimp]);;
 147
 148 let imp_add_concl = prove
 149  (`!A p q r. A |-- p --> q ==> A |-- (q --> r) --> (p --> r)`,
 150   MESON_TAC[modusponens; imp_swap; imp_trans_th]);;
 151
 152 let imp_trans2 = prove
 153  (`!A p q r s. A |-- p --> q --> r /\ A |-- r --> s ==> A |-- p --> q --> s`,
 154   MESON_TAC[imp_add_assum; modusponens; imp_trans_th]);;
 155
 156 let imp_swap_th = prove
 157  (`!A p q r. A |-- (p --> q --> r) --> (q --> p --> r)`,
 158   MESON_TAC[imp_trans; axiom_distribimp; imp_add_concl; axiom_addimp]);;
 159
 160 let contrapos = prove
 161  (`!A p q. A |-- p --> q ==> A |-- Not q --> Not p`,
 162   MESON_TAC[imp_trans; iff_imp1; axiom_not; imp_add_concl; iff_imp2]);;
 163
 164 let imp_truefalse = prove
 165  (`!p q. A |-- (q --> False) --> p --> (p --> q) --> False`,
 166   MESON_TAC[imp_trans; imp_trans_th; imp_swap_th]);;
 167
 168 let imp_insert = prove
 169  (`!A p q r. A |-- p --> r ==> A |-- p --> q --> r`,
 170   MESON_TAC[imp_trans; axiom_addimp]);;
 171
 172 let imp_mono_th = prove
 173  (`A |-- (p' --> p) --> (q --> q') --> (p --> q) --> (p' --> q')`,
 174   MESON_TAC[imp_trans; imp_swap; imp_trans_th]);;
 175
 176 let ex_falso = prove
 177  (`!A p. A |-- False --> p`,
 178   MESON_TAC[imp_trans; axiom_addimp; axiom_doubleneg]);;
 179
 180 let imp_contr = prove
 181  (`!A p q. A |-- (p --> False) --> (p --> r)`,
 182   MESON_TAC[imp_add_assum; ex_falso]);;
 183
 184 let imp_contrf = prove
 185  (`!A p r. A |-- p --> negatef p --> r`,
 186   REPEAT GEN_TAC THEN REWRITE_TAC[negatef; negativef] THEN
 187   COND_CASES_TAC THEN POP_ASSUM STRIP_ASSUME_TAC THEN
 188   ASM_REWRITE_TAC[form_INJ] THEN
 189   ASM_MESON_TAC[imp_contr; imp_swap]);;
 190
 191 let contrad = prove
 192  (`!A p. A |-- (p --> False) --> p ==> A |-- p`,
 193   MESON_TAC[modusponens; axiom_distribimp; imp_refl; axiom_doubleneg]);;
 194
 195 let bool_cases = prove
 196  (`!p q. A |-- p --> q /\ A |-- (p --> False) --> q ==> A |-- q`,
 197   MESON_TAC[contrad; imp_trans; imp_add_concl]);;
 198
 199 let imp_false_rule = prove
 200  (`!p q r. A |-- (q --> False) --> p --> r
 201            ==> A |-- ((p --> q) --> False) --> r`,
 202   MESON_TAC[imp_add_concl; imp_add_assum; ex_falso; axiom_addimp; imp_swap;
 203             imp_trans; axiom_doubleneg; imp_unduplicate]);;
 204
 205 let imp_true_rule = prove
 206  (`!A p q r. A |-- (p --> False) --> r /\ A |-- q --> r
 207              ==> A |-- (p --> q) --> r`,
 208   MESON_TAC[imp_insert; imp_swap; modusponens; imp_trans_th; bool_cases]);;
 209
 210 let truth = prove
 211  (`!A. A |-- True`,
 212   MESON_TAC[modusponens; axiom_true; imp_refl; iff_imp2]);;
 213
 214 let and_left = prove
 215  (`!A p q. A |-- p && q --> p`,
 216   MESON_TAC[imp_add_assum; axiom_addimp; imp_trans; imp_add_concl;
 217             axiom_doubleneg; imp_trans; iff_imp1; axiom_and]);;
 218
 219 let and_right = prove
 220  (`!A p q. A |-- p && q --> q`,
 221   MESON_TAC[axiom_addimp; imp_trans; imp_add_concl; axiom_doubleneg;
 222             iff_imp1; axiom_and]);;
 223
 224 let and_pair = prove
 225  (`!A p q. A |-- p --> q --> p && q`,
 226   MESON_TAC[iff_imp2; axiom_and; imp_swap_th; imp_add_assum; imp_trans2;
 227             modusponens; imp_swap; imp_refl]);;
 228
 229 let META_AND = prove
 230  (`!A p q. A |-- p && q <=> A |-- p /\ A |-- q`,
 231   MESON_TAC[and_left; and_right; and_pair; modusponens]);;
 232
 233 let shunt = prove
 234  (`!A p q r. A |-- p && q --> r ==> A |-- p --> q --> r`,
 235   MESON_TAC[modusponens; imp_add_assum; and_pair]);;
 236
 237 let ante_conj = prove
 238  (`!A p q r. A |-- p --> q --> r ==> A |-- p && q --> r`,
 239   MESON_TAC[imp_trans_chain_2; and_left; and_right]);;
 240
 241 let not_not_false = prove
 242  (`!A p. A |-- (p --> False) --> False <-> p`,
 243   MESON_TAC[imp_antisym; axiom_doubleneg; imp_swap; imp_refl]);;
 244
 245 let iff_sym = prove
 246  (`!A p q. A |-- p <-> q <=> A |-- q <-> p`,
 247   MESON_TAC[iff_imp1; iff_imp2; imp_antisym]);;
 248
 249 let iff_trans = prove
 250  (`!A p q r. A |-- p <-> q /\ A |-- q <-> r ==> A |-- p <-> r`,
 251   MESON_TAC[iff_imp1; iff_imp2; imp_trans; imp_antisym]);;
 252
 253 let not_not = prove
 254  (`!A p. A |-- Not(Not p) <-> p`,
 255   MESON_TAC[iff_trans; not_not_false; axiom_not; imp_antisym; imp_add_concl;
 256             iff_imp1; iff_imp2]);;
 257
 258 let contrapos_eq = prove
 259  (`!A p q. A |-- Not p --> Not q <=> A |-- q --> p`,
 260   MESON_TAC[contrapos; not_not; iff_imp1; iff_imp2; imp_trans]);;
 261
 262 let or_left = prove
 263  (`!A p q. A |-- q --> p || q`,
 264   MESON_TAC[imp_trans; not_not; iff_imp2; and_right; contrapos; axiom_or]);;
 265
 266 let or_right = prove
 267  (`!A p q. A |-- p --> p || q`,
 268   MESON_TAC[imp_trans; not_not; iff_imp2; and_left; contrapos; axiom_or]);;
 269
 270 let ante_disj = prove
 271  (`!A p q r. A |-- p --> r /\ A |-- q --> r
 272              ==> A |-- p || q --> r`,
 273   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM contrapos_eq] THEN
 274   MESON_TAC[imp_trans; imp_trans_chain_2; and_pair; contrapos_eq; not_not;
 275             axiom_or; iff_imp1; iff_imp2; imp_trans]);;
 276
 277 let iff_def = prove
 278  (`!A p q. A |-- (p <-> q) <-> (p --> q) && (q --> p)`,
 279   MESON_TAC[imp_antisym; imp_trans_chain_2; axiom_iffimp1; axiom_iffimp2;
 280             and_pair; axiom_impiff; imp_trans_chain_2; and_left; and_right]);;
 281
 282 let iff_refl = prove
 283  (`!A p. A |-- p <-> p`,
 284   MESON_TAC[imp_antisym; imp_refl]);;
 285
 286 (* ------------------------------------------------------------------------- *)
 287 (* Equality rules.                                                           *)
 288 (* ------------------------------------------------------------------------- *)
 289
 290 let eq_sym = prove
 291  (`!A s t. A |-- s === t --> t === s`,
 292   MESON_TAC[axiom_eqrefl; modusponens; imp_swap; axiom_predcong]);;
 293
 294 let icongruence_general = prove
 295  (`!A p x s t tm.
 296      A |-- s === t -->
 297            termsubst ((x |-> s) v) tm === termsubst ((x |-> t) v) tm`,
 298   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 299   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[termsubst] THEN
 300   REPEAT CONJ_TAC THENL
 301    [MESON_TAC[axiom_eqrefl; add_assum];
 302     GEN_TAC THEN REWRITE_TAC[valmod] THEN
 303     COND_CASES_TAC THEN REWRITE_TAC[imp_refl] THEN
 304     MESON_TAC[axiom_eqrefl; add_assum];
 305     MESON_TAC[imp_trans; axiom_funcong];
 306     MESON_TAC[imp_trans; axiom_funcong; imp_swap; imp_unduplicate];
 307     MESON_TAC[imp_trans; axiom_funcong; imp_swap; imp_unduplicate]]);;
 308
 309 let icongruence = prove
 310  (`!A x s t tm.
 311      A |-- s === t --> termsubst (x |=> s) tm === termsubst (x |=> t) tm`,
 312   REWRITE_TAC[assign; icongruence_general]);;
 313
 314 let icongruence_var = prove
 315  (`!A x t tm.
 316      A |-- V x === t --> tm === termsubst (x |=> t) tm`,
 317   MESON_TAC[icongruence; TERMSUBST_TRIV; ASSIGN_TRIV]);;
 318
 319 (* ------------------------------------------------------------------------- *)
 320 (* First-order rules.                                                        *)
 321 (* ------------------------------------------------------------------------- *)
 322
 323 let gen_right = prove
 324  (`!A x p q. ~(x IN FV(p)) /\ A |-- p --> q
 325              ==> A |-- p --> !!x q`,
 326   MESON_TAC[axiom_allimp; modusponens; gen; imp_trans; axiom_impall]);;
 327
 328 let genimp = prove
 329  (`!x p q. A |-- p --> q ==> A |-- (!!x p) --> (!!x q)`,
 330   MESON_TAC[modusponens; axiom_allimp; gen]);;
 331
 332 let eximp = prove
 333  (`!x p q. A |-- p --> q ==> A |-- (??x p) --> (??x q)`,
 334   MESON_TAC[contrapos; genimp; contrapos; imp_trans; iff_imp1; iff_imp2;
 335             axiom_exists]);;
 336
 337 let exists_imp = prove
 338  (`!A x p q. A |-- ??x (p --> q) /\ ~(x IN FV(q)) ==> A |-- (!!x p) --> q`,
 339   REPEAT STRIP_TAC THEN
 340   SUBGOAL_THEN `A |-- (q --> False) --> !!x (p --> Not(p --> q))`
 341   ASSUME_TAC THENL
 342    [MATCH_MP_TAC gen_right THEN
 343     ASM_REWRITE_TAC[FV; IN_UNION; NOT_IN_EMPTY] THEN
 344     ASM_MESON_TAC[iff_imp2; axiom_not; imp_trans2; imp_truefalse];
 345     ALL_TAC] THEN
 346   SUBGOAL_THEN `A |-- (q --> False) --> !!x p --> !!x (Not(p --> q))`
 347   ASSUME_TAC THENL
 348    [ASM_MESON_TAC[imp_trans; axiom_allimp]; ALL_TAC] THEN
 349   SUBGOAL_THEN `A |-- ((q --> False) --> !!x (Not(p --> q)))
 350                       --> (q --> False) --> False`
 351   ASSUME_TAC THENL
 352    [ASM_MESON_TAC[modusponens; iff_imp1; axiom_exists; axiom_not; imp_trans_th];
 353     ALL_TAC] THEN
 354   ASM_MESON_TAC[imp_trans; imp_swap; axiom_doubleneg]);;
 355
 356 let subspec = prove
 357  (`!A x t p q. ~(x IN FVT(t)) /\ ~(x IN FV(q)) /\ A |-- V x === t --> p --> q
 358                ==> A |-- (!!x p) --> q`,
 359   MESON_TAC[exists_imp; modusponens; eximp; axiom_existseq]);;
 360
 361 let subalpha = prove
 362  (`!A x y p q. ((x = y) \/ ~(x IN FV(q)) /\ ~(y IN FV(p))) /\
 363                A |-- V x === V y --> p --> q
 364                ==> A |-- (!!x p) --> (!!y q)`,
 365   REPEAT GEN_TAC THEN ASM_CASES_TAC `x = y:num` THEN ASM_REWRITE_TAC[] THEN
 366   STRIP_TAC THENL
 367    [FIRST_X_ASSUM SUBST_ALL_TAC THEN
 368     ASM_MESON_TAC[genimp; modusponens; axiom_eqrefl];
 369     ALL_TAC] THEN
 370   MATCH_MP_TAC gen_right THEN ASM_REWRITE_TAC[FV; IN_DELETE] THEN
 371   MATCH_MP_TAC subspec THEN EXISTS_TAC `V y` THEN
 372   ASM_REWRITE_TAC[FVT; IN_SING]);;
 373
 374 (* ------------------------------------------------------------------------- *)
 375 (* We'll perform induction on this measure.                                  *)
 376 (* ------------------------------------------------------------------------- *)
 377
 378 let complexity = new_recursive_definition form_RECURSION
 379   `(complexity False = 1) /\
 380    (complexity True = 1) /\
 381    (!s t. complexity (s === t) = 1) /\
 382    (!s t. complexity (s << t) = 1) /\
 383    (!s t. complexity (s <<= t) = 1) /\
 384    (!p. complexity (Not p) = complexity p + 3) /\
 385    (!p q. complexity (p && q) = complexity p + complexity q + 6) /\
 386    (!p q. complexity (p || q) = complexity p + complexity q + 16) /\
 387    (!p q. complexity (p --> q) = complexity p + complexity q + 1) /\
 388    (!p q. complexity (p <-> q) = 2 * (complexity p + complexity q) + 9) /\
 389    (!x p. complexity (!!x p) = complexity p + 1) /\
 390    (!x p. complexity (??x p) = complexity p + 8)`;;
 391
 392 let COMPLEXITY_FORMSUBST = prove
 393  (`!p i. complexity(formsubst i p) = complexity p`,
 394   MATCH_MP_TAC form_INDUCT THEN
 395   SIMP_TAC[formsubst; complexity; LET_DEF; LET_END_DEF]);;
 396
 397 let isubst_general = prove
 398  (`!A p x v s t. A |-- s === t
 399                        --> formsubst ((x |-> s) v) p
 400                            --> formsubst ((x |-> t) v) p`,
 401   GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `complexity p` THEN
 402   POP_ASSUM MP_TAC THEN SPEC_TAC(`p:form`,`p:form`) THEN
 403   MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[formsubst; complexity] THEN
 404   REPEAT CONJ_TAC THENL
 405    [MESON_TAC[imp_refl; add_assum];
 406     MESON_TAC[imp_refl; add_assum];
 407     MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
 408     MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
 409     MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
 410     X_GEN_TAC `p:form` THEN DISCH_THEN(K ALL_TAC) THEN
 411     DISCH_THEN(MP_TAC o SPEC `p --> False`) THEN
 412     REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 413     REWRITE_TAC[formsubst] THEN
 414     MESON_TAC[axiom_not; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
 415     MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 416     DISCH_THEN(MP_TAC o SPEC `(p --> q --> False) --> False`) THEN
 417     REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 418     REWRITE_TAC[formsubst] THEN
 419     MESON_TAC[axiom_and; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
 420     MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 421     DISCH_THEN(MP_TAC o SPEC `Not(Not p && Not q)`) THEN
 422     REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 423     REWRITE_TAC[formsubst] THEN
 424     MESON_TAC[axiom_or; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
 425     MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 426     DISCH_THEN(fun th -> MP_TAC(SPEC `p:form` th) THEN
 427                          MP_TAC(SPEC `q:form` th)) THEN
 428     REWRITE_TAC[ARITH_RULE `p < p + q + 1 /\ q < p + q + 1`] THEN
 429     MESON_TAC[imp_mono_th; eq_sym; imp_trans; imp_trans_chain_2];
 430     MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 431     DISCH_THEN(MP_TAC o SPEC `(p --> q) && (q --> p)`) THEN
 432     REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 433     REWRITE_TAC[formsubst] THEN
 434     MESON_TAC[iff_def; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
 435     ALL_TAC;
 436     MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 437     DISCH_THEN(MP_TAC o SPEC `Not(!!x (Not p))`) THEN
 438     REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 439     REWRITE_TAC[formsubst] THEN
 440     REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 441     REWRITE_TAC[FV] THEN REPEAT LET_TAC THEN
 442     ASM_MESON_TAC[axiom_exists; iff_imp1; iff_imp2; imp_swap; imp_trans;
 443                   imp_trans2]] THEN
 444   MAP_EVERY X_GEN_TAC [`u:num`; `p:form`] THEN DISCH_THEN(K ALL_TAC) THEN
 445   REWRITE_TAC[ARITH_RULE `a < b + 1 <=> a <= b`] THEN DISCH_TAC THEN
 446   MAP_EVERY X_GEN_TAC [`v:num`; `i:num->term`; `s:term`; `t:term`] THEN
 447   MAP_EVERY ABBREV_TAC
 448    [`x = if ?y. y IN FV (!! u p) /\ u IN FVT ((v |-> s) i y)
 449          then VARIANT (FV (formsubst ((u |-> V u) ((v |-> s) i)) p))
 450          else u`;
 451     `y = if ?y. y IN FV (!! u p) /\ u IN FVT ((v |-> t) i y)
 452          then VARIANT (FV (formsubst ((u |-> V u) ((v |-> t) i)) p))
 453          else u`] THEN
 454   REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
 455   SUBGOAL_THEN `~(x IN FV(formsubst ((v |-> s) i) (!!u p))) /\
 456                 ~(y IN FV(formsubst ((v |-> t) i) (!!u p)))`
 457   STRIP_ASSUME_TAC THENL
 458    [MAP_EVERY EXPAND_TAC ["x"; "y"] THEN CONJ_TAC THEN
 459     (COND_CASES_TAC THENL
 460        [ALL_TAC; ASM_REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM]] THEN
 461       MATCH_MP_TAC NOT_IN_VARIANT THEN REWRITE_TAC[FV_FINITE] THEN
 462       REWRITE_TAC[SUBSET; FORMSUBST_FV; IN_ELIM_THM; FV; IN_DELETE] THEN
 463       REWRITE_TAC[valmod] THEN MESON_TAC[FVT; IN_SING]);
 464     ALL_TAC] THEN
 465   ASM_CASES_TAC `v:num = u` THENL
 466    [ASM_REWRITE_TAC[VALMOD_VALMOD_BASIC] THEN
 467     MATCH_MP_TAC add_assum THEN MATCH_MP_TAC subalpha THEN
 468     ASM_SIMP_TAC[LE_REFL] THEN
 469     ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 470      [UNDISCH_TAC `~(x IN FV (formsubst ((v |-> s) i) (!! u p)))`;
 471       UNDISCH_TAC `~(y IN FV (formsubst ((v |-> t) i) (!! u p)))`] THEN
 472     ASM_REWRITE_TAC[FORMSUBST_FV; FV; IN_ELIM_THM; IN_DELETE] THEN
 473     MATCH_MP_TAC MONO_NOT THEN MATCH_MP_TAC MONO_EXISTS THEN
 474     X_GEN_TAC `w:num` THEN ASM_CASES_TAC `w:num = u` THEN
 475     ASM_REWRITE_TAC[VALMOD_BASIC; FVT; IN_SING] THEN
 476     ASM_REWRITE_TAC[valmod; FVT; IN_SING];
 477     ALL_TAC] THEN
 478   SUBGOAL_THEN
 479    `?z. ~(z IN FVT s) /\ ~(z IN FVT t) /\
 480         A |-- !!x (formsubst ((u |-> V x) ((v |-> s) i)) p)
 481               --> !!z (formsubst ((u |-> V z) ((v |-> s) i)) p) /\
 482         A |-- !!z (formsubst ((u |-> V z) ((v |-> t) i)) p)
 483               --> !!y (formsubst ((u |-> V y) ((v |-> t) i)) p)`
 484   MP_TAC THENL
 485    [ALL_TAC;
 486     DISCH_THEN(X_CHOOSE_THEN `z:num` STRIP_ASSUME_TAC) THEN
 487     MATCH_MP_TAC imp_trans THEN
 488     EXISTS_TAC `(!!z (formsubst ((v |-> s) ((u |-> V z) i)) p))
 489                      --> (!!z (formsubst ((v |-> t) ((u |-> V z) i)) p))` THEN
 490     CONJ_TAC THENL
 491      [MATCH_MP_TAC imp_trans THEN
 492       EXISTS_TAC `!!z (formsubst ((v |-> s) ((u |-> V z) i)) p
 493                        --> formsubst ((v |-> t) ((u |-> V z) i)) p)` THEN
 494       REWRITE_TAC[axiom_allimp] THEN
 495       ASM_SIMP_TAC[complexity; LE_REFL; FV; IN_UNION; gen_right];
 496       ALL_TAC] THEN
 497     FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP VALMOD_SWAP th]) THEN
 498     ASM_MESON_TAC[imp_mono_th; modusponens]] THEN
 499   MP_TAC(SPEC
 500    `FVT(s) UNION FVT(t) UNION
 501     FV(formsubst ((u |-> V x) ((v |-> s) i)) p) UNION
 502     FV(formsubst ((u |-> V y) ((v |-> t) i)) p)` VARIANT_FINITE) THEN
 503   REWRITE_TAC[FINITE_UNION; FV_FINITE; FVT_FINITE] THEN
 504   W(fun (_,w) -> ABBREV_TAC(mk_comb(`(=) (z:num)`,lhand(rand(lhand w))))) THEN
 505   REWRITE_TAC[IN_UNION; DE_MORGAN_THM] THEN STRIP_TAC THEN
 506   EXISTS_TAC `z:num` THEN ASM_REWRITE_TAC[] THEN
 507   CONJ_TAC THEN MATCH_MP_TAC subalpha THEN ASM_SIMP_TAC[LE_REFL] THENL
 508    [ASM_CASES_TAC `z:num = x` THEN ASM_REWRITE_TAC[] THEN
 509     UNDISCH_TAC `~(x IN FV (formsubst ((v |-> s) i) (!! u p)))`;
 510     ASM_CASES_TAC `z:num = y` THEN ASM_REWRITE_TAC[] THEN
 511     UNDISCH_TAC `~(y IN FV (formsubst ((v |-> t) i) (!! u p)))`] THEN
 512   ASM_REWRITE_TAC[FORMSUBST_FV; FV; IN_ELIM_THM; IN_DELETE] THEN
 513   MATCH_MP_TAC MONO_NOT THEN MATCH_MP_TAC MONO_EXISTS THEN
 514   X_GEN_TAC `w:num` THEN ASM_CASES_TAC `w:num = u` THEN
 515   ASM_REWRITE_TAC[VALMOD_BASIC; FVT; IN_SING] THEN
 516   ASM_REWRITE_TAC[valmod; FVT; IN_SING]);;
 517
 518 let isubst = prove
 519  (`!A p x s t. A |-- s === t
 520                      --> formsubst (x |=> s) p --> formsubst (x |=> t) p`,
 521   REWRITE_TAC[assign; isubst_general]);;
 522
 523 let isubst_var = prove
 524  (`!A p x t. A |-- V x === t --> p --> formsubst (x |=> t) p`,
 525   MESON_TAC[FORMSUBST_TRIV; ASSIGN_TRIV; isubst]);;
 526
 527 let alpha = prove
 528  (`!A x z p. ~(z IN FV p) ==> A |-- (!!x p) --> !!z (formsubst (x |=> V z) p)`,
 529   REPEAT STRIP_TAC THEN MATCH_MP_TAC subalpha THEN CONJ_TAC THENL
 530    [ALL_TAC; MESON_TAC[isubst_var]] THEN
 531   REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; ASSIGN] THEN
 532   ASM_MESON_TAC[IN_SING; FVT]);;
 533
 534 (* ------------------------------------------------------------------------- *)
 535 (* To conclude cleanly, useful to have all variables.                        *)
 536 (* ------------------------------------------------------------------------- *)
 537
 538 let VARS = new_recursive_definition form_RECURSION
 539  `(VARS False = {}) /\
 540   (VARS True = {}) /\
 541   (VARS (s === t) = FVT s UNION FVT t) /\
 542   (VARS (s << t) = FVT s UNION FVT t) /\
 543   (VARS (s <<= t) = FVT s UNION FVT t) /\
 544   (VARS (Not p) = VARS p) /\
 545   (VARS (p && q) = VARS p UNION VARS q) /\
 546   (VARS (p || q) = VARS p UNION VARS q) /\
 547   (VARS (p --> q) = VARS p UNION VARS q) /\
 548   (VARS (p <-> q) = VARS p UNION VARS q) /\
 549   (VARS (!! x p) = x INSERT VARS p) /\
 550   (VARS (?? x p) = x INSERT VARS p)`;;
 551
 552 let VARS_FINITE = prove
 553  (`!p. FINITE(VARS p)`,
 554   MATCH_MP_TAC form_INDUCT THEN
 555   ASM_SIMP_TAC[VARS; FINITE_RULES; FVT_FINITE; FINITE_UNION; FINITE_DELETE]);;
 556
 557 let FV_SUBSET_VARS = prove
 558  (`!p. FV(p) SUBSET VARS(p)`,
 559   REWRITE_TAC[SUBSET] THEN
 560   MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[FV; VARS] THEN
 561   REWRITE_TAC[IN_INSERT; IN_UNION; IN_DELETE] THEN MESON_TAC[]);;
 562
 563 let TERMSUBST_TWICE_GENERAL = prove
 564  (`!x z t v s. ~(z IN FVT s)
 565                ==> (termsubst ((x |-> t) v) s =
 566                     termsubst ((z |-> t) v) (termsubst (x |=> V z) s))`,
 567   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 568   MATCH_MP_TAC term_INDUCT THEN
 569   REWRITE_TAC[termsubst; ASSIGN; valmod; FVT; IN_SING; IN_UNION] THEN
 570   MESON_TAC[termsubst; ASSIGN]);;
 571
 572 let TERMSUBST_TWICE = prove
 573  (`!x z t s. ~(z IN FVT s)
 574              ==> (termsubst (x |=> t) s =
 575                   termsubst (z |=> t) (termsubst (x |=> V z) s))`,
 576   MESON_TAC[assign; TERMSUBST_TWICE_GENERAL]);;
 577
 578 let FORMSUBST_TWICE_GENERAL = prove
 579  (`!p i j.
 580         (!x. x IN VARS p ==> safe_for x i)
 581         ==> formsubst j (formsubst i p) = formsubst (termsubst j o i) p`,
 582   MATCH_MP_TAC form_INDUCT THEN
 583   REWRITE_TAC[VARS; FORALL_IN_INSERT; IN_UNION; NOT_IN_EMPTY; FORALL_AND_THM;
 584               TAUT `p \/ q ==> r <=> (p ==> r) /\ (q ==> r)`] THEN
 585   SIMP_TAC[FORMSUBST_SAFE_FOR] THEN
 586   REWRITE_TAC[formsubst; TERMSUBST_TERMSUBST] THEN SIMP_TAC[] THEN
 587   CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
 588   STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`i:num->term`; `j:num->term`] THEN
 589   STRIP_TAC THEN
 590   REWRITE_TAC[FV; FORMSUBST_FV; TERMSUBST_FVT; o_THM;
 591               IN_ELIM_THM; IN_DELETE] THEN
 592  (SUBGOAL_THEN
 593    `(?y. ((?y'. y' IN FV p /\ y IN FVT ((x |-> V x) i y')) /\ ~(y = x)) /\
 594           x IN FVT (j y)) <=>
 595     (?y. (y IN FV p /\ ~(y = x)) /\
 596          (?y'. y' IN FVT (i y) /\ x IN FVT (j y')))`
 597    (fun th -> REWRITE_TAC[th])
 598   THENL
 599    [REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 600     ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 601     AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 602     X_GEN_TAC `y:num` THEN
 603     ASM_CASES_TAC `y IN FV p` THEN ASM_REWRITE_TAC[] THEN
 604     ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THENL
 605      [ASM_REWRITE_TAC[VALMOD; FVT; IN_SING] THEN MESON_TAC[]; ALL_TAC] THEN
 606     AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 607     X_GEN_TAC `z:num` THEN
 608     ASM_CASES_TAC `x IN FVT(j(z:num))` THEN ASM_REWRITE_TAC[] THEN
 609     ASM_REWRITE_TAC[VALMOD] THEN ASM_MESON_TAC[safe_for];
 610     ALL_TAC] THEN
 611   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 612   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 613    [SUBGOAL_THEN
 614      `{x' | ?y. (?y'. y' IN FV p /\ y IN FVT ((x |-> V x) i y')) /\
 615                 x' IN FVT ((x |-> V x) j y)} =
 616       {x' | ?y. y IN FV p /\ x' IN FVT ((x |-> V x) (termsubst j o i) y)}`
 617      (fun th -> REWRITE_TAC[th])
 618     THENL
 619      [REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN X_GEN_TAC `z:num` THEN
 620       REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 621       ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 622       AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 623       X_GEN_TAC `y:num` THEN
 624       ASM_CASES_TAC `y IN FV p` THEN ASM_REWRITE_TAC[] THEN
 625       ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THEN
 626       ASM_REWRITE_TAC[VALMOD; FVT; IN_SING; UNWIND_THM2] THEN
 627       REWRITE_TAC[o_THM; TERMSUBST_FVT; IN_ELIM_THM] THEN
 628       ASM_MESON_TAC[safe_for];
 629       ABBREV_TAC `z = VARIANT
 630        {x' | ?y. y IN FV p /\ x' IN FVT ((x |-> V x) (termsubst j o i) y)}`];
 631       ALL_TAC]) THEN
 632   AP_TERM_TAC THEN FIRST_X_ASSUM(fun th ->
 633    W(MP_TAC o PART_MATCH (lhs o rand) th o lhs o snd)) THEN
 634   ASM_SIMP_TAC[SAFE_FOR_VALMOD; FVT; IN_SING] THEN
 635   DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC FORMSUBST_EQ THEN
 636   X_GEN_TAC `y:num` THEN DISCH_TAC THEN
 637   REWRITE_TAC[VALMOD; o_THM] THEN
 638   COND_CASES_TAC THEN ASM_REWRITE_TAC[termsubst; VALMOD] THEN
 639   MATCH_MP_TAC TERMSUBST_EQ THEN
 640   X_GEN_TAC `w:num` THEN REWRITE_TAC[VALMOD] THEN
 641   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[safe_for]);;
 642
 643 let FORMSUBST_TWICE = prove
 644  (`!z p x t. ~(z IN VARS p)
 645              ==> (formsubst (z |=> t) (formsubst (x |=> V z) p) =
 646                   formsubst (x |=> t) p)`,
 647   REPEAT STRIP_TAC THEN
 648   W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_TWICE_GENERAL o lhs o snd) THEN
 649   REWRITE_TAC[SAFE_FOR_ASSIGN; FVT; IN_SING] THEN
 650   ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN
 651   MATCH_MP_TAC FORMSUBST_EQ THEN REPEAT STRIP_TAC THEN
 652   REWRITE_TAC[o_THM; VALMOD; ASSIGN] THEN
 653   COND_CASES_TAC THEN ASM_REWRITE_TAC[termsubst; ASSIGN] THEN
 654   ASM_MESON_TAC[FV_SUBSET_VARS; SUBSET]);;
 655
 656 let ispec_lemma = prove
 657  (`!A x p t. ~(x IN FVT(t)) ==> A |-- !!x p --> formsubst (x |=> t) p`,
 658   REPEAT STRIP_TAC THEN MATCH_MP_TAC subspec THEN
 659   EXISTS_TAC `t:term` THEN ASM_REWRITE_TAC[isubst_var] THEN
 660   ASM_REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; ASSIGN] THEN
 661   ASM_MESON_TAC[FVT; IN_SING]);;
 662
 663 let ispec = prove
 664  (`!A x p t. A |-- !!x p --> formsubst (x |=> t) p`,
 665   REPEAT STRIP_TAC THEN ASM_CASES_TAC `x IN FVT(t)` THEN
 666   ASM_SIMP_TAC[ispec_lemma] THEN
 667   ABBREV_TAC `z = VARIANT (FVT t UNION VARS p)` THEN
 668   MATCH_MP_TAC imp_trans THEN
 669   EXISTS_TAC `!!z (formsubst (x |=> V z) p)` THEN CONJ_TAC THENL
 670    [MATCH_MP_TAC alpha THEN EXPAND_TAC "z" THEN
 671     MATCH_MP_TAC NOT_IN_VARIANT THEN
 672     REWRITE_TAC[FINITE_UNION; SUBSET; IN_UNION] THEN
 673     MESON_TAC[SUBSET; FVT_FINITE; VARS_FINITE; FV_SUBSET_VARS];
 674     SUBGOAL_THEN
 675      `formsubst (x |=> t) p =
 676       formsubst (z |=> t) (formsubst (x |=> V z) p)`
 677     SUBST1_TAC THENL
 678      [MATCH_MP_TAC(GSYM FORMSUBST_TWICE); MATCH_MP_TAC ispec_lemma] THEN
 679     EXPAND_TAC "z" THEN MATCH_MP_TAC NOT_IN_VARIANT THEN
 680     REWRITE_TAC[VARS_FINITE; FVT_FINITE; FINITE_UNION] THEN
 681     SIMP_TAC[SUBSET; IN_UNION]]);;
 682
 683 let spec = prove
 684  (`!A x p t. A |-- !!x p ==> A |-- formsubst (x |=> t) p`,
 685   MESON_TAC[ispec; modusponens]);;
 686
 687 let spec_var = prove
 688  (`!A x p. A |-- !!x p ==> A |-- p`,
 689   REPEAT GEN_TAC THEN
 690   DISCH_THEN(MP_TAC o SPEC `V x` o MATCH_MP spec) THEN
 691   SIMP_TAC[ASSIGN_TRIV; FORMSUBST_TRIVIAL]);;
 692
 693 let instantiation = prove
 694  (`!A v p. A |-- p ==> A |-- formsubst v p`,
 695   let lemma = prove
 696    (`!A p v. (!x y. x IN FV p /\ y IN FV p /\ x IN FVT(v y)
 697                     ==> x = y /\ v x = V x) /\
 698              A |-- p
 699              ==> A |-- formsubst v p`,
 700     REPEAT GEN_TAC THEN
 701     WF_INDUCT_TAC `CARD {x | x IN FV(p) /\ ~(v x = V x)}` THEN
 702     ASM_CASES_TAC `!x. x IN FV p ==> v x = V x` THEN
 703     ASM_SIMP_TAC[FORMSUBST_TRIVIAL] THEN
 704     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
 705     REWRITE_TAC[NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
 706     X_GEN_TAC `x:num` THEN REPEAT STRIP_TAC THEN
 707     FIRST_X_ASSUM(MP_TAC o SPECL [`p:form`; `(x |-> V x) v`]) THEN
 708     ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 709      [MATCH_MP_TAC CARD_PSUBSET THEN SIMP_TAC[FINITE_RESTRICT; FV_FINITE] THEN
 710       REWRITE_TAC[PSUBSET_ALT] THEN CONJ_TAC THENL
 711        [REWRITE_TAC[SUBSET; VALMOD; IN_ELIM_THM] THEN ASM_MESON_TAC[];
 712         EXISTS_TAC `x:num` THEN ASM_REWRITE_TAC[VALMOD; IN_ELIM_THM] THEN
 713         ASM_MESON_TAC[]];
 714       ALL_TAC] THEN
 715     ANTS_TAC THENL
 716      [REPEAT GEN_TAC THEN REWRITE_TAC[VALMOD] THEN
 717       COND_CASES_TAC THEN ASM_SIMP_TAC[FVT; IN_SING] THEN ASM_MESON_TAC[];
 718       ALL_TAC] THEN
 719     SUBGOAL_THEN
 720      `formsubst v p = formsubst ((x |-> v x) v) p`
 721     SUBST1_TAC THENL [SIMP_TAC[VALMOD_TRIVIAL]; ALL_TAC] THEN
 722     DISCH_THEN(MP_TAC o SPEC `x:num` o MATCH_MP gen) THEN
 723     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] modusponens) THEN
 724     MATCH_MP_TAC exists_imp THEN CONJ_TAC THENL
 725      [ALL_TAC;
 726       REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; NOT_EXISTS_THM; VALMOD] THEN
 727       ASM SET_TAC[]] THEN
 728     MATCH_MP_TAC modusponens THEN EXISTS_TAC `??x (V x === v x)` THEN
 729     SIMP_TAC[eximp; isubst_general] THEN ASM_MESON_TAC[axiom_existseq]) in
 730   REPEAT STRIP_TAC THEN
 731   SUBGOAL_THEN
 732    `?n. !x. x IN VARS p \/ x IN FV(formsubst v p) ==> x < n`
 733   STRIP_ASSUME_TAC THENL
 734    [EXISTS_TAC `SUC(SETMAX(VARS p UNION FV(formsubst v p)))` THEN
 735     REWRITE_TAC[GSYM IN_UNION; LT_SUC_LE] THEN MATCH_MP_TAC SETMAX_MEMBER THEN
 736     REWRITE_TAC[FINITE_UNION; VARS_FINITE; FV_FINITE];
 737     ALL_TAC] THEN
 738   SUBGOAL_THEN
 739    `formsubst v p =
 740     formsubst (\i. v(i - n)) (formsubst (\i. V(i + n)) p)`
 741   SUBST1_TAC THENL
 742    [W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_TWICE_GENERAL o
 743       rand o snd) THEN
 744     REWRITE_TAC[safe_for; FVT; IN_SING] THEN ANTS_TAC THENL
 745      [ASM_MESON_TAC[ARITH_RULE `~(x + n:num < n)`];
 746       DISCH_THEN SUBST1_TAC THEN
 747       REWRITE_TAC[o_DEF; termsubst; ADD_SUB; ETA_AX]];
 748     MATCH_MP_TAC lemma THEN REWRITE_TAC[FVT] THEN CONJ_TAC THENL
 749      [REWRITE_TAC[FORMSUBST_FV; FVT; IN_SING] THEN
 750       REWRITE_TAC[SET_RULE `{x | ?y. y IN s /\ x = f y} = IMAGE f s`] THEN
 751       REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 752       X_GEN_TAC `x:num` THEN DISCH_TAC THEN REWRITE_TAC[ADD_SUB; FVT] THEN
 753       X_GEN_TAC `y:num` THEN REPEAT DISCH_TAC THEN
 754       FIRST_X_ASSUM(MP_TAC o SPEC `x + n:num`) THEN
 755       MATCH_MP_TAC(TAUT `~p /\ q ==> (r \/ q ==> p) ==> s`) THEN
 756       CONJ_TAC THENL [ARITH_TAC; REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM]] THEN
 757       ASM_MESON_TAC[];
 758       MATCH_MP_TAC lemma THEN REWRITE_TAC[FVT; IN_SING] THEN
 759       ASM_MESON_TAC[ARITH_RULE `x < n /\ y < n ==> ~(x = y + n)`;
 760                     FV_SUBSET_VARS; SUBSET]]]);;
 761
 762 (* ------------------------------------------------------------------------- *)
 763 (* Monotonicity and the deduction theorem.                                   *)
 764 (* ------------------------------------------------------------------------- *)
 765
 766 let PROVES_MONO = prove
 767  (`!A B p. A SUBSET B /\ A |-- p ==> B |-- p`,
 768   GEN_TAC THEN GEN_TAC THEN
 769   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 770   MATCH_MP_TAC proves_INDUCT THEN  ASM_MESON_TAC[proves_RULES; SUBSET]);;
 771
 772 let DEDUCTION_LEMMA = prove
 773  (`!A p q. p INSERT A |-- q /\ closed p ==> A |-- p --> q`,
 774   GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
 775   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 776   GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC proves_INDUCT THEN
 777   REPEAT CONJ_TAC THEN X_GEN_TAC `r:form` THENL
 778    [REWRITE_TAC[IN_INSERT] THEN MESON_TAC[proves_RULES; add_assum; imp_refl];
 779     MESON_TAC[modusponens; axiom_distribimp];
 780     ASM_MESON_TAC[gen_right; closed; NOT_IN_EMPTY]]);;
 781
 782 let DEDUCTION = prove
 783  (`!A p q. closed p ==> (A |-- p --> q <=> p INSERT A |-- q)`,
 784   MESON_TAC[DEDUCTION_LEMMA; modusponens; IN_INSERT; proves_RULES;
 785             PROVES_MONO; SUBSET]);;
 786
 787 (* ------------------------------------------------------------------------- *)
 788 (* A few more derived rules.                                                 *)
 789 (* ------------------------------------------------------------------------- *)
 790
 791 let eq_trans = prove
 792  (`!A s t u. A |-- s === t --> t === u --> s === u`,
 793   MESON_TAC[axiom_predcong; modusponens; imp_swap; axiom_eqrefl; imp_trans;
 794             eq_sym]);;
 795
 796 let spec_right = prove
 797  (`!A p q x. A |-- p --> !!x q ==> A |-- p --> formsubst (x |=> t) q`,
 798   MESON_TAC[imp_trans; ispec]);;
 799
 800 let eq_trans_rule = prove
 801  (`!A s t u. A |-- s === t /\ A |-- t === u ==> A |-- s === u`,
 802   MESON_TAC[modusponens; eq_trans]);;
 803
 804 let eq_sym_rule = prove
 805  (`!A s t. A |-- s === t <=> A |-- t === s`,
 806   MESON_TAC[modusponens; eq_sym]);;
 807
 808 let allimp = prove
 809  (`!A x p q. A |-- p --> q ==> A |-- !!x p --> !!x q`,
 810   MESON_TAC[axiom_allimp; modusponens; gen]);;
 811
 812 let alliff = prove
 813  (`!A x p q. A |-- p <-> q ==> A |-- !!x p <-> !!x q`,
 814   MESON_TAC[allimp; iff_imp1; iff_imp2; imp_antisym]);;
 815
 816 let exiff = prove
 817  (`!A x p q. A |-- p <-> q ==> A |-- ??x p <-> ??x q`,
 818   MESON_TAC[eximp; iff_imp1; iff_imp2; imp_antisym]);;
 819
 820 let cong_suc = prove
 821  (`!A s t. A |-- s === t ==> A |-- Suc s === Suc t`,
 822   MESON_TAC[modusponens; axiom_funcong]);;
 823
 824 let cong_add = prove
 825  (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ++ u === t ++ v`,
 826   MESON_TAC[modusponens; axiom_funcong]);;
 827
 828 let cong_mul = prove
 829  (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ** u === t ** v`,
 830   MESON_TAC[modusponens; axiom_funcong]);;
 831
 832 let cong_eq = prove
 833  (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s === u <-> t === v`,
 834   REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN
 835   ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
 836
 837 let cong_le = prove
 838  (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s <<= u <-> t <<= v`,
 839   REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN
 840   ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
 841
 842 let cong_lt = prove
 843  (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s << u <-> t << v`,
 844   REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN
 845   ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
 846
 847 let iexists = prove
 848  (`!A x t p. A |-- formsubst (x |=> t) p --> ??x p`,
 849   REPEAT GEN_TAC THEN TRANS_TAC imp_trans `Not(!!x (Not p))` THEN
 850   CONJ_TAC THENL [ALL_TAC; MESON_TAC[axiom_exists; iff_imp2]] THEN
 851   TRANS_TAC imp_trans `Not(formsubst (x |=> t) (Not p))` THEN
 852   REWRITE_TAC[contrapos_eq; ispec] THEN REWRITE_TAC[formsubst] THEN
 853   MESON_TAC[not_not; iff_imp2]);;
 854
 855 let exists_intro = prove
 856  (`!A x t p. A |-- formsubst (x |=> t) p ==> A |-- ??x p`,
 857   MESON_TAC[iexists; modusponens]);;
 858
 859 let impex = prove
 860  (`!A x p. ~(x IN FV p) ==> A |-- (??x p) --> p`,
 861   REPEAT STRIP_TAC THEN TRANS_TAC imp_trans `Not(Not p)` THEN
 862   CONJ_TAC THENL [ALL_TAC; MESON_TAC[not_not; iff_imp1]] THEN
 863   TRANS_TAC imp_trans `Not(!!x (Not p))` THEN
 864   ASM_SIMP_TAC[contrapos_eq; axiom_impall; FV] THEN
 865   MESON_TAC[axiom_exists; iff_imp1]);;
 866
 867 let ichoose = prove
 868  (`!A x p q. A |-- !!x (p --> q) /\ ~(x IN FV q) ==> A |-- (??x p) --> q`,
 869   REPEAT STRIP_TAC THEN
 870   FIRST_ASSUM(MP_TAC o MATCH_MP spec_var) THEN
 871   DISCH_THEN(MP_TAC o SPEC `x:num` o MATCH_MP eximp) THEN
 872   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] imp_trans) THEN
 873   ASM_SIMP_TAC[impex]);;
 874
 875 let eq_trans_imp = prove
 876  (`A |-- s === s' /\ A |-- t === t' ==> A |-- s === t --> s' === t'`,
 877   MESON_TAC[axiom_predcong; modusponens]);;
 878
 879 (* ------------------------------------------------------------------------- *)
 880 (* Some conversions for performing explicit substitution operations in what  *)
 881 (* we hope is the common case where no variable renaming occurs.             *)
 882 (* ------------------------------------------------------------------------- *)
 883
 884 let fv_theorems = ref
 885  [FV; FV_AXIOM; FV_DIAGONALIZE; FV_DIVIDES; FV_FINITE; FV_FIXPOINT; FV_FORM;
 886   FV_FORM1; FV_FREEFORM; FV_FREEFORM1; FV_FREETERM; FV_FREETERM1;
 887   FV_GNUMERAL; FV_GNUMERAL1; FV_GNUMERAL1'; FV_GSENTENCE;
 888   FV_HSENTENCE; FV_PRIME; FV_PRIMEPOW; FV_PRIMREC; FV_PRIMRECSTEP; FV_PROV;
 889   FV_PROV1; FV_QDIAG; FV_QSUBST; FV_RTC; FV_RTCP; FV_SUBSET_VARS; FV_TERM;
 890   FV_TERM1; FVT; FVT_NUMERAL];;
 891
 892 let IN_FV_RULE ths tm =
 893   try EQT_ELIM
 894        ((GEN_REWRITE_CONV TOP_DEPTH_CONV
 895              ([IN_UNION; IN_DELETE; NOT_IN_EMPTY; IN_INSERT] @
 896               ths @ !fv_theorems) THENC
 897          NUM_REDUCE_CONV) tm)
 898   with Failure _ -> ASSUME tm;;
 899
 900 let rec SAFE_FOR_RULE tm =
 901   try PART_MATCH I SAFE_FOR_V tm
 902   with Failure _ ->
 903   try let th1 = PART_MATCH lhand SAFE_FOR_ASSIGN tm in
 904       let th2 = IN_FV_RULE [] (rand(concl th1)) in
 905       EQ_MP (SYM th1) th2
 906   with Failure _ ->
 907       let th1 = PART_MATCH rand SAFE_FOR_VALMOD tm in
 908       let l,r = dest_conj(lhand(concl th1)) in
 909       let th2 = CONJ (SAFE_FOR_RULE l) (IN_FV_RULE [] r) in
 910       MP th1 th2;;
 911
 912 let VALMOD_CONV =
 913   GEN_REWRITE_CONV TOP_DEPTH_CONV [ASSIGN; VALMOD] THENC NUM_REDUCE_CONV;;
 914
 915 let TERMSUBST_NUMERAL = prove
 916  (`!v n. termsubst v (numeral n) = numeral n`,
 917   SIMP_TAC[TERMSUBST_TRIVIAL; FVT_NUMERAL; NOT_IN_EMPTY]);;
 918
 919 let rec TERMSUBST_CONV tm =
 920   (GEN_REWRITE_CONV I [CONJ TERMSUBST_NUMERAL (CONJUNCT1 termsubst)] ORELSEC
 921    (GEN_REWRITE_CONV I [el 1 (CONJUNCTS termsubst)] THENC
 922     VALMOD_CONV) ORELSEC
 923    (GEN_REWRITE_CONV I [el 2 (CONJUNCTS termsubst)] THENC
 924     RAND_CONV TERMSUBST_CONV) ORELSEC
 925    (GEN_REWRITE_CONV I [funpow 3 CONJUNCT2 termsubst] THENC
 926     BINOP_CONV TERMSUBST_CONV)) tm;;
 927
 928 let rec FORMSUBST_CONV tm =
 929   (GEN_REWRITE_CONV I
 930     [el 0 (CONJUNCTS formsubst); el 1 (CONJUNCTS formsubst)] ORELSEC
 931    (GEN_REWRITE_CONV I
 932     [el 2 (CONJUNCTS formsubst); el 3 (CONJUNCTS formsubst);
 933      el 4 (CONJUNCTS formsubst)] THENC BINOP_CONV TERMSUBST_CONV) ORELSEC
 934    (GEN_REWRITE_CONV I [el 5 (CONJUNCTS formsubst)] THENC
 935     RAND_CONV FORMSUBST_CONV) ORELSEC
 936    (GEN_REWRITE_CONV I
 937      [el 6 (CONJUNCTS formsubst); el 7 (CONJUNCTS formsubst);
 938       el 8 (CONJUNCTS formsubst); el 9 (CONJUNCTS formsubst)] THENC
 939     BINOP_CONV FORMSUBST_CONV) ORELSEC
 940    ((fun tm ->
 941      let th =
 942        try PART_MATCH (lhand o rand) (CONJUNCT1 FORMSUBST_SAFE_FOR) tm
 943        with Failure _ ->
 944            PART_MATCH (lhand o rand) (CONJUNCT2 FORMSUBST_SAFE_FOR) tm in
 945      MP th (SAFE_FOR_RULE (lhand(concl th)))) THENC
 946     RAND_CONV FORMSUBST_CONV)) tm;;
 947
 948 (* ------------------------------------------------------------------------- *)
 949 (* Hence a more convenient specialization rule.                              *)
 950 (* ------------------------------------------------------------------------- *)
 951
 952 let spec_var_rule th = MATCH_MP spec_var th;;
 953
 954 let spec_all_rule = repeat spec_var_rule;;
 955
 956 let instantiate_rule ilist th =
 957   let v_tm = `(|->):num->term->(num->term)->(num->term)` in
 958   let v = itlist (fun (t,x) v ->
 959         mk_comb(mk_comb(mk_comb(v_tm,mk_small_numeral x),t),v)) ilist `V` in
 960   CONV_RULE (RAND_CONV FORMSUBST_CONV)
 961             (SPEC v (MATCH_MP instantiation th));;
 962
 963 let specl_rule tms th =
 964   let avs = striplist (dest_binop `!!`) (rand(concl th)) in
 965   let vs = fst(chop_list(length tms) avs) in
 966   let ilist = map2 (fun t v -> (t,dest_small_numeral v)) tms vs in
 967   instantiate_rule ilist (funpow (length vs) spec_var_rule th);;
 968
 969 let spec_rule t th = specl_rule [t] th;;
 970
 971 let gen_rule t th = SPEC (mk_small_numeral t) (MATCH_MP gen th);;
 972
 973 let gens_tac ns (asl,w) =
 974   let avs,bod = nsplit dest_forall ns w in
 975   let nvs = map (curry mk_comb `V` o mk_small_numeral) ns in
 976   let bod' = subst (zip nvs avs) bod in
 977   let th = GENL avs (instantiate_rule (zip avs ns) (ASSUME bod')) in
 978   MATCH_MP_TAC (DISCH_ALL th) (asl,w);;
 979
 980 let gen_tac n = gens_tac [n];;