[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
schropp at in.tum.de
Fri Aug 26 16:28:17 CEST 2011
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,
and still incomplete, so I don't think we will ever manage to prove
important about Isabelle. I am even being generous here, excluding e.g.
which is part of the trusted code (for speed I guess) but generates
In my eyes, the only reason we can claim to satisfy the deBruijn
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.
More information about the isabelle-dev