Email Gateway (Aug 18 2022 at 15:59): Email Gateway (Aug 18 2022 at 15:59):From: John Munroe <munddr@gmail.com>
Hi,
I'm wondering why the exception handling in the following doesn't
behave what I expected to. Does it not try to prove goal1, and if it
fails, it tries to prove goal2? goal2 should be provable, but I still
get a Proof failed exception.
let
val ctxt = @{context}
val goal1 = @{prop "EX x y. x > y"}
val goal2 = @{prop "EX (x::real) y. x > y"}
in
Goal.prove ctxt [] [] goal1
(fn _ => auto_tac (clasimpset_of ctxt))
handle THM _ =>
Goal.prove ctxt [] [] goal2
(fn _ => auto_tac (clasimpset_of ctxt))
end;
Thank you for the help.
John
Email Gateway (Aug 18 2022 at 15:59):From: Makarius <makarius@sketis.net>
The exception produced by Goal.prove is ERROR, not THM (which is a for
operations close to the inference kernel).
Normally you would organize proof attempts using tacticals such as ORELSE,
within a single goal state configuration.
Makarius
Email Gateway (Aug 18 2022 at 15:59):From: Alexander Krauss <krauss@in.tum.de>
John Munroe wrote:
[...]
The Goal module catches the internal THM exception itself and re-raises
it as a user error (exception ERROR). So the "handle THM _" does not
catch it...
Alex
Email Gateway (Aug 18 2022 at 15:59):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
John Munroe wrote:
John,
Without addressing your specific example closely, I can just point out
that to talk of a tactic application "failing" (as the documentation
does) is potentially ambiguous.
It can mean
(1) the resulting lazy list of new proof states is empty
(2) an ML exception is raised
Needless to say one sort of failure can (and no doubt there are examples
in the code) can be converted to the other
I'd guess that this issue would explain the unexpected behaviour
Jeremy
Email Gateway (Aug 18 2022 at 16:00):From: John Munroe <munddr@gmail.com>
Without addressing your specific example closely, I can just point out that
to talk of a tactic application "failing" (as the documentation does) is
potentially ambiguous.It can mean
(1) the resulting lazy list of new proof states is empty
(2) an ML exception is raisedNeedless to say one sort of failure can (and no doubt there are examples in
the code) can be converted to the otherI'd guess that this issue would explain the unexpected behaviour
Handling ERROR instead solves my problem. Thanks!
John
Jeremy
Last updated: Apr 24 2024 at 12:33 UTC