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.


	Makarius





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