*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Common monadic programming idioms and termination*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 23 Oct 2015 17:48:44 +0200*In-reply-to*: <CAFAp4FnbBhNQAtSZekc+DQ3MBiDu2a6CqtEu6+CM7xQ4EpDadA@mail.gmail.com>*References*: <CAFAp4FnbBhNQAtSZekc+DQ3MBiDu2a6CqtEu6+CM7xQ4EpDadA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

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

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

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

- Previous by Date: [isabelle] Common monadic programming idioms and termination
- Next by Date: Re: [isabelle] Common monadic programming idioms and termination
- Previous by Thread: [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