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



Hi Andreas,

Thanks for the reply.

After playing around some more with my code I noticed that a
copy-paste error meant that an induction principle was marked as a
simp rule, by mistake.  After removing the simp attribute from that
theorem the "done" command is now processed immediately.

Thanks,
Dominic

On 5 July 2017 at 16:18, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
> 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.