*To*: Dominic Mulligan <dominic.p.mulligan at googlemail.com>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] "Sorry" and "done" command diverging with function definition*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 5 Jul 2017 17:18:20 +0200*In-reply-to*: <CAFAp4F=Qozkha7BBq6unujx+wxhqj+2vHH5uFNJm=OR1x6+NtA@mail.gmail.com>*References*: <CAFAp4F=Qozkha7BBq6unujx+wxhqj+2vHH5uFNJm=OR1x6+NtA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

Dear Dominic, Your function definition works for me in Isabelle2016-1 if I use the following locale: locale model = fixes successors :: "'w â 'w set"

Best, Andreas On 05/07/17 17:02, Dominic Mulligan via Cl-isabelle-users wrote:

Hi, I am trying to define a recursive function over sets that will require a conditional termination proof, like so: ... function (in model) (domintros) rla_exists_until :: "'w set â 'w set â 'w set" where "rla_exists_until S T = (let U = {s â S - T. successors s â T â {}} in if U â {} then rla_exists_until S (T â {SOME x. x â U}) else T)" ... As usual, this opens a number of subgoals which appear to be solvable using pat_completeness followed by blast, i.e. applying those tactics produces the message "No more subgoals". However, when typing "done" after this set of tactic invocations, the "done" command appears to diverge. Further, replacing the pat_completeness and blast tactics with "sorry" also appears to diverge. I have tried to rewrite the function above in various different forms, inlining the let, and so on, to no avail. Is there a way to debug what is going on, or any suggestion as to what the problem may be? I have already written and proved conditionally terminating a function very similar to the one above with no problem, so there is clearly some sensitivity to the precise shape of the function definition... Thanks, Dominic

**Follow-Ups**:**Re: [isabelle] "Sorry" and "done" command diverging with function definition***From:*Dominic Mulligan via Cl-isabelle-users

**References**:**[isabelle] "Sorry" and "done" command diverging with function definition***From:*Dominic Mulligan via Cl-isabelle-users

- Previous by Date: [isabelle] "Sorry" and "done" command diverging with function definition
- Next by Date: Re: [isabelle] "Sorry" and "done" command diverging with function definition
- Previous by Thread: [isabelle] "Sorry" and "done" command diverging with function definition
- Next by Thread: Re: [isabelle] "Sorry" and "done" command diverging with function definition
- Cl-isabelle-users July 2017 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