Arithmetic/fol.ml

   1 (* ========================================================================= *)
   2 (* First order logic based on the language of arithmetic.                    *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Syntax of terms.                                                          *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 parse_as_infix("++",(20,"right"));;
  12 parse_as_infix("**",(22,"right"));;
  13
  14 let term_INDUCT,term_RECURSION = define_type
  15   "term = Z
  16         | V num
  17         | Suc term
  18         | ++ term term
  19         | ** term term";;
  20
  21 let term_CASES = prove_cases_thm term_INDUCT;;
  22
  23 let term_DISTINCT = distinctness "term";;
  24
  25 let term_INJ = injectivity "term";;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Syntax of formulas.                                                       *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 parse_as_infix("===",(18,"right"));;
  32 parse_as_infix("<<",(18,"right"));;
  33 parse_as_infix("<<=",(18,"right"));;
  34
  35 parse_as_infix("&&",(16,"right"));;
  36 parse_as_infix("||",(15,"right"));;
  37 parse_as_infix("-->",(14,"right"));;
  38 parse_as_infix("<->",(13,"right"));;
  39
  40 let form_INDUCT,form_RECURSION = define_type
  41   "form = False
  42         | True
  43         | === term term
  44         | << term term
  45         | <<= term term
  46         | Not form
  47         | && form form
  48         | || form form
  49         | --> form form
  50         | <-> form form
  51         | !! num form
  52         | ?? num form";;
  53
  54 let form_CASES = prove_cases_thm form_INDUCT;;
  55
  56 let form_DISTINCT = distinctness "form";;
  57
  58 let form_INJ = injectivity "form";;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* Semantics of terms and formulas in the standard model.                    *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 parse_as_infix("|->",(22,"right"));;
  65
  66 let valmod = new_definition
  67   `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
  68
  69 let termval = new_recursive_definition term_RECURSION
  70   `(termval v Z = 0) /\
  71    (termval v (V n) = v(n)) /\
  72    (termval v (Suc t) = SUC (termval v t)) /\
  73    (termval v (s ++ t) = termval v s + termval v t) /\
  74    (termval v (s ** t) = termval v s * termval v t)`;;
  75
  76 let holds = new_recursive_definition form_RECURSION
  77   `(holds v False <=> F) /\
  78    (holds v True <=> T) /\
  79    (holds v (s === t) <=> (termval v s = termval v t)) /\
  80    (holds v (s << t) <=> (termval v s < termval v t)) /\
  81    (holds v (s <<= t) <=> (termval v s <= termval v t)) /\
  82    (holds v (Not p) <=> ~(holds v p)) /\
  83    (holds v (p && q) <=> holds v p /\ holds v q) /\
  84    (holds v (p || q) <=> holds v p \/ holds v q) /\
  85    (holds v (p --> q) <=> holds v p ==> holds v q) /\
  86    (holds v (p <-> q) <=> (holds v p <=> holds v q)) /\
  87    (holds v (!! x p) <=> !a. holds ((x|->a) v) p) /\
  88    (holds v (?? x p) <=> ?a. holds ((x|->a) v) p)`;;
  89
  90 let true_def = new_definition
  91   `true p <=> !v. holds v p`;;
  92
  93 let VALMOD = prove
  94  (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
  95   REWRITE_TAC[valmod]);;
  96
  97 let VALMOD_BASIC = prove
  98  (`!v x y. (x |-> y) v x = y`,
  99   REWRITE_TAC[valmod]);;
 100
 101 let VALMOD_VALMOD_BASIC = prove
 102  (`!v a b x. (x |-> a) ((x |-> b) v) = (x |-> a) v`,
 103   REWRITE_TAC[valmod; FUN_EQ_THM] THEN
 104   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
 105
 106 let VALMOD_REPEAT = prove
 107  (`!v x. (x |-> v(x)) v = v`,
 108   REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
 109
 110 let FORALL_VALMOD = prove
 111  (`!x. (!v a. P((x |-> a) v)) <=> (!v. P v)`,
 112   MESON_TAC[VALMOD_REPEAT]);;
 113
 114 let VALMOD_SWAP = prove
 115  (`!v x y a b.
 116      ~(x = y) ==> ((x |-> a) ((y |-> b) v) = (y |-> b) ((x |-> a) v))`,
 117   REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
 118
 119 let VALMOD_TRIVIAL = prove
 120  (`!v x. v x = t ==> (x |-> t) v = v`,
 121   REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Assignment.                                                               *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 parse_as_infix("|=>",(22,"right"));;
 128
 129 let assign = new_definition
 130  `(x |=> a) = (x |-> a) V`;;
 131
 132 let ASSIGN = prove
 133  (`!x y a. (x |=> a) y = if y = x then a else V(y)`,
 134   REWRITE_TAC[assign; valmod]);;
 135
 136 let ASSIGN_TRIV = prove
 137  (`!x. (x |=> V x) = V`,
 138   REWRITE_TAC[VALMOD_REPEAT; assign]);;
 139
 140 (* ------------------------------------------------------------------------- *)
 141 (* Variables in a term and free variables in a formula.                      *)
 142 (* ------------------------------------------------------------------------- *)
 143
 144 let FVT = new_recursive_definition term_RECURSION
 145   `(FVT Z = {}) /\
 146    (FVT (V n) = {n}) /\
 147    (FVT (Suc t) = FVT t) /\
 148    (FVT (s ++ t) = (FVT s) UNION (FVT t)) /\
 149    (FVT (s ** t) = (FVT s) UNION (FVT t))`;;
 150
 151 let FV = new_recursive_definition form_RECURSION
 152   `(FV False = {}) /\
 153    (FV True = {}) /\
 154    (FV (s === t) = (FVT s) UNION (FVT t)) /\
 155    (FV (s << t) = (FVT s) UNION (FVT t)) /\
 156    (FV (s <<= t) = (FVT s) UNION (FVT t)) /\
 157    (FV (Not p) = FV p) /\
 158    (FV (p && q) = (FV p) UNION (FV q)) /\
 159    (FV (p || q) = (FV p) UNION (FV q)) /\
 160    (FV (p --> q) = (FV p) UNION (FV q)) /\
 161    (FV (p <-> q) = (FV p) UNION (FV q)) /\
 162    (FV (!!x p) = (FV p) DELETE x) /\
 163    (FV (??x p) = (FV p) DELETE x)`;;
 164
 165 let FVT_FINITE = prove
 166  (`!t. FINITE(FVT t)`,
 167   MATCH_MP_TAC term_INDUCT THEN
 168   SIMP_TAC[FVT; FINITE_RULES; FINITE_INSERT; FINITE_UNION]);;
 169
 170 let FV_FINITE = prove
 171  (`!p. FINITE(FV p)`,
 172   MATCH_MP_TAC form_INDUCT THEN
 173   SIMP_TAC[FV; FVT_FINITE; FINITE_RULES; FINITE_DELETE; FINITE_UNION]);;
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Logical axioms.                                                           *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179 let axiom_RULES,axiom_INDUCT,axiom_CASES = new_inductive_definition
 180  `(!p q. axiom(p --> (q --> p))) /\
 181   (!p q r. axiom((p --> q --> r) --> (p --> q) --> (p --> r))) /\
 182   (!p. axiom(((p --> False) --> False) --> p)) /\
 183   (!x p q. axiom((!!x (p --> q)) --> (!!x p) --> (!!x q))) /\
 184   (!x p. ~(x IN FV p) ==> axiom(p --> !!x p)) /\
 185   (!x t. ~(x IN FVT t) ==> axiom(??x (V x === t))) /\
 186   (!t. axiom(t === t)) /\
 187   (!s t. axiom((s === t) --> (Suc s === Suc t))) /\
 188   (!s t u v. axiom(s === t --> u === v --> s ++ u === t ++ v)) /\
 189   (!s t u v. axiom(s === t --> u === v --> s ** u === t ** v)) /\
 190   (!s t u v. axiom(s === t --> u === v --> s === u --> t === v)) /\
 191   (!s t u v. axiom(s === t --> u === v --> s << u --> t << v)) /\
 192   (!s t u v. axiom(s === t --> u === v --> s <<= u --> t <<= v)) /\
 193   (!p q. axiom((p <-> q) --> p --> q)) /\
 194   (!p q. axiom((p <-> q) --> q --> p)) /\
 195   (!p q. axiom((p --> q) --> (q --> p) --> (p <-> q))) /\
 196   axiom(True <-> (False --> False)) /\
 197   (!p. axiom(Not p <-> (p --> False))) /\
 198   (!p q. axiom((p && q) <-> (p --> q --> False) --> False)) /\
 199   (!p q. axiom((p || q) <-> Not(Not p && Not q))) /\
 200   (!x p. axiom((??x p) <-> Not(!!x (Not p))))`;;
 201
 202 (* ------------------------------------------------------------------------- *)
 203 (* Deducibility from additional set of nonlogical axioms.                    *)
 204 (* ------------------------------------------------------------------------- *)
 205
 206 parse_as_infix("|--",(11,"right"));;
 207
 208 let proves_RULES,proves_INDUCT,proves_CASES = new_inductive_definition
 209   `(!p. axiom p \/ p IN A ==> A |-- p) /\
 210    (!p q. A |-- (p --> q) /\ A |-- p ==> A |-- q) /\
 211    (!p x. A |-- p ==> A |-- (!!x p))`;;
 212
 213 (* ------------------------------------------------------------------------- *)
 214 (* Some lemmas.                                                              *)
 215 (* ------------------------------------------------------------------------- *)
 216
 217 let TERMVAL_VALUATION = prove
 218  (`!t v v'. (!x. x IN FVT(t) ==> (v'(x) = v(x)))
 219             ==> (termval v' t = termval v t)`,
 220   MATCH_MP_TAC term_INDUCT THEN
 221   REWRITE_TAC[termval; FVT; IN_INSERT; IN_UNION; NOT_IN_EMPTY] THEN
 222   REPEAT STRIP_TAC THEN ASM_MESON_TAC[]);;
 223
 224 let HOLDS_VALUATION = prove
 225  (`!p v v'.
 226       (!x. x IN (FV p) ==> (v'(x) = v(x)))
 227       ==> (holds v' p <=> holds v p)`,
 228   MATCH_MP_TAC form_INDUCT THEN
 229   REWRITE_TAC[FV; holds; IN_UNION; IN_DELETE] THEN
 230   SIMP_TAC[TERMVAL_VALUATION] THEN
 231   REWRITE_TAC[valmod] THEN REPEAT STRIP_TAC THEN
 232   AP_TERM_TAC THEN ABS_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 233   ASM_SIMP_TAC[]);;
 234
 235 let TERMVAL_VALMOD_OTHER = prove
 236  (`!v x a t. ~(x IN FVT t) ==> (termval ((x |-> a) v) t = termval v t)`,
 237   MESON_TAC[TERMVAL_VALUATION; VALMOD]);;
 238
 239 let HOLDS_VALMOD_OTHER = prove
 240  (`!v x a p. ~(x IN FV p) ==> (holds ((x |-> a) v) p <=> holds v p)`,
 241   MESON_TAC[HOLDS_VALUATION; VALMOD]);;
 242
 243 (* ------------------------------------------------------------------------- *)
 244 (* Proof of soundness.                                                       *)
 245 (* ------------------------------------------------------------------------- *)
 246
 247 let AXIOMS_TRUE = prove
 248  (`!p. axiom p ==> true p`,
 249   MATCH_MP_TAC axiom_INDUCT THEN
 250   REWRITE_TAC[true_def] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[holds] THENL
 251    [CONV_TAC TAUT;
 252     CONV_TAC TAUT;
 253     SIMP_TAC[];
 254     REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN REPEAT GEN_TAC THEN
 255     MATCH_MP_TAC EQ_IMP THEN
 256     MATCH_MP_TAC HOLDS_VALUATION THEN
 257     REWRITE_TAC[valmod] THEN GEN_TAC THEN COND_CASES_TAC THEN
 258     ASM_MESON_TAC[];
 259     EXISTS_TAC `termval v t` THEN
 260     REWRITE_TAC[termval; valmod] THEN
 261     MATCH_MP_TAC TERMVAL_VALUATION THEN
 262     GEN_TAC THEN REWRITE_TAC[] THEN
 263     COND_CASES_TAC THEN ASM_MESON_TAC[];
 264     SIMP_TAC[termval];
 265     SIMP_TAC[termval];
 266     SIMP_TAC[termval];
 267     SIMP_TAC[termval];
 268     SIMP_TAC[termval];
 269     SIMP_TAC[termval];
 270     SIMP_TAC[termval];
 271     SIMP_TAC[termval];
 272     CONV_TAC TAUT;
 273     CONV_TAC TAUT;
 274     CONV_TAC TAUT;
 275     MESON_TAC[]]);;
 276
 277 let THEOREMS_TRUE = prove
 278  (`!A p. (!q. q IN A ==> true q) /\ A |-- p ==> true p`,
 279   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 280   DISCH_TAC THEN MATCH_MP_TAC proves_INDUCT THEN
 281   ASM_SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 282   REWRITE_TAC[IN; AXIOMS_TRUE] THEN
 283   SIMP_TAC[holds; true_def]);;
 284
 285 (* ------------------------------------------------------------------------- *)
 286 (* Variant variables for use in renaming substitution.                       *)
 287 (* ------------------------------------------------------------------------- *)
 288
 289 let MAX_SYM = prove
 290  (`!x y. MAX x y = MAX y x`,
 291   ARITH_TAC);;
 292
 293 let MAX_ASSOC = prove
 294  (`!x y z. MAX x (MAX y z) = MAX (MAX x y) z`,
 295   ARITH_TAC);;
 296
 297 let SETMAX = new_definition
 298   `SETMAX s = ITSET MAX s 0`;;
 299
 300 let VARIANT = new_definition
 301   `VARIANT s = SETMAX s + 1`;;
 302
 303 let SETMAX_LEMMA = prove
 304  (`(SETMAX {} = 0) /\
 305    (!x s. FINITE s ==>
 306            (SETMAX (x INSERT s) = if x IN s then SETMAX s
 307                                   else MAX x (SETMAX s)))`,
 308   REWRITE_TAC[SETMAX] THEN MATCH_MP_TAC FINITE_RECURSION THEN
 309   REWRITE_TAC[MAX] THEN REPEAT GEN_TAC THEN
 310   MAP_EVERY ASM_CASES_TAC
 311    [`x:num <= s`; `y:num <= s`; `x:num <= y`; `y <= x`] THEN
 312   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LE_CASES; LE_TRANS; LE_ANTISYM]);;
 313
 314 let SETMAX_MEMBER = prove
 315  (`!s. FINITE s ==> !x. x IN s ==> x <= SETMAX s`,
 316   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 317   REWRITE_TAC[NOT_IN_EMPTY; IN_INSERT] THEN
 318   REPEAT GEN_TAC THEN STRIP_TAC THEN
 319   ASM_SIMP_TAC [SETMAX_LEMMA] THEN
 320   ASM_REWRITE_TAC[MAX] THEN
 321   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
 322   ASM_REWRITE_TAC[LE_REFL] THEN
 323   ASM_MESON_TAC[LE_CASES; LE_TRANS]);;
 324
 325 let SETMAX_THM = prove
 326  (`(SETMAX {} = 0) /\
 327    (!x s. FINITE s ==>
 328            (SETMAX (x INSERT s) = MAX x (SETMAX s)))`,
 329   REPEAT STRIP_TAC THEN ASM_SIMP_TAC [SETMAX_LEMMA] THEN
 330   COND_CASES_TAC THEN REWRITE_TAC[MAX] THEN
 331   COND_CASES_TAC THEN ASM_MESON_TAC[SETMAX_MEMBER]);;
 332
 333 let SETMAX_UNION = prove
 334  (`!s t. FINITE(s UNION t)
 335          ==> (SETMAX(s UNION t) = MAX (SETMAX s) (SETMAX t))`,
 336   let lemma = prove(`(x INSERT s) UNION t = x INSERT (s UNION t)`,SET_TAC[]) in
 337   SUBGOAL_THEN `!t. FINITE(t) ==> !s. FINITE(s) ==>
 338                         (SETMAX(s UNION t) = MAX (SETMAX s) (SETMAX t))`
 339    (fun th -> MESON_TAC[th; FINITE_UNION]) THEN
 340   GEN_TAC THEN DISCH_TAC THEN
 341   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 342   REWRITE_TAC[UNION_EMPTY; SETMAX_THM] THEN CONJ_TAC THENL
 343    [REWRITE_TAC[MAX; LE_0]; ALL_TAC] THEN
 344   REPEAT STRIP_TAC THEN REWRITE_TAC[lemma] THEN
 345   ASM_SIMP_TAC [SETMAX_THM; FINITE_UNION] THEN
 346   REWRITE_TAC[MAX_ASSOC]);;
 347
 348 let VARIANT_FINITE = prove
 349  (`!s:num->bool. FINITE(s) ==> ~(VARIANT(s) IN s)`,
 350   REWRITE_TAC[VARIANT] THEN
 351   MESON_TAC[SETMAX_MEMBER; ARITH_RULE `~(x + 1 <= x)`]);;
 352
 353 let VARIANT_THM = prove
 354  (`!p. ~(VARIANT(FV p) IN FV(p))`,
 355   GEN_TAC THEN MATCH_MP_TAC VARIANT_FINITE THEN REWRITE_TAC[FV_FINITE]);;
 356
 357 let NOT_IN_VARIANT = prove
 358  (`!s t. FINITE s /\ t SUBSET s ==> ~(VARIANT(s) IN t)`,
 359   MESON_TAC[SUBSET; VARIANT_FINITE]);;
 360
 361 (* ------------------------------------------------------------------------- *)
 362 (* Substitution within terms.                                                *)
 363 (* ------------------------------------------------------------------------- *)
 364
 365 let termsubst = new_recursive_definition term_RECURSION
 366  `(termsubst v Z = Z) /\
 367   (!x. termsubst v (V x) = v(x)) /\
 368   (!t. termsubst v (Suc t) = Suc(termsubst v t)) /\
 369   (!s t. termsubst v (s ++ t) = termsubst v s ++ termsubst v t) /\
 370   (!s t. termsubst v (s ** t) = termsubst v s ** termsubst v t)`;;
 371
 372 let TERMVAL_TERMSUBST = prove
 373  (`!v i t. termval v (termsubst i t) = termval (termval v o i) t`,
 374   GEN_TAC THEN GEN_TAC THEN
 375   MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termval; termsubst; o_THM]);;
 376
 377 let TERMSUBST_TERMSUBST = prove
 378  (`!i j t. termsubst j (termsubst i t) = termsubst (termsubst j o i) t`,
 379   GEN_TAC THEN GEN_TAC THEN
 380   MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termval; termsubst; o_THM]);;
 381
 382 let TERMSUBST_TRIV = prove
 383  (`!t. termsubst V t = t`,
 384   MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termsubst]);;
 385
 386 let TERMSUBST_EQ = prove
 387  (`!t v v'. (!x. x IN (FVT t) ==> (v'(x) = v(x)))
 388             ==> (termsubst v' t = termsubst v t)`,
 389   MATCH_MP_TAC term_INDUCT THEN
 390   SIMP_TAC[termsubst; FVT; IN_SING; IN_UNION] THEN MESON_TAC[]);;
 391
 392 let TERMSUBST_FVT = prove
 393  (`!t i. FVT(termsubst i t) = {x | ?y. y IN FVT(t) /\ x IN FVT(i y)}`,
 394   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 395   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[FVT; termsubst] THEN
 396   REWRITE_TAC[IN_UNION; IN_SING; NOT_IN_EMPTY] THEN MESON_TAC[]);;
 397
 398 let TERMSUBST_ASSIGN = prove
 399  (`!x s t. ~(x IN FVT t) ==> (termsubst (x |=> s) t = t)`,
 400   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM TERMSUBST_TRIV] THEN
 401   MATCH_MP_TAC TERMSUBST_EQ THEN
 402   REWRITE_TAC[ASSIGN] THEN ASM_MESON_TAC[]);;
 403
 404 let TERMSUBST_TRIVIAL = prove
 405  (`!v t. (!x. x IN FVT t ==> v x = V x) ==> termsubst v t = t`,
 406   MESON_TAC[TERMSUBST_EQ; TERMSUBST_TRIV]);;
 407
 408 (* ------------------------------------------------------------------------- *)
 409 (* Formula substitution --- somewhat less trivial.                           *)
 410 (* ------------------------------------------------------------------------- *)
 411
 412 let formsubst = new_recursive_definition form_RECURSION
 413   `(formsubst v False = False) /\
 414    (formsubst v True = True) /\
 415    (formsubst v (s === t) = termsubst v s === termsubst v t) /\
 416    (formsubst v (s << t) = termsubst v s << termsubst v t) /\
 417    (formsubst v (s <<= t) = termsubst v s <<= termsubst v t) /\
 418    (formsubst v (Not p) = Not(formsubst v p)) /\
 419    (formsubst v (p && q) = formsubst v p && formsubst v q) /\
 420    (formsubst v (p || q) = formsubst v p || formsubst v q) /\
 421    (formsubst v (p --> q) = formsubst v p --> formsubst v q) /\
 422    (formsubst v (p <-> q) = formsubst v p <-> formsubst v q) /\
 423    (formsubst v (!!x q) =
 424         let z = if ?y. y IN FV(!!x q) /\ x IN FVT(v(y))
 425                 then VARIANT(FV(formsubst ((x |-> V x) v) q)) else x in
 426         !!z (formsubst ((x |-> V(z)) v) q)) /\
 427    (formsubst v (??x q) =
 428         let z = if ?y. y IN FV(??x q) /\ x IN FVT(v(y))
 429                 then VARIANT(FV(formsubst ((x |-> V x) v) q)) else x in
 430         ??z (formsubst ((x |-> V(z)) v) q))`;;
 431
 432 let FORMSUBST_PROPERTIES = prove
 433  (`!p. (!i. FV(formsubst i p) = {x | ?y. y IN FV(p) /\ x IN FVT(i y)}) /\
 434        (!i v. holds v (formsubst i p) = holds (termval v o i) p)`,
 435   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 436   MATCH_MP_TAC form_INDUCT THEN
 437   REWRITE_TAC[FV; holds; formsubst; TERMSUBST_FVT; IN_ELIM_THM; NOT_IN_EMPTY;
 438               IN_UNION; TERMVAL_TERMSUBST] THEN
 439   REPEAT(CONJ_TAC THENL [MESON_TAC[];ALL_TAC]) THEN CONJ_TAC THEN
 440   (MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN STRIP_TAC THEN
 441    REWRITE_TAC[AND_FORALL_THM] THEN X_GEN_TAC `i:num->term` THEN
 442    LET_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
 443    SUBGOAL_THEN `~(?y. y IN (FV(p) DELETE x) /\ z IN FVT(i y))`
 444    ASSUME_TAC THENL
 445     [EXPAND_TAC "z" THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 446      MP_TAC(SPEC `formsubst ((x |-> V x) i) p` VARIANT_THM) THEN
 447      ASM_REWRITE_TAC[valmod; IN_DELETE; CONTRAPOS_THM] THEN
 448      MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[];
 449      ALL_TAC] THEN
 450    CONJ_TAC THEN GEN_TAC THEN ASM_REWRITE_TAC[FV; IN_DELETE; holds] THENL
 451     [REWRITE_TAC[LEFT_AND_EXISTS_THM; valmod] THEN AP_TERM_TAC THEN
 452      ABS_TAC THEN COND_CASES_TAC THEN ASM_MESON_TAC[FVT; IN_SING; IN_DELETE];
 453      AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HOLDS_VALUATION THEN
 454      GEN_TAC THEN REWRITE_TAC[valmod; o_DEF] THEN COND_CASES_TAC THEN
 455      ASM_REWRITE_TAC[termval] THEN DISCH_TAC THEN
 456      MATCH_MP_TAC TERMVAL_VALUATION THEN GEN_TAC THEN
 457      REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_MESON_TAC[IN_DELETE]]));;
 458
 459 let FORMSUBST_FV = prove
 460  (`!p i. FV(formsubst i p) = {x | ?y. y IN FV(p) /\ x IN FVT(i y)}`,
 461   REWRITE_TAC[FORMSUBST_PROPERTIES]);;
 462
 463 let HOLDS_FORMSUBST = prove
 464  (`!p i v. holds v (formsubst i p) <=> holds (termval v o i) p`,
 465   REWRITE_TAC[FORMSUBST_PROPERTIES]);;
 466
 467 let FORMSUBST_EQ = prove
 468  (`!p i j. (!x. x IN FV(p) ==> (i(x) = j(x)))
 469            ==> (formsubst i p = formsubst j p)`,
 470   MATCH_MP_TAC form_INDUCT THEN
 471   REWRITE_TAC[FV; formsubst; IN_UNION; IN_DELETE] THEN
 472   SIMP_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN
 473   GEN_REWRITE_TAC I [GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
 474    [MESON_TAC[TERMSUBST_EQ]; ALL_TAC] THEN
 475   CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
 476   (DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`i:num->term`; `j:num->term`] THEN
 477    DISCH_TAC THEN REWRITE_TAC[LET_DEF; LET_END_DEF; form_INJ] THEN
 478    MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN SIMP_TAC[] THEN
 479    CONJ_TAC THENL
 480     [ALL_TAC;
 481      DISCH_THEN(K ALL_TAC) THEN FIRST_ASSUM MATCH_MP_TAC THEN
 482      REWRITE_TAC[valmod] THEN ASM_SIMP_TAC[]] THEN
 483    AP_THM_TAC THEN BINOP_TAC THENL
 484     [ASM_MESON_TAC[];
 485      AP_TERM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 486      REWRITE_TAC[valmod] THEN ASM_MESON_TAC[]]));;
 487
 488 let FORMSUBST_TRIV = prove
 489  (`!p. formsubst V p = p`,
 490   MATCH_MP_TAC form_INDUCT THEN
 491   SIMP_TAC[formsubst; TERMSUBST_TRIV] THEN
 492   REWRITE_TAC[FVT; IN_SING; FV; IN_DELETE] THEN
 493   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
 494   ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; VALMOD_REPEAT] THEN
 495   ASM_MESON_TAC[]);;
 496
 497 let FORMSUBST_TRIVIAL = prove
 498  (`!v p. (!x. x IN FV(p) ==> v x = V x) ==> formsubst v p = p`,
 499   MESON_TAC[FORMSUBST_EQ; FORMSUBST_TRIV]);;
 500
 501 (* ------------------------------------------------------------------------- *)
 502 (* Predicate ensuring that a substitution will not cause variable renaming.  *)
 503 (* ------------------------------------------------------------------------- *)
 504
 505 let safe_for = new_definition
 506  `safe_for x v <=> !y. x IN FVT(v y) ==> y = x`;;
 507
 508 let SAFE_FOR_V = prove
 509  (`!x. safe_for x V`,
 510   SIMP_TAC[safe_for; FVT; IN_SING]);;
 511
 512 let SAFE_FOR_VALMOD = prove
 513  (`!v x y t. safe_for x v /\ (x IN FVT t ==> y = x)
 514              ==> safe_for x ((y |-> t) v)`,
 515   REWRITE_TAC[safe_for; VALMOD] THEN MESON_TAC[]);;
 516
 517 let SAFE_FOR_ASSIGN = prove
 518  (`!x y t. safe_for x (y |=> t) <=> x IN FVT t ==> y = x`,
 519   REWRITE_TAC[safe_for; ASSIGN] THEN MESON_TAC[FVT; IN_SING]);;
 520
 521 let FORMSUBST_SAFE_FOR = prove
 522  (`(!v x p. safe_for x v
 523             ==> formsubst v (!! x p) = !!x (formsubst ((x |-> V x) v) p)) /\
 524    (!v x p. safe_for x v
 525             ==> formsubst v (?? x p) = ??x (formsubst ((x |-> V x) v) p))`,
 526   REWRITE_TAC[safe_for; formsubst; LET_DEF; LET_END_DEF; FV] THEN
 527   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN ASM SET_TAC[]);;
 528
 529 (* ------------------------------------------------------------------------- *)
 530 (* Quasi-substitution.                                                       *)
 531 (* ------------------------------------------------------------------------- *)
 532
 533 let qsubst = new_definition
 534  `qsubst (x,t) p = ??x (V x === t && p)`;;
 535
 536 let FV_QSUBST = prove
 537  (`!x n p. FV(qsubst (x,t) p) = (FV(p) UNION FVT(t)) DELETE x`,
 538   REWRITE_TAC[qsubst; FV; FVT] THEN SET_TAC[]);;
 539
 540 let HOLDS_QSUBST = prove
 541  (`!v t p v. ~(x IN FVT(t))
 542              ==> (holds v (qsubst (x,t) p) <=>
 543                   holds ((x |-> termval v t) v) p)`,
 544   REPEAT STRIP_TAC THEN
 545   SUBGOAL_THEN `!v z. termval ((x |-> z) v) t = termval v t` ASSUME_TAC THENL
 546    [REWRITE_TAC[valmod] THEN ASM_MESON_TAC[TERMVAL_VALUATION];
 547     ASM_REWRITE_TAC[holds; qsubst; termval; VALMOD_BASIC; UNWIND_THM2]]);;
 548
 549 (* ------------------------------------------------------------------------- *)
 550 (* The numeral mapping.                                                      *)
 551 (* ------------------------------------------------------------------------- *)
 552
 553 let numeral = new_recursive_definition num_RECURSION
 554   `(numeral 0 = Z) /\
 555    (!n. numeral (SUC n) = Suc(numeral n))`;;
 556
 557 let TERMVAL_NUMERAL = prove
 558  (`!v n. termval v (numeral n) = n`,
 559   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[termval;numeral]);;
 560
 561 let FVT_NUMERAL = prove
 562  (`!n. FVT(numeral n) = {}`,
 563   INDUCT_TAC THEN ASM_REWRITE_TAC[FVT; numeral]);;
 564
 565 (* ------------------------------------------------------------------------- *)
 566 (* Closed-ness.                                                              *)
 567 (* ------------------------------------------------------------------------- *)
 568
 569 let closed = new_definition
 570   `closed p <=> (FV p = {})`;;