Re: [isabelle] Goal.prove automatically produces schematic type variables

On Tue, 12 Jan 2016, Bohua Zhan wrote:

This behavior is very strange to me. Example (in Isabelle2016-RC0):

This produces:
val th = "(1::?'a) + - inverse (2::?'a) = inverse (2::?'a)": thm

Interestingly this is no longer the case if there is a free variable

Output is:
val th = "(1::'a) + - inverse (2::'a) + (m::'a) = inverse (2::'a) + m": thm

This is a consequence of Hindley-Milner polymorphism wrt. to the local context. See also section 6.1 of the "implementation" manual, which contains further explanations and some abstract examples.

If anything is still unclear after reading that, we should continue the discussion here. These concepts are very important in Isabelle after 1999. Further discussion of difficulties also helps to improve the manual.


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