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 (mk_set (map (#Bvar o dest_forall) conjs)) 108 of [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 (mem 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 if (is_set lines) 483 then let val graph = zip lines (map (intersect lines) rhs_free_vars) 484 val (intern,extern) = partition (fn p => mem (fst p) internals) 485 graph 486 in extern@intern 487 end 488 else raise FAIL "graph_of_term" 489 end 490 491fun loops_containing_line line graph chain = 492 let val successors = map fst 493 (filter (fn (_,predecs) => mem (Lib.trye hd chain) predecs) graph) 494 val not_in_chain = filter (fn line => not (mem line chain)) successors 495 val new_chains = map (fn line => line::chain) not_in_chain 496 (* flatten(map ...) should be an itlist *) 497 val new_loops = flatten (map (loops_containing_line line graph) 498 new_chains) 499 in if (mem line successors) 500 then (rev chain)::new_loops 501 else new_loops 502 end 503 504fun chop_at x (l as (a::rst)) = 505 if (a = x) then ([],l) 506 else let val (l1,l2) = chop_at x rst 507 in (a::l1, l2) 508 end 509 | chop_at _ _ = raise FAIL "chop_at"; 510 511(* before has infix status in SML/NJ, so changed to befre *) 512fun equal_loops lp1 lp2 = 513 if (set_eq lp1 lp2) 514 then let val (befre,rest) = chop_at (Lib.trye hd lp1) lp2 515 in lp1 = (rest @ befre) 516 end 517 else false 518 519fun distinct_loops [] = [] 520 | distinct_loops (h::t) = 521 if (exists (fn lp => equal_loops lp h) t) 522 then distinct_loops t 523 else h ::(distinct_loops t) 524 525(* Could use an itlist here again and collapse the maps. *) 526fun loops_of_graph graph = 527 distinct_loops 528 (flatten 529 (map (fn line => loops_containing_line line graph [line]) 530 (map fst graph))) 531 532fun list_after x (l as (h::t)) = 533 if (x = h) then t else list_after x t 534 | list_after _ _ = raise UNWIND_ERR "list_after" ""; 535 536fun rev_front_of l n front = 537 if (n < 0) 538 then raise FAIL "rev_front_of" 539 else if (n = 0) 540 then front 541 else rev_front_of (Lib.trye tl l) (n - 1) (Lib.trye hd l ::front) 542 543fun next_comb_at_this_level source n (h::t) = 544 let val l = list_after h source 545 in if (length l > n) 546 then (rev_front_of l (n + 1) []) @ t 547 else next_comb_at_this_level source (n + 1) t 548 end 549 | next_comb_at_this_level _ _ _ = raise FAIL "next_comb_at_this_level" 550 551fun next_combination source previous = 552 next_comb_at_this_level source 0 previous 553 handle HOL_ERR _ => rev_front_of source ((length previous) + 1) [] 554 555fun break_all_loops lps lines previous = 556 let val comb = next_combination lines previous 557 in if (all (fn lp => not (null (intersect lp comb))) lps) 558 then comb 559 else break_all_loops lps lines comb 560 end 561 562fun breaks internals graph = 563 let val loops = loops_of_graph graph 564 val single_el_loops = filter (fn l => length l = 1) loops 565 val single_breaks = flatten single_el_loops 566 val loops' = filter (null o (intersect single_breaks)) loops 567 val only_internal_loops = 568 filter (fn l => null (set_diff l internals)) loops' 569 val only_internal_lines = end_itlist union only_internal_loops 570 handle HOL_ERR _ => [] 571 val internal_breaks = 572 break_all_loops only_internal_loops only_internal_lines [] 573 handle HOL_ERR _ => [] 574 val external_loops = filter (null o (intersect internal_breaks)) loops' 575 val external_lines = 576 set_diff (end_itlist union external_loops handle HOL_ERR _ => []) 577 internals 578 val external_breaks = 579 break_all_loops external_loops external_lines [] 580 handle HOL_ERR _ => [] 581 in single_breaks @ (rev internal_breaks) @ (rev external_breaks) 582 end 583 584 585fun conv dependencies used t = 586 let val vars = map fst (filter ((fn l => null (set_diff l used)) o snd) 587 dependencies) 588 in if (null vars) 589 then REFL t 590 else ((UNWIND_ONCE_CONV (fn tm => mem (line_var tm) vars)) THENC 591 (conv (filter (fn p => not (mem (fst p) vars)) dependencies) 592 (used @ vars))) t 593 end 594in 595fun UNWIND_AUTO_CONV tm = 596 let val internals = fst (strip_exists tm) 597 and graph = graph_of_term tm 598 val brks = breaks internals graph 599 val dependencies = map (I ## (fn l => set_diff l brks)) 600 (filter (fn p => not (mem (fst p) brks)) graph) 601 in DEPTH_EXISTS_CONV (conv dependencies []) tm 602 end handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_AUTO_CONV" "" 603end; 604 605(*---------------------------------------------------------------------------*) 606(* UNWIND_ALL_BUT_RIGHT_RULE : string list -> thm -> thm *) 607(* *) 608(* Unwind all lines (except those in the list l) as much as possible. *) 609(* *) 610(* WARNING -- MAY LOOP! *) 611(* *) 612(* UNWIND_ALL_BUT_RIGHT_RULE l *) 613(* *) 614(* A |- !z1 ... zr. *) 615(* t = *) 616(* (?l1 ... lp. t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn) *) 617(* --------------------------------------------------------------------- *) 618(* A |- !z1 ... zr. *) 619(* t = *) 620(* (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn') *) 621(* *) 622(* where ti' (for 1 <= i <= n) is ti rewritten with the equations *) 623(* eqni (1 <= i <= m). These equations are those conjuncts with line name not*) 624(* in l (and which are equations). *) 625(*---------------------------------------------------------------------------*) 626 627fun UNWIND_ALL_BUT_RIGHT_RULE l th = 628 CONV_RULE 629 (DEPTH_FORALL_CONV (RAND_CONV (DEPTH_EXISTS_CONV (UNWIND_ALL_BUT_CONV l)))) 630 th 631 handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_ALL_BUT_RIGHT_RULE" ""; 632 633(*---------------------------------------------------------------------------*) 634(* UNWIND_AUTO_RIGHT_RULE : thm -> thm *) 635(* *) 636(* A |- !z1 ... zr. t = ?l1 ... lm. t1 /\ ... /\ tn *) 637(* ---------------------------------------------------- *) 638(* A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn' *) 639(* *) 640(* where tj' is tj rewritten with equations selected from the ti's. The *) 641(* function decides which equations to use by performing a loop analysis on *) 642(* the graph representing the dependencies of the lines. By this means the *) 643(* equations can be unwound as much as possible without the risk of looping. *) 644(* The user is left to deal with the recursive equations. *) 645(*---------------------------------------------------------------------------*) 646 647fun UNWIND_AUTO_RIGHT_RULE th = 648 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV UNWIND_AUTO_CONV)) th 649 handle HOL_ERR _ => raise UNWIND_ERR "UNWIND_AUTO_RIGHT_RULE" ""; 650 651(*===========================================================================*) 652(* Rules for pruning *) 653(*===========================================================================*) 654(*---------------------------------------------------------------------------*) 655(* EXISTS_DEL1_CONV : conv *) 656(* *) 657(* "?x. t" *) 658(* ----> *) 659(* |- (?x. t) = t *) 660(* *) 661(* provided x is not free in t. *) 662(* *) 663(* Deletes one existential quantifier. *) 664(*---------------------------------------------------------------------------*) 665 666fun EXISTS_DEL1_CONV tm = 667 let val {Bvar,Body} = dest_exists tm 668 val th = ASSUME Body 669 val th1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) th) 670 and th2 = DISCH Body (EXISTS (tm,Bvar) th) 671 in IMP_ANTISYM_RULE th1 th2 672 end handle HOL_ERR _ => raise UNWIND_ERR"EXISTS_DEL1_CONV" ""; 673 674(*---------------------------------------------------------------------------*) 675(* EXISTS_DEL_CONV : conv *) 676(* *) 677(* "?x1 ... xn. t" *) 678(* ----> *) 679(* |- (?x1 ... xn. t) = t *) 680(* *) 681(* provided x1,...,xn are not free in t. *) 682(* *) 683(* Deletes existential quantifiers. The conversion fails if any of the x's *) 684(* appear free in t. It does not perform a partial deletion; for example, if *) 685(* x1 and x2 do not appear free in t but x3 does, the function will fail; it *) 686(* will not return |- ?x1 ... xn. t = ?x3 ... xn. t. *) 687(*---------------------------------------------------------------------------*) 688 689local fun terms_and_vars tm = 690 let val {Bvar,Body} = dest_exists tm 691 in (tm,Bvar)::terms_and_vars Body 692 end handle HOL_ERR _ => [] 693in 694fun EXISTS_DEL_CONV tm = 695 let val txs = terms_and_vars tm 696 val t = #Body (dest_exists (fst (last txs))) handle _ => tm 697 val th = ASSUME t 698 val th1 = DISCH tm (itlist (fn (tm,x) => CHOOSE (x, ASSUME tm)) txs th) 699 and th2 = DISCH t (itlist EXISTS txs th) 700 in IMP_ANTISYM_RULE th1 th2 701 end 702 handle HOL_ERR _ => raise UNWIND_ERR "EXISTS_DEL_CONV" "" 703end; 704 705(*---------------------------------------------------------------------------*) 706(* EXISTS_EQN_CONV : conv *) 707(* *) 708(* "?l. !y1 ... ym. l x1 ... xn = t" *) 709(* ----> *) 710(* |- (?l. !y1 ... ym. l x1 ... xn = t) = T *) 711(* *) 712(* provided l is not free in t. Both m and n may be zero. *) 713(*---------------------------------------------------------------------------*) 714 715fun EXISTS_EQN_CONV t = 716 let val {Bvar = l,Body} = dest_exists t 717 val (ys,A) = strip_forall Body 718 val {lhs,rhs} = dest_eq A 719 val xs = snd ((assert (curry (op =) l) ## I) (strip_comb lhs)) 720 val t3 = list_mk_abs (xs,rhs) 721 val th1 = GENL ys (RIGHT_CONV_RULE LIST_BETA_CONV 722 (REFL (list_mk_comb (t3,xs)))) 723 in EQT_INTRO (EXISTS (t,t3) th1) 724 end handle HOL_ERR _ => raise UNWIND_ERR "EXISTS_EQN_CONV" ""; 725 726(*---------------------------------------------------------------------------*) 727(* PRUNE_ONCE_CONV : conv *) 728(* *) 729(* Prunes one hidden variable. *) 730(* *) 731(* "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" *) 732(* ----> *) 733(* |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = *) 734(* (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) *) 735(* *) 736(* where eq has the form "!y1 ... ym. l x1 ... xn = b" and l does not appear *) 737(* free in the ti's or in b. The conversion works if eq is not present, *) 738(* i.e. if l is not free in any of the conjuncts, but does not work if l *) 739(* appears free in more than one of the conjuncts. Each of m, n and p may be *) 740(* zero. *) 741(*---------------------------------------------------------------------------*) 742 743local val AP_AND = AP_TERM AND 744in 745fun PRUNE_ONCE_CONV tm = 746 let val {Bvar,Body} = dest_exists tm 747 in 748 case (partition (free_in Bvar) (strip_conj Body)) 749 of ([], _) => EXISTS_DEL1_CONV tm 750 | ([eq],l2) => 751 let val th1 = EXISTS_EQN_CONV (mk_exists {Bvar=Bvar, Body=eq}) 752 in 753 if (null l2) then th1 754 else let val conj = list_mk_conj l2 755 val th2 = AP_THM (AP_AND th1) conj 756 val th3 = EXISTS_EQ Bvar 757 (CONJUNCTS_AC 758 (Body,mk_conj{conj1=eq, conj2=conj})) 759 val th4 = RIGHT_CONV_RULE EXISTS_AND_CONV th3 760 in 761 TRANS th4 (TRANS th2 (CONJUNCT1 (SPEC conj AND_CLAUSES))) 762 end 763 end 764 | _ => raise UNWIND_ERR "" "" 765 end handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_ONCE_CONV" "" 766end; 767 768(*---------------------------------------------------------------------------*) 769(* PRUNE_ONE_CONV : string -> conv *) 770(* *) 771(* Prunes one hidden variable. *) 772(* *) 773(* PRUNE_ONE_CONV "lj" *) 774(* *) 775(* "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" *) 776(* ----> *) 777(* |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = *) 778(* (?l1 ... l(j-1) l(j+1) ... lr. *) 779(* t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) *) 780(* *) 781(* where eq has the form "!y1 ... ym. lj x1 ... xn = b" and lj does not *) 782(* appear free in the ti's or in b. The conversion works if eq is not *) 783(* present, i.e. if lj is not free in any of the conjuncts, but does not work*) 784(* if lj appears free in more than one of the conjuncts. Each of m, n and p *) 785(* may be zero. *) 786(* *) 787(* If there is more than one line with the specified name (but with different*) 788(* types), the one that appears outermost in the existential quantifications *) 789(* is pruned. *) 790(*---------------------------------------------------------------------------*) 791 792fun PRUNE_ONE_CONV v tm = 793 let val {Bvar,Body} = dest_exists tm 794 in if (#Name (dest_var Bvar) = v) 795 then if (is_exists Body) 796 then (SWAP_EXISTS_CONV THENC 797 RAND_CONV (ABS_CONV (PRUNE_ONE_CONV v))) tm 798 else PRUNE_ONCE_CONV tm 799 else RAND_CONV (ABS_CONV (PRUNE_ONE_CONV v)) tm 800 end handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_ONE_CONV" ""; 801 802(*---------------------------------------------------------------------------*) 803(* PRUNE_SOME_CONV : string list -> conv *) 804(* *) 805(* Prunes several hidden variables. *) 806(* *) 807(* PRUNE_SOME_CONV ["li1";...;"lik"] *) 808(* *) 809(* "?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp" *) 810(* ----> *) 811(* |- (?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp) = *) 812(* (?li(k+1) ... lir. t1 /\ ... /\ tp) *) 813(* *) 814(* where for 1 <= j <= k, each eqnij has the form: *) 815(* *) 816(* "!y1 ... ym. lij x1 ... xn = b" *) 817(* *) 818(* and lij does not appear free in any of the other conjuncts or in b. *) 819(* The li's are related by the equation: *) 820(* *) 821(* {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} *) 822(* *) 823(* The conversion works if one or more of the eqnij's are not present, *) 824(* i.e. if lij is not free in any of the conjuncts, but does not work if lij *) 825(* appears free in more than one of the conjuncts. p may be zero, that is, *) 826(* all the conjuncts may be eqnij's. In this case the body of the result will*) 827(* be T (true). Also, for each eqnij, m and n may be zero. *) 828(* *) 829(* If there is more than one line with a specified name (but with different *) 830(* types), the one that appears outermost in the existential quantifications *) 831(* is pruned. If such a line name is mentioned twice in the list, the two *) 832(* outermost occurrences of lines with that name will be pruned, and so on. *) 833(*---------------------------------------------------------------------------*) 834 835fun PRUNE_SOME_CONV [] tm = REFL tm 836 | PRUNE_SOME_CONV (h::t) tm = 837 (PRUNE_SOME_CONV t THENC PRUNE_ONE_CONV h) tm 838 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_SOME_CONV" ""; 839 840(*---------------------------------------------------------------------------*) 841(* PRUNE_CONV : conv *) 842(* *) 843(* Prunes all hidden variables. *) 844(* *) 845(* "?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp" *) 846(* ----> *) 847(* |- (?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp) = *) 848(* (t1 /\ ... /\ tp) *) 849(* *) 850(* where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does *) 851(* not appear free in any of the other conjuncts or in b. The conversion *) 852(* works if one or more of the eqni's are not present, i.e. if li is not free*) 853(* in any of the conjuncts, but does not work if li appears free in more than*) 854(* one of the conjuncts. p may be zero, that is, all the conjuncts may be *) 855(* eqni's. In this case the result will be simply T (true). Also, for each *) 856(* eqni, m and n may be zero. *) 857(*---------------------------------------------------------------------------*) 858 859fun PRUNE_CONV tm = 860 if (is_exists tm) 861 then (RAND_CONV (ABS_CONV PRUNE_CONV) THENC PRUNE_ONCE_CONV) tm 862 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_CONV" "" 863 else REFL tm; 864 865(*---------------------------------------------------------------------------*) 866(* PRUNE_SOME_RIGHT_RULE : string list -> thm -> thm *) 867(* *) 868(* Prunes several hidden variables. *) 869(* *) 870(* PRUNE_SOME_RIGHT_RULE ["li1";...;"lik"] *) 871(* *) 872(* A |- !z1 ... zr. *) 873(* t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp *) 874(* -----------------------------------------------------------------------*) 875(* A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp *) 876(* *) 877(* where for 1 <= j <= k, each eqnij has the form: *) 878(* *) 879(* "!y1 ... ym. lij x1 ... xn = b" *) 880(* *) 881(* and lij does not appear free in any of the other conjuncts or in b. *) 882(* The li's are related by the equation: *) 883(* *) 884(* {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} *) 885(* *) 886(* The rule works if one or more of the eqnij's are not present, i.e. if lij *) 887(* is not free in any of the conjuncts, but does not work if lij appears free*) 888(* in more than one of the conjuncts. p may be zero, that is, all the *) 889(* conjuncts may be eqnij's. In this case the conjunction will be transformed*) 890(* to T (true). Also, for each eqnij, m and n may be zero. *) 891(* *) 892(* If there is more than one line with a specified name (but with different *) 893(* types), the one that appears outermost in the existential quantifications *) 894(* is pruned. If such a line name is mentioned twice in the list, the two *) 895(* outermost occurrences of lines with that name will be pruned, and so on. *) 896(*---------------------------------------------------------------------------*) 897 898fun PRUNE_SOME_RIGHT_RULE vs th = 899 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (PRUNE_SOME_CONV vs))) th 900 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_SOME_RIGHT_RULE" ""; 901 902(*---------------------------------------------------------------------------*) 903(* PRUNE_RIGHT_RULE : thm -> thm *) 904(* *) 905(* Prunes all hidden variables. *) 906(* *) 907(* A |- !z1 ... zr. *) 908(* t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp *) 909(* --------------------------------------------------------------------- *) 910(* A |- !z1 ... zr. t = t1 /\ ... /\ tp *) 911(* *) 912(* where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does *) 913(* not appear free in any of the other conjuncts or in b. The rule works if *) 914(* one or more of the eqni's are not present, i.e. if li is not free in any *) 915(* of the conjuncts, but does not work if li appears free in more than one of*) 916(* the conjuncts. p may be zero, that is, all the conjuncts may be eqni's. In*) 917(* this case the result will be simply T (true). Also, for each eqni, m and n*) 918(* may be zero. *) 919(*---------------------------------------------------------------------------*) 920 921fun PRUNE_RIGHT_RULE th = 922 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV PRUNE_CONV)) th 923 handle HOL_ERR _ => raise UNWIND_ERR "PRUNE_RIGHT_RULE" ""; 924 925(*===========================================================================*) 926(* Functions which do unfolding, unwinding and pruning *) 927(*===========================================================================*) 928 929(*---------------------------------------------------------------------------*) 930(* EXPAND_ALL_BUT_CONV : string list -> thm list -> conv *) 931(* *) 932(* Unfold with the theorems thl, then unwind all lines (except those in the *) 933(* list) as much as possible and prune the unwound lines. *) 934(* *) 935(* WARNING -- MAY LOOP! *) 936(* *) 937(* EXPAND_ALL_BUT_CONV ["li(k+1)";...;"lim"] thl *) 938(* *) 939(* "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" *) 940(* ----> *) 941(* B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = *) 942(* (?li(k+1) ... lim. t1' /\ ... /\ tn') *) 943(* *) 944(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 945(* set of assumptions B is the union of the instantiated assumptions of the *) 946(* theorems used for rewriting. If none of the rewrites are applicable to a *) 947(* conjunct, it is unchanged. Those conjuncts that after rewriting are *) 948(* equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are *) 949(* used to unwind and the lines li1,...,lik are then pruned. If this is not *) 950(* possible the function will fail. It is also possible for the function to *) 951(* attempt unwinding indefinitely (to loop). *) 952(* *) 953(* The li's are related by the equation: *) 954(* *) 955(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 956(*---------------------------------------------------------------------------*) 957fun EXPAND_ALL_BUT_CONV l thl tm = 958 (DEPTH_EXISTS_CONV ((UNFOLD_CONV thl) THENC (UNWIND_ALL_BUT_CONV l)) THENC 959 (fn tm => let val var_names = map (#Name o dest_var) (fst(strip_exists tm)) 960 in PRUNE_SOME_CONV (subtract var_names l) tm 961 end)) 962 tm handle HOL_ERR _ => raise UNWIND_ERR"EXPAND_ALL_BUT_CONV" ""; 963 964(*---------------------------------------------------------------------------*) 965(* EXPAND_AUTO_CONV : thm list -> conv *) 966(* *) 967(* Unfold with the theorems thl, then unwind as much as possible and prune *) 968(* the unwound lines. *) 969(* *) 970(* EXPAND_AUTO_CONV thl *) 971(* *) 972(* "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" *) 973(* ----> *) 974(* B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = *) 975(* (?li(k+1) ... lim. t1' /\ ... /\ tn') *) 976(* *) 977(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 978(* set of assumptions B is the union of the instantiated assumptions of the *) 979(* theorems used for rewriting. If none of the rewrites are applicable to a *) 980(* conjunct, it is unchanged. After rewriting the function decides which of *) 981(* the resulting terms to use for unwinding by performing a loop analysis on *) 982(* the graph representing the dependencies of the lines. *) 983(* *) 984(* Suppose the function decides to unwind the lines li1,...,lik using the *) 985(* terms ui1',...,uik' respectively. Then after unwinding the lines *) 986(* li1,...,lik are pruned (provided they have been eliminated from the RHS's *) 987(* of the conjuncts that are equations, and from the whole of any other *) 988(* conjuncts) resulting in the elimination of ui1',...,uik'. *) 989(* *) 990(* The li's are related by the equation: *) 991(* *) 992(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 993(* *) 994(* The loop analysis allows the term to be unwound as much as possible *) 995(* without the risk of looping. The user is left to deal with the recursive *) 996(* equations. *) 997(*---------------------------------------------------------------------------*) 998 999fun EXPAND_AUTO_CONV thl tm = 1000 (DEPTH_EXISTS_CONV (UNFOLD_CONV thl) THENC 1001 UNWIND_AUTO_CONV THENC 1002 (fn tm => 1003 let val (internals,conjs) = (I ## strip_conj) (strip_exists tm) 1004 val vars = flatten (map 1005 (free_vars o (fn tm => (rhs tm) handle HOL_ERR _ => tm) 1006 o snd o strip_forall) conjs) 1007 in PRUNE_SOME_CONV(map (#Name o dest_var) (set_diff internals vars)) tm 1008 end)) 1009 tm 1010 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_AUTO_CONV" ""; 1011 1012(*---------------------------------------------------------------------------*) 1013(* EXPAND_ALL_BUT_RIGHT_RULE : string list -> thm list -> thm -> thm *) 1014(* *) 1015(* Unfold with the theorems thl, then unwind all lines (except those in the *) 1016(* list) as much as possible and prune the unwound lines. *) 1017(* *) 1018(* WARNING -- MAY LOOP! *) 1019(* *) 1020(* EXPAND_ALL_BUT_RIGHT_RULE ["li(k+1)";...;"lim"] thl *) 1021(* *) 1022(* A |- !z1 ... zr. *) 1023(* t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn *) 1024(* -----------------------------------------------------------------------*) 1025(* B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' *) 1026(* *) 1027(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 1028(* set of assumptions B is the union of the instantiated assumptions of the *) 1029(* theorems used for rewriting. If none of the rewrites are applicable to a *) 1030(* conjunct, it is unchanged. Those conjuncts that after rewriting are *) 1031(* equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are *) 1032(* used to unwind and the lines li1,...,lik are then pruned. If this is not *) 1033(* possible the function will fail. It is also possible for the function to *) 1034(* attempt unwinding indefinitely (to loop). *) 1035(* *) 1036(* The li's are related by the equation: *) 1037(* *) 1038(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 1039(*---------------------------------------------------------------------------*) 1040 1041fun EXPAND_ALL_BUT_RIGHT_RULE l thl th = 1042 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (EXPAND_ALL_BUT_CONV l thl))) th 1043 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_ALL_BUT_RIGHT_RULE" ""; 1044 1045(*---------------------------------------------------------------------------*) 1046(* EXPAND_AUTO_RIGHT_RULE : thm list -> thm -> thm *) 1047(* *) 1048(* Unfold with the theorems thl, then unwind as much as possible and prune *) 1049(* the unwound lines. *) 1050(* *) 1051(* EXPAND_AUTO_RIGHT_RULE thl *) 1052(* *) 1053(* A |- !z1 ... zr. *) 1054(* t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn *) 1055(* -----------------------------------------------------------------------*) 1056(* B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' *) 1057(* *) 1058(* where each ti' is the result of rewriting ti with the theorems in thl. The*) 1059(* set of assumptions B is the union of the instantiated assumptions of the *) 1060(* theorems used for rewriting. If none of the rewrites are applicable to a *) 1061(* conjunct, it is unchanged. After rewriting the function decides which of *) 1062(* the resulting terms to use for unwinding by performing a loop analysis on *) 1063(* the graph representing the dependencies of the lines. *) 1064(* *) 1065(* Suppose the function decides to unwind the lines li1,...,lik using the *) 1066(* terms ui1',...,uik' respectively. Then after unwinding the lines *) 1067(* li1,...,lik are pruned (provided they have been eliminated from the RHS's *) 1068(* of the conjuncts that are equations, and from the whole of any other *) 1069(* conjuncts) resulting in the elimination of ui1',...,uik'. *) 1070(* *) 1071(* The li's are related by the equation: *) 1072(* *) 1073(* {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} *) 1074(* *) 1075(* The loop analysis allows the term to be unwound as much as possible *) 1076(* without the risk of looping. The user is left to deal with the recursive *) 1077(* equations. *) 1078(*---------------------------------------------------------------------------*) 1079 1080fun EXPAND_AUTO_RIGHT_RULE thl th = 1081 CONV_RULE (DEPTH_FORALL_CONV (RAND_CONV (EXPAND_AUTO_CONV thl))) th 1082 handle HOL_ERR _ => raise UNWIND_ERR "EXPAND_AUTO_RIGHT_RULE" ""; 1083 1084 1085end; (* unwindLib *) 1086