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
