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 initial claim.

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 context.

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.


	Makarius






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