Arithmetic/sigmacomplete.ml

   1 (* ========================================================================= *)
   2 (* Sigma_1 completeness of Robinson's axioms Q.                              *)
   3 (* ========================================================================= *)
   4
   5 let robinson = new_definition
   6  `robinson =
   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)))`;;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* Individual "axioms" and their instances.                                  *)
  18 (* ------------------------------------------------------------------------- *)
  19
  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}`))));;
  23
  24 let suc_inj' = prove
  25  (`!s t. {robinson} |-- Suc(s) === Suc(t) --> s === t`,
  26   REWRITE_TAC[specl_rule [`s:term`; `t:term`] suc_inj]);;
  27
  28 let num_cases' = prove
  29  (`!t z. ~(z IN FVT t)
  30            ==> {robinson} |--  (Not(t === Z) <-> ??z (t === Suc(V z)))`,
  31   REPEAT STRIP_TAC THEN
  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
  55     ASM_MESON_TAC[]]);;
  56
  57 let add_0' = prove
  58  (`!t. {robinson} |--  Z ++ t === t`,
  59   REWRITE_TAC[spec_rule `t:term` add_0]);;
  60
  61 let add_suc' = prove
  62  (`!s t. {robinson} |--  Suc(s) ++ t === Suc(s ++ t)`,
  63   REWRITE_TAC[specl_rule [`s:term`; `t:term`] add_suc]);;
  64
  65 let mul_0' = prove
  66  (`!t. {robinson} |--  Z ** t === Z`,
  67   REWRITE_TAC[spec_rule `t:term` mul_0]);;
  68
  69 let mul_suc' = prove
  70  (`!s t. {robinson} |--  Suc(s) ** t === t ++ s ** t`,
  71   REWRITE_TAC[specl_rule [`s:term`; `t:term`] mul_suc]);;
  72
  73 let lt_def' = prove
  74  (`!s t. {robinson} |--  (s << t <-> Suc(s) <<= t)`,
  75   REWRITE_TAC[specl_rule [`s:term`; `t:term`] lt_def]);;
  76
  77 (* ------------------------------------------------------------------------- *)
  78 (* All ground terms can be evaluated by proof.                               *)
  79 (* ------------------------------------------------------------------------- *)
  80
  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]);;
  85
  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]]);;
  95
  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];
 104     ALL_TAC] THEN
 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]);;
 110
 111 (* ------------------------------------------------------------------------- *)
 112 (* Convenient stepping theorems for atoms and other useful lemmas.           *)
 113 (* ------------------------------------------------------------------------- *)
 114
 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]
 119    `A |-- p <-> q
 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]
 123          lemma0
 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`;;
 128
 129 let CANONIZE_TAC =
 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]);;
 134
 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]);;
 138
 139 let suc_le_eq = prove
 140  (`!s t. {robinson} |-- Suc s <<= Suc t <-> s <<= t`,
 141   gens_tac [0;1] THEN
 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']);;
 151
 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']);;
 157
 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']);;
 161
 162 let not_suc_eq_0 = prove
 163  (`!t. {robinson} |-- Suc t === Z --> False`,
 164   gen_tac 1 THEN
 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]]);;
 171
 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`
 179   MP_TAC THENL
 180    [ALL_TAC;
 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']);;
 189
 190 let not_lt_0 = prove
 191  (`!t. {robinson} |-- t << Z --> False`,
 192   MESON_TAC[not_suc_le_0; lt_def'; imp_trans; iff_imp1]);;
 193
 194 (* ------------------------------------------------------------------------- *)
 195 (* Evaluation of atoms built from numerals by proof.                         *)
 196 (* ------------------------------------------------------------------------- *)
 197
 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]);;
 202
 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]);;
 212
 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]);;
 218
 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]);;
 225
 226 let ATOM_EQ_TRUE = prove
 227  (`!m n. m = n ==> {robinson} |-- numeral m === numeral n`,
 228   MESON_TAC[axiom_eqrefl]);;
 229
 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
 236   CONJ_TAC THENL
 237    [MP_TAC(itlist spec_rule [`numeral(m + n)`; `numeral m`] le_def) THEN
 238     MESON_TAC[iff_imp2];
 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]]);;
 242
 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]);;
 249
 250 (* ------------------------------------------------------------------------- *)
 251 (* A kind of case analysis rule; might make it induction in case of PA.      *)
 252 (* ------------------------------------------------------------------------- *)
 253
 254 let FORMSUBST_FORMSUBST_SAME_NONE = prove
 255  (`!s t x p.
 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
 263     ASM SET_TAC[FVT];
 264     ALL_TAC] 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
 269   CONJ_TAC THENL
 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]])]);;
 283
 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`,
 288   let lemma = prove
 289    (`!A p x t. A |-- formsubst (x |=> t) p ==> A |-- V x === t --> p`,
 290     REPEAT GEN_TAC THEN
 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
 296   REPEAT GEN_TAC THEN
 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];
 304     ALL_TAC] THEN
 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
 310     ASM SET_TAC[];
 311     ALL_TAC] 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]);;
 326
 327 (* ------------------------------------------------------------------------- *)
 328 (* Now full Sigma-1 completeness.                                            *)
 329 (* ------------------------------------------------------------------------- *)
 330
 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)`,
 335   let lemma1 = prove
 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;
 345       ALL_TAC] THEN
 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
 355       rand o snd) THEN
 356     REWRITE_TAC[FVT; FVT_NUMERAL] THEN DISCH_THEN SUBST1_TAC THEN
 357     REWRITE_TAC[termsubst; ASSIGN; numeral]) in
 358   let lemma2 = prove
 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
 367   let lemma3 = prove
 368    (`!v x t p.
 369           FVT t = {} /\
 370           (!m. m < termval v t
 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
 378     ASM_MESON_TAC[])
 379   and lemma4 = prove
 380    (`!v x t p.
 381           FVT t = {} /\
 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
 390     ASM_MESON_TAC[])
 391   and lemma5 = prove
 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
 403   ONCE_REWRITE_TAC
 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
 406   CONJ_TAC THENL
 407    [CONJ_TAC THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[holds] THEN
 408     MESON_TAC[imp_refl; truth];
 409     ALL_TAC] THEN
 410   CONJ_TAC THENL
 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];
 430     ALL_TAC] THEN
 431   CONJ_TAC THENL
 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[];
 438     ALL_TAC] THEN
 439   CONJ_TAC THENL
 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
 460     ASM_MESON_TAC[];
 461     ALL_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
 521       ANTS_TAC THENL
 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
 533         REWRITE_TAC[ispec]];
 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]]]);;
 564
 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 (* ------------------------------------------------------------------------- *)
 569
 570 let G1_ROBINSON = prove
 571  (`!A. definable_by (SIGMA 1) (IMAGE gform A) /\
 572        consistent A /\ A |-- robinson
 573        ==> ?G. PI 1 G /\
 574                closed G /\
 575                true G /\
 576                ~(A |-- G) /\
 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
 588   SET_TAC[]);;
 589
 590 (* ------------------------------------------------------------------------- *)
 591 (* More metaproperties of axioms systems now we have some derived rules.     *)
 592 (* ------------------------------------------------------------------------- *)
 593
 594 let complete = new_definition
 595   `complete A <=> !p. closed p ==> A |-- p \/ A |-- Not p`;;
 596
 597 let sound = new_definition
 598   `sound A <=> !p. A |-- p ==> true p`;;
 599
 600 let semcomplete = new_definition
 601   `semcomplete A <=> !p. true p ==> A |-- p`;;
 602
 603 let generalize = new_definition
 604   `generalize vs p = ITLIST (!!) vs p`;;
 605
 606 let closure = new_definition
 607   `closure p = generalize (list_of_set(FV p)) p`;;
 608
 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]);;
 615
 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]);;
 621
 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[]);;
 627
 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]);;
 632
 633 let TRUE_CLOSURE = prove
 634  (`!p. true(closure p) <=> true p`,
 635   REWRITE_TAC[closure; TRUE_GENERALIZE]);;
 636
 637 let PROVABLE_CLOSURE = prove
 638  (`!A p. A |-- closure p <=> A |-- p`,
 639   REWRITE_TAC[closure; PROVABLE_GENERALIZE]);;
 640
 641 let DEFINABLE_DEFINABLE_BY = prove
 642  (`definable = definable_by (\x. T)`,
 643   REWRITE_TAC[FUN_EQ_THM; definable; definable_by]);;
 644
 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
 654   MESON_TAC[]);;
 655
 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]);;
 660
 661 let SEMCOMPLETE_IMP_COMPLETE = prove
 662  (`!A. semcomplete A ==> complete A`,
 663   REWRITE_TAC[semcomplete; complete] THEN MESON_TAC[CLOSED_TRUE_OR_FALSE]);;
 664
 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]);;
 669
 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]);;
 675
 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]);;