*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Induction rule for partial_function (tailrec)*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 18 Mar 2013 10:04:29 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51463E82.5080108@in.tum.de>*References*: <51402CC1.6030903@inf.ethz.ch> <51463E82.5080108@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130308 Thunderbird/17.0.4

Hi Alex,

Andreas On 17/03/13 23:06, Alexander Krauss wrote:

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?partial_function currently expects induction rules whose conclusion is of the form "... ==> P x y" where ... intuitively means "f x terminates and evaluates to y". In the option monad, this is simply "f x = Some y ==> P x y", but in the degenerate tailrec monad you would get something like "f x = y ==> y ~= undefined ==> P x y". 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 eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (λf. U (F (C f))))" assumes inverse2: "⋀f. U (C f) = f" assumes step: "⋀f x y. (⋀x y. U f x = y ⟹ y ≠ undefined ⟹ P x y) ⟹ U (F f) x = y ⟹ y ≠ undefined ⟹ P x y" 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. I cannot say on the spot whether partial_function could be modified to accept rules like yours. The problem is the curry/uncurry translation, which must do some explicit instantiations and assumes a certain syntactic form. Let me know when you make progress (or run into more problems). Alex

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

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

**Re: [isabelle] Induction rule for partial_function (tailrec)***From:*Alexander Krauss

- Previous by Date: [isabelle] PxTP 2013: Second Call for Papers
- Next by Date: Re: [isabelle] help
- Previous by Thread: Re: [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