Re: [isabelle] function (tailrec,sequential) fails



Dear Joachim,

thanks. I applied the fix, and it worked so far. But when I tried to
reduce the number of equations generated by sequential by simplifying
the pattern matches, I get an error message that does not occur without
tailrec.

[...]

The error message I get is:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*** Proof failed.
*** accp evalF_evalC_rel x
***  1. ⋀evalF_evalC_sum ct cf as ve b y cta cfa asa vea ba a list int aa lista
***        ab listb x.
***        ⟦⋀a list inta aaa lista aba listb x.
***            ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta;
***             list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧
***            ⟹ evalF_evalC_graph (Inl (aaa, [], vea, Suc ba))
***                (evalF_evalC_sum (Inl (aaa, [], vea, Suc ba)));
[...]

Tailrec performs some very ugly proofs internally, and unfortunately it relies on the simplifier to do certain case splits automatically, which does not seem to work in general in the presence of "case". There is no fix at the moment, and I won't try to find one, since I am working on a new package for certain classes of partial functions, which will subsume and replace tailrec in its current form.

For the moment, if all else fails, you must fall back to the good old while combinator (HOL/Library/While_Combinator".

Alex





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