Re: [isabelle] "Sorry" and "done" command diverging with function definition



Dear Dominic,

Your function definition works for me in Isabelle2016-1 if I use the following locale:

locale model = fixes successors :: "'w â 'w set"

When done or sorry are processed, the function package internally carries out the definition and derives all the theorems. This may take a while, but should terminate.

Then, as you are using the context specification (in model), Isabelle will restore the previous context. So if you are inside some other large locale when you do this function command, then after done or sorry, the other locale context will be restored, which can take quite some time when large contexts are involved. If this is the case, try to close the context before the definition and see if things improve.

If this does not help, can you post a minimal example that includes all relevant definitions of the locale model?

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.