1 (* ========================================================================= *)
2 (* Sigma_1 completeness of Robinson's axioms Q. *)
3 (* ========================================================================= *)
5 let robinson = new_definition
7 (!!0 (!!1 (Suc(V 0) === Suc(V 1) --> V 0 === V 1))) &&
8 (!!1 (Not(V 1 === Z) <-> ??0 (V 1 === Suc(V 0)))) &&
9 (!!1 (Z ++ V 1 === V 1)) &&
10 (!!0 (!!1 (Suc(V 0) ++ V 1 === Suc(V 0 ++ V 1)))) &&
11 (!!1 (Z ** V 1 === Z)) &&
12 (!!0 (!!1 (Suc(V 0) ** V 1 === V 1 ++ V 0 ** V 1))) &&
13 (!!0 (!!1 (V 0 <<= V 1 <-> ??2 (V 0 ++ V 2 === V 1)))) &&
14 (!!0 (!!1 (V 0 << V 1 <-> Suc(V 0) <<= V 1)))`;;
16 (* ------------------------------------------------------------------------- *)
17 (* Individual "axioms" and their instances. *)
18 (* ------------------------------------------------------------------------- *)
20 let [suc_inj; num_cases; add_0; add_suc; mul_0; mul_suc; le_def; lt_def] =
21 CONJUNCTS(REWRITE_RULE[META_AND] (GEN_REWRITE_RULE RAND_CONV [robinson]
22 (MATCH_MP assume (SET_RULE `robinson IN {robinson}`))));;
25 (`!s t. {robinson} |-- Suc(s) === Suc(t) --> s === t`,
26 REWRITE_TAC[specl_rule [`s:term`; `t:term`] suc_inj]);;
28 let num_cases' = prove
30 ==> {robinson} |-- (Not(t === Z) <-> ??z (t === Suc(V z)))`,
32 MP_TAC(SPEC `t:term` (MATCH_MP spec num_cases)) THEN
33 REWRITE_TAC[formsubst] THEN
34 CONV_TAC(ONCE_DEPTH_CONV TERMSUBST_CONV) THEN
35 REWRITE_TAC[FV; FVT; SET_RULE `({1} UNION {0}) DELETE 0 = {1} DIFF {0}`] THEN
36 REWRITE_TAC[IN_DIFF; IN_SING; UNWIND_THM2; GSYM CONJ_ASSOC; ASSIGN] THEN
37 REWRITE_TAC[ARITH_EQ] THEN LET_TAC THEN
38 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] iff_trans) THEN
39 SUBGOAL_THEN `~(z' IN FVT t)` ASSUME_TAC THENL
40 [EXPAND_TAC "z'" THEN COND_CASES_TAC THEN
41 ASM_SIMP_TAC[SET_RULE `a IN s ==> s UNION {a} = s`;
42 VARIANT_FINITE; FVT_FINITE];
43 MATCH_MP_TAC imp_antisym THEN
44 ASM_CASES_TAC `z':num = z` THEN ASM_REWRITE_TAC[imp_refl] THEN
45 CONJ_TAC THEN MATCH_MP_TAC ichoose THEN
46 ASM_REWRITE_TAC[FV; IN_DELETE; IN_UNION; IN_SING; FVT] THEN
47 MATCH_MP_TAC gen THEN MATCH_MP_TAC imp_trans THENL
48 [EXISTS_TAC `formsubst (z |=> V z') (t === Suc(V z))`;
49 EXISTS_TAC `formsubst (z' |=> V z) (t === Suc(V z'))`] THEN
50 REWRITE_TAC[iexists] THEN REWRITE_TAC[formsubst] THEN
51 ASM_REWRITE_TAC[termsubst; ASSIGN] THEN
52 MATCH_MP_TAC(MESON[imp_refl] `p = q ==> A |-- p --> q`) THEN
53 AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
54 MATCH_MP_TAC TERMSUBST_TRIVIAL THEN REWRITE_TAC[ASSIGN] THEN
58 (`!t. {robinson} |-- Z ++ t === t`,
59 REWRITE_TAC[spec_rule `t:term` add_0]);;
62 (`!s t. {robinson} |-- Suc(s) ++ t === Suc(s ++ t)`,
63 REWRITE_TAC[specl_rule [`s:term`; `t:term`] add_suc]);;
66 (`!t. {robinson} |-- Z ** t === Z`,
67 REWRITE_TAC[spec_rule `t:term` mul_0]);;
70 (`!s t. {robinson} |-- Suc(s) ** t === t ++ s ** t`,
71 REWRITE_TAC[specl_rule [`s:term`; `t:term`] mul_suc]);;
74 (`!s t. {robinson} |-- (s << t <-> Suc(s) <<= t)`,
75 REWRITE_TAC[specl_rule [`s:term`; `t:term`] lt_def]);;
77 (* ------------------------------------------------------------------------- *)
78 (* All ground terms can be evaluated by proof. *)
79 (* ------------------------------------------------------------------------- *)
81 let SIGMA1_COMPLETE_ADD = prove
82 (`!m n. {robinson} |-- numeral m ++ numeral n === numeral(m + n)`,
83 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; numeral] THEN
84 ASM_MESON_TAC[add_0'; add_suc'; axiom_funcong; eq_trans; modusponens]);;
86 let SIGMA1_COMPLETE_MUL = prove
87 (`!m n. {robinson} |-- (numeral m ** numeral n === numeral(m * n))`,
88 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; numeral] THENL
89 [ASM_MESON_TAC[mul_0']; ALL_TAC] THEN
90 GEN_TAC THEN MATCH_MP_TAC eq_trans_rule THEN
91 EXISTS_TAC `numeral(n) ++ numeral(m * n)` THEN CONJ_TAC THENL
92 [ASM_MESON_TAC[mul_suc'; eq_trans_rule; axiom_funcong; imp_trans;
93 modusponens; imp_swap;add_assum; axiom_eqrefl];
94 ASM_MESON_TAC[SIGMA1_COMPLETE_ADD; ADD_SYM; eq_trans_rule]]);;
96 let SIGMA1_COMPLETE_TERM = prove
97 (`!v t n. FVT t = {} /\ termval v t = n
98 ==> {robinson} |-- (t === numeral n)`,
99 let lemma = prove(`(!n. p /\ (x = n) ==> P n) <=> p ==> P x`,MESON_TAC[]) in
100 GEN_TAC THEN MATCH_MP_TAC term_INDUCT THEN
101 REWRITE_TAC[termval;FVT; NOT_INSERT_EMPTY] THEN CONJ_TAC THENL
102 [GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[numeral] THEN
103 MESON_TAC[axiom_eqrefl; add_assum];
105 REWRITE_TAC[lemma] THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
106 DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN
107 RULE_ASSUM_TAC(REWRITE_RULE[EMPTY_UNION]) THEN ASM_REWRITE_TAC[numeral] THEN
108 MESON_TAC[SIGMA1_COMPLETE_ADD; SIGMA1_COMPLETE_MUL;
109 cong_suc; cong_add; cong_mul; eq_trans_rule]);;
111 (* ------------------------------------------------------------------------- *)
112 (* Convenient stepping theorems for atoms and other useful lemmas. *)
113 (* ------------------------------------------------------------------------- *)
115 let canonize_clauses =
116 let lemma0 = MESON[imp_refl; imp_swap; modusponens; axiom_doubleneg]
117 `!A p. A |-- (p --> False) --> False <=> A |-- p`
118 and lemma1 = MESON[iff_imp1; iff_imp2; modusponens; imp_trans]
120 ==> (A |-- p <=> A |-- q) /\ (A |-- p --> False <=> A |-- q --> False)` in
121 itlist (CONJ o MATCH_MP lemma1 o SPEC_ALL)
122 [axiom_true; axiom_not; axiom_and; axiom_or; iff_def; axiom_exists]
124 and false_imp = MESON[imp_truefalse; modusponens]
125 `A |-- p /\ A |-- q --> False ==> A |-- (p --> q) --> False`
126 and true_imp = MESON[axiom_addimp; modusponens; ex_falso; imp_trans]
127 `A |-- p --> False \/ A |-- q ==> A |-- p --> q`;;
130 REWRITE_TAC[canonize_clauses; imp_refl] THEN
131 REPEAT((MATCH_MP_TAC false_imp THEN CONJ_TAC) ORELSE
132 MATCH_MP_TAC true_imp THEN
133 REWRITE_TAC[canonize_clauses; imp_refl]);;
135 let suc_inj_eq = prove
136 (`!s t. {robinson} |-- Suc s === Suc t <-> s === t`,
137 MESON_TAC[suc_inj'; axiom_funcong; imp_antisym]);;
139 let suc_le_eq = prove
140 (`!s t. {robinson} |-- Suc s <<= Suc t <-> s <<= t`,
142 TRANS_TAC iff_trans `??2 (Suc(V 0) ++ V 2 === Suc(V 1))` THEN
143 REWRITE_TAC[itlist spec_rule [`Suc(V 1)`; `Suc(V 0)`] le_def] THEN
144 TRANS_TAC iff_trans `??2 (V 0 ++ V 2 === V 1)` THEN
145 GEN_REWRITE_TAC RAND_CONV [iff_sym] THEN
146 REWRITE_TAC[itlist spec_rule [`V 1`; `V 0`] le_def] THEN
147 MATCH_MP_TAC exiff THEN
148 TRANS_TAC iff_trans `Suc(V 0 ++ V 2) === Suc(V 1)` THEN
149 REWRITE_TAC[suc_inj_eq] THEN MATCH_MP_TAC cong_eq THEN
150 REWRITE_TAC[axiom_eqrefl; add_suc']);;
152 let le_iff_lt = prove
153 (`!s t. {robinson} |-- s <<= t <-> s << Suc t`,
154 REPEAT GEN_TAC THEN TRANS_TAC iff_trans `Suc s <<= Suc t` THEN
155 ONCE_REWRITE_TAC[iff_sym] THEN
156 REWRITE_TAC[suc_le_eq; lt_def']);;
158 let suc_lt_eq = prove
159 (`!s t. {robinson} |-- Suc s << Suc t <-> s << t`,
160 MESON_TAC[iff_sym; iff_trans; le_iff_lt; lt_def']);;
162 let not_suc_eq_0 = prove
163 (`!t. {robinson} |-- Suc t === Z --> False`,
165 SUBGOAL_THEN `{robinson} |-- Not(Suc(V 1) === Z)` MP_TAC THENL
166 [ALL_TAC; REWRITE_TAC[canonize_clauses]] THEN
167 SUBGOAL_THEN `{robinson} |-- ?? 0 (Suc(V 1) === Suc(V 0))` MP_TAC THENL
168 [MATCH_MP_TAC exists_intro THEN EXISTS_TAC `V 1` THEN
169 CONV_TAC(RAND_CONV FORMSUBST_CONV) THEN REWRITE_TAC[axiom_eqrefl];
170 MESON_TAC[iff_imp2; modusponens; spec_rule `Suc(V 1)` num_cases]]);;
172 let not_suc_le_0 = prove
173 (`!t. {robinson} |-- Suc t <<= Z --> False`,
174 X_GEN_TAC `s:term` THEN
175 SUBGOAL_THEN `{robinson} |-- !!0 (Suc(V 0) <<= Z --> False)` MP_TAC THENL
176 [ALL_TAC; DISCH_THEN(ACCEPT_TAC o spec_rule `s:term`)] THEN
177 MATCH_MP_TAC gen THEN
178 SUBGOAL_THEN `{robinson} |-- ?? 2 (Suc (V 0) ++ V 2 === Z) --> False`
181 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] imp_trans) THEN
182 MATCH_MP_TAC iff_imp1 THEN
183 ACCEPT_TAC(itlist spec_rule [`Z`; `Suc(V 0)`] le_def)] THEN
184 MATCH_MP_TAC ichoose THEN REWRITE_TAC[FV; NOT_IN_EMPTY] THEN
185 MATCH_MP_TAC gen THEN TRANS_TAC imp_trans `Suc(V 0 ++ V 2) === Z` THEN
186 REWRITE_TAC[not_suc_eq_0] THEN MATCH_MP_TAC iff_imp1 THEN
187 MATCH_MP_TAC cong_eq THEN REWRITE_TAC[axiom_eqrefl] THEN
188 REWRITE_TAC[add_suc']);;
191 (`!t. {robinson} |-- t << Z --> False`,
192 MESON_TAC[not_suc_le_0; lt_def'; imp_trans; iff_imp1]);;
194 (* ------------------------------------------------------------------------- *)
195 (* Evaluation of atoms built from numerals by proof. *)
196 (* ------------------------------------------------------------------------- *)
198 let add_0_right = prove
199 (`!n. {robinson} |-- numeral n ++ Z === numeral n`,
200 GEN_TAC THEN MP_TAC(ISPECL [`n:num`; `0`] SIGMA1_COMPLETE_ADD) THEN
201 REWRITE_TAC[numeral; ADD_CLAUSES]);;
203 let ATOM_EQ_FALSE = prove
204 (`!m n. ~(m = n) ==> {robinson} |-- numeral m === numeral n --> False`,
205 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
206 MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[] THEN CONJ_TAC THENL
207 [MESON_TAC[eq_sym; imp_trans]; ALL_TAC] THEN
208 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
209 INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN INDUCT_TAC THEN
210 REWRITE_TAC[numeral; not_suc_eq_0; LT_SUC; SUC_INJ] THEN
211 ASM_MESON_TAC[suc_inj_eq; imp_trans; iff_imp1; iff_imp2]);;
213 let ATOM_LE_FALSE = prove
214 (`!m n. n < m ==> {robinson} |-- numeral m <<= numeral n --> False`,
215 INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN
216 INDUCT_TAC THEN REWRITE_TAC[numeral; not_suc_le_0; LT_SUC] THEN
217 ASM_MESON_TAC[suc_le_eq; imp_trans; iff_imp1; iff_imp2]);;
219 let ATOM_LT_FALSE = prove
220 (`!m n. n <= m ==> {robinson} |-- numeral m << numeral n --> False`,
221 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LT_SUC_LE] THEN
222 DISCH_THEN(MP_TAC o MATCH_MP ATOM_LE_FALSE) THEN
223 REWRITE_TAC[numeral] THEN
224 ASM_MESON_TAC[lt_def'; imp_trans; iff_imp1; iff_imp2]);;
226 let ATOM_EQ_TRUE = prove
227 (`!m n. m = n ==> {robinson} |-- numeral m === numeral n`,
228 MESON_TAC[axiom_eqrefl]);;
230 let ATOM_LE_TRUE = prove
231 (`!m n. m <= n ==> {robinson} |-- numeral m <<= numeral n`,
232 SUBGOAL_THEN `!m n. {robinson} |-- numeral m <<= numeral(m + n)`
233 MP_TAC THENL [ALL_TAC; MESON_TAC[LE_EXISTS]] THEN
234 REPEAT GEN_TAC THEN MATCH_MP_TAC modusponens THEN
235 EXISTS_TAC `?? 2 (numeral m ++ V 2 === numeral(m + n))` THEN
237 [MP_TAC(itlist spec_rule [`numeral(m + n)`; `numeral m`] le_def) THEN
239 MATCH_MP_TAC exists_intro THEN EXISTS_TAC `numeral n` THEN
240 CONV_TAC(RAND_CONV FORMSUBST_CONV) THEN
241 REWRITE_TAC[SIGMA1_COMPLETE_ADD]]);;
243 let ATOM_LT_TRUE = prove
244 (`!m n. m < n ==> {robinson} |-- numeral m << numeral n`,
245 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LE_SUC_LT] THEN
246 DISCH_THEN(MP_TAC o MATCH_MP ATOM_LE_TRUE) THEN
247 REWRITE_TAC[numeral] THEN
248 ASM_MESON_TAC[lt_def'; modusponens; iff_imp1; iff_imp2]);;
250 (* ------------------------------------------------------------------------- *)
251 (* A kind of case analysis rule; might make it induction in case of PA. *)
252 (* ------------------------------------------------------------------------- *)
254 let FORMSUBST_FORMSUBST_SAME_NONE = prove
256 FVT t = {x} /\ FVT s = {}
257 ==> formsubst (x |=> s) (formsubst (x |=> t) p) =
258 formsubst (x |=> termsubst (x |=> s) t) p`,
259 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
260 REPEAT GEN_TAC THEN STRIP_TAC THEN
261 SUBGOAL_THEN `!y. safe_for y (x |=> termsubst (x |=> s) t)` ASSUME_TAC THENL
262 [GEN_TAC THEN REWRITE_TAC[SAFE_FOR_ASSIGN; TERMSUBST_FVT; ASSIGN] THEN
265 MATCH_MP_TAC form_INDUCT THEN
266 ASM_SIMP_TAC[FORMSUBST_SAFE_FOR; SAFE_FOR_ASSIGN; IN_SING; NOT_IN_EMPTY] THEN
267 SIMP_TAC[formsubst] THEN
268 MATCH_MP_TAC(TAUT `(p /\ q /\ r) /\ s ==> p /\ q /\ r /\ s`) THEN
270 [REPEAT STRIP_TAC THEN BINOP_TAC THEN
271 REWRITE_TAC[TERMSUBST_TERMSUBST] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
272 REWRITE_TAC[o_DEF; FUN_EQ_THM] THEN X_GEN_TAC `y:num` THEN
273 REWRITE_TAC[ASSIGN] THEN COND_CASES_TAC THEN
274 ASM_REWRITE_TAC[termsubst; ASSIGN];
275 CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`y:num`; `p:form`] THEN DISCH_TAC THEN
276 (ASM_CASES_TAC `y:num = x` THENL
277 [ASM_REWRITE_TAC[assign; VALMOD_VALMOD_BASIC] THEN
278 SIMP_TAC[VALMOD_TRIVIAL; FORMSUBST_TRIV];
279 SUBGOAL_THEN `!u. (y |-> V y) (x |=> u) = (x |=> u)`
280 (fun th -> ASM_REWRITE_TAC[th]) THEN
281 GEN_TAC THEN MATCH_MP_TAC VALMOD_TRIVIAL THEN
282 ASM_REWRITE_TAC[ASSIGN]])]);;
284 let num_cases_rule = prove
285 (`!p x. {robinson} |-- formsubst (x |=> Z) p /\
286 {robinson} |-- formsubst (x |=> Suc(V x)) p
287 ==> {robinson} |-- p`,
289 (`!A p x t. A |-- formsubst (x |=> t) p ==> A |-- V x === t --> p`,
291 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] modusponens) THEN
292 MATCH_MP_TAC imp_swap THEN
293 GEN_REWRITE_TAC (funpow 3 RAND_CONV) [GSYM FORMSUBST_TRIV] THEN
294 CONV_TAC(funpow 3 RAND_CONV(SUBS_CONV[SYM(SPEC `x:num` ASSIGN_TRIV)])) THEN
295 TRANS_TAC imp_trans `t === V x` THEN REWRITE_TAC[isubst; eq_sym]) in
297 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM FORMSUBST_TRIV] THEN
298 CONV_TAC(RAND_CONV(SUBS_CONV[SYM(SPEC `x:num` ASSIGN_TRIV)])) THEN
299 SUBGOAL_THEN `?z. ~(z = x) /\ ~(z IN VARS p)` STRIP_ASSUME_TAC THENL
300 [EXISTS_TAC `VARIANT(x INSERT VARS p)` THEN
301 REWRITE_TAC[GSYM DE_MORGAN_THM; GSYM IN_INSERT] THEN
302 MATCH_MP_TAC NOT_IN_VARIANT THEN
303 SIMP_TAC[VARS_FINITE; FINITE_INSERT; SUBSET_REFL];
305 FIRST_X_ASSUM(fun th ->
306 ONCE_REWRITE_TAC[GSYM(MATCH_MP FORMSUBST_TWICE th)]) THEN
307 SUBGOAL_THEN `~(x IN FV(formsubst (x |=> V z) p))` MP_TAC THENL
308 [REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; ASSIGN; NOT_EXISTS_THM] THEN
309 GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[FVT] THEN
312 SPEC_TAC(`formsubst (x |=> V z) p`,`p:form`) THEN
313 REPEAT STRIP_TAC THEN MATCH_MP_TAC spec THEN MATCH_MP_TAC gen THEN
314 FIRST_X_ASSUM(MP_TAC o MATCH_MP lemma) THEN
315 DISCH_THEN(MP_TAC o SPEC `x:num` o MATCH_MP gen) THEN
316 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] ichoose)) THEN
317 FIRST_X_ASSUM(MP_TAC o MATCH_MP lemma) THEN ASM_REWRITE_TAC[IMP_IMP] THEN
318 DISCH_THEN(MP_TAC o MATCH_MP ante_disj) THEN
319 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] modusponens) THEN
320 MP_TAC(ISPECL [`V z`; `x:num`] num_cases') THEN
321 ASM_REWRITE_TAC[FVT; IN_SING] THEN
322 DISCH_THEN(MP_TAC o MATCH_MP iff_imp1) THEN
323 REWRITE_TAC[canonize_clauses] THEN
324 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] imp_trans) THEN
325 MESON_TAC[imp_swap; axiom_not; iff_imp1; imp_trans]);;
327 (* ------------------------------------------------------------------------- *)
328 (* Now full Sigma-1 completeness. *)
329 (* ------------------------------------------------------------------------- *)
331 let SIGMAPI1_COMPLETE = prove
332 (`!v p b. sigmapi b 1 p /\ closed p
333 ==> (b /\ holds v p ==> {robinson} |-- p) /\
334 (~b /\ ~holds v p ==> {robinson} |-- p --> False)`,
336 (`!x n p. (!m. m < n ==> {robinson} |-- formsubst (x |=> numeral m) p)
337 ==> {robinson} |-- !!x (V x << numeral n --> p)`,
338 GEN_TAC THEN INDUCT_TAC THEN X_GEN_TAC `p:form` THEN DISCH_TAC THEN
339 REWRITE_TAC[numeral] THENL
340 [ASM_MESON_TAC[gen; imp_trans; ex_falso; not_lt_0]; ALL_TAC] THEN
341 MATCH_MP_TAC gen THEN MATCH_MP_TAC num_cases_rule THEN
342 EXISTS_TAC `x:num` THEN CONJ_TAC THENL
343 [ONCE_REWRITE_TAC[formsubst] THEN MATCH_MP_TAC add_assum THEN
344 REWRITE_TAC[GSYM numeral] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ARITH_TAC;
346 REWRITE_TAC[formsubst; termsubst; TERMSUBST_NUMERAL; ASSIGN] THEN
347 TRANS_TAC imp_trans `V x << numeral n` THEN
348 CONJ_TAC THENL [MESON_TAC[suc_lt_eq; iff_imp1]; ALL_TAC] THEN
349 MATCH_MP_TAC spec_var THEN EXISTS_TAC `x:num` THEN
350 FIRST_X_ASSUM MATCH_MP_TAC THEN
351 X_GEN_TAC `m:num` THEN DISCH_TAC THEN
352 FIRST_X_ASSUM(MP_TAC o SPEC `SUC m`) THEN
353 ASM_REWRITE_TAC[LT_SUC] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
354 W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_FORMSUBST_SAME_NONE o
356 REWRITE_TAC[FVT; FVT_NUMERAL] THEN DISCH_THEN SUBST1_TAC THEN
357 REWRITE_TAC[termsubst; ASSIGN; numeral]) in
359 (`!x n p. (!m. m <= n ==> {robinson} |-- formsubst (x |=> numeral m) p)
360 ==> {robinson} |-- !!x (V x <<= numeral n --> p)`,
361 REPEAT STRIP_TAC THEN
362 MP_TAC(ISPECL [`x:num`; `SUC n`; `p:form`] lemma1) THEN
363 ASM_REWRITE_TAC[LT_SUC_LE] THEN DISCH_TAC THEN MATCH_MP_TAC gen THEN
364 FIRST_ASSUM(MP_TAC o MATCH_MP spec_var) THEN REWRITE_TAC[numeral] THEN
365 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] imp_trans) THEN
366 MESON_TAC[iff_imp1; le_iff_lt]) in
371 ==> {robinson} |-- formsubst (x |=> numeral m) p)
372 ==> {robinson} |-- !!x (V x << t --> p)`,
373 REPEAT STRIP_TAC THEN MATCH_MP_TAC gen THEN
374 FIRST_ASSUM(MP_TAC o MATCH_MP spec_var o MATCH_MP lemma1) THEN
375 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] imp_trans) THEN
376 MATCH_MP_TAC iff_imp1 THEN MATCH_MP_TAC cong_lt THEN
377 REWRITE_TAC[axiom_eqrefl] THEN MATCH_MP_TAC SIGMA1_COMPLETE_TERM THEN
382 (!m. m <= termval v t
383 ==> {robinson} |-- formsubst (x |=> numeral m) p)
384 ==> {robinson} |-- !!x (V x <<= t --> p)`,
385 REPEAT STRIP_TAC THEN MATCH_MP_TAC gen THEN
386 FIRST_ASSUM(MP_TAC o MATCH_MP spec_var o MATCH_MP lemma2) THEN
387 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] imp_trans) THEN
388 MATCH_MP_TAC iff_imp1 THEN MATCH_MP_TAC cong_le THEN
389 REWRITE_TAC[axiom_eqrefl] THEN MATCH_MP_TAC SIGMA1_COMPLETE_TERM THEN
392 (`!A x p q. A |-- !!x (p --> Not q) ==> A |-- !!x (Not(p && q))`,
393 REPEAT STRIP_TAC THEN MATCH_MP_TAC gen THEN
394 FIRST_ASSUM(MP_TAC o MATCH_MP spec_var) THEN
395 REWRITE_TAC[canonize_clauses] THEN
396 MESON_TAC[imp_trans; axiom_not; iff_imp1; iff_imp2]) in
397 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[closed] THEN
398 WF_INDUCT_TAC `complexity p` THEN
399 POP_ASSUM MP_TAC THEN SPEC_TAC(`p:form`,`p:form`) THEN
400 MATCH_MP_TAC form_INDUCT THEN
401 REWRITE_TAC[SIGMAPI_CLAUSES; complexity; ARITH] THEN
402 REWRITE_TAC[MESON[] `(if p then q else F) <=> p /\ q`] THEN
404 [TAUT `a /\ b /\ c /\ d /\ e /\ f /\ g /\ h /\ i /\ j /\ k /\ l <=>
405 (a /\ b) /\ (c /\ d /\ e) /\ f /\ (g /\ h /\ i /\ j) /\ (k /\ l)`] THEN
407 [CONJ_TAC THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[holds] THEN
408 MESON_TAC[imp_refl; truth];
411 [REPEAT CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`s:term`; `t:term`] THEN
412 DISCH_THEN(K ALL_TAC) THEN X_GEN_TAC `b:bool` THEN
413 REWRITE_TAC[FV; EMPTY_UNION] THEN STRIP_TAC THEN
414 MP_TAC(ISPECL [`v:num->num`; `t:term`; `termval v t`]
415 SIGMA1_COMPLETE_TERM) THEN
416 MP_TAC(ISPECL [`v:num->num`; `s:term`; `termval v s`]
417 SIGMA1_COMPLETE_TERM) THEN
418 ASM_REWRITE_TAC[IMP_IMP] THENL
419 [DISCH_THEN(MP_TAC o MATCH_MP cong_eq);
420 DISCH_THEN(MP_TAC o MATCH_MP cong_lt);
421 DISCH_THEN(MP_TAC o MATCH_MP cong_le)] THEN
422 STRIP_TAC THEN REWRITE_TAC[holds; NOT_LE; NOT_LT] THEN
423 (REPEAT STRIP_TAC THENL
424 [FIRST_X_ASSUM(MATCH_MP_TAC o
425 MATCH_MP(REWRITE_RULE[IMP_CONJ] modusponens) o MATCH_MP iff_imp2);
426 FIRST_X_ASSUM(MATCH_MP_TAC o
427 MATCH_MP(REWRITE_RULE[IMP_CONJ] imp_trans) o MATCH_MP iff_imp1)]) THEN
428 ASM_SIMP_TAC[ATOM_EQ_FALSE; ATOM_EQ_TRUE; ATOM_LT_FALSE; ATOM_LT_TRUE;
429 ATOM_LE_FALSE; ATOM_LE_TRUE];
432 [X_GEN_TAC `p:form` THEN DISCH_THEN(K ALL_TAC) THEN
433 DISCH_THEN(MP_TAC o SPEC `p:form`) THEN
434 ANTS_TAC THENL [ARITH_TAC; DISCH_TAC] THEN
435 X_GEN_TAC `b:bool` THEN REWRITE_TAC[FV] THEN STRIP_TAC THEN
436 FIRST_X_ASSUM(MP_TAC o SPEC `~b`) THEN ASM_REWRITE_TAC[holds] THEN
437 BOOL_CASES_TAC `b:bool` THEN CANONIZE_TAC THEN ASM_MESON_TAC[];
440 [REPEAT CONJ_TAC THEN
441 MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
442 DISCH_TAC THEN X_GEN_TAC `b:bool` THEN REWRITE_TAC[FV; EMPTY_UNION] THEN
443 STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
444 MP_TAC(SPEC `p:form` th) THEN MP_TAC(SPEC `q:form` th)) THEN
445 (ANTS_TAC THENL [ARITH_TAC; ALL_TAC]) THEN
446 ONCE_REWRITE_TAC[TAUT `p ==> q ==> r <=> q ==> p ==> r`] THEN
447 (ANTS_TAC THENL [ARITH_TAC; ASM_REWRITE_TAC[IMP_IMP]]) THEN
448 ASM_REWRITE_TAC[holds; canonize_clauses] THENL
449 [DISCH_THEN(CONJUNCTS_THEN(MP_TAC o SPEC `b:bool`));
450 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o SPEC `b:bool`));
451 DISCH_THEN(CONJUNCTS_THEN2
452 (MP_TAC o SPEC `~b`) (MP_TAC o SPEC `b:bool`));
453 DISCH_THEN(CONJUNCTS_THEN(fun th ->
454 MP_TAC(SPEC `~b` th) THEN MP_TAC(SPEC `b:bool` th)))] THEN
455 ASM_REWRITE_TAC[] THEN BOOL_CASES_TAC `b:bool` THEN
456 ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN CANONIZE_TAC THEN
457 TRY(FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
458 `~(p <=> q) ==> (p /\ ~q ==> r) /\ (~p /\ q ==> s) ==> r \/ s`)) THEN
459 REPEAT STRIP_TAC THEN CANONIZE_TAC) THEN
462 CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
463 DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[canonize_clauses; holds] THEN
464 DISCH_TAC THEN X_GEN_TAC `b:bool` THENL
465 [BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[] THENL
466 [REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC; FV] THEN
467 ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
468 MAP_EVERY X_GEN_TAC [`q:form`; `t:term`] THEN DISCH_THEN
469 (CONJUNCTS_THEN2 (DISJ_CASES_THEN SUBST_ALL_TAC) ASSUME_TAC) THEN
470 REWRITE_TAC[SIGMAPI_CLAUSES; FV; holds] THEN
471 (ASM_CASES_TAC `FVT t = {}` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
472 (ASM_CASES_TAC `FV(q) SUBSET {x}` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
473 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o CONJUNCT2)) THEN
474 ABBREV_TAC `n = termval v t` THEN
475 ASM_SIMP_TAC[TERMVAL_VALMOD_OTHER; termval; VALMOD] THENL
476 [DISCH_TAC THEN MATCH_MP_TAC lemma3;
477 DISCH_TAC THEN MATCH_MP_TAC lemma4] THEN
478 EXISTS_TAC `v:num->num` THEN
479 ASM_REWRITE_TAC[] THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
480 FIRST_X_ASSUM(MP_TAC o SPEC `formsubst (x |=> numeral m) q`) THEN
481 REWRITE_TAC[complexity; COMPLEXITY_FORMSUBST] THEN
482 (ANTS_TAC THENL [ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `T`)]) THEN
483 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN MATCH_MP_TAC THEN
484 ASM_SIMP_TAC[SIGMAPI_FORMSUBST] THEN
485 REWRITE_TAC[FORMSUBST_FV; ASSIGN] THEN
486 REPLICATE_TAC 2 (ONCE_REWRITE_TAC[COND_RAND]) THEN
487 REWRITE_TAC[FVT_NUMERAL; NOT_IN_EMPTY; FVT; IN_SING] THEN
488 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
489 FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ASM_REWRITE_TAC[] THEN
490 REWRITE_TAC[HOLDS_FORMSUBST] THEN
491 MATCH_MP_TAC EQ_IMP THEN MATCH_MP_TAC HOLDS_VALUATION THEN
492 X_GEN_TAC `y:num` THEN
493 (ASM_CASES_TAC `y:num = x` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
494 ASM_REWRITE_TAC[o_DEF; ASSIGN; VALMOD; TERMVAL_NUMERAL];
495 STRIP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
496 X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC imp_trans THEN
497 EXISTS_TAC `formsubst (x |=> numeral n) p` THEN REWRITE_TAC[ispec] THEN
498 FIRST_X_ASSUM(MP_TAC o SPEC `formsubst (x |=> numeral n) p`) THEN
499 REWRITE_TAC[COMPLEXITY_FORMSUBST; ARITH_RULE `n < n + 1`] THEN
500 DISCH_THEN(MP_TAC o SPEC `F`) THEN
501 ASM_SIMP_TAC[SIGMAPI_FORMSUBST; IMP_IMP] THEN
502 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL
503 [UNDISCH_TAC `FV (!! x p) = {}` THEN
504 REWRITE_TAC[FV; FORMSUBST_FV; SET_RULE
505 `s DELETE a = {} <=> s = {} \/ s = {a}`] THEN STRIP_TAC THEN
506 ASM_REWRITE_TAC[NOT_IN_EMPTY; IN_SING; EMPTY_GSPEC;
507 ASSIGN; UNWIND_THM2; FVT_NUMERAL];
508 UNDISCH_TAC `~holds((x |-> n) v) p` THEN
509 REWRITE_TAC[HOLDS_FORMSUBST; CONTRAPOS_THM] THEN
510 MATCH_MP_TAC EQ_IMP THEN MATCH_MP_TAC HOLDS_VALUATION THEN
511 RULE_ASSUM_TAC(REWRITE_RULE[FV]) THEN X_GEN_TAC `y:num` THEN
512 ASM_CASES_TAC `y:num = x` THENL [ALL_TAC; ASM SET_TAC[]] THEN
513 ASM_REWRITE_TAC[o_THM; ASSIGN; VALMOD; TERMVAL_NUMERAL]]];
514 BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[] THENL
515 [REWRITE_TAC[FV] THEN STRIP_TAC THEN
516 DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN
517 FIRST_X_ASSUM(MP_TAC o SPEC `formsubst (x |=> numeral n) (Not p)`) THEN
518 REWRITE_TAC[COMPLEXITY_FORMSUBST; complexity] THEN
519 ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `F`)] THEN
520 ASM_SIMP_TAC[IMP_IMP; SIGMAPI_CLAUSES; SIGMAPI_FORMSUBST] THEN
522 [REWRITE_TAC[FORMSUBST_FV; ASSIGN] THEN
523 REPLICATE_TAC 2 (ONCE_REWRITE_TAC[COND_RAND]) THEN
524 REWRITE_TAC[FVT_NUMERAL; NOT_IN_EMPTY; FVT; FV; IN_SING] THEN
525 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
526 UNDISCH_TAC `holds ((x |-> n) v) p` THEN
527 REWRITE_TAC[formsubst; holds; HOLDS_FORMSUBST] THEN
528 MATCH_MP_TAC EQ_IMP THEN MATCH_MP_TAC HOLDS_VALUATION THEN
529 RULE_ASSUM_TAC(REWRITE_RULE[FV]) THEN X_GEN_TAC `y:num` THEN
530 ASM_CASES_TAC `y:num = x` THENL [ALL_TAC; ASM SET_TAC[]] THEN
531 ASM_REWRITE_TAC[o_THM; ASSIGN; VALMOD; TERMVAL_NUMERAL];
532 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] imp_trans) THEN
534 REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC; FV] THEN
535 ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
536 MAP_EVERY X_GEN_TAC [`q:form`; `t:term`] THEN DISCH_THEN
537 (CONJUNCTS_THEN2 (DISJ_CASES_THEN SUBST_ALL_TAC) ASSUME_TAC) THEN
538 REWRITE_TAC[SIGMAPI_CLAUSES; FV; holds] THEN
539 (ASM_CASES_TAC `FVT t = {}` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
540 (ASM_CASES_TAC `FV(q) SUBSET {x}` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
541 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o CONJUNCT2)) THEN
542 ABBREV_TAC `n = termval v t` THEN
543 ASM_SIMP_TAC[TERMVAL_VALMOD_OTHER; termval; VALMOD] THEN
544 REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`] THEN
545 DISCH_TAC THEN MATCH_MP_TAC lemma5 THENL
546 [MATCH_MP_TAC lemma3; MATCH_MP_TAC lemma4] THEN
547 EXISTS_TAC `v:num->num` THEN
548 ASM_REWRITE_TAC[] THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
549 FIRST_X_ASSUM(MP_TAC o SPEC `formsubst (x |=> numeral m) (Not q)`) THEN
550 REWRITE_TAC[complexity; COMPLEXITY_FORMSUBST] THEN
551 (ANTS_TAC THENL [ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `T`)]) THEN
552 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN MATCH_MP_TAC THEN
553 ASM_SIMP_TAC[SIGMAPI_FORMSUBST; SIGMAPI_CLAUSES] THEN
554 REWRITE_TAC[FORMSUBST_FV; FV; ASSIGN] THEN
555 REPLICATE_TAC 2 (ONCE_REWRITE_TAC[COND_RAND]) THEN
556 REWRITE_TAC[FVT_NUMERAL; NOT_IN_EMPTY; FVT; IN_SING] THEN
557 (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
558 FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ASM_REWRITE_TAC[] THEN
559 REWRITE_TAC[HOLDS_FORMSUBST; holds; CONTRAPOS_THM] THEN
560 MATCH_MP_TAC EQ_IMP THEN MATCH_MP_TAC HOLDS_VALUATION THEN
561 X_GEN_TAC `y:num` THEN
562 (ASM_CASES_TAC `y:num = x` THENL [ALL_TAC; ASM SET_TAC[]]) THEN
563 ASM_REWRITE_TAC[o_DEF; ASSIGN; VALMOD; TERMVAL_NUMERAL]]]);;
565 (* ------------------------------------------------------------------------- *)
566 (* Hence a nice alternative form of Goedel's theorem for any consistent *)
567 (* sigma_1-definable axioms A that extend (i.e. prove) the Robinson axioms. *)
568 (* ------------------------------------------------------------------------- *)
570 let G1_ROBINSON = prove
571 (`!A. definable_by (SIGMA 1) (IMAGE gform A) /\
572 consistent A /\ A |-- robinson
577 (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
578 REPEAT STRIP_TAC THEN MATCH_MP_TAC G1_TRAD THEN
579 ASM_REWRITE_TAC[complete_for; INTER; IN_ELIM_THM] THEN
580 X_GEN_TAC `p:form` THEN REWRITE_TAC[IN; true_def] THEN STRIP_TAC THEN
581 MATCH_MP_TAC modusponens THEN EXISTS_TAC `robinson` THEN
582 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC PROVES_MONO THEN
583 EXISTS_TAC `{}:form->bool` THEN REWRITE_TAC[EMPTY_SUBSET] THEN
584 W(MP_TAC o PART_MATCH (lhs o rand) DEDUCTION o snd) THEN
585 MP_TAC(ISPECL [`I:num->num`; `p:form`; `T`] SIGMAPI1_COMPLETE) THEN
586 ASM_REWRITE_TAC[GSYM SIGMA] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
587 DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[robinson; closed; FV; FVT] THEN
590 (* ------------------------------------------------------------------------- *)
591 (* More metaproperties of axioms systems now we have some derived rules. *)
592 (* ------------------------------------------------------------------------- *)
594 let complete = new_definition
595 `complete A <=> !p. closed p ==> A |-- p \/ A |-- Not p`;;
597 let sound = new_definition
598 `sound A <=> !p. A |-- p ==> true p`;;
600 let semcomplete = new_definition
601 `semcomplete A <=> !p. true p ==> A |-- p`;;
603 let generalize = new_definition
604 `generalize vs p = ITLIST (!!) vs p`;;
606 let closure = new_definition
607 `closure p = generalize (list_of_set(FV p)) p`;;
609 let TRUE_GENERALIZE = prove
610 (`!vs p. true(generalize vs p) <=> true p`,
611 REWRITE_TAC[generalize; true_def] THEN
612 LIST_INDUCT_TAC THEN REWRITE_TAC[ITLIST; holds] THEN GEN_TAC THEN
613 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
614 MESON_TAC[VALMOD_REPEAT]);;
616 let PROVABLE_GENERALIZE = prove
617 (`!A p vs. A |-- generalize vs p <=> A |-- p`,
618 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[generalize] THEN LIST_INDUCT_TAC THEN
619 REWRITE_TAC[ITLIST] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
620 MESON_TAC[spec; gen; FORMSUBST_TRIV; ASSIGN_TRIV]);;
622 let FV_GENERALIZE = prove
623 (`!p vs. FV(generalize vs p) = FV(p) DIFF (set_of_list vs)`,
624 GEN_TAC THEN REWRITE_TAC[generalize] THEN
625 LIST_INDUCT_TAC THEN REWRITE_TAC[set_of_list; DIFF_EMPTY; ITLIST] THEN
626 ASM_REWRITE_TAC[FV] THEN SET_TAC[]);;
628 let CLOSED_CLOSURE = prove
629 (`!p. closed(closure p)`,
630 REWRITE_TAC[closed; closure; FV_GENERALIZE] THEN
631 SIMP_TAC[SET_OF_LIST_OF_SET; FV_FINITE; DIFF_EQ_EMPTY]);;
633 let TRUE_CLOSURE = prove
634 (`!p. true(closure p) <=> true p`,
635 REWRITE_TAC[closure; TRUE_GENERALIZE]);;
637 let PROVABLE_CLOSURE = prove
638 (`!A p. A |-- closure p <=> A |-- p`,
639 REWRITE_TAC[closure; PROVABLE_GENERALIZE]);;
641 let DEFINABLE_DEFINABLE_BY = prove
642 (`definable = definable_by (\x. T)`,
643 REWRITE_TAC[FUN_EQ_THM; definable; definable_by]);;
645 let DEFINABLE_ONEVAR = prove
646 (`definable s <=> ?p x. (FV p = {x}) /\ !v. holds v p <=> (v x) IN s`,
647 REWRITE_TAC[definable] THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
648 DISCH_THEN(X_CHOOSE_THEN `p:form` (X_CHOOSE_TAC `x:num`)) THEN
649 EXISTS_TAC `(V x === V x) && formsubst (\y. if y = x then V x else Z) p` THEN
650 EXISTS_TAC `x:num` THEN
651 ASM_REWRITE_TAC[HOLDS_FORMSUBST; FORMSUBST_FV; FV; holds] THEN
652 REWRITE_TAC[COND_RAND; EXTENSION; IN_ELIM_THM; IN_SING; FVT; IN_UNION;
653 COND_EXPAND; NOT_IN_EMPTY; o_THM; termval] THEN
656 let CLOSED_TRUE_OR_FALSE = prove
657 (`!p. closed p ==> true p \/ true(Not p)`,
658 REWRITE_TAC[closed; true_def; holds] THEN REPEAT STRIP_TAC THEN
659 ASM_MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
661 let SEMCOMPLETE_IMP_COMPLETE = prove
662 (`!A. semcomplete A ==> complete A`,
663 REWRITE_TAC[semcomplete; complete] THEN MESON_TAC[CLOSED_TRUE_OR_FALSE]);;
665 let SOUND_CLOSED = prove
666 (`sound A <=> !p. closed p /\ A |-- p ==> true p`,
667 REWRITE_TAC[sound] THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
668 MESON_TAC[TRUE_CLOSURE; PROVABLE_CLOSURE; CLOSED_CLOSURE]);;
670 let SOUND_IMP_CONSISTENT = prove
671 (`!A. sound A ==> consistent A`,
672 REWRITE_TAC[sound; consistent; CONSISTENT_ALT] THEN
673 SUBGOAL_THEN `~(true False)` (fun th -> MESON_TAC[th]) THEN
674 REWRITE_TAC[true_def; holds]);;
676 let SEMCOMPLETE_SOUND_EQ_CONSISTENT = prove
677 (`!A. semcomplete A ==> (sound A <=> consistent A)`,
678 REWRITE_TAC[semcomplete] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN
679 REWRITE_TAC[SOUND_IMP_CONSISTENT] THEN
680 REWRITE_TAC[consistent; SOUND_CLOSED] THEN
681 ASM_MESON_TAC[CLOSED_TRUE_OR_FALSE]);;