Re: [isabelle] primcorec does not terminate



Hi Jasmin,

Thanks for the hint of fully specifying the function. This is certainly better than taking the quick_and_dirty road.

On 20/04/15 14:51, Jasmin Blanchette wrote:
Hi Andreas,

In the attached theory, the primcorec definition of a function does not terminate (tested with both Isabelle2014 and Isabelle2015-RC0). Is is because my definition is erroneous or a shortcoming of the primcorec implementation?

It is, indeed, a shortcoming of the selector-theorem generating tactic â I think it might eventually have terminated, given enough resources.

The tactic doesnât look easy to fix. Iâll need to dig into it more deeply, which is unlikely to happen in the very near future. However, an easy workaround is to add an explicit case

    | LCons (Inr x) xsâ => Nil_call)â

to deal with the missing unspecified case. (Otherwise, âprimcorecâ expands the resulting implicit âundefinedâ into a trivial âcaseâ, which complicates the destructor view â cf. our ITP 2014 paper.)
When I use primcorec, I usually either define it using the destructor view (and then manually derive a suitable code view -- the automatically generated one is usually not idiomatic) or specify the code view with cases (from which I derive pattern-matching equations using simps_of_case) and then manually derive the destructor rules, as the generated theorems use cases rather than selectors and discriminators. So I am not so worried about these generated theorems becoming more complex (although undefined indeed does add some problems, but I am not planning to call my function on arguments that result in undefined.

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.