1(*****************************************************************************) 2(* FILE : unwindLib.sml *) 3(* DESCRIPTION : Rules for unfolding, unwinding, pruning, etc. *) 4(* *) 5(* READS FILES : <none> *) 6(* WRITES FILES : <none> *) 7(* *) 8(* AUTHOR : Originally written for LCF-LSM by Mike Gordon (MJCG). *) 9(* 21.May.1985 : Additions by Tom Melham (TFM). *) 10(* 10.Mar.1988 : Modifications by David Shepherd (DES) of INMOS. *) 11(* 24.Mar.1988 : Bug fixes by David Shepherd (DES). *) 12(* 23.Apr.1990 : Modifications by Tom Melham (TFM). *) 13(* 22.Aug.1991 : Additions and tidying-up by Richard Boulton (RJB). *) 14(* *) 15(* LAST MODIFIED : R.J.Boulton *) 16(* DATE : 3rd September 1991 *) 17(* TRANSLATOR : Konrad Slind, University of Calgary *) 18(*****************************************************************************) 19 20structure unwindLib :> unwindLib = 21struct 22 23open HolKernel Parse boolLib Rsyntax ; 24 25infix THENC ##; 26 27val UNWIND_ERR = mk_HOL_ERR "Unwind"; 28 29val AND = boolSyntax.conjunction; 30 31(*===========================================================================*) 32(* Tools for manipulating device implementations `by hand' *) 33(*===========================================================================*) 34 35(*---------------------------------------------------------------------------*) 36(* DEPTH_FORALL_CONV : conv -> conv *) 37(* *) 38(* DEPTH_FORALL_CONV conv "!x1 ... xn. body" applies conv to "body" and *) 39(* returns a theorem of the form: *) 40(* *) 41(* |- (!x1 ... xn. body) = (!x1 ... xn. body') *) 42(*---------------------------------------------------------------------------*) 43 44fun DEPTH_FORALL_CONV conv tm = 45 if (is_forall tm) 46 then RAND_CONV (ABS_CONV (DEPTH_FORALL_CONV conv)) tm 47 else conv tm; 48 49(*---------------------------------------------------------------------------*) 50(* DEPTH_EXISTS_CONV : conv -> conv *) 51(* *) 52(* DEPTH_EXISTS_CONV conv "?x1 ... xn. body" applies conv to "body" and *) 53(* returns a theorem of the form: *) 54(* *) 55(* |- (?x1 ... xn. body) = (?x1 ... xn. body') *) 56(*---------------------------------------------------------------------------*) 57 58fun DEPTH_EXISTS_CONV conv tm = 59 if (is_exists tm) 60 then RAND_CONV (ABS_CONV (DEPTH_EXISTS_CONV conv)) tm 61 else conv tm; 62 63(*---------------------------------------------------------------------------*) 64(* FLATTEN_CONJ_CONV : conv *) 65(* *) 66(* "t1 /\ ... /\ tn" *) 67(* ----> *) 68(* |- t1 /\ ... /\ tn = u1 /\ ... /\ un *) 69(* *) 70(* where the RHS of the equation is a flattened version of the LHS. *) 71(*---------------------------------------------------------------------------*) 72 73fun FLATTEN_CONJ_CONV t = CONJUNCTS_AC (t,list_mk_conj (strip_conj t)); 74 75(*===========================================================================*) 76(* Moving universal quantifiers in and out of conjunctions *) 77(*===========================================================================*) 78 79(*---------------------------------------------------------------------------*) 80(* CONJ_FORALL_ONCE_CONV : conv *) 81(* *) 82(* "(!x. t1) /\ ... /\ (!x. tn)" *) 83(* ----> *) 84(* |- (!x. t1) /\ ... /\ (!x. tn) = !x. t1 /\ ... /\ tn *) 85(* *) 86(* where the original term can be an arbitrary tree of /\s, not just linear. *) 87(* The structure of the tree is retained in both sides of the equation. *) 88(* *) 89(* To avoid deriving incompatible theorems for IMP_ANTISYM_RULE when one or *) 90(* more of the ti's is a conjunction, the original term is broken up as well *) 91(* as the theorem. If this were not done, the conversion would fail in such *) 92(* cases. *) 93(*---------------------------------------------------------------------------*) 94 95local exception NOT_ALL_SAME_VAR 96in 97fun CONJ_FORALL_ONCE_CONV t = 98 let fun conj_tree_map f t th = 99 let val {conj1,conj2} = dest_conj t 100 and (th1,th2) = CONJ_PAIR th 101 in CONJ (conj_tree_map f conj1 th1) (conj_tree_map f conj2 th2) 102 end handle HOL_ERR _ => (f th) 103 val conjs = strip_conj t 104 in if (length conjs = 1) 105 then REFL t 106 else let val var = 107 case op_mk_set aconv (map (#Bvar o dest_forall) conjs) of 108 [x] => x 109 | _ => raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" 110 "bound vars do not have same name" 111 val th = GEN var (conj_tree_map (SPEC var) t (ASSUME t)) 112 val th1 = DISCH t th 113 and th2 = DISCH (concl th) 114 (conj_tree_map (GEN var) t 115 (SPEC var (ASSUME (concl th)))) 116 in IMP_ANTISYM_RULE th1 th2 117 end 118 end 119 handle (e as HOL_ERR{origin_function = "CONJ_FORALL_ONCE_CONV",...}) 120 => raise e 121 | HOL_ERR _ => raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" 122end; 123 124(*---------------------------------------------------------------------------*) 125(* FORALL_CONJ_ONCE_CONV : conv *) 126(* *) 127(* "!x. t1 /\ ... /\ tn" *) 128(* ----> *) 129(* |- !x. t1 /\ ... /\ tn = (!x. t1) /\ ... /\ (!x. tn) *) 130(* *) 131(* where the original term can be an arbitrary tree of /\s, not just linear. *) 132(* The structure of the tree is retained in both sides of the equation. *) 133(*---------------------------------------------------------------------------*) 134 135fun FORALL_CONJ_ONCE_CONV t = 136 let fun conj_tree_map f th = 137 let val (th1,th2) = CONJ_PAIR th 138 in CONJ (conj_tree_map f th1) (conj_tree_map f th2) 139 end handle HOL_ERR _ => f th 140 val var = #Bvar (dest_forall t) 141 val th = conj_tree_map (GEN var) (SPEC var (ASSUME t)) 142 val th1 = DISCH t th 143 and th2 = DISCH (concl th) 144 (GEN var (conj_tree_map (SPEC var) (ASSUME (concl th)))) 145 in IMP_ANTISYM_RULE th1 th2 146 end 147 handle HOL_ERR _ => raise UNWIND_ERR "FORALL_CONJ_ONCE_CONV" ""; 148 149(*---------------------------------------------------------------------------*) 150(* CONJ_FORALL_CONV : conv *) 151(* *) 152(* "(!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)" *) 153(* ----> *) 154(* |- (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) = *) 155(* !x1 ... xm. t1 /\ ... /\ tn *) 156(* *) 157(* where the original term can be an arbitrary tree of /\s, not just linear. *) 158(* The structure of the tree is retained in both sides of the equation. *) 159(*---------------------------------------------------------------------------*) 160 161(* 162local exception FAIL 163in 164fun CONJ_FORALL_CONV tm = 165 (if (length (strip_conj tm) = 1) 166 then raise FAIL 167 else (CONJ_FORALL_ONCE_CONV THENC RAND_CONV (ABS_CONV CONJ_FORALL_CONV)) tm) 168 handle _ => REFL tm 169end; 170*) 171 172fun CONJ_FORALL_CONV tm = 173 case (strip_conj tm) 174 of [_] => REFL tm 175 | _ => (CONJ_FORALL_ONCE_CONV THENC 176 RAND_CONV (ABS_CONV CONJ_FORALL_CONV)) tm 177 handle HOL_ERR _ => REFL tm; 178 179 180(*---------------------------------------------------------------------------*) 181(* FORALL_CONJ_CONV : conv *) 182(* *) 183(* "!x1 ... xm. t1 /\ ... /\ tn" *) 184(* ----> *) 185(* |- !x1 ... xm. t1 /\ ... /\ tn = *) 186(* (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) *) 187(* *) 188(* where the original term can be an arbitrary tree of /\s, not just linear. *) 189(* The structure of the tree is retained in both sides of the equation. *) 190(*---------------------------------------------------------------------------*) 191 192fun FORALL_CONJ_CONV tm = 193 if (is_forall tm) 194 then (RAND_CONV (ABS_CONV FORALL_CONJ_CONV) THENC FORALL_CONJ_ONCE_CONV) tm 195 else REFL tm; 196 197(*---------------------------------------------------------------------------*) 198(* CONJ_FORALL_RIGHT_RULE : thm -> thm *) 199(* *) 200(* A |- !z1 ... zr. *) 201(* t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) *) 202(* ------------------------------------------------------------------- *) 203(* A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn *) 204(* *) 205(*---------------------------------------------------------------------------*) 206 207fun CONJ_FORALL_RIGHT_RULE th = 208 CONV_RULE 209 (DEPTH_FORALL_CONV (RAND_CONV (DEPTH_EXISTS_CONV CONJ_FORALL_CONV))) th 210 handle HOL_ERR _ => raise UNWIND_ERR "CONJ_FORALL_RIGHT_RULE" ""; 211 212(*---------------------------------------------------------------------------*) 213(* FORALL_CONJ_RIGHT_RULE : thm -> thm *) 214(* *) 215(* A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn *) 216(* ------------------------------------------------------------------- *) 217(* A |- !z1 ... zr. *) 218(* t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) *) 219(* *) 220(*---------------------------------------------------------------------------*) 221 222fun FORALL_CONJ_RIGHT_RULE th = 223 CONV_RULE 224 (DEPTH_FORALL_CONV (RAND_CONV (DEPTH_EXISTS_CONV FORALL_CONJ_CONV))) th 225 handle HOL_ERR _ => raise UNWIND_ERR "FORALL_CONJ_RIGHT_RULE" ""; 226 227(*===========================================================================*) 228(* Rules for unfolding *) 229(*===========================================================================*) 230(*---------------------------------------------------------------------------*) 231(* UNFOLD_CONV : thm list -> conv *) 232(* *) 233(* UNFOLD_CONV thl *) 234(* *) 235(* "t1 /\ ... /\ tn" *) 236(* ----> *) 237(* B |- t1 /\ ... /\ tn = t1' /\ ... /\ tn' *) 238(* *) 239(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 240(* set of assumptions B is the union of the instantiated assumptions of the *) 241(* theorems used for rewriting. If none of the rewrites are applicable to a *) 242(* ti, it is unchanged. *) 243(*---------------------------------------------------------------------------*) 244 245fun UNFOLD_CONV thl = 246 let val the_net = Rewrite.add_rewrites Rewrite.empty_rewrites thl 247 fun THENQC conv1 conv2 tm = 248 let val th1 = conv1 tm 249 in TRANS th1 (conv2 (rhs (concl th1))) 250 handle HOL_ERR _ => th1 251 end handle HOL_ERR _ => conv2 tm 252 fun CONJ_TREE_CONV conv tm = 253 if (is_conj tm) 254 then THENQC (RATOR_CONV (RAND_CONV (CONJ_TREE_CONV conv))) 255 (RAND_CONV (CONJ_TREE_CONV conv)) tm 256 else conv tm 257 in fn t => 258 if (null thl) 259 then REFL t 260 else CONJ_TREE_CONV (Rewrite.REWRITES_CONV the_net) t 261 handle HOL_ERR _ => REFL t 262 end; 263 264(*---------------------------------------------------------------------------*) 265(* UNFOLD_RIGHT_RULE : thm list -> thm -> thm *) 266(* *) 267(* UNFOLD_RIGHT_RULE thl *) 268(* *) 269(* A |- !z1 ... zr. t = ?y1 ... yp. t1 /\ ... /\ tn *) 270(* -------------------------------------------------------- *) 271(* B u A |- !z1 ... zr. t = ?y1 ... yp. t1' /\ ... /\ tn' *) 272(* *) 273(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 274(* set of assumptions B is the union of the instantiated assumptions of the *) 275(* theorems used for rewriting. If none of the rewrites are applicable to a *) 276(* ti, it is unchanged. *) 277(*---------------------------------------------------------------------------*) 278 279fun UNFOLD_RIGHT_RULE thl th = 280 CONV_RULE 281 (DEPTH_FORALL_CONV (RAND_CONV (DEPTH_EXISTS_CONV (UNFOLD_CONV thl)))) 282 th 283 handle HOL_ERR _ => raise UNWIND_ERR "UNFOLD_RIGHT_RULE" ""; 284 285(*===========================================================================*) 286(* Rules for unwinding device implementations *) 287(*===========================================================================*) 288 289(*---------------------------------------------------------------------------*) 290(* line_var : term -> term *) 291(* *) 292(* line_var "!y1 ... ym. f x1 ... xn = t" ----> "f" *) 293(*---------------------------------------------------------------------------*) 294 295fun line_var tm = 296 (fst o strip_comb o lhs o snd o strip_forall) tm 297 handle HOL_ERR _ => raise UNWIND_ERR "line_var" ""; 298 299(*---------------------------------------------------------------------------*) 300(* line_name : term -> string *) 301(* *) 302(* line_name "!y1 ... ym. f x1 ... xn = t" ----> "f" *) 303(*---------------------------------------------------------------------------*) 304 305fun line_name tm = (#Name o dest_var o line_var) tm 306 handle HOL_ERR _ => raise UNWIND_ERR "line_name" ""; 307 308(*---------------------------------------------------------------------------*) 309(* UNWIND_ONCE_CONV : (term -> bool) -> conv *) 310(* *) 311(* Basic conversion for parallel unwinding of equations defining wire values *) 312(* in a standard device specification. *) 313(* *) 314(* USAGE: UNWIND_ONCE_CONV p tm *) 315(* *) 316(* DESCRIPTION: tm should be a conjunction of terms, equivalent under *) 317(* associative-commutative reordering to: *) 318(* *) 319(* t1 /\ t2 /\ ... /\ tn. *) 320(* *) 321(* The function p:term->bool is a predicate which will be *) 322(* used to partition the terms ti for 1 <= i <= n into two *) 323(* disjoint sets: *) 324(* *) 325(* REW = {ti | p ti} and OBJ = {ti | ~p ti} *) 326(* *) 327(* The terms ti for which p is true are then used as a set *) 328(* of rewrite rules (thus they should be equations) to do a *) 329(* single top-down parallel rewrite of the remaining terms. *) 330(* The rewritten terms take the place of the original terms *) 331(* in the input conjunction. *) 332(* *) 333(* For example, if tm is: *) 334(* *) 335(* t1 /\ t2 /\ t3 /\ t4 *) 336(* *) 337(* and REW = {t1,t3} then the result is: *) 338(* *) 339(* |- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4' *) 340(* *) 341(* where ti' is ti rewritten with the equations REW. *) 342(* *) 343(* IMPLEMENTATION NOTE: *) 344(* *) 345(* The assignment: *) 346(* *) 347(* let pf,fn,eqns = trav p tm [] *) 348(* *) 349(* makes *) 350(* *) 351(* eqns = a list of theorems constructed by assuming each term for *) 352(* which p is true, i.e., eqns = the list of rewrites. *) 353(* *) 354(* fnn = a function which, when applied to a rewriting conversion *) 355(* will reconstruct the original term in the original structure, *) 356(* but with the subterms for which p is not true rewritten *) 357(* using the supplied conversion. *) 358(* *) 359(* pf = a function which maps |- tm to [|- t1;...;|- tj] where each *) 360(* ti is a term for which p is true. *) 361(*---------------------------------------------------------------------------*) 362 363local 364fun trav p tm rl = 365 let val {conj1,conj2} = dest_conj tm 366 val (pf2,fn2,tmp) = trav p conj2 rl 367 val (pf1,fn1,rew) = trav p conj1 tmp 368 val pf = (op @) o (pf1##pf2) o CONJ_PAIR 369 in (pf,(fn rf => MK_COMB ((AP_TERM AND (fn1 rf)),(fn2 rf))),rew) 370 end handle HOL_ERR _ 371 => if (p tm handle HOL_ERR _ => false) 372 then ((fn th => [th]),(fn rf => REFL tm),(ASSUME tm :: rl)) 373 else ((fn th => []),(fn rf => rf tm),rl) 374in 375fun UNWIND_ONCE_CONV p tm = 376 let val (pf,fnn,eqns) = trav p tm [] 377 val rconv = ONCE_DEPTH_CONV 378 (REWRITES_CONV 379 (Rewrite.add_rewrites Rewrite.empty_rewrites eqns)) 380 val th = fnn rconv 381 val {lhs,rhs} = dest_eq (concl th) 382 val lth = ASSUME lhs 383 and rth = ASSUME rhs 384 val imp1 = DISCH lhs (EQ_MP (itlist PROVE_HYP (pf lth) th) lth) 385 and imp2 = DISCH rhs (EQ_MP (SYM (itlist PROVE_HYP (pf rth) th)) rth) 386 in IMP_ANTISYM_RULE imp1 imp2 387 end 388 handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_ONCE_CONV" "" 389end; 390 391(*---------------------------------------------------------------------------*) 392(* UNWIND_CONV : (term -> bool) -> conv *) 393(* *) 394(* Unwind device behaviour using line equations eqnx selected by p until no *) 395(* change. *) 396(* *) 397(* WARNING -- MAY LOOP! *) 398(* *) 399(* UNWIND_CONV p *) 400(* *) 401(* "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" *) 402(* ----> *) 403(* |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = *) 404(* t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' *) 405(* *) 406(* where ti' (for 1 <= i <= n) is ti rewritten with the equations *) 407(* eqni (1 <= i <= m). These equations are the conjuncts for which the *) 408(* predicate p is true. The ti terms are the conjuncts for which p is false. *) 409(* The rewriting is repeated until no changes take place. *) 410(*---------------------------------------------------------------------------*) 411 412fun UNWIND_CONV p tm = 413 let val th = UNWIND_ONCE_CONV p tm 414 in if lhs (concl th) ~~ rhs (concl th) 415 then th 416 else TRANS th (UNWIND_CONV p (rhs (concl th))) 417 end; 418 419(*---------------------------------------------------------------------------*) 420(* UNWIND_ALL_BUT_CONV : string list -> conv *) 421(* *) 422(* Unwind all lines (except those in the list l) as much as possible. *) 423(* *) 424(* WARNING -- MAY LOOP! *) 425(* *) 426(* UNWIND_ALL_BUT_CONV l *) 427(* *) 428(* "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" *) 429(* ----> *) 430(* |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = *) 431(* t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' *) 432(* *) 433(* where ti' (for 1 <= i <= n) is ti rewritten with the equations *) 434(* eqni (1 <= i <= m). These equations are those conjuncts with line name not*) 435(* in l (and which are equations). *) 436(*---------------------------------------------------------------------------*) 437 438fun UNWIND_ALL_BUT_CONV l tm = 439 let val line_names = set_diff (mapfilter line_name (strip_conj tm)) l 440 fun p line tm = (line_name tm) = line 441 fun itfn line th = TRANS th (UNWIND_CONV (p line) (rhs (concl th))) 442 in itlist itfn line_names (REFL tm) 443 end 444 handle HOL_ERR _ => raise UNWIND_ERR"UNWIND_ALL_BUT_CONV" ""; 445 446(*---------------------------------------------------------------------------*) 447(* UNWIND_AUTO_CONV : conv *) 448(* *) 449(* "?l1 ... lm. t1 /\ ... /\ tn" *) 450(* ----> *) 451(* |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn') *) 452(* *) 453(* where tj' is tj rewritten with equations selected from the ti's. The *) 454(* function decides which equations to use by performing a loop analysis on *) 455(* the graph representing the dependencies of the lines. By this means the *) 456(* term can be unwound as much as possible without the risk of looping. The *) 457(* user is left to deal with the recursive equations. *) 458(* *) 459(* The algorithms used for loop analysis in this function are extremely *) 460(* naive. There is also some inefficiency in that certain lines may be used *) 461(* in unwinding even though they do not appear in any RHS's. *) 462(* *) 463(* Amongst other things, the internal function "graph_of_term' rearranges the*) 464(* lines in the graph representation so that external lines come first. This *) 465(* gives them priority over the internal lines when the function is *) 466(* determining where to "break" loops. This is useful because the line chosen*) 467(* as the break will be left in the resultant term, and further manipulations*) 468(* by the user should be easier if it is an external rather than an internal *) 469(* line that is left in. *) 470(*---------------------------------------------------------------------------*) 471 472local fun FAIL s = UNWIND_ERR "UNWIND_AUTO_CONV" s 473fun is_set [] = true 474 | is_set (a::rst) = (not (tmem a rst)) andalso is_set rst 475fun pdeq tm = let val {lhs,rhs} = dest_eq tm in (lhs,rhs) end 476fun graph_of_term tm = 477 let val (internals,t) = strip_exists tm 478 val (lines,rhs_free_vars) = 479 unzip (mapfilter (((assert is_var o fst o strip_comb)##free_vars) o 480 pdeq o snd o strip_forall) 481 (strip_conj t)) 482 in 483 if (is_set lines) then 484 let 485 val graph = 486 zip lines (map (op_intersect aconv lines) rhs_free_vars) 487 val (intern,extern) = partition (fn p => tmem (fst p) internals) graph 488 in extern@intern 489 end 490 else raise FAIL "graph_of_term" 491 end 492 493fun loops_containing_line line graph chain = 494 let val successors = map fst 495 (filter (fn (_,predecs) => tmem (Lib.trye hd chain) predecs) graph) 496 val not_in_chain = filter (fn line => not (tmem line chain)) successors 497 val new_chains = map (fn line => line::chain) not_in_chain 498 (* flatten(map ...) should be an itlist *) 499 val new_loops = flatten (map (loops_containing_line line graph) 500 new_chains) 501 in if tmem line successors then (rev chain)::new_loops 502 else new_loops 503 end 504 505fun chop_at x (l as (a::rst)) = 506 if a ~~ x then ([],l) 507 else let val (l1,l2) = chop_at x rst 508 in (a::l1, l2) 509 end 510 | chop_at _ _ = raise FAIL "chop_at"; 511 512(* before has infix status in SML/NJ, so changed to befre *) 513fun op_set_eq eqf l1 l2 = 514 null (op_set_diff eqf l1 l2) andalso null (op_set_diff eqf l2 l1) 515fun equal_loops lp1 lp2 = 516 if (op_set_eq aconv lp1 lp2) 517 then let val (befre,rest) = chop_at (Lib.trye hd lp1) lp2 518 in tml_eq lp1 (rest @ befre) 519 end 520 else false 521 522fun distinct_loops [] = [] 523 | distinct_loops (h::t) = 524 if (exists (fn lp => equal_loops lp h) t) 525 then distinct_loops t 526 else h ::(distinct_loops t) 527 528(* Could use an itlist here again and collapse the maps. *) 529fun loops_of_graph graph = 530 distinct_loops 531 (flatten 532 (map (fn line => loops_containing_line line graph [line]) 533 (map fst graph))) 534 535fun list_after x (l as (h::t)) = 536 if x ~~ h then t else list_after x t 537 | list_after _ _ = raise UNWIND_ERR "list_after" ""; 538 539fun rev_front_of l n front = 540 if (n < 0) 541 then raise FAIL "rev_front_of" 542 else if (n = 0) 543 then front 544 else rev_front_of (Lib.trye tl l) (n - 1) (Lib.trye hd l ::front) 545 546fun next_comb_at_this_level source n (h::t) = 547 let val l = list_after h source 548 in if (length l > n) 549 then (rev_front_of l (n + 1) []) @ t 550 else next_comb_at_this_level source (n + 1) t 551 end 552 | next_comb_at_this_level _ _ _ = raise FAIL "next_comb_at_this_level" 553 554fun next_combination source previous = 555 next_comb_at_this_level source 0 previous 556 handle HOL_ERR _ => rev_front_of source ((length previous) + 1) [] 557 558fun break_all_loops lps lines previous = 559 let val comb = next_combination lines previous 560 in if (all (fn lp => not (null (op_intersect aconv lp comb))) lps) 561 then comb 562 else break_all_loops lps lines comb 563 end 564 565fun breaks internals graph = 566 let val loops = loops_of_graph graph 567 val single_el_loops = filter (fn l => length l = 1) loops 568 val single_breaks = flatten single_el_loops 569 val loops' = filter (null o (op_intersect aconv single_breaks)) loops 570 val only_internal_loops = 571 filter (fn l => null (op_set_diff aconv l internals)) loops' 572 val only_internal_lines = end_itlist (op_union aconv) only_internal_loops 573 handle HOL_ERR _ => [] 574 val internal_breaks = 575 break_all_loops only_internal_loops only_internal_lines [] 576 handle HOL_ERR _ => [] 577 val external_loops = 578 filter (null o (op_intersect aconv internal_breaks)) loops' 579 val external_lines = 580 op_set_diff aconv 581 (end_itlist (op_union aconv) external_loops 582 handle HOL_ERR _ => []) 583 internals 584 val external_breaks = 585 break_all_loops external_loops external_lines [] 586 handle HOL_ERR _ => [] 587 in single_breaks @ (rev internal_breaks) @ (rev external_breaks) 588 end 589 590 591fun conv dependencies used t = 592 let 593 val vars = map fst (filter ((fn l => null (op_set_diff aconv l used)) o snd) 594 dependencies) 595 in 596 if (null vars) then REFL t 597 else ((UNWIND_ONCE_CONV (fn tm => tmem (line_var tm) vars)) THENC 598 (conv (filter (fn p => not (tmem (fst p) vars)) dependencies) 599 (used @ vars))) t 600 end 601in 602fun UNWIND_AUTO_CONV tm = 603 let val internals = fst (strip_exists tm) 604 and graph = graph_of_term tm 605 val brks = breaks internals graph 606 val dependencies = map (I ## (fn l => op_set_diff aconv l brks)) 607 (filter (fn p => not (tmem (fst p) brks)) graph) 608 in DEPTH_EXISTS_CONV (conv dependencies []) tm 609 end handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_AUTO_CONV" "" 610end; 611 612(*---------------------------------------------------------------------------*) 613(* UNWIND_ALL_BUT_RIGHT_RULE : string list -> thm -> thm *) 614(* *) 615(* Unwind all lines (except those in the list l) as much as possible. *) 616(* *) 617(* WARNING -- MAY LOOP! *) 618(* *) 619(* UNWIND_ALL_BUT_RIGHT_RULE l *) 620(* *) 621(* A |- !z1 ... zr. *) 622(* t = *) 623(* (?l1 ... lp. t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn) *) 624(* --------------------------------------------------------------------- *) 625(* A |- !z1 ... zr. *) 626(* t = *) 627(* (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn') *) 628(* *) 629(* where ti' (for 1 <= i <= n) is ti rewritten with the equations *) 630(* eqni (1 <= i <= m). These equations are those conjuncts with line name not*) 631(* in l (and which are equations). *) 632(*---------------------------------------------------------------------------*) 633 634fun UNWIND_ALL_BUT_RIGHT_RULE l th = 635 CONV_RULE 636 (DEPTH_FORALL_CONV (RAND_CONV (DEPTH_EXISTS_CONV (UNWIND_ALL_BUT_CONV l)))) 637 th 638 handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_ALL_BUT_RIGHT_RULE" ""; 639 640(*---------------------------------------------------------------------------*) 641(* UNWIND_AUTO_RIGHT_RULE : thm -> thm *) 642(* *) 643(* A |- !z1 ... zr. t = ?l1 ... lm. t1 /\ ... /\ tn *) 644(* ---------------------------------------------------- *) 645(* A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn' *) 646(* *) 647(* where tj' is tj rewritten with equations selected from the ti's. The *) 648(* function decides which equations to use by performing a loop analysis on *) 649(* the graph representing the dependencies of the lines. By this means the *) 650(* equations can be unwound as much as possible without the risk of looping. *) 651(* The user is left to deal with the recursive equations. *) 652(*---------------------------------------------------------------------------*) 653 654fun UNWIND_AUTO_RIGHT_RULE th = 655 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV UNWIND_AUTO_CONV)) th 656 handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_AUTO_RIGHT_RULE" ""; 657 658(*===========================================================================*) 659(* Rules for pruning *) 660(*===========================================================================*) 661(*---------------------------------------------------------------------------*) 662(* EXISTS_DEL1_CONV : conv *) 663(* *) 664(* "?x. t" *) 665(* ----> *) 666(* |- (?x. t) = t *) 667(* *) 668(* provided x is not free in t. *) 669(* *) 670(* Deletes one existential quantifier. *) 671(*---------------------------------------------------------------------------*) 672 673fun EXISTS_DEL1_CONV tm = 674 let val {Bvar,Body} = dest_exists tm 675 val th = ASSUME Body 676 val th1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) th) 677 and th2 = DISCH Body (EXISTS (tm,Bvar) th) 678 in IMP_ANTISYM_RULE th1 th2 679 end handle HOL_ERR _ => raise UNWIND_ERR"EXISTS_DEL1_CONV" ""; 680 681(*---------------------------------------------------------------------------*) 682(* EXISTS_DEL_CONV : conv *) 683(* *) 684(* "?x1 ... xn. t" *) 685(* ----> *) 686(* |- (?x1 ... xn. t) = t *) 687(* *) 688(* provided x1,...,xn are not free in t. *) 689(* *) 690(* Deletes existential quantifiers. The conversion fails if any of the x's *) 691(* appear free in t. It does not perform a partial deletion; for example, if *) 692(* x1 and x2 do not appear free in t but x3 does, the function will fail; it *) 693(* will not return |- ?x1 ... xn. t = ?x3 ... xn. t. *) 694(*---------------------------------------------------------------------------*) 695 696local fun terms_and_vars tm = 697 let val {Bvar,Body} = dest_exists tm 698 in (tm,Bvar)::terms_and_vars Body 699 end handle HOL_ERR _ => [] 700in 701fun EXISTS_DEL_CONV tm = 702 let val txs = terms_and_vars tm 703 val t = #Body (dest_exists (fst (last txs))) handle _ => tm 704 val th = ASSUME t 705 val th1 = DISCH tm (itlist (fn (tm,x) => CHOOSE (x, ASSUME tm)) txs th) 706 and th2 = DISCH t (itlist EXISTS txs th) 707 in IMP_ANTISYM_RULE th1 th2 708 end 709 handle HOL_ERR _ => raise UNWIND_ERR "EXISTS_DEL_CONV" "" 710end; 711 712(*---------------------------------------------------------------------------*) 713(* EXISTS_EQN_CONV : conv *) 714(* *) 715(* "?l. !y1 ... ym. l x1 ... xn = t" *) 716(* ----> *) 717(* |- (?l. !y1 ... ym. l x1 ... xn = t) = T *) 718(* *) 719(* provided l is not free in t. Both m and n may be zero. *) 720(*---------------------------------------------------------------------------*) 721 722fun EXISTS_EQN_CONV t = 723 let val {Bvar = l,Body} = dest_exists t 724 val (ys,A) = strip_forall Body 725 val {lhs,rhs} = dest_eq A 726 val xs = snd ((assert (aconv l) ## I) (strip_comb lhs)) 727 val t3 = list_mk_abs (xs,rhs) 728 val th1 = GENL ys (RIGHT_CONV_RULE LIST_BETA_CONV 729 (REFL (list_mk_comb (t3,xs)))) 730 in EQT_INTRO (EXISTS (t,t3) th1) 731 end handle HOL_ERR _ => raise UNWIND_ERR "EXISTS_EQN_CONV" ""; 732 733(*---------------------------------------------------------------------------*) 734(* PRUNE_ONCE_CONV : conv *) 735(* *) 736(* Prunes one hidden variable. *) 737(* *) 738(* "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" *) 739(* ----> *) 740(* |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = *) 741(* (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) *) 742(* *) 743(* where eq has the form "!y1 ... ym. l x1 ... xn = b" and l does not appear *) 744(* free in the ti's or in b. The conversion works if eq is not present, *) 745(* i.e. if l is not free in any of the conjuncts, but does not work if l *) 746(* appears free in more than one of the conjuncts. Each of m, n and p may be *) 747(* zero. *) 748(*---------------------------------------------------------------------------*) 749 750local val AP_AND = AP_TERM AND 751in 752fun PRUNE_ONCE_CONV tm = 753 let val {Bvar,Body} = dest_exists tm 754 in 755 case (partition (free_in Bvar) (strip_conj Body)) 756 of ([], _) => EXISTS_DEL1_CONV tm 757 | ([eq],l2) => 758 let val th1 = EXISTS_EQN_CONV (mk_exists {Bvar=Bvar, Body=eq}) 759 in 760 if (null l2) then th1 761 else let val conj = list_mk_conj l2 762 val th2 = AP_THM (AP_AND th1) conj 763 val th3 = EXISTS_EQ Bvar 764 (CONJUNCTS_AC 765 (Body,mk_conj{conj1=eq, conj2=conj})) 766 val th4 = RIGHT_CONV_RULE EXISTS_AND_CONV th3 767 in 768 TRANS th4 (TRANS th2 (CONJUNCT1 (SPEC conj AND_CLAUSES))) 769 end 770 end 771 | _ => raise UNWIND_ERR "" "" 772 end handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_ONCE_CONV" "" 773end; 774 775(*---------------------------------------------------------------------------*) 776(* PRUNE_ONE_CONV : string -> conv *) 777(* *) 778(* Prunes one hidden variable. *) 779(* *) 780(* PRUNE_ONE_CONV "lj" *) 781(* *) 782(* "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" *) 783(* ----> *) 784(* |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = *) 785(* (?l1 ... l(j-1) l(j+1) ... lr. *) 786(* t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) *) 787(* *) 788(* where eq has the form "!y1 ... ym. lj x1 ... xn = b" and lj does not *) 789(* appear free in the ti's or in b. The conversion works if eq is not *) 790(* present, i.e. if lj is not free in any of the conjuncts, but does not work*) 791(* if lj appears free in more than one of the conjuncts. Each of m, n and p *) 792(* may be zero. *) 793(* *) 794(* If there is more than one line with the specified name (but with different*) 795(* types), the one that appears outermost in the existential quantifications *) 796(* is pruned. *) 797(*---------------------------------------------------------------------------*) 798 799fun PRUNE_ONE_CONV v tm = 800 let val {Bvar,Body} = dest_exists tm 801 in if (#Name (dest_var Bvar) = v) 802 then if (is_exists Body) 803 then (SWAP_EXISTS_CONV THENC 804 RAND_CONV (ABS_CONV (PRUNE_ONE_CONV v))) tm 805 else PRUNE_ONCE_CONV tm 806 else RAND_CONV (ABS_CONV (PRUNE_ONE_CONV v)) tm 807 end handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_ONE_CONV" ""; 808 809(*---------------------------------------------------------------------------*) 810(* PRUNE_SOME_CONV : string list -> conv *) 811(* *) 812(* Prunes several hidden variables. *) 813(* *) 814(* PRUNE_SOME_CONV ["li1";...;"lik"] *) 815(* *) 816(* "?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp" *) 817(* ----> *) 818(* |- (?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp) = *) 819(* (?li(k+1) ... lir. t1 /\ ... /\ tp) *) 820(* *) 821(* where for 1 <= j <= k, each eqnij has the form: *) 822(* *) 823(* "!y1 ... ym. lij x1 ... xn = b" *) 824(* *) 825(* and lij does not appear free in any of the other conjuncts or in b. *) 826(* The li's are related by the equation: *) 827(* *) 828(* {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} *) 829(* *) 830(* The conversion works if one or more of the eqnij's are not present, *) 831(* i.e. if lij is not free in any of the conjuncts, but does not work if lij *) 832(* appears free in more than one of the conjuncts. p may be zero, that is, *) 833(* all the conjuncts may be eqnij's. In this case the body of the result will*) 834(* be T (true). Also, for each eqnij, m and n may be zero. *) 835(* *) 836(* If there is more than one line with a specified name (but with different *) 837(* types), the one that appears outermost in the existential quantifications *) 838(* is pruned. If such a line name is mentioned twice in the list, the two *) 839(* outermost occurrences of lines with that name will be pruned, and so on. *) 840(*---------------------------------------------------------------------------*) 841 842fun PRUNE_SOME_CONV [] tm = REFL tm 843 | PRUNE_SOME_CONV (h::t) tm = 844 (PRUNE_SOME_CONV t THENC PRUNE_ONE_CONV h) tm 845 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_SOME_CONV" ""; 846 847(*---------------------------------------------------------------------------*) 848(* PRUNE_CONV : conv *) 849(* *) 850(* Prunes all hidden variables. *) 851(* *) 852(* "?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp" *) 853(* ----> *) 854(* |- (?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp) = *) 855(* (t1 /\ ... /\ tp) *) 856(* *) 857(* where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does *) 858(* not appear free in any of the other conjuncts or in b. The conversion *) 859(* works if one or more of the eqni's are not present, i.e. if li is not free*) 860(* in any of the conjuncts, but does not work if li appears free in more than*) 861(* one of the conjuncts. p may be zero, that is, all the conjuncts may be *) 862(* eqni's. In this case the result will be simply T (true). Also, for each *) 863(* eqni, m and n may be zero. *) 864(*---------------------------------------------------------------------------*) 865 866fun PRUNE_CONV tm = 867 if (is_exists tm) 868 then (RAND_CONV (ABS_CONV PRUNE_CONV) THENC PRUNE_ONCE_CONV) tm 869 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_CONV" "" 870 else REFL tm; 871 872(*---------------------------------------------------------------------------*) 873(* PRUNE_SOME_RIGHT_RULE : string list -> thm -> thm *) 874(* *) 875(* Prunes several hidden variables. *) 876(* *) 877(* PRUNE_SOME_RIGHT_RULE ["li1";...;"lik"] *) 878(* *) 879(* A |- !z1 ... zr. *) 880(* t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp *) 881(* -----------------------------------------------------------------------*) 882(* A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp *) 883(* *) 884(* where for 1 <= j <= k, each eqnij has the form: *) 885(* *) 886(* "!y1 ... ym. lij x1 ... xn = b" *) 887(* *) 888(* and lij does not appear free in any of the other conjuncts or in b. *) 889(* The li's are related by the equation: *) 890(* *) 891(* {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} *) 892(* *) 893(* The rule works if one or more of the eqnij's are not present, i.e. if lij *) 894(* is not free in any of the conjuncts, but does not work if lij appears free*) 895(* in more than one of the conjuncts. p may be zero, that is, all the *) 896(* conjuncts may be eqnij's. In this case the conjunction will be transformed*) 897(* to T (true). Also, for each eqnij, m and n may be zero. *) 898(* *) 899(* If there is more than one line with a specified name (but with different *) 900(* types), the one that appears outermost in the existential quantifications *) 901(* is pruned. If such a line name is mentioned twice in the list, the two *) 902(* outermost occurrences of lines with that name will be pruned, and so on. *) 903(*---------------------------------------------------------------------------*) 904 905fun PRUNE_SOME_RIGHT_RULE vs th = 906 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (PRUNE_SOME_CONV vs))) th 907 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_SOME_RIGHT_RULE" ""; 908 909(*---------------------------------------------------------------------------*) 910(* PRUNE_RIGHT_RULE : thm -> thm *) 911(* *) 912(* Prunes all hidden variables. *) 913(* *) 914(* A |- !z1 ... zr. *) 915(* t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp *) 916(* --------------------------------------------------------------------- *) 917(* A |- !z1 ... zr. t = t1 /\ ... /\ tp *) 918(* *) 919(* where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does *) 920(* not appear free in any of the other conjuncts or in b. The rule works if *) 921(* one or more of the eqni's are not present, i.e. if li is not free in any *) 922(* of the conjuncts, but does not work if li appears free in more than one of*) 923(* the conjuncts. p may be zero, that is, all the conjuncts may be eqni's. In*) 924(* this case the result will be simply T (true). Also, for each eqni, m and n*) 925(* may be zero. *) 926(*---------------------------------------------------------------------------*) 927 928fun PRUNE_RIGHT_RULE th = 929 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV PRUNE_CONV)) th 930 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_RIGHT_RULE" ""; 931 932(*===========================================================================*) 933(* Functions which do unfolding, unwinding and pruning *) 934(*===========================================================================*) 935 936(*---------------------------------------------------------------------------*) 937(* EXPAND_ALL_BUT_CONV : string list -> thm list -> conv *) 938(* *) 939(* Unfold with the theorems thl, then unwind all lines (except those in the *) 940(* list) as much as possible and prune the unwound lines. *) 941(* *) 942(* WARNING -- MAY LOOP! *) 943(* *) 944(* EXPAND_ALL_BUT_CONV ["li(k+1)";...;"lim"] thl *) 945(* *) 946(* "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" *) 947(* ----> *) 948(* B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = *) 949(* (?li(k+1) ... lim. t1' /\ ... /\ tn') *) 950(* *) 951(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 952(* set of assumptions B is the union of the instantiated assumptions of the *) 953(* theorems used for rewriting. If none of the rewrites are applicable to a *) 954(* conjunct, it is unchanged. Those conjuncts that after rewriting are *) 955(* equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are *) 956(* used to unwind and the lines li1,...,lik are then pruned. If this is not *) 957(* possible the function will fail. It is also possible for the function to *) 958(* attempt unwinding indefinitely (to loop). *) 959(* *) 960(* The li's are related by the equation: *) 961(* *) 962(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 963(*---------------------------------------------------------------------------*) 964fun EXPAND_ALL_BUT_CONV l thl tm = 965 (DEPTH_EXISTS_CONV ((UNFOLD_CONV thl) THENC (UNWIND_ALL_BUT_CONV l)) THENC 966 (fn tm => let val var_names = map (#Name o dest_var) (fst(strip_exists tm)) 967 in PRUNE_SOME_CONV (subtract var_names l) tm 968 end)) 969 tm handle HOL_ERR _ => raise UNWIND_ERR"EXPAND_ALL_BUT_CONV" ""; 970 971(*---------------------------------------------------------------------------*) 972(* EXPAND_AUTO_CONV : thm list -> conv *) 973(* *) 974(* Unfold with the theorems thl, then unwind as much as possible and prune *) 975(* the unwound lines. *) 976(* *) 977(* EXPAND_AUTO_CONV thl *) 978(* *) 979(* "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" *) 980(* ----> *) 981(* B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = *) 982(* (?li(k+1) ... lim. t1' /\ ... /\ tn') *) 983(* *) 984(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 985(* set of assumptions B is the union of the instantiated assumptions of the *) 986(* theorems used for rewriting. If none of the rewrites are applicable to a *) 987(* conjunct, it is unchanged. After rewriting the function decides which of *) 988(* the resulting terms to use for unwinding by performing a loop analysis on *) 989(* the graph representing the dependencies of the lines. *) 990(* *) 991(* Suppose the function decides to unwind the lines li1,...,lik using the *) 992(* terms ui1',...,uik' respectively. Then after unwinding the lines *) 993(* li1,...,lik are pruned (provided they have been eliminated from the RHS's *) 994(* of the conjuncts that are equations, and from the whole of any other *) 995(* conjuncts) resulting in the elimination of ui1',...,uik'. *) 996(* *) 997(* The li's are related by the equation: *) 998(* *) 999(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 1000(* *) 1001(* The loop analysis allows the term to be unwound as much as possible *) 1002(* without the risk of looping. The user is left to deal with the recursive *) 1003(* equations. *) 1004(*---------------------------------------------------------------------------*) 1005 1006fun EXPAND_AUTO_CONV thl tm = 1007 (DEPTH_EXISTS_CONV (UNFOLD_CONV thl) THENC 1008 UNWIND_AUTO_CONV THENC 1009 (fn tm => 1010 let val (internals,conjs) = (I ## strip_conj) (strip_exists tm) 1011 val vars = flatten (map 1012 (free_vars o (fn tm => (rhs tm) handle HOL_ERR _ => tm) 1013 o snd o strip_forall) conjs) 1014 in 1015 PRUNE_SOME_CONV 1016 (map (#Name o dest_var) (op_set_diff aconv internals vars)) 1017 tm 1018 end)) 1019 tm 1020 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_AUTO_CONV" ""; 1021 1022(*---------------------------------------------------------------------------*) 1023(* EXPAND_ALL_BUT_RIGHT_RULE : string list -> thm list -> thm -> thm *) 1024(* *) 1025(* Unfold with the theorems thl, then unwind all lines (except those in the *) 1026(* list) as much as possible and prune the unwound lines. *) 1027(* *) 1028(* WARNING -- MAY LOOP! *) 1029(* *) 1030(* EXPAND_ALL_BUT_RIGHT_RULE ["li(k+1)";...;"lim"] thl *) 1031(* *) 1032(* A |- !z1 ... zr. *) 1033(* t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn *) 1034(* -----------------------------------------------------------------------*) 1035(* B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' *) 1036(* *) 1037(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 1038(* set of assumptions B is the union of the instantiated assumptions of the *) 1039(* theorems used for rewriting. If none of the rewrites are applicable to a *) 1040(* conjunct, it is unchanged. Those conjuncts that after rewriting are *) 1041(* equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are *) 1042(* used to unwind and the lines li1,...,lik are then pruned. If this is not *) 1043(* possible the function will fail. It is also possible for the function to *) 1044(* attempt unwinding indefinitely (to loop). *) 1045(* *) 1046(* The li's are related by the equation: *) 1047(* *) 1048(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 1049(*---------------------------------------------------------------------------*) 1050 1051fun EXPAND_ALL_BUT_RIGHT_RULE l thl th = 1052 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (EXPAND_ALL_BUT_CONV l thl))) th 1053 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_ALL_BUT_RIGHT_RULE" ""; 1054 1055(*---------------------------------------------------------------------------*) 1056(* EXPAND_AUTO_RIGHT_RULE : thm list -> thm -> thm *) 1057(* *) 1058(* Unfold with the theorems thl, then unwind as much as possible and prune *) 1059(* the unwound lines. *) 1060(* *) 1061(* EXPAND_AUTO_RIGHT_RULE thl *) 1062(* *) 1063(* A |- !z1 ... zr. *) 1064(* t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn *) 1065(* -----------------------------------------------------------------------*) 1066(* B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' *) 1067(* *) 1068(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 1069(* set of assumptions B is the union of the instantiated assumptions of the *) 1070(* theorems used for rewriting. If none of the rewrites are applicable to a *) 1071(* conjunct, it is unchanged. After rewriting the function decides which of *) 1072(* the resulting terms to use for unwinding by performing a loop analysis on *) 1073(* the graph representing the dependencies of the lines. *) 1074(* *) 1075(* Suppose the function decides to unwind the lines li1,...,lik using the *) 1076(* terms ui1',...,uik' respectively. Then after unwinding the lines *) 1077(* li1,...,lik are pruned (provided they have been eliminated from the RHS's *) 1078(* of the conjuncts that are equations, and from the whole of any other *) 1079(* conjuncts) resulting in the elimination of ui1',...,uik'. *) 1080(* *) 1081(* The li's are related by the equation: *) 1082(* *) 1083(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 1084(* *) 1085(* The loop analysis allows the term to be unwound as much as possible *) 1086(* without the risk of looping. The user is left to deal with the recursive *) 1087(* equations. *) 1088(*---------------------------------------------------------------------------*) 1089 1090fun EXPAND_AUTO_RIGHT_RULE thl th = 1091 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (EXPAND_AUTO_CONV thl))) th 1092 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_AUTO_RIGHT_RULE" ""; 1093 1094 1095end; (* unwindLib *) 1096