*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]*From*: OndÅej KunÄar <kuncar at in.tum.de>*Date*: Tue, 22 Sep 2015 17:07:37 +0200*In-reply-to*: <560164FF.6000807@informatik.tu-muenchen.de>*References*: <A3211BFC-696D-4616-AAD4-1E916B859A78@lri.fr> <560164FF.6000807@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

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:

Ondrej

**Follow-Ups**:

**References**:**[isabelle] Isabelle Foundation & Certification***From:*Burkhart Wolff

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

- Previous by Date: [isabelle] find_consts does not find constants from BNF package
- Next by Date: Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]
- Previous by Thread: Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]
- Next by Thread: Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list