[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Andreas Schropp]

On 08/25/2011 11:26 PM, Florian Haftmann wrote:
> Hi Andreas,
>
>    
>> Let me ask something stupid:
>>    why exactly do you guys axiomatize 'a set?
>> Sure it's admissable and all, but why not do this definitionally
>> via the obvious typedef?
>>      
> the answer is rather technical: »typedef« in its current implementation
> needs set syntax / set type as prerequisite.

If 'a set is introduced definitionally (as it were)
this is fine for me, but if you axiomatize 'a set my setup in HOL->ZF
gets slightly more complicated. So now I am slightly against this. ;D

> Of course you could change
> »typedef« to be based on predicates, but there is some kind of unspoken
> agreement not to set one's hand on that ancient and time-honoured Gordon
> HOL primitive.
>    

Haha, very funny!
We are a long distance from the "ancient HOL primitive" already:
   local typedefs, sort constraints on type parameters,
overloaded constants in representation sets.
Perhaps you remember there was quite a suprise regarding those
"meta-safety" "proofs" that were once regarded as justification
of Isabelle/HOL's extensions to HOL. These days it seems my
translation is the only account of the generalized conservativity
result that still holds.

Of course I am probably the only one that will ever care about
these things, so whatever. ;D

> Rgds.,
> 	Florian
>
>