[isabelle] function (tailrec,sequential) fails


I’m trying to work with two mutual recursive, partially defined and
not-always terminating functions (It evaluates a program, the code is at
if anyone is curious). The functions happen to be tail-recursive, so I’d
like to use the function package’s support for that.

Unfortunately, it fails when using both tailrec and sequential. But
already the following simple example fails, so don’t bother looking at
my code :-):

theory Tmp imports Main

function (sequential,tailrec) f where "f True = 0"
  apply pat_completeness
  apply auto

gives me:

*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** f_sumC False = undefined
*** At command "done".

Is that easily fixable, or is there a work-around?

Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part

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