[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

Andreas Lochbihler andreas.lochbihler at kit.edu
Mon Jul 9 08:27:47 CEST 2012

> On the sister thread
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00028.html
> 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
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

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 mailing list