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



On 09/22/2015 04:26 PM, Florian Haftmann wrote:
[This thread has become too voluminous to be followed in detail by a
casual bystander, so I try here with Âone issue â one mailÂ.]

I am personally very sympathetic towards a refined, stricter, more
accurate, better understood consistency check. The separation of
Isabelle/Pure and Isabelle/HOL however is an integral part of the system
design and needs to be respected and reflected in the design of components.

In the past, we always managed to leave typedef itself unchanged,
resisting obvious temptations like
* replace sets by predicates (which is conceptually possible but would
break down the bridges to Gordon HOL);
* move typedef to Pure (which seems just to be wrong, although I have no
example at hand for a valid Pure model that would be invalidated by that).

It is a capriole of Isabelle/Pure to provide types (Âsyntactic
categoriesÂ) and overloading but no means to introduce new types with
specific properties other than purely axiomatic statements. So I wonder
how a check considering constant definitions and Âtype definitions at
the same time ought to be designed. Conceding that I don't know the
essence of previous discussions, two spontaneous ideas:
* A hook design for defs.ML, where more specific checks can be plugged
in later?
* Shadow constants declared by typedef to mimic the additional
dependencies imposed by a stricter check?

There is a third solution, which I used in my proof-of-concept patch:
* if c = t is defined in Pure you let c depend on all entities (in t) that are from Pure's logic and that have a global name, i.e., constants and type constructors. I argue that is not an intrusion of Isabelle/HOL into Isabelle/Pure because the very notion of a type constructor is defined in Pure and therefore c must depend on the type constructors from t nevertheless if we have a definitional mechanism for types at this point. * if there is an object logic that provides additional definitional mechanisms (e.g., typedef in Isabelle/HOL), this object logic can add additional "edges" to the graph of dependencies, as it is already done nowadays for example for Abs and Rep morphisms. E.g., if I define tau = S, I let tau depend on all entities from S. * As you can see no hooks and no shadow constants are needed and we can still keep separation between the meta-logic and object logics. * 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.

Ondrej





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