[isabelle-dev] typedef

Andreas Schropp schropp at in.tum.de
Fri Aug 26 23:02:19 CEST 2011

On 08/26/2011 11:08 PM, Brian Huffman wrote:
> 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!

So you suggest using e.g.
   if EX x. x : A then A
   else {0}
instead of A as the semantic interpretation?

> - Brian

More information about the isabelle-dev mailing list