[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
makarius at sketis.net
Fri Aug 26 13:08:58 CEST 2011
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?
More information about the isabelle-dev