1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6(* --------------------------------------------------------------------- *) 7(* Embedding the semantaics of objects as a foundational layer, *) 8(* according to Abadi and Cardelli, "A Theory of Objects." *) 9(* --------------------------------------------------------------------- *) 10 11 12val _ = new_theory "lift"; 13 14 15open prim_recTheory pairTheory pairLib listTheory; 16open combinTheory pred_setTheory; 17open numTheory numLib arithmeticTheory; 18open bossLib; 19open Mutual; 20open dep_rewrite; 21open more_listTheory more_setTheory; 22open variableTheory; 23open objectTheory; 24open alphaTheory; 25 26open quotientLib; 27 28open tactics; 29open Rsyntax; 30 31 32 33val vars = ty_antiq( ==`:var list`== ); 34val subs = ty_antiq( ==`:(var # obj1) list`== ); 35val obj = ty_antiq( ==`:obj1`== ); 36val dict = ty_antiq( ==`:(string # method1) list`== ); 37val entry = ty_antiq( ==`:string # method1`== ); 38val method = ty_antiq( ==`:method1`== ); 39 40 41val [ALPHA_obj_REFL, ALPHA_dict_REFL, ALPHA_entry_REFL, ALPHA_method_REFL] 42 = CONJUNCTS ALPHA_REFL; 43 44val [ALPHA_obj_SYM, ALPHA_dict_SYM, ALPHA_entry_SYM, ALPHA_method_SYM] 45 = map (GEN_ALL o CONJUNCT2 o SPEC_ALL o REWRITE_RULE[EQ_IMP_THM]) 46 (CONJUNCTS ALPHA_SYM); 47 48val [ALPHA_obj_TRANS, ALPHA_dict_TRANS, ALPHA_entry_TRANS, ALPHA_method_TRANS] 49 = CONJUNCTS ALPHA_TRANS; 50 51val ALPHA_obj_EQUIV = save_thm("ALPHA_obj_EQUIV", 52 refl_sym_trans_equiv ALPHA_obj_REFL ALPHA_obj_SYM ALPHA_obj_TRANS); 53 54val ALPHA_dict_EQUIV = save_thm("ALPHA_dict_EQUIV", 55 refl_sym_trans_equiv ALPHA_dict_REFL ALPHA_dict_SYM ALPHA_dict_TRANS); 56 57val ALPHA_entry_EQUIV = save_thm("ALPHA_entry_EQUIV", 58 refl_sym_trans_equiv ALPHA_entry_REFL ALPHA_entry_SYM ALPHA_entry_TRANS); 59 60val ALPHA_method_EQUIV = save_thm("ALPHA_method_EQUIV", 61 refl_sym_trans_equiv ALPHA_method_REFL ALPHA_method_SYM ALPHA_method_TRANS); 62 63val ALPHA_EQUIV = LIST_CONJ 64 [ALPHA_obj_EQUIV, ALPHA_dict_EQUIV, ALPHA_entry_EQUIV, ALPHA_method_EQUIV]; 65 66 67(* ALPHA_dict/entry_EQUIV will not be used, rather SUBST_EQUIV: *) 68 69val SUBST_EQUIV = make_equiv [ALPHA_obj_EQUIV] [LIST_EQUIV, PAIR_EQUIV] 70 ``:(var # obj1) list``; 71 72 73val ALPHA_entry_EQ = store_thm 74 ("ALPHA_entry_EQ", 75 ���ALPHA_entry = ($= ### ALPHA_method)���, 76 CONV_TAC (FUN_EQ_CONV THENC RAND_CONV (ABS_CONV FUN_EQ_CONV)) 77 THEN Cases 78 THEN Cases 79 THEN ASM_REWRITE_TAC[ALPHA_object_pos,ALPHA_object_neg,PAIR_REL_THM] 80 ); 81 82val ALPHA_dict_EQ = store_thm 83 ("ALPHA_dict_EQ", 84 ���ALPHA_dict = LIST_REL ($= ### ALPHA_method)���, 85 CONV_TAC (FUN_EQ_CONV THENC RAND_CONV (ABS_CONV FUN_EQ_CONV)) 86 THEN Induct 87 THENL [ ALL_TAC, GEN_TAC ] 88 THEN Induct 89 THEN REPEAT GEN_TAC 90 THEN ASM_REWRITE_TAC[ALPHA_object_pos,ALPHA_object_neg,LIST_REL_def, 91 ALPHA_entry_EQ] 92 ); 93 94 95 96 97 98(* Prove the respectfulness theorems for the functions to be lifted. *) 99 100val ALPHA_object_pos1 = 101 REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ] ALPHA_object_pos; 102 103val OVAR1_RSP = store_thm 104 ("OVAR1_RSP", 105 ���!x1 x2. 106 (x1 = x2) ==> 107 ALPHA_obj (OVAR1 x1) (OVAR1 x2)���, 108 REPEAT GEN_TAC 109 THEN STRIP_TAC 110 THEN ASM_REWRITE_TAC[ALPHA_object_pos1] 111 ); 112 113val OBJ1_RSP = store_thm 114 ("OBJ1_RSP", 115 ���!d1 d2. 116 LIST_REL ($= ### ALPHA_method) d1 d2 ==> 117 ALPHA_obj (OBJ1 d1) (OBJ1 d2)���, 118 REPEAT GEN_TAC 119 THEN STRIP_TAC 120 THEN ASM_REWRITE_TAC[ALPHA_object_pos1] 121 ); 122 123val INVOKE1_RSP = store_thm 124 ("INVOKE1_RSP", 125 ���!o1 o2 s1 s2. 126 ALPHA_obj o1 o2 /\ (s1 = s2) ==> 127 ALPHA_obj (INVOKE1 o1 s1) (INVOKE1 o2 s2)���, 128 REPEAT GEN_TAC 129 THEN STRIP_TAC 130 THEN ASM_REWRITE_TAC[ALPHA_object_pos1] 131 ); 132 133val UPDATE1_RSP = store_thm 134 ("UPDATE1_RSP", 135 ���!o1 o2 s1 s2 m1 m2. 136 ALPHA_obj o1 o2 /\ (s1 = s2) /\ ALPHA_method m1 m2 ==> 137 ALPHA_obj (UPDATE1 o1 s1 m1) (UPDATE1 o2 s2 m2)���, 138 REPEAT GEN_TAC 139 THEN STRIP_TAC 140 THEN ASM_REWRITE_TAC[ALPHA_object_pos] 141 ); 142 143val SIGMA1_RSP = store_thm 144 ("SIGMA1_RSP", 145 ���!x1 x2 o1 o2. 146 (x1 = x2) /\ ALPHA_obj o1 o2 ==> 147 ALPHA_method (SIGMA1 x1 o1) (SIGMA1 x2 o2)���, 148 REPEAT GEN_TAC 149 THEN STRIP_TAC 150 THEN ASM_REWRITE_TAC[ALPHA_method_SIGMA] 151 ); 152 153val [HEIGHT_obj1_RSP, HEIGHT_dict1_RSP, HEIGHT_entry1_RSP, HEIGHT_method1_RSP] 154 = CONJUNCTS (REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ] ALPHA_HEIGHT); 155 156val [FV_obj1_RSP, FV_dict1_RSP, FV_entry1_RSP, FV_method1_RSP] 157 = CONJUNCTS (REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ] ALPHA_FV); 158 159val vsubst1_RSP = store_thm 160 ("vsubst1_RSP", 161 ���!xs1 xs2 ys1 ys2. 162 (xs1 = xs2) /\ (ys1 = ys2) ==> 163 LIST_REL ($= ### ALPHA_obj) (xs1 // ys1) ((xs2 // ys2):^subs)���, 164 REPEAT GEN_TAC 165 THEN STRIP_TAC 166 THEN ASM_REWRITE_TAC[equiv_refl SUBST_EQUIV] 167 ); 168 169val ALPHA_SUB1 = store_thm 170 ("ALPHA_SUB1", 171 ���!s1:^subs s2 x. LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 172 ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)���, 173 LIST_INDUCT_TAC 174 THENL [ALL_TAC, GEN_TAC] 175 THEN LIST_INDUCT_TAC 176 THEN REPEAT GEN_TAC 177 THEN REWRITE_TAC[LIST_REL_def] 178 THEN REWRITE_TAC[SUB1_def] 179 THEN REWRITE_TAC[ALPHA_obj_REFL] 180 THEN POP_TAC 181 THEN ONCE_REWRITE_TAC[GSYM PAIR] 182 THEN CONV_TAC (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV 183 (PURE_REWRITE_CONV[PAIR_REL] 184 THENC DEPTH_CONV GEN_BETA_CONV))))) 185 THEN STRIP_TAC 186 THEN RES_TAC 187 THEN CONV_TAC (DEPTH_CONV let_CONV) 188 THEN ASM_REWRITE_TAC[] 189 THEN COND_CASES_TAC 190 THEN ASM_REWRITE_TAC[] 191 ); 192 193val SUB1_RSP = store_thm 194 ("SUB1_RSP", 195 ���!s1:^subs s2 x1 x2. 196 LIST_REL ($= ### ALPHA_obj) s1 s2 /\ (x1 = x2) ==> 197 ALPHA_obj (SUB1 s1 x1) (SUB1 s2 x2)���, 198 REPEAT STRIP_TAC 199 THEN ASM_REWRITE_TAC[] 200 THEN MATCH_MP_TAC ALPHA_SUB1 201 THEN ASM_REWRITE_TAC[] 202 ); 203 204 205val FV_subst_RSP = store_thm 206 ("FV_subst_RSP", 207 ���!s1:^subs s2 xs ys. 208 LIST_REL ($= ### ALPHA_obj) s1 s2 /\ (xs = ys) ==> 209 (FV_subst1 s1 xs = FV_subst1 s2 ys)���, 210 REPEAT STRIP_TAC 211 THEN POP_ASSUM REWRITE_THM 212 THEN REWRITE_TAC[FV_subst1] 213 THEN AP_TERM_TAC 214 THEN AP_THM_TAC 215 THEN AP_TERM_TAC 216 THEN CONV_TAC FUN_EQ_CONV 217 THEN GEN_TAC 218 THEN REWRITE_TAC[o_THM] 219 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_FV)) 220 THEN MATCH_MP_TAC ALPHA_SUB1 221 THEN ASM_REWRITE_TAC[] 222 ); 223 224 225val ALPHA_subst_obj_RSP = store_thm 226 ("ALPHA_subst_obj_RSP", 227 ���!s1:^subs s2 o1:obj1. 228 LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 229 ALPHA_subst (FV_obj1 o1) s1 s2���, 230 REPEAT GEN_TAC 231 THEN DISCH_TAC 232 THEN REWRITE_TAC[ALPHA_subst] 233 THEN GEN_TAC 234 THEN DISCH_TAC 235 THEN MATCH_MP_TAC ALPHA_SUB1 236 THEN FIRST_ASSUM ACCEPT_TAC 237 ); 238 239val ALPHA_subst_dict_RSP = store_thm 240 ("ALPHA_subst_dict_RSP", 241 ���!s1:^subs s2 d. 242 LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 243 ALPHA_subst (FV_dict1 d) s1 s2���, 244 REPEAT GEN_TAC 245 THEN DISCH_TAC 246 THEN REWRITE_TAC[ALPHA_subst] 247 THEN GEN_TAC 248 THEN DISCH_TAC 249 THEN MATCH_MP_TAC ALPHA_SUB1 250 THEN FIRST_ASSUM ACCEPT_TAC 251 ); 252 253val ALPHA_subst_entry_RSP = store_thm 254 ("ALPHA_subst_entry_RSP", 255 ���!s1:^subs s2 e. 256 LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 257 ALPHA_subst (FV_entry1 e) s1 s2���, 258 REPEAT GEN_TAC 259 THEN DISCH_TAC 260 THEN REWRITE_TAC[ALPHA_subst] 261 THEN GEN_TAC 262 THEN DISCH_TAC 263 THEN MATCH_MP_TAC ALPHA_SUB1 264 THEN FIRST_ASSUM ACCEPT_TAC 265 ); 266 267val ALPHA_subst_method_RSP = store_thm 268 ("ALPHA_subst_method_RSP", 269 ���!s1:^subs s2 m. 270 LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 271 ALPHA_subst (FV_method1 m) s1 s2���, 272 REPEAT GEN_TAC 273 THEN DISCH_TAC 274 THEN REWRITE_TAC[ALPHA_subst] 275 THEN GEN_TAC 276 THEN DISCH_TAC 277 THEN MATCH_MP_TAC ALPHA_SUB1 278 THEN FIRST_ASSUM ACCEPT_TAC 279 ); 280 281 282val SUBo_RSP = store_thm 283 ("SUBo_RSP", 284 ���!o1:^obj o2 s1 s2. 285 ALPHA_obj o1 o2 /\ LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 286 ALPHA_obj (o1 <[ s1) (o2 <[ s2)���, 287 REPEAT STRIP_TAC 288 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_SUB_CONTEXT)) 289 THEN IMP_RES_TAC ALPHA_subst_obj_RSP 290 THEN ASM_REWRITE_TAC[] 291 ); 292 293val ALPHA_SUB_CONTEXT = 294 REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ] ALPHA_SUB_CONTEXT; 295 296val SUBd_RSP = store_thm 297 ("SUBd_RSP", 298 ���!d1 d2 s1 s2. 299 LIST_REL ($= ### ALPHA_method) d1 d2 /\ 300 LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 301 LIST_REL ($= ### ALPHA_method) (d1 <[ s1) (d2 <[ s2)���, 302 REPEAT STRIP_TAC 303 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS (ALPHA_SUB_CONTEXT))) 304 THEN IMP_RES_TAC ALPHA_subst_dict_RSP 305 THEN ASM_REWRITE_TAC[] 306 ); 307 308val SUBe_RSP = store_thm 309 ("SUBe_RSP", 310 ���!e1 e2 s1 s2. 311 ($= ### ALPHA_method) e1 e2 /\ LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 312 ($= ### ALPHA_method) (e1 <[ s1) (e2 <[ s2)���, 313 REPEAT STRIP_TAC 314 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_SUB_CONTEXT)) 315 THEN IMP_RES_TAC ALPHA_subst_entry_RSP 316 THEN ASM_REWRITE_TAC[] 317 ); 318 319val SUBm_RSP = store_thm 320 ("SUBm_RSP", 321 ���!m1 m2 s1 s2. 322 ALPHA_method m1 m2 /\ LIST_REL ($= ### ALPHA_obj) s1 s2 ==> 323 ALPHA_method (m1 <[ s1) (m2 <[ s2)���, 324 REPEAT STRIP_TAC 325 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_SUB_CONTEXT)) 326 THEN IMP_RES_TAC ALPHA_subst_method_RSP 327 THEN ASM_REWRITE_TAC[] 328 ); 329 330 331val ALPHA_subst_RSP = store_thm 332 ("ALPHA_subst_RSP", 333 ���!s1:^subs s2 t1 t2 (t:var -> bool). 334 LIST_REL ($= ### ALPHA_obj) s1 s2 /\ 335 LIST_REL ($= ### ALPHA_obj) t1 t2 ==> 336 (ALPHA_subst t s1 t1 = ALPHA_subst t s2 t2)���, 337 REPEAT GEN_TAC 338 THEN STRIP_TAC 339 THEN REWRITE_TAC[ALPHA_subst] 340 THEN EQ_TAC 341 THEN DISCH_TAC 342 THEN GEN_TAC 343 THEN DISCH_TAC 344 THEN RES_TAC 345 THEN IMP_RES_THEN (ASSUME_TAC o SPEC_ALL) ALPHA_SUB1 346 THEN IMP_RES_TAC ALPHA_SYM 347 THEN IMP_RES_TAC ALPHA_TRANS 348 ); 349 350 351val BV_subst_RSP = store_thm 352 ("BV_subst_RSP", 353 ���!REL (abs:'a -> 'b) rep. 354 QUOTIENT REL abs rep 355 ==> 356 !s1 s2. 357 (LIST_REL ($= ### REL)) s1 s2 ==> 358 (BV_subst s1 = BV_subst s2)���, 359 REPEAT GEN_TAC 360 THEN STRIP_TAC 361 THEN Induct 362 THENL [ALL_TAC, GEN_TAC] 363 THEN Induct 364 THEN REWRITE_TAC[LIST_REL_def] 365 THEN REPEAT STRIP_TAC 366 THEN REWRITE_TAC[BV_subst_def] 367 THEN MK_COMB_TAC 368 THENL 369 [ AP_TERM_TAC 370 THEN IMP_RES_TAC (MATCH_MP FST_RSP (identity_quotient (==`:var`==))), 371 372 FIRST_ASSUM MATCH_MP_TAC 373 THEN FIRST_ASSUM ACCEPT_TAC 374 ] 375 ); 376 377val BV_subst_PRS = store_thm 378 ("BV_subst_PRS", 379 ���!REL (abs:'a -> 'b) rep. 380 QUOTIENT REL abs rep 381 ==> 382 !s. BV_subst s = BV_subst (MAP(I ## rep) s)���, 383 REPEAT GEN_TAC 384 THEN STRIP_TAC 385 THEN Induct 386 THEN REWRITE_TAC[MAP] 387 THEN REWRITE_TAC[BV_subst_def] 388 THEN Cases 389 THEN REWRITE_TAC[PAIR_MAP_THM,I_THM,FST] 390 THEN AP_TERM_TAC 391 THEN FIRST_ASSUM ACCEPT_TAC 392 ); 393 394 395val FV_subst_EQ1' = store_thm 396 ("FV_subst_EQ1'", 397 ���!s1:^subs s2 t. 398 (!x. (x IN t) ==> ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)) ==> 399 (FV_subst1 s1 t = FV_subst1 s2 t)���, 400 REPEAT STRIP_TAC 401 THEN REWRITE_TAC[FV_subst1] 402 THEN AP_TERM_TAC 403 THEN REWRITE_TAC[EXTENSION] 404 THEN GEN_TAC 405 THEN REWRITE_TAC[IN_IMAGE,o_THM] 406 THEN EQ_TAC 407 THEN STRIP_TAC 408 THENL 409 [ EXISTS_TAC ���x':var��� 410 THEN ASM_REWRITE_TAC[] 411 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_FV)) 412 THEN RES_TAC, 413 414 EXISTS_TAC ���x':var��� 415 THEN ASM_REWRITE_TAC[] 416 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 417 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_FV)) 418 THEN RES_TAC 419 ] 420 ); 421 422 423val TAUT_PROVE = EQT_ELIM o tautLib.TAUT_CONV; 424val OR_IMP = TAUT_PROVE ���(a \/ b ==> c) = ((a ==> c) /\ (b ==> c))���; 425 426val subst_EQ1' = store_thm 427 ("subst_EQ1'", 428 ���(!a s1 s2. 429 (!x. (x IN FV_obj1 a) ==> ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)) ==> 430 ALPHA_obj (a <[ s1) (a <[ s2)) /\ 431 (!a s1 s2. 432 (!x. (x IN FV_dict1 a) ==> ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)) ==> 433 LIST_REL ($= ### ALPHA_method) (a <[ s1) (a <[ s2)) /\ 434 (!a s1 s2. 435 (!x. (x IN FV_entry1 a) ==> ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)) ==> 436 ($= ### ALPHA_method) (a <[ s1) (a <[ s2)) /\ 437 (!a s1 s2. 438 (!x. (x IN FV_method1 a) ==> ALPHA_obj (SUB1 s1 x) (SUB1 s2 x)) ==> 439 ALPHA_method (a <[ s1) (a <[ s2))���, 440 Induct 441 THEN REWRITE_TAC[FV_object1_def,IN_UNION,IN] 442 THEN REWRITE_TAC[OR_IMP] 443 THEN CONV_TAC (DEPTH_CONV FORALL_AND_CONV) 444 THEN REPEAT STRIP_TAC 445 THEN REWRITE_TAC[SUB_object1_def] 446 THEN RES_TAC 447 (* 8 subgoals *) 448 THENL 449 [ FIRST_ASSUM MATCH_MP_TAC 450 THEN REFL_TAC, 451 452 MATCH_MP_TAC OBJ1_RSP 453 THEN FIRST_ASSUM ACCEPT_TAC, 454 455 MATCH_MP_TAC INVOKE1_RSP 456 THEN ASM_REWRITE_TAC[], 457 458 MATCH_MP_TAC UPDATE1_RSP 459 THEN REWRITE_TAC[] 460 THEN CONJ_TAC 461 THEN FIRST_ASSUM ACCEPT_TAC, 462 463 IMP_RES_THEN REWRITE_THM FV_subst_EQ1' 464 THEN CONV_TAC (DEPTH_CONV let_CONV) 465 THEN MATCH_MP_TAC SIGMA1_RSP 466 THEN REWRITE_TAC[] 467 THEN FIRST_ASSUM MATCH_MP_TAC 468 THEN REWRITE_TAC[SUB1] 469 THEN GEN_TAC 470 THEN DISCH_TAC 471 THEN COND_CASES_TAC 472 THEN ASM_REWRITE_TAC[ALPHA_REFL] 473 THEN FIRST_ASSUM MATCH_MP_TAC 474 THEN ASM_REWRITE_TAC[IN_DIFF,IN], 475 476 REWRITE_TAC[LIST_REL_def], 477 478 REWRITE_TAC[LIST_REL_def] 479 THEN CONJ_TAC 480 THEN FIRST_ASSUM ACCEPT_TAC, 481 482 REWRITE_TAC[PAIR_REL_THM] 483 THEN FIRST_ASSUM ACCEPT_TAC 484 ] 485 ); 486 487 488val BV_subst_IDENT1 = store_thm 489 ("BV_subst_IDENT1", 490 ���!s:^subs x. ~(x IN (BV_subst s)) ==> (SUB1 s x = OVAR1 x)���, 491 LIST_INDUCT_TAC 492 THEN REWRITE_TAC[BV_subst_def,SUB1_def] 493 THEN REWRITE_TAC[IN,DE_MORGAN_THM] 494 THEN REPEAT STRIP_TAC 495 THEN RES_TAC 496 THEN ONCE_REWRITE_TAC[GSYM PAIR] 497 THEN CONV_TAC (DEPTH_CONV let_CONV) 498 THEN ASM_REWRITE_TAC[] 499 ); 500 501val BV_vsubst1 = store_thm 502 ("BV_vsubst1", 503 ���!xs ys. (LENGTH xs = LENGTH ys) ==> 504 (BV_subst ((xs // ys) :^subs) = SL xs)���, 505 LIST_INDUCT_TAC 506 THEN REWRITE_TAC[BV_subst_def,vsubst1,SL] 507 THEN GEN_TAC 508 THEN LIST_INDUCT_TAC 509 THEN REWRITE_TAC[LENGTH,NOT_SUC,INV_SUC_EQ] 510 THEN POP_TAC 511 THEN REPEAT STRIP_TAC 512 THEN RES_TAC 513 THEN ASM_REWRITE_TAC[BV_subst_def,vsubst1,FST] 514 ); 515 516val HEIGHT1_SUB1_var = store_thm 517 ("HEIGHT1_SUB1_var", 518 ���!xs ys v. 519 HEIGHT_obj1 (SUB1 ((xs // ys):^subs) v) = 0���, 520 Induct 521 THENL [ ALL_TAC, GEN_TAC ] 522 THEN Cases 523 THEN REPEAT GEN_TAC 524 THEN ASM_REWRITE_TAC[vsubst1,SUB1,HEIGHT1_def] 525 THEN COND_CASES_TAC 526 THEN ASM_REWRITE_TAC[HEIGHT1_def] 527 ); 528 529val HEIGHT1_var_list_subst = store_thm 530 ("HEIGHT1_var_list_subst", 531 ���(!t:^obj xs ys. 532 HEIGHT_obj1 (t <[ (xs // ys)) = HEIGHT_obj1 t) /\ 533 (!t:^dict xs ys. 534 HEIGHT_dict1 (t <[ (xs // ys)) = HEIGHT_dict1 t) /\ 535 (!t:^entry xs ys. 536 HEIGHT_entry1 (t <[ (xs // ys)) = HEIGHT_entry1 t) /\ 537 (!t:^method xs ys. 538 HEIGHT_method1 (t <[ (xs // ys)) = HEIGHT_method1 t)���, 539 Induct 540 THEN REPEAT GEN_TAC 541 THEN ASM_REWRITE_TAC[SUB_object1_def,SUB1,HEIGHT1_def] 542 THENL 543 [ REWRITE_TAC[HEIGHT1_SUB1_var], 544 545 CONV_TAC (DEPTH_CONV let_CONV) 546 THEN ONCE_REWRITE_TAC[GSYM vsubst1] 547 THEN ASM_REWRITE_TAC[HEIGHT1_def] 548 ] 549 ); 550 551val HEIGHT1_var_subst = store_thm 552 ("HEIGHT1_var_subst", 553 ���(!t:^obj x y. 554 HEIGHT_obj1 (t <[ [x, OVAR1 y]) = HEIGHT_obj1 t) /\ 555 (!t:^dict x y. 556 HEIGHT_dict1 (t <[ [x, OVAR1 y]) = HEIGHT_dict1 t) /\ 557 (!t:^entry x y. 558 HEIGHT_entry1 (t <[ [x, OVAR1 y]) = HEIGHT_entry1 t) /\ 559 (!t:^method x y. 560 HEIGHT_method1 (t <[ [x, OVAR1 y]) = HEIGHT_method1 t)���, 561 REWRITE_TAC[GSYM vsubst1] 562 THEN REWRITE_TAC[HEIGHT1_var_list_subst] 563 ); 564 565 566val object1_distinct' = store_thm 567 ("object1_distinct'", 568 ���((!x d. ~(ALPHA_obj (OVAR1 x) (OBJ1 d : ^obj))) /\ 569 (!x a l. ~(ALPHA_obj (OVAR1 x) (INVOKE1 a l : ^obj))) /\ 570 (!x a l m. ~(ALPHA_obj (OVAR1 x) (UPDATE1 a l m : ^obj))) /\ 571 (!d a l. ~(ALPHA_obj (OBJ1 d) (INVOKE1 a l : ^obj))) /\ 572 (!d a l m. ~(ALPHA_obj (OBJ1 d) (UPDATE1 a l m : ^obj))) /\ 573 (!a l b s m. ~(ALPHA_obj (INVOKE1 a l) (UPDATE1 b s m : ^obj))) /\ 574 (!d x. ~(ALPHA_obj (OBJ1 d) (OVAR1 x : ^obj))) /\ 575 (!a l x. ~(ALPHA_obj (INVOKE1 a l) (OVAR1 x : ^obj))) /\ 576 (!a l m x. ~(ALPHA_obj (UPDATE1 a l m) (OVAR1 x : ^obj))) /\ 577 (!a l d. ~(ALPHA_obj (INVOKE1 a l) (OBJ1 d : ^obj))) /\ 578 (!a l m d. ~(ALPHA_obj (UPDATE1 a l m) (OBJ1 d : ^obj))) /\ 579 (!a l m b s. ~(ALPHA_obj (UPDATE1 a l m) (INVOKE1 b s : ^obj)))) 580 ���, 581 REWRITE_TAC[ALPHA_object,ALPHA1_object_neg] 582 ); 583 584 585val object1_cases' = store_thm 586 ("object1_cases'", 587 ���(!a:^obj. (?x. ALPHA_obj a (OVAR1 x)) \/ 588 (?d. ALPHA_obj a (OBJ1 d)) \/ 589 (?b l. ALPHA_obj a (INVOKE1 b l)) \/ 590 (?b l m. ALPHA_obj a (UPDATE1 b l m))) /\ 591 (!d. (?e d'. ALPHA_dict d (e::d')) \/ 592 (ALPHA_dict d [])) /\ 593 (!e. (?l m. ALPHA_entry e (l,m))) /\ 594 (!m. (?x a. ALPHA_method m (SIGMA1 x a)))���, 595 REPEAT STRIP_TAC 596 THENL (map (STRIP_ASSUME_TAC o SPEC_ALL) (CONJUNCTS object1_cases)) 597 THEN PROVE_TAC[ALPHA_object_pos,ALPHA_REFL] 598 ); 599 600 601val object1_one_one' = store_thm 602 ("object1_one_one'", 603 ���(!a a'. ALPHA_obj (OVAR1 a) (OVAR1 a') = (a = a')) /\ 604 (!a a'. ALPHA_obj (OBJ1 a) (OBJ1 a') = ALPHA_dict a a') /\ 605 (!a0 a1 a0' a1'. 606 ALPHA_obj (INVOKE1 a0 a1) (INVOKE1 a0' a1') = 607 ALPHA_obj a0 a0' /\ (a1 = a1')) /\ 608 (!a0 a1 a2 a0' a1' a2'. 609 ALPHA_obj (UPDATE1 a0 a1 a2) (UPDATE1 a0' a1' a2') = 610 ALPHA_obj a0 a0' /\ (a1 = a1') /\ ALPHA_method a2 a2') /\ 611 (!a0 a1 a0' a1'. ALPHA_dict (a0::a1) (a0'::a1') = 612 ALPHA_entry a0 a0' /\ ALPHA_dict a1 a1') /\ 613 (!a0 a1 a0' a1'. ALPHA_entry (a0,a1) (a0',a1') = 614 (a0 = a0') /\ ALPHA_method a1 a1') /\ 615 (!a0 a1 a1'. ALPHA_method (SIGMA1 a0 a1) (SIGMA1 a0 a1') = 616 ALPHA_obj a1 a1')���, 617 REWRITE_TAC[ALPHA_object_pos,ALPHA_method_one_one,subst_SAME_ONE1] 618 ); 619 620 621(* AXIOM 3 *) 622 623(* Melham and Gordon's third axiom, on alpha-equivalence. *) 624 625val CHANGE_ONE_VAR1 = store_thm 626 ("CHANGE_ONE_VAR1", 627 ���!x v t. 628 ~(x IN FV_method1 (SIGMA1 v t)) ==> 629 ALPHA_method (SIGMA1 v t) (SIGMA1 x (t <[ [(v, OVAR1 x)]))���, 630 REWRITE_TAC[FV_object1_def] 631 THEN REPEAT STRIP_TAC 632 THEN IMP_RES_TAC ALPHA_CHANGE_ONE_VAR 633 THEN ONCE_REWRITE_TAC[ALPHA_SYM] 634 THEN ASM_REWRITE_TAC[] 635 ); 636 637 638 639 640(* ------------------------------------------------------------------- *) 641(* We now begin the development that leads to the lifting of *) 642(* the "function existance" theorem for the lambda calculus. *) 643(* This is AXIOM 4 for Gordon and Melham in "Five Axioms" paper. *) 644(* They proved their axiom from an underlying deBruijn representa- *) 645(* tion, but to my knowledge this has never been proven for a name- *) 646(* carrying syntax at the lower level like this before, and has *) 647(* never been automatically lifted to the higher, abstract level. *) 648(* *) 649(* Most of this is to express this theorem at the lower level as: *) 650(* *) 651(* !(var : var->'a) obj inv upd cns nil par sgm. *) 652(* ?!ho :: respects(ALPHA_obj,$=). *) 653(* ?!hd :: respects(ALPHA_dict,$=). *) 654(* ?!he :: respects(ALPHA_entry,$=). *) 655(* ?!hm :: respects(ALPHA_method,$=). *) 656(* (!x. ho (OVAR1 x) = var x) /\ *) 657(* (!d. ho (OBJ1 d) = obj (hd d)) /\ *) 658(* (!a l. ho (INVOKE1 a l) = inv (ho a) l) /\ *) 659(* (!a l m. ho (UPDATE1 a l m) = upd (ho a) l (hm m)) /\ *) 660(* (!e d. hd (e::d) = cns (he e) (hd d)) /\ *) 661(* ( hd [] = nil) /\ *) 662(* (!l m. he (l,m) = par l (hm m)) /\ *) 663(* (!x a. hm (SIGMA1 x a) = sgm (\y. ho (a <[ [x, OVAR1 y]))) *) 664(* *) 665(* ------------------------------------------------------------------- *) 666 667(* 668val term1_hom_def = 669 Hol_defn "term1_hom" 670 `(term1_hom con var app abs (Con1 a :^term) = (con a):'b) /\ 671 (term1_hom con var app abs (Var1 x) = (var x)) /\ 672 (term1_hom con var app abs (App1 t u) = 673 app (term1_hom con var app abs t) 674 (term1_hom con var app abs u) t u) /\ 675 (term1_hom con var app abs (Lam1 x u) = 676 abs (\y. term1_hom con var app abs 677 (u <[ [x, Var1 y])) 678 (\y. u <[ [x, Var1 y]))`; 679*) 680 681val object1_hom_def = 682 Hol_defn "object1_hom" 683 `(hom_o (OVAR1 x) var obj nvk upd cns nil par sgm = (var x):'a) /\ 684 (hom_o (OBJ1 d) var obj nvk upd cns nil par sgm = 685 obj (hom_d d var obj nvk upd cns nil par sgm) d) /\ 686 (hom_o (INVOKE1 a l) var obj nvk upd cns nil par sgm = 687 nvk (hom_o a var obj nvk upd cns nil par sgm) a l) /\ 688 (hom_o (UPDATE1 a l m) var obj nvk upd cns nil par sgm = 689 upd (hom_o a var obj nvk upd cns nil par sgm) 690 (hom_m m var obj nvk upd cns nil par sgm) a l m) /\ 691 (hom_d (e::d) var obj nvk upd cns nil par sgm = 692 cns (hom_e e var obj nvk upd cns nil par sgm) 693 (hom_d d var obj nvk upd cns nil par sgm) e d) /\ 694 (hom_d ([]) var obj nvk upd cns nil par sgm = nil:'b) /\ 695 (hom_e (l,m) var obj nvk upd cns nil par sgm = 696 (par (hom_m m var obj nvk upd cns nil par sgm) l m):'c) /\ 697 (hom_m (SIGMA1 x a) var obj nvk upd cns nil par sgm = 698 (sgm (\y. hom_o (a <[ [x, OVAR1 y]) var obj nvk upd cns nil par sgm) 699 (\y. a <[ [x, OVAR1 y]) 700 :'d))`; 701 702val _ = set_fixity "+-+" (Infixr 490); 703 704val SUMVAL_def = xDefine "SUM_VAL" 705 `(($+-+ f g) (INL (x:'a)) = ((f x):'c)) /\ 706 (($+-+ f g) (INR (y:'b)) = ((g y):'c))`; 707 708val PBETA_TAC = PairRules.PBETA_TAC 709val PGEN_TAC = PairRules.PGEN_TAC 710 711(* 712Defn.tgoal object1_hom_def; 713e(WF_REL_TAC `measure ( 714 HEIGHT_obj1 o FST 715 +-+ HEIGHT_dict1 o FST 716 +-+ HEIGHT_entry1 o FST 717 +-+ HEIGHT_method1 o FST)`); 718e(REPEAT CONJ_TAC); 719(* 8 subgoals *) 720 721 e(REWRITE_TAC[SUMVAL_def]); 722 e(PBETA_TAC); 723 e(REWRITE_TAC[HEIGHT1_def]); 724 e(REPEAT GEN_TAC); 725 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 726 e(REWRITE_TAC[LESS_EQ_REFL]); 727 728 e(REWRITE_TAC[SUMVAL_def]); 729 e(PBETA_TAC); 730 e(REWRITE_TAC[HEIGHT1_def,HEIGHT1_var_subst]); 731 e(REPEAT GEN_TAC); 732 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 733 e(REWRITE_TAC[LESS_EQ_REFL]); 734 735 e(REWRITE_TAC[SUMVAL_def]); 736 e(PBETA_TAC); 737 e(REWRITE_TAC[HEIGHT1_def]); 738 e(REPEAT GEN_TAC); 739 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 740 e(REWRITE_TAC[LESS_EQ_MAX]); 741 742 e(REWRITE_TAC[SUMVAL_def]); 743 e(PBETA_TAC); 744 e(REWRITE_TAC[HEIGHT1_def]); 745 e(REPEAT GEN_TAC); 746 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 747 e(REWRITE_TAC[LESS_EQ_MAX]); 748 749 e(REWRITE_TAC[SUMVAL_def]); 750 e(PBETA_TAC); 751 e(REWRITE_TAC[HEIGHT1_def]); 752 e(REPEAT PGEN_TAC); 753 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 754 e(REWRITE_TAC[LESS_EQ_MAX]); 755 756 e(REWRITE_TAC[SUMVAL_def]); 757 e(PBETA_TAC); 758 e(REWRITE_TAC[HEIGHT1_def]); 759 e(REPEAT GEN_TAC); 760 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 761 e(REWRITE_TAC[LESS_EQ_REFL]); 762 763 e(REWRITE_TAC[SUMVAL_def]); 764 e(PBETA_TAC); 765 e(REWRITE_TAC[HEIGHT1_def]); 766 e(REPEAT GEN_TAC); 767 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 768 e(REWRITE_TAC[LESS_EQ_REFL]); 769 770 e(REWRITE_TAC[SUMVAL_def]); 771 e(PBETA_TAC); 772 e(REWRITE_TAC[HEIGHT1_def]); 773 e(REPEAT GEN_TAC); 774 e(MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC); 775 e(REWRITE_TAC[LESS_EQ_MAX]); 776*) 777 778val (object1_hom_eqns, object1_hom_ind) = 779 Defn.tprove 780 (object1_hom_def, 781 WF_REL_TAC `measure ( 782 HEIGHT_obj1 o FST 783 +-+ HEIGHT_dict1 o FST 784 +-+ HEIGHT_entry1 o FST 785 +-+ HEIGHT_method1 o FST)` 786 THEN REWRITE_TAC[SUMVAL_def] 787 THEN PBETA_TAC 788 THEN REWRITE_TAC[HEIGHT1_var_subst] 789 THEN REWRITE_TAC[HEIGHT1_def] 790 THEN REPEAT CONJ_TAC 791 THEN REPEAT PGEN_TAC 792 THEN MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC 793 THEN REWRITE_TAC[LESS_EQ_MAX,LESS_EQ_REFL] 794 ); 795 796 797 798val object1_hom_RSP_LEMMA = TAC_PROOF(([], 799 ���!(var :var -> 'a) obj nvk upd cns (nil:'b) 800 (par:'d -> string -> method1 -> 'c) sgm. 801 respects($= ===> ALPHA_dict ===> $=) obj /\ 802 respects($= ===> ALPHA_obj ===> $= ===> $=) nvk /\ 803 respects($= ===> $= ===> ALPHA_obj ===> $= ===> ALPHA_method ===> $=) 804 upd /\ 805 respects($= ===> $= ===> ALPHA_entry ===> ALPHA_dict ===> $=) cns /\ 806 respects($= ===> $= ===> ALPHA_method ===> $=) par /\ 807 respects($= ===> ($= ===> ALPHA_obj) ===> $=) sgm ==> 808 !n. 809 (!t:^obj u. (HEIGHT_obj1 t <= n) /\ ALPHA_obj t u ==> 810 (hom_o t var obj nvk upd cns nil par sgm = 811 hom_o u var obj nvk upd cns nil par sgm)) /\ 812 (!t:^dict u. (HEIGHT_dict1 t <= n) /\ ALPHA_dict t u ==> 813 (hom_d t var obj nvk upd cns nil par sgm = 814 hom_d u var obj nvk upd cns nil par sgm)) /\ 815 (!t:^entry u. (HEIGHT_entry1 t <= n) /\ ALPHA_entry t u ==> 816 (hom_e t var obj nvk upd cns nil par sgm = 817 hom_e u var obj nvk upd cns nil par sgm)) /\ 818 (!t:^method u. (HEIGHT_method1 t <= n) /\ ALPHA_method t u ==> 819 (hom_m t var obj nvk upd cns nil par sgm = 820 hom_m u var obj nvk upd cns nil par sgm))���), 821 REPEAT GEN_TAC 822 THEN REWRITE_TAC[RESPECTS,FUN_REL] 823 THEN CONV_TAC (RATOR_CONV (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 824 THEN REWRITE_TAC[AND_IMP_INTRO,GSYM CONJ_ASSOC] 825 THEN STRIP_TAC 826 THEN INDUCT_TAC (* two subgoals *) 827 THENL [ ALL_TAC, POP_ASSUM STRIP_ASSUME_TAC ] 828 THEN REPEAT CONJ_TAC (* 8 subgoals *) 829 THEN Cases THEN Cases (* 44 subgoals *) 830 THEN REWRITE_TAC[HEIGHT1_def,LESS_EQ_0,NOT_SUC,SUC_NOT] 831 THEN REWRITE_TAC[ALPHA_object_neg] 832 THEN REWRITE_TAC[ALPHA_object_pos] 833 THEN REWRITE_TAC[INV_SUC_EQ,LESS_EQ_MONO,MAX_LESS_EQ] 834 THEN REWRITE_TAC[ZERO_LESS_EQ] 835 THEN REWRITE_TAC[object1_hom_eqns] 836 THEN REPEAT STRIP_TAC 837 THEN ASM_REWRITE_TAC[] (* 6 subgoals *) 838 THEN TRY (FIRST_ASSUM MATCH_MP_TAC 839 THEN ASM_REWRITE_TAC[] 840 THEN REPEAT CONJ_TAC 841 THEN FIRST_ASSUM MATCH_MP_TAC 842 THEN ASM_REWRITE_TAC[] 843 THEN NO_TAC) 844 THEN FIRST_ASSUM MATCH_MP_TAC 845 THEN CONJ_TAC 846 THENL 847 [ CONV_TAC FUN_EQ_CONV 848 THEN GEN_TAC 849 THEN BETA_TAC 850 THEN FIRST_ASSUM MATCH_MP_TAC 851 THEN ASM_REWRITE_TAC[HEIGHT1_var_subst] 852 THEN MATCH_MP_TAC ALPHA_SIGMA_subst 853 THEN FIRST_ASSUM ACCEPT_TAC, 854 855 REPEAT GEN_TAC 856 THEN DISCH_THEN REWRITE_THM 857 THEN BETA_TAC 858 THEN MATCH_MP_TAC ALPHA_SIGMA_subst 859 THEN FIRST_ASSUM ACCEPT_TAC 860 ] 861 ); 862 863 864val object1_hom_RSP = TAC_PROOF(([], 865 ���!(var :var -> 'a) obj nvk upd cns (nil:'b) 866 (par:'d -> string -> method1 -> 'c) sgm. 867 respects($= ===> ALPHA_dict ===> $=) obj /\ 868 respects($= ===> ALPHA_obj ===> $= ===> $=) nvk /\ 869 respects($= ===> $= ===> ALPHA_obj ===> $= ===> ALPHA_method ===> $=) 870 upd /\ 871 respects($= ===> $= ===> ALPHA_entry ===> ALPHA_dict ===> $=) cns /\ 872 respects($= ===> $= ===> ALPHA_method ===> $=) par /\ 873 respects($= ===> ($= ===> ALPHA_obj) ===> $=) sgm ==> 874 respects(ALPHA_obj ===> $=) 875 (\a. hom_o a var obj nvk upd cns nil par sgm) /\ 876 respects(ALPHA_dict ===> $=) 877 (\d. hom_d d var obj nvk upd cns nil par sgm) /\ 878 respects(ALPHA_entry ===> $=) 879 (\e. hom_e e var obj nvk upd cns nil par sgm) /\ 880 respects(ALPHA_method ===> $=) 881 (\m. hom_m m var obj nvk upd cns nil par sgm)���), 882 REPEAT GEN_TAC 883 THEN DISCH_TAC 884 THEN REWRITE_TAC[RESPECTS,FUN_REL] 885 THEN MP_TAC (SPEC_ALL object1_hom_RSP_LEMMA) 886 THEN ASM_REWRITE_TAC[] 887 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 888 THEN REPEAT STRIP_TAC 889 THEN BETA_TAC 890 THEN FIRST_ASSUM MATCH_MP_TAC 891 THEN PROVE_TAC[LESS_EQ_REFL] 892 ); 893 894 895 896val RESPECTS_PAIR_REL = store_thm( 897 "RESPECTS_PAIR_REL", 898 ���!R1 R2 (a:'a) (b:'b). 899 respects (R1 ### R2) (a,b) = 900 respects R1 a /\ respects R2 b���, 901 REPEAT GEN_TAC 902 THEN REWRITE_TAC[RESPECTS,PAIR_REL_THM] 903 ); 904 905val object1_respects_Axiom_exists = store_thm( 906 "object1_respects_Axiom_exists", 907 ���!(var :var -> 'a) obj nvk upd cns (nil:'b) 908 (par:'d -> string -> method1 -> 'c) sgm. 909 respects($= ===> ALPHA_dict ===> $=) obj /\ 910 respects($= ===> ALPHA_obj ===> $= ===> $=) nvk /\ 911 respects($= ===> $= ===> ALPHA_obj ===> $= ===> ALPHA_method ===> $=) 912 upd /\ 913 respects($= ===> $= ===> ALPHA_entry ===> ALPHA_dict ===> $=) cns /\ 914 respects($= ===> $= ===> ALPHA_method ===> $=) par /\ 915 respects($= ===> ($= ===> ALPHA_obj) ===> $=) sgm ==> 916 ?(hom_o, hom_d, hom_e, hom_m) 917 :: respects((ALPHA_obj ===> $=) ### 918 (ALPHA_dict ===> $=) ### 919 (ALPHA_entry ===> $=) ### 920 (ALPHA_method ===> $=)). 921 (!x. hom_o (OVAR1 x) = var x) /\ 922 (!d. hom_o (OBJ1 d) = obj (hom_d d) d) /\ 923 (!a l. hom_o (INVOKE1 a l) = nvk (hom_o a) a l) /\ 924 (!a l m. hom_o (UPDATE1 a l m) = upd (hom_o a) (hom_m m) a l m) /\ 925 (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d) e d) /\ 926 ( hom_d ([]) = nil) /\ 927 (!l m. hom_e (l,m) = (par (hom_m m) l m):'c) /\ 928 (!x a. hom_m (SIGMA1 x a) = 929 ((sgm (\y. hom_o (a <[ [x, OVAR1 y])) 930 (\y. a <[ [x, OVAR1 y]) )):'d)���, 931 REPEAT GEN_TAC 932 THEN DISCH_THEN (STRIP_ASSUME_TAC o SPEC_ALL o MATCH_MP object1_hom_RSP) 933 THEN CONV_TAC (DEPTH_CONV res_quanLib.RES_EXISTS_CONV) 934 THEN EXISTS_TAC 935 ���((\t:^obj. hom_o t (var:var->'a) obj nvk upd cns 936 (nil:'b) (par:'d->string->method1->'c) sgm), 937 (\t:^dict. hom_d t var obj nvk upd cns nil par sgm), 938 (\t:^entry. hom_e t var obj nvk upd cns nil par sgm), 939 (\t:^method. hom_m t var obj nvk upd cns nil par sgm))��� 940 THEN REWRITE_TAC[SPECIFICATION] 941 THEN REWRITE_TAC[RESPECTS_PAIR_REL] 942 THEN ASM_REWRITE_TAC[] 943 THEN PairRules.PBETA_TAC 944 THEN BETA_TAC 945 THEN REWRITE_TAC[object1_hom_eqns] 946 ); 947 948 949val object1_respects_Axiom_11_LEMMA = TAC_PROOF(([], 950 ���!hom_o1 hom_o2 hom_d1 hom_d2 hom_e1 hom_e2 hom_m1 hom_m2 951 (var :var -> 'a) obj nvk upd cns (nil:'b) 952 (par:'d -> string -> method1 -> 'c) sgm. 953 hom_o1 IN respects (ALPHA_obj ===> $=) /\ 954 hom_o2 IN respects (ALPHA_obj ===> $=) /\ 955 hom_d1 IN respects (ALPHA_dict ===> $=) /\ 956 hom_d2 IN respects (ALPHA_dict ===> $=) /\ 957 hom_e1 IN respects (ALPHA_entry ===> $=) /\ 958 hom_e2 IN respects (ALPHA_entry ===> $=) /\ 959 hom_m1 IN respects (ALPHA_method ===> $=) /\ 960 hom_m2 IN respects (ALPHA_method ===> $=) /\ 961 ((!x. hom_o1 (OVAR1 x) = var x) /\ 962 (!d. hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\ 963 (!a l. hom_o1 (INVOKE1 a l) = nvk (hom_o1 a) a l) /\ 964 (!a l m. hom_o1 (UPDATE1 a l m) = upd (hom_o1 a)(hom_m1 m)a l m) /\ 965 (!e d. hom_d1 (e::d) = cns (hom_e1 e) (hom_d1 d) e d) /\ 966 ( hom_d1 ([]) = nil) /\ 967 (!l m. hom_e1 (l,m) = (par (hom_m1 m) l m):'c) /\ 968 (!x a. hom_m1 (SIGMA1 x a) = 969 ((sgm (\y. hom_o1 (a <[ [x, OVAR1 y])) 970 (\y. a <[ [x, OVAR1 y]))):'d)) /\ 971 ((!x. hom_o2 (OVAR1 x) = var x) /\ 972 (!d. hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\ 973 (!a l. hom_o2 (INVOKE1 a l) = nvk (hom_o2 a) a l) /\ 974 (!a l m. hom_o2 (UPDATE1 a l m) = upd (hom_o2 a)(hom_m2 m)a l m) /\ 975 (!e d. hom_d2 (e::d) = cns (hom_e2 e) (hom_d2 d) e d) /\ 976 ( hom_d2 ([]) = nil) /\ 977 (!l m. hom_e2 (l,m) = (par (hom_m2 m) l m):'c) /\ 978 (!x a. hom_m2 (SIGMA1 x a) = 979 ((sgm (\y. hom_o2 (a <[ [x, OVAR1 y])) 980 (\y. a <[ [x, OVAR1 y]))):'d)) 981 ==> 982 (!n. (!t. (HEIGHT_obj1 t <= n) ==> (hom_o1 t = hom_o2 t)) /\ 983 (!t. (HEIGHT_dict1 t <= n) ==> (hom_d1 t = hom_d2 t)) /\ 984 (!t. (HEIGHT_entry1 t <= n) ==> (hom_e1 t = hom_e2 t)) /\ 985 (!t. (HEIGHT_method1 t <= n) ==> (hom_m1 t = hom_m2 t)))���), 986 REWRITE_TAC[SPECIFICATION,RESPECTS_THM] 987 THEN REPEAT GEN_TAC 988 THEN STRIP_TAC 989 THEN Induct 990 THENL [ ALL_TAC, POP_ASSUM STRIP_ASSUME_TAC ] 991 THEN REPEAT CONJ_TAC 992 THEN Cases (* 16 subgoals *) 993 THEN REWRITE_TAC[HEIGHT1_def,LESS_EQ_0,NOT_SUC] 994 THEN REWRITE_TAC[LESS_EQ_MONO,MAX_LESS_EQ] 995 THEN REWRITE_TAC[ZERO_LESS_EQ] 996 THEN ASM_REWRITE_TAC[] (* 6 subgoals *) 997 THEN STRIP_TAC 998 THEN TRY (RES_TAC 999 THEN ASM_REWRITE_TAC[] 1000 THEN NO_TAC) 1001 THEN AP_THM_TAC 1002 THEN AP_TERM_TAC 1003 THEN CONV_TAC FUN_EQ_CONV 1004 THEN GEN_TAC 1005 THEN BETA_TAC 1006 THEN FIRST_ASSUM MATCH_MP_TAC 1007 THEN ASM_REWRITE_TAC[HEIGHT1_var_subst] 1008 ); 1009 1010val object1_respects_Axiom_11_LEMMA2 = TAC_PROOF(([], 1011 ���!hom_o1 hom_o2 hom_d1 hom_d2 hom_e1 hom_e2 hom_m1 hom_m2 1012 (var :var -> 'a) obj nvk upd cns (nil:'b) 1013 (par:'d -> string -> method1 -> 'c) sgm. 1014 hom_o1 IN respects (ALPHA_obj ===> $=) /\ 1015 hom_o2 IN respects (ALPHA_obj ===> $=) /\ 1016 hom_d1 IN respects (ALPHA_dict ===> $=) /\ 1017 hom_d2 IN respects (ALPHA_dict ===> $=) /\ 1018 hom_e1 IN respects (ALPHA_entry ===> $=) /\ 1019 hom_e2 IN respects (ALPHA_entry ===> $=) /\ 1020 hom_m1 IN respects (ALPHA_method ===> $=) /\ 1021 hom_m2 IN respects (ALPHA_method ===> $=) /\ 1022 ((!x. hom_o1 (OVAR1 x) = var x) /\ 1023 (!d. hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\ 1024 (!a l. hom_o1 (INVOKE1 a l) = nvk (hom_o1 a) a l) /\ 1025 (!a l m. hom_o1 (UPDATE1 a l m) = upd (hom_o1 a)(hom_m1 m)a l m) /\ 1026 (!e d. hom_d1 (e::d) = cns (hom_e1 e) (hom_d1 d) e d) /\ 1027 ( hom_d1 ([]) = nil) /\ 1028 (!l m. hom_e1 (l,m) = (par (hom_m1 m) l m):'c) /\ 1029 (!x a. hom_m1 (SIGMA1 x a) = 1030 ((sgm (\y. hom_o1 (a <[ [x, OVAR1 y])) 1031 (\y. a <[ [x, OVAR1 y]))):'d)) /\ 1032 ((!x. hom_o2 (OVAR1 x) = var x) /\ 1033 (!d. hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\ 1034 (!a l. hom_o2 (INVOKE1 a l) = nvk (hom_o2 a) a l) /\ 1035 (!a l m. hom_o2 (UPDATE1 a l m) = upd (hom_o2 a)(hom_m2 m)a l m) /\ 1036 (!e d. hom_d2 (e::d) = cns (hom_e2 e) (hom_d2 d) e d) /\ 1037 ( hom_d2 ([]) = nil) /\ 1038 (!l m. hom_e2 (l,m) = (par (hom_m2 m) l m):'c) /\ 1039 (!x a. hom_m2 (SIGMA1 x a) = 1040 ((sgm (\y. hom_o2 (a <[ [x, OVAR1 y])) 1041 (\y. a <[ [x, OVAR1 y]))):'d)) 1042 ==> 1043 (hom_o1 = hom_o2) /\ 1044 (hom_d1 = hom_d2) /\ 1045 (hom_e1 = hom_e2) /\ 1046 (hom_m1 = hom_m2)���), 1047 REPEAT GEN_TAC 1048 THEN DISCH_THEN (STRIP_ASSUME_TAC o 1049 MATCH_MP object1_respects_Axiom_11_LEMMA) 1050 THEN POP_ASSUM (STRIP_ASSUME_TAC o 1051 CONV_RULE (TOP_DEPTH_CONV FORALL_AND_CONV)) 1052 THEN REPEAT CONJ_TAC 1053 THEN CONV_TAC FUN_EQ_CONV 1054 THEN GEN_TAC 1055 THEN FIRST_ASSUM MATCH_MP_TAC 1056 THEN PROVE_TAC[LESS_EQ_REFL] 1057 ); 1058 1059val object1_respects_Axiom_11 = store_thm( 1060 "object1_respects_Axiom_11", 1061 ���!(var :var -> 'a) obj nvk upd cns (nil:'b) 1062 (par:'d -> string -> method1 -> 'c) sgm. 1063 !(hom_o1, hom_d1, hom_e1, hom_m1) :: 1064 respects((ALPHA_obj ===> $=) ### 1065 (ALPHA_dict ===> $=) ### 1066 (ALPHA_entry ===> $=) ### 1067 (ALPHA_method ===> $=)) . 1068 !(hom_o2, hom_d2, hom_e2, hom_m2) :: 1069 respects((ALPHA_obj ===> $=) ### 1070 (ALPHA_dict ===> $=) ### 1071 (ALPHA_entry ===> $=) ### 1072 (ALPHA_method ===> $=)) . 1073 ((!x. hom_o1 (OVAR1 x) = var x) /\ 1074 (!d. hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\ 1075 (!a l. hom_o1 (INVOKE1 a l) = nvk (hom_o1 a) a l) /\ 1076 (!a l m. hom_o1 (UPDATE1 a l m) = upd (hom_o1 a)(hom_m1 m)a l m) /\ 1077 (!e d. hom_d1 (e::d) = cns (hom_e1 e) (hom_d1 d) e d) /\ 1078 ( hom_d1 ([]) = nil) /\ 1079 (!l m. hom_e1 (l,m) = (par (hom_m1 m) l m):'c) /\ 1080 (!x a. hom_m1 (SIGMA1 x a) = 1081 ((sgm (\y. hom_o1 (a <[ [x, OVAR1 y])) 1082 (\y. a <[ [x, OVAR1 y]))):'d)) /\ 1083 ((!x. hom_o2 (OVAR1 x) = var x) /\ 1084 (!d. hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\ 1085 (!a l. hom_o2 (INVOKE1 a l) = nvk (hom_o2 a) a l) /\ 1086 (!a l m. hom_o2 (UPDATE1 a l m) = upd (hom_o2 a)(hom_m2 m)a l m) /\ 1087 (!e d. hom_d2 (e::d) = cns (hom_e2 e) (hom_d2 d) e d) /\ 1088 ( hom_d2 ([]) = nil) /\ 1089 (!l m. hom_e2 (l,m) = (par (hom_m2 m) l m):'c) /\ 1090 (!x a. hom_m2 (SIGMA1 x a) = 1091 ((sgm (\y. hom_o2 (a <[ [x, OVAR1 y])) 1092 (\y. a <[ [x, OVAR1 y]))):'d)) 1093 ==> 1094 (hom_o1 = hom_o2) /\ 1095 (hom_d1 = hom_d2) /\ 1096 (hom_e1 = hom_e2) /\ 1097 (hom_m1 = hom_m2)���, 1098 REPEAT GEN_TAC 1099 THEN REPEAT res_quanLib.RESQ_GEN_TAC 1100 THEN PairRules.PBETA_TAC 1101 THEN REPEAT res_quanLib.RESQ_GEN_TAC 1102 THEN PairRules.PBETA_TAC 1103 THEN STRIP_TAC 1104 THEN MATCH_MP_TAC (SPEC_ALL object1_respects_Axiom_11_LEMMA2) 1105 THEN ASM_REWRITE_TAC[] 1106 THEN UNDISCH_ALL_TAC 1107 THEN DISCH_THEN (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1108 THEN DISCH_THEN (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1109 THEN UNDISCH_ALL_TAC 1110 THEN PURE_REWRITE_TAC[SPECIFICATION,RESPECTS_PAIR_REL] 1111 THEN STRIP_TAC 1112 THEN POP_ASSUM (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1113 THEN STRIP_TAC 1114 THEN POP_ASSUM (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1115 THEN UNDISCH_ALL_TAC 1116 THEN PURE_REWRITE_TAC[SPECIFICATION,RESPECTS_PAIR_REL] 1117 THEN STRIP_TAC 1118 THEN STRIP_TAC 1119 THEN POP_ASSUM (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1120 THEN STRIP_TAC 1121 THEN STRIP_TAC 1122 THEN POP_ASSUM (ASSUME_TAC o PURE_ONCE_REWRITE_RULE [GSYM PAIR]) 1123 THEN UNDISCH_ALL_TAC 1124 THEN PURE_REWRITE_TAC[SPECIFICATION,RESPECTS_PAIR_REL] 1125 THEN REPEAT STRIP_TAC 1126 THEN ASM_REWRITE_TAC[] 1127 ); 1128 1129 1130 1131fun PAIR_LAMBDA_CONV abs = 1132 let val {Bvar=x, Body=body} = dest_abs abs 1133 val {Name, Ty} = dest_var x 1134 val tys = strip_prod Ty 1135 val free = free_vars abs 1136 val xs = foldl (fn (ty,vrs) => 1137 vrs @ [prim_variant (vrs @ free) 1138 (mk_var{Name=Name, Ty=ty})]) [] tys 1139 val p = list_mk_pair xs 1140 val body' = beta_conv (mk_comb{Rator=abs, Rand=p}) 1141 val abs' = mk_pabs(p, body') 1142 val eq_tm = mk_eq{lhs=abs, rhs=abs'} 1143 val th = TAC_PROOF(([],eq_tm), 1144 CONV_TAC FUN_EQ_CONV 1145 THEN PairRules.PBETA_TAC 1146 THEN GEN_TAC 1147 THEN REFL_TAC) 1148 in th end; 1149 1150fun CHECK_RATOR_NAME_CONV nm tm = 1151 let val {Rator, Rand} = dest_comb tm 1152 val _ = assert (curry op = nm o #Name o dest_const) Rator 1153 in 1154 REFL tm 1155 end; 1156 1157val PAIR_EXISTS_CONV = CHECK_RATOR_NAME_CONV "?" 1158 THENC RAND_CONV PAIR_LAMBDA_CONV; 1159 1160val PAIR_FORALL_CONV = CHECK_RATOR_NAME_CONV "!" 1161 THENC RAND_CONV PAIR_LAMBDA_CONV; 1162 1163val PAIR_RES_EXISTS_CONV = RATOR_CONV (CHECK_RATOR_NAME_CONV "RES_EXISTS") 1164 THENC RAND_CONV PAIR_LAMBDA_CONV; 1165 1166val PAIR_RES_FORALL_CONV = RATOR_CONV (CHECK_RATOR_NAME_CONV "RES_FORALL") 1167 THENC RAND_CONV PAIR_LAMBDA_CONV; 1168 1169 1170 1171val object1_respects_Axiom = store_thm( 1172 "object1_respects_Axiom", 1173 ���!(var :var -> 'a) 1174 (obj :: respects($= ===> ALPHA_dict ===> $=)) 1175 (nvk :: respects($= ===> ALPHA_obj ===> $= ===> $=)) 1176 (upd :: respects($= ===> $= ===> ALPHA_obj ===> $= ===> 1177 ALPHA_method ===> $=)) 1178 (cns :: respects($= ===> $= ===> ALPHA_entry ===> ALPHA_dict ===> $=)) 1179 (nil:'b) 1180 (par:'d -> string -> method1 -> 'c 1181 :: respects($= ===> $= ===> ALPHA_method ===> $=)) 1182 (sgm :: respects($= ===> ($= ===> ALPHA_obj) ===> $=)). 1183 ?!(hom_o, hom_d, hom_e, hom_m) 1184 :: respects((ALPHA_obj ===> $=) ### 1185 (ALPHA_dict ===> $=) ### 1186 (ALPHA_entry ===> $=) ### 1187 (ALPHA_method ===> $=)). 1188 (!x. hom_o (OVAR1 x) = var x) /\ 1189 (!d. hom_o (OBJ1 d) = obj (hom_d d) d) /\ 1190 (!a l. hom_o (INVOKE1 a l) = nvk (hom_o a) a l) /\ 1191 (!a l m. hom_o (UPDATE1 a l m) = upd (hom_o a) (hom_m m) a l m) /\ 1192 (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d) e d) /\ 1193 ( hom_d ([]) = nil) /\ 1194 (!l m. hom_e (l,m) = (par (hom_m m) l m):'c) /\ 1195 (!x a. hom_m (SIGMA1 x a) = 1196 ((sgm (\y. hom_o (a <[ [x, OVAR1 y])) 1197 (\y. a <[ [x, OVAR1 y]))):'d)���, 1198 REPEAT (GEN_TAC ORELSE res_quanLib.RESQ_GEN_TAC) 1199 THEN CONV_TAC res_quanLib.RES_EXISTS_UNIQUE_CONV 1200 THEN CONJ_TAC 1201 THENL 1202 [ CONV_TAC PAIR_RES_EXISTS_CONV 1203 THEN PairRules.PBETA_TAC 1204 THEN REWRITE_ALL_TAC[SPECIFICATION] 1205 THEN IMP_RES_TAC (res_quanLib.RESQ_REWR_CANON 1206 object1_respects_Axiom_exists) 1207 THEN ASM_REWRITE_TAC[], 1208 1209 CONV_TAC (DEPTH_CONV PAIR_RES_FORALL_CONV) 1210 THEN PairRules.PBETA_TAC 1211 THEN REWRITE_TAC[PAIR_EQ] 1212 THEN REWRITE_TAC[object1_respects_Axiom_11] 1213 ] 1214 ); 1215 1216 1217(* ---------------------------------------------------------------- *) 1218(* Now we develop the last of the Gordon-Melham axioms, that states *) 1219(* the existence of a function `Abs' such that *) 1220(* SIGMA x a = ABS (\y. a <[ [x, OVAR y]) *) 1221(* ---------------------------------------------------------------- *) 1222 1223val ABS1_def = 1224 Define 1225 `ABS1 (f : var -> obj1) = 1226 let x = VAR "x" 0 in 1227 let v = variant x (FV_obj1 (f x)) in 1228 SIGMA1 v (f v)`; 1229 1230(* Prove ABS1 is respectful. *) 1231 1232val ABS1_ALPHA_LEMMA = store_thm 1233 ("ABS1_ALPHA_LEMMA", 1234 ���!f1 f2 x. 1235 ($= ===> ALPHA_obj) f1 f2 ==> 1236 (variant x (FV_obj1 (f1 x)) = variant x (FV_obj1 (f2 x)))���, 1237 REPEAT GEN_TAC 1238 THEN REWRITE_TAC[FUN_REL] 1239 THEN DISCH_TAC 1240 THEN AP_TERM_TAC 1241 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA_FV)) 1242 THEN FIRST_ASSUM MATCH_MP_TAC 1243 THEN REFL_TAC 1244 ); 1245 1246val ABS1_ALPHA = store_thm 1247 ("ABS1_ALPHA", 1248 ���!f1 f2 :var->obj1. 1249 ($= ===> ALPHA_obj) f1 f2 ==> 1250 ALPHA_method (ABS1 f1) (ABS1 f2)���, 1251 REPEAT STRIP_TAC 1252 THEN IMP_RES_TAC ABS1_ALPHA_LEMMA 1253 THEN ASM_REWRITE_TAC[ABS1_def] 1254 THEN CONV_TAC (DEPTH_CONV let_CONV) 1255 THEN MATCH_MP_TAC SIGMA1_RSP 1256 THEN REWRITE_ALL_TAC[FUN_REL] 1257 THEN FIRST_ASSUM MATCH_MP_TAC 1258 THEN REFL_TAC 1259 ); 1260 1261val SINGLE_vsubst = TAC_PROOF(([], 1262 ���!x y:var. 1263 [x, OVAR1 y :obj1] = ([x] // [y])���), 1264 REPEAT GEN_TAC 1265 THEN REWRITE_TAC[vsubst1] 1266 ); 1267 1268val SINGLE_SL = TAC_PROOF(([], 1269 ���!x:var. 1270 {x} = SL [x]���), 1271 GEN_TAC 1272 THEN REWRITE_TAC[SL] 1273 ); 1274 1275(* Melham and Gordon's fifth and final axiom. *) 1276 1277val SIGMA1_ABS1 = store_thm 1278 ("SIGMA1_ABS1", 1279 ���!x a:obj1. 1280 ALPHA_method (SIGMA1 x a) (ABS1 (\y. a <[ [x, OVAR1 y]))���, 1281 REPEAT GEN_TAC 1282 THEN REWRITE_TAC[ABS1_def] 1283 THEN CONV_TAC (DEPTH_CONV let_CONV) 1284 THEN BETA_TAC 1285 THEN ONCE_REWRITE_TAC[ALPHA_SYM] 1286 THEN MATCH_MP_TAC ALPHA_CHANGE_ONE_VAR 1287 THEN MATCH_MP_TAC variant_not_in_subset 1288 THEN REWRITE_TAC[FINITE_FV_object1] 1289 THEN REWRITE_TAC[SINGLE_vsubst,SINGLE_SL] 1290 THEN REWRITE_TAC[FV_vsubst1] 1291 ); 1292 1293 1294(* ---------------------------------------------------------------- *) 1295(* Now we prepare for the creation of the quotient of the object *) 1296(* calculus syntax by alpha-equivalence. Accordingly, we establish *) 1297(* the arguments to be passed to the quotient tool. *) 1298(* ---------------------------------------------------------------- *) 1299 1300val equivs = [ALPHA_obj_EQUIV, ALPHA_method_EQUIV]; 1301 1302val fnlist = [{def_name="OVAR_def", fname="OVAR", 1303 func= ���OVAR1 :var->^obj���, fixity=NONE 1304 (* see structure Parse *)}, 1305 {def_name="OBJ_def", fname="OBJ", 1306 func= ���OBJ1 :^dict -> ^obj���, fixity=NONE}, 1307 {def_name="INVOKE_def", fname="INVOKE", 1308 func= ���INVOKE1 :^obj -> string -> ^obj���, fixity=NONE}, 1309 {def_name="UPDATE_def", fname="UPDATE", 1310 func= ���UPDATE1 :^obj -> string -> ^method -> ^obj���, 1311 fixity=NONE}, 1312 {def_name="SIGMA_def", fname="SIGMA", 1313 func= ���SIGMA1 :var -> ^obj -> ^method���, fixity=NONE}, 1314 {def_name="ABS_def", fname="ABS", 1315 func= ���ABS1 :(var -> ^obj) -> ^method���, fixity=NONE}, 1316 {def_name="HEIGHT_obj_def", fname="HEIGHT_obj", 1317 func= ���HEIGHT_obj1 :^obj -> num���, fixity=NONE}, 1318 {def_name="HEIGHT_dict_def", fname="HEIGHT_dict", 1319 func= ���HEIGHT_dict1 :^dict -> num���, fixity=NONE}, 1320 {def_name="HEIGHT_entry_def", fname="HEIGHT_entry", 1321 func= ���HEIGHT_entry1 :^entry -> num���, fixity=NONE}, 1322 {def_name="HEIGHT_method_def", fname="HEIGHT_method", 1323 func= ���HEIGHT_method1 :^method -> num���, fixity=NONE}, 1324 {def_name="FV_obj_def", fname="FV_obj", 1325 func= ���FV_obj1 :^obj -> var -> bool���, fixity=NONE}, 1326 {def_name="FV_dict_def", fname="FV_dict", 1327 func= ���FV_dict1 :^dict -> var -> bool���, fixity=NONE}, 1328 {def_name="FV_entry_def", fname="FV_entry", 1329 func= ���FV_entry1 :^entry -> var -> bool���, fixity=NONE}, 1330 {def_name="FV_method_def", fname="FV_method", 1331 func= ���FV_method1 :^method -> var -> bool���,fixity=NONE}, 1332 {def_name="SUB_def", fname="SUB", 1333 func= ���SUB1 :^subs -> var -> ^obj���, fixity=NONE}, 1334 {def_name="FV_subst_def", fname="FV_subst", 1335 func= ���FV_subst1 :^subs -> (var -> bool) -> var -> bool���, 1336 fixity=NONE}, 1337 {def_name="SUBo_def", fname="SUBo", 1338 func= ���SUB1o :^obj -> ^subs -> ^obj���, 1339 fixity=SOME(Infix(NONASSOC,150))}, 1340 {def_name="SUBd_def", fname="SUBd", 1341 func= ���SUB1d :^dict -> ^subs -> ^dict���, 1342 fixity=SOME(Infix(NONASSOC,150))}, 1343 {def_name="SUBe_def", fname="SUBe", 1344 func= ���SUB1e :^entry -> ^subs -> ^entry���, 1345 fixity=SOME(Infix(NONASSOC,150))}, 1346 {def_name="SUBm_def", fname="SUBm", 1347 func= ���SUB1m :^method -> ^subs -> ^method���, 1348 fixity=SOME(Infix(NONASSOC,150))}, 1349 {def_name="vsubst_def", fname="/", 1350 func= ���$// :var list -> var list -> ^subs���, 1351 fixity=SOME(Infix(NONASSOC,150))}, 1352 {def_name="obj_0_def", fname="obj_0", 1353 func= ���obj1_0���, fixity=NONE}, 1354 {def_name="method_0_def", fname="method_0", 1355 func= ���method1_0���, fixity=NONE}, 1356 {def_name="invoke_method_def", fname="invoke_method", 1357 func= ���invoke_method1���, fixity=NONE}, 1358 {def_name="invoke_dict_def", fname="invoke_dict", 1359 func= ���invoke_dict1���, fixity=NONE}, 1360 {def_name="invoke_def", fname="invoke", 1361 func= ���invoke1���, fixity=NONE}, 1362 {def_name="update_dict_def", fname="update_dict", 1363 func= ���update_dict1���, fixity=NONE}, 1364 {def_name="update_def", fname="update", 1365 func= ���update1���, fixity=NONE}, 1366 {def_name="subst_eq_def", fname="subst_eq", 1367 func= ���ALPHA_subst:(var -> bool) ->^subs ->^subs -> bool���, 1368 fixity=NONE} 1369 ]; 1370 1371 1372val respects = [OVAR1_RSP, OBJ1_RSP, INVOKE1_RSP, UPDATE1_RSP, SIGMA1_RSP, 1373 ABS1_ALPHA, ALPHA_subst_RSP, 1374 HEIGHT_obj1_RSP, HEIGHT_dict1_RSP, HEIGHT_entry1_RSP, 1375 HEIGHT_method1_RSP, FV_obj1_RSP, FV_dict1_RSP, FV_entry1_RSP, 1376 FV_method1_RSP, SUB1_RSP, FV_subst_RSP, vsubst1_RSP, 1377 SUBo_RSP, SUBd_RSP, SUBe_RSP, SUBm_RSP, 1378 obj1_0_RSP,method1_0_RSP, 1379 invoke_method1_RSP, 1380 REWRITE_RULE[ALPHA_dict_EQ] invoke_dict1_RSP, 1381 invoke1_RSP, 1382 REWRITE_RULE[ALPHA_dict_EQ] update_dict1_RSP, 1383 update1_RSP] 1384 1385val polydfs = [BV_subst_PRS, COND_PRS, CONS_PRS, NIL_PRS, 1386 COMMA_PRS, FST_PRS, SND_PRS, 1387 LET_PRS, o_PRS, UNCURRY_PRS, 1388 FORALL_PRS, EXISTS_PRS, 1389 EXISTS_UNIQUE_PRS, ABSTRACT_PRS]; 1390 1391val polywfs = [BV_subst_RSP, COND_RSP, CONS_RSP, NIL_RSP, 1392 COMMA_RSP, FST_RSP, SND_RSP, 1393 LET_RSP, o_RSP, UNCURRY_RSP, 1394 RES_FORALL_RSP, RES_EXISTS_RSP, 1395 RES_EXISTS_EQUIV_RSP, RES_ABSTRACT_RSP]; 1396 1397 1398fun gg tm = proofManagerLib.set_goal([],tm); 1399 1400 1401val term_EQ_IS_ALPHA = 1402 TAC_PROOF 1403 (([], 1404 ���(!t x. 1405 (t = OVAR1 x) = ALPHA_obj t (OVAR1 x)) /\ 1406 (!d:(string # method1) list. 1407 (d = []) = LIST_REL ($= ### ALPHA_method) d [])���), 1408 REPEAT CONJ_TAC 1409 THEN Cases 1410 THEN REPEAT GEN_TAC 1411 THEN REWRITE_TAC[object1_one_one,object1_distinct, 1412 ALPHA_object_pos,ALPHA_object_neg,GSYM ALPHA_dict_EQ] 1413 ); 1414 1415 1416val old_thms = 1417 [HEIGHT1_def, 1418 REWRITE_RULE[term_EQ_IS_ALPHA] HEIGHT_LESS_EQ_ZERO1, 1419 FV_object1_def, 1420 FINITE_FV_object1, 1421 SUB1, 1422 SUB1_def, 1423 SUB_vsubst_OVAR1, 1424 REWRITE_RULE[term_EQ_IS_ALPHA] IN_FV_SUB_vsubst1, 1425 SUB_APPEND_vsubst1, 1426 SUB_FREE_vsubst1, 1427 FV_subst1, 1428 FINITE_FV_subst1, 1429 FV_subst_EQ1', 1430 REWRITE_RULE[term_EQ_IS_ALPHA] FV_subst_IDENT1, 1431 FV_subst_NIL1, 1432 SUB_object1_def, 1433 ALPHA_method_SIGMA, 1434 subst_SAME_ONE1, 1435 (* subst_SAME_TWO1, *) 1436 subst_EQ1', 1437 FREE_SUB1, 1438 BV_subst_IDENT1, 1439 BV_vsubst1, 1440 FREE_FV_SUB1, 1441 FREE_IDENT_SUBST1, 1442 REWRITE_RULE[term_EQ_IS_ALPHA] subst_IDENT1, 1443 subst_NIL1, 1444 HEIGHT1_SUB1_var, 1445 HEIGHT1_var_list_subst, 1446 HEIGHT1_var_subst, 1447 object1_distinct', 1448 object1_cases, (* not regular, but lifts! *) 1449 REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ] object1_one_one', 1450 ALPHA_method_one_one, 1451 vsubst1_def, 1452 vsubst1, 1453 SUB_APPEND_FREE_vsubst1, 1454 (* ALPHA_subst, *) 1455 ALPHA_SUB_CONTEXT, 1456 ALPHA_CHANGE_VAR, 1457 ALPHA_CHANGE_ONE_VAR, 1458 CHANGE_ONE_VAR1, 1459 ALPHA_SIGMA_subst, 1460 1461 obj1_0, 1462 method1_0, 1463 invoke_method1_def, 1464 invoke_dict1_def, 1465 invoke_dict1, 1466 LIST_CONJ (map GEN_ALL (CONJUNCTS invoke1_def)), 1467 invoke1, 1468 update_dict1_def, 1469 update_dict1, 1470 LIST_CONJ (map GEN_ALL (CONJUNCTS update1_def)), 1471 update1, 1472 1473 SIGMA1_ABS1, 1474 obj1_induction, 1475 REWRITE_RULE[ALPHA_dict_EQ,ALPHA_entry_EQ(*,FUN_REL_EQ*)] 1476 object1_respects_Axiom 1477 ]; 1478 1479 1480(* ==================================================== *) 1481(* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *) 1482(* ==================================================== *) 1483 1484val _ = quotient.chatting := true; 1485 1486val [HEIGHT, 1487 HEIGHT_LESS_EQ_ZERO, 1488 FV_object, (* AXIOM 1 of Gordon and Melham *) 1489 FINITE_FV_object, 1490 SUB, 1491 SUB_def, 1492 SUB_vsubst_OVAR, 1493 IN_FV_SUB_vsubst, 1494 SUB_APPEND_vsubst, 1495 SUB_FREE_vsubst, 1496 FV_subst, 1497 FINITE_FV_subst, 1498 FV_subst_EQ, 1499 FV_subst_IDENT, 1500 FV_subst_NIL, 1501 SUB_object, 1502 SIGMA_EQ, 1503 subst_SAME_ONE, 1504 (* subst_SAME_TWO, *) 1505 subst_EQ, 1506 FREE_SUB, 1507 BV_subst_IDENT, 1508 BV_vsubst, 1509 FREE_FV_SUB, 1510 FREE_IDENT_SUBST, 1511 subst_IDENT, 1512 subst_NIL, 1513 HEIGHT_SUB_var, 1514 HEIGHT_var_list_subst, 1515 HEIGHT_var_subst, 1516 object_distinct, 1517 object_cases, 1518 object_one_one, 1519 SIGMA_one_one, 1520 vsubst_def, 1521 vsubst, 1522 SUB_APPEND_FREE_vsubst, 1523 SUB_CONTEXT, 1524 SIGMA_CHANGE_VAR, 1525 SIGMA_CHANGE_ONE_VAR, 1526 CHANGE_ONE_VAR, 1527 SIGMA_subst, 1528 obj_0, 1529 method_0, 1530 invoke_method_def, 1531 invoke_dict_def, 1532 invoke_dict, 1533 invoke_def, 1534 invoke, 1535 update_dict_def, 1536 update_dict, 1537 update_def, 1538 update, 1539 SIGMA_ABS, 1540 object_induct, 1541 object_Axiom 1542 ] = 1543 define_quotient_types 1544 {types = [{name = "obj", equiv = ALPHA_obj_EQUIV}, 1545 {name = "method", equiv = ALPHA_method_EQUIV}], 1546 tyop_equivs = [LIST_EQUIV, PAIR_EQUIV], 1547 tyop_quotients = [LIST_QUOTIENT, PAIR_QUOTIENT, FUN_QUOTIENT], 1548 tyop_simps = [LIST_REL_EQ, LIST_MAP_I, PAIR_REL_EQ, PAIR_MAP_I, 1549 FUN_REL_EQ, FUN_MAP_I], 1550 defs = fnlist, 1551 respects = respects, 1552 poly_preserves = polydfs, 1553 poly_respects = polywfs, 1554 old_thms = old_thms}; 1555 1556 1557val _ = map save_thm 1558 [("HEIGHT",HEIGHT), 1559 ("HEIGHT_LESS_EQ_ZERO",HEIGHT_LESS_EQ_ZERO), 1560 ("FV_object",FV_object), (* AXIOM 1 of Gordon and Melham *) 1561 ("FINITE_FV_object",FINITE_FV_object), 1562 ("SUB",SUB), 1563 ("SUB_def",SUB_def), 1564 ("SUB_vsubst_OVAR",SUB_vsubst_OVAR), 1565 ("IN_FV_SUB_vsubst",IN_FV_SUB_vsubst), 1566 ("SUB_APPEND_vsubst",SUB_APPEND_vsubst), 1567 ("SUB_FREE_vsubst",SUB_FREE_vsubst), 1568 ("FV_subst",FV_subst), 1569 ("FINITE_FV_subst",FINITE_FV_subst), 1570 ("FV_subst_EQ",FV_subst_EQ), 1571 ("FV_subst_IDENT",FV_subst_IDENT), 1572 ("FV_subst_NIL",FV_subst_NIL), 1573 ("SUB_object",SUB_object), 1574 ("SIGMA_EQ",SIGMA_EQ), 1575 ("subst_SAME_ONE",subst_SAME_ONE), 1576 (* ("subst_SAME_TWO",subst_SAME_TWO), *) 1577 ("subst_EQ",subst_EQ), 1578 ("FREE_SUB",FREE_SUB), 1579 ("BV_subst_IDENT",BV_subst_IDENT), 1580 ("BV_vsubst",BV_vsubst), 1581 ("FREE_FV_SUB",FREE_FV_SUB), 1582 ("FREE_IDENT_SUBST",FREE_IDENT_SUBST), 1583 ("subst_IDENT",subst_IDENT), 1584 ("subst_NIL",subst_NIL), 1585 ("HEIGHT_SUB_var",HEIGHT_SUB_var), 1586 ("HEIGHT_var_list_subst",HEIGHT_var_list_subst), 1587 ("HEIGHT_var_subst",HEIGHT_var_subst), 1588 ("object_distinct",object_distinct), 1589 ("object_cases",object_cases), 1590 ("object_one_one",object_one_one), 1591 ("SIGMA_one_one",SIGMA_one_one), 1592 ("vsubst_def",vsubst_def), 1593 ("vsubst",vsubst), 1594 ("SUB_APPEND_FREE_vsubst",SUB_APPEND_FREE_vsubst), 1595 ("SUB_CONTEXT",SUB_CONTEXT), 1596 ("SIGMA_CHANGE_VAR",SIGMA_CHANGE_VAR), 1597 ("SIGMA_CHANGE_ONE_VAR",SIGMA_CHANGE_ONE_VAR), 1598 ("CHANGE_ONE_VAR",CHANGE_ONE_VAR), 1599 ("SIGMA_subst",SIGMA_subst), 1600 ("obj_0",obj_0), 1601 ("method_0",method_0), 1602 ("invoke_method_def",invoke_method_def), 1603 ("invoke_dict_def",invoke_dict_def), 1604 ("invoke_dict",invoke_dict), 1605 ("invoke_def",invoke_def), 1606 ("invoke",invoke), 1607 ("update_dict_def",update_dict_def), 1608 ("update_dict",update_dict), 1609 ("update_def",update_def), 1610 ("update",update), 1611 ("SIGMA_ABS",SIGMA_ABS), 1612 ("object_induct",object_induct), 1613 ("object_Axiom",object_Axiom) 1614 ]; 1615 1616 1617 1618(* Now overload the substitution operator <[ to refer to any of the *) 1619(* object, dict, entry, or method substitution operators defined: *) 1620 1621val _ = map (fn t => overload_on("<[", t)) 1622 [���$SUBo���,���$SUBd���,���$SUBe���,���$SUBm���] 1623handle e => Raise e; 1624 1625val subs = ty_antiq( ==`:(var # obj) list`== ); 1626val obj = ty_antiq( ==`:obj`== ); 1627val dict = ty_antiq( ==`:(string # method) list`== ); 1628val entry = ty_antiq( ==`:string # method`== ); 1629val method = ty_antiq( ==`:method`== ); 1630 1631 1632 1633 1634 1635 1636(* Now test the lifted induction principle: *) 1637 1638val HEIGHT_LESS_EQ_ZERO = store_thm 1639 ("HEIGHT_LESS_EQ_ZERO", 1640 ���(!o'. (HEIGHT_obj o' <= 0) = (?x. o' = OVAR x)) /\ 1641 (!d. (HEIGHT_dict d <= 0) = (d = NIL)) /\ 1642 (!e. (HEIGHT_entry e <= 0) = F) /\ 1643 (!m. (HEIGHT_method m <= 0) = F)���, 1644 MUTUAL_INDUCT_THEN object_induct ASSUME_TAC 1645 THEN REPEAT GEN_TAC 1646 THEN REWRITE_TAC[HEIGHT] 1647 THEN ASM_REWRITE_TAC[NOT_SUC_LESS_EQ_0,LESS_EQ_REFL] 1648 THEN REWRITE_TAC[object_distinct,NOT_CONS_NIL,NOT_NIL_CONS] 1649 THEN REWRITE_TAC[object_one_one] 1650 THEN EXISTS_TAC ���v:var��� 1651 THEN REWRITE_TAC[] 1652 ); 1653 1654 1655(* We will sometimes wish to induct on the height of an object. *) 1656 1657val object_height_induct_LEMMA = store_thm 1658 ("object_height_induct_LEMMA", 1659 ���!n obj_Prop dict_Prop entry_Prop method_Prop. 1660 (!x. obj_Prop (OVAR x)) /\ 1661 (!d. dict_Prop d ==> obj_Prop (OBJ d)) /\ 1662 (!o'. obj_Prop o' ==> (!l. obj_Prop (INVOKE o' l))) /\ 1663 (!o' m. 1664 obj_Prop o' /\ method_Prop m ==> (!l. obj_Prop (UPDATE o' l m))) /\ 1665 (!e d. entry_Prop e /\ dict_Prop d ==> dict_Prop (CONS e d)) /\ 1666 dict_Prop [] /\ 1667 (!m. method_Prop m ==> (!l. entry_Prop (l,m))) /\ 1668 (!o'. (!o''. (HEIGHT_obj o' = HEIGHT_obj o'') ==> obj_Prop o'') ==> 1669 (!x. method_Prop (SIGMA x o'))) ==> 1670 (!o'. (HEIGHT_obj o' <= n) ==> obj_Prop o') /\ 1671 (!d. (HEIGHT_dict d <= n) ==> dict_Prop d) /\ 1672 (!e. (HEIGHT_entry e <= n) ==> entry_Prop e) /\ 1673 (!m. (HEIGHT_method m <= n) ==> method_Prop m)���, 1674 INDUCT_TAC 1675 THEN REPEAT GEN_TAC 1676 THEN STRIP_TAC 1677 THENL 1678 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 1679 THEN REPEAT STRIP_TAC 1680 THEN ASM_REWRITE_TAC[], 1681 1682 UNDISCH_ALL_TAC 1683 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 1684 THEN ASSUME_TAC th) o SPEC_ALL) 1685 THEN POP_ASSUM MP_TAC 1686 THEN ASM_REWRITE_TAC[] 1687 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 1688 THEN REPEAT DISCH_TAC 1689 THEN MUTUAL_INDUCT_THEN object_induct ASSUME_TAC 1690 THEN REWRITE_TAC[HEIGHT] 1691 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 1692 THEN REPEAT STRIP_TAC 1693 THEN ASM_REWRITE_TAC[] 1694 THENL (* 6 subgoals *) 1695 [ FIRST_ASSUM MATCH_MP_TAC 1696 THEN FIRST_ASSUM MATCH_MP_TAC 1697 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1698 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1699 1700 FIRST_ASSUM MATCH_MP_TAC 1701 THEN FIRST_ASSUM MATCH_MP_TAC 1702 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1703 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1704 1705 FIRST_ASSUM MATCH_MP_TAC 1706 THEN CONJ_TAC 1707 THEN FIRST_ASSUM MATCH_MP_TAC 1708 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1709 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1710 1711 FIRST_ASSUM MATCH_MP_TAC 1712 THEN REPEAT STRIP_TAC 1713 THEN FIRST_ASSUM MATCH_MP_TAC 1714 THEN POP_ASSUM (REWRITE_THM o SYM) 1715 THEN FIRST_ASSUM ACCEPT_TAC, 1716 1717 FIRST_ASSUM MATCH_MP_TAC 1718 THEN CONJ_TAC 1719 THEN FIRST_ASSUM MATCH_MP_TAC 1720 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1721 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1722 1723 FIRST_ASSUM MATCH_MP_TAC 1724 THEN FIRST_ASSUM MATCH_MP_TAC 1725 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1726 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1727 ] 1728 ] 1729 ); 1730 1731 1732val object_height_induct = store_thm 1733 ("object_height_induct", 1734 ���!obj_Prop dict_Prop entry_Prop method_Prop. 1735 (!x. obj_Prop (OVAR x)) /\ 1736 (!d. dict_Prop d ==> obj_Prop (OBJ d)) /\ 1737 (!o'. obj_Prop o' ==> (!l. obj_Prop (INVOKE o' l))) /\ 1738 (!o' m. 1739 obj_Prop o' /\ method_Prop m ==> (!l. obj_Prop (UPDATE o' l m))) /\ 1740 (!e d. entry_Prop e /\ dict_Prop d ==> dict_Prop (CONS e d)) /\ 1741 dict_Prop [] /\ 1742 (!m. method_Prop m ==> (!l. entry_Prop (l,m))) /\ 1743 (!o'. (!o2. (HEIGHT_obj o' = HEIGHT_obj o2) ==> obj_Prop o2) ==> 1744 (!x. method_Prop (SIGMA x o'))) ==> 1745 (!a. obj_Prop a) /\ 1746 (!d. dict_Prop d) /\ 1747 (!e. entry_Prop e) /\ 1748 (!m. method_Prop m)���, 1749 REPEAT STRIP_TAC 1750 THENL 1751 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm object_height_induct_LEMMA))) 1752 [���HEIGHT_obj a���,���HEIGHT_dict d���, 1753 ���HEIGHT_entry e���,���HEIGHT_method m���]) 1754 THEN ASM_REWRITE_TAC[] 1755 THEN REPEAT STRIP_TAC 1756 THEN FIRST_ASSUM MATCH_MP_TAC 1757 THEN REWRITE_TAC[LESS_EQ_REFL] 1758 ); 1759 1760 1761val HEIGHT_SUB_vsubst = store_thm 1762 ("HEIGHT_SUB_vsubst", 1763 ���!xs ys x. 1764 HEIGHT_obj (SUB (xs / ys) x) = 0���, 1765 REPEAT GEN_TAC 1766 THEN STRIP_ASSUME_TAC (SPEC_ALL SUB_vsubst_OVAR) 1767 THEN ASM_REWRITE_TAC[HEIGHT] 1768 ); 1769 1770 1771val subst_EMPTY = store_thm 1772 ("subst_EMPTY", 1773 ���(!a x b. ~(x IN FV_obj a) ==> ((a <[ [x,b]) = a)) /\ 1774 (!d x b. ~(x IN FV_dict d) ==> ((d <[ [x,b]) = d)) /\ 1775 (!e x b. ~(x IN FV_entry e) ==> ((e <[ [x,b]) = e)) /\ 1776 (!m x b. ~(x IN FV_method m) ==> ((m <[ [x,b]) = m))���, 1777 REPEAT STRIP_TAC 1778 THENL (map MATCH_MP_TAC (CONJUNCTS subst_IDENT)) 1779 THEN REWRITE_TAC[SUB] 1780 THEN GEN_TAC 1781 THEN COND_CASES_TAC 1782 THEN ASM_REWRITE_TAC[] 1783 ); 1784 1785 1786val FV_object_subst = store_thm 1787 ("FV_object_subst", 1788 ���(!a s. FV_obj (a <[ s) = FV_subst s (FV_obj a)) /\ 1789 (!d s. FV_dict (d <[ s) = FV_subst s (FV_dict d)) /\ 1790 (!e s. FV_entry (e <[ s) = FV_subst s (FV_entry e)) /\ 1791 (!m s. FV_method (m <[ s) = FV_subst s (FV_method m))���, 1792 REWRITE_TAC[FV_subst] 1793 THEN MUTUAL_INDUCT_THEN object_induct ASSUME_TAC 1794 THEN REWRITE_TAC[SUB_object] 1795 THEN CONV_TAC (DEPTH_CONV let_CONV) 1796 THEN REWRITE_TAC[FV_object] 1797 THEN ASM_REWRITE_TAC[IMAGE_UNION,UNION_SET_UNION] 1798 THEN REWRITE_TAC[IMAGE,UNION_SET,UNION_EMPTY,o_THM] 1799 (* only one subgoal at this point! *) 1800 THEN REPEAT GEN_TAC 1801 THEN DEFINE_NEW_VAR 1802 ���v' = variant v (FV_subst s (FV_obj a DIFF {v}))��� 1803 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1804 THEN REWRITE_TAC[EXTENSION] 1805 THEN REWRITE_TAC[IN_DIFF,IN_UNION_SET,IN_IMAGE] 1806 THEN REWRITE_TAC[IN,o_THM] 1807 THEN GEN_TAC 1808 THEN EQ_TAC 1809 THENL 1810 [ STRIP_TAC 1811 THEN EXISTS_TAC ���si:var set��� 1812 THEN (CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC)) 1813 THEN EXISTS_TAC ���x':var��� 1814 THEN REWRITE_ALL_TAC[SUB] 1815 THEN SUBGOAL_THEN ���~((v:var) = x')��� ASSUME_TAC 1816 THENL 1817 [ DISCH_THEN (REWRITE_ALL_THM o SYM) 1818 THEN REWRITE_ALL_TAC[FV_object] 1819 THEN UNDISCH_THEN ���si = {v':var}��� REWRITE_ALL_THM 1820 THEN REWRITE_ALL_TAC[IN] 1821 THEN RES_TAC, 1822 1823 FIRST_ASSUM (REWRITE_ALL_THM o GSYM) 1824 THEN CONJ_TAC 1825 THEN FIRST_ASSUM ACCEPT_TAC 1826 ], 1827 1828 STRIP_TAC 1829 THEN CONJ_TAC 1830 THENL 1831 [ EXISTS_TAC ���si:var set��� 1832 THEN (CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC)) 1833 THEN EXISTS_TAC ���x':var��� 1834 THEN (CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC)) 1835 THEN REWRITE_TAC[SUB] 1836 THEN POP_ASSUM MP_TAC 1837 THEN FIRST_ASSUM (REWRITE_THM o GSYM) 1838 THEN ASM_REWRITE_TAC[], 1839 1840 MATCH_MP_TAC IN_NOT_IN 1841 THEN EXISTS_TAC ���FV_subst s (FV_obj a DIFF {v})��� 1842 THEN CONJ_TAC 1843 THENL 1844 [ REWRITE_TAC[FV_subst] 1845 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,IN_DIFF] 1846 THEN REWRITE_TAC[IN,o_THM] 1847 THEN EXISTS_TAC ���si:var set��� 1848 THEN FIRST_ASSUM REWRITE_THM 1849 THEN EXISTS_TAC ���x':var��� 1850 THEN REPEAT CONJ_TAC 1851 THEN FIRST_ASSUM ACCEPT_TAC, 1852 1853 ASM_REWRITE_TAC[] 1854 THEN MATCH_MP_TAC variant_not_in_set 1855 THEN MATCH_MP_TAC FINITE_FV_subst 1856 THEN MATCH_MP_TAC FINITE_DIFF 1857 THEN REWRITE_TAC[FINITE_FV_object] 1858 ] 1859 ] 1860 ] 1861 ); 1862 1863 1864val NOT_IN_FV_subst = store_thm 1865 ("NOT_IN_FV_subst", 1866 ���!y x a s. 1867 ~(y IN FV_obj a) /\ ~(y IN s) 1868 ==> ~(y IN FV_subst [x,a] s)���, 1869 REPEAT GEN_TAC 1870 THEN STRIP_TAC 1871 THEN REWRITE_TAC[FV_subst] 1872 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,o_THM,SUB] 1873 THEN STRIP_TAC 1874 THEN UNDISCH_LAST_TAC 1875 THEN ASM_REWRITE_TAC[] 1876 THEN COND_CASES_TAC 1877 THENL 1878 [ ASM_REWRITE_TAC[], 1879 1880 ASM_REWRITE_TAC[FV_object,IN] 1881 THEN IMP_RES_THEN (IMP_RES_THEN (REWRITE_THM o GSYM)) IN_NOT_IN 1882 ] 1883 ); 1884 1885 1886val NOT_IN_FV_subst2 = store_thm 1887 ("NOT_IN_FV_subst2", 1888 ���!y x1 (t1:^obj) x2 t2 s. 1889 ~(y IN FV_obj t1) /\ ~(y IN FV_obj t2) /\ ~(y IN s) 1890 ==> ~(y IN FV_subst [(x1,t1);(x2,t2)] s)���, 1891 REPEAT GEN_TAC 1892 THEN STRIP_TAC 1893 THEN REWRITE_TAC[FV_subst] 1894 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,o_THM,SUB] 1895 THEN STRIP_TAC 1896 THEN UNDISCH_LAST_TAC 1897 THEN ASM_REWRITE_TAC[] 1898 THEN COND_CASES_TAC 1899 THENL 1900 [ ASM_REWRITE_TAC[], 1901 1902 COND_CASES_TAC 1903 THENL 1904 [ ASM_REWRITE_TAC[], 1905 1906 ASM_REWRITE_TAC[FV_object,IN] 1907 THEN IMP_RES_THEN (IMP_RES_THEN (REWRITE_THM o GSYM)) IN_NOT_IN 1908 ] 1909 ] 1910 ); 1911 1912 1913val SIGMA_CHANGE_BOUND_VAR = store_thm 1914 ("SIGMA_CHANGE_BOUND_VAR", 1915 ���!y x a. 1916 ~(y IN (FV_obj a DIFF {x})) ==> 1917 (SIGMA x a = 1918 SIGMA y (a <[ [x, OVAR y]))���, 1919 REPEAT STRIP_TAC 1920 THEN MP_TAC (SPECL [���y:var���,���x:var���,���[]:^subs���, 1921 ���x:var���,���a:obj���] 1922 SIGMA_CHANGE_VAR) 1923 THEN REWRITE_TAC[FV_subst_NIL] 1924 THEN POP_ASSUM REWRITE_THM 1925 THEN REWRITE_TAC[IN_DIFF,IN,DE_MORGAN_THM] 1926 THEN DEP_ONCE_REWRITE_TAC[subst_IDENT] 1927 THEN GEN_TAC 1928 THEN REWRITE_TAC[SUB] 1929 THEN COND_CASES_TAC 1930 THEN ASM_REWRITE_TAC[] 1931 ); 1932 1933 1934val SIGMA_CLEAN_VAR = store_thm 1935 ("SIGMA_CLEAN_VAR", 1936 ���!s x a. FINITE s ==> 1937 ?x' o'. 1938 ~(x' IN (FV_obj a DIFF {x})) /\ ~(x' IN s) /\ 1939 (HEIGHT_obj a = HEIGHT_obj o') /\ 1940 (SIGMA x a = SIGMA x' o')���, 1941 REPEAT STRIP_TAC 1942 THEN MP_TAC (SPECL [���variant x ((FV_obj a DIFF {x}) UNION s)���, 1943 ���x:var���,���a:obj���] 1944 SIGMA_CHANGE_BOUND_VAR) 1945 THEN MP_TAC (SPECL [���x:var���,���(FV_obj a DIFF {x}) UNION s���] 1946 variant_not_in_set) 1947 THEN ASM_REWRITE_TAC[FINITE_UNION] 1948 THEN ASSUME_TAC (SPEC_ALL (CONJUNCT1 FINITE_FV_object)) 1949 THEN IMP_RES_THEN REWRITE_THM FINITE_DIFF 1950 THEN REWRITE_TAC[IN_UNION,DE_MORGAN_THM] 1951 THEN STRIP_TAC 1952 THEN ASM_REWRITE_TAC[] 1953 THEN STRIP_TAC 1954 THEN FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[HEIGHT,INV_SUC_EQ] o 1955 AP_TERM ���HEIGHT_method���) 1956 THEN EXISTS_TAC ���variant x ((FV_obj a DIFF {x}) UNION s)��� 1957 THEN EXISTS_TAC 1958 ���a <[ [x,OVAR (variant x ((FV_obj a DIFF {x}) UNION s))]��� 1959 THEN ASM_REWRITE_TAC[] 1960 ); 1961 1962 1963val SIGMA_LIST_CHANGE_BOUND_VAR = TAC_PROOF(([], 1964 ���!os y x. 1965 EVERY (\a. ~(y IN (FV_obj a DIFF {x}))) os ==> 1966 EVERY (\a. SIGMA x a = SIGMA y (a <[ [x, OVAR y])) os���), 1967 LIST_INDUCT_TAC 1968 THEN REWRITE_TAC[EVERY_DEF] 1969 THEN BETA_TAC 1970 THEN REPEAT STRIP_TAC 1971 THENL 1972 [ IMP_RES_TAC SIGMA_CHANGE_BOUND_VAR, 1973 1974 RES_TAC 1975 ] 1976 ); 1977 1978val FINITE_FOLDR = TAC_PROOF(([], 1979 ���!(l:'a list) f (i:'b set). 1980 (!x y. FINITE y ==> FINITE (f x y)) /\ FINITE i ==> 1981 FINITE (FOLDR f i l)���), 1982 LIST_INDUCT_TAC 1983 THEN REWRITE_TAC[FOLDR] 1984 THEN REPEAT STRIP_TAC 1985 THEN FIRST_ASSUM MATCH_MP_TAC 1986 THEN RES_TAC 1987 ); 1988 1989val FINITE_FOLDR_LEMMA = TAC_PROOF(([], 1990 ���!os s x. 1991 FINITE s ==> 1992 FINITE (FOLDR (\o' s. (FV_obj o' DIFF {x}) UNION s) s os)���), 1993 REPEAT STRIP_TAC 1994 THEN MATCH_MP_TAC FINITE_FOLDR 1995 THEN BETA_TAC 1996 THEN ASM_REWRITE_TAC[FINITE_UNION] 1997 THEN REPEAT GEN_TAC 1998 THEN DISCH_TAC 1999 THEN ASM_REWRITE_TAC[] 2000 THEN MATCH_MP_TAC FINITE_DIFF 2001 THEN REWRITE_TAC[FINITE_FV_object] 2002 ); 2003 2004val IN_FOLDR = TAC_PROOF(([], 2005 ���!os s x z. 2006 ~(z IN FOLDR (\o' s. (FV_obj o' DIFF {x}) UNION s) s os) ==> 2007 ~(z IN s) /\ 2008 EVERY (\a. ~(z IN FV_obj a DIFF {x})) os���), 2009 LIST_INDUCT_TAC 2010 THEN REWRITE_TAC[EVERY_DEF,FOLDR] 2011 THEN BETA_TAC 2012 THEN REWRITE_TAC[IN_UNION,DE_MORGAN_THM] 2013 THEN REPEAT GEN_TAC THEN STRIP_TAC 2014 THEN RES_TAC 2015 THEN ASM_REWRITE_TAC[] 2016 ); 2017 2018val EVERY_HEIGHT_LEMMA = TAC_PROOF(([], 2019 ���!os x z. 2020 EVERY (\a. SIGMA x a = SIGMA z (a <[ [x,OVAR z])) os ==> 2021 EVERY (\x'. HEIGHT_obj x' = HEIGHT_obj (x' <[ [x,OVAR z])) os 2022 ���), 2023 LIST_INDUCT_TAC 2024 THEN REWRITE_TAC[EVERY_DEF] 2025 THEN BETA_TAC 2026 THEN REPEAT GEN_TAC THEN STRIP_TAC 2027 THEN UNDISCH_LAST_TAC 2028 THEN FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[HEIGHT,INV_SUC_EQ] o 2029 AP_TERM ���HEIGHT_method���) 2030 THEN STRIP_TAC 2031 THEN RES_TAC 2032 THEN ASM_REWRITE_TAC[] 2033 ); 2034 2035 2036val MAP2_MAP = TAC_PROOF(([], 2037 ���!l (f:'a->'b->'c) g. 2038 MAP2 f l (MAP g l) = MAP (\x. f x (g x)) l���), 2039 LIST_INDUCT_TAC 2040 THEN REWRITE_TAC[MAP2,MAP] 2041 THEN BETA_TAC 2042 THEN ASM_REWRITE_TAC[] 2043 ); 2044 2045val EVERY_MAP = TAC_PROOF(([], 2046 ���!l P (f:'a->'b). 2047 EVERY P (MAP f l) = EVERY (P o f) l���), 2048 LIST_INDUCT_TAC 2049 THEN REWRITE_TAC[EVERY_DEF,MAP] 2050 THEN ASM_REWRITE_TAC[o_THM] 2051 ); 2052 2053val SIGMA_LIST_CLEAN_VAR = store_thm 2054 ("SIGMA_LIST_CLEAN_VAR", 2055 ���!s x os. FINITE s ==> 2056 ?z os'. 2057 ~(z IN s) /\ 2058 EVERY (\a. ~(z IN (FV_obj a DIFF {x}))) os /\ 2059 EVERY I (MAP2 (\a o'. HEIGHT_obj a = HEIGHT_obj o') os os') /\ 2060 EVERY I (MAP2 (\a o'. SIGMA x a = SIGMA z o') os os') /\ 2061 (LENGTH os' = LENGTH os)���, 2062 2063 let val s = ���FOLDR (\o' s. (FV_obj o' DIFF {x}) UNION s) s os��� 2064 val z = ���variant x ^s��� 2065 in 2066 REPEAT STRIP_TAC 2067 THEN DEFINE_NEW_VAR ���z = ^z��� 2068 THEN POP_ASSUM (ASSUME_TAC o SYM) 2069 THEN EXISTS_TAC ���z:var��� 2070 THEN EXISTS_TAC ���MAP (\a:obj. a <[ [x,OVAR z]) os��� 2071 THEN MP_TAC (SPECL [���os:obj list���,z,���x:var���] 2072 SIGMA_LIST_CHANGE_BOUND_VAR) 2073 THEN MP_TAC (SPECL [���x:var���,s] variant_not_in_set) 2074 THEN ASM_REWRITE_TAC[LENGTH_MAP] 2075 THEN IMP_RES_THEN REWRITE_THM FINITE_FOLDR_LEMMA 2076 THEN DISCH_TAC 2077 THEN IMP_RES_THEN REWRITE_THM IN_FOLDR 2078 THEN DISCH_TAC 2079 THEN REWRITE_TAC[MAP2_MAP] 2080 THEN BETA_TAC 2081 THEN ASM_REWRITE_TAC[EVERY_MAP,I_o_ID] 2082 THEN IMP_RES_TAC EVERY_HEIGHT_LEMMA 2083 end 2084 ); 2085 2086(* 2087val EQ_subst = 2088 new_definition 2089 ("EQ_subst", 2090 ���EQ_subst t s1 s2 = 2091 (!x. (x IN t) ==> 2092 (SUB s1 x = SUB s2 x))���); 2093 2094 2095val SUB_CONTEXT = store_thm 2096 ("SUB_CONTEXT", 2097 ���(!a s1 s2. 2098 EQ_subst (FV_obj a) s1 s2 ==> ((a <[ s1) = (a <[ s2))) /\ 2099 (!d s1 s2. 2100 EQ_subst (FV_dict d) s1 s2 ==> ((d <[ s1) = (d <[ s2))) /\ 2101 (!e s1 s2. 2102 EQ_subst (FV_entry e) s1 s2 ==> ((e <[ s1) = (e <[ s2))) /\ 2103 (!m s1 s2. 2104 EQ_subst (FV_method m) s1 s2 ==> ((m <[ s1) = (m <[ s2)))���, 2105 REPEAT CONJ_TAC 2106 THEN REPEAT GEN_TAC 2107 THEN REWRITE_TAC[EQ_subst,FV_object,SUB_def] 2108 THEN DISCH_TAC 2109 THEN REWRITE_TAC[object_REP_equal_equiv] 2110 THENL (map (REWRITE_THM o ALPHA_EQ_RULES) (CONJUNCTS REP_SUB_object)) 2111 THENL (map MATCH_MP_TAC (CONJUNCTS ALPHA_SUB_CONTEXT)) 2112 THEN REWRITE_TAC[ALPHA_REFL] 2113 THEN REWRITE_TAC[ALPHA_subst] 2114 THEN GEN_TAC 2115 THEN DISCH_TAC 2116 THEN RES_TAC 2117 THEN UNDISCH_LAST_TAC 2118 THEN REWRITE_TAC[object_equiv_ABS_equal] 2119 ); 2120*) 2121 2122val SIGMA_SUBST_SIMPLE = store_thm 2123 ("SIGMA_SUBST_SIMPLE", 2124 ���!x a s. 2125 ~(x IN FV_subst s (FV_obj a DIFF {x})) /\ 2126 ~(x IN BV_subst s) ==> 2127 (SIGMA x a <[ s = SIGMA x (a <[ s))���, 2128 REPEAT STRIP_TAC 2129 THEN REWRITE_TAC[SUB_object] 2130 THEN DEP_REWRITE_TAC[variant_ident,FINITE_FV_subst,FINITE_DIFF] 2131 THEN IMP_RES_TAC BV_subst_IDENT 2132 THEN ASM_REWRITE_TAC[FINITE_FV_object] 2133 THEN CONV_TAC (DEPTH_CONV let_CONV) 2134 THEN DEP_ONCE_REWRITE_TAC[SPECL [���a:obj���, 2135 ���CONS (x, OVAR x) s���,���s:^subs���] 2136 (CONJUNCT1 subst_EQ)] 2137 THEN REPEAT STRIP_TAC 2138 THEN REWRITE_TAC[SUB] 2139 THEN COND_CASES_TAC 2140 THEN ASM_REWRITE_TAC[] 2141 ); 2142 2143 2144val SIGMA_SUBST_VAR = store_thm 2145 ("SIGMA_SUBST_VAR", 2146 ���!x a s. 2147 ?x' o'. 2148 ~(x' IN (FV_obj a DIFF {x})) /\ 2149 ~(x' IN FV_subst s (FV_obj a DIFF {x})) /\ 2150 ~(x' IN FV_subst s (FV_obj o' DIFF {x'})) /\ 2151 ~(x' IN BV_subst s) /\ 2152 (SUB s x' = OVAR x') /\ 2153 (HEIGHT_obj a = HEIGHT_obj o') /\ 2154 (SIGMA x a = SIGMA x' o') /\ 2155 ((SIGMA x a <[ s) = SIGMA x' (o' <[ s))���, 2156 REPEAT GEN_TAC 2157 THEN MP_TAC (SPECL [���FV_subst s (FV_obj a DIFF {x}) 2158 UNION BV_subst s���, 2159 ���x:var���,���a:obj���] 2160 SIGMA_CLEAN_VAR) 2161 THEN REWRITE_TAC[FINITE_UNION,FINITE_BV_subst] 2162 THEN DEP_REWRITE_TAC[FINITE_FV_subst,FINITE_DIFF] 2163 THEN REWRITE_TAC[FINITE_FV_object,IN_UNION,DE_MORGAN_THM] 2164 THEN DISCH_THEN (Q.X_CHOOSE_THEN `x'` 2165 (Q.X_CHOOSE_THEN `o'` STRIP_ASSUME_TAC)) 2166 THEN EXISTS_TAC ���x':var��� 2167 THEN EXISTS_TAC ���o':obj��� 2168 THEN ASM_REWRITE_TAC[] 2169 THEN FIRST_ASSUM (ASSUME_TAC o SYM o REWRITE_RULE[FV_object] o 2170 AP_TERM ���FV_method���) 2171 THEN IMP_RES_TAC BV_subst_IDENT 2172 THEN ASM_REWRITE_TAC[] 2173 THEN MATCH_MP_TAC SIGMA_SUBST_SIMPLE 2174 THEN ASM_REWRITE_TAC[] 2175 ); 2176 2177 2178val ALL_SIGMA_OBJ_EQ = store_thm 2179 ("ALL_SIGMA_OBJ_EQ", 2180 ���!obj_Prop. 2181 (!o'. (\o'. !o2. (?v x. SIGMA v o' = SIGMA x o2) 2182 ==> obj_Prop o2) o') 2183 = 2184 (!o'. obj_Prop o')���, 2185 GEN_TAC 2186 THEN BETA_TAC 2187 THEN EQ_TAC 2188 THEN STRIP_TAC 2189 THEN ASM_REWRITE_TAC[] 2190 THEN GEN_TAC 2191 THEN FIRST_ASSUM MATCH_MP_TAC 2192 THEN EXISTS_TAC ���o':obj��� 2193 THEN EXISTS_TAC ���v:var��� 2194 THEN EXISTS_TAC ���v:var��� 2195 THEN REFL_TAC 2196 ); 2197 2198 2199 2200(* ===================================================================== *) 2201(* End of the lifting of object calculus types and basic definitions *) 2202(* to the higher, more abstract level where alpha-equivalent expressions *) 2203(* are actually equal in HOL. *) 2204(* ===================================================================== *) 2205 2206 2207 2208val _ = export_theory(); 2209 2210val _ = print_theory_to_file "lift.lst"; 2211 2212val _ = html_theory "lift"; 2213 2214val _ = print_theory_size(); 2215