[isabelle-dev] typedef

[Andreas Schropp]

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?
Interesting!

> - Brian
>