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



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.