*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How to access a locale type parameter in a quotient type definition*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Tue, 9 Jul 2019 22:21:45 +0300*In-reply-to*: <CALaF1UJEOiNQ9BdVcbGYmG=WMhddz6f6G0L7Jp8T-XVo=hnBgA@mail.gmail.com>*References*: <CALaF1UKS6tOo=Q+gjdkK2TCr7gSdz9yvfFdqqFUCMrxqBC=WgQ@mail.gmail.com> <CALaF1UJEOiNQ9BdVcbGYmG=WMhddz6f6G0L7Jp8T-XVo=hnBgA@mail.gmail.com>

Dear Wolfgang Jeltsch Therefore the message I’m taking from your e-mail is that > what I want isn’t supported and making it somehow supported is > complicated and gives only a partial solution. > I think for my use case it’s easiest to just define the quotient types > manually for each individual interpretation of the locale. I believe that the opening remark in my original email was not very clear - I was in a rush to finish the email and was slightly careless - please accept my apologies. However, indeed, I meant to say exactly what you inferred from it. I would also like to provide a more clear explanation of the opening remark using the PhD thesis Ondřej Kunčar as the general reference. Isabelle/HOL provides two definitional primitives: one for overloaded constants and one for types (i.e. typedef). All other definitional mechanisms (including, e.g., quotient_type) have to be defined in terms of these primitives, provided that one does not neglect the LCF approach. The typedef primitive allows for the definition of new types in terms of an isomorphism with respect to an arbitrary non-empty subset of an existing type. typedef α k = S requires S to be a closed term, k to be a fresh type constructor and all type variables in S need to be among the variables in α. If one is to try to define a nullary type constructor based on an existing fixed type variable, then the last condition will be inevitably violated. Unfortunately, provided that there is no misunderstanding on my part, this is exactly what you were trying to do by calling the command quotient_type with the fixed type variable occurring in the input term and not occurring on the lhs in the specification of the type constructor. Also, perhaps, I can provide an explanation for another remark from your original email "although it does accept referring to `'a` in types". When you invoke the command quotient_type, your intention is to declare a new type constructor. Of course, the mechanism of the declaration of new type constructors is very different from merely using a fixed type variable as an input to the existing type constructor. Hopefully, this clarifies why one can refer to fixed variables when constructing new types, but not new type constructors. Thank you -- Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.

**References**:**Re: [isabelle] How to access a locale type parameter in a quotient type definition***From:*mailing-list anonymous

**Re: [isabelle] How to access a locale type parameter in a quotient type definition***From:*mailing-list anonymous

- Previous by Date: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Next by Date: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Previous by Thread: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Next by Thread: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Cl-isabelle-users July 2019 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