[isabelle] Induction rule for partial_function (tailrec)



Every now and then, I want to prove that a function that I have defined with partial_function (tailrec) is undefined when the recursion does not terminate. Unfortunately, partial_function (tailrec) does not generate an induction theorem for the functions. So I set out to prove my own generic induction rule (fixp_induct_tailrec_undefined in the attachment) similar to fixp_induct_option in Partial_Function.thy. If I manually instantiate it with the ..._def theorem of the partial function ..., everything works fine. However, when I register it as the induction theorem to be used for tailrec (like it is done for fixp_induct_option and option in Partial_Function.thy), I only get exceptions when using partial_function.

What's wrong with my induction theorem? How can I change it such that it works with partial_function?

Andreas

Attachment: Scratch.thy
Description: application/example



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