Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]
- To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Subject: Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]
- From: Makarius <makarius at sketis.net>
- Date: Tue, 6 Oct 2015 19:53:06 +0200 (CEST)
- Cc: Ondřej Kunčar <kuncar at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <56017F45.firstname.lastname@example.org>
- References: <A3211BFC-696D-4616-AAD4-1E916B859A78@lri.fr> <560164FF.email@example.com> <56016EB9.firstname.lastname@example.org> <56017F45.email@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Tue, 22 Sep 2015, Florian Haftmann wrote:
* From a technical/implementation point of view: the only conceptual
change of the code is that you have to separate name spaces of types and
constants in defs.ML. But because the implementation of defs.ML is
already visionary, this is the only change that has to be done. You can
treat type instances of type constructors and constants in an uniform
way, i.e., there is not any change in the algorithm's itself. You just
need a more complicated type for names of the nodes in the graph.
thanks for explaining this so thoroughly.
So, the technical complication in the first instance is a name space issue.
To maintain the ÂvisionaryÂ property of defs.ML, it could also be
generalized to administrate dependencies of Ânamed symbolsÂ in general,
e.g. by using some kind of name space tagging etc. instead of hard-coded
constructors. These could serve potential specification object logics
dealing with different kinds of entities than type constructors and
constants also, but this is highly speculative.
This "speculative" treatment of specification items that may be either
consts or types is already part of the Isabelle code base for the coming
release. I even added a 'print_definitions' command that prints a keyword
"type" with PIDE markup, to make it easier to spot these extremely rare
occurrences of overloaded type constructors. Moreover, the syntax
"typedef (overloaded)" makes clear to the user where traditional HOL
interpretation according to A. Pitts is transcended.
Formally all of this is just a certain abstract service of Isabelle/Pure,
which is used inside Pure itself for constant definitions. Object-logics
like Isabelle/HOL then add their own axiomatization schemes with extra
dependencies, and then call them "definitional". The explanation how this
can be justified is in the ITP paper, despite some gaps compared to the
Thus we are back to the standard invariant of Isabelle development over 3
decades, that the concepts behind the implementation and the concepts
behind published papers are slightly divergent.
This archive was generated by a fusion of
Pipermail (Mailman edition) and