Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]



On Tue, 22 Sep 2015, Florian Haftmann wrote:

Hi OndÅej,

[...]

* 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 actual code.

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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.