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

[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?

Just a few bits,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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