Re: [isabelle] How to access a locale type parameter in a quotient type definition



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.



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