[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses
andreas.lochbihler at kit.edu
Mon Jul 9 08:27:47 CEST 2012
> On the sister thread
> Henri mentions finite_UNIV.
Henri refers to finite_UNIV in HOL/Finite_Set, you seem to talk about
finite_UNIV from HOL/Library/Cardinality.
> Trying to reproduce the observed effects with Isabelle2012 vs.
> Isabelle/3155cee13c49 from today reveals a difference wrt. Phantom('a).
> The latter was introduced in Isabelle/f0ecc1550998 with an almost vacous
> log entry, and no coverage in NEWS nor CONTRIBUTORS.
I planned to cover the whole business of phantom type and the type classes
finite_UNIV and card_UNIV once I have finished moving FinFuns from the AFP to
> What is its purpose? Where is it documented?
The first hit in Google when you search for "phantom type" tells you what a
phantom type is.
"A phantom type is a type whose type parameter do not all appear on the
right-hand side of it's defintion."
As can be seen from the usage of Phantom('a) in Cardinality (e97369f20c30 and
3d9c1ddb9f47) and the commit message in e97369f20c30, phantom types can be used
to make a type parameter appear in a constant's type. Typically in Isabelle,
such constants take an additional argument 'a itself for that purpose, but this
generates less efficient code than boxing values in phantom types of which the
ML/Haskell compiler gets rid again.
Karlsruher Institut für Technologie
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
More information about the isabelle-dev