Re: [isabelle] Handling failed proof



John Munroe wrote:
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

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







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