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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and