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

[Andreas Schropp]

On 08/26/2011 01:08 PM, Makarius wrote:
> On Thu, 25 Aug 2011, Andreas Schropp wrote:
>> 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.

No offense: the last time we discussed these things
you were introducing local typedefs directly instead of expressing them
via global typedefs, which I told you is not exactly hard.
It looks like you are more concerned with an easy implementation,
leaving any matters of conservativity to me. I am not saying this is
bad, but every time my transformation gets harder, I am not
exactly feeling that "Makarius always cares about conservativity". ;D

>
> Maybe you want to start a realistic formalization yourself?
>

This conservativity result that I am animating is a global theory
transformation featuring replacement of certain typedefs by
their representing sets, regarding them as soft types.
If someone is interested I would indeed write this up, but
given the complexity (I guess 3-4 pages of rule systems, without text)
I don't think we can hope for a realistic formalization.

BTW: Steven should get credit for seriously trying
conservativity of overloading at least. This helped to expose
the misconception, though he did not notice the problem.

Also my write-up of the Isabelle-Kernel is 8 pages (of rule systems, 
without text!)
and still incomplete, so I don't think we will ever manage to prove 
something
important about Isabelle. I am even being generous here, excluding e.g. 
unification
which is part of the trusted code (for speed I guess) but generates 
proof terms.
In my eyes, the only reason we can claim to satisfy the deBruijn 
criterion is
that proof-checking is much easier in ZF. From an LCF POV we are not really
in game, because unification et al are trusted code.

>
>     Makarius