[isabelle-dev] typedef

[Andreas Schropp]

On 08/30/2011 08:12 PM, Brian Huffman wrote:
> 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?
>    

Its been a while, I don't remember the exact details,
but type classes are a global concept, so this is quite
different from the complications via local typedefs.

Think: type constructor well-formedness arguments
via type classes can stay global.
Non-Emptiness-Proofs are still global in this case
because instances are global.

If I am not mistaken I don't have to do anything
to treat typedefs with type class constraints:
   due to our efforts back then, type class reasoning
is eliminated directly in the kernel.

> 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.
>    

The question is not so much about typedef semantics IMO (but it can be 
resolved
this way), but more about the status of globality/localness of 
non-emptiness proofs
demanded by the typedef principle.
Of course the empty set could always be written down there, but whether this
"justified" globally or locally is more interesting ...

> - Brian
>