*To*: Dominic Mulligan <dominic.p.mulligan at googlemail.com>, Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Common monadic programming idioms and termination*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 27 Oct 2015 13:24:29 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAFAp4Fn2XAE9N-ED88fLt82hh_hf2aFq0TvXO3obyAuqyX-Tfw@mail.gmail.com>*References*: <CAFAp4FnbBhNQAtSZekc+DQ3MBiDu2a6CqtEu6+CM7xQ4EpDadA@mail.gmail.com> <562A56DC.5070601@in.tum.de> <CAFAp4Fn2XAE9N-ED88fLt82hh_hf2aFq0TvXO3obyAuqyX-Tfw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Dominic.

Best, Andreas On 27/10/15 12:41, Dominic Mulligan via Cl-isabelle-users wrote:

Hi, Actually, after returning to this subject after unfortunately getting distracted doing something else, I'm afraid that the lemmas that Manuel suggested do not seem to work in transforming the termination conditions generated by Isabelle into something that looks provable. I've attached the same stripped down Isabelle theory file as last time with the suggested lemmas added, marked as fundef_cong, and the issue remains at the point marked XXX. This persists after trying to use some alternative congruence rules, also. Part of the issue is that I have no idea what the need for the rather mysterious set_error_fail and set_error_return lemmas is in Manuel's previous e-mail, or how I would even go about finding the need for those lemmas. From what I understand the "set_error" constant is automatically generated by the new datatype machinery, but how this interacts with termination is not clearly documented in either of the Datatype or Function PDFs bundled with Isabelle. Lastly, is there any way to get Isabelle to spit out which congruence rules it is trying to apply when constructing these proof obligations, or which congruence rules it at least has knowledge of other than grepping the Isabelle library source? Many thanks for any help, Dominic On 23 October 2015 at 16:48, Manuel Eberl <eberlm at in.tum.de> wrote:The problem is that you have a recursive call in an argument of the âbindâ function, and the function package has no idea what kind of parameter this call will get. For instance, the âbindâ function could simply double the list it gets as the first input and call the function it gets as second input on it â then your function would never terminate. So, what you need to do is you need to tell the function package a little bit about what kinds of inputs the âbindâ function will give to its function parameter. You can do that with a congruence rule: lemma error_bind_cong [fundef_cong]: "(map_error f x = map_error f' x') â error_bind x f = error_bind x' f'" by (cases x; cases x') simp_all This essentially implies that bind only calls the function you give it with a value contained in the error object you give it. Once you have proven this lemma and declared it as [fundef_cong], your proof obligation in the termination proof will look a lot saner. Add two more simp lemmasâ lemma set_error_fail [simp]: "set_error (error_fail m) = {}" by (simp add: error_fail_def) lemma set_error_return [simp]: "set_error (error_return s) = {s}" by (simp add: error_return_def) âand everything works automagically. Cheers, Manuel the function package does not know anything about your âbindâ function. On 23/10/15 17:24, Dominic Mulligan via Cl-isabelle-users wrote:Hi all, I have a problem with a development that I am working on (in Isabelle 2015). A slimmed down and simplified version of the problematic code has been attached in a dedicated theory file to this e-mail with the problem annotated with an (* XXX *) comment. The problem arises when trying to prove termination of recursive functions that follow a fairly natural monadic programming style, namely recursively calling your function on a decreasing argument that is produced by earlier monadic code, hence lambda-bound following a bind. Here, the termination machinery seems to generate proof obligations that are not solveable, demanding one prove that an arbitrary list is shorter (according to the measure) than a non-empty list, like so: âxs xa. xs â [] â length xa < length xs Interestingly, HOL4's termination machinery also seems to behave similarly, and with the help of Anthony Fox the issue has been reported to Konrad Slind. Does anybody have any suggestions on how to proceed other than completely rewriting all of my monadic code? The problematic code is automatically generated, and comes from a rather large model, so I'd rather not have to rewrite everything. Many thanks for any help proffered, Dominic

**Follow-Ups**:**Re: [isabelle] Common monadic programming idioms and termination***From:*Dominic Mulligan via Cl-isabelle-users

**References**:**[isabelle] Common monadic programming idioms and termination***From:*Dominic Mulligan via Cl-isabelle-users

**Re: [isabelle] Common monadic programming idioms and termination***From:*Manuel Eberl

**Re: [isabelle] Common monadic programming idioms and termination***From:*Dominic Mulligan via Cl-isabelle-users

- Previous by Date: Re: [isabelle] inductive_set and ordinal induction
- Next by Date: Re: [isabelle] Common monadic programming idioms and termination
- Previous by Thread: Re: [isabelle] Common monadic programming idioms and termination
- Next by Thread: Re: [isabelle] Common monadic programming idioms and termination
- Cl-isabelle-users October 2015 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