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

[Makarius]

On Thu, 25 Aug 2011, Andreas Schropp wrote:

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

There are indeed many formal jokes concerning "typedef", which is in fact 
an axiomatization scheme that happens to with a certain semantic 
interpretation of HOL that was designed specifically to make it work.

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

I have always cared about that, starting about 1994 in my first 
investigations what HOL actually is -- there are still various 
misunderstandings in printed texts.  And of course there is still no fully 
formal theory of all the aspects that have been emphasized in the variety 
of HOL implementations.

Maybe you want to start a realistic formalization yourself?


 	Makarius