Re: [isabelle] primcorec does not terminate
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:
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 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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and