Re: [isabelle] primcorec does not terminate

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.)

Iâll let you know if and when I improved the tactic.


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