[isabelle] function (tailrec,sequential) fails



Hi,

I’m trying to work with two mutual recursive, partially defined and
not-always terminating functions (It evaluates a program, the code is at
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/Eval.thy;hb=HEAD
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
begin

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

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?

Thanks,
Joachim
-- 
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.