1 (* ========================================================================= *)
2 (* First order logic based on the language of arithmetic. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
9 (* ------------------------------------------------------------------------- *)
11 parse_as_infix("++",(20,"right"));;
12 parse_as_infix("**",(22,"right"));;
14 let term_INDUCT,term_RECURSION = define_type
21 let term_CASES = prove_cases_thm term_INDUCT;;
23 let term_DISTINCT = distinctness "term";;
25 let term_INJ = injectivity "term";;
27 (* ------------------------------------------------------------------------- *)
28 (* Syntax of formulas. *)
29 (* ------------------------------------------------------------------------- *)
31 parse_as_infix("===",(18,"right"));;
32 parse_as_infix("<<",(18,"right"));;
33 parse_as_infix("<<=",(18,"right"));;
35 parse_as_infix("&&",(16,"right"));;
36 parse_as_infix("||",(15,"right"));;
37 parse_as_infix("-->",(14,"right"));;
38 parse_as_infix("<->",(13,"right"));;
40 let form_INDUCT,form_RECURSION = define_type
54 let form_CASES = prove_cases_thm form_INDUCT;;
56 let form_DISTINCT = distinctness "form";;
58 let form_INJ = injectivity "form";;
60 (* ------------------------------------------------------------------------- *)
61 (* Semantics of terms and formulas in the standard model. *)
62 (* ------------------------------------------------------------------------- *)
64 parse_as_infix("|->",(22,"right"));;
66 let valmod = new_definition
67 `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
69 let termval = new_recursive_definition term_RECURSION
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)`;;
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)`;;
90 let true_def = new_definition
91 `true p <=> !v. holds v p`;;
94 (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
95 REWRITE_TAC[valmod]);;
97 let VALMOD_BASIC = prove
98 (`!v x y. (x |-> y) v x = y`,
99 REWRITE_TAC[valmod]);;
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[]);;
106 let VALMOD_REPEAT = prove
107 (`!v x. (x |-> v(x)) v = v`,
108 REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
110 let FORALL_VALMOD = prove
111 (`!x. (!v a. P((x |-> a) v)) <=> (!v. P v)`,
112 MESON_TAC[VALMOD_REPEAT]);;
114 let VALMOD_SWAP = prove
116 ~(x = y) ==> ((x |-> a) ((y |-> b) v) = (y |-> b) ((x |-> a) v))`,
117 REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
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[]);;
123 (* ------------------------------------------------------------------------- *)
125 (* ------------------------------------------------------------------------- *)
127 parse_as_infix("|=>",(22,"right"));;
129 let assign = new_definition
130 `(x |=> a) = (x |-> a) V`;;
133 (`!x y a. (x |=> a) y = if y = x then a else V(y)`,
134 REWRITE_TAC[assign; valmod]);;
136 let ASSIGN_TRIV = prove
137 (`!x. (x |=> V x) = V`,
138 REWRITE_TAC[VALMOD_REPEAT; assign]);;
140 (* ------------------------------------------------------------------------- *)
141 (* Variables in a term and free variables in a formula. *)
142 (* ------------------------------------------------------------------------- *)
144 let FVT = new_recursive_definition term_RECURSION
147 (FVT (Suc t) = FVT t) /\
148 (FVT (s ++ t) = (FVT s) UNION (FVT t)) /\
149 (FVT (s ** t) = (FVT s) UNION (FVT t))`;;
151 let FV = new_recursive_definition form_RECURSION
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)`;;
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]);;
170 let FV_FINITE = prove
172 MATCH_MP_TAC form_INDUCT THEN
173 SIMP_TAC[FV; FVT_FINITE; FINITE_RULES; FINITE_DELETE; FINITE_UNION]);;
175 (* ------------------------------------------------------------------------- *)
176 (* Logical axioms. *)
177 (* ------------------------------------------------------------------------- *)
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))))`;;
202 (* ------------------------------------------------------------------------- *)
203 (* Deducibility from additional set of nonlogical axioms. *)
204 (* ------------------------------------------------------------------------- *)
206 parse_as_infix("|--",(11,"right"));;
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))`;;
213 (* ------------------------------------------------------------------------- *)
215 (* ------------------------------------------------------------------------- *)
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[]);;
224 let HOLDS_VALUATION = prove
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
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]);;
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]);;
243 (* ------------------------------------------------------------------------- *)
244 (* Proof of soundness. *)
245 (* ------------------------------------------------------------------------- *)
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
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
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[];
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]);;
285 (* ------------------------------------------------------------------------- *)
286 (* Variant variables for use in renaming substitution. *)
287 (* ------------------------------------------------------------------------- *)
290 (`!x y. MAX x y = MAX y x`,
293 let MAX_ASSOC = prove
294 (`!x y z. MAX x (MAX y z) = MAX (MAX x y) z`,
297 let SETMAX = new_definition
298 `SETMAX s = ITSET MAX s 0`;;
300 let VARIANT = new_definition
301 `VARIANT s = SETMAX s + 1`;;
303 let SETMAX_LEMMA = prove
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]);;
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]);;
325 let SETMAX_THM = prove
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]);;
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]);;
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)`]);;
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]);;
357 let NOT_IN_VARIANT = prove
358 (`!s t. FINITE s /\ t SUBSET s ==> ~(VARIANT(s) IN t)`,
359 MESON_TAC[SUBSET; VARIANT_FINITE]);;
361 (* ------------------------------------------------------------------------- *)
362 (* Substitution within terms. *)
363 (* ------------------------------------------------------------------------- *)
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)`;;
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]);;
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]);;
382 let TERMSUBST_TRIV = prove
383 (`!t. termsubst V t = t`,
384 MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termsubst]);;
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[]);;
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[]);;
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[]);;
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]);;
408 (* ------------------------------------------------------------------------- *)
409 (* Formula substitution --- somewhat less trivial. *)
410 (* ------------------------------------------------------------------------- *)
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))`;;
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))`
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[];
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]]));;
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]);;
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]);;
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
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
485 AP_TERM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
486 REWRITE_TAC[valmod] THEN ASM_MESON_TAC[]]));;
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
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]);;
501 (* ------------------------------------------------------------------------- *)
502 (* Predicate ensuring that a substitution will not cause variable renaming. *)
503 (* ------------------------------------------------------------------------- *)
505 let safe_for = new_definition
506 `safe_for x v <=> !y. x IN FVT(v y) ==> y = x`;;
508 let SAFE_FOR_V = prove
510 SIMP_TAC[safe_for; FVT; IN_SING]);;
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[]);;
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]);;
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[]);;
529 (* ------------------------------------------------------------------------- *)
530 (* Quasi-substitution. *)
531 (* ------------------------------------------------------------------------- *)
533 let qsubst = new_definition
534 `qsubst (x,t) p = ??x (V x === t && p)`;;
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[]);;
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]]);;
549 (* ------------------------------------------------------------------------- *)
550 (* The numeral mapping. *)
551 (* ------------------------------------------------------------------------- *)
553 let numeral = new_recursive_definition num_RECURSION
555 (!n. numeral (SUC n) = Suc(numeral n))`;;
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]);;
561 let FVT_NUMERAL = prove
562 (`!n. FVT(numeral n) = {}`,
563 INDUCT_TAC THEN ASM_REWRITE_TAC[FVT; numeral]);;
565 (* ------------------------------------------------------------------------- *)
567 (* ------------------------------------------------------------------------- *)
569 let closed = new_definition
570 `closed p <=> (FV p = {})`;;