Re: [isabelle] Proving with Goal.prove
On Tue, 5 Oct 2010, Michael Chan wrote:
Since we're on Goal.prove, I'd like to ask a quick question: can it be
used to prove schematic goals? It seems that if the goal is, say, "EX
(f::?'a=>?'b)...", the type of f in concl of the focus becomes "'a=>'b".
So if Goal.prove takes only concl of the focus, it'd be non-schematic.
So it seems like Goal.prove handles schematic goals as non-schematic
ones. Am I missing something here?
Goal.prove itself does not interfere with the schematic status of the
input, it merely checks that the final result is an instance of the
Since you speak about "focus" above, I reckon that you are also using the
very convenient Subgoal.FOCUS suite of combinators. This relatively
recent technology is able to address almost all issues and surprises about
goal states that have accumulated over the years, but it limits the part
of the subgoal you are focusing to a fixed view of variables. So indeed,
it temporarily imports ?'a=>?'b and presents it as 'a=>'b in the auxiliary
Apart from that, goals with schematic *type* variables are always prone to
cause problems elsewhere: various proof tools choke on that. It is
technically relatively hard to "synthesize" Pure/HOL types in Isabelle,
harder than synthesizing term instances.
This archive was generated by a fusion of
Pipermail (Mailman edition) and