1(* ===================================================================== *) 2(* FILE : variableScript.sml *) 3(* VERSION : 1.0 *) 4(* DESCRIPTION : Defines variables data structure, and variants of *) 5(* variables. . *) 6(* *) 7(* AUTHOR : Peter Vincent Homeier *) 8(* DATE : October 19, 2000 *) 9(* COPYRIGHT : Copyright (c) 2000 by Peter Vincent Homeier *) 10(* *) 11(* ===================================================================== *) 12 13 (* ================== *) 14 (* THE SUNRISE SYSTEM *) 15 (* \ | / *) 16 (* ---_*_--- *) 17 (* ================== *) 18 19 20(* --------------------------------------------------------------------- *) 21(* Boilerplate. *) 22(* --------------------------------------------------------------------- *) 23open HolKernel Parse boolLib; 24infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 25infixr -->; 26 27 28(* --------------------------------------------------------------------- *) 29(* Create the theory. *) 30(* --------------------------------------------------------------------- *) 31val _ = new_theory "variable"; 32 33 34(* 35app load ["stringTheory", "stringLib", "pred_setTheory", "pred_setLib", 36 "listTheory", "rich_listTheory", "listLib", 37 "numLib", "Datatype", 38 "arithmeticTheory", "Psyntax", "Define_type", 39 "more_listTheory", "more_setTheory", 40 "dep_rewrite", "bossLib" ]; 41*) 42open stringTheory stringLib pred_setTheory pred_setLib; 43open listTheory rich_listTheory listLib; 44open numLib prim_recTheory combinTheory PairedLambda; 45open arithmeticTheory Psyntax; 46open more_listTheory more_setTheory; 47open dep_rewrite bossLib; 48 49 50open tactics; 51 52 53 54(*===========================================================*) 55(* The actual "names" of variables will be defined as a *) 56(* composite type, containing not only a string but also a *) 57(* "variant" number; initially this will be zero, but when *) 58(* this is positive, it indicates a numeric postfix to the *) 59(* variable name. This is to make it easier to define *) 60(* recognizable variants of variable names. A zero postfix *) 61(* will not be read; thus ("x",0) => "x" but ("y",2) => "y2".*) 62(*===========================================================*) 63 64val _ = Hol_datatype `var = VAR of string => num`; 65 66(* 67val var_Axiom = theorem "var_Axiom"; 68val var_induct = theorem "var_induction"; 69val var_cases = theorem "var_nchotomy"; 70val var_one_one = theorem "var_11"; 71*) 72 73 74 75(* =============================================================== *) 76(* We define Base v as the string which is the base of v. *) 77(* =============================================================== *) 78 79val Base_def = 80 Define `(Base (VAR s n) = s)`; 81 82(* =============================================================== *) 83(* We define Index v as the "variant" number attached to the base. *) 84(* =============================================================== *) 85 86val Index_def = 87 Define `(Index (VAR s n) = n)`; 88 89 90val Base_Index = store_thm 91 ("Base_Index", 92 ���!x. VAR (Base x) (Index x) = x���, 93 Induct 94 THEN REWRITE_TAC[Base_def,Index_def] 95 ); 96 97(* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *) 98 99 100val VAR_EQ_IMP = store_thm 101 ("VAR_EQ_IMP", 102 ���!x y. (Base x = Base y) /\ (Index x = Index y) ==> (x = y)���, 103 Induct 104 THEN GEN_TAC THEN GEN_TAC 105 THEN Induct 106 THEN RW_TAC std_ss [Base_def,Index_def] 107 ); 108 109val VAR_EQ = store_thm 110 ("VAR_EQ", 111 ���!x y. (x = y) = (Base x = Base y) /\ (Index x = Index y)���, 112 GEN_TAC THEN GEN_TAC THEN 113 EQ_TAC THENL 114 [ DISCH_THEN REWRITE_THM, 115 REWRITE_TAC[VAR_EQ_IMP] ] 116 ); 117 118 119(* =============================================================== *) 120(* Variants of variables are variables with the same name, but *) 121(* with different numbers attached. They are considered different *) 122(* variables in the state. For a clean definition, a variable *) 123(* itself is also considered to be a (null) variant of itself. *) 124(* =============================================================== *) 125 126(* =============================================================== *) 127(* An easy way to make a variant is to take an existing variable *) 128(* and add an integer to its "variant" number. *) 129(* =============================================================== *) 130 131val mk_variant_def = 132 Define 133 `mk_variant (VAR s n) m = (VAR s (n+m))`; 134 135val Index_mk_variant = store_thm 136 ("Index_mk_variant", 137 ���!x k. Index(mk_variant x k) = Index x + k���, 138 Induct THEN 139 REWRITE_TAC[mk_variant_def,Index_def] 140 ); 141 142val Base_mk_variant = store_thm 143 ("Base_mk_variant", 144 ���!x k. Base(mk_variant x k) = Base x���, 145 Induct THEN 146 REWRITE_TAC[mk_variant_def,Base_def] 147 ); 148 149val mk_variant_ident = store_thm 150 ("mk_variant_ident", 151 ���!x k. (mk_variant x k = x) = (k = 0)���, 152 Induct 153 THEN RW_TAC arith_ss [mk_variant_def] 154 ); 155 156val mk_variant_equal = store_thm 157 ("mk_variant_equal", 158 ���!x m n. (mk_variant x m = mk_variant x n) = (m = n)���, 159 Induct 160 THEN RW_TAC arith_ss [mk_variant_def] 161 ); 162 163val mk_variant_compose = store_thm 164 ("mk_variant_compose", 165 ���!x m n. mk_variant (mk_variant x m) n = (mk_variant x (m+n))���, 166 Induct 167 THEN RW_TAC arith_ss [mk_variant_def] 168 ); 169 170 171(* =============================================================== *) 172(* We would like to be able to test if a variable is a variant of *) 173(* another variable. *) 174(* =============================================================== *) 175 176(* For Taupo-1 (to come!): 177new_infix("is_variant", ==`:var->var->bool`==, 450); 178*) 179 180val is_variant = new_definition ( 181 "is_variant", 182 ``$is_variant y x = 183 ((Base y = Base x) /\ (Index x <= Index y))``) 184val _ = set_fixity "is_variant" (Infix(NONASSOC, 450)) 185 186 187val is_variant_reflexive = store_thm 188 ("is_variant_reflexive", 189 ���!x. x is_variant x���, 190 Induct 191 THEN RW_TAC arith_ss [is_variant] 192 ); 193 194val mk_variant_is_variant = store_thm 195 ("mk_variant_is_variant", 196 ���!x k. (mk_variant x k) is_variant x���, 197 Induct 198 THEN RW_TAC arith_ss [mk_variant_def,is_variant,Base_def,Index_def] 199 ); 200 201val is_variant_TRANS = store_thm 202 ("is_variant_TRANS", 203 ���!x y z. (z is_variant y) /\ (y is_variant x) ==> (z is_variant x)���, 204 RW_TAC arith_ss [is_variant] 205 ); 206 207val is_variant_SOME_mk_variant = store_thm 208 ("is_variant_SOME_mk_variant", 209 ���!x y. y is_variant x = (?k. y = mk_variant x k)���, 210 Induct 211 THEN GEN_TAC THEN GEN_TAC 212 THEN Induct 213 THEN RW_TAC arith_ss [mk_variant_def,is_variant,Base_def,Index_def] 214 THEN EQ_TAC 215 THENL 216 [ STRIP_TAC 217 THEN EXISTS_TAC ���n' - n��� 218 THEN RW_TAC arith_ss [], 219 220 STRIP_TAC 221 THEN RW_TAC arith_ss [] 222 ] 223 ); 224 225val is_variant_NOT_EQ = store_thm 226 ("is_variant_NOT_EQ", 227 ���!x y. (y is_variant x) /\ ~(x = y) ==> 228 (y is_variant mk_variant x 1)���, 229 RW_TAC arith_ss [is_variant,Base_mk_variant,Index_mk_variant,VAR_EQ] 230 THENL 231 [ UNDISCH_LAST_TAC 232 THEN ASM_REWRITE_TAC[], 233 234 RW_TAC arith_ss [] 235 ] 236 ); 237 238 239(* =============================================================== *) 240(* Once we can make variants of a variable, we can make a whole *) 241(* set of them, of any size we like, all distinct from each other. *) 242(* =============================================================== *) 243 244fun new_prim_rec_definition (name,tm) = 245 new_recursive_definition 246 {rec_axiom = prim_recTheory.num_Axiom, 247 name = name, 248 def = tm}; 249 250val variant_set = 251 new_prim_rec_definition 252 ("variant_set", 253 ���(variant_set x 0 = EMPTY) /\ 254 (variant_set x (SUC k) = (mk_variant x k) INSERT 255 (variant_set x k))���); 256 257val IN_variant_set = store_thm 258 ("IN_variant_set", 259 ���!m x y. (y IN variant_set x m) 260 = (?n. (n < m) /\ (y = mk_variant x n))���, 261 INDUCT_TAC 262 THEN ASM_REWRITE_TAC[variant_set,IN,NOT_LESS_0,LESS_THM] 263 THEN REPEAT STRIP_TAC 264 THEN EQ_TAC 265 THENL 266 [ REPEAT STRIP_TAC THENL 267 [ EXISTS_TAC ���m:num��� THEN 268 ASM_REWRITE_TAC[], 269 270 EXISTS_TAC ���n:num��� THEN 271 ASM_REWRITE_TAC[] 272 ], 273 274 REPEAT STRIP_TAC THENL 275 [ ASM_REWRITE_TAC[], 276 277 DISJ2_TAC THEN 278 EXISTS_TAC ���n:num��� THEN 279 ASM_REWRITE_TAC[] 280 ] 281 ] 282 ); 283 284 285val FINITE_variant_set = store_thm 286 ("FINITE_variant_set", 287 ���!m x. FINITE (variant_set x m)���, 288 INDUCT_TAC 289 THEN REWRITE_TAC[variant_set] 290 THEN ASM_REWRITE_TAC[FINITE_EMPTY,FINITE_INSERT] 291 ); 292 293 294val FINITE_SL = store_thm 295 ("FINITE_SL", 296 ���!l:('a)list. FINITE (SL l)���, 297 LIST_INDUCT_TAC 298 THEN REWRITE_TAC[SL] 299 THEN ASM_REWRITE_TAC[FINITE_EMPTY,FINITE_INSERT] 300 ); 301 302 303val CARD_variant_set = store_thm 304 ("CARD_variant_set", 305 ���!m x. CARD (variant_set x m) = m���, 306 INDUCT_TAC 307 THEN REWRITE_TAC[variant_set,CARD_DEF] 308 THEN GEN_TAC 309 THEN DEP_REWRITE_TAC[CONJUNCT2 CARD_DEF] 310 THEN REWRITE_TAC[FINITE_variant_set] 311 THEN REWRITE_TAC[IN_variant_set,mk_variant_equal] 312 THEN COND_CASES_TAC 313 THENL [POP_ASSUM STRIP_ASSUME_TAC 314 THEN IMP_RES_TAC EQ_SYM 315 THEN IMP_RES_TAC LESS_NOT_EQ, 316 317 ASM_REWRITE_TAC[] 318 ] 319 ); 320 321 322(* =================================================================== *) 323(* We need to be able to detect when a variable is a variant of *) 324(* another variable, and when it is the *minimum* such variant, *) 325(* subject to the condition that it not be a member of a given set of *) 326(* forbidden variables. *) 327(* =================================================================== *) 328 329 330(* ======================================================= *) 331(* Here finally is the definition of the variant function. *) 332(* "variant x s" is a string with x as its prefix, but *) 333(* with some number appended to x. This variant is *) 334(* guaranteed to not be in s, and to be the smallest *) 335(* such variant (with the least index appended). *) 336(* ======================================================= *) 337 338val variant_EXISTS = 339 TAC_PROOF 340 (([], ���!x s. ?y. 341 FINITE s ==> 342 (y IN variant_set x (SUC(CARD s)) /\ ~(y IN s)) 343 /\ !z. z IN variant_set x (SUC(CARD s)) /\ ~(z IN s) ==> 344 (Index y <= Index z)���), 345 REWRITE_TAC[GSYM IN_DIFF] 346 THEN CONV_TAC (ONCE_DEPTH_CONV EXISTS_IMP_CONV) 347 THEN REWRITE_TAC[GSYM SET_MINIMUM] 348 THEN REWRITE_TAC[MEMBER_NOT_EMPTY] 349 THEN REPEAT GEN_TAC 350 THEN STRIP_TAC 351 THEN DEP_REWRITE_TAC[GSYM CARD_EQ_0] 352 THEN CONJ_TAC 353 THENL 354 [ MATCH_MP_TAC FINITE_DIFF 355 THEN REWRITE_TAC[FINITE_variant_set], 356 357 ONCE_REWRITE_TAC[EQ_SYM_EQ] 358 THEN MATCH_MP_TAC LESS_NOT_EQ 359 THEN DEP_REWRITE_TAC[IMP2AND 360 (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV) LESS_CARD_DIFF)] 361 THEN ASM_REWRITE_TAC[FINITE_variant_set,CARD_variant_set, 362 LESS_SUC_REFL] 363 ] 364 ); 365 366 367 368local 369open Rsyntax 370in 371val variant = 372 let val th1 = CONV_RULE SKOLEM_CONV variant_EXISTS in 373 new_specification 374 {name = "variant", 375 consts = [{const_name = "variant", fixity = NONE (*700*)}], 376 sat_thm = th1} 377 end 378end; 379 380 381 382(* variant = 383 |- !x s. 384 FINITE s ==> 385 (variant x s IN variant_set x (SUC (CARD s)) /\ 386 ~(variant x s IN s)) /\ 387 (!z. 388 z IN variant_set x (SUC (CARD s)) /\ ~(z IN s) ==> 389 Index (variant x s) <= Index z) : thm 390*) 391 392 393(* We may want to use any of these three properties specifically. *) 394(* The next three corollaries select each property. *) 395(* We prove two versions of each, one for general finite sets, *) 396(* and one for sets made using the SL function on a list, which *) 397(* is guarranteed to be finite. *) 398 399 400val variant_in_variant_set = store_thm 401 ("variant_in_variant_set", 402 ���!x s. FINITE s ==> (variant x s) IN (variant_set x (SUC(CARD s)))���, 403 REPEAT STRIP_TAC 404 THEN IMP_RES_THEN REWRITE_THM variant 405 ); 406 407 408val variant_not_in_set = store_thm 409 ("variant_not_in_set", 410 ���!x s. FINITE s ==> ~(variant x s IN s)���, 411 REPEAT GEN_TAC 412 THEN STRIP_TAC 413 THEN IMP_RES_THEN REWRITE_THM variant 414 ); 415 416 417val variant_minimum = store_thm 418 ("variant_minimum", 419 ���!x s y. FINITE s /\ y IN (variant_set x (SUC(CARD s))) /\ ~(y IN s) ==> 420 (Index(variant x s)) <= (Index y)���, 421 REPEAT GEN_TAC 422 THEN STRIP_TAC 423 THEN IMP_RES_TAC variant 424 ); 425 426 427 428val variant_not_in_subset = store_thm 429 ("variant_not_in_subset", 430 ���!x s t. FINITE s /\ t SUBSET s ==> ~(variant x s IN t)���, 431 REPEAT GEN_TAC 432 THEN STRIP_TAC 433 THEN IMP_RES_THEN (ASSUME_TAC o SPEC_ALL) variant_not_in_set 434 THEN IMP_RES_TAC NOT_IN_SUBSET 435 ); 436 437val variant_is_variant = store_thm 438 ("variant_is_variant", 439 ���!x s. FINITE s ==> (variant x s) is_variant x���, 440 REPEAT GEN_TAC 441 THEN STRIP_TAC 442 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 443 (REWRITE_RULE[IN_variant_set] variant_in_variant_set) 444 THEN ASM_REWRITE_TAC[mk_variant_is_variant] 445 ); 446 447 448(* Now we wish to express the variant definition more simply, *) 449(* by just saying that the variant selected is just a variant, *) 450(* without referring to any variant-sets. *) 451 452 453val variant_DEF = store_thm 454 ("variant_DEF", 455 ���!x s. 456 FINITE s ==> 457 ((variant x s) is_variant x /\ ~((variant x s) IN s)) 458 /\ !z. z is_variant x /\ ~(z IN s) ==> 459 (Index (variant x s) <= Index z)���, 460 REPEAT GEN_TAC 461 THEN STRIP_TAC 462 THEN IMP_RES_THEN REWRITE_THM variant 463 THEN IMP_RES_THEN REWRITE_THM variant_is_variant 464 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL o 465 REWRITE_RULE[IN_variant_set]) 466 variant_in_variant_set 467 THEN REWRITE_TAC[is_variant_SOME_mk_variant] 468 THEN REPEAT STRIP_TAC 469 THEN DISJ_CASES_TAC (SPECL [���k:num���, 470 ���SUC(CARD (s:var -> bool))���] LESS_CASES) 471 THENL 472 [ MATCH_MP_TAC variant_minimum 473 THEN ASM_REWRITE_TAC[IN_variant_set] 474 THEN EXISTS_TAC ���k:num��� 475 THEN ASM_REWRITE_TAC[], 476 477 ASM_REWRITE_TAC[Index_mk_variant] 478 THEN ONCE_REWRITE_TAC[ADD_SYM] 479 THEN REWRITE_TAC[LESS_EQ_MONO_ADD_EQ] 480 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 481 THEN IMP_RES_TAC LESS_EQ_TRANS 482 ] 483 ); 484 485 486val variant_minimum_DEF = store_thm 487 ("variant_minimum_DEF", 488 ���!x s y. FINITE s /\ y is_variant x /\ ~(y IN s) ==> 489 (Index(variant x s) <= Index y)���, 490 REPEAT STRIP_TAC 491 THEN IMP_RES_TAC variant_DEF 492 ); 493 494 495val variant_is_variant = store_thm 496 ("variant_is_variant", 497 ���!x s. FINITE s ==> (variant x s) is_variant x���, 498 REPEAT GEN_TAC 499 THEN STRIP_TAC 500 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 501 (REWRITE_RULE[IN_variant_set] variant_in_variant_set) 502 THEN ASM_REWRITE_TAC[mk_variant_is_variant] 503 ); 504 505 506 507(* =============================================================== *) 508(* Now we need to prove that the variant function as defined above *) 509(* satisfies the three properties that we require: *) 510(* *) 511(* 1. the variant is a real variant of the original variable; *) 512(* *) 513(* 2. the variant is not a member of the exclusion list; and *) 514(* *) 515(* 3. the variant is the minimum such variant, as reckoned by *) 516(* its Index. *) 517(* =============================================================== *) 518 519 520val Base_variant = store_thm 521 ("Base_variant", 522 ���!x s. FINITE s ==> (Base (variant x s) = Base x)���, 523 REPEAT STRIP_TAC 524 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 525 (REWRITE_RULE[is_variant] variant_is_variant) 526 ); 527 528val Index_variant = store_thm 529 ("Index_variant", 530 ���!x s. FINITE s ==> Index x <= Index (variant x s)���, 531 REPEAT STRIP_TAC 532 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 533 (REWRITE_RULE[is_variant] variant_is_variant) 534 ); 535 536 537val variant_EMPTY = store_thm 538 ("variant_EMPTY", 539 ���!x. variant x EMPTY = x���, 540 GEN_TAC 541 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY) 542 THEN IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 543 (REWRITE_RULE[is_variant] variant_is_variant) 544 THEN STRIP_ASSUME_TAC (SPEC_ALL is_variant_reflexive) 545 THEN MATCH_MP_TAC VAR_EQ_IMP 546 THEN ASM_REWRITE_TAC[] 547 THEN MATCH_MP_TAC LESS_EQUAL_ANTISYM 548 THEN ASM_REWRITE_TAC[] 549 THEN MATCH_MP_TAC variant_minimum 550 THEN REWRITE_TAC[IN_variant_set,FINITE_EMPTY,IN] 551 THEN EXISTS_TAC ���0��� 552 THEN REWRITE_TAC[LESS_0] 553 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 554 THEN REWRITE_TAC[mk_variant_ident] 555 ); 556 557 558val LESS_EQ_NOT_EQ = store_thm 559 ("LESS_EQ_NOT_EQ", 560 ���!m n. m <= n /\ ~(m = n) ==> (m+1) <= n���, 561 REWRITE_TAC[SYM(SPEC_ALL ADD1),SYM(SPEC_ALL LESS_EQ)] 562 THEN REWRITE_TAC[LESS_OR_EQ] 563 THEN REPEAT GEN_TAC 564 THEN STRIP_TAC 565 THEN RES_TAC 566 ); 567 568 569val SET_IN_OUT = 570 TAC_PROOF 571 (([], ���!(x:'a) y s. (x IN s) /\ ~(y IN s) ==> ~(x = y)���), 572 REPEAT STRIP_TAC 573 THEN UNDISCH_TAC ���(x:'a) IN s��� 574 THEN ASM_REWRITE_TAC[] 575 ); 576 577 578val variant_not_ident = store_thm 579 ("variant_not_ident", 580 ���!x s. FINITE s /\ (x IN s) ==> ~(x = variant x s)���, 581 REPEAT GEN_TAC 582 THEN STRIP_TAC 583 THEN MATCH_MP_TAC SET_IN_OUT 584 THEN EXISTS_TAC ���s:var -> bool��� 585 THEN ASM_REWRITE_TAC[] 586 THEN MATCH_MP_TAC variant_not_in_set 587 THEN ASM_REWRITE_TAC[] 588 ); 589 590 591val Index_variant_not_ident = store_thm 592 ("Index_variant_not_ident", 593 ���!x s. FINITE s /\ (x IN s) ==> ~(Index x = Index (variant x s))���, 594 REPEAT STRIP_TAC 595 THEN IMP_RES_THEN (ASSUME_TAC o SYM o SPEC_ALL) Base_variant 596 THEN IMP_RES_TAC VAR_EQ 597 THEN IMP_RES_TAC variant_not_ident 598 ); 599 600val variant_mk_variant_is_variant = store_thm 601 ("variant_mk_variant_is_variant", 602 ���!x k s. FINITE s ==> (variant (mk_variant x k) s) is_variant x���, 603 REPEAT STRIP_TAC 604 THEN MATCH_MP_TAC is_variant_TRANS 605 THEN EXISTS_TAC ���mk_variant x k��� 606 THEN IMP_RES_TAC variant_is_variant 607 THEN ASM_REWRITE_TAC[mk_variant_is_variant] 608 ); 609 610val variant_mk_variant_not_ident = store_thm 611 ("variant_mk_variant_not_ident", 612 ���!x s. FINITE s ==> ~(variant (mk_variant x 1) s = x)���, 613 REPEAT GEN_TAC 614 THEN STRIP_TAC 615 THEN ONCE_REWRITE_TAC[SYM(SPEC_ALL Base_Index)] 616 THEN RW_TAC std_ss [] 617 THEN IMP_RES_THEN REWRITE_THM Base_variant 618 THEN REWRITE_TAC[Base_mk_variant] 619 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 620 THEN MATCH_MP_TAC LESS_NOT_EQ 621 THEN REWRITE_TAC[LESS_EQ,ADD1] 622 THEN REWRITE_TAC[SYM(SPEC_ALL Index_mk_variant)] 623 THEN IMP_RES_THEN REWRITE_THM Index_variant 624 ); 625 626 627val variant_THM = store_thm 628 ("variant_THM", 629 ���!x s. FINITE s ==> 630 (variant x s = (if x IN s then variant (mk_variant x 1) s else x))���, 631 REPEAT STRIP_TAC 632 THEN COND_CASES_TAC 633 THEN MATCH_MP_TAC VAR_EQ_IMP 634 THEN IMP_RES_THEN REWRITE_THM Base_variant 635 THEN REWRITE_TAC[Base_mk_variant] 636 THEN MATCH_MP_TAC LESS_EQUAL_ANTISYM 637 THENL 638 [ STRIP_TAC 639 THEN MATCH_MP_TAC variant_minimum_DEF 640 THEN IMP_RES_THEN REWRITE_THM variant_not_in_set 641 THEN IMP_RES_THEN ASM_REWRITE_THM variant_mk_variant_is_variant 642 THEN REWRITE_TAC[is_variant] 643 THEN IMP_RES_THEN REWRITE_THM Base_variant 644 THEN REWRITE_TAC[Base_mk_variant,Index_mk_variant] 645 THEN MATCH_MP_TAC LESS_EQ_NOT_EQ 646 THEN IMP_RES_THEN REWRITE_THM Index_variant 647 THEN IMP_RES_TAC Index_variant_not_ident, 648 649 STRIP_TAC 650 THENL 651 [ 652 MATCH_MP_TAC variant_minimum_DEF 653 THEN ASM_REWRITE_TAC[is_variant_reflexive], 654 655 IMP_RES_THEN REWRITE_THM Index_variant 656 ] 657 ] 658 ); 659 660 661val variant_ident = 662 store_thm 663 ("variant_ident", 664 ���!x s. FINITE s /\ ~(x IN s) ==> (variant x s = x)���, 665 REPEAT STRIP_TAC THEN 666 IMP_RES_THEN ONCE_REWRITE_THM variant_THM THEN 667 ASM_REWRITE_TAC[] 668 ); 669 670 671val variant_DELETE = 672 store_thm 673 ("variant_DELETE", 674 ���!x s. FINITE s ==> (variant x (s DELETE x) = x)���, 675 REPEAT STRIP_TAC THEN 676 MATCH_MP_TAC variant_ident THEN 677 ASM_REWRITE_TAC[FINITE_DELETE,IN_DELETE] 678 ); 679 680 681val variant_increment = 682 store_thm 683 ("variant_increment", 684 ���!x s. 685 FINITE s /\ (x IN s) ==> (variant x s = variant (mk_variant x 1) s)���, 686 REPEAT STRIP_TAC 687 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM 688 THEN ASM_REWRITE_TAC[] 689 ); 690 691 692 693(* We define the function 'variants', to take a list of variables *) 694(* and form a list of variants of the variables in the list, with *) 695(* the provision that the list produced should have no duplicates. *) 696 697 698fun new_list_rec_def name tm = 699 new_recursive_definition 700 {rec_axiom = list_Axiom, 701 name = name, 702 def = tm}; 703 704val variants = 705 new_list_rec_def "variants" 706 ���(variants NIL s = NIL) /\ 707 (variants (CONS x xs) s = 708 (let x' = variant x s in 709 (CONS x' (variants xs (x' INSERT s)))))���; 710 711(* Alternative definition of variants: 712 713val variants = 714 new_list_rec_def "variants" 715 ���(variants NIL s = NIL) /\ 716 (variants (CONS x xs) s = 717 (let xs' = variants xs s in 718 (CONS (variant x (SL xs' UNION s)) xs')))���; 719*) 720 721 722val variants_THM = 723 store_thm 724 ("variants_THM", 725 ���(variants NIL s = NIL) /\ 726 (variants (CONS x xs) s = 727 (CONS (variant x s) (variants xs ((variant x s) INSERT s))))���, 728 REWRITE_TAC[variants] 729 THEN CONV_TAC (DEPTH_CONV let_CONV) 730 THEN REFL_TAC 731 ); 732 733 734val NOT_IN_variants_INSERT = 735 store_thm 736 ("NOT_IN_variants_INSERT", 737 ���!xs y s. FINITE s ==> ~(y IN SL (variants xs (y INSERT s)))���, 738 LIST_INDUCT_TAC 739 THEN REWRITE_TAC[variants_THM,SL,IN,DE_MORGAN_THM] 740 THEN REPEAT GEN_TAC 741 THEN STRIP_TAC 742 THEN STRIP_TAC 743 THENL 744 [ MATCH_MP_TAC IN_NOT_IN 745 THEN EXISTS_TAC ���(y:var) INSERT s��� 746 THEN REWRITE_TAC[COMPONENT] 747 THEN MATCH_MP_TAC variant_not_in_set 748 THEN ASM_REWRITE_TAC[FINITE_INSERT], 749 750 ONCE_REWRITE_TAC[INSERT_COMM] 751 THEN FIRST_ASSUM MATCH_MP_TAC 752 THEN ASM_REWRITE_TAC[FINITE_INSERT] 753 ] 754 ); 755 756 757val variants_APPEND = 758 store_thm 759 ("variants_APPEND", 760 ���!x y s. 761 variants (APPEND x y) s = 762 APPEND (variants x s) (variants y (SL(variants x s) UNION s))���, 763 LIST_INDUCT_TAC 764 THEN REWRITE_TAC[variants_THM,SL,APPEND,UNION] 765 THEN REPEAT STRIP_TAC 766 THEN ASM_REWRITE_TAC[CONS_11] 767 THEN ONCE_REWRITE_TAC[UNION_COMM] 768 THEN REWRITE_TAC[UNION] 769 ); 770 771 772val DISJOINT_variants = 773 store_thm 774 ("DISJOINT_variants", 775 ���!x s. FINITE s ==> (DISJOINT (SL (variants x s)) s)���, 776 LIST_INDUCT_TAC 777 THEN REWRITE_TAC[variants_THM,SL,DISJOINT_EMPTY,DISJOINT_INSERT] 778 THEN REPEAT GEN_TAC 779 THEN DISCH_TAC 780 THEN IMP_RES_THEN REWRITE_THM variant_not_in_set 781 THEN FIRST_ASSUM (MP_TAC o SPEC ���(variant x' s) INSERT s���) 782 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 783 THEN ASM_REWRITE_TAC[DISJOINT_INSERT,FINITE_INSERT] 784 THEN DISCH_THEN REWRITE_THM 785 ); 786 787val DISJOINT_variants_SL = 788 store_thm 789 ("DISJOINT_variants_SL", 790 ���!x l. DISJOINT (SL (variants x (SL l))) (SL l)���, 791 REPEAT STRIP_TAC 792 THEN MATCH_MP_TAC DISJOINT_variants 793 THEN REWRITE_TAC[FINITE_SL] 794 ); 795 796 797 798val DL_variants = 799 store_thm 800 ("DL_variants", 801 ���!x s. FINITE s ==> DL (variants x s)���, 802 LIST_INDUCT_TAC 803 THEN REWRITE_TAC[variants_THM,DL] 804 THEN REPEAT GEN_TAC 805 THEN DISCH_TAC 806 THEN IMP_RES_THEN REWRITE_THM NOT_IN_variants_INSERT 807 THEN FIRST_ASSUM MATCH_MP_TAC 808 THEN ASM_REWRITE_TAC[FINITE_INSERT] 809 ); 810 811val DL_variants_SL = 812 store_thm 813 ("DL_variants_SL", 814 ���!x l. DL (variants x (SL l))���, 815 REPEAT STRIP_TAC 816 THEN MATCH_MP_TAC DL_variants 817 THEN REWRITE_TAC[FINITE_SL] 818 ); 819 820 821val LENGTH_variants = 822 store_thm 823 ("LENGTH_variants", 824 ���!x s. LENGTH (variants x s) = LENGTH x���, 825 LIST_INDUCT_TAC 826 THEN ASM_REWRITE_TAC[variants_THM,LENGTH] 827 ); 828 829 830val NOT_IN_variants = 831 store_thm 832 ("NOT_IN_variants", 833 ���!x y s. FINITE s /\ y IN s ==> ~(y IN SL (variants x s))���, 834 REPEAT GEN_TAC THEN STRIP_TAC 835 THEN IMP_RES_THEN (ASSUME_TAC o SPEC_ALL) DISJOINT_variants 836 THEN IMP_RES_TAC IN_DISJOINT_IMP 837 ); 838 839 840val DISJOINT_variants_UNION = 841 store_thm 842 ("DISJOINT_variants_UNION", 843 ���!x s t. 844 FINITE s /\ FINITE t ==> 845 DISJOINT (SL(variants x (s UNION t))) s /\ 846 DISJOINT (SL(variants x (s UNION t))) t���, 847 REPEAT GEN_TAC 848 THEN STRIP_TAC 849 THEN (MP_TAC o SPECL[���x:(var)list���,���(s:(var)-> bool) UNION t���]) 850 DISJOINT_variants 851 THEN ASM_REWRITE_TAC[FINITE_UNION] 852 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 853 THEN REWRITE_TAC[DISJOINT_UNION] 854 ); 855 856 857val DISJOINT_variants_APPEND = 858 store_thm 859 ("DISJOINT_variants_APPEND", 860 ���!x a b. 861 DISJOINT (SL (variants x (SL (APPEND a b)))) (SL a) /\ 862 DISJOINT (SL (variants x (SL (APPEND a b)))) (SL b) ���, 863 REPEAT GEN_TAC 864 THEN REWRITE_TAC[SL_APPEND] 865 THEN MATCH_MP_TAC DISJOINT_variants_UNION 866 THEN REWRITE_TAC[FINITE_SL] 867 ); 868 869 870val DISJOINT_variants_UNION1 = 871 store_thm 872 ("DISJOINT_variants_UNION1", 873 ���!x s t. 874 FINITE s /\ FINITE t ==> 875 DISJOINT (SL (variants x (s UNION t))) s���, 876 REPEAT STRIP_TAC 877 THEN IMP_RES_TAC DISJOINT_variants_UNION 878 THEN ASM_REWRITE_TAC[] 879 ); 880 881 882val DISJOINT_variants_UNION2 = 883 store_thm 884 ("DISJOINT_variants_UNION2", 885 ���!x s t. 886 FINITE s /\ FINITE t ==> 887 DISJOINT (SL (variants x (s UNION t))) t���, 888 REPEAT STRIP_TAC 889 THEN IMP_RES_TAC DISJOINT_variants_UNION 890 THEN ASM_REWRITE_TAC[] 891 ); 892 893 894val DISJOINT_variants_UNION3 = 895 store_thm 896 ("DISJOINT_variants_UNION3", 897 ���!x s t u. 898 FINITE s /\ FINITE t /\ FINITE u ==> 899 DISJOINT (SL(variants x (s UNION (t UNION u)))) s /\ 900 DISJOINT (SL(variants x (s UNION (t UNION u)))) t /\ 901 DISJOINT (SL(variants x (s UNION (t UNION u)))) u /\ 902 DISJOINT s (SL(variants x (s UNION (t UNION u)))) /\ 903 DISJOINT t (SL(variants x (s UNION (t UNION u)))) /\ 904 DISJOINT u (SL(variants x (s UNION (t UNION u))))���, 905 REPEAT GEN_TAC 906 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 907 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 908 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 909 THEN REWRITE_TAC[DISJOINT_UNION] 910 THEN STRIP_TAC 911 THEN ASM_REWRITE_TAC[] 912 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 913 THEN ASM_REWRITE_TAC[] 914 ); 915 916val DISJOINT_variants_UNION_LEFT_1 = 917 store_thm 918 ("DISJOINT_variants_UNION_LEFT_1", 919 ���!x s t u. 920 FINITE s /\ FINITE t /\ FINITE u ==> 921 DISJOINT (SL(variants x (s UNION (t UNION u)))) s���, 922 REPEAT GEN_TAC 923 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 924 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 925 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 926 THEN REWRITE_TAC[DISJOINT_UNION] 927 THEN STRIP_TAC 928 ); 929 930val DISJOINT_variants_UNION_LEFT_2 = 931 store_thm 932 ("DISJOINT_variants_UNION_LEFT_2", 933 ���!x s t u. 934 FINITE s /\ FINITE t /\ FINITE u ==> 935 DISJOINT (SL(variants x (s UNION (t UNION u)))) t���, 936 REPEAT GEN_TAC 937 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 938 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 939 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 940 THEN REWRITE_TAC[DISJOINT_UNION] 941 THEN STRIP_TAC 942 ); 943 944val DISJOINT_variants_UNION_LEFT_3 = 945 store_thm 946 ("DISJOINT_variants_UNION_LEFT_3", 947 ���!x s t u. 948 FINITE s /\ FINITE t /\ FINITE u ==> 949 DISJOINT (SL(variants x (s UNION (t UNION u)))) u���, 950 REPEAT GEN_TAC 951 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 952 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 953 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 954 THEN REWRITE_TAC[DISJOINT_UNION] 955 THEN STRIP_TAC 956 ); 957 958val DISJOINT_variants_UNION_RIGHT_1 = 959 store_thm 960 ("DISJOINT_variants_UNION_RIGHT_1", 961 ���!x s t u. 962 FINITE s /\ FINITE t /\ FINITE u ==> 963 DISJOINT s (SL(variants x (s UNION (t UNION u))))���, 964 REPEAT GEN_TAC 965 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 966 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 967 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 968 THEN REWRITE_TAC[DISJOINT_UNION] 969 THEN STRIP_TAC 970 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 971 THEN ASM_REWRITE_TAC[] 972 ); 973 974val DISJOINT_variants_UNION_RIGHT_2 = 975 store_thm 976 ("DISJOINT_variants_UNION_RIGHT_2", 977 ���!x s t u. 978 FINITE s /\ FINITE t /\ FINITE u ==> 979 DISJOINT t (SL(variants x (s UNION (t UNION u))))���, 980 REPEAT GEN_TAC 981 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 982 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 983 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 984 THEN REWRITE_TAC[DISJOINT_UNION] 985 THEN STRIP_TAC 986 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 987 THEN ASM_REWRITE_TAC[] 988 ); 989 990val DISJOINT_variants_UNION_RIGHT_3 = 991 store_thm 992 ("DISJOINT_variants_UNION_RIGHT_3", 993 ���!x s t u. 994 FINITE s /\ FINITE t /\ FINITE u ==> 995 DISJOINT u (SL(variants x (s UNION (t UNION u))))���, 996 REPEAT GEN_TAC 997 THEN REWRITE_TAC[(SYM o SPEC_ALL) FINITE_UNION] 998 THEN DISCH_THEN (MP_TAC o SPEC_ALL o MATCH_MP DISJOINT_variants) 999 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 1000 THEN REWRITE_TAC[DISJOINT_UNION] 1001 THEN STRIP_TAC 1002 THEN ONCE_REWRITE_TAC[DISJOINT_SYM] 1003 THEN ASM_REWRITE_TAC[] 1004 ); 1005 1006 1007val _ = export_theory(); 1008 1009val _ = print_theory_to_file "-" "variable.lst"; 1010 1011val _ = html_theory "variable"; 1012 1013val _ = print_theory_size(); 1014