Re: [isabelle] Proving with Goal.prove
On Thu, 30 Sep 2010, Michael Chan wrote:
Does the value prop not contain the goal of lem1? If not, how can the
goal for the current goal state be retrieved?
I'm not sure myself, but it seems like the prop here is:
EX (x::'a) y::'a. y < x ==> (EX (x::'a) y::'a. y < x)
so that doesn't look like the goal in lem1. Hopefully someone more familiar
with the ML level can answer your question.
There are some explanations in the Isabelle/Isar implementation manual,
section 3.1 and 3.2. The invisible prop marker is written as # in 3.1.
Administrative operations like Goal.conclude should be only used on your
own Goal.init states, not arbitrary goal states seen by tactics. Regular
tactics cannot count on any particular format of the main conclusion --
there might be 0 or more main goal markers.
All regular tactical reasoning takes place on the left side, operating on
the list of subgoals. The main conclusion is a no-go area for tactics.
This archive was generated by a fusion of
Pipermail (Mailman edition) and