Yes, I thought that was one of the more likely possible causes. Let me know if you can devise a better congruence rule that still gets the termination argument to go through.
On 23 February 2016 at 15:40, Konrad Slind <[email protected]> wrote: > Preliminary comment: the congruence rule looks a bit suspect. I doubt the > termination condition extractor is setup to deal with pairs in the > concluding equality of a congruence rule. > > Konrad. > > > On Mon, Feb 22, 2016 at 9:36 PM, Ramana Kumar <[email protected]> > wrote: >> >> 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 >> > >> > > > ------------------------------------------------------------------------------ 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
