*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Induction rule for partial_function (tailrec)*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sun, 17 Mar 2013 23:06:58 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51402CC1.6030903@inf.ethz.ch>*References*: <51402CC1.6030903@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi Andreas, On 03/13/2013 08:37 AM, Andreas Lochbihler wrote:

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?

I just tried this and got the following rule accepted by partial_function. lemma fixp_induct_tailrec_undefined: fixes F :: "'c ⇒ 'c" and U :: "'c ⇒ 'b ⇒ 'a" and C :: "('b ⇒ 'a) ⇒ 'c" and P :: "'b ⇒ 'a ⇒ bool" and x :: "'b" assumes mono: "⋀x. mono_tailrec (λf. U (F (C f)) x)"

assumes inverse2: "⋀f. U (C f) = f"

assumes result: "U f x = y" assumes defined: "y ≠ undefined" shows "P x y" sorry I believe this rule should be provable and sufficient for what you want.

Let me know when you make progress (or run into more problems). Alex

**Follow-Ups**:**Re: [isabelle] Induction rule for partial_function (tailrec)***From:*Andreas Lochbihler

**References**:**[isabelle] Induction rule for partial_function (tailrec)***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] help
- Next by Date: [isabelle] PxTP 2013: Second Call for Papers
- Previous by Thread: [isabelle] Induction rule for partial_function (tailrec)
- Next by Thread: Re: [isabelle] Induction rule for partial_function (tailrec)
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list