[isabelle-dev] typedef

[Brian Huffman]

On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp <schropp at in.tum.de> wrote:
> Formerly the non-emptiness proof was global, now its local!
>
> locale bla =
>  assume "False"
>  typedef empty = {}
>
> Now I have to put up with the fact the semantic interpretation of empty is
> the empty set. Formerly only non-empty sets were semantic interpretations of
> type constructors. The way around this is to localize derivations related to
> type constructor well-formedness, using False to forge all those crazy
> things.

Andreas,

How would your HOL->ZF translation handle the following typedef?

class infinite = assumes infinite_UNIV: "~ finite UNIV"

typedef 'a infset = "{A::('a::infinite) set. ~ finite A}"
  using infinite_UNIV [where 'a='a] by fast

This example does not rely on locales at all. It doesn't rely on any
overloaded constants either, not even indirectly.

However, the nonemptiness proof does rely on type class assumptions:
Indeed, "{A. ~ finite A}" is actually empty for any finite type 'a.

So it seems to me that this problem you describe where "the semantic
interpretation of [a type] is the empty set" predates the localization
of typedef.

- Brian