Re: [isabelle] tail recursive definition



Hi Jesus,

function (tailrec) remove :: "'a set => (nat => 'a) => 'a set" where "remove A f = (if A = {} then A else remove (A - {f 1}) (%k.
if k < (1::nat) then f k else f (Suc k)))"

When such a thing happens with a definitional package (e.g.,
"datatype", "inductive", "function"), it usually indicates a bug in
the package. The "tailrec" option is seldom used or tested; a bug
there wouldn't be so surprising.

That's a very polite way of expressing it :-). "function (tailrec)" is very buggy and currently the top thing on my kill list. It is a funny coincidence that just today I eliminated the remaining uses from the AFP, (cf. http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/cfeb14dc4509 , in particular, SatSolverCode.thy).

My recommendation is to move to Isabelle2011 and use the new "partial_function (tailrec)" command. There is an example in HOL/ex/Fundefs.thy, and you should be able to see from the changeset above how to port things. Note that currently no pattern matching is supported, but you can easily work around this by using "case" on the right-hand side.

Hope this helps.

Alex





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