Re: [isabelle] Proving with Goal.prove



On Thu, 30 Sep 2010, John Munroe wrote:

I'm trying another example with Goal.prove, but it can't seem to
discharge the proof goal. I must have done something wrong:

ML {*

fun foo ctxt st =
 let
   val {prop,...} = Thm.rep_thm st
   val tac = auto_tac (clasimpset_of ctxt)
   val t = Goal.prove ctxt [] [] prop
     (fn _ => tac)
 in
   tac st
 end;

*}

lemma lem1: "EX x y. x = y"
apply (tactic {* foo @{context} *})

Does the value prop not contain the goal of lem1? If not, how can the goal for the current goal state be retrieved?

First of all, the function foo above looks formally like a tactic, so it has to be called foo_tac, and probably parameterized over i: int (subgoal number).

Inspecting the full prop of a goal "st" hardly ever makes sense.

The most basic way to get hold of a certain subgoal is via the SUBGOAL combinator.

SUBPROOF or FOCUS and variants are far more advanced technologies that are convenient in many cases, but definitely overkill to peek at a specified subgoal.

Forget everything you have heard about Goal.init, Goal.conclude unprotect etc. on this thread. That's a completely different story about implementing a structured goal concept, not just using it.


	Makarius





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