Re: [isabelle] Handling failed proof



On Wed, 29 Sep 2010, John Munroe wrote:

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;

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





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