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)))"
> 
> Are there any problems with the definition? Which additional facts
> have to be proved? (I am using Isabelle 2009-2).

If you try "apply auto", you should see the reassuring message "No subgoals!". Things go sour only when you enter "done", and then the error says "Proof failed". This indicates than an internal proof obligation couldn't be discharged by "function".

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.

Alex will hopefully be able to help you here...

Cheers,

Jasmin






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