1open HolKernel Parse boolLib bossLib; 2 3open mp_then 4 5open pred_setTheory set_relationTheory listTheory 6open folSkolemTheory folPrenexTheory folModelsTheory folLangTheory 7 folPropTheory 8 9fun f $ x = f x 10 11val _ = new_theory "folCanon"; 12 13(* ========================================================================= *) 14(* Canonical models in FOL and their use to derive classic metatheorems. *) 15(* ========================================================================= *) 16 17(* ------------------------------------------------------------------------- *) 18(* Domain of a canonical model for given language. *) 19(* ------------------------------------------------------------------------- *) 20 21Inductive terms: 22 (���x. terms fns (V x)) ��� 23 (���f l. (f,LENGTH l) ��� fns ��� (���t. MEM t l ��� terms fns t) ��� 24 terms fns (Fn f l)) 25End 26 27val stupid_canondom_lemma = Q.prove( 28 ������t. t ��� terms (FST L) ��� term_functions t ��� FST L���, 29 simp[IN_DEF] >> Induct_on ���terms��� >> 30 dsimp[SUBSET_DEF, MEM_MAP] >> metis_tac[]); 31 32Theorem finite_subset_instance: 33 ���t'. FINITE t' ��� t' ��� { formsubst v p | P v ��� p ��� s} ��� 34 ���t. FINITE t ��� t ��� s ��� t' ��� {formsubst v p | P v ��� p ��� t} 35Proof 36 Induct_on���FINITE��� >> simp[] >> rw[] 37 >- (qexists_tac ��������� >> simp[]) >> fs[] >> 38 rename [���p ��� s���, ���formsubst v p ��� t'���, ���t ��� s���] >> 39 qexists_tac ���p INSERT t��� >> simp[] >> conj_tac >- metis_tac[] >> 40 fs[SUBSET_DEF] >>metis_tac[] 41QED 42 43Theorem finite_subset_SKOLEM: 44 ���s u. FINITE u ��� u ��� { SKOLEM p | p ��� s} ��� 45 ���t. FINITE t ��� t ��� s ��� u = {SKOLEM p | p ��� t} 46Proof 47 Induct_on ���FINITE��� >> simp[] >> rw[] 48 >- (qexists_tac ��������� >> simp[]) >> 49 first_x_assum (drule_then (qx_choose_then ���tt��� strip_assume_tac)) >> rw[] >> 50 rename [���p ��� s���] >> qexists_tac ���p INSERT tt��� >> simp[] >> 51 dsimp[EXTENSION] 52QED 53 54Theorem valuation_exists: 55 ���M. M.Dom ��� ��� ��� ���v:num -> ��. valuation M v 56Proof 57 simp[EXTENSION, PULL_EXISTS, valuation_def] >> qx_genl_tac [���M���, ���x���] >> 58 strip_tac >> qexists_tac ���K x��� >> simp[] 59QED 60 61Theorem holds_FOLDR_exists: 62 ���M xs v. 63 holds M v (FOLDR Exists p xs) ��� 64 ���as. LENGTH as = LENGTH xs ��� EVERY M.Dom as ��� 65 holds M (FOLDL (combin$C (UNCURRY UPDATE)) v (MAP2 $, xs as)) p 66Proof 67 Induct_on ���xs��� >> simp[PULL_EXISTS] >> rpt gen_tac >> eq_tac 68 >- (disch_then (qx_choosel_then [���a���, ���as���] strip_assume_tac) >> 69 qexists_tac ���a::as��� >> simp[] >> fs[IN_DEF]) >> 70 simp[PULL_EXISTS] >> Cases >> simp[] >> rw[] >> 71 rename [���LENGTH as = LENGTH xs���, ���M.Dom a���] >> 72 map_every qexists_tac [���a���, ���as���] >> simp[] >> simp[IN_DEF] 73QED 74 75(* ------------------------------------------------------------------------- *) 76(* Canonical model based on the language of a set of formulas. *) 77(* ------------------------------------------------------------------------- *) 78 79Definition canonical_def: 80 canonical L M ��� M.Dom = terms (FST L) ��� ���f. M.Fun f = Fn f 81End 82 83(* ------------------------------------------------------------------------- *) 84(* Mappings between models and propositional valuations. *) 85(* ------------------------------------------------------------------------- *) 86 87Definition prop_of_model_def: 88 prop_of_model M v (Pred p l) ��� holds M v (Pred p l) 89End 90 91Definition canon_of_prop_def: 92 canon_of_prop L v = <| Dom := terms (FST L); Fun := Fn; 93 Pred := ��p zs. v (Pred p zs) |> 94End 95 96Theorem pholds_prop_of_model: 97 ���p. qfree p ��� (pholds (prop_of_model M v) p ��� holds M v p) 98Proof 99 Induct >> simp[prop_of_model_def] 100QED 101 102Theorem prop_of_canon_of_prop: 103 ���p l. prop_of_model (canon_of_prop L v) V (Pred p l) = v (Pred p l) 104Proof 105 simp[prop_of_model_def, canon_of_prop_def] >> rpt gen_tac >> 106 rpt AP_TERM_TAC >> 107 qmatch_abbrev_tac ���MAP f l = l��� >> 108 ������t. f t = t��� suffices_by simp[LIST_EQ_REWRITE, EL_MAP] >> 109 Induct >> simp[Abbr���f���, Cong MAP_CONG'] 110QED 111 112Theorem holds_canon_of_prop: 113 qfree p ��� (holds (canon_of_prop L v) V p ��� pholds v p) 114Proof 115 strip_tac >> 116 drule_then (rewrite_tac o Portable.single o GSYM) pholds_prop_of_model >> 117 Induct_on ���p��� >> simp[prop_of_canon_of_prop] 118QED 119 120Theorem holds_canon_of_prop_general: 121 qfree p ��� (holds (canon_of_prop L v1) v2 p ��� pholds v1 (formsubst v2 p)) 122Proof 123 strip_tac >> 124 drule_then (rewrite_tac o Portable.single o GSYM) pholds_prop_of_model >> 125 Induct_on ���p��� >> simp[] >> 126 simp[prop_of_model_def, canon_of_prop_def] >> 127 simp[Cong MAP_CONG', GSYM termsubst_termval] 128QED 129 130Theorem canonical_canon_of_prop: 131 canonical L (canon_of_prop L d) 132Proof 133 simp[canonical_def, canon_of_prop_def] 134QED 135 136Theorem interpretation_canon_of_prop: 137 ���L d. interpretation L (canon_of_prop L d) 138Proof 139 simp[interpretation_def, canon_of_prop_def, pairTheory.FORALL_PROD] >> 140 metis_tac[terms_rules,IN_DEF] 141QED 142 143(* ------------------------------------------------------------------------- *) 144(* Equivalence theorems for tautologies. *) 145(* ------------------------------------------------------------------------- *) 146 147Theorem prop_valid_imp_fol_valid: 148 ���p. qfree p ��� (���d. pholds d p) ��� ���M v. holds M v p 149Proof 150 metis_tac[pholds_prop_of_model] 151QED 152 153Theorem fol_valid_imp_prop_valid: 154 !p. qfree p ��� 155 (���C (v:num->term). canonical(language {p}) C ��� holds C v p) 156 ==> !d. pholds d p 157Proof 158 metis_tac[canonical_canon_of_prop, holds_canon_of_prop] 159QED 160 161(* ------------------------------------------------------------------------- *) 162(* Same thing for satisfiability. *) 163(* ------------------------------------------------------------------------- *) 164 165Theorem satisfies_psatisfies: 166 (���p. p ��� s ��� qfree p) ��� M satisfies s ��� valuation M v ��� 167 prop_of_model M v psatisfies s 168Proof 169 simp[satisfies_def, psatisfies_def] >> metis_tac[pholds_prop_of_model] 170QED 171 172Theorem psatisfies_instances: 173 (���p. p ��� s ��� qfree p) ��� 174 d psatisfies {formsubst v p | (���x. v x ��� terms (FST L)) ��� p ��� s} ��� 175 canon_of_prop L d satisfies s 176Proof 177 simp[satisfies_def, psatisfies_def, PULL_EXISTS] >> strip_tac >> 178 simp[SimpL ���$==>���, valuation_def, canon_of_prop_def] >> rpt strip_tac >> 179 ���pholds d (formsubst v p)��� by metis_tac[] >> 180 ���holds (canon_of_prop L d) V (formsubst v p)��� 181 by metis_tac[holds_canon_of_prop, qfree_formsubst] >> 182 fs[holds_formsubst] >> 183 ���termval (canon_of_prop L d) V o v = v��� suffices_by (strip_tac >> fs[]) >> 184 simp[FUN_EQ_THM] >> simp[termval_triv, canon_of_prop_def] 185QED 186 187Theorem satisfies_instances: 188 interpretation (language t) M ��� 189 (M satisfies {formsubst i p | p ��� s ��� ���x. i x ��� terms (FST (language t))} ��� 190 M satisfies s) 191Proof 192 simp[satisfies_def, PULL_EXISTS] >> rpt strip_tac >> eq_tac >> rpt strip_tac 193 >- metis_tac[formsubst_triv, IN_DEF, terms_rules] >> 194 simp[holds_formsubst] >> first_assum irule >> simp[valuation_def] >> 195 gen_tac >> irule interpretation_termval >> simp[] >> 196 qexists_tac ���predicates t��� >> 197 irule interpretation_sublang >> fs[language_def] >> 198 metis_tac[stupid_canondom_lemma, pairTheory.FST] 199QED 200 201(* ------------------------------------------------------------------------- *) 202(* So we have compactness in a strong form. *) 203(* ------------------------------------------------------------------------- *) 204 205Theorem COMPACT_CANON_QFREE: 206 (���p. p ��� s ��� qfree p) ��� 207 (���t. FINITE t ��� t ��� s ��� 208 ���M. interpretation (language ss) M ��� M.Dom ��� ��� ��� M satisfies t) ��� 209 ���C. interpretation (language ss) C ��� canonical (language ss) C ��� 210 C satisfies s 211Proof 212 rpt strip_tac >> 213 ���psatisfiable 214 { formsubst v p | (���x. v x ��� terms (FST (language ss))) ��� p ��� s }��� 215 by (rewrite_tac[psatisfiable_def, psatisfies_def] >> irule COMPACT_PROP >> 216 simp[GSYM psatisfies_def, GSYM psatisfiable_def] >> 217 qx_gen_tac ���u��� >> strip_tac >> 218 ������t. FINITE t ��� t ��� s ��� 219 u ��� {formsubst v p | 220 (���x. v x ��� terms (FST (language ss))) ��� p ��� t }��� 221 by (ho_match_mp_tac finite_subset_instance >> simp[]) >> 222 irule psatisfiable_mono >> 223 goal_assum (first_assum o mp_then Any mp_tac) >> 224 first_x_assum (drule_all_then strip_assume_tac) >> 225 drule_then (qx_choose_then ���v��� strip_assume_tac) valuation_exists >> 226 drule_then strip_assume_tac satisfies_instances >> 227 ������p. p ��� t ��� qfree p��� by metis_tac[SUBSET_DEF] >> 228 rewrite_tac[psatisfiable_def, psatisfies_def] >> 229 qexists_tac ���prop_of_model M v��� >> simp[GSYM psatisfies_def] >> 230 irule satisfies_psatisfies >> simp[PULL_EXISTS] >> 231 fs[AC CONJ_ASSOC CONJ_COMM]) >> 232 fs[psatisfiable_def] >> rename [���d psatisfies _���] >> 233 qexists_tac ���canon_of_prop (language ss) d��� >> 234 simp[canonical_canon_of_prop, interpretation_canon_of_prop, 235 psatisfies_instances] 236QED 237 238(* ------------------------------------------------------------------------- *) 239(* Tedious lemma about sublanguage. *) 240(* ------------------------------------------------------------------------- *) 241 242Theorem interpretation_restrictlanguage: 243 ���M s t. t ��� s ��� interpretation (language s) M ��� interpretation (language t) M 244Proof 245 rw[language_def] >> irule interpretation_sublang >> 246 goal_assum (first_assum o mp_then Any mp_tac) >> 247 simp[functions_def, SUBSET_DEF, PULL_EXISTS] >> metis_tac[SUBSET_DEF] 248QED 249 250Theorem interpretation_extendlanguage: 251 ���M s t. interpretation (language t) M ��� M.Dom ��� ��� ��� M satisfies t ��� 252 ���M'. M'.Dom = M.Dom ��� M'.Pred = M.Pred ��� 253 interpretation (language s) M' ��� M' satisfies t 254Proof 255 rpt strip_tac >> 256 qexists_tac ���M with Fun := ��g zs. if (g,LENGTH zs) ��� functions t then 257 M.Fun g zs 258 else @a. a ��� M.Dom��� >> 259 simp[] >> conj_tac 260 >- (fs[interpretation_def, language_def] >> rw[] >> SELECT_ELIM_TAC >> 261 fs[EXTENSION] >> metis_tac[]) >> 262 pop_assum mp_tac >> simp[satisfies_def, valuation_def] >> 263 rpt strip_tac >> qmatch_abbrev_tac ���holds M' v p��� >> 264 ������v. holds M v p ��� holds M' v p��� suffices_by metis_tac[] >> 265 irule holds_functions >> simp[Abbr���M'���] >> simp[functions_def, PULL_EXISTS] >> 266 rw[] >> metis_tac[] 267QED 268 269(* ------------------------------------------------------------------------- *) 270(* Generalize to any formulas, via Skolemization. *) 271(* ------------------------------------------------------------------------- *) 272 273Theorem COMPACT_LS: 274 (���t. FINITE t ��� t ��� s ��� 275 ���M. interpretation (language s) M ��� M.Dom ��� ��� ��� M satisfies t) 276 ��� 277 ���C:term model. C.Dom ��� ��� ��� interpretation (language s) C ��� C satisfies s 278Proof 279 strip_tac >> 280 ������u. FINITE u ��� u ��� {SKOLEM p | p ��� s} ��� 281 ���M. interpretation (language {SKOLEM p | p ��� s }) M ��� 282 M.Dom ��� ��� ��� M satisfies u��� 283 by (rpt strip_tac >> 284 ������t. u = {SKOLEM p | p ��� t} ��� FINITE t ��� t ��� s��� 285 by metis_tac[finite_subset_SKOLEM] >> rw[] >> 286 first_x_assum (drule_all_then (qx_choose_then ���M��� strip_assume_tac))>> 287 Q.SUBGOAL_THEN ������M. M.Dom ��� ��� ��� interpretation (language t) M ��� 288 M satisfies t��� 289 (qx_choose_then ���M0��� strip_assume_tac o 290 ONCE_REWRITE_RULE[SKOLEM_SATISFIABLE]) 291 >- (qexists_tac ���M��� >> simp[] >> 292 irule interpretation_restrictlanguage >> metis_tac[]) >> 293 metis_tac[interpretation_extendlanguage]) >> 294 ������q. q ��� {SKOLEM p | p ��� s} ��� qfree q��� by simp[PULL_EXISTS] >> 295 drule_all_then (qx_choose_then ���CM��� strip_assume_tac) COMPACT_CANON_QFREE >> 296 simp[Once SKOLEM_SATISFIABLE] >> qexists_tac ���CM��� >> simp[] >> 297 fs[canonical_def] >> simp[EXTENSION] >> simp[IN_DEF] >> 298 metis_tac[terms_rules] 299QED 300 301(* ------------------------------------------------------------------------- *) 302(* Split away the compactness argument. *) 303(* ------------------------------------------------------------------------- *) 304 305Theorem CANON: 306 ���M:�� model s. 307 interpretation (language s) M ��� 308 M.Dom ��� ��� ��� (���p. p IN s ��� qfree p) /\ M satisfies s 309 ��� 310 ���C:term model. 311 C.Dom ��� ��� ��� interpretation (language s) C ��� C satisfies s 312Proof 313 rpt strip_tac >> irule COMPACT_LS THEN 314 metis_tac[satisfies_def, SUBSET_DEF] 315QED 316 317(* ------------------------------------------------------------------------- *) 318(* Conventional form of the LS theorem. *) 319(* ------------------------------------------------------------------------- *) 320 321Definition LOWMOD_def: 322 LOWMOD M = <| Dom := { num_of_term t | t ��� M.Dom } ; 323 Fun := ��g zs. num_of_term (M.Fun g (MAP term_of_num zs)) ; 324 Pred := ��p zs. M.Pred p (MAP term_of_num zs) |> 325End 326 327Theorem DOM_LOWMOD_EMPTY[simp]: 328 (LOWMOD M).Dom = ��� ��� M.Dom = ��� 329Proof 330 simp[LOWMOD_def, EXTENSION] 331QED 332 333Theorem LOWMOD_termval: 334 valuation (LOWMOD M) v ��� 335 ���t. termval (LOWMOD M) v t = num_of_term (termval M (term_of_num o v) t) 336Proof 337 simp[SimpL ���$==>���, valuation_def, LOWMOD_def] >> strip_tac >> 338 Induct >> simp[Cong MAP_CONG'] >- metis_tac[TERM_OF_NUM] >> 339 simp[LOWMOD_def, MAP_MAP_o, combinTheory.o_ABS_R] 340QED 341 342Theorem term_of_num_composition: 343 term_of_num o v��� n ��� num_of_term t ��� = (term_of_num o v)��� n ��� t ��� 344Proof 345 simp[FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM] >> rw[] 346QED 347 348 349Theorem holds_LOWMOD[simp]: 350 ���p v. valuation (LOWMOD M) v ��� 351 (holds (LOWMOD M) v p ��� holds M (term_of_num o v) p) 352Proof 353 Induct >> simp[Cong MAP_CONG', LOWMOD_termval] 354 >- simp[LOWMOD_def, MAP_MAP_o, combinTheory.o_ABS_R] >> 355 rw[] >> simp[LOWMOD_def, PULL_EXISTS, term_of_num_composition] 356QED 357 358Theorem interpretation_LOWMOD[simp]: 359 ���L M. interpretation L (LOWMOD M) ��� interpretation L M 360Proof 361 simp[interpretation_def, pairTheory.FORALL_PROD, LOWMOD_def] >> 362 rw[EQ_IMP_THM] 363 >- (rename [���M.Fun f zs ��� M.Dom���] >> 364 first_x_assum (qspecl_then [���f���, ���MAP num_of_term zs���] mp_tac) >> 365 simp[MEM_MAP, PULL_EXISTS, MAP_MAP_o, combinTheory.o_DEF]) >> 366 first_x_assum irule >> simp[MEM_MAP, PULL_EXISTS] >> rpt strip_tac >> 367 first_x_assum drule >> simp[PULL_EXISTS] 368QED 369 370Theorem LS: 371 ���M : �� model s. 372 interpretation (language s) M ��� M.Dom ��� ��� ��� (���p. p ��� s ��� qfree p) ��� 373 M satisfies s 374 ��� 375 ���N: num model. 376 interpretation (language s) N ��� N.Dom ��� ��� ��� N satisfies s 377Proof 378 rw[] >> drule_all_then strip_assume_tac CANON >> 379 qexists_tac ���LOWMOD C��� >> simp[] >> 380 fs[satisfies_def] >> rw[] >> first_x_assum irule >> 381 fs[valuation_def, LOWMOD_def] >> metis_tac[TERM_OF_NUM] 382QED 383 384Theorem COMPACT_LS_ALPHA: 385 INFINITE ����(:��) ��� 386 (���t. FINITE t ��� t ��� s ��� 387 ���M:�� model. 388 interpretation (language s) M ��� M.Dom ��� ��� ��� M satisfies t) ��� 389 ���M:�� model. 390 interpretation (language s) M ��� M.Dom ��� ��� ��� M satisfies s 391Proof 392 rw[] >> drule_then (qx_choose_then ���Cm��� strip_assume_tac) COMPACT_LS >> 393 ������f. INJ f ����(:term) ����(:��)��� 394 by (fs[infinite_num_inj] >> qexists_tac ���f o num_of_term��� >> 395 fs[INJ_IFF]) >> 396 metis_tac[copy_models] 397QED 398 399Theorem COMPACTNESS_satisfiable: 400 INFINITE ����(:��) ��� ffinsat (:��) s ��� satisfiable (:��) s 401Proof 402 rw[ffinsat_def, satisfiable_def] >> 403 ������t. FINITE t ��� t ��� s ��� 404 ���M. M.Dom ��� ��� ��� interpretation (language s) M ��� M satisfies t��� 405 by (rw[] >> first_x_assum (drule_all_then strip_assume_tac) >> 406 metis_tac[interpretation_extendlanguage]) >> 407 metis_tac[COMPACT_LS_ALPHA] 408QED 409 410Definition tm_constify_def[simp]: 411 (tm_constify kvs (V x) = if x ��� kvs then V x else Fn (1 ��� x) []) ��� 412 (tm_constify kvs (Fn f zs) = Fn (0 ��� f) (MAP (tm_constify kvs) zs)) 413Termination 414 WF_REL_TAC ���measure (term_size o SND)��� >> simp[] 415End 416 417Definition varify_map_def: 418 varify_map kvs m k = if k ��� kvs then V k else m k 419End 420 421Theorem tm_constify_varify: 422 tm_constify keeps t = 423 termsubst (varify_map keeps (��n. Fn (1 ��� n) [])) (bumpterm t) 424Proof 425 Induct_on ���t��� >> simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] >> 426 simp[varify_map_def] 427QED 428 429Definition fm_constify_def[simp]: 430 fm_constify kvs False = False ��� 431 fm_constify kvs (Pred n zs) = Pred n (MAP (tm_constify kvs) zs) ��� 432 fm_constify kvs (IMP p1 p2) = IMP (fm_constify kvs p1) (fm_constify kvs p2) ��� 433 fm_constify kvs (FALL x p) = FALL x (fm_constify (x INSERT kvs) p) 434End 435 436Theorem FVT_tm_constify[simp]: 437 ���t. FVT (tm_constify kvs t) = kvs ��� FVT t 438Proof 439 Induct >> simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] 440 >- (rw[EXTENSION] >> csimp[]) >> 441 simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[] 442QED 443 444Theorem FV_fm_constify[simp]: 445 ���p kvs. FV(fm_constify kvs p) = kvs ��� FV p 446Proof 447 Induct >> simp[fm_constify_def, formsubst_FV, UNION_OVER_INTER] 448 >- (simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[]) >> 449 simp[Once EXTENSION] >> csimp[] >> metis_tac[] 450QED 451 452Definition constifymod_def: 453 constifymod v M = <| Dom := M.Dom ; 454 Fun := ��g zs. if nfst g = 1 ��� zs = [] then 455 v (nsnd g) 456 else M.Fun (nsnd g) zs ; 457 Pred := M.Pred |> 458End 459 460Theorem constifymod_rwts[simp]: 461 (constifymod v M).Dom = M.Dom ��� (constifymod v M).Pred = M.Pred 462Proof 463 simp[constifymod_def] 464QED 465 466Theorem termval_constify[simp]: 467 termval (constifymod v M) w (tm_constify kvs t) = 468 termval M (��vnm. if vnm ��� kvs then w vnm else v vnm) t 469Proof 470 Induct_on ���t��� >> simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] >> 471 simp[constifymod_def] >> rw[] 472QED 473 474Theorem holds_constify: 475 ����� kvs v w M. 476 holds (constifymod v M) w (fm_constify kvs ��) ��� 477 holds M (��vnm. if vnm ��� kvs then w vnm else v vnm) �� 478Proof 479 Induct_on �������� >> simp[MAP_MAP_o, combinTheory.o_DEF] 480 >- asm_simp_tac (srw_ss() ++ boolSimps.ETA_ss) [] >> 481 rpt gen_tac >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE ABS_TAC) >> 482 simp[FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM] >> rw[] >> fs[] 483QED 484 485val _ = overload_on ("FMC", ���fm_constify ������) 486Theorem holds_constify_thm[simp]: 487 holds (constifymod v M) w (fm_constify ��� ��) ��� holds M v �� 488Proof 489 simp_tac (srw_ss() ++ boolSimps.ETA_ss) [holds_constify] 490QED 491 492Theorem FMC_Not: 493 FMC (Not ��) = Not (FMC ��) 494Proof 495 simp[Not_def] 496QED 497 498Theorem language_NOT_INSERT: 499 language (Not �� INSERT s) = language (�� INSERT s) 500Proof 501 rw[language_def, functions_def, predicates_def] >> 502 simp[Once EXTENSION, PULL_EXISTS] >> dsimp[Not_def] 503QED 504 505Theorem term_functions_tm_constify: 506 term_functions (tm_constify kvs t) = 507 { (0 ��� n, l) | (n,l) ��� term_functions t } ��� 508 { (1 ��� n, 0) | n ��� FVT t ��� n ��� kvs } 509Proof 510 Induct_on ���t��� >> simp[] 511 >- (rw[] >> csimp[] >> simp[EXTENSION]) >> 512 simp[MEM_MAP, PULL_EXISTS, Cong MAP_CONG', MAP_MAP_o] >> 513 dsimp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[] 514QED 515 516Theorem form_functions_fm_constify: 517 ���p kvs. form_functions (fm_constify kvs p) = 518 { (0 ��� n, l) | (n,l) ��� form_functions p } ��� 519 { (1 ��� n, 0) | n ��� FV p ��� n ��� kvs } 520Proof 521 Induct_on ���p��� >> 522 simp[MAP_MAP_o, MEM_MAP, combinTheory.o_DEF, PULL_EXISTS, 523 term_functions_tm_constify] 524 >- (dsimp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[]) 525 >- (simp[Once EXTENSION] >> metis_tac[]) >> 526 simp[Once EXTENSION] >> metis_tac[] 527QED 528 529Theorem form_predicates_fm_constify[simp]: 530 ���p kvs. form_predicates (fm_constify kvs p) = form_predicates p 531Proof 532 Induct >> simp[] 533QED 534 535Theorem functions_fmc: 536 functions {FMC p | p ��� s} = 537 { (0 ��� n,l) | (n,l) ��� functions s } ��� 538 { (1 ��� n,0) | n ��� BIGUNION (IMAGE FV s) } 539Proof 540 dsimp[functions_def, Once EXTENSION, PULL_EXISTS, 541 form_functions_fm_constify] >> metis_tac[] 542QED 543 544Theorem predicates_fmc[simp]: 545 predicates {FMC p | p ��� s } = predicates s 546Proof 547 simp[predicates_def, Once EXTENSION, PULL_EXISTS] 548QED 549 550Theorem valuation_constifymod[simp]: 551 valuation (constifymod v M) w ��� valuation M w 552Proof 553 simp[valuation_def] 554QED 555 556Theorem constifymod_interpretation: 557 valuation M v ��� 558 (interpretation (language {FMC p | p ��� s}) (constifymod v M) ��� 559 interpretation (language s) M) 560Proof 561 dsimp[interpretation_def, language_def, functions_fmc, valuation_def] >> 562 simp[constifymod_def] >> metis_tac[] 563QED 564 565Definition uncm_mod_def: 566 uncm_mod M = <| Dom := M.Dom ; 567 Fun := ��g zs. M.Fun (0 ��� g) zs ; 568 Pred := M.Pred |> 569End 570 571Theorem uncm_mod_rwts[simp]: 572 (uncm_mod M).Dom = M.Dom ��� 573 (uncm_mod M).Fun n l = M.Fun (0 ��� n) l ��� 574 (uncm_mod M).Pred = M.Pred 575Proof 576 simp[uncm_mod_def] 577QED 578 579Definition uncm_map_def: 580 uncm_map M fvs vnm = if vnm ��� fvs then M.Fun (1 ��� vnm) [] 581 else @a. a ��� M.Dom 582End 583 584Theorem termval_uncm: 585 ���t. (FVT t DIFF kvs) ��� fs ��� 586 termval M v (tm_constify kvs t) = 587 termval (uncm_mod M) 588 (��vnm. if vnm ��� kvs then v vnm else uncm_map M fs vnm) 589 t 590Proof 591 Induct >> simp[] >- rw[uncm_map_def] >> 592 strip_tac >> simp[MAP_MAP_o, combinTheory.o_ABS_R] >> 593 ������t. MEM t ts ��� FVT t DIFF kvs ��� fs��� 594 by (fs[SUBSET_DEF, MEM_MAP, PULL_EXISTS] >> metis_tac[]) >> 595 simp[Cong MAP_CONG'] 596QED 597 598Theorem UNION_DIFF_lemma: 599 (s ��� t) DIFF r = (s DIFF r) ��� (t DIFF r) 600Proof 601 simp[EXTENSION] >> metis_tac[] 602QED 603 604Theorem holds_uncm: 605 ����� v kvs fs. 606 FV �� DIFF kvs ��� fs ��� 607 (holds (uncm_mod M) 608 (��vnm. if vnm ��� kvs then v vnm else uncm_map M fs vnm) 609 �� ��� holds M v (fm_constify kvs ��)) 610Proof 611 Induct_on �������� >> simp[MAP_MAP_o, combinTheory.o_DEF, UNION_DIFF_lemma] 612 >- (rpt strip_tac >> rename [���M.Pred pnm (MAP _ zs)���] >> 613 ������t. MEM t zs ��� FVT t DIFF kvs ��� fs��� 614 by (fs[SUBSET_DEF, MEM_MAP, PULL_EXISTS] >> metis_tac[]) >> 615 asm_simp_tac (srw_ss() ++ boolSimps.ETA_ss) 616 [GSYM termval_uncm, Cong MAP_CONG']) >> 617 rpt strip_tac >> 618 ���FV �� DIFF (n INSERT kvs) ��� fs��� by fs[SUBSET_DEF] >> 619 first_x_assum (drule_then (assume_tac o GSYM)) >> simp[] >> 620 rpt (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE ABS_TAC) >> 621 simp[FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM] >> rw[] >> fs[] 622QED 623 624Theorem interpretation_uncm: 625 interpretation (language {FMC p | p ��� s}) M ��� 626 interpretation (language s) (uncm_mod M) 627Proof 628 simp[interpretation_def, language_def, functions_fmc, PULL_EXISTS] 629QED 630 631Theorem interpretation_uncm_valuation: 632 interpretation (language {FMC p | p ��� s}) M ��� M.Dom ��� ��� ��� 633 valuation (uncm_mod M) (uncm_map M (BIGUNION (IMAGE FV s))) 634Proof 635 dsimp[interpretation_def, language_def, functions_fmc, PULL_EXISTS, 636 valuation_def, uncm_map_def] >> rw[] >> fs[EXTENSION] >> 637 SELECT_ELIM_TAC >> simp[] >> metis_tac[] 638QED 639 640Theorem entails_constify: 641 entails (:��) {FMC p | p ��� H} (FMC ��) ��� entails (:��) H �� 642Proof 643 simp[entails_def, hold_def] >> 644 qmatch_abbrev_tac ���P = Q��� >> �����P ��� ��Q��� suffices_by simp[] >> 645 simp_tac pure_ss [NOT_FORALL_THM, Abbr���P���, Abbr���Q���, 646 DECIDE �����(p ��� q) ��� p ��� ��q���, PULL_EXISTS, GSYM HOLDS, 647 GSYM FMC_Not] >> 648 ONCE_REWRITE_TAC[GSYM language_NOT_INSERT] >> 649 ONCE_REWRITE_TAC[GSYM FMC_Not] >> 650 qspec_tac(���Not �����, ��������) >> qx_gen_tac �������� >> reverse eq_tac >> rw[] 651 >- (map_every qexists_tac [���constifymod v M���, ���v���] >> simp[] >> 652 qmatch_abbrev_tac ���interpretation (language FML) _��� >> 653 ���FML = { FMC p | p ��� �� INSERT H }��� by dsimp[EXTENSION, Abbr���FML���] >> 654 pop_assum SUBST1_TAC >> simp[constifymod_interpretation]) >> 655 qabbrev_tac ���A = �� INSERT H��� >> 656 qabbrev_tac ���fvs = BIGUNION (IMAGE FV A)��� >> 657 ���FV �� DIFF ��� ��� fvs��� by simp[Abbr���A���, Abbr���fvs���] >> 658 ������p. p ��� H ��� FV p DIFF ��� ��� fvs��� 659 by (fs[Abbr���A���, Abbr���fvs���, SUBSET_DEF, PULL_EXISTS] >> metis_tac[]) >> 660 FREEZE_THEN (fn th => fs[th]) 661 (holds_uncm |> SPEC_ALL |> Q.INST [���fs��� |-> ���fvs���, ���kvs��� |-> ���������] 662 |> SIMP_RULE (srw_ss()) [] |> GSYM |> Q.GENL [��������]) >> 663 qmatch_asmsub_abbrev_tac ���interpretation (language FML) _��� >> 664 ���FML = {FMC p | p ��� A}��� 665 by (simp[Abbr���FML���, Abbr���A���, EXTENSION] >> metis_tac[]) >> 666 map_every qexists_tac [���uncm_mod M���, ���uncm_map M fvs���] >> simp[] >> 667 full_simp_tac(srw_ss() ++ boolSimps.ETA_ss)[interpretation_uncm] >> 668 Q.UNABBREV_TAC ���fvs��� >> simp[interpretation_uncm_valuation] 669QED 670 671(* but not the reverse: there might be one model that makes all the new 672 constants satisfy the constraints, but then when those constants turn 673 back into variables, it's by no means guaranteed that every valuation 674 will satisfy the constraints *) 675Theorem satisfiable_constify: 676 satisfiable (:��) s ��� satisfiable (:��) { FMC p | p ��� s } 677Proof 678 simp[satisfiable_def, satisfies_def, PULL_EXISTS] >> rpt strip_tac >> 679 ������d. d ��� M.Dom��� by (fs[EXTENSION] >> metis_tac[]) >> 680 ���valuation M (K d : num -> ��)��� by simp[valuation_def] >> 681 qexists_tac ���constifymod (K d) M��� >> 682 simp[constifymod_interpretation] 683QED 684 685Theorem holds_FMC_ARB: 686 holds M v (FMC p) ��� holds M ARB (FMC p) 687Proof 688 simp[holds_valuation] 689QED 690 691 692Theorem not_entails: 693 ��entails (:��) H �� ��� satisfiable (:��) { FMC p | p ��� Not �� INSERT H } 694Proof 695 ONCE_REWRITE_TAC [GSYM entails_constify] >> 696 ������P s. {FMC p | P p} = IMAGE FMC {x | P x}��� 697 by (simp[EXTENSION] >> metis_tac[IN_DEF]) >> 698 dsimp[entails_def, hold_def, satisfiable_def, satisfies_def, PULL_EXISTS, 699 holds_FMC_ARB, FMC_Not, language_NOT_INSERT] >> 700 eq_tac >> rw[] >- (qexists_tac ���M��� >> simp[]) >> 701 qexists_tac ���M��� >> simp[] >> 702 ������v:num -> ��. valuation M v��� suffices_by metis_tac[] >> 703 fs[valuation_def, EXTENSION] >> rename [���d ��� M.Dom���] >> qexists_tac ���K d��� >> 704 simp[] 705QED 706 707Theorem entails_mono: 708 entails (:��) ����� �� ��� ����� ��� ����� ��� entails (:��) ����� �� 709Proof 710 rw[entails_def, hold_def] >> last_x_assum irule >> simp[] >> 711 ���interpretation (language (�� INSERT �����)) M��� suffices_by 712 metis_tac[SUBSET_DEF] >> 713 fs[language_def] >> irule interpretation_sublang >> 714 goal_assum (first_assum o mp_then Any mp_tac) >> 715 fs[SUBSET_DEF, functions_def] >> metis_tac[] 716QED 717 718Theorem satisfiable_antimono: 719 satisfiable (:��) s��� ��� s��� ��� s��� ��� satisfiable (:��) s��� 720Proof 721 simp[satisfiable_def, SUBSET_DEF, satisfies_def] >> strip_tac >> 722 ���interpretation (language s���) M��� suffices_by metis_tac[] >> 723 fs[language_def] >> irule interpretation_sublang >> 724 goal_assum (first_assum o mp_then Any mp_tac) >> 725 simp[functions_def, SUBSET_DEF, PULL_EXISTS] >> metis_tac[] 726QED 727 728Theorem tm_constify_11[simp]: 729 ���t1 t2. tm_constify ks t1 = tm_constify ks t2 ��� t1 = t2 730Proof 731 Induct >> Cases_on ���t2��� >> simp[] >> rw[] 732 >- metis_tac[] 733 >- metis_tac[] >> 734 rw[EQ_IMP_THM] >> fs[LIST_EQ_REWRITE, EL_MAP] >> 735 rfs[EL_MAP] >> metis_tac[MEM_EL] 736QED 737 738Theorem fm_constify_11[simp]: 739 ���f1 f2 ks. fm_constify ks f1 = fm_constify ks f2 ��� f1 = f2 740Proof 741 Induct >> Cases_on ���f2��� >> csimp[INJ_MAP_EQ_IFF, INJ_IFF] 742QED 743 744Theorem finite_entailment: 745 INFINITE ����(:��) ��� 746 (entails (:��) �� �� ��� ��������. FINITE ����� ��� ����� ��� �� ��� entails (:��) ����� ��) 747Proof 748 strip_tac >> reverse eq_tac >- metis_tac[entails_mono] >> CCONTR_TAC >> 749 fs[] >> 750 pop_assum (fn th => 751 �����������. FINITE ����� ��� ����� ��� �� ��� ��entails (:��) ����� ����� by metis_tac[th]) >> 752 fs[not_entails] >> 753 ���ffinsat (:��) { FMC p | p ��� (Not ��) INSERT �� }��� 754 suffices_by ( 755 strip_tac >> drule_all COMPACTNESS_satisfiable >> 756 metis_tac[not_entails] 757 ) >> 758 simp[ffinsat_def] >> rpt strip_tac >> 759 rename [���FINITE t���, ���t ��� _ ���] >> 760 ���satisfiable (:��) (FMC (Not ��) INSERT t)��� 761 suffices_by metis_tac[SUBSET_OF_INSERT, satisfiable_antimono] >> 762 ������t0. FMC (Not ��) INSERT t = {FMC p | p = Not �� ��� p ��� t0} ��� FINITE t0 ��� 763 t0 ��� ����� suffices_by metis_tac[] >> 764 qexists_tac ���PREIMAGE FMC t DELETE Not ����� >> 765 dsimp[EXTENSION] >> rw[] 766 >- (rw[EQ_IMP_THM] >> fs[SUBSET_DEF] >> first_x_assum drule >> 767 rw[] >> metis_tac[]) 768 >- (irule FINITE_PREIMAGE >> simp[]) >> 769 fs[SUBSET_DEF] >> rw[] >> first_x_assum drule >> simp[] 770QED 771 772val _ = export_theory() 773