1open HolKernel Parse boolLib bossLib; 2 3open boolSimps pred_setTheory listTheory nlistTheory 4open folPrenexTheory folModelsTheory folLangTheory 5open mp_then 6 7val _ = new_theory "folSkolem"; 8 9Theorem holds_exists_lemma: 10 ���p t x M v (preds : (num # num) set). 11 interpretation (term_functions t, preds) M ��� 12 valuation M v ��� 13 holds M v (formsubst V���x ��� t��� p) 14 ��� 15 holds M v (Exists x p) 16Proof 17 rw[holds_formsubst1] >> metis_tac[interpretation_termval] 18QED 19 20Definition Skolem1_def: 21 Skolem1 f x p = 22 formsubst V��� x ��� Fn f (MAP V (SET_TO_LIST (FV (Exists x p))))��� p 23End 24 25Theorem FV_Skolem1[simp]: 26 FV (Skolem1 f x p) = FV (Exists x p) 27Proof 28 simp[Skolem1_def, formsubst_FV, combinTheory.APPLY_UPDATE_THM, EXTENSION, 29 EQ_IMP_THM, FORALL_AND_THM, PULL_EXISTS] >> 30 simp_tac (srw_ss() ++ COND_elim_ss ++ DNF_ss) [EXISTS_OR_THM, MEM_MAP] 31QED 32 33Theorem size_Skolem1[simp]: 34 size (Skolem1 f x p) = size p 35Proof 36 simp[Skolem1_def] 37QED 38 39Theorem prenex_Skolem1[simp]: 40 prenex (Skolem1 f x p) ��� prenex p 41Proof 42 simp[Skolem1_def] 43QED 44 45Theorem form_predicates_Skolem1[simp]: 46 form_predicates (Skolem1 f x p) = form_predicates p 47Proof 48 simp[Skolem1_def] 49QED 50 51Theorem LIST_UNION_MAP_KEMPTY[simp]: 52 LIST_UNION (MAP (��a. ���) l) = ��� ��� 53 LIST_UNION (MAP (K ���) l) = ��� 54Proof 55 Induct_on ���l��� >> simp[] 56QED 57 58Theorem form_functions_Skolem1: 59 form_functions (Skolem1 f x p) ��� 60 (f, CARD (FV (Exists x p))) INSERT form_functions p ��� 61 form_functions p ��� form_functions (Skolem1 f x p) 62Proof 63 simp[Skolem1_def] >> Cases_on ���x ��� FV p��� 64 >- (simp[form_functions_formsubst1, MAP_MAP_o, combinTheory.o_ABS_L, 65 SET_TO_LIST_CARD] >> 66 simp[SUBSET_DEF]) >> 67 simp[SUBSET_DEF] 68QED 69 70Theorem Skolem1_ID[simp]: 71 x ��� FV p ��� Skolem1 f x p = p 72Proof 73 simp[Skolem1_def] 74QED 75 76Theorem holds_Skolem1_I: 77 (f,CARD (FV (Exists x p))) ��� form_functions (Exists x p) 78 ��� 79 ���M. interpretation (language {p}) M ��� M.Dom ��� ��� ��� 80 (���v. valuation M v ��� holds M v (Exists x p)) 81 ��� 82 ���M'. M'.Dom = M.Dom ��� M'.Pred = M.Pred ��� 83 (���g zs. g ��� f ��� LENGTH zs ��� CARD (FV (Exists x p)) ��� 84 M'.Fun g zs = M.Fun g zs) ��� 85 interpretation (language {Skolem1 f x p}) M' ��� 86 ���v. valuation M' v ��� holds M' v (Skolem1 f x p) 87Proof 88 reverse (Cases_on ���x ��� FV p���) 89 >- (simp[holds_nonFV] >> metis_tac[]) >> 90 qabbrev_tac ���FF = FV (Exists x p)��� >> simp[Skolem1_def] >> 91 qabbrev_tac ���ft = Fn f (MAP V (SET_TO_LIST FF))��� >> rw[] >> 92 qexists_tac ���<| 93 Dom := M.Dom ; Pred := M.Pred ; 94 Fun := M.Fun ��� f ��� 95 ��args. if LENGTH args = CARD FF then 96 @a. a ��� M.Dom ��� 97 holds M (FOLDR (��(k,v) f. f ��� k ��� v ���) 98 (��z. @c. c ��� M.Dom) 99 (ZIP(SET_TO_LIST FF, args))) 100 ��� x ��� a ��� 101 p 102 else M.Fun f args ��� 103 |>��� >> simp[] >> rw[] 104 >- simp[combinTheory.APPLY_UPDATE_THM] 105 >- rw[combinTheory.APPLY_UPDATE_THM] 106 >- (fs[interpretation_def, language_def] >> 107 rw[combinTheory.APPLY_UPDATE_THM] 108 >- (rename [���(f,LENGTH l) ��� form_functions p���] >> metis_tac[]) 109 >- (rename [���(f,LENGTH l) ��� term_functions ft���] >> 110 ���FINITE FF��� by simp[Abbr���FF���]>> 111 reverse (fs[Abbr���ft���, MAP_MAP_o, MEM_MAP, SET_TO_LIST_CARD]) 112 >- (rw[] >> fs[]) >> 113 SELECT_ELIM_TAC >> simp[] >> 114 first_x_assum irule >> simp[valuation_def] >> 115 ������(vars:num list) (vals:�� list) n. 116 (���v. MEM v vals ��� v ��� M.Dom) ��� LENGTH vars = LENGTH vals ��� 117 FOLDR (��(k,v) f. f ���k ��� v���) (��z. @c. c ��� M.Dom) 118 (ZIP (vars, vals)) n ��� M.Dom��� 119 suffices_by metis_tac[SET_TO_LIST_CARD] >> 120 Induct >> simp[] 121 >- (SELECT_ELIM_TAC >> fs[EXTENSION] >> metis_tac[]) >> 122 Cases_on ���vals��� >> 123 simp[DISJ_IMP_THM, FORALL_AND_THM, combinTheory.APPLY_UPDATE_THM] >> 124 rw[]) 125 >- (rename [���f ��� g���, ���(g,LENGTH l) ��� form_functions p���] >> metis_tac[]) >> 126 rename [���f ��� g���, ���(g,LENGTH l) ��� term_functions ft���] >> 127 fs[Abbr���ft���, MEM_MAP, SET_TO_LIST_CARD] >> rw[] >> fs[]) >> 128 qmatch_abbrev_tac ���holds <| Dom := M.Dom; Fun := CF; Pred := M.Pred |> _ _��� >> 129 simp[holds_formsubst1, Abbr���ft���, MAP_MAP_o, combinTheory.o_ABS_L] >> 130 irule (holds_functions 131 |> CONV_RULE (RAND_CONV (REWRITE_CONV [EQ_IMP_THM])) 132 |> UNDISCH |> Q.SPEC ���v��� |> CONJUNCT2 |> Q.GEN ���v��� |> DISCH_ALL) >> 133 qexists_tac ���M��� >> simp[] >> conj_tac 134 >- (rw[Abbr���CF���, combinTheory.APPLY_UPDATE_THM] >> metis_tac[]) >> 135 ���FINITE FF��� by simp[Abbr���FF���] >> 136 simp[Abbr���CF���, SET_TO_LIST_CARD, combinTheory.APPLY_UPDATE_THM] >> 137 SELECT_ELIM_TAC >> conj_tac 138 >- (first_x_assum irule >> fs[valuation_def] >> 139 ������l. (���n. v n ��� M.Dom) ��� 140 ���n. FOLDR (��(k,v) f. f ��� k ��� v ���) (��z. @c. c ��� M.Dom) 141 (ZIP (l,MAP (��a. v a) l)) n ��� M.Dom��� 142 suffices_by metis_tac[] >> Induct >> simp[] 143 >- (SELECT_ELIM_TAC >> fs[EXTENSION] >>metis_tac[]) >> 144 rfs[combinTheory.APPLY_UPDATE_THM] >> rw[]) >> 145 qx_gen_tac ���a��� >> 146 qmatch_abbrev_tac ���a ��� M.Dom ��� holds M vv��� x ��� a ��� p ��� holds M v��� x ��� a ��� p���>> 147 fs[valuation_def] >> strip_tac >> 148 ������var. var ��� FV p ��� vv��� x ��� a ��� var = v��� x ��� a ��� var��� 149 suffices_by metis_tac[holds_valuation] >> 150 rw[combinTheory.APPLY_UPDATE_THM] >> simp[Abbr���vv���] >> 151 ������vars (var:num). 152 MEM var vars ��� ALL_DISTINCT vars ��� 153 FOLDR (��(k,v) f. f ��� k ��� v ���) (��z. @c. c ��� M.Dom) 154 (ZIP (vars,MAP (��a. v a) vars)) var = v var��� 155 suffices_by (disch_then irule >> simp[] >> simp[Abbr���FF���]) >> 156 Induct >> simp[] >> rw[combinTheory.APPLY_UPDATE_THM] 157QED 158 159Theorem holds_Skolem1_E: 160 (f,CARD (FV (Exists x p))) ��� form_functions (Exists x p) ��� 161 ���N. interpretation (language {Skolem1 f x p}) N ��� N.Dom ��� ��� 162 ��� 163 ���v. valuation N v ��� holds N v (Skolem1 f x p) ��� holds N v (Exists x p) 164Proof 165 reverse (Cases_on ���x ��� FV p���) 166 >- (simp[holds_nonFV, EXTENSION] >> metis_tac[]) >> 167 qabbrev_tac ���FF = FV (Exists x p)��� >> simp[Skolem1_def] >> 168 qabbrev_tac ���ft = Fn f (MAP V (SET_TO_LIST FF))��� >> 169 ���FINITE FF��� by simp[Abbr���FF���] >> 170 simp[holds_formsubst1] >> rw[] >> 171 ���termval N v ft ��� N.Dom��� suffices_by metis_tac[] >> 172 simp[Abbr���ft���, MAP_MAP_o, combinTheory.o_ABS_L] >> 173 rfs[interpretation_def, language_def, form_functions_formsubst1, 174 MEM_MAP, MAP_MAP_o, PULL_EXISTS, DISJ_IMP_THM, FORALL_AND_THM, 175 RIGHT_AND_OVER_OR] >> 176 first_x_assum 177 (fn th => irule th >> 178 fs[MEM_MAP, PULL_EXISTS, SET_TO_LIST_CARD, valuation_def] >> 179 NO_TAC) 180QED 181 182(* ------------------------------------------------------------------------- *) 183(* Multiple Skolemization of a prenex formula. *) 184(* ------------------------------------------------------------------------- *) 185 186Definition Skolems_def: 187 Skolems J r k = 188 PPAT (��x q. FALL x (Skolems J q k)) 189 (��x q. Skolems J (Skolem1 (J *, k) x q) (k + 1)) 190 (��p. p) r 191Termination 192 WF_REL_TAC ���measure (��(a,b,c). size b)��� >> simp[] >> 193 simp[Skolem1_def] 194End 195 196Theorem prenex_Skolems_universal[simp]: 197 ���J p k. prenex p ��� universal (Skolems J p k) 198Proof 199 ho_match_mp_tac Skolems_ind >> rw[] >> 200 Cases_on ������x p0. p = Exists x p0��� >> fs[] 201 >- (simp[Once Skolems_def] >> first_x_assum irule >> fs[]) >> 202 Cases_on ������x p0. p = FALL x p0��� >> fs[] 203 >- (simp[Once Skolems_def] >> fs[universal_rules]) >> 204 simp[Once Skolems_def] >> 205 simp[Once universal_cases] >> metis_tac[prenex_cases] 206QED 207 208Theorem FV_Skolems[simp]: 209 ���J p k. FV (Skolems J p k) = FV p 210Proof 211 ho_match_mp_tac Skolems_ind >> rw[] >> 212 Cases_on ������x p0. p = Exists x p0��� >> fs[] >- simp[Once Skolems_def] >> 213 Cases_on ������x p0. p = FALL x p0��� >> fs[] >- simp[Once Skolems_def] >> 214 simp[Once Skolems_def] 215QED 216 217Theorem form_predicates_Skolems[simp]: 218 ���J p k. form_predicates (Skolems J p k) = form_predicates p 219Proof 220 ho_match_mp_tac Skolems_ind >> rw[] >> 221 Cases_on ������x p0. p = Exists x p0��� >> fs[] 222 >- (simp[Once Skolems_def] >> simp[Exists_def, Not_def]) >> 223 Cases_on ������x p0. p = FALL x p0��� >> fs[] >- simp[Once Skolems_def] >> 224 simp[Once Skolems_def] 225QED 226 227Theorem form_functions_Skolems_up: 228 ���J p k. 229 form_functions (Skolems J p k) ��� 230 {(J ��� l, m) | l, m | k ��� l} ��� form_functions p 231Proof 232 ho_match_mp_tac Skolems_ind >> rw[] >> 233 Cases_on ������x p0. p = Exists x p0��� >> fs[] 234 >- (simp[Once Skolems_def] >> fs[] >> 235 first_x_assum (qspecl_then [���p0���, ���x���] mp_tac) >> simp[] >> 236 simp[SUBSET_DEF] >> rw[] >> first_x_assum drule >> rw[] >> 237 mp_tac (form_functions_Skolem1 |> CONJUNCT1 |> GEN_ALL) >> 238 REWRITE_TAC[SUBSET_DEF] >> rw[] >> 239 pop_assum (drule_then strip_assume_tac) >> rw[]) >> 240 Cases_on ������x p0. p = FALL x p0��� >> fs[] >- simp[Once Skolems_def] >> 241 simp[Once Skolems_def] 242QED 243 244Theorem form_functions_Skolems_down: 245 ���J p k. 246 form_functions p ��� form_functions (Skolems J p k) 247Proof 248 ho_match_mp_tac Skolems_ind >> rw[] >> 249 Cases_on ������x p0. p = Exists x p0��� >> fs[] 250 >- (simp[Once Skolems_def] >> fs[] >> 251 first_x_assum (qspecl_then [���p0���, ���x���] mp_tac) >> simp[] >> 252 simp[SUBSET_DEF] >> rw[] >> first_x_assum irule >> rw[] >> 253 metis_tac[SUBSET_DEF, form_functions_Skolem1]) >> 254 Cases_on ������x p0. p = FALL x p0��� >> fs[] >- simp[Once Skolems_def] >> 255 simp[Once Skolems_def] 256QED 257 258Theorem holds_Skolems_I: 259 ���J p k M. 260 interpretation (language{p}) M ��� M.Dom ��� ��� ��� 261 (���v. valuation M v ��� holds M v p) ��� 262 (���l m. (J ��� l,m) ��� form_functions p ��� l < k) 263 ��� 264 ���M'. M'.Dom = M.Dom ��� M'.Pred = M.Pred ��� 265 (���g zs. M'.Fun g zs ��� M.Fun g zs ��� ���l. k ��� l ��� g = J ��� l) ��� 266 interpretation (language {Skolems J p k}) M' ��� 267 ���v. valuation M' v ��� holds M' v (Skolems J p k) 268Proof 269 ho_match_mp_tac Skolems_ind >> rw[] >> 270 Cases_on ������x p0. p = FALL x p0��� >> fs[] >> fs[] 271 >- (ONCE_REWRITE_TAC [Skolems_def] >> simp[] >> 272 first_x_assum 273 (first_assum o mp_then.mp_then (mp_then.Pos (el 2)) mp_tac) >> 274 impl_tac 275 >- (simp[] >> 276 reverse conj_tac 277 >- (first_x_assum ACCEPT_TAC (* freshness assumption *)) >> 278 qx_gen_tac ���valn��� >> strip_tac >> 279 first_x_assum (drule_then (qspec_then ���valn x��� mp_tac)) >> 280 simp[combinTheory.APPLY_UPDATE_ID] >> disch_then irule >> 281 fs[valuation_def]) >> 282 disch_then (qx_choose_then ���N��� strip_assume_tac) >> qexists_tac ���N��� >> 283 simp[] >> first_assum ACCEPT_TAC) >> 284 reverse (Cases_on ������x p0. p = Exists x p0���) >> fs[] 285 >- (ONCE_REWRITE_TAC [Skolems_def] >> simp[] >> metis_tac[]) >> 286 rw[] >> fs[] >> rw[] >> ONCE_REWRITE_TAC [Skolems_def] >> simp[] >> 287 (* apply Skolem1 result: holds_Skolem1_I *) 288 rename [���Skolem1 (J ��� k) xv �����] >> 289 first_assum 290 (mp_then.mp_then (mp_then.Pos (el 2)) mp_tac (GEN_ALL holds_Skolem1_I)) >> 291 simp[Excl "FV_extras"] >> 292 disch_then (first_assum o mp_then.mp_then (mp_then.Pos (el 2)) mp_tac) >> 293 disch_then (qspec_then ���J ��� k��� mp_tac) >> 294 qabbrev_tac ���FF = FV (Exists xv ��)��� >> ���FINITE FF��� by simp[Abbr���FF���] >> 295 disch_then (PROVEHYP_THEN (K (qx_choose_then ���M1��� strip_assume_tac))) 296 >- (strip_tac >> first_x_assum drule >> simp[]) >> 297 qpat_x_assum 298 ������p n. size p < size _ + _ ��� 299 ���M. interpretation (language {Skolem1 _ _ _ }) M ��� _ ��� _��� 300 (first_assum o mp_then.mp_then (mp_then.Pos (el 2)) mp_tac) >> 301 simp[] >> 302 qpat_x_assum ������p. size p < size _ + _ ��� _��� (K ALL_TAC) >> 303 impl_tac 304 >- (rw[] >> rename [���(J ��� n,m) ��� form_functions (Skolem1 (J ��� k) _ _)���] >> 305 mp_tac (form_functions_Skolem1 |> CONJUNCT1 |> GEN_ALL) >> 306 simp[SUBSET_DEF, Excl "FV_extras", Excl "form_functions_Skolem1"] >> 307 disch_then drule >> simp[] >> rw[] >> simp[] >> 308 metis_tac[DECIDE ���x < k ��� x < k + 1���]) >> 309 disch_then (qx_choose_then ���N��� strip_assume_tac) >> qexists_tac ���N��� >> 310 simp[] >> 311 rw[] >> rename [���N.Fun g args = M.Fun g args���] >> 312 Cases_on ���N.Fun g args = M1.Fun g args��� >> fs[] 313 >- metis_tac [DECIDE ���x ��� x���] >> 314 first_x_assum (pop_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac) >> 315 simp[PULL_EXISTS] 316QED 317 318Theorem interpretation_Skolem1_E: 319 ���N f x p. interpretation (language {Skolem1 f x p}) N ��� 320 interpretation (language {p}) N 321Proof 322 rpt gen_tac >> reverse (Cases_on ���x ��� FV p���) >> simp[Skolem1_ID] >> 323 simp[Skolem1_def, language_def, form_functions_formsubst1, 324 predicates_def, interpretation_def] 325QED 326 327Theorem interpretation_Skolems_E: 328 ���J p k N. interpretation (language {Skolems J p k}) N ��� 329 interpretation (language {p}) N 330Proof 331 ho_match_mp_tac Skolems_ind >> rpt gen_tac >> strip_tac >> 332 Cases_on ������x p0. p = FALL x p0��� >> fs[] 333 >- (ONCE_REWRITE_TAC[Skolems_def] >> simp[]) >> 334 reverse (Cases_on ������x p0. p = Exists x p0���) >> fs[] 335 >- (ONCE_REWRITE_TAC[Skolems_def] >> simp[]) >> 336 ONCE_REWRITE_TAC[Skolems_def] >> simp[] >> rw[] >> fs[] >> 337 qpat_x_assum ������f:form n. _��� 338 (first_assum o mp_then.mp_then mp_then.Any mp_tac) >> simp[] >> 339 metis_tac[interpretation_Skolem1_E] 340QED 341 342Theorem holds_Skolems_E: 343 ���J p k. 344 (���l m. (J ��� l, m) ��� form_functions p ��� l < k) ��� 345 ���N. interpretation (language {Skolems J p k}) N ��� N.Dom ��� ��� ��� 346 ���v. valuation N v ��� holds N v (Skolems J p k) ��� 347 holds N v p 348Proof 349 ho_match_mp_tac Skolems_ind >> rpt gen_tac >> ntac 2 strip_tac >> 350 Cases_on ������x p0. p = FALL x p0��� >> fs[] 351 >- (ONCE_REWRITE_TAC [Skolems_def] >> simp[] >> rw[] >> fs[] >> 352 first_x_assum 353 (first_assum o mp_then.mp_then (mp_then.Pos (el 2)) mp_tac) >> 354 simp[]) >> 355 reverse (Cases_on ������x p0. p = Exists x p0���) >> fs[] 356 >- (ONCE_REWRITE_TAC [Skolems_def] >> simp[]) >> 357 ONCE_REWRITE_TAC [Skolems_def] >> simp[] >> rw[] >> fs[] >> 358 qpat_x_assum ������q:form n:num. _��� 359 (first_assum o mp_then.mp_then (mp_then.Pos (el 3)) mp_tac) >> simp[] >> 360 disch_then (first_assum o mp_then.mp_then mp_then.Any mp_tac) >> simp[] >> 361 impl_tac 362 >- (rw[] >> rename [���(J ��� n,m) ��� form_functions _���] >> 363 mp_tac (form_functions_Skolem1 |> CONJUNCT1 |> GEN_ALL) >> 364 simp[SUBSET_DEF, Excl "form_functions_Skolem1", Excl "FV_extras"] >> 365 disch_then drule >> rw[Excl "FV_extras"] >> simp[] >> 366 first_x_assum drule >> simp[]) >> 367 strip_tac >> 368 first_assum (mp_then.mp_then (mp_then.Pos last) mp_tac holds_Skolem1_E) >> 369 reverse impl_tac >> simp[] >> conj_tac 370 >- (strip_tac >> first_x_assum drule >> simp[]) >> 371 metis_tac[interpretation_Skolems_E] 372QED 373 374(* ------------------------------------------------------------------------- *) 375(* Now Skolemize an arbitrary (non-prenex) formula. *) 376(* ------------------------------------------------------------------------- *) 377 378Definition Skopre_def: 379 Skopre J p = Skolems J (Prenex p) 0 380End 381 382Theorem FV_Skopre[simp]: 383 FV (Skopre i p) = FV p 384Proof 385 simp[Skopre_def] 386QED 387 388Theorem universal_Skopre[simp]: 389 universal (Skopre i p) 390Proof 391 simp[Skopre_def] 392QED 393 394Theorem form_predicates_Skopre[simp]: 395 form_predicates (Skopre j p) = form_predicates p 396Proof 397 simp[Skopre_def] 398QED 399 400Theorem form_functions_Skopre_I: 401 form_functions p ��� form_functions (Skopre j p) 402Proof 403 simp[Skopre_def] >> 404 metis_tac[SUBSET_TRANS,form_functions_Prenex, form_functions_Skolems_down] 405QED 406 407Theorem form_functions_Skopre_E: 408 form_functions (Skopre j p) ��� {(j ��� l, m) | l,m | T } ��� form_functions p 409Proof 410 simp[Skopre_def] >> 411 qspecl_then [���j���, ���Prenex p���, ���0���] mp_tac form_functions_Skolems_up >> 412 simp[] 413QED 414 415Theorem holds_Skopre_I: 416 ���p j M. 417 (���l m. (j ��� l, m) ��� form_functions p) ��� 418 interpretation (language {p}) M ��� M.Dom ��� ��� ��� 419 (���v. valuation M v ��� holds M v p) 420 ��� 421 ���M'. M'.Dom = M.Dom ��� M'.Pred = M.Pred ��� 422 (���g zs. M'.Fun g zs ��� M.Fun g zs ��� ���l. g = j ��� l) ��� 423 interpretation (language {Skopre j p}) M' ��� 424 ���v. valuation M' v ��� holds M' v (Skopre j p) 425Proof 426 rw[Skopre_def] >> 427 qspecl_then [���j���, ���Prenex p���, ���0���] mp_tac holds_Skolems_I >> simp[] 428QED 429 430Theorem holds_Skopre_E: 431 ���p j N. (���l m. (j ��� l, m) ��� form_functions p) ��� 432 interpretation (language{Skopre j p}) N ��� N.Dom ��� ��� ��� 433 ���v. valuation N v ��� holds N v (Skopre j p) ��� holds N v p 434Proof 435 rw[Skopre_def] >> 436 qspecl_then [���j���, ���Prenex p���, ���0���] mp_tac holds_Skolems_E >> simp[] 437QED 438 439Theorem interpretation_Skopre_E: 440 ���p j N. interpretation (language {Skopre j p}) N ��� 441 interpretation (language {p}) N 442Proof 443 rw[Skopre_def] >> drule interpretation_Skolems_E >> simp[] 444QED 445 446(* ------------------------------------------------------------------------- *) 447(* Bumping up function indices to leave room for Skolem functions. *) 448(* ------------------------------------------------------------------------- *) 449 450Definition bumpmod_def: 451 bumpmod M = M with Fun := ��k zs. M.Fun (nsnd k) zs 452End 453 454Theorem bumpmod_rwts[simp]: 455 (bumpmod M).Pred = M.Pred ��� (bumpmod M).Dom = M.Dom ��� 456 (bumpmod M).Fun (m ��� n) = M.Fun n 457Proof 458 simp[bumpmod_def, FUN_EQ_THM] 459QED 460 461Theorem valuation_bumpmod[simp]: 462 valuation (bumpmod M) v ��� valuation M v 463Proof 464 simp[valuation_def] 465QED 466 467Definition bumpterm_def[simp]: 468 bumpterm (V x) = V x ��� 469 bumpterm (Fn k l) = Fn (0 ��� k) (MAP bumpterm l) 470Termination 471 WF_REL_TAC ���measure term_size��� >> simp[] 472End 473 474Theorem termval_bump[simp]: 475 ���M v t. termval (bumpmod M) v (bumpterm t) = termval M v t 476Proof 477 Induct_on ���t��� >> simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] 478QED 479 480Theorem TFV_bumpterm[simp]: 481 FVT (bumpterm t) = FVT t 482Proof 483 Induct_on ���t��� >> simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] 484QED 485 486Definition bumpform_def[simp]: 487 bumpform False = False ��� 488 bumpform (Pred p l) = Pred p (MAP bumpterm l) ��� 489 bumpform (IMP p q) = IMP (bumpform p) (bumpform q) ��� 490 bumpform (FALL x p) = FALL x (bumpform p) 491End 492 493Theorem FV_bumpform[simp]: 494 FV (bumpform p) = FV p 495Proof 496 Induct_on ���p��� >> 497 asm_simp_tac (srw_ss() ++ ETA_ss) [MAP_MAP_o, combinTheory.o_DEF] 498QED 499 500Theorem holds_bump[simp]: 501 ���M v p. holds (bumpmod M) v (bumpform p) ��� holds M v p 502Proof 503 Induct_on ���p��� >> simp[MAP_MAP_o, combinTheory.o_DEF, Cong MAP_CONG'] 504QED 505 506Theorem term_functions_bumpterm[simp]: 507 term_functions (bumpterm t) = { (0 ��� k, m) | (k,m) ��� term_functions t } 508Proof 509 Induct_on ���t��� >> simp[MAP_MAP_o, Cong MAP_CONG', MEM_MAP, PULL_EXISTS] >> 510 simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[] 511QED 512 513Theorem form_functions_bumpform: 514 form_functions (bumpform p) = { (0 ��� k, m) | (k,m) ��� form_functions p } 515Proof 516 Induct_on ���p��� >> simp[MEM_MAP, MAP_MAP_o, PULL_EXISTS] 517 >- (simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[]) >> 518 simp[Once EXTENSION] >> metis_tac[] 519QED 520 521Theorem form_predicates_bumpform[simp]: 522 form_predicates (bumpform p) = form_predicates p 523Proof 524 Induct_on ���p��� >> simp[] 525QED 526 527Theorem interpretation_bumpform[simp]: 528 interpretation (language {bumpform p}) (bumpmod M) ��� 529 interpretation (language {p}) M 530Proof 531 simp[interpretation_def, language_def, PULL_EXISTS, form_functions_bumpform]>> 532 metis_tac[] 533QED 534 535Definition unbumpterm_def[simp]: 536 unbumpterm (V x) = V x ��� 537 unbumpterm (Fn k l) = Fn (nsnd k) (MAP unbumpterm l) 538Termination 539 WF_REL_TAC ���measure term_size��� >> simp[] 540End 541 542Definition unbumpform_def[simp]: 543 unbumpform False = False ��� 544 unbumpform (Pred p l) = Pred p (MAP unbumpterm l) ��� 545 unbumpform (IMP f1 f2) = IMP (unbumpform f1) (unbumpform f2) ��� 546 unbumpform (FALL x f) = FALL x (unbumpform f) 547End 548 549Theorem bumpterm_inv[simp]: 550 unbumpterm (bumpterm t) = t 551Proof 552 Induct_on ���t��� >> simp[MAP_MAP_o, Cong MAP_CONG'] 553QED 554 555Theorem bumpform_inv[simp]: 556 unbumpform (bumpform p) = p 557Proof 558 Induct_on ���p��� >> simp[MAP_MAP_o, Cong MAP_CONG'] 559QED 560 561Definition unbumpmod_def: 562 unbumpmod M = M with Fun := ��k zs. M.Fun (0 ��� k) zs 563End 564 565Theorem unbumpmod_rwts[simp]: 566 (unbumpmod M).Dom = M.Dom ��� 567 (unbumpmod M).Pred = M.Pred ��� 568 (���v. valuation (unbumpmod M) v ��� valuation M v) 569Proof 570 simp[unbumpmod_def, valuation_def] 571QED 572 573Theorem termval_unbumpmod: 574 termval (unbumpmod M) v t = termval M v (bumpterm t) 575Proof 576 Induct_on ���t��� >> simp[Cong MAP_CONG', MAP_MAP_o] >> simp[unbumpmod_def] 577QED 578 579Theorem holds_unbumpmod: 580 ���M v p. holds (unbumpmod M) v p ��� holds M v (bumpform p) 581Proof 582 Induct_on ���p��� >> simp[MAP_MAP_o, Cong MAP_CONG', termval_unbumpmod] >> 583 simp[unbumpmod_def] 584QED 585 586(* ------------------------------------------------------------------------- *) 587(* Skolemization function. *) 588(* ------------------------------------------------------------------------- *) 589 590Definition SKOLEMIZE_def: 591 SKOLEMIZE p = Skopre (num_of_form (bumpform p) + 1) (bumpform p) 592End 593 594Theorem SKOLEMIZE_props[simp]: 595 universal (SKOLEMIZE p) ��� 596 prenex (SKOLEMIZE p) ��� 597 form_predicates (SKOLEMIZE p) = form_predicates p ��� 598 FV (SKOLEMIZE p) = FV p 599Proof 600 simp[SKOLEMIZE_def, universal_prenex] 601QED 602 603Theorem form_functions_SKOLEMIZE_I = 604 form_functions_Skopre_I 605 |> Q.INST [���p��� |-> ���bumpform p���, 606 ���j��� |-> ���num_of_form (bumpform p) + 1���] 607 |> SIMP_RULE (srw_ss()) [GSYM SKOLEMIZE_def]; 608 609Theorem form_functions_SKOLEMIZE_E: 610 form_functions (SKOLEMIZE p) ��� 611 {(k ��� l, m) | k,l,m | k = num_of_form (bumpform p) +1} ��� 612 form_functions (bumpform p) 613Proof 614 rw[SKOLEMIZE_def, SUBSET_DEF] >> 615 drule (form_functions_Skopre_E |> SIMP_RULE (srw_ss()) [SUBSET_DEF]) >> 616 metis_tac[] 617QED 618 619Theorem holds_SKOLEMIZE_I: 620 ���M p. interpretation (language {bumpform p}) M ��� M.Dom ��� ��� ��� 621 (���v. valuation M v ��� holds M v (bumpform p)) 622 ��� 623 ���M'. M'.Dom = M.Dom ��� 624 M'.Pred = M.Pred ��� 625 (���g zs. M'.Fun g zs ��� M.Fun g zs ��� 626 ���l. g = (num_of_form (bumpform p) + 1) ��� l) ��� 627 interpretation (language {SKOLEMIZE p}) M' ��� 628 ���v. valuation M' v ��� holds M' v (SKOLEMIZE p) 629Proof 630 simp[SKOLEMIZE_def] >> rpt strip_tac >> 631 irule holds_Skopre_I >> 632 simp[form_functions_bumpform] 633QED 634 635Theorem holds_SKOLEMIZE_E: 636 ���N. interpretation (language {SKOLEMIZE p}) N ��� N.Dom ��� ��� 637 ��� 638 ���v. valuation N v ��� holds N v (SKOLEMIZE p) ��� 639 holds N v (bumpform p) 640Proof 641 simp[SKOLEMIZE_def] >> rpt strip_tac >> irule holds_Skopre_E >> 642 simp[form_functions_bumpform] >> 643 goal_assum (first_assum o mp_then Any mp_tac) >> simp[] 644QED 645 646Theorem interpretation_SKOLEMIZE_E: 647 interpretation (language {SKOLEMIZE p}) N ��� 648 interpretation (language {bumpform p}) N 649Proof 650 simp[SKOLEMIZE_def] >> strip_tac >> irule interpretation_Skopre_E >> 651 metis_tac[] 652QED 653 654Theorem form_functions_SKOLEMIZE_IN_E = 655 SIMP_RULE (srw_ss()) 656 [SUBSET_DEF, form_functions_bumpform, pairTheory.FORALL_PROD] 657 form_functions_SKOLEMIZE_E 658 659(* ------------------------------------------------------------------------- *) 660(* Construction of Skolem model for a formula. *) 661(* ------------------------------------------------------------------------- *) 662 663Definition SKOMOD1_def: 664 SKOMOD1 p M = 665 if (���v. valuation M v ��� holds M v p) then 666 @M'. M'.Dom = (bumpmod M).Dom ��� 667 M'.Pred = (bumpmod M).Pred ��� 668 (���g zs. M'.Fun g zs ��� (bumpmod M).Fun g zs ��� 669 ���l. g = (num_of_form (bumpform p) + 1) ��� l) ��� 670 interpretation (language {SKOLEMIZE p}) M' ��� 671 ���v. valuation M' v ��� holds M' v (SKOLEMIZE p) 672 else M with Fun := ��g zs. @a. a ��� M.Dom 673End 674 675Theorem SKOMOD1_rwts[simp]: 676 interpretation (language{p}) M ��� M.Dom ��� ��� ��� 677 (SKOMOD1 p M).Dom = M.Dom ��� 678 (SKOMOD1 p M).Pred = M.Pred ��� 679 interpretation (language {SKOLEMIZE p}) (SKOMOD1 p M) 680Proof 681 simp[SKOMOD1_def] >> reverse COND_CASES_TAC >> simp[] 682 >- (simp[interpretation_def,language_def] >> rw[] >> 683 fs[EXTENSION] >> SELECT_ELIM_TAC >> simp[] >> metis_tac[]) >> 684 strip_tac >> SELECT_ELIM_TAC >> simp[] >> 685 ���M.Dom = (bumpmod M).Dom ��� M.Pred = (bumpmod M).Pred��� by simp[] >> 686 ASM_REWRITE_TAC[] >> irule holds_SKOLEMIZE_I >> 687 ntac 2 (pop_assum (K ALL_TAC)) >> simp[] 688QED 689 690Theorem holds_SKOMOD1_I: 691 interpretation (language{p}) M ��� M.Dom ��� ��� ��� 692 (���v. valuation M v ��� holds M v p) 693 ��� 694 (���g zs. (SKOMOD1 p M).Fun g zs ��� (bumpmod M).Fun g zs ��� 695 ���l. g = (num_of_form (bumpform p) + 1) ��� l) ��� 696 ���v. valuation M v ��� holds (SKOMOD1 p M) v (SKOLEMIZE p) 697Proof 698 strip_tac >> strip_tac >> simp[SKOMOD1_def] >> SELECT_ELIM_TAC >> simp[] >> 699 rw[] 700 >- (���M.Dom = (bumpmod M).Dom ��� M.Pred = (bumpmod M).Pred��� by simp[] >> 701 ASM_REWRITE_TAC[] >> irule holds_SKOLEMIZE_I >> 702 ntac 2 (pop_assum (K ALL_TAC)) >> simp[]) 703 >- metis_tac[] >> 704 first_x_assum irule >> rfs[valuation_def] 705QED 706 707Definition SKOMOD_def: 708 SKOMOD M = 709 M with 710 Fun := ��g zs. 711 if nfst g = 0 then M.Fun (nsnd g) zs 712 else (SKOMOD1 (unbumpform (form_of_num (nfst g - 1))) M).Fun g zs 713End 714 715Theorem SKOMOD_rwts[simp]: 716 (SKOMOD M).Dom = M.Dom ��� 717 (SKOMOD M).Pred = M.Pred ��� 718 (���v. valuation (SKOMOD M) v = valuation M v) 719Proof 720 simp[SKOMOD_def, valuation_def] 721QED 722 723Theorem SKOMOD_INTERPRETATION: 724 interpretation (language {p}) M ��� M.Dom ��� ��� 725 ��� 726 interpretation (language {SKOLEMIZE p}) (SKOMOD M) 727Proof 728 strip_tac >> drule_all_then strip_assume_tac SKOMOD1_rwts >> 729 fs[interpretation_def, language_def, SKOMOD_def] >> rw[] >> 730 drule form_functions_SKOLEMIZE_IN_E >> rw[] >> fs[] >> rfs[] 731QED 732 733Theorem SKOMOD_WORKS: 734 interpretation (language {p}) M ��� M.Dom ��� ��� ��� 735 ((���v. valuation M v ��� holds (SKOMOD M) v (SKOLEMIZE p)) ��� 736 (���v. valuation M v ��� holds M v p)) 737Proof 738 strip_tac >> reverse eq_tac >> strip_tac 739 >- (rpt strip_tac >> 740 ���holds (SKOMOD1 p M) v (SKOLEMIZE p)��� 741 by metis_tac[holds_SKOMOD1_I] >> 742 ���holds (SKOMOD M) v (SKOLEMIZE p) ��� holds (SKOMOD1 p M) v (SKOLEMIZE p)��� 743 suffices_by simp[] >> 744 irule holds_functions >> simp[SKOMOD_def] >> rpt strip_tac >> 745 drule form_functions_SKOLEMIZE_IN_E >> rw[] >> fs[] >> 746 CCONTR_TAC >> 747 ���(SKOMOD1 p M).Fun (0 ��� k) zs ��� (bumpmod M).Fun (0 ��� k) zs��� 748 by simp[] >> 749 drule_all_then strip_assume_tac holds_SKOMOD1_I >> 750 first_x_assum (qpat_x_assum ���_ ��� _��� o mp_then (Pos hd) mp_tac) >> 751 simp[]) >> 752 rpt strip_tac >> first_x_assum (first_assum o mp_then (Pos hd) assume_tac) >> 753 drule_all_then assume_tac SKOMOD_INTERPRETATION >> 754 ���valuation (SKOMOD M) v ��� (SKOMOD M).Dom ��� ������ by simp[] >> 755 drule_all_then assume_tac holds_SKOLEMIZE_E >> 756 ���holds (bumpmod M) v (bumpform p)��� suffices_by simp[] >> 757 ���holds (bumpmod M) v (bumpform p) ��� holds (SKOMOD M) v (bumpform p)��� 758 suffices_by simp[] >> irule holds_functions >> 759 simp[form_functions_bumpform, PULL_EXISTS, SKOMOD_def] 760QED 761 762Theorem SKOMOD_INTERPRETATION_SET: 763 interpretation (language s) M ��� M.Dom ��� ��� 764 ��� 765 interpretation (language {SKOLEMIZE p | p ��� s}) (SKOMOD M) 766Proof 767 mp_tac 768 (SKOMOD1_rwts |> UNDISCH |> CONJUNCTS |> last |> DISCH_ALL |> Q.GEN ���p���) >> 769 simp[interpretation_def, language_def, functions_def, Excl "SKOMOD1_rwts"] >> 770 simp[PULL_EXISTS] >> rw[] >> 771 rename [���p ��� s���, ���(f,LENGTH zs) ��� form_functions (SKOLEMIZE p)���] >> 772 first_x_assum (qpat_assum `p ��� s` o mp_then Any mp_tac) >> strip_tac >> 773 first_x_assum (first_assum o mp_then (Pos hd) strip_assume_tac) >> rfs[] >> 774 ���(SKOMOD1 p M).Dom = M.Dom��� 775 by (irule (SKOMOD1_rwts |> UNDISCH |> CONJUNCT1 |> DISCH_ALL) >> 776 simp[interpretation_def, language_def]) >> fs[] >> 777 simp[SKOMOD_def] >> drule form_functions_SKOLEMIZE_IN_E >> rw[] >> fs[] 778QED 779 780Theorem interpretation_language_member: 781 interpretation (language s) M ��� p ��� s ��� 782 interpretation (language {p}) M 783Proof 784 simp[interpretation_def, functions_def, language_def, PULL_EXISTS] >> 785 metis_tac[] 786QED 787 788Theorem SKOLEMIZE_SATISFIABLE: 789 (���M : �� model. M.Dom ��� ��� ��� interpretation (language s) M ��� M satisfies s) ��� 790 (���M : �� model. 791 M.Dom ��� ��� ��� interpretation (language {SKOLEMIZE p | p ��� s}) M ��� 792 M satisfies {SKOLEMIZE p | p ��� s}) 793Proof 794 simp[satisfies_def, PULL_EXISTS] >> rw[EQ_IMP_THM] 795 >- (qexists_tac ���SKOMOD M��� >> simp[SKOMOD_INTERPRETATION_SET] >> 796 metis_tac[SKOMOD_WORKS, interpretation_language_member]) >> 797 qexists_tac ���unbumpmod M��� >> simp[] >> conj_tac 798 >- (fs[interpretation_def, language_def, PULL_EXISTS, functions_def, 799 unbumpmod_def] >> rw[] >> 800 last_x_assum irule >> simp[] >> 801 goal_assum drule >> 802 irule (REWRITE_RULE [SUBSET_DEF] form_functions_SKOLEMIZE_I) >> 803 simp[form_functions_bumpform]) >> 804 simp[holds_unbumpmod] >> rw[] >> rename [����� ��� s���] >> 805 ���interpretation (language {SKOLEMIZE ��}) M��� 806 suffices_by metis_tac[holds_SKOLEMIZE_E] >> 807 irule interpretation_language_member >> 808 goal_assum (first_assum o mp_then Any mp_tac) >> simp[] >> metis_tac[] 809QED 810 811(* ------------------------------------------------------------------------- *) 812(* Skolemization right down to quantifier-free formula. *) 813(* ------------------------------------------------------------------------- *) 814 815Definition specialize_def[simp]: 816 specialize False = False ��� 817 specialize (Pred p l) = Pred p l ��� 818 specialize (IMP p1 p2) = IMP p1 p2 ��� 819 specialize (FALL x p) = specialize p 820End 821 822Theorem holds_specialize[simp]: 823 ���M p. M.Dom ��� ��� ��� 824 ((���v. valuation M v ��� holds M v (specialize p)) ��� 825 (���v. valuation M v ��� holds M v p)) 826Proof 827 Induct_on ���p��� >> simp[Excl "holds_def", Excl "HOLDS", holds_uclose] 828QED 829 830Theorem specialize_satisfies: 831 M.Dom ��� ��� ��� (M satisfies {specialize p | p ��� s} ��� M satisfies s) 832Proof 833 rw[satisfies_def, PULL_EXISTS] >> metis_tac[holds_specialize] 834QED 835 836Theorem specialize_satisfies_IMAGE: 837 M.Dom ��� ��� ��� (M satisfies (IMAGE specialize s) ��� M satisfies s) 838Proof 839 ���IMAGE specialize s = {specialize p | p ��� s}��� 840 suffices_by simp[specialize_satisfies] >> simp[EXTENSION] 841QED 842 843Theorem specialize_qfree: 844 ���p. universal p ��� qfree(specialize p) 845Proof 846 Induct >> simp[Once universal_cases] 847QED 848 849Theorem form_functions_specialize[simp]: 850 form_functions (specialize p) = form_functions p 851Proof 852 Induct_on ���p��� >> simp[] 853QED 854 855Theorem form_predicates_specialize[simp]: 856 form_predicates (specialize p) = form_predicates p 857Proof 858 Induct_on ���p��� >> simp[] 859QED 860 861Theorem language_specialize[simp]: 862 language {specialize p | p ��� s} = language s 863Proof 864 simp[language_def, functions_def, predicates_def] >> 865 ONCE_REWRITE_TAC[EXTENSION] >> simp[PULL_EXISTS] 866QED 867 868Theorem language_specialize_IMAGE[simp]: 869 language (IMAGE specialize s) = language s 870Proof 871 simp[language_def, functions_def, predicates_def] >> 872 ONCE_REWRITE_TAC[EXTENSION] >> simp[PULL_EXISTS] 873QED 874 875Definition SKOLEM_def: (* the last of them *) 876 SKOLEM p = specialize (SKOLEMIZE p) 877End 878 879Theorem qfree_SKOLEM[simp]: 880 qfree (SKOLEM p) 881Proof 882 simp[SKOLEM_def, specialize_qfree] 883QED 884 885Theorem SKOLEM_SATISFIABLE: 886 (���M:�� model. M.Dom ��� ��� ��� interpretation (language s) M ��� M satisfies s) ��� 887 (���M:�� model. 888 M.Dom ��� ��� ��� interpretation (language {SKOLEM p | p ��� s}) M ��� 889 M satisfies {SKOLEM p | p ��� s}) 890Proof 891 simp[SimpLHS, Once SKOLEMIZE_SATISFIABLE] >> eq_tac >> rw[SKOLEM_def] >> 892 ���{specialize (SKOLEMIZE p) | p ��� s} = IMAGE specialize { SKOLEMIZE p | p ��� s}��� 893 by simp[EXTENSION, PULL_EXISTS] >> fs[] >> 894 rfs[specialize_satisfies_IMAGE] >> csimp[specialize_satisfies_IMAGE] >> 895 metis_tac[] 896QED 897 898Theorem satisfiable_SKOLEM: 899 satisfiable (:��) { SKOLEM p | p ��� s } ��� satisfiable (:��) s 900Proof 901 simp[satisfiable_def, GSYM SKOLEM_SATISFIABLE] 902QED 903 904 905val _ = export_theory(); 906