1% Rules for unfolding, unwinding, pruning etc. % 2 3% Rules for unfolding % 4 5% 6 A1 |- t1 = t1' , ... , An |- tn = tn' 7 --------------------------------------------------------- 8 A1 u ... u An |- (t1 /\ ... /\ tn) = (t1' /\ ... /\ tn') 9% 10 11letrec MK_CONJL thl = 12 (if null thl 13 then fail 14 if null(tl thl) 15 then hd thl 16 else 17 (let th = MK_CONJL(tl thl) 18 in 19 let t1,() = dest_eq(concl(hd thl)) 20 and (),t2' = dest_eq(concl th) 21 in 22 (AP_TERM "$/\ ^t1" th) TRANS (AP_THM (AP_TERM "$/\" (hd thl)) t2')) 23 ) ? failwith `MK_CONJL`;; 24 25% 26 A1 |- t1 = t1' , ... , An |- tn = tn' 27 -------------------------------------------------- 28 A1 u ... u An |- ?l1 ... lm. t1 /\ ... /\ tn = 29 ?l1 ... lm. t1' /\ ... /\ tn' 30% 31 32let UNFOLD thl = 33 let net = mk_conv_net thl 34 in 35 \t. 36 ((let vars, eqs = strip_exists t 37 and rewrite = REWRITES_CONV net 38 in 39 LIST_MK_EXISTS vars (MK_CONJL(map rewrite (conjuncts eqs))) 40 ) ? failwith `UNFOLD`);; 41 42% 43 44 A1 |- t1 = t1' , ... , An |- tn = tn' 45 46 A |- t = (?l1 ... lm. t1 /\ ... /\ tn) 47 ------------------------------------------ 48 A |- t = (?l1 ... lm. t1' /\ ... /\ tn') 49% 50 51let UNFOLD_RULE thl th = 52 RIGHT_CONV_RULE (UNFOLD(map SPEC_ALL thl)) (SPEC_ALL th) 53 ? failwith`UNFOLD_RULE`;; 54 55% 56 |- (x1 = t1) /\ ... (xm = tm) /\ ... /\ (xn = tn) = 57 (x1 = t1') /\ ... /\ (x[m-1] = t[m-1]') /\ (xm = tm) /\ ... /\ (xn = tn) 58 59where: 60 61 1. ti' = ti[tm,...,tn/xm,...,xn] 62 63 2. none of x1,...,xn are free in any of tm,...,tn 64 (the xi's need not be variables) 65 66 3. not all of the terms in the conjunction have to be equations 67 (only the equations are used in unwinding) 68 69In fact, the equations (xi = ti) (where i is between m and n) 70can occur anywhere - they don't have to be bunched up at the right 71hand end. 72 73let OLD_UNWIND_ONCE_CONV t = 74 (let eqns = conjuncts t 75 in 76 letrec check_frees l t = 77 (if null l then false 78 if free_in(hd l)t then true else check_frees (tl l) t) 79 in 80 let lefts = mapfilter lhs eqns 81 in 82 let l1,l2 = partition (\t. check_frees lefts (rhs t) ? true) eqns 83 in 84 if null l1 85 then REFL(list_mk_conj l2) 86 else 87 (let th1 = end_itlist CONJ (map ASSUME l2) 88 in 89 let subs_list = map 90 (\th. (th, genvar(type_of(lhs(concl th))))) 91 (CONJUNCTS th1) 92 in 93 let rn_list = map (\(th,v).(v,lhs(concl th))) subs_list 94 in 95 let subs_fn t = 96 (mk_eq o (I # subst rn_list) o dest_eq) t ? subst rn_list t 97 in 98 let th2 = SUBST_CONV 99 subs_list 100 (list_mk_conj 101 (map subs_fn l1)) 102 (list_mk_conj l1) 103 in 104 let th3 = CONJ_DISCHL l2 th2 105 in 106 let th4 = CONJUNCTS_CONV(t, lhs(concl th3)) 107 in 108 (th4 TRANS th3)) 109 ) ? failwith `OLD_UNWIND_ONCE_CONV`;; 110 111% 112 113let OLD_UNWIND_ONCE_CONV t = 114 (let eqns = conjuncts t 115 in 116 letrec check_frees l t = %any member of l free in t?% 117 (if null l then false 118 if free_in(hd l)t then true else check_frees (tl l) t) 119 in 120 let lefts = mapfilter lhs eqns 121 in 122 let l1,l2 = partition (\t. check_frees lefts (rhs t) ? true) eqns 123 in 124 if null l1 125 then REFL(list_mk_conj eqns) 126 else 127 (let subs_fun = subst(map(flip o dest_eq)l2) 128 in 129 let l1' = map ((mk_eq o (I # subs_fun) o dest_eq) orelsef subs_fun) l1 130 in 131 mk_thm([], mk_eq(t, list_mk_conj(l1'@l2)))) 132 ) ? failwith `OLD_UNWIND_ONCE_CONV`;; 133 134% Unwind until no change - may loop! 135 136letrec UNWIND_EQS eqs = 137 let th = OLD_UNWIND_ONCE_CONV eqs 138 in 139 if lhs(concl th)=rhs(concl th) 140 then th 141 else th TRANS (UNWIND_EQS(rhs(concl th)));; 142% 143 144letrec UNWIND_EQS eqs = 145 (let th = OLD_UNWIND_ONCE_CONV eqs 146 in 147 let t1,t2 = dest_eq(concl th) 148 in 149 if t1 = t2 150 then th 151 else mk_thm([],mk_eq(t1, rhs(concl(UNWIND_EQS t2)))) 152 ) ? failwith`UNWIND_EQS`;; 153 154% 155 |- (?l1 ... lm. x1 = t1 /\ ... /\ xn = tn) = 156 (?l1 ... lm. x1 = t1' /\ ... /\ xn = tn') 157 158Where t1',...,tn' are got from t1,...,tn by unwinding using the equations 159% 160 161let UNWIND t = 162 let l,eqs = strip_exists t 163 in 164 LIST_MK_EXISTS l (UNWIND_EQS eqs);; 165 166let OLD_UNWIND_RULE th = 167 RIGHT_CONV_RULE UNWIND th ? failwith `OLD_UNWIND_RULE`;; 168 169% 170 "(!x. t1) /\ ... /\ (!x. tn)" ---> 171 |- (!x. t1) /\ ... /\ (!x. tn) = !x. t1 /\ ... /\ tn 172 173let AND_FORALL_CONV t = 174 (let xt1,xt2 = dest_conj t 175 in 176 let x = fst(dest_forall xt1) 177 in 178 let thl1 = CONJUNCTS(ASSUME t) 179 in 180 let th1 = DISCH_ALL(GEN x (LIST_CONJ(map(SPEC x)thl1))) 181 in 182 let thl2 = 183 CONJUNCTS 184 (SPEC x 185 (ASSUME 186 (mk_forall(x,(list_mk_conj(map(snd o dest_forall o concl)thl1)))))) 187 in 188 let th2 = DISCH_ALL(LIST_CONJ(map (GEN x) thl2)) 189 in 190 IMP_ANTISYM_RULE th1 th2 191 ) ? failwith `AND_FORALL_CONV`;; 192% 193 194% "(!x. t1) /\ ... /\ (!x. tn)" ---> ("x", ["t1"; ... ;"tn"]) % 195 196letrec dest_andl t = 197 ((let x1,t1 = dest_forall t 198 in 199 (x1,[t1]) 200 ) 201 ? 202 (let first,rest = dest_conj t 203 in 204 let x1,l1 = dest_andl first 205 and x2,l2 = dest_andl rest 206 in 207 if x1=x2 then (x1, l1@l2) else fail) 208 ) ? failwith `dest_andl`;; 209 210% Version of AND_FORALL_CONV below will pull quantifiers out and flatten an 211 arbitrary tree of /\s, not just a linear list. % 212 213let AND_FORALL_CONV t = 214 (let x,l = dest_andl t 215 in 216 mk_thm([], mk_eq(t,mk_forall(x,list_mk_conj l))) 217 ) ? failwith `AND_FORALL_CONV`;; 218 219% 220 "!x. t1 /\ ... /\ tn" ---> 221 |- !x. t1 /\ ... /\ tn = (!x. t1) /\ ... /\ (!x. tn) 222 223let FORALL_AND_CONV t = 224 (let x,l = ((I # conjuncts) o dest_forall) t 225 in 226 SYM(AND_FORALL_CONV(list_mk_conj(map(curry mk_forall x)l))) 227 ) ? failwith `AND_FORALL_CONV`;; 228% 229 230let FORALL_AND_CONV t = 231 (let x,l = ((I # conjuncts) o dest_forall) t 232 in 233 mk_thm([],mk_eq(t, list_mk_conj(map(curry mk_forall x)l))) 234 ) ? failwith `FORALL_AND_CONV`;; 235 236% 237 |- (?l1 ... lm. (!x. x1 = t1) /\ ... /\ (!x. xn = tn)) = 238 (?l1 ... lm. (!x. x1 = t1') /\ ... /\ (!x. xn = tn')) 239 240Where t1',...,tn' are got from t1,...,tn by unwinding using the equations: 241 242 x1 = t1 /\ ... /\ xn = tn 243 244% 245 246let UNWINDF t = 247 (let l,body = strip_exists t 248 in 249 let th1 = AND_FORALL_CONV body 250 in 251 let x,eqs = dest_forall(rhs(concl th1)) 252 in 253 let th2 = FORALL_EQ x (UNWIND_EQS eqs) 254 in 255 let th3 = FORALL_AND_CONV(rhs(concl th2)) 256 in 257 LIST_MK_EXISTS l (th1 TRANS th2 TRANS th3) 258 ) ? failwith `UNWINDF`;; 259 260let UNWINDF_RULE th = RIGHT_CONV_RULE UNWINDF th ? failwith `UNWINDF_RULE`;; 261 262% 263 A |- t1 = t2 264 -------------- (t2' got from t2 by unwinding) 265 A |- t1 = t2' 266% 267 268% The next lot of rules are for pruning % 269 270% EXISTS_AND_LEFT: term -> thm 271 "?x.t1/\t2" 272 273 | - ?x. t1 /\ t2 = t1 /\ (?x. t2)" (If x not free in t1) 274% 275 276let EXISTS_AND_LEFT t = 277 (let x,t1,t2 = ((I # dest_conj) o dest_exists) t 278 in 279 let t1_frees, t2_frees = frees t1, frees t2 280 in 281 if not(mem x t2_frees & not(mem x t1_frees)) 282 then fail 283 else 284 (let th1 = ASSUME "^t1 /\ ^t2" 285 and t' = "^t1 /\ (?^x.^t2)" 286 in 287 let th2 = ASSUME t' 288 in 289 let th3 = DISCH 290 t 291 (CHOOSE 292 (x, ASSUME t) 293 (CONJ(CONJUNCT1 th1)(EXISTS("?^x.^t2",x)(CONJUNCT2 th1)))) 294 % th3 = |-"?x. t1 /\ t2 ==> t1 /\ (?x. t2)" % 295 and th4 = DISCH 296 t' 297 (CHOOSE 298 (x, CONJUNCT2 th2) 299 (EXISTS(t,x)(CONJ(CONJUNCT1 th2)(ASSUME t2)))) 300 % th4 = |-"t1 /\ (?x. t2) ==> ?x. t1 /\ t2" % 301 in 302 IMP_ANTISYM_RULE th3 th4) 303 ) ? failwith `EXISTS_AND_LEFT`;; 304 305% EXISTS_AND_RIGHT: term -> thm 306 ?x.t1/\t2 307 308 |- ?x. t1 /\ t2 = (?x. t1) /\ t2" (If x not free in t2) 309% 310 311let EXISTS_AND_RIGHT t = 312 (let x,t1,t2 = ((I # dest_conj) o dest_exists) t 313 in 314 let t1_frees, t2_frees = frees t1, frees t2 315 and th1 = ASSUME "^t1 /\ ^t2" 316 in 317 if not(mem x t1_frees & not(mem x t2_frees)) 318 then fail 319 else 320 (let t' = "(?^x.^t1) /\ ^t2" 321 in 322 let th2 = ASSUME t' 323 in 324 let th3 = DISCH 325 t 326 (CHOOSE 327 (x, ASSUME t) 328 (CONJ(EXISTS("?^x.^t1",x)(CONJUNCT1 th1))(CONJUNCT2 th1))) 329 % th3 = |-"?x. t1 /\ t2 ==> (?x.t1) /\ t2" % 330 and th4 = DISCH 331 t' 332 (CHOOSE 333 (x, CONJUNCT1 th2) 334 (EXISTS(t,x)(CONJ(ASSUME t1)(CONJUNCT2 th2)))) 335 % th4 = |-"(?x.t1) /\ t2 ==> ?x. t1 /\ t2" % 336 in 337 IMP_ANTISYM_RULE th3 th4) 338 ) ? failwith `EXISTS_AND_RIGHT`;; 339 340% EXISTS_AND_BOTH: term -> thm 341 ?x.t1/\t2 342 343 |- ?x. t1 /\ t2 = t1 /\ t2" (If x not free in t1 or t2) 344% 345 346let EXISTS_AND_BOTH t = 347 (let x,t1,t2 = ((I # dest_conj) o dest_exists) t 348 in 349 let t1_frees, t2_frees = frees t1, frees t2 350 and th1 = ASSUME "^t1 /\ ^t2" 351 in 352 if (mem x t2_frees) or (mem x t1_frees) 353 then fail 354 else 355 (let t' = "^t1 /\ ^t2" 356 in 357 let th3 = DISCH 358 t 359 (CHOOSE 360 (x, ASSUME t) 361 (ASSUME t')) 362 % th3 = |-"?x. t1 /\ t2 ==> t1 /\ t2" % 363 and th4 = DISCH 364 t' 365 (EXISTS(t, x)(ASSUME t')) 366 % th4 = |-"t1 /\ t2 ==> ?x. t1 /\ t2" % 367 in IMP_ANTISYM_RULE th3 th4) 368 ) ? failwith `EXISTS_AND_BOTH`;; 369 370% EXISTS_AND: term -> thm 371 ?x.t1/\t2 372 373 |- ?x. t1 /\ t2 = t1 /\ (?x. t2)" (If x not free in t1) 374 375 |- ?x. t1 /\ t2 = (?x. t1) /\ t2" (If x not free in t2) 376 377 |- ?x. t1 /\ t2 = t1 /\ t2" (If x not free in t1 or t2) 378% 379 380let EXISTS_AND t = 381 EXISTS_AND_LEFT t ? 382 EXISTS_AND_RIGHT t ? 383 EXISTS_AND_BOTH t ? 384 failwith`EXISTS_AND`;; 385 386% 387 A |- ?x.?y.t 388 ------------ 389 A |- ?y.?x.t" 390% 391 392let EXISTS_PERM th = 393 let x,y,t = ((I # dest_exists) o dest_exists o concl) th 394 in 395 CHOOSE 396 (x,th) 397 (CHOOSE 398 (y, ASSUME "?^y.^t") 399 (EXISTS("?^y^x.^t",y)(EXISTS("?^x.^t",x)(ASSUME t))));; 400 401% |- (?x y. t) = (?y x.t) % 402 403let EXISTS_PERM_CONV t = 404 (let th1 = EXISTS_PERM(ASSUME t) 405 in 406 let t' = concl th1 407 in 408 IMP_ANTISYM_RULE (DISCH t th1) (DISCH t' (EXISTS_PERM(ASSUME t'))) 409 ) ? failwith`EXISTS_PERM_CONV`;; 410 411% 412 EXISTS_EQN 413 414 "?l. l x1 ... xn = t" --> |- (?l.l x1 ... xn = t) = T 415 416 (if l not free in t) 417% 418 419let EXISTS_EQN t = 420 (let l,t1,t2 = ((I # dest_equiv) o dest_exists) t 421 in 422 let l',xs = strip_comb t1 423 in 424 let t3 = list_mk_abs(xs,t2) 425 in 426 let th1 = RIGHT_CONV_RULE LIST_BETA_CONV (REFL(list_mk_comb(t3,xs))) 427 in 428 EQT_INTRO(EXISTS("?^l.^(list_mk_comb(l,xs))=^(rhs(concl th1))",t3)th1) 429 ) ? failwith `EXISTS_EQN`;; 430 431% 432 EXISTS_EQNF 433 434 "?l. !x1 ... xn. l x1 ... xn = t" --> 435 |- (?l. !x1 ... xn. l x1 ... xn = t) = T 436 437 (if l not free in t) 438% 439 440let EXISTS_EQNF t = 441 (let l,vars,t1,t2 = 442 ((I # (I # dest_eq)) o (I # strip_forall) o dest_exists) t 443 in 444 let l',xs = strip_comb t1 445 in 446 let t3 = list_mk_abs(xs,t2) 447 in 448 let th1 = 449 GENL vars (RIGHT_CONV_RULE LIST_BETA_CONV (REFL(list_mk_comb(t3,xs)))) 450 in 451 EQT_INTRO 452 (EXISTS 453 ((mk_exists 454 (l, 455 list_mk_forall 456 (xs, 457 (mk_eq(list_mk_comb(l,xs), rhs(snd(strip_forall(concl th1)))))))), 458 t3) 459 th1) 460 ) ? failwith `EXISTS_EQNF`;; 461 462 463% |- (?x.t) = t if x not free in t 464 465let EXISTS_DEL1 tm = 466 (let x,t = dest_exists tm 467 in 468 let th1 = DISCH tm (CHOOSE (x, ASSUME tm) (ASSUME t)) 469 and th2 = DISCH t (EXISTS(tm,x)(ASSUME t)) 470 in 471 IMP_ANTISYM_RULE th1 th2 472 ) ? failwith `EXISTS_DEL`;; 473% 474 475% |- (?x1 ... xn.t) = t if x1,...,xn not free in t 476 477letrec EXISTS_DEL tm = 478 (if is_exists tm 479 then 480 (let th1 = EXISTS_DEL1 tm 481 in 482 let th2 = EXISTS_DEL(rhs(concl th1)) 483 in 484 th1 TRANS th2) 485 else REFL tm 486 ) ? failwith`EXISTS_DEL`;; 487% 488 489let EXISTS_DEL tm = 490 (let l,t = strip_exists tm 491 and l' = frees tm 492 in 493 if intersect l l' = [] then mk_thm([], mk_eq(tm,t)) else fail 494 ) ? failwith`EXISTS_DEL`;; 495 496% 497 The pruning rule below will need to be made more complicated. 498 499 |- (?l1 ... lm. t1 /\ ... /\ tn) = (u1 /\ ... /\ up) 500 501 where each ti is an equation "xi = ti'" and the uis are those tis 502 for which xi is not one of l1, ... ,lm. The rule below assumes that 503 for each li there is exactly one ti with xi=li. This will have to be 504 relaxed later. 505% 506 507% PRUNE1 prunes one hidden variable % 508 509let PRUNE1 x eqs = 510 (let l1,l2 = partition(free_in x)(conjuncts eqs) 511 in 512 let th1 = LIST_MK_EXISTS [x] (CONJ_SET_CONV (conjuncts eqs) (l1@l2)) 513 in 514 let th2 = th1 TRANS EXISTS_AND_RIGHT(rhs(concl th1)) 515 in 516 let t1,t2 = dest_conj(rhs(concl th2)) 517 in 518 let th3 = th2 TRANS (AP_THM(AP_TERM "$/\" (EXISTS_EQN t1))t2) 519 and th4 = SPEC t2 AND_CLAUSE1 520 in 521 th3 TRANS th4 522 ) ? failwith`PRUNE1`;; 523 524% 525 526 |- (?l1 ... lm. t1 /\ ... /\ tn) = (u1 /\ ... /\ up) 527 528 where each ti has the form "!x. xi x = ti'" and the uis are those tis 529 for which xi is not one of l1, ... ,lm. The rule below assumes that 530 for each li there is exactly one ti with xi=li. This will have to be 531 relaxed later. 532% 533 534% PRUNE1F prunes one hidden variable % 535 536let PRUNE1F x eqs = 537 (let l1,l2 = partition(free_in x)(conjuncts eqs) 538 in 539 let th1 = LIST_MK_EXISTS [x] (CONJ_SET_CONV (conjuncts eqs) (l1@l2)) 540 in 541 let th2 = th1 TRANS EXISTS_AND_RIGHT(rhs(concl th1)) 542 in 543 let t1,t2 = dest_conj(rhs(concl th2)) 544 in 545 let th3 = th2 TRANS (AP_THM(AP_TERM "$/\" (EXISTS_EQNF t1))t2) 546 and th4 = SPEC t2 AND_CLAUSE1 547 in 548 th3 TRANS th4 549 ) ? failwith`PRUNE1F`;; 550 551letrec PRUNEL vars eqs = 552 (if null vars 553 then REFL eqs 554 if null(tl vars) 555 then PRUNE1 (hd vars) eqs 556 else 557 (let th1 = PRUNEL (tl vars) eqs 558 in 559 let th2 = PRUNE1 (hd vars) (rhs(concl th1)) 560 in 561 (LIST_MK_EXISTS [hd vars] th1) TRANS th2) 562 ) ? failwith`PRUNEL`;; 563 564let PRUNE t = 565 (let vars,eqs = strip_exists t in PRUNEL vars eqs) ? failwith`PRUNE`;; 566 567let PRUNE_RULE th = RIGHT_CONV_RULE PRUNE th ? failwith `PRUNE_RULE`;; 568 569letrec PRUNELF vars eqs = 570 (if null vars 571 then REFL eqs 572 if null(tl vars) 573 then PRUNE1F (hd vars) eqs 574 else 575 (let th1 = PRUNELF (tl vars) eqs 576 in 577 let th2 = PRUNE1F (hd vars) (rhs(concl th1)) 578 in 579 (LIST_MK_EXISTS [hd vars] th1) TRANS th2) 580 ) ? failwith`PRUNELF`;; 581 582let PRUNEF t = 583 (let vars,eqs = strip_exists t in PRUNELF vars eqs) ? failwith`PRUNEF`;; 584 585let PRUNEF_RULE th = RIGHT_CONV_RULE PRUNEF th ? failwith `PRUNEF_RULE`;; 586 587% EXPAND below is like EXPAND_IMP of LCF_LSM; it unfolds, unwinds and prunes % 588 589let EXPAND thl th = 590 let th1 = UNFOLD_RULE thl th 591 in 592 let th2 = OLD_UNWIND_RULE th1 593 in 594 PRUNE_RULE th2;; 595 596let EXPANDF thl th = 597 let th1 = UNFOLD_RULE thl th 598 in 599 let th2 = UNWINDF_RULE th1 600 in 601 PRUNEF_RULE th2;; 602 603% The stuff below superceeds some of the stuff above. Some cleaning % 604% up is needed ... % 605 606% New HOL Inference rules for unwinding device implementations. % 607% % 608% DATE 85.05.21 % 609% AUTHOR T. Melham % 610 611% AUXILIARY FUNCTION DEFINITIONS -------------------------------------- % 612 613 614% line_var "!v1 ... vn. f v1 ... vn = t" ====> "f" % 615 616let line_var tm = fst(strip_comb(lhs(snd(strip_forall tm))));; 617 618% var_name "var" ====> `var` % 619 620let var_name = fst o dest_var;; 621 622% line_name "!v1 ... vn. f v1 ... vn = t" ====> `f` % 623 624let line_name = var_name o line_var;; 625 626% UNWIND CONVERSIONS -------------------------------------------------- % 627 628% UNWIND_ONCE_CONV - Basic conversion for parallel unwinding of lines. % 629% % 630% DESCRIPTION: tm should be a conjunction, t1 /\ t2 ... /\ tn. % 631% p:term->bool is a function which is used to partition the% 632% terms (ti) into two sets. Those ti which p is true of % 633% are then used as a set of rewrite rules (thus they must % 634% be equations) to do a top-down one-step parallel rewrite % 635% of the conjunction of the remaining terms. I.e. % 636% % 637% t1 /\ ... /\ eqn1 /\ ... /\ eqni /\ ... /\ tn % 638% --------------------------------------------- % 639% |- t1 /\ ... /\ eqn1 /\ ... /\ eqni /\ ... /\ tn % 640% = % 641% eqn1 /\ ... /\ eqni /\ ... /\ t1' /\ ... /\ tn' % 642% % 643% where tj' is tj rewritten with the equations eqnx % 644 645let UNWIND_ONCE_CONV p tm = 646 let eqns = conjuncts tm in 647 let eq1,eq2 = partition (\tm. ((p tm) ? false)) eqns in 648 if (null eq1) or (null eq2) 649 then REFL tm 650 else let thm = CONJ_DISCHL eq1 651 (ONCE_DEPTH_CONV 652 (REWRITES_CONV (mk_conv_net (map ASSUME eq1))) 653 (list_mk_conj eq2)) in 654 let re = CONJUNCTS_CONV(tm,(lhs(concl thm))) in 655 re TRANS thm;; 656 657% Unwind until no change using equations selected by p. % 658% WARNING -- MAY LOOP! % 659 660letrec UNWIND_CONV p tm = 661 let th = UNWIND_ONCE_CONV p tm in 662 if lhs(concl th)=rhs(concl th) 663 then th 664 else th TRANS (UNWIND_CONV p (rhs(concl th)));; 665 666% UNWIND CONVERSIONS -------------------------------------------------- % 667 668% One-step unwinding of device behaviour with hidden lines using line % 669% equations selected by p. % 670let UNWIND_ONCE_RULE p th = 671 let rhs_conv = \rhs. (let lines,eqs = strip_exists rhs in 672 LIST_MK_EXISTS lines (UNWIND_ONCE_CONV p eqs)) in 673 RIGHT_CONV_RULE rhs_conv th ? failwith `UNWIND_ONCE_RULE`;; 674 675% Unwind device behaviour using line equations selected by p until no % 676% change. WARNING --- MAY LOOP! % 677let UNWIND_RULE p th = 678 let rhs_conv = \rhs. (let lines,eqs = strip_exists rhs in 679 LIST_MK_EXISTS lines (UNWIND_CONV p eqs)) in 680 RIGHT_CONV_RULE rhs_conv th ? failwith `UNWIND_RULE`;; 681 682% Unwind all lines (except those in the list l) as much as possible. % 683let UNWIND_ALL_RULE l th = 684 let rhs_conv = 685 \rh. (let lines,eqs = strip_exists rh in 686 let eqns = filter (can line_name) (conjuncts eqs) in 687 let line_names = subtract (map line_name eqns) l in 688 let p = \line. \tm. (line_name tm) = line in 689 let itfn = \line. \th. th TRANS 690 UNWIND_CONV (p line) (rhs(concl th)) in 691 LIST_MK_EXISTS lines (itlist itfn line_names (REFL eqs))) in 692 RIGHT_CONV_RULE rhs_conv th ? failwith `UNWIND_ALL_RULE`;; 693 694 695let NEW_EXPANDF l thl th = 696 let th1 = UNFOLD_RULE thl th 697 in 698 let th2 = UNWIND_ALL_RULE l th1 699 in 700 PRUNEF_RULE th2;; 701 702% TEST CASES ---------------- 703let imp = ASSUME 704 "IMP(f,g,h) = ?l3 l2 l1. 705 (!x:num. f x = (l1 (x+1)) + (l2 (x+2)) + (l3 (x+3))) /\ 706 (!x. g x = (l3 (l3 (l3 x)))) /\ 707 (!x. l2 x = (l3 x) - 1) /\ 708 (!x. h x = l3 x) /\ 709 (!x. l1 x = (l2 x) + 1) /\ 710 (!x. l3 x = 7) /\ 711 notanequation:bool";; 712 713let tm = "(!x:num. f x = (l1 (x+1)) + (l2 (x+2)) + (l3 (x+3))) /\ 714 (!x. l1 x = (l2 x) + 1) /\ 715 (!x. g x = (l3 (l3 (l3 x)))) /\ 716 (!x. l2 x = (l3 x) - 1) /\ 717 (!x. h x = l3 x) /\ 718 (!x. l3 x = 7) /\ 719 notanequation:bool";; 720 721UNWIND_ONCE_CONV (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) tm;; 722 723UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) tm;; 724 725UNWIND_ONCE_RULE (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) imp;; 726 727UNWIND_RULE (\tm. mem (line_name tm) [`l1`;`l2`;`l3`]) imp;; 728 729UNWIND_ALL_RULE [] imp;; 730 731UNWIND_ALL_RULE [`l3`] imp;; 732 733% 734