1 (* ========================================================================= *)
2 (* Derived properties of provability. *)
3 (* ========================================================================= *)
5 let negativef = new_definition
6 `negativef p = ?q. p = q --> False`;;
8 let negatef = new_definition
9 `negatef p = if negativef p then @q. p = q --> False else p --> False`;;
11 (* ------------------------------------------------------------------------- *)
12 (* The primitive basis, separated into its named components. *)
13 (* ------------------------------------------------------------------------- *)
15 let axiom_addimp = prove
16 (`!A p q. A |-- p --> (q --> p)`,
17 MESON_TAC[proves_RULES; axiom_RULES]);;
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]);;
23 let axiom_doubleneg = prove
24 (`!A p. A |-- ((p --> False) --> False) --> p`,
25 MESON_TAC[proves_RULES; axiom_RULES]);;
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]);;
31 let axiom_impall = prove
32 (`!A x p. ~(x IN FV p) ==> A |-- p --> !!x p`,
33 MESON_TAC[proves_RULES; axiom_RULES]);;
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]);;
39 let axiom_eqrefl = prove
40 (`!A t. A |-- t === t`,
41 MESON_TAC[proves_RULES; axiom_RULES]);;
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]);;
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]);;
55 let axiom_iffimp1 = prove
56 (`!A p q. A |-- (p <-> q) --> p --> q`,
57 MESON_TAC[proves_RULES; axiom_RULES]);;
59 let axiom_iffimp2 = prove
60 (`!A p q. A |-- (p <-> q) --> q --> p`,
61 MESON_TAC[proves_RULES; axiom_RULES]);;
63 let axiom_impiff = prove
64 (`!A p q. A |-- (p --> q) --> (q --> p) --> (p <-> q)`,
65 MESON_TAC[proves_RULES; axiom_RULES]);;
67 let axiom_true = prove
68 (`A |-- True <-> (False --> False)`,
69 MESON_TAC[proves_RULES; axiom_RULES]);;
72 (`!A p. A |-- Not p <-> (p --> False)`,
73 MESON_TAC[proves_RULES; axiom_RULES]);;
76 (`!A p q. A |-- (p && q) <-> (p --> q --> False) --> False`,
77 MESON_TAC[proves_RULES; axiom_RULES]);;
80 (`!A p q. A |-- (p || q) <-> Not(Not p && Not q)`,
81 MESON_TAC[proves_RULES; axiom_RULES]);;
83 let axiom_exists = prove
84 (`!A x p. A |-- (??x p) <-> Not(!!x (Not p))`,
85 MESON_TAC[proves_RULES; axiom_RULES]);;
88 (`!A p. p IN A ==> A |-- p`,
89 MESON_TAC[proves_RULES]);;
91 let modusponens = prove
92 (`!A p. A |-- (p --> q) /\ A |-- p ==> A |-- q`,
93 MESON_TAC[proves_RULES]);;
96 (`!A p x. A |-- p ==> A |-- !!x p`,
97 MESON_TAC[proves_RULES]);;
99 (* ------------------------------------------------------------------------- *)
100 (* Some purely propositional schemas and derived rules. *)
101 (* ------------------------------------------------------------------------- *)
104 (`!A p q. A |-- p <-> q ==> A |-- p --> q`,
105 MESON_TAC[modusponens; axiom_iffimp1]);;
108 (`!A p q. A |-- p <-> q ==> A |-- q --> p`,
109 MESON_TAC[modusponens; axiom_iffimp2]);;
111 let imp_antisym = prove
112 (`!A p q. A |-- p --> q /\ A |-- q --> p ==> A |-- p <-> q`,
113 MESON_TAC[modusponens; axiom_impiff]);;
115 let add_assum = prove
116 (`!A p q. A |-- q ==> A |-- p --> q`,
117 MESON_TAC[modusponens; axiom_addimp]);;
120 (`!A p. A |-- p --> p`,
121 MESON_TAC[modusponens; axiom_distribimp; axiom_addimp]);;
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]);;
127 let imp_unduplicate = prove
128 (`!A p q. A |-- p --> p --> q ==> A |-- p --> q`,
129 MESON_TAC[modusponens; axiom_distribimp; imp_refl]);;
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]);;
136 (`!A p q r. A |-- p --> q --> r ==> A |-- q --> p --> r`,
137 MESON_TAC[imp_trans; axiom_addimp; modusponens; axiom_distribimp]);;
139 let imp_trans_chain_2 = prove
140 (`!A p q1 q2 r. A |-- p --> q1 /\ A |-- p --> q2 /\ A |-- q1 --> q2 --> r
142 ASM_MESON_TAC[imp_trans; imp_swap; imp_unduplicate]);;
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]);;
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]);;
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]);;
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]);;
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]);;
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]);;
168 let imp_insert = prove
169 (`!A p q r. A |-- p --> r ==> A |-- p --> q --> r`,
170 MESON_TAC[imp_trans; axiom_addimp]);;
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]);;
177 (`!A p. A |-- False --> p`,
178 MESON_TAC[imp_trans; axiom_addimp; axiom_doubleneg]);;
180 let imp_contr = prove
181 (`!A p q. A |-- (p --> False) --> (p --> r)`,
182 MESON_TAC[imp_add_assum; ex_falso]);;
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]);;
192 (`!A p. A |-- (p --> False) --> p ==> A |-- p`,
193 MESON_TAC[modusponens; axiom_distribimp; imp_refl; axiom_doubleneg]);;
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]);;
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]);;
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]);;
212 MESON_TAC[modusponens; axiom_true; imp_refl; iff_imp2]);;
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]);;
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]);;
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]);;
230 (`!A p q. A |-- p && q <=> A |-- p /\ A |-- q`,
231 MESON_TAC[and_left; and_right; and_pair; modusponens]);;
234 (`!A p q r. A |-- p && q --> r ==> A |-- p --> q --> r`,
235 MESON_TAC[modusponens; imp_add_assum; and_pair]);;
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]);;
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]);;
246 (`!A p q. A |-- p <-> q <=> A |-- q <-> p`,
247 MESON_TAC[iff_imp1; iff_imp2; imp_antisym]);;
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]);;
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]);;
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]);;
263 (`!A p q. A |-- q --> p || q`,
264 MESON_TAC[imp_trans; not_not; iff_imp2; and_right; contrapos; axiom_or]);;
267 (`!A p q. A |-- p --> p || q`,
268 MESON_TAC[imp_trans; not_not; iff_imp2; and_left; contrapos; axiom_or]);;
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]);;
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]);;
283 (`!A p. A |-- p <-> p`,
284 MESON_TAC[imp_antisym; imp_refl]);;
286 (* ------------------------------------------------------------------------- *)
287 (* Equality rules. *)
288 (* ------------------------------------------------------------------------- *)
291 (`!A s t. A |-- s === t --> t === s`,
292 MESON_TAC[axiom_eqrefl; modusponens; imp_swap; axiom_predcong]);;
294 let icongruence_general = prove
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]]);;
309 let icongruence = prove
311 A |-- s === t --> termsubst (x |=> s) tm === termsubst (x |=> t) tm`,
312 REWRITE_TAC[assign; icongruence_general]);;
314 let icongruence_var = prove
316 A |-- V x === t --> tm === termsubst (x |=> t) tm`,
317 MESON_TAC[icongruence; TERMSUBST_TRIV; ASSIGN_TRIV]);;
319 (* ------------------------------------------------------------------------- *)
320 (* First-order rules. *)
321 (* ------------------------------------------------------------------------- *)
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]);;
329 (`!x p q. A |-- p --> q ==> A |-- (!!x p) --> (!!x q)`,
330 MESON_TAC[modusponens; axiom_allimp; gen]);;
333 (`!x p q. A |-- p --> q ==> A |-- (??x p) --> (??x q)`,
334 MESON_TAC[contrapos; genimp; contrapos; imp_trans; iff_imp1; iff_imp2;
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))`
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];
346 SUBGOAL_THEN `A |-- (q --> False) --> !!x p --> !!x (Not(p --> q))`
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`
352 [ASM_MESON_TAC[modusponens; iff_imp1; axiom_exists; axiom_not; imp_trans_th];
354 ASM_MESON_TAC[imp_trans; imp_swap; axiom_doubleneg]);;
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]);;
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
367 [FIRST_X_ASSUM SUBST_ALL_TAC THEN
368 ASM_MESON_TAC[genimp; modusponens; axiom_eqrefl];
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]);;
374 (* ------------------------------------------------------------------------- *)
375 (* We'll perform induction on this measure. *)
376 (* ------------------------------------------------------------------------- *)
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)`;;
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]);;
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];
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;
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
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))
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))
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]);
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];
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)`
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
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];
497 FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP VALMOD_SWAP th]) THEN
498 ASM_MESON_TAC[imp_mono_th; modusponens]] THEN
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]);;
519 (`!A p x s t. A |-- s === t
520 --> formsubst (x |=> s) p --> formsubst (x |=> t) p`,
521 REWRITE_TAC[assign; isubst_general]);;
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]);;
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]);;
534 (* ------------------------------------------------------------------------- *)
535 (* To conclude cleanly, useful to have all variables. *)
536 (* ------------------------------------------------------------------------- *)
538 let VARS = new_recursive_definition form_RECURSION
539 `(VARS False = {}) /\
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)`;;
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]);;
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[]);;
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]);;
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]);;
578 let FORMSUBST_TWICE_GENERAL = prove
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
590 REWRITE_TAC[FV; FORMSUBST_FV; TERMSUBST_FVT; o_THM;
591 IN_ELIM_THM; IN_DELETE] THEN
593 `(?y. ((?y'. y' IN FV p /\ y IN FVT ((x |-> V x) i y')) /\ ~(y = x)) /\
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])
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];
611 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
612 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
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])
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)}`];
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]);;
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]);;
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]);;
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];
675 `formsubst (x |=> t) p =
676 formsubst (z |=> t) (formsubst (x |=> V z) p)`
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]]);;
684 (`!A x p t. A |-- !!x p ==> A |-- formsubst (x |=> t) p`,
685 MESON_TAC[ispec; modusponens]);;
688 (`!A x p. A |-- !!x p ==> A |-- p`,
690 DISCH_THEN(MP_TAC o SPEC `V x` o MATCH_MP spec) THEN
691 SIMP_TAC[ASSIGN_TRIV; FORMSUBST_TRIVIAL]);;
693 let instantiation = prove
694 (`!A v p. A |-- p ==> A |-- formsubst v p`,
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) /\
699 ==> A |-- formsubst v p`,
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
716 [REPEAT GEN_TAC THEN REWRITE_TAC[VALMOD] THEN
717 COND_CASES_TAC THEN ASM_SIMP_TAC[FVT; IN_SING] THEN ASM_MESON_TAC[];
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
726 REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; NOT_EXISTS_THM; VALMOD] 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
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];
740 formsubst (\i. v(i - n)) (formsubst (\i. V(i + n)) p)`
742 [W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_TWICE_GENERAL o
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
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]]]);;
762 (* ------------------------------------------------------------------------- *)
763 (* Monotonicity and the deduction theorem. *)
764 (* ------------------------------------------------------------------------- *)
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]);;
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]]);;
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]);;
787 (* ------------------------------------------------------------------------- *)
788 (* A few more derived rules. *)
789 (* ------------------------------------------------------------------------- *)
792 (`!A s t u. A |-- s === t --> t === u --> s === u`,
793 MESON_TAC[axiom_predcong; modusponens; imp_swap; axiom_eqrefl; imp_trans;
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]);;
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]);;
804 let eq_sym_rule = prove
805 (`!A s t. A |-- s === t <=> A |-- t === s`,
806 MESON_TAC[modusponens; eq_sym]);;
809 (`!A x p q. A |-- p --> q ==> A |-- !!x p --> !!x q`,
810 MESON_TAC[axiom_allimp; modusponens; gen]);;
813 (`!A x p q. A |-- p <-> q ==> A |-- !!x p <-> !!x q`,
814 MESON_TAC[allimp; iff_imp1; iff_imp2; imp_antisym]);;
817 (`!A x p q. A |-- p <-> q ==> A |-- ??x p <-> ??x q`,
818 MESON_TAC[eximp; iff_imp1; iff_imp2; imp_antisym]);;
821 (`!A s t. A |-- s === t ==> A |-- Suc s === Suc t`,
822 MESON_TAC[modusponens; axiom_funcong]);;
825 (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ++ u === t ++ v`,
826 MESON_TAC[modusponens; axiom_funcong]);;
829 (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ** u === t ** v`,
830 MESON_TAC[modusponens; axiom_funcong]);;
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]);;
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]);;
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]);;
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]);;
855 let exists_intro = prove
856 (`!A x t p. A |-- formsubst (x |=> t) p ==> A |-- ??x p`,
857 MESON_TAC[iexists; modusponens]);;
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]);;
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]);;
875 let eq_trans_imp = prove
876 (`A |-- s === s' /\ A |-- t === t' ==> A |-- s === t --> s' === t'`,
877 MESON_TAC[axiom_predcong; modusponens]);;
879 (* ------------------------------------------------------------------------- *)
880 (* Some conversions for performing explicit substitution operations in what *)
881 (* we hope is the common case where no variable renaming occurs. *)
882 (* ------------------------------------------------------------------------- *)
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];;
892 let IN_FV_RULE ths tm =
894 ((GEN_REWRITE_CONV TOP_DEPTH_CONV
895 ([IN_UNION; IN_DELETE; NOT_IN_EMPTY; IN_INSERT] @
896 ths @ !fv_theorems) THENC
898 with Failure _ -> ASSUME tm;;
900 let rec SAFE_FOR_RULE tm =
901 try PART_MATCH I SAFE_FOR_V tm
903 try let th1 = PART_MATCH lhand SAFE_FOR_ASSIGN tm in
904 let th2 = IN_FV_RULE [] (rand(concl th1)) in
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
913 GEN_REWRITE_CONV TOP_DEPTH_CONV [ASSIGN; VALMOD] THENC NUM_REDUCE_CONV;;
915 let TERMSUBST_NUMERAL = prove
916 (`!v n. termsubst v (numeral n) = numeral n`,
917 SIMP_TAC[TERMSUBST_TRIVIAL; FVT_NUMERAL; NOT_IN_EMPTY]);;
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
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;;
928 let rec FORMSUBST_CONV tm =
930 [el 0 (CONJUNCTS formsubst); el 1 (CONJUNCTS formsubst)] ORELSEC
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
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
942 try PART_MATCH (lhand o rand) (CONJUNCT1 FORMSUBST_SAFE_FOR) tm
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;;
948 (* ------------------------------------------------------------------------- *)
949 (* Hence a more convenient specialization rule. *)
950 (* ------------------------------------------------------------------------- *)
952 let spec_var_rule th = MATCH_MP spec_var th;;
954 let spec_all_rule = repeat spec_var_rule;;
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));;
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);;
969 let spec_rule t th = specl_rule [t] th;;
971 let gen_rule t th = SPEC (mk_small_numeral t) (MATCH_MP gen th);;
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);;
980 let gen_tac n = gens_tac [n];;