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



Possibly now is a good time to plug my own paper "Defining functions on equivalence classes”, which is available* from my webpage (https://www.cl.cam.ac.uk/~lp15/papers/refereed.html). In this I outline how one can create quotient constructions quite easily using the set-theoretic primitives of Isabelle/HOL. Obviously quotient_type is easier to use, but as discussed, it wants to introduce a type and there is no reason on earth to conflate quotient constructions with types.

Larry Paulson

* It is available via an ACM system that supposedly provides open access from the author’s own webpage. If it doesn’t work for you, please email me for a copy.

> On 8 Jul 2019, at 15:52, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
> 
> Consider the following attempt of a locale definition:
> 
>    locale example =
>      fixes R :: "['a, 'a] ⇒ bool"
>      assumes is_equivalence: "equivp R"
>    begin
> 
>    quotient_type Q = 'a / R
> 
>    end
> 
> Isabelle doesn’t accept the use of the type variable `'a` in the
> quotient type definition, although it does accept referring to `'a` in
> types. How can I define a quotient type for the type `'a`?





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