1open HolKernel Parse boolLib bossLib; 2 3open pred_setTheory listTheory 4open boolSimps combinTheory 5open folLangTheory folModelsTheory 6 7val _ = new_theory "folPrenex"; 8 9Definition qfree_def: 10 (qfree False ��� T) ��� 11 (qfree (Pred _ _) ��� T) ��� 12 (qfree (IMP f1 f2) ��� qfree f1 ��� qfree f2) ��� 13 (qfree (FALL _ _) ��� F) 14End 15 16Theorem QFREE[simp]: 17 (qfree False ��� T) ��� 18 (qfree True ��� T) ��� 19 (qfree (Pred n ts) ��� T) ��� 20 (qfree (Not p) ��� qfree p) ��� 21 (qfree (Or p q) ��� qfree p ��� qfree q) ��� 22 (qfree (And p q) ��� qfree p ��� qfree q) ��� 23 (qfree (Iff p q) ��� qfree p ��� qfree q) ��� 24 (qfree (IMP p q) ��� qfree p ��� qfree q) ��� 25 (qfree (FALL n p) ��� F) ��� 26 (qfree (Exists n p) ��� F) 27Proof 28 simp[qfree_def, Exists_def, And_def, Or_def, True_def, Not_def, Iff_def] >> 29 metis_tac[] 30QED 31 32Theorem qfree_formsubst[simp]: 33 qfree (formsubst i p) ��� qfree p 34Proof 35 Induct_on ���p��� >> simp[] 36QED 37 38Theorem qfree_bv_empty: 39 qfree p ��� (BV p = ���) 40Proof 41 Induct_on ���p��� >> simp[] 42QED 43 44val (prenex_rules, prenex_ind, prenex_cases) = Hol_reln��� 45 (���p. qfree p ��� prenex p) ��� 46 (���x p. prenex p ��� prenex (FALL x p)) ��� 47 (���x p. prenex p ��� prenex (Exists x p)) 48���; 49 50val (universal_rules, universal_ind, universal_cases) = Hol_reln��� 51 (���p. qfree p ��� universal p) ��� 52 (���x p. universal p ��� universal (FALL x p)) 53���; 54 55Theorem prenex_INDUCT_NOT: 56 ���P. (���p. qfree p ��� P p) ��� 57 (���x p. P p ��� P (FALL x p)) ��� 58 (���p. P p ��� P (Not p)) 59 ��� 60 ���p. prenex p ��� P p 61Proof 62 ntac 2 strip_tac >> Induct_on ���prenex��� >> simp[Exists_def] 63QED 64 65Theorem universal_prenex: 66 ���p. universal p ��� prenex p 67Proof 68 Induct_on ���universal��� >> simp[prenex_rules] 69QED 70 71Theorem Exists_eqns[simp]: 72 Exists x p ��� Or q r ��� 73 Exists x p ��� Iff q r ��� 74 Exists x p ��� And q r ��� 75 Exists x p ��� FALL y q ��� 76 Exists x p ��� Pred n ts ��� 77 ((Exists x p = IMP q r) ��� (q = FALL x (IMP p False)) ��� (r = False)) ��� 78 ((Exists x p = Exists y q) ��� (x = y) ��� (p = q)) 79Proof 80 simp[And_def, Or_def, Iff_def, Exists_def, Not_def] >> metis_tac[] 81QED 82 83Theorem PRENEX[simp]: 84 (prenex False ��� T) ��� 85 (prenex True ��� T) ��� 86 (prenex (Pred n ts) ��� T) ��� 87 (prenex (Not p) ��� qfree p ��� ���x q. (Not p = Exists x q) ��� prenex q) ��� 88 (prenex (Or p q) ��� qfree p ��� qfree q) ��� 89 (prenex (And p q) ��� qfree p ��� qfree q) ��� 90 (prenex (IMP p q) ��� qfree p ��� qfree q ��� 91 ���x r. (IMP p q = Exists x r) ��� prenex r) ��� 92 (prenex (Iff p q) ��� qfree p ��� qfree q) ��� 93 (prenex (FALL x p) ��� prenex p) ��� 94 (prenex (Exists x p) ��� prenex p) 95Proof 96 rpt conj_tac >> 97 simp[SimpLHS, Once prenex_cases] >> 98 simp[And_def, Or_def, Iff_def, Not_def] 99QED 100 101Theorem formsubst_EQ[simp]: 102 (���i p. (formsubst i p = False) ��� (p = False)) ��� 103 (���i p. (False = formsubst i p) ��� (p = False)) ��� 104 (���i p n ts. (formsubst i p = Pred n ts) ��� ���ts0. (p = Pred n ts0) ��� 105 (ts = MAP (termsubst i) ts0)) ��� 106 (���i p q r. (formsubst i p = IMP q r) ��� 107 ���q0 r0. (p = IMP q0 r0) ��� (q = formsubst i q0) ��� 108 (r = formsubst i r0)) ��� 109 (���i p q. (formsubst i p = Not q) ��� ���q0. (p = Not q0) ��� (q = formsubst i q0)) 110Proof 111 csimp[Not_def] >> rw[] >> Cases_on ���p��� >> simp[] >> metis_tac[] 112QED 113 114Theorem formsubst_Not[simp]: 115 formsubst i (Not p) = Not (formsubst i p) 116Proof 117 rw[Not_def] 118QED 119 120Theorem Not_11[simp]: 121 (Not p = Not q) ��� (p = q) 122Proof 123 rw[Not_def] 124QED 125 126Theorem formsubst_EQ_FALL: 127 (���x q. formsubst i p = FALL x q) ��� (���x q. p = FALL x q) 128Proof 129 Cases_on ���p��� >> simp[] 130QED 131 132Theorem formsubst_EQ_Exists: 133 (���x q. formsubst i p = Exists x q) ��� (���x q. p = Exists x q) 134Proof 135 Cases_on ���p��� >> simp[] >> 136 rename [���subf2 = False���, ���formsubst i subf1 = FALL _ _���] >> 137 Cases_on ���subf2 = False��� >> simp[] >> 138 Cases_on ���subf1��� >> simp[] 139QED 140 141Theorem prenex_formsubst[simp]: 142 prenex (formsubst i p) ��� prenex p 143Proof 144 ���(���p. prenex p ��� ���i. prenex (formsubst i p)) ��� 145 (���p. prenex p ��� ���i q. (p = formsubst i q) ��� prenex q)��� 146 suffices_by metis_tac[] >> 147 conj_tac >> Induct_on ���prenex��� >> simp[] >> rw[] 148 >- metis_tac[qfree_formsubst, prenex_rules] 149 >- simp[Exists_def] 150 >- metis_tac[qfree_formsubst, prenex_rules] 151 >- (rename [���FALL n p = formsubst i q���] >> 152 ������m r. q = FALL m r��� by metis_tac[formsubst_EQ_FALL] >> rw[] >> fs[] >> 153 metis_tac[]) 154 >- (rename [���Exists n p = formsubst i q���] >> 155 ������m r. q = Exists m r��� by metis_tac[formsubst_EQ_Exists] >> rw[] >> 156 fs[Exists_def] >> metis_tac[]) 157QED 158 159Definition size_def: 160 (size False = 1) ��� 161 (size (Pred _ _) = 1) ��� 162 (size (IMP q r) = 1 + size q + size r) ��� 163 (size (FALL _ q) = 1 + size q) 164End 165 166Theorem SIZE[simp]: 167 (size False = 1) ��� 168 (size True = 3) ��� 169 (size (Pred n ts) = 1) ��� 170 (size (Not p) = 2 + size p) ��� 171 (size (Or p q) = size p + 2 * size q + 2) ��� 172 (size (And p q) = size p + 2 * size q + 10) ��� 173 (size (Iff p q) = 3 * size p + 3 * size q + 13) ��� 174 (size (IMP p q) = size p + size q + 1) ��� 175 (size (FALL x p) = 1 + size p) ��� 176 (size (Exists x p) = 5 + size p) 177Proof 178 simp[And_def, Or_def, Iff_def, size_def, Exists_def, Not_def, True_def] 179QED 180 181Theorem size_formsubst[simp]: 182 ���i. size (formsubst i p) = size p 183Proof 184 Induct_on ���p��� >> simp[] 185QED 186 187Definition PPAT_def: 188 PPAT A B C p = 189 case some (x,q). p = Exists x q of 190 SOME (x,q) => B x q 191 | NONE => 192 case p of 193 FALL x q => A x q 194 | _ => C p 195End 196 197Theorem PPAT[simp]: 198 (PPAT A B C (FALL x p) = A x p) ��� 199 (PPAT A B C (Exists x p) = B x p) ��� 200 ((!x q. p ��� FALL x q) ��� (���x q. p ��� Exists x q) ��� (PPAT A B C p = C p)) 201Proof 202 simp[PPAT_def, pairTheory.ELIM_UNCURRY]>> 203 ������a b. (��y. (a:num = FST y) ��� (b:form = SND y)) = (��p. p = (a,b))��� 204 by simp[FUN_EQ_THM, pairTheory.FORALL_PROD, EQ_SYM_EQ] >> 205 simp[] >> 206 Cases_on ���p��� >> simp[Exists_def] 207QED 208 209Theorem PPAT_CONG[defncong]: 210 ���A1 A2 B1 B2 C1 C2 q q'. 211 (���x p. size p < size q ��� (A1 x p = A2 x p)) ��� 212 (���x p. size p < size q ��� (B1 x p = B2 x p)) ��� (���p. C1 p = C2 p) ��� 213 (q = q') ��� 214 (PPAT A1 B1 C1 q = PPAT A2 B2 C2 q') 215Proof 216 rw[] >> 217 Cases_on ������n p0. q = Exists n p0��� >> fs[] >> 218 Cases_on ���q��� >> simp[] 219QED 220 221Definition prenexR_def: 222 prenexR p q = 223 PPAT 224 (��x q0. let y = VARIANT (FV p ��� FV(FALL x q0)) 225 in 226 FALL y (prenexR p (formsubst V���x ��� V y��� q0))) 227 (��x q0. let y = VARIANT (FV p ��� FV(Exists x q0)) 228 in 229 Exists y (prenexR p (formsubst V���x ��� V y��� q0))) 230 (��q. IMP p q) 231 q 232Termination 233 WF_REL_TAC ���measure (size o SND)��� >> simp[] 234End 235 236Theorem prenexR_thm[simp]: 237 (prenexR p (FALL x q) = let y = VARIANT (FV p ��� FV (FALL x q)) 238 in 239 FALL y (prenexR p (formsubst V���x ��� V y��� q))) ��� 240 (prenexR p (Exists x q) = let y = VARIANT (FV p ��� FV(Exists x q)) 241 in 242 Exists y (prenexR p (formsubst V���x ��� V y��� q))) ��� 243 (qfree q ��� (prenexR p q = IMP p q)) 244Proof 245 rpt conj_tac >> simp[SimpLHS, Once prenexR_def] >> simp[] >> strip_tac >> 246 ���(���x r. q ��� FALL x r) ��� (���x r. q ��� Exists x r)��� 247 by (rpt strip_tac >> fs[]) >> 248 simp[] 249QED 250 251Definition prenexL_def: 252 prenexL p q = 253 PPAT (��x p0. let y = VARIANT (FV (FALL x p0) ��� FV q) 254 in 255 Exists y (prenexL (formsubst V���x ��� V y��� p0) q)) 256 (��x p0. let y = VARIANT (FV (Exists x p0) ��� FV q) 257 in 258 FALL y (prenexL (formsubst V���x ��� V y��� p0) q)) 259 (��p. prenexR p q) p 260Termination 261 WF_REL_TAC ���measure (size o FST)��� >> simp[] 262End 263 264Theorem prenexL_thm[simp]: 265 (prenexL (FALL x p) q = let y = VARIANT (FV (FALL x p) ��� FV q) 266 in 267 Exists y (prenexL (formsubst V���x ��� V y��� p) q)) ��� 268 (prenexL (Exists x p) q = let y = VARIANT (FV (Exists x p) ��� FV q) 269 in 270 FALL y (prenexL (formsubst V���x ��� V y��� p) q)) ��� 271 (qfree p ��� (prenexL p q = prenexR p q)) 272Proof 273 rpt conj_tac >> simp[Once prenexL_def, SimpLHS] >> simp[] >> strip_tac >> 274 ���(���x r. p ��� FALL x r) ��� (���x r. p ��� Exists x r)��� 275 by (rpt strip_tac >> fs[]) >> 276 simp[] 277QED 278 279Definition Prenex_def[simp]: 280 (Prenex False = False) ��� 281 (Prenex (Pred n ts) = Pred n ts) ��� 282 (Prenex (IMP f1 f2) = prenexL (Prenex f1) (Prenex f2)) ��� 283 (Prenex (FALL x f) = FALL x (Prenex f)) 284End 285 286Theorem prenexR_language[simp]: 287 ���p. language {prenexR p q} = language {IMP p q} 288Proof 289 completeInduct_on ���size q��� >> fs[PULL_FORALL, language_SING] >> rpt gen_tac >> 290 disch_then SUBST_ALL_TAC >> 291 Cases_on ������x q0. q = Exists x q0��� >> fs[] 292 >- (simp[Exists_def, Not_def, form_functions_formsubst] >> 293 simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >> 294 Cases_on ������x q0. q = FALL x q0��� >> fs[] 295 >- simp_tac (srw_ss() ++ COND_elim_ss) 296 [form_functions_formsubst,combinTheory.APPLY_UPDATE_THM] >> 297 conj_tac >> simp[Once prenexR_def] 298QED 299 300Theorem prenexL_language[simp]: 301 ���q. language {prenexL p q} = language {IMP p q} 302Proof 303 completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rpt gen_tac >> 304 disch_then SUBST_ALL_TAC >> 305 Cases_on ������x p0. p = Exists x p0��� >> fs[] >> fs[] 306 >- (fs[Exists_def, Not_def, form_functions_formsubst, language_SING] >> 307 simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >> 308 Cases_on ������x p0. p = FALL x p0��� >> fs[] 309 >- full_simp_tac (srw_ss() ++ COND_elim_ss) 310 [language_SING,form_functions_formsubst,APPLY_UPDATE_THM,Exists_def, 311 Not_def] >> 312 simp[Once prenexL_def] 313QED 314 315Theorem prenex_lemma_forall: 316 P ��� (FV f1 = FV f2) ��� (language {f1} = language {f2}) ��� 317 (���M:�� model v. M.Dom ��� ��� ��� (holds M v f1 ��� holds M v f2)) ��� 318 P ��� (FV (FALL z f1) = FV (FALL z f2)) ��� 319 (language {FALL z f1} = language {FALL z f2}) ��� 320 ���M:�� model v. M.Dom ��� ��� ��� (holds M v (FALL z f1) ��� holds M v (FALL z f2)) 321Proof 322 rw[language_SING] 323QED 324 325Theorem prenex_lemma_exists: 326 P ��� (FV f1 = FV f2) ��� (language {f1} = language {f2}) ��� 327 (���M:�� model v. M.Dom ��� ��� ��� (holds M v f1 ��� holds M v f2)) ��� 328 P ��� (FV (Exists z f1) = FV (Exists z f2)) ��� 329 (language {Exists z f1} = language {Exists z f2}) ��� 330 ���M:�� model v. M.Dom ��� ��� ��� (holds M v (Exists z f1) ��� holds M v (Exists z f2)) 331Proof 332 rw[language_SING, Exists_def, Not_def] 333QED 334 335Theorem prenex_rename1[simp]: 336 ���f x y. prenex (formsubst V���x ��� V y��� f) ��� prenex f 337Proof 338 completeInduct_on ���size f��� >> fs[PULL_FORALL] 339QED 340 341Theorem tfresh_rename_inverts: 342 ���t x y. y ��� FVT t ��� (termsubst V���y ��� V x��� (termsubst V���x ��� V y��� t) = t) 343Proof 344 ho_match_mp_tac term_induct >> simp[] >> rw[MEM_MAP, MAP_MAP_o] 345 >- rw[combinTheory.APPLY_UPDATE_THM] >> 346 irule EQ_TRANS >> qexists_tac ���MAP I ts��� >> reverse conj_tac 347 >- simp[] >> 348 irule listTheory.MAP_CONG >> simp[] >> qx_gen_tac ���t0��� >> strip_tac >> 349 first_x_assum irule >> metis_tac[] 350QED 351 352Theorem holds_nonFV: 353 v ��� FV f ��� (holds M i��� v ��� t ��� f ��� holds M i f) 354Proof 355 strip_tac >> irule holds_valuation >> 356 simp[combinTheory.APPLY_UPDATE_THM] >> rw[] >> fs[] 357QED 358 359Theorem prenexR_FV[simp]: 360 FV (prenexR p q) = FV p ��� FV q 361Proof 362 completeInduct_on ���size q��� >> fs[PULL_FORALL] >> rw[] >> 363 Cases_on ������v q0. q = Exists v q0��� >> fs[] 364 >- (simp_tac (srw_ss() ++ COND_elim_ss) 365 [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >> 366 qmatch_goalsub_abbrev_tac ���VARIANT s��� >> 367 qabbrev_tac ���vv = VARIANT s��� >> 368 ���vv ��� s��� by simp[Abbr���vv���, Abbr���s���, VARIANT_FINITE] >> 369 Q.UNABBREV_TAC ���s��� >> fs[] >> gen_tac >> 370 eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >> 371 Cases_on ������v q0. q = FALL v q0��� >> fs[] 372 >- (simp_tac (srw_ss() ++ COND_elim_ss) 373 [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >> 374 qmatch_goalsub_abbrev_tac ���VARIANT s��� >> 375 qabbrev_tac ���vv = VARIANT s��� >> 376 ���vv ��� s��� by simp[Abbr���vv���, Abbr���s���, VARIANT_FINITE] >> 377 Q.UNABBREV_TAC ���s��� >> fs[] >> gen_tac >> 378 eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >> 379 simp[prenexR_def] 380QED 381 382Theorem prenexR_prenex: 383 qfree p ��� prenex q ��� prenex (prenexR p q) 384Proof 385 completeInduct_on ���size q��� >> fs[PULL_FORALL] >> gen_tac >> 386 disch_then SUBST_ALL_TAC >> 387 simp[Once prenex_cases, SimpLHS] >> dsimp[] 388QED 389 390Theorem prenexR_holds: 391 ���M v. M.Dom ��� ��� ��� (holds M v (prenexR p q) ��� holds M v (IMP p q)) 392Proof 393 completeInduct_on ���size q��� >> fs[PULL_FORALL] >> rw[] >> 394 Cases_on ������v q0. q = Exists v q0��� >> fs[] >> fs[] 395 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 396 ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >> 397 qabbrev_tac ���vv = VARIANT ss��� >> 398 rename [���holds M vln��� vv ��� _ ��� f1���, ���formsubst _ f2���] >> 399 ���vv ��� FV f1��� by fs[Abbr���ss���] >> 400 ������t. holds M vln���vv ��� t��� f1 ��� holds M vln f1��� 401 by (gen_tac >> irule holds_valuation >> 402 metis_tac[combinTheory.APPLY_UPDATE_THM]) >> 403 simp[] >> Cases_on ���holds M vln f1��� >> simp[] 404 >- (AP_TERM_TAC >> ABS_TAC >> 405 rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >> 406 simp[holds_formsubst] >> irule holds_valuation >> 407 rw[combinTheory.APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >> 408 metis_tac[MEMBER_NOT_EMPTY]) >> 409 Cases_on ������v q0. q = FALL v q0��� >> fs[] >> fs[] 410 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 411 ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >> 412 qabbrev_tac ���vv = VARIANT ss��� >> 413 rename [���holds M vln��� vv ��� _ ��� f1���, ���formsubst V���v��� ��� V vv��� f2���] >> 414 ���vv ��� FV f1��� by fs[Abbr���ss���] >> 415 ������d. holds M vln���vv ��� d��� f1 ��� holds M vln f1��� 416 by (gen_tac >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >> 417 metis_tac[]) >> 418 simp[] >> Cases_on ���holds M vln f1��� >> simp[holds_formsubst] >> 419 AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >> 420 simp[] >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >> 421 rw[APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >> 422 simp[Once prenexR_def] 423QED 424 425Theorem prenexL_FV[simp]: 426 FV (prenexL p q) = FV p ��� FV q 427Proof 428 completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >> 429 Cases_on ������v p1. p = Exists v p1��� >> fs[] 430 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 431 ���VARIANT ss ��� ss��� by fs[Abbr���ss���, VARIANT_FINITE] >> 432 simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >> 433 simp[EXTENSION] >> qx_gen_tac ���n��� >> eq_tac >> 434 asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[] 435 >- simp[Abbr���ss���] 436 >- simp[Abbr���ss���] 437 >- (dsimp[] >> fs[Abbr���ss���]) 438 >- metis_tac[]) >> 439 Cases_on ������v p1. p = FALL v p1��� >> fs[] 440 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 441 ���VARIANT ss ��� ss��� by fs[Abbr���ss���, VARIANT_FINITE] >> 442 simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >> 443 simp[EXTENSION] >> qx_gen_tac ���n��� >> eq_tac >> 444 asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[] 445 >- simp[Abbr���ss���] 446 >- simp[Abbr���ss���] 447 >- (dsimp[] >> fs[Abbr���ss���]) 448 >- metis_tac[]) >> 449 simp[prenexL_def] 450QED 451 452Theorem prenexL_prenex[simp]: 453 prenex p ��� prenex q ��� prenex (prenexL p q) 454Proof 455 completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >> 456 Cases_on ������v p0. p = Exists v p0��� >> fs[] >> 457 Cases_on ������v p0. p = FALL v p0��� >> fs[] >> fs[] >> 458 simp[prenexL_def] >> 459 ���qfree p��� suffices_by metis_tac[prenexR_prenex] >> 460 Q.UNDISCH_THEN ���prenex p��� mp_tac >> simp[Once prenex_cases] 461QED 462 463Theorem prenexL_holds[simp]: 464 ���M vln. M.Dom ��� ��� ��� (holds M vln (prenexL p q) ��� holds M vln (IMP p q)) 465Proof 466 completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >> 467 Cases_on ������v p0. p = Exists v p0��� >> fs[] 468 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 469 ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >> 470 ������d. holds M vln��� VARIANT ss ��� d��� q ��� holds M vln q��� 471 by (gen_tac >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >> 472 fs[Abbr���ss���]) >> simp[PULL_EXISTS] >> 473 AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >> 474 simp[] >> AP_THM_TAC >> AP_TERM_TAC >> 475 simp[holds_formsubst] >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >> 476 fs[Abbr���ss���] >> metis_tac[]) >> 477 Cases_on ������v p0. p = FALL v p0��� >> fs[] 478 >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >> 479 ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >> 480 simp[GSYM LEFT_EXISTS_IMP_THM] >> 481 ������d. holds M vln��� VARIANT ss ��� d ��� q ��� holds M vln q��� 482 by (gen_tac >> irule holds_nonFV >> fs[Abbr���ss���]) >> 483 simp[] >> Cases_on ���holds M vln q��� >> simp[] 484 >- metis_tac[MEMBER_NOT_EMPTY] >> 485 AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >> 486 simp[] >> simp[holds_formsubst] >> irule holds_valuation >> 487 rw[APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >> 488 simp[Once prenexL_def, prenexR_holds] 489QED 490 491Theorem prenex_Prenex[simp]: 492 prenex (Prenex f) 493Proof 494 Induct_on ���f��� >> simp[] 495QED 496 497Theorem FV_Prenex[simp]: 498 FV (Prenex f) = FV f 499Proof 500 Induct_on ���f��� >> simp[] 501QED 502 503Theorem holds_Prenex[simp]: 504 ���vln. M.Dom ��� ��� ��� (holds M vln (Prenex f) ��� holds M vln f) 505Proof 506 Induct_on ���f��� >> simp[prenexL_holds] 507QED 508 509Theorem language_Prenex[simp]: 510 language {Prenex f} = language {f} 511Proof 512 Induct_on ���f��� >> simp[] >> fs[language_SING] 513QED 514 515Theorem form_functions_prenexR[simp]: 516 ���f1 f2. form_functions (prenexR f1 f2) = form_functions f1 ��� form_functions f2 517Proof 518 ho_match_mp_tac prenexR_ind >> rpt strip_tac >> simp[Once prenexR_def] >> 519 Cases_on������x f2'. f2 = Exists x f2'��� >> 520 full_simp_tac (srw_ss() ++ COND_elim_ss) 521 [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] >> 522 Cases_on ������x f2'. f2 = FALL x f2'��� >> 523 full_simp_tac (srw_ss() ++ COND_elim_ss) 524 [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] 525QED 526 527Theorem form_functions_prenexL[simp]: 528 ���f1 f2. form_functions (prenexL f1 f2) = form_functions f1 ��� form_functions f2 529Proof 530 ho_match_mp_tac prenexL_ind >> rpt strip_tac >> 531 simp[Once prenexL_def] >> 532 Cases_on������x f1'. f1 = Exists x f1'��� >> 533 full_simp_tac (srw_ss() ++ COND_elim_ss) 534 [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] >> 535 Cases_on ������x f1'. f1 = FALL x f1'��� >> 536 full_simp_tac (srw_ss() ++ COND_elim_ss) 537 [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] 538QED 539 540Theorem form_functions_Prenex[simp]: 541 form_functions (Prenex f) = form_functions f 542Proof 543 Induct_on ���f��� >> simp[] 544QED 545 546Theorem form_predicates_prenexR[simp]: 547 ���f1 f2. 548 form_predicates (prenexR f1 f2) = form_predicates f1 ��� form_predicates f2 549Proof 550 ho_match_mp_tac prenexR_ind >> rpt strip_tac >> 551 simp[Once prenexR_def] >> 552 Cases_on������x f2'. f2 = Exists x f2'��� >> fs [] >> 553 Cases_on ������x f2'. f2 = FALL x f2'��� >> fs [] 554QED 555 556Theorem form_predicates_prenexL[simp]: 557 ���f1 f2. 558 form_predicates (prenexL f1 f2) = form_predicates f1 ��� form_predicates f2 559Proof 560 ho_match_mp_tac prenexL_ind >> rpt strip_tac >> 561 simp[Once prenexL_def] >> 562 Cases_on������x f1'. f1 = Exists x f1'��� >> fs [] >> 563 Cases_on ������x f1'. f1 = FALL x f1'��� >> fs [] 564QED 565 566Theorem form_predicates_Prenex[simp]: 567 form_predicates (Prenex p) = form_predicates p 568Proof 569 Induct_on ���p��� >> simp[] 570QED 571 572 573val _ = export_theory(); 574