Email Gateway (Aug 22 2022 at 15:44): Email Gateway (Aug 22 2022 at 15:44):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 15:45):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 15:46):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Last updated: Apr 26 2024 at 12:28 UTC