Hi Konrad, Thanks for looking into this. I have made a cut-down version of the problem in the attached script file. It should build in a recent version of HOL without any prerequisites. The problem is that the theorem returned by the final call to Define (for my_quote_exp_aux) still contains RESTRICT. (In my real example, I also needed to provide a termination tactic for this call, but in the cut down version termination is proved automatically, but luckily for me the problem still showed up.)
Let me know if you figure it out. Cheers, Ramana On 23 February 2016 at 04:39, Konrad Slind <[email protected]> wrote: > Looks horrible. There shouldn't be remaining occurrences of RESTRICT. > Termination-condition extraction should remove them all. > > Can you send me a cut-down version of the problematic function? > > Konrad. > > > On Sun, Feb 21, 2016 at 5:34 AM, Ramana Kumar <[email protected]> > wrote: >> >> I have managed to make a definition where the theorem returned to me >> by tDefine still contains occurrences of ``RESTRICT new_func (@R. WF R >> /\ ...)``. >> >> Is this to be expected from tricky input equations, or is it a sign of >> a problem in the recursive function package? >> >> Would it be easy to post-process the resulting definition theorem to >> remove the RESTRICT? >> >> As is usual in such situations, there is a fair amount of context >> required to explore what's going on interactively, but if anyone is >> interested the relevant definition is made here: >> >> https://github.com/machine-intelligence/Botworld.HOL/blob/37747faa1eda333086612101023803967a8645e5/botworld_quoteScript.sml#L135 >> >> >> ------------------------------------------------------------------------------ >> Site24x7 APM Insight: Get Deep Visibility into Application Performance >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month >> Monitor end-to-end web transactions and take corrective actions now >> Troubleshoot faster and improve end-user experience. Signup Now! >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info > >
RESTRICT_remainsScript.sml
Description: application/smil
------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
