*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Common monadic programming idioms and termination*From*: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Tue, 27 Oct 2015 12:40:39 +0000*Cc*: Manuel Eberl <eberlm at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <562F6CFD.7040804@inf.ethz.ch>*References*: <CAFAp4FnbBhNQAtSZekc+DQ3MBiDu2a6CqtEu6+CM7xQ4EpDadA@mail.gmail.com> <562A56DC.5070601@in.tum.de> <CAFAp4Fn2XAE9N-ED88fLt82hh_hf2aFq0TvXO3obyAuqyX-Tfw@mail.gmail.com> <562F6CFD.7040804@inf.ethz.ch>*Reply-to*: Dominic Mulligan <dominic.p.mulligan at googlemail.com>

Dear Andreas, Thanks! That was obvious in hindsight. I now have termination conditions that look much more amenable. Many thanks, Dominic On 27 October 2015 at 12:24, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > Dear Dominic. > > The congruence rules must be declared as [fundef_cong] before the function > definition takes place. In your example, they are declared between the > definition and the termination proof. > > The theorems about set_error help to automate the termination proof. You can > discover such lemmas when you try to do the proof manually. > > 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 >>>> >>> >

**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

**Re: [isabelle] Common monadic programming idioms and termination***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Common monadic programming idioms and termination
- Next by Date: Re: [isabelle] inductive_set and ordinal induction
- Previous by Thread: Re: [isabelle] Common monadic programming idioms and termination
- Next by Thread: Re: [isabelle] Locales: Interpretation changes behaviour of locale expression
- 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