[isabelle-dev] typedef

[Brian Huffman]

On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp <schropp at in.tum.de> wrote:
> 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.

As I understand it, the typedef in the above example will cause a
conditional axiom to be generated, something like this:

axiom type_definition_empty:
  "False ==> type_definition Rep_empty Abs_empty {}"

As far as I can tell, this axiom doesn't force you to use the empty
set to denote type "empty" in your set-theoretic model. In fact, you
can use any set you want to denote type "empty", because the axiom
type_definition_empty doesn't assert anything about it at all!

- Brian