1(*===========================================================================*) 2(* Propositional Logic, up to soundness and completeness. The development is *) 3(* a mixture of that in Peter Johnstone's book, Notes on Logic and Set Theory*) 4(* and Peter Andrew's book, An Introduction to Mathematical Logic and Type *) 5(* Theory : to Truth Through Proof. Further discussion with John Harrison *) 6(* revealed that the completeness proof is due originally to Kalmar, *) 7(* according to an attribution in Mendelson's book. *) 8(*===========================================================================*) 9 10open HolKernel boolLib Parse bossLib pred_setTheory; 11 12local open stringLib in end; 13 14val _ = new_theory "PropLogic" 15 16(*---------------------------------------------------------------------------*) 17(* Simplification set for arithmetic and sets *) 18(*---------------------------------------------------------------------------*) 19 20val prop_ss = arith_ss ++ pred_setLib.PRED_SET_ss; 21 22(*---------------------------------------------------------------------------*) 23(* Useful lemmas about sets. *) 24(*---------------------------------------------------------------------------*) 25 26val SUBSET_INSERT_MONO = Q.prove 27(`!A B x. A SUBSET B ==> (x INSERT A) SUBSET (x INSERT B)`, 28 RW_TAC prop_ss [SUBSET_DEF]); 29 30val IN_MONO = Q.prove 31(`!x s. x IN s ==> !h. x IN (h INSERT s)`, 32 RW_TAC prop_ss []); 33 34val IMAGE_CONG = Q.prove 35(`!f1 f2 s. (!x. x IN s ==> (f1 x = f2 x)) ==> (IMAGE f1 s = IMAGE f2 s)`, 36 RW_TAC prop_ss [IN_IMAGE, EXTENSION] THEN METIS_TAC[]); 37 38val DIFF_UNION = Q.prove 39(`!x y. y SUBSET x ==> ((x DIFF y) UNION y = x)`, 40 RW_TAC prop_ss [EXTENSION,SUBSET_DEF] THEN METIS_TAC[]); 41 42val DIFF_INTER = Q.prove 43(`!x y. (x DIFF y) INTER y = {}`, 44 RW_TAC prop_ss [EXTENSION] THEN METIS_TAC[]); 45 46val lem1 = Q.prove 47(`!e s1 s2. (e INSERT s1) UNION s2 = s1 UNION (e INSERT s2)`, 48 RW_TAC prop_ss [EXTENSION] THEN METIS_TAC []); 49 50val lem2 = Q.prove 51(`!e s1 s2. ~(e IN s1) /\ ~(e IN s2) ==> 52 ((e INSERT s1) INTER s2 = s1 INTER (e INSERT s2))`, 53 RW_TAC prop_ss [EXTENSION] THEN METIS_TAC[]); 54 55 56(*---------------------------------------------------------------------------*) 57(* Declare HOL datatype of propositions. *) 58(*---------------------------------------------------------------------------*) 59 60val _ = Hol_datatype `prop = Var of string 61 | False 62 | Imp of prop => prop`; 63 64(*---------------------------------------------------------------------------*) 65(* Make --> into an infix representing Imp(lication). *) 66(*---------------------------------------------------------------------------*) 67 68val _ = set_fixity "-->" (Infixr 490); 69val _ = overload_on ("-->", ``Imp``); 70 71 72(*---------------------------------------------------------------------------*) 73(* Variables of a proposition. *) 74(*---------------------------------------------------------------------------*) 75 76val Vars_def = 77 Define 78 `(Vars (Var s) = {Var s}) /\ 79 (Vars False = {}) /\ 80 (Vars (p --> q) = (Vars p) UNION (Vars q))`; 81 82val IN_Vars = Q.prove 83(`!x p. x IN Vars(p) ==> ?d. x = Var d`, 84 GEN_TAC THEN Induct THEN RW_TAC prop_ss [Vars_def] THEN METIS_TAC[]); 85 86val IN_Vars = Q.prove 87(`!x p. x IN Vars(p) ==> ?d. x = Var d`, 88 Induct_on `p` THEN RW_TAC prop_ss [Vars_def] THEN METIS_TAC[]); 89 90val FINITE_Vars = Q.prove 91(`!p. FINITE (Vars p)`, 92 Induct THEN RW_TAC prop_ss [Vars_def]); 93 94 95(*---------------------------------------------------------------------------*) 96(* Value of a proposition in an environment. Environments represented by *) 97(* functions of type string->bool. *) 98(*---------------------------------------------------------------------------*) 99 100val Value_def = 101 Define 102 `(Value env (Var s) = env s) /\ 103 (Value env False = F) /\ 104 (Value env (p --> q) = ((Value env p) ==> (Value env q)))`; 105 106(*---------------------------------------------------------------------------*) 107(* Extra variables mapped by environments do not change the result of Value. *) 108(*---------------------------------------------------------------------------*) 109 110val Value_only_on_Vars = Q.prove 111(`!p env d b. 112 ~(Var d IN Vars p) ==> 113 (Value (\x. if x=d then b else env(x)) p = Value env p)`, 114 Induct THEN RW_TAC prop_ss [Value_def,Vars_def]); 115 116 117(*---------------------------------------------------------------------------*) 118(* A tautology evaluates to T in every environment. *) 119(*---------------------------------------------------------------------------*) 120 121val Tautology_def = 122 Define 123 `Tautology p = !env. Value env p = T`; 124 125 126(*---------------------------------------------------------------------------*) 127(* Define the inference system. First the axioms. Note S and K similarity. *) 128(*---------------------------------------------------------------------------*) 129 130val Ax1_def = 131 Define 132 `Ax1 p q = p --> q --> p`; 133 134val Ax2_def = 135 Define 136 `Ax2 p q r = (p --> q --> r) --> (p --> q) --> (p --> r)`; 137 138val Ax3_def = 139 Define 140 `Ax3 p = ((p --> False) --> False) --> p`; 141 142 143(*---------------------------------------------------------------------------*) 144(* Syntactic entailment via an inductive definition. *) 145(*---------------------------------------------------------------------------*) 146 147val (is_thm_rules, is_thm_ind, is_thm_cases) = 148 Hol_reln 149 `(!p q (H:prop set). is_thm H (Ax1 p q)) /\ 150 (!p q r H. is_thm H (Ax2 p q r)) /\ 151 (!p H. is_thm H (Ax3 p)) /\ 152 (!p H. p IN H ==> is_thm H p) /\ 153 (!H p q. is_thm H (p --> q) /\ is_thm H p ==> is_thm H q)`; 154 155val [is_thm_Ax1, is_thm_Ax2, 156 is_thm_Ax3, is_thm_inH, is_thm_MP] = CONJUNCTS is_thm_rules; 157 158(*---------------------------------------------------------------------------*) 159(* Make ||- into an infix representing syntactic entailment. *) 160(*---------------------------------------------------------------------------*) 161 162val _ = set_fixity "||-" (Infix(NONASSOC, 450)); 163val _ = overload_on ("||-", ``is_thm``); 164 165(*---------------------------------------------------------------------------*) 166(* Make a "strong" version of induction on the structure of a proof. *) 167(* Not actually used in rest of the development. *) 168(*---------------------------------------------------------------------------*) 169 170val is_thm_strong_ind = 171 IndDefLib.derive_strong_induction (is_thm_rules, is_thm_ind); 172 173 174(*---------------------------------------------------------------------------*) 175(* An example object-logic theorem and its proof. *) 176(*---------------------------------------------------------------------------*) 177 178val p_Imp_p = Q.prove 179(`!H p. H ||- (p --> p)`, 180 REPEAT GEN_TAC THEN 181 `H ||- (Ax1 p (p --> p))` by METIS_TAC [is_thm_rules] THEN 182 `H ||- (Ax2 p (p --> p) p)` by METIS_TAC [is_thm_rules] THEN 183 `H ||- ((p --> p --> p) --> (p --> p))` 184 by METIS_TAC [is_thm_rules,Ax1_def,Ax2_def] THEN 185 `H ||- Ax1 p p` by METIS_TAC [is_thm_rules] THEN 186 METIS_TAC [Ax1_def,is_thm_rules]); 187 188 189(*---------------------------------------------------------------------------*) 190(* Weakening and the Deduction theorem are used in the completeness proof *) 191(* and help in many object-logic deductions. *) 192(*---------------------------------------------------------------------------*) 193 194val weakening_lemma = Q.prove 195(`!G p. G ||- p ==> !H. (G SUBSET H) ==> H ||- p`, 196 HO_MATCH_MP_TAC is_thm_ind 197 THEN REPEAT CONJ_TAC THENL 198 [METIS_TAC [is_thm_rules], 199 METIS_TAC [is_thm_rules], 200 METIS_TAC [is_thm_rules], 201 METIS_TAC [is_thm_rules,SUBSET_DEF], 202 METIS_TAC [is_thm_rules]]); 203 204val WEAKENING = Q.prove 205(`!G H p. G ||- p /\ (G SUBSET H) ==> H ||- p`, 206 METIS_TAC [weakening_lemma]); 207 208val Ded1 = Q.prove 209(`!H p q. H ||- (p --> q) ==> (p INSERT H) ||- q`, 210 REPEAT STRIP_TAC THEN 211 `(p INSERT H) ||- (p --> q)` by METIS_TAC[WEAKENING,SUBSET_DEF,IN_INSERT] THEN 212 `(p INSERT H) ||- p` by METIS_TAC[is_thm_rules,IN_INSERT] THEN 213 `(p INSERT H) ||- q` by METIS_TAC[is_thm_rules]); 214 215val Ded2_lemma = Q.prove 216(`!H1 q. H1 ||- q ==> !p H. (H1 = p INSERT H) ==> H ||- (p --> q)`, 217 HO_MATCH_MP_TAC is_thm_ind THEN RW_TAC prop_ss [] THENL 218 [METIS_TAC [is_thm_rules, Ax1_def], 219 METIS_TAC [is_thm_rules, Ax1_def], 220 METIS_TAC [is_thm_rules, Ax1_def], 221 Cases_on `q=p` THENL 222 [(* nts: (p --> p) *) 223 FULL_SIMP_TAC prop_ss [] THEN RW_TAC prop_ss [p_Imp_p], 224 (* (same as cases 1-3)*) 225 METIS_TAC [is_thm_rules, Ax1_def,IN_INSERT]], 226 `H ||- (p --> q)` by METIS_TAC [] THEN 227 `H ||- (p --> q --> q')` by METIS_TAC[] THEN REPEAT(WEAKEN_TAC is_forall) THEN 228 `H ||- ((p --> q --> q') --> (p --> q) --> (p --> q'))` 229 by METIS_TAC [is_thm_rules, Ax2_def] THEN 230 METIS_TAC [is_thm_rules]]); 231 232val Ded2 = Q.prove 233(`!H p q. (p INSERT H) ||- q ==> H ||- (p --> q)`, 234 METIS_TAC [Ded2_lemma]); 235 236val DEDUCTION = Q.prove 237(`!H p q. is_thm (p INSERT H) q <=> H ||- (p --> q)`, 238 METIS_TAC [Ded1, Ded2]); 239 240(*---------------------------------------------------------------------------*) 241(* Applications of Deduction Thm: false implies any prop, plus some others *) 242(*---------------------------------------------------------------------------*) 243 244val P_Imp_P = Q.prove 245(`!H p. (p INSERT H) ||- p`, 246 METIS_TAC [p_Imp_p,DEDUCTION]); 247 248val False_Imp_P = Q.prove 249(`!H p. H ||- (False --> p)`, 250 REPEAT GEN_TAC THEN 251 `H ||- (Ax1 False (p --> False))` 252 by METIS_TAC [is_thm_rules,WEAKENING,SUBSET_EMPTY] THEN 253 FULL_SIMP_TAC prop_ss [Ax1_def] THEN 254 `(False INSERT H) ||- ((p --> False) --> False)` 255 by METIS_TAC [DEDUCTION] THEN 256 `(False INSERT H) ||- (((p --> False) --> False) --> p)` 257 by METIS_TAC [is_thm_Ax3,Ax3_def, 258 WEAKENING,SUBSET_INSERT_RIGHT,SUBSET_REFL] THEN 259 `(False INSERT H) ||- p` by METIS_TAC [is_thm_MP ] THEN 260 METIS_TAC [DEDUCTION]); 261 262(*---------------------------------------------------------------------------*) 263(* Contrapositive: (p --> q) --> (~q --> ~p) *) 264(*---------------------------------------------------------------------------*) 265 266val Contrapos = Q.prove 267(`!H p q. H ||- ((p --> q) --> ((q --> False) --> (p --> False)))`, 268 REPEAT GEN_TAC THEN 269 `(p INSERT (q --> False) INSERT (p --> q) INSERT H) ||- (p --> q)` 270 by METIS_TAC [DEDUCTION, p_Imp_p,WEAKENING,EMPTY_SUBSET, 271 SUBSET_INSERT_MONO, INSERT_COMM] THEN 272 `(p INSERT (q --> False) INSERT (p --> q) INSERT H) ||- p` 273 by METIS_TAC [DEDUCTION, p_Imp_p,WEAKENING,EMPTY_SUBSET, 274 SUBSET_INSERT_MONO, INSERT_COMM] THEN 275 `(p INSERT (q --> False) INSERT (p --> q) INSERT H) ||- q` 276 by METIS_TAC [is_thm_MP] THEN 277 `(p INSERT (q --> False) INSERT (p --> q) INSERT H) ||- (q --> False)` 278 by (MATCH_MP_TAC WEAKENING THEN Q.EXISTS_TAC `{q --> False}` THEN 279 RW_TAC prop_ss [P_Imp_P]) THEN 280 `(p INSERT (q --> False) INSERT (p --> q) INSERT H) ||- False` 281 by METIS_TAC [is_thm_MP] THEN 282 METIS_TAC [DEDUCTION]); 283 284(*---------------------------------------------------------------------------*) 285(* The following statement can also be read (more comfortably) as *) 286(* *) 287(* (p --> r) --> (q --> r) --> (p \/ q) --> r *) 288(* *) 289(*---------------------------------------------------------------------------*) 290 291val Disj_Elim = Q.prove 292(`!H p q r. 293 H ||- ((p --> r) --> (q --> r) --> ((p --> False) --> q) --> r)`, 294 REPEAT GEN_TAC THEN 295 `((r --> False) INSERT ((p --> False) --> q) INSERT 296 (q --> r) INSERT (p --> r) INSERT H) ||- (r --> False)` 297 by METIS_TAC [DEDUCTION, p_Imp_p,WEAKENING,EMPTY_SUBSET,SUBSET_INSERT_MONO] 298 THEN 299 `((r --> False) INSERT ((p --> False) --> q) INSERT 300 (q --> r) INSERT (p --> r) INSERT H) ||- (q --> r)` 301 by (MATCH_MP_TAC WEAKENING THEN Q.EXISTS_TAC `{q --> r}` 302 THEN RW_TAC prop_ss [P_Imp_P]) THEN 303 `((r --> False) INSERT((p --> False) --> q) INSERT 304 (q --> r) INSERT (p --> r) INSERT H) ||- ((r --> False) --> (q --> False))` 305 by METIS_TAC [is_thm_MP,Contrapos] THEN 306 `((r --> False) INSERT ((p --> False) --> q) INSERT 307 (q --> r) INSERT (p --> r) INSERT H) ||- (q --> False)` 308 by METIS_TAC [is_thm_MP] THEN 309 `((r --> False) INSERT ((p --> False) --> q) INSERT 310 (q --> r) INSERT (p --> r) INSERT H) ||- ((p --> False) --> q)` 311 by (MATCH_MP_TAC WEAKENING THEN Q.EXISTS_TAC `{(p --> False) --> q}` 312 THEN RW_TAC prop_ss [P_Imp_P]) THEN 313 `((r --> False) INSERT ((p --> False) --> q) INSERT 314 (q --> r) INSERT (p --> r) INSERT H) ||- ((p --> False) --> False)` 315 by METIS_TAC [is_thm_MP,Contrapos] THEN 316 `((r --> False) INSERT ((p --> False) --> q) INSERT 317 (q --> r) INSERT (p --> r) INSERT H) ||- p` 318 by METIS_TAC [is_thm_MP,is_thm_Ax3,Ax3_def] THEN 319 `((r --> False) INSERT ((p --> False) --> q) INSERT 320 (q --> r) INSERT (p --> r) INSERT H) ||- (p --> r)` 321 by (MATCH_MP_TAC WEAKENING THEN Q.EXISTS_TAC `{p --> r}` 322 THEN RW_TAC prop_ss [P_Imp_P]) THEN 323 `((r --> False) INSERT ((p --> False) --> q) INSERT 324 (q --> r) INSERT (p --> r) INSERT H) ||- r` 325 by METIS_TAC [is_thm_MP] THEN 326 `((r --> False) INSERT ((p --> False) --> q) INSERT 327 (q --> r) INSERT (p --> r) INSERT H) ||- False` 328 by METIS_TAC [is_thm_MP] THEN 329 `(((p --> False) --> q) INSERT (q --> r) INSERT 330 (p --> r) INSERT H) ||- ((r --> False) --> False)` 331 by METIS_TAC [DEDUCTION] THEN 332 `(((p --> False) --> q) INSERT (q --> r) INSERT (p --> r) INSERT H) ||- r` 333 by METIS_TAC [is_thm_Ax3, Ax3_def, is_thm_MP] THEN 334 METIS_TAC [DEDUCTION]); 335 336 337(*---------------------------------------------------------------------------*) 338(* (p --> q) --> (~p --> q) --> q *) 339(*---------------------------------------------------------------------------*) 340 341val Case_Split = Q.prove 342(`!H p q. H ||- ((p --> q) --> ((p --> False) --> q) --> q)`, 343 let val lem = Q.SPECL [`H`,`p`,`p --> False`, `q`] Disj_Elim 344 in 345 REPEAT GEN_TAC THEN ASSUME_TAC lem THEN 346 `(((p --> False) --> q) INSERT (p --> q) INSERT H) 347 ||- (((p --> False) --> p --> False) --> q)` 348 by METIS_TAC [DEDUCTION] THEN 349 `(((p --> False) --> q) INSERT (p --> q) INSERT H) 350 ||- ((p --> False) --> p --> False)` 351 by METIS_TAC [P_Imp_P,DEDUCTION] THEN 352 `(((p --> False) --> q) INSERT (p --> q) INSERT H) ||- q` 353 by METIS_TAC [is_thm_MP] 354 THEN METIS_TAC [DEDUCTION] 355 end); 356 357(*===========================================================================*) 358(* Soundness: every theorem is a tautology. Note that we have to modify *) 359(* the statement in order for it to be in the right shape for induction *) 360(* (on the construction of a proof) to apply. *) 361(*===========================================================================*) 362 363(* 364g `!H p. H ||- p ==> (H={}) ==> Tautology p`; 365e (HO_MATCH_MP_TAC is_thm_ind); 366e (RW_TAC prop_ss [Tautology_def]); 367(*1*) 368e (RW_TAC prop_ss [Ax1_def, Value_def]); 369(*2*) 370e (RW_TAC prop_ss [Ax2_def, Value_def]); 371(*3*) 372e (RW_TAC prop_ss [Ax3_def, Value_def]); 373(*4*) 374e (FULL_SIMP_TAC prop_ss []); 375(*5*) 376e (FULL_SIMP_TAC prop_ss [Value_def]); 377*) 378 379(*---------------------------------------------------------------------------*) 380(* Previous proof revised into a single tactic invocation. *) 381(*---------------------------------------------------------------------------*) 382 383val Sound_lemma = Q.prove 384(`!H p. H ||- p ==> (H = {}) ==> Tautology p`, 385 HO_MATCH_MP_TAC is_thm_ind 386 THEN RW_TAC prop_ss [Tautology_def, Value_def, Ax1_def, Ax2_def, Ax3_def] 387 THEN FULL_SIMP_TAC prop_ss []); 388 389val Soundness = Q.store_thm( 390 "Soundness", 391 `!p. ({} ||- p) ==> Tautology p`, 392 METIS_TAC [Sound_lemma]); 393 394 395(*===========================================================================*) 396(* Completeness: every tautology is a theorem. *) 397(* *) 398(* First define IValue, which changes the syntax of p, if need be, so that *) 399(* p will evaluate to T in the given env. *) 400(*===========================================================================*) 401 402val IValue_def = 403 Define 404 `IValue env p = if Value env p = T then p else (p --> False)`; 405 406(*---------------------------------------------------------------------------*) 407(* Sanity check, not used later. *) 408(*---------------------------------------------------------------------------*) 409 410val Value_IValue = Q.prove 411(`!p env. Value env (IValue env p) = T`, 412 RW_TAC prop_ss [IValue_def,Value_def]); 413 414(*---------------------------------------------------------------------------*) 415(* Variables disjoint from those of p are not moved by IValue. *) 416(*---------------------------------------------------------------------------*) 417 418val IValue_only_on_Vars = Q.prove 419(`!p env d b. ~(Var d IN Vars p) ==> 420 (IValue (\x. if x=d then b else env(x)) p = IValue env p)`, 421 RW_TAC prop_ss [IValue_def] THEN METIS_TAC[Value_only_on_Vars]); 422 423val IMAGE_IValue_only_on_Vars = Q.prove 424(`!s env d b. ~(Var d IN s) /\ (!x. x IN s ==> ?e. x = Var e) ==> 425 (IMAGE (IValue (\x. if x=d then b else env(x))) s = 426 IMAGE (IValue env) s)`, 427 REPEAT STRIP_TAC THEN MATCH_MP_TAC IMAGE_CONG THEN 428 REPEAT STRIP_TAC THEN MATCH_MP_TAC IValue_only_on_Vars THEN 429 METIS_TAC [Vars_def,IN_INSERT,NOT_IN_EMPTY,IMAGE_CONG,IValue_only_on_Vars]); 430 431 432(*---------------------------------------------------------------------------*) 433(* Important lemma (from Peter Andrews' book "To Truth Through Proof"). *) 434(*---------------------------------------------------------------------------*) 435 436val Andrews_Lemma = Q.store_thm( 437 "Andrews_Lemma", 438 `!p env H. 439 (Vars p) SUBSET H ==> (IMAGE (IValue env) H) ||- (IValue env p)`, 440 Induct THENL 441 [MAP_EVERY Q.X_GEN_TAC [`s`, `env`, `H`] THEN RW_TAC prop_ss [] THEN 442 FULL_SIMP_TAC prop_ss [Vars_def] THEN 443 `H ||- (Var s)` by METIS_TAC [is_thm_inH] THEN 444 `IValue env (Var s) IN (IMAGE (IValue env) H)` by METIS_TAC[IMAGE_IN] 445 THEN METIS_TAC[is_thm_inH], 446 RW_TAC prop_ss [IValue_def,Value_def] THEN 447 METIS_TAC [p_Imp_p, EMPTY_SUBSET,WEAKENING], 448 RW_TAC prop_ss [] THEN 449 `(IMAGE (IValue env) H) ||- (IValue env p) /\ (* use IH *) 450 (IMAGE (IValue env) H) ||- (IValue env p')` 451 by METIS_TAC [Vars_def,UNION_SUBSET] THEN 452 NTAC 2 (POP_ASSUM MP_TAC) THEN REPEAT (WEAKEN_TAC (K true)) THEN 453 SIMP_TAC prop_ss [IValue_def,Value_def] THEN 454 RW_TAC prop_ss [] THEN FULL_SIMP_TAC std_ss [] THEN RW_TAC std_ss [] THENL 455 [(*3.1*) 456 `(p INSERT (IMAGE (IValue env) H)) ||- p'` 457 by METIS_TAC [WEAKENING,SUBSET_INSERT_RIGHT,SUBSET_REFL] 458 THEN METIS_TAC[DEDUCTION], 459 (*3.2*) 460 `((p --> p') INSERT (IMAGE (IValue env) H)) ||- (p --> p')` 461 by METIS_TAC [IN_INSERT, is_thm_inH] THEN 462 `((p --> p') INSERT (IMAGE (IValue env) H)) ||- p /\ 463 ((p --> p') INSERT (IMAGE (IValue env) H)) ||- (p' --> False)` 464 by METIS_TAC [WEAKENING,SUBSET_INSERT_RIGHT,SUBSET_REFL] THEN 465 `((p --> p') INSERT (IMAGE (IValue env) H)) ||- p'` 466 by METIS_TAC [is_thm_MP] THEN 467 `((p --> p') INSERT (IMAGE (IValue env) H)) ||- False` 468 by METIS_TAC [is_thm_MP] THEN 469 METIS_TAC[DEDUCTION], 470 (*3.3*) 471 `(p INSERT (IMAGE (IValue env) H)) ||- False` by METIS_TAC [DEDUCTION] THEN 472 `(p INSERT (IMAGE (IValue env) H)) ||- p'` 473 by METIS_TAC [False_Imp_P,is_thm_MP] 474 THEN METIS_TAC[DEDUCTION], 475 (*3.4*) 476 `(p INSERT (IMAGE (IValue env) H)) ||- False` by METIS_TAC [DEDUCTION] THEN 477 `(p INSERT (IMAGE (IValue env) H)) ||- p'` 478 by METIS_TAC [False_Imp_P,is_thm_MP] 479 THEN METIS_TAC[DEDUCTION]]]); 480 481(*---------------------------------------------------------------------------*) 482(* Proof by induction on the number of variables removed from Vars(p) to get *) 483(* V. If no variables dropped (base case), then V = Vars(p) and can use *) 484(* Andrews' Lemma. Otherwise, we have removed n variables and can still *) 485(* prove the prop; if one more is removed, need to show the prop is still *) 486(* provable. *) 487(*---------------------------------------------------------------------------*) 488 489val Completeness_Lemma = Q.prove 490(`!p V. Tautology p /\ (V SUBSET (Vars p)) 491 ==> 492 !env. (IMAGE (IValue env) V) ||- p`, 493 REPEAT GEN_TAC THEN STRIP_TAC THEN 494 `?U. (U UNION V = Vars(p)) /\ (U INTER V = {}) /\ FINITE U` 495 by (Q.EXISTS_TAC `Vars(p) DIFF V` THEN 496 METIS_TAC [DIFF_UNION,DIFF_INTER,FINITE_UNION,FINITE_Vars]) THEN 497 POP_ASSUM (fn th => 498 NTAC 3 (POP_ASSUM MP_TAC) THEN Q.ID_SPEC_TAC `V` THEN MP_TAC th) THEN 499 Q.ID_SPEC_TAC `U` THEN 500 HO_MATCH_MP_TAC FINITE_INDUCT THEN RW_TAC prop_ss [] THENL 501 [METIS_TAC [Andrews_Lemma,IValue_def,Tautology_def], 502 `U UNION (e INSERT V) = Vars p` by METIS_TAC [lem1] THEN 503 `e IN Vars(p)` by METIS_TAC [IN_UNION, IN_INSERT] THEN 504 `(e INSERT V) SUBSET Vars p` by METIS_TAC [INSERT_SUBSET] THEN 505 `~(e IN V)` 506 by (Q.PAT_ASSUM `x INTER y = {}` MP_TAC THEN 507 RW_TAC prop_ss [EXTENSION] THEN METIS_TAC[]) THEN 508 `U INTER (e INSERT V) = {}` by METIS_TAC [lem2] THEN 509 (* finally, use IH *) 510 `!env. is_thm (IMAGE (IValue env) (e INSERT V)) p` 511 by METIS_TAC[] THEN 512 REPEAT (WEAKEN_TAC is_eq) THEN POP_ASSUM MP_TAC THEN 513 REPEAT (WEAKEN_TAC is_forall) THEN Q.PAT_ASSUM `FINITE s` (K ALL_TAC) THEN 514 Q.PAT_ASSUM `(e INSERT V) SUBSET Vars p` (K ALL_TAC) THEN STRIP_TAC THEN 515 `?d. e = Var(d)` by METIS_TAC [IN_Vars] THEN RW_TAC std_ss [] THEN 516 `(IMAGE (IValue (\x. if x=d then T else env(x))) (Var(d) INSERT V)) ||- p` 517 by METIS_TAC[] THEN 518 `(IMAGE (IValue (\x. if x=d then F else env(x))) (Var(d) INSERT V)) ||- p` 519 by METIS_TAC[] THEN 520 Q.PAT_ASSUM `!env. (f env) ||- p` (K ALL_TAC) THEN 521 FULL_SIMP_TAC std_ss [IMAGE_INSERT,IValue_def,Value_def] THEN 522 `(Var d INSERT IMAGE (IValue(\x. if x=d then T else env x)) V) ||- p /\ 523 ((Var d --> False) INSERT 524 IMAGE (IValue(\x. if x=d then F else env x)) V) ||- p` 525 by METIS_TAC [] THEN 526 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 527 `!x. x IN V ==> ?e. x = Var(e)` by METIS_TAC [SUBSET_DEF,IN_Vars] THEN 528 `!b. IMAGE (IValue (\x. (if x = d then b else env x))) V = 529 IMAGE (IValue env) V` by METIS_TAC [IMAGE_IValue_only_on_Vars] THEN 530 RW_TAC prop_ss [] THEN 531 (* Now just do a little object logic proof. *) 532 `(IMAGE (IValue env) V) ||- (Var d --> p)` by METIS_TAC [DEDUCTION] THEN 533 `(IMAGE (IValue env) V) ||- ((Var d --> False) --> p)` 534 by METIS_TAC [DEDUCTION] THEN 535 `(IMAGE(IValue env) V) ||- ((Var d --> p) --> ((Var d --> False) --> p) --> p)` 536 by METIS_TAC [Case_Split] THEN 537 METIS_TAC [is_thm_MP]]); 538 539 540(*---------------------------------------------------------------------------*) 541(* Completeness is then an easy consequence. *) 542(*---------------------------------------------------------------------------*) 543 544val Completeness = Q.store_thm( 545 "Completeness", 546 `!p. Tautology p ==> {} ||- p`, 547 METIS_TAC [EMPTY_SUBSET,IMAGE_EMPTY,Completeness_Lemma]); 548 549val _ = export_theory() 550