Re: [isabelle] Schematic goal



Michael Chan schrieb:

I have a quick question about schematic goal statements in 2009-2. Are they allowed? I believe 2009-1 allows them, e.g., "EX (x::?'a)...". Now in 2009-2, I keep getting an error saying "Illegal schematic goal statement".


On Thu, 5 Aug 2010, Andreas Lochbihler wrote:

Also note that you only need schematic type variables if you want to instantiate the type only during the proof and are too lazy to write this type down in full in the goal statement. If you want your lemma to be polymorphic, just omit the question mark and use an ordinary type variable. Existential type quantification is not possible in HOL anyway.

"EX (x::'a). ..."

This means the explicit 'schematic_lemma' commands not only help the system in performance tuning, but also users to prevent accidental use of schematic variables. In particular, schematic types in goal statements make various proof tools do unexpected things. (Often they stem from copying the printed version of existing facts.)

The normal way is to give fixed statements, and let the system produce a general result in the very end.


	Makarius





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