[isabelle] tail recursive definition

Hi all,

the following definition (a simplified version of what i need) of a
tail recursive function produces two subgoals, that can be proved, for
instance, by "apply auto". Nevertheless, the proof cannot be completed
(as can be seen by trying "by auto"). A goal seems to remain

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).

Thanks in advance for any help,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

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