## File: entries.tex

package info (click to toggle)
hol88 2.02.19940316-35
 1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351 \chapter{ML Functions in the unwind Library}\input{entries-intro}\DOC{CONJ\_FORALL\_CONV} \TYPE {\small\verb%CONJ_FORALL_CONV : conv%}\egroup \SYNOPSIS Moves universal quantifiers up through a tree of conjunctions. \DESCRIBE {\small\verb%CONJ_FORALL_CONV "(!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)"%} returns the following theorem: {\par\samepage\setseps\small \begin{verbatim} |- (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) = !x1 ... xm. t1 /\ ... /\ tn \end{verbatim} } \noindent where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (y:*) (z:*). b)) /\ # (!(x:*) (y:*) (z:*). c)";; |- ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c) = (!x y z. (a /\ b) /\ c) #CONJ_FORALL_CONV "T";; |- T = T #CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (w:*) (z:*). b)) /\ # (!(x:*) (y:*) (z:*). c)";; |- ((!x y z. a) /\ (!x w z. b)) /\ (!x y z. c) = (!x. ((!y z. a) /\ (!w z. b)) /\ (!y z. c)) \end{verbatim} } \SEEALSO FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE. \ENDDOC \DOC{CONJ\_FORALL\_ONCE\_CONV} \TYPE {\small\verb%CONJ_FORALL_ONCE_CONV : conv%}\egroup \SYNOPSIS Moves a single universal quantifier up through a tree of conjunctions. \DESCRIBE {\small\verb%CONJ_FORALL_ONCE_CONV "(!x. t1) /\ ... /\ (!x. tn)"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- (!x. t1) /\ ... /\ (!x. tn) = !x. t1 /\ ... /\ tn \end{verbatim} } \noindent where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation. \FAILURE Fails if the argument term is not of the required form. The term need not be a conjunction, but if it is every conjunct must be universally quantified with the same variable. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c)";; |- ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c) = (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)) #CONJ_FORALL_ONCE_CONV "!x. x \/ a";; |- (!x. x \/ a) = (!x. x \/ a) #CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!y. y \/ b)) /\ (!x. x \/ c)";; evaluation failed CONJ_FORALL_ONCE_CONV \end{verbatim} } \SEEALSO FORALL_CONJ_ONCE_CONV, CONJ_FORALL_CONV, FORALL_CONJ_CONV, CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE. \ENDDOC \DOC{CONJ\_FORALL\_RIGHT\_RULE} \TYPE {\small\verb%CONJ_FORALL_RIGHT_RULE : (thm -> thm)%}\egroup \SYNOPSIS Moves universal quantifiers up through a tree of conjunctions. \DESCRIBE {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) ------------------------------------------------------------------- A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn \end{verbatim} } \FAILURE Fails if the argument theorem is not of the required form, though either or both of {\small\verb%r%} and {\small\verb%p%} may be zero. \SEEALSO FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_CONV, FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV. \ENDDOC \DOC{DEPTH\_EXISTS\_CONV} \TYPE {\small\verb%DEPTH_EXISTS_CONV : (conv -> conv)%}\egroup \SYNOPSIS Applies a conversion to the body of nested existential quantifications. \DESCRIBE {\small\verb%DEPTH_EXISTS_CONV conv "?x1 ... xn. body"%} applies {\small\verb%conv%} to {\small\verb%"body"%} and returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?x1 ... xn. body) = (?x1 ... xn. body') \end{verbatim} } \FAILURE Fails if the application of {\small\verb%conv%} fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #DEPTH_EXISTS_CONV BETA_CONV "?x y z. (\w. x /\ y /\ z /\ w) T";; |- (?x y z. (\w. x /\ y /\ z /\ w)T) = (?x y z. x /\ y /\ z /\ T) \end{verbatim} } \SEEALSO DEPTH_FORALL_CONV. \ENDDOC \DOC{DEPTH\_FORALL\_CONV} \TYPE {\small\verb%DEPTH_FORALL_CONV : (conv -> conv)%}\egroup \SYNOPSIS Applies a conversion to the body of nested universal quantifications. \DESCRIBE {\small\verb%DEPTH_FORALL_CONV conv "!x1 ... xn. body"%} applies {\small\verb%conv%} to {\small\verb%"body"%} and returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (!x1 ... xn. body) = (!x1 ... xn. body') \end{verbatim} } \FAILURE Fails if the application of {\small\verb%conv%} fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #DEPTH_FORALL_CONV BETA_CONV "!x y z. (\w. x /\ y /\ z /\ w) T";; |- (!x y z. (\w. x /\ y /\ z /\ w)T) = (!x y z. x /\ y /\ z /\ T) \end{verbatim} } \SEEALSO DEPTH_EXISTS_CONV. \ENDDOC \DOC{EXISTS\_DEL1\_CONV} \TYPE {\small\verb%EXISTS_DEL1_CONV : conv%}\egroup \SYNOPSIS Deletes one existential quantifier. \DESCRIBE {\small\verb%EXISTS_DEL1_CONV "?x. t"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- (?x. t) = t \end{verbatim} } \noindent provided {\small\verb%x%} is not free in {\small\verb%t%}. \FAILURE Fails if the argument term is not an existential quantification or if {\small\verb%x%} is free in {\small\verb%t%}. \SEEALSO EXISTS_DEL_CONV, PRUNE_ONCE_CONV. \ENDDOC \DOC{EXISTS\_DEL\_CONV} \TYPE {\small\verb%EXISTS_DEL_CONV : conv%}\egroup \SYNOPSIS Deletes existential quantifiers. \DESCRIBE {\small\verb%EXISTS_DEL_CONV "?x1 ... xn. t"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- (?x1 ... xn. t) = t \end{verbatim} } \noindent provided {\small\verb%x1,...,xn%} are not free in {\small\verb%t%}. \FAILURE Fails if any of the {\small\verb%x%}'s appear free in {\small\verb%t%}. The function does not perform a partial deletion; for example, if {\small\verb%x1%} and {\small\verb%x2%} do not appear free in {\small\verb%t%} but {\small\verb%x3%} does, the function will fail; it will not return: {\par\samepage\setseps\small \begin{verbatim} |- ?x1 ... xn. t = ?x3 ... xn. t \end{verbatim} } \SEEALSO EXISTS_DEL1_CONV, PRUNE_CONV. \ENDDOC \DOC{EXISTS\_EQN\_CONV} \TYPE {\small\verb%EXISTS_EQN_CONV : conv%}\egroup \SYNOPSIS Proves the existence of a line that has a non-recursive equation. \DESCRIBE {\small\verb%EXISTS_EQN_CONV "?l. !y1 ... ym. l x1 ... xn = t"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- (?l. !y1 ... ym. l x1 ... xn = t) = T \end{verbatim} } \noindent provided {\small\verb%l%} is not free in {\small\verb%t%}. Both {\small\verb%m%} and {\small\verb%n%} may be zero. \FAILURE Fails if the argument term is not of the specified form or if {\small\verb%l%} appears free in {\small\verb%t%}. \SEEALSO PRUNE_ONCE_CONV. \ENDDOC \DOC{EXPAND\_ALL\_BUT\_CONV} \TYPE {\small\verb%EXPAND_ALL_BUT_CONV : (string list -> thm list -> conv)%}\egroup \SYNOPSIS Unfolds, then unwinds all lines (except those specified) as much as possible, then prunes the unwound lines. \DESCRIBE {\small\verb%EXPAND_ALL_BUT_CONV [li(k+1);...;lim] thl%} when applied to the following term: {\par\samepage\setseps\small \begin{verbatim} "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" \end{verbatim} } \noindent returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = (?li(k+1) ... lim. t1' /\ ... /\ tn') \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. Those conjuncts that after rewriting are equations for the lines {\small\verb%li1,...,lik%} (they are denoted by {\small\verb%ui1,...,uik%}) are used to unwind and the lines {\small\verb%li1,...,lik%} are then pruned. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} \end{verbatim} } \FAILURE The function may fail if the argument term is not of the specified form. It will also fail if the unwound lines cannot be pruned. It is possible for the function to attempt unwinding indefinitely (to loop). \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #EXPAND_ALL_BUT_CONV [l1] # [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] # "?l1 l2. # INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";; . |- (?l1 l2. INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) = (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1))) \end{verbatim} } \SEEALSO EXPAND_AUTO_CONV, EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_RIGHT_RULE, UNFOLD_CONV, UNWIND_ALL_BUT_CONV, PRUNE_SOME_CONV. \ENDDOC \DOC{EXPAND\_ALL\_BUT\_RIGHT\_RULE} \TYPE {\small\verb%EXPAND_ALL_BUT_RIGHT_RULE : (string list -> thm list -> thm -> thm)%}\egroup \SYNOPSIS Unfolds, then unwinds all lines (except those specified) as much as possible, then prunes the unwound lines. \DESCRIBE {\small\verb%EXPAND_ALL_BUT_RIGHT_RULE [li(k+1);...;lim] thl%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn ------------------------------------------------------------------- B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. Those conjuncts that after rewriting are equations for the lines {\small\verb%li1,...,lik%} (they are denoted by {\small\verb%ui1,...,uik%}) are used to unwind and the lines {\small\verb%li1,...,lik%} are then pruned. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} \end{verbatim} } \FAILURE The function may fail if the argument theorem is not of the specified form. It will also fail if the unwound lines cannot be pruned. It is possible for the function to attempt unwinding indefinitely (to loop). \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #EXPAND_ALL_BUT_RIGHT_RULE [l1] # [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] # (ASSUME # "!(in:num->bool) out. # DEV(in,out) = # ?l1 l2. # INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");; .. |- !in out. DEV(in,out) = (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = in t \/ ~~l1(t - 1))) \end{verbatim} } \SEEALSO EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_CONV, EXPAND_AUTO_CONV, UNFOLD_RIGHT_RULE, UNWIND_ALL_BUT_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE. \ENDDOC \DOC{EXPAND\_AUTO\_CONV} \TYPE {\small\verb%EXPAND_AUTO_CONV : (thm list -> conv)%}\egroup \SYNOPSIS Unfolds, then unwinds as much as possible, then prunes the unwound lines. \DESCRIBE {\small\verb%EXPAND_AUTO_CONV thl%} when applied to the following term: {\par\samepage\setseps\small \begin{verbatim} "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" \end{verbatim} } \noindent returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = (?li(k+1) ... lim. t1' /\ ... /\ tn') \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. After rewriting, the function decides which of the resulting terms to use for unwinding, by performing a loop analysis on the graph representing the dependencies of the lines. Suppose the function decides to unwind {\small\verb%li1,...,lik%} using the terms {\small\verb%ui1',...,uik'%} respectively. Then, after unwinding, the lines {\small\verb%li1,...,lik%} are pruned (provided they have been eliminated from the right-hand sides of the conjuncts that are equations, and from the whole of any other conjuncts) resulting in the elimination of {\small\verb%ui1',...,uik'%}. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} \end{verbatim} } \noindent The loop analysis allows the term to be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations. \FAILURE The function may fail if the argument term is not of the specified form. It also fails if there is more than one equation for any line variable. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #EXPAND_AUTO_CONV # [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] # "?l1 l2. # INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";; . |- (?l1 l2. INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) = (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1))) \end{verbatim} } \SEEALSO EXPAND_ALL_BUT_CONV, EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_RIGHT_RULE, UNFOLD_CONV, UNWIND_AUTO_CONV, PRUNE_SOME_CONV. \ENDDOC \DOC{EXPAND\_AUTO\_RIGHT\_RULE} \TYPE {\small\verb%EXPAND_AUTO_RIGHT_RULE : (thm list -> thm -> thm)%}\egroup \SYNOPSIS Unfolds, then unwinds as much as possible, then prunes the unwound lines. \DESCRIBE {\small\verb%EXPAND_AUTO_RIGHT_RULE thl%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn ------------------------------------------------------------------- B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. After rewriting, the function decides which of the resulting terms to use for unwinding, by performing a loop analysis on the graph representing the dependencies of the lines. Suppose the function decides to unwind {\small\verb%li1,...,lik%} using the terms {\small\verb%ui1',...,uik'%} respectively. Then, after unwinding, the lines {\small\verb%li1,...,lik%} are pruned (provided they have been eliminated from the right-hand sides of the conjuncts that are equations, and from the whole of any other conjuncts) resulting in the elimination of {\small\verb%ui1',...,uik'%}. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm} \end{verbatim} } \noindent The loop analysis allows the term to be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations. \FAILURE The function may fail if the argument theorem is not of the specified form. It also fails if there is more than one equation for any line variable. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #EXPAND_AUTO_RIGHT_RULE # [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] # (ASSUME # "!(in:num->bool) out. # DEV(in,out) = # ?l1 l2. # INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");; .. |- !in out. DEV(in,out) = (!t. out t = ~~(in t \/ out(t - 1))) \end{verbatim} } \SEEALSO EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_CONV, EXPAND_ALL_BUT_CONV, UNFOLD_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE. \ENDDOC \DOC{FLATTEN\_CONJ\_CONV} \TYPE {\small\verb%FLATTEN_CONJ_CONV : conv%}\egroup \SYNOPSIS Flattens a tree' of conjunctions. \DESCRIBE {\small\verb%FLATTEN_CONJ_CONV "t1 /\ ... /\ tn"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- t1 /\ ... /\ tn = u1 /\ ... /\ un \end{verbatim} } \noindent where the right-hand side of the equation is a flattened version of the left-hand side. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FLATTEN_CONJ_CONV "(a /\ (b /\ c)) /\ ((d /\ e) /\ f)";; |- (a /\ b /\ c) /\ (d /\ e) /\ f = a /\ b /\ c /\ d /\ e /\ f \end{verbatim} } \SEEALSO CONJUNCTS_CONV. \ENDDOC \DOC{FORALL\_CONJ\_CONV} \TYPE {\small\verb%FORALL_CONJ_CONV : conv%}\egroup \SYNOPSIS Moves universal quantifiers down through a tree of conjunctions. \DESCRIBE {\small\verb%FORALL_CONJ_CONV "!x1 ... xm. t1 /\ ... /\ tn"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- !x1 ... xm. t1 /\ ... /\ tn = (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) \end{verbatim} } \noindent where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). (a /\ b) /\ c";; |- (!x y z. (a /\ b) /\ c) = ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c) #FORALL_CONJ_CONV "T";; |- T = T #FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). T";; |- (!x y z. T) = (!x y z. T) \end{verbatim} } \SEEALSO CONJ_FORALL_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE. \ENDDOC \DOC{FORALL\_CONJ\_ONCE\_CONV} \TYPE {\small\verb%FORALL_CONJ_ONCE_CONV : conv%}\egroup \SYNOPSIS Moves a single universal quantifier down through a tree of conjunctions. \DESCRIBE {\small\verb%FORALL_CONJ_ONCE_CONV "!x. t1 /\ ... /\ tn"%} returns the theorem: {\par\samepage\setseps\small \begin{verbatim} |- !x. t1 /\ ... /\ tn = (!x. t1) /\ ... /\ (!x. tn) \end{verbatim} } \noindent where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation. \FAILURE Fails if the argument term is not of the required form. The body of the term need not be a conjunction. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)";; |- (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)) = ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c) #FORALL_CONJ_ONCE_CONV "!x. x \/ a";; |- (!x. x \/ a) = (!x. x \/ a) #FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)";; |- (!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)) = ((!x. x \/ a) /\ (!x. y \/ b)) /\ (!x. x \/ c) \end{verbatim} } \SEEALSO CONJ_FORALL_ONCE_CONV, FORALL_CONJ_CONV, CONJ_FORALL_CONV, FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE. \ENDDOC \DOC{FORALL\_CONJ\_RIGHT\_RULE} \TYPE {\small\verb%FORALL_CONJ_RIGHT_RULE : (thm -> thm)%}\egroup \SYNOPSIS Moves universal quantifiers down through a tree of conjunctions. \DESCRIBE {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn ------------------------------------------------------------------- A |- !z1 ... zr. t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) \end{verbatim} } \FAILURE Fails if the argument theorem is not of the required form, though either or both of {\small\verb%r%} and {\small\verb%p%} may be zero. \SEEALSO CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_CONV, CONJ_FORALL_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV. \ENDDOC \DOC{line\_name} \TYPE {\small\verb%line_name : (term -> string)%}\egroup \SYNOPSIS Computes the line name of an equation. \DESCRIBE {\small\verb%line_name "!y1 ... ym. f x1 ... xn = t"%} returns the string {\small\verb%f%}. \FAILURE Fails if the argument term is not of the specified form. \SEEALSO line_var. \ENDDOC \DOC{line\_var} \TYPE {\small\verb%line_var : (term -> term)%}\egroup \SYNOPSIS Computes the line variable of an equation. \DESCRIBE {\small\verb%line_var "!y1 ... ym. f x1 ... xn = t"%} returns the variable {\small\verb%"f"%}. \FAILURE Fails if the argument term is not of the specified form. \SEEALSO line_name. \ENDDOC \DOC{PRUNE\_CONV} \TYPE {\small\verb%PRUNE_CONV : conv%}\egroup \SYNOPSIS Prunes all hidden variables. \DESCRIBE {\small\verb%PRUNE_CONV "?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp) = (t1 /\ ... /\ tp) \end{verbatim} } \noindent where each {\small\verb%eqni%} has the form {\small\verb%"!y1 ... ym. li x1 ... xn = b"%} and {\small\verb%li%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The conversion works if one or more of the {\small\verb%eqni%}'s are not present, that is if {\small\verb%li%} is not free in any of the conjuncts, but does not work if {\small\verb%li%} appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the conjuncts may be {\small\verb%eqni%}'s. In this case the result will be simply {\small\verb%T%} (true). Also, for each {\small\verb%eqni%}, {\small\verb%m%} and {\small\verb%n%} may be zero. \FAILURE Fails if the argument term is not of the specified form or if any of the {\small\verb%li%}'s are free in more than one of the conjuncts or if the equation for any {\small\verb%li%} is recursive. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_CONV # "?l2 l1. # (!(x:num). l1 x = F) /\ (!x. l2 x = ~(out x)) /\ (!(x:num). out x = T)";; |- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~out x) /\ (!x. out x = T)) = (!x. out x = T) \end{verbatim} } \SEEALSO PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_SOME_RIGHT_RULE, PRUNE_RIGHT_RULE. \ENDDOC \DOC{PRUNE\_ONCE\_CONV} \TYPE {\small\verb%PRUNE_ONCE_CONV : conv%}\egroup \SYNOPSIS Prunes one hidden variable. \DESCRIBE {\small\verb%PRUNE_ONCE_CONV "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) \end{verbatim} } \noindent where {\small\verb%eq%} has the form {\small\verb%"!y1 ... ym. l x1 ... xn = b"%} and {\small\verb%l%} does not appear free in the {\small\verb%ti%}'s or in {\small\verb%b%}. The conversion works if {\small\verb%eq%} is not present, that is if {\small\verb%l%} is not free in any of the conjuncts, but does not work if {\small\verb%l%} appears free in more than one of the conjuncts. Each of {\small\verb%m%}, {\small\verb%n%} and {\small\verb%p%} may be zero. \FAILURE Fails if the argument term is not of the specified form or if {\small\verb%l%} is free in more than one of the conjuncts or if the equation for {\small\verb%l%} is recursive. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_ONCE_CONV "?l2. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";; |- (?l2. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (!x. l1 x = F) \end{verbatim} } \SEEALSO PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE, PRUNE_RIGHT_RULE. \ENDDOC \DOC{PRUNE\_ONE\_CONV} \TYPE {\small\verb%PRUNE_ONE_CONV : (string -> conv)%}\egroup \SYNOPSIS Prunes a specified hidden variable. \DESCRIBE {\small\verb%PRUNE_ONE_CONV lj%} when applied to the term: {\par\samepage\setseps\small \begin{verbatim} "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" \end{verbatim} } \noindent returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) = (?l1 ... l(j-1) l(j+1) ... lr. t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp) \end{verbatim} } \noindent where {\small\verb%eq%} has the form {\small\verb%"!y1 ... ym. lj x1 ... xn = b"%} and {\small\verb%lj%} does not appear free in the {\small\verb%ti%}'s or in {\small\verb%b%}. The conversion works if {\small\verb%eq%} is not present, that is if {\small\verb%lj%} is not free in any of the conjuncts, but does not work if {\small\verb%lj%} appears free in more than one of the conjuncts. Each of {\small\verb%m%}, {\small\verb%n%} and {\small\verb%p%} may be zero. If there is more than one line with the specified name (but with different types), the one that appears outermost in the existential quantifications is pruned. \FAILURE Fails if the argument term is not of the specified form or if {\small\verb%lj%} is free in more than one of the conjuncts or if the equation for {\small\verb%lj%} is recursive. The function also fails if the specified line is not one of the existentially quantified lines. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_ONE_CONV l2 "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";; |- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (?l1. !x. l1 x = F) #PRUNE_ONE_CONV l1 "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";; evaluation failed PRUNE_ONE_CONV \end{verbatim} } \SEEALSO PRUNE_ONCE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE, PRUNE_RIGHT_RULE. \ENDDOC \DOC{PRUNE\_RIGHT\_RULE} \TYPE {\small\verb%PRUNE_RIGHT_RULE : (thm -> thm)%}\egroup \SYNOPSIS Prunes all hidden variables. \DESCRIBE {\small\verb%PRUNE_RIGHT_RULE%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp --------------------------------------------------------------------- A |- !z1 ... zr. t = t1 /\ ... /\ tp \end{verbatim} } \noindent where each {\small\verb%eqni%} has the form {\small\verb%"!y1 ... ym. li x1 ... xn = b"%} and {\small\verb%li%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The rule works if one or more of the {\small\verb%eqni%}'s are not present, that is if {\small\verb%li%} is not free in any of the conjuncts, but does not work if {\small\verb%li%} appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the conjuncts may be {\small\verb%eqni%}'s. In this case the result will be simply {\small\verb%T%} (true). Also, for each {\small\verb%eqni%}, {\small\verb%m%} and {\small\verb%n%} may be zero. \FAILURE Fails if the argument theorem is not of the specified form or if any of the {\small\verb%li%}'s are free in more than one of the conjuncts or if the equation for any {\small\verb%li%} is recursive. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_RIGHT_RULE # (ASSUME # "!(in:num->bool) (out:num->bool). # DEV (in,out) = # ?(l1:num->bool) l2. # (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");; . |- !in out. DEV(in,out) = (!x. out x = ~in x) \end{verbatim} } \SEEALSO PRUNE_SOME_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV. \ENDDOC \DOC{PRUNE\_SOME\_CONV} \TYPE {\small\verb%PRUNE_SOME_CONV : (string list -> conv)%}\egroup \SYNOPSIS Prunes several hidden variables. \DESCRIBE {\small\verb%PRUNE_SOME_CONV [li1;...;lik]%} when applied to the term: {\par\samepage\setseps\small \begin{verbatim} "?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp" \end{verbatim} } \noindent returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp) = (?li(k+1) ... lir. t1 /\ ... /\ tp) \end{verbatim} } \noindent where for {\small\verb%1 <= j <= k%}, each {\small\verb%eqnij%} has the form: {\par\samepage\setseps\small \begin{verbatim} "!y1 ... ym. lij x1 ... xn = b" \end{verbatim} } \noindent and {\small\verb%lij%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} \end{verbatim} } \noindent The conversion works if one or more of the {\small\verb%eqnij%}'s are not present, that is if {\small\verb%lij%} is not free in any of the conjuncts, but does not work if {\small\verb%lij%} appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the conjuncts may be {\small\verb%eqnij%}'s. In this case the body of the result will be {\small\verb%T%} (true). Also, for each {\small\verb%eqnij%}, {\small\verb%m%} and {\small\verb%n%} may be zero. If there is more than one line with a specified name (but with different types), the one that appears outermost in the existential quantifications is pruned. If such a line name is mentioned twice in the list, the two outermost occurrences of lines with that name will be pruned, and so on. \FAILURE Fails if the argument term is not of the specified form or if any of the {\small\verb%lij%}'s are free in more than one of the conjuncts or if the equation for any {\small\verb%lij%} is recursive. The function also fails if any of the specified lines are not one of the existentially quantified lines. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_SOME_CONV [l1;l2] # "?l3 l2 l1. # (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l3 x)) /\ (!(x:num). l3 x = T)";; |- (?l3 l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l3 x) /\ (!x. l3 x = T)) = (?l3. !x. l3 x = T) \end{verbatim} } \SEEALSO PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE, PRUNE_RIGHT_RULE. \ENDDOC \DOC{PRUNE\_SOME\_RIGHT\_RULE} \TYPE {\small\verb%PRUNE_SOME_RIGHT_RULE : (string list -> thm -> thm)%}\egroup \SYNOPSIS Prunes several hidden variables. \DESCRIBE {\small\verb%PRUNE_SOME_RIGHT_RULE [li1;...;lik]%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp ----------------------------------------------------------------------- A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp \end{verbatim} } \noindent where for {\small\verb%1 <= j <= k%}, each {\small\verb%eqnij%} has the form: {\par\samepage\setseps\small \begin{verbatim} "!y1 ... ym. lij x1 ... xn = b" \end{verbatim} } \noindent and {\small\verb%lij%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The {\small\verb%li%}'s are related by the equation: {\par\samepage\setseps\small \begin{verbatim} {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr} \end{verbatim} } \noindent The rule works if one or more of the {\small\verb%eqnij%}'s are not present, that is if {\small\verb%lij%} is not free in any of the conjuncts, but does not work if {\small\verb%lij%} appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the conjuncts may be {\small\verb%eqnij%}'s. In this case the conjunction will be transformed to {\small\verb%T%} (true). Also, for each {\small\verb%eqnij%}, {\small\verb%m%} and {\small\verb%n%} may be zero. If there is more than one line with a specified name (but with different types), the one that appears outermost in the existential quantifications is pruned. If such a line name is mentioned twice in the list, the two outermost occurrences of lines with that name will be pruned, and so on. \FAILURE Fails if the argument theorem is not of the specified form or if any of the {\small\verb%lij%}'s are free in more than one of the conjuncts or if the equation for any {\small\verb%lij%} is recursive. The function also fails if any of the specified lines are not one of the existentially quantified lines. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #PRUNE_SOME_RIGHT_RULE [l1;l2] # (ASSUME # "!(in:num->bool) (out:num->bool). # DEV (in,out) = # ?(l1:num->bool) l2. # (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");; . |- !in out. DEV(in,out) = (!x. out x = ~in x) \end{verbatim} } \SEEALSO PRUNE_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV. \ENDDOC \DOC{UNFOLD\_CONV} \TYPE {\small\verb%UNFOLD_CONV : (thm list -> conv)%}\egroup \SYNOPSIS Expands sub-components of a hardware description using their definitions. \DESCRIBE {\small\verb%UNFOLD_CONV thl "t1 /\ ... /\ tn"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} B |- t1 /\ ... /\ tn = t1' /\ ... /\ tn' \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a {\small\verb%ti%}, it is unchanged. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNFOLD_CONV [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] # "INV (l1,l2) /\ INV (l2,l3) /\ (!(t:num). l1 t = l2 (t-1) \/ l3 (t-1))";; . |- INV(l1,l2) /\ INV(l2,l3) /\ (!t. l1 t = l2(t - 1) \/ l3(t - 1)) = (!t. l2 t = ~l1 t) /\ (!t. l3 t = ~l2 t) /\ (!t. l1 t = l2(t - 1) \/ l3(t - 1)) \end{verbatim} } \SEEALSO UNFOLD_RIGHT_RULE. \ENDDOC \DOC{UNFOLD\_RIGHT\_RULE} \TYPE {\small\verb%UNFOLD_RIGHT_RULE : (thm list -> thm -> thm)%}\egroup \SYNOPSIS Expands sub-components of a hardware description using their definitions. \DESCRIBE {\small\verb%UNFOLD_RIGHT_RULE thl%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?y1 ... yp. t1 /\ ... /\ tn -------------------------------------------------------- B u A |- !z1 ... zr. t = ?y1 ... yp. t1' /\ ... /\ tn' \end{verbatim} } \noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in {\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a {\small\verb%ti%}, it is unchanged. \FAILURE Fails if the second argument is not of the required form, though either or both of {\small\verb%r%} and {\small\verb%p%} may be zero. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNFOLD_RIGHT_RULE [ASSUME "!in out. INV(in,out) = !(t:num). out t = ~(in t)"] # (ASSUME "!(in:num->bool) out. BUF(in,out) = ?l. INV(in,l) /\ INV(l,out)");; .. |- !in out. BUF(in,out) = (?l. (!t. l t = ~in t) /\ (!t. out t = ~l t)) \end{verbatim} } \SEEALSO UNFOLD_CONV. \ENDDOC \DOC{UNWIND\_ALL\_BUT\_CONV} \TYPE {\small\verb%UNWIND_ALL_BUT_CONV : (string list -> conv)%}\egroup \SYNOPSIS Unwinds all lines of a device (except those in the argument list) as much as possible. \DESCRIBE {\small\verb%UNWIND_ALL_BUT_CONV l%} when applied to the following term: {\par\samepage\setseps\small \begin{verbatim} "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" \end{verbatim} } \noindent returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' \end{verbatim} } \noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations {\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are those conjuncts with line name not in {\small\verb%l%} (and which are equations). \FAILURE Never fails but may loop indefinitely. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_ALL_BUT_CONV [l2] # "(!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)";; |- (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ (!x. l2 x = 7) = (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\ (!x. l2 x = 7) \end{verbatim} } \SEEALSO UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE. \ENDDOC \DOC{UNWIND\_ALL\_BUT\_RIGHT\_RULE} \TYPE {\small\verb%UNWIND_ALL_BUT_RIGHT_RULE : (string list -> thm -> thm)%}\egroup \SYNOPSIS Unwinds all lines of a device (except those in the argument list) as much as possible. \DESCRIBE {\small\verb%UNWIND_ALL_BUT_RIGHT_RULE l%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = (?l1 ... lp. t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn) --------------------------------------------------------------------- A |- !z1 ... zr. t = (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn') \end{verbatim} } \noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations {\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are those conjuncts with line name not in {\small\verb%l%} (and which are equations). \FAILURE Fails if the argument theorem is not of the required form, though either or both of {\small\verb%p%} and {\small\verb%r%} may be zero. May loop indefinitely. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_ALL_BUT_RIGHT_RULE [l2] # (ASSUME # "!f. IMP(f) = # ?l2 l1. # (!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)");; . |- !f. IMP f = (?l2 l1. (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\ (!x. l2 x = 7)) \end{verbatim} } \SEEALSO UNWIND_AUTO_RIGHT_RULE, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ONCE_CONV, UNWIND_CONV. \ENDDOC \DOC{UNWIND\_AUTO\_CONV} \TYPE {\small\verb%UNWIND_AUTO_CONV : conv%}\egroup \SYNOPSIS Automatic unwinding of equations defining wire values in a standard device specification. \DESCRIBE {\small\verb%UNWIND_AUTO_CONV "?l1 ... lm. t1 /\ ... /\ tn"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn') \end{verbatim} } \noindent where {\small\verb%tj'%} is {\small\verb%tj%} rewritten with equations selected from the {\small\verb%ti%}'s. The function decides which equations to use for rewriting by performing a loop analysis on the graph representing the dependencies of the lines. By this means the term can be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations. \FAILURE Fails if there is more than one equation for any line variable. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_AUTO_CONV # "(!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)";; |- (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ (!x. l2 x = 7) = (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7) \end{verbatim} } \SEEALSO UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE. \ENDDOC \DOC{UNWIND\_AUTO\_RIGHT\_RULE} \TYPE {\small\verb%UNWIND_AUTO_RIGHT_RULE : (thm -> thm)%}\egroup \SYNOPSIS Automatic unwinding of equations defining wire values in a standard device specification. \DESCRIBE {\small\verb%UNWIND_AUTO_RIGHT_RULE%} behaves as follows: {\par\samepage\setseps\small \begin{verbatim} A |- !z1 ... zr. t = ?l1 ... lm. t1 /\ ... /\ tn ---------------------------------------------------- A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn' \end{verbatim} } \noindent where {\small\verb%tj'%} is {\small\verb%tj%} rewritten with equations selected from the {\small\verb%ti%}'s. The function decides which equations to use for rewriting by performing a loop analysis on the graph representing the dependencies of the lines. By this means the term can be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations. \FAILURE Fails if there is more than one equation for any line variable, or if the argument theorem is not of the required form, though either or both of {\small\verb%m%} and {\small\verb%r%} may be zero. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_AUTO_RIGHT_RULE # (ASSUME # "!f. IMP(f) = # ?l2 l1. # (!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)");; . |- !f. IMP f = (?l2 l1. (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)) \end{verbatim} } \SEEALSO UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_CONV, UNWIND_ONCE_CONV, UNWIND_CONV. \ENDDOC \DOC{UNWIND\_CONV} \TYPE {\small\verb%UNWIND_CONV : ((term -> bool) -> conv)%}\egroup \SYNOPSIS Unwinds device behaviour using selected line equations until no change. \DESCRIBE {\small\verb%UNWIND_CONV p "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn"%} returns a theorem of the form: {\par\samepage\setseps\small \begin{verbatim} |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' \end{verbatim} } \noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations {\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are the conjuncts for which the predicate {\small\verb%p%} is true. The {\small\verb%ti%} terms are the conjuncts for which {\small\verb%p%} is false. The rewriting is repeated until no changes take place. \FAILURE Never fails but may loop indefinitely. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_CONV (\tm. mem (line_name tm) [l1;l2]) # "(!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)";; |- (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ (!x. l2 x = 7) = (!x. l1 x = (l2 x) - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7) \end{verbatim} } \SEEALSO UNWIND_ONCE_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE. \ENDDOC \DOC{UNWIND\_ONCE\_CONV} \TYPE {\small\verb%UNWIND_ONCE_CONV : ((term -> bool) -> conv)%}\egroup \SYNOPSIS Basic conversion for parallel unwinding of equations defining wire values in a standard device specification. \DESCRIBE {\small\verb%UNWIND_ONCE_CONV p tm%} unwinds the conjunction {\small\verb%tm%} using the equations selected by the predicate {\small\verb%p%}. {\small\verb%tm%} should be a conjunction, equivalent under associative-commutative reordering to: {\par\samepage\setseps\small \begin{verbatim} t1 /\ t2 /\ ... /\ tn \end{verbatim} } \noindent {\small\verb%p%} is used to partition the terms {\small\verb%ti%} for {\small\verb%1 <= i <= n%} into two disjoint sets: {\par\samepage\setseps\small \begin{verbatim} REW = {ti | p ti} OBJ = {ti | ~p ti} \end{verbatim} } \noindent The terms {\small\verb%ti%} for which {\small\verb%p%} is true are then used as a set of rewrite rules (thus they should be equations) to do a single top-down parallel rewrite of the remaining terms. The rewritten terms take the place of the original terms in the input conjunction. For example, if {\small\verb%tm%} is: {\par\samepage\setseps\small \begin{verbatim} t1 /\ t2 /\ t3 /\ t4 \end{verbatim} } \noindent and {\small\verb%REW = {t1,t3}%} then the result is: {\par\samepage\setseps\small \begin{verbatim} |- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4' \end{verbatim} } \noindent where {\small\verb%ti'%} is {\small\verb%ti%} rewritten with the equations {\small\verb%REW%}. \FAILURE Never fails. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #UNWIND_ONCE_CONV (\tm. mem (line_name tm) [l1;l2]) # "(!(x:num). l1 x = (l2 x) - 1) /\ # (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ # (!x. l2 x = 7)";; |- (!x. l1 x = (l2 x) - 1) /\ (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ (!x. l2 x = 7) = (!x. l1 x = (l2 x) - 1) /\ (!x. f x = 7 + ((l2(x + 2)) - 1)) /\ (!x. l2 x = 7) \end{verbatim} } \SEEALSO UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE. \ENDDOC `