*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] How to extract the record from a locale?*From*: Holden Lee <hl422 at cam.ac.uk>*Date*: Thu, 10 Jul 2014 12:38:44 +0100*Cc*: Holden Lee <hl422 at cam.ac.uk>*In-reply-to*: <53BE6C4C.8020201@inf.ethz.ch>*References*: <CAKSvo_Z-jH2QNwrWX=ODS0K=HYPZpzzaD7-w9gEufHvJY2gVOg@mail.gmail.com> <53BE6C4C.8020201@inf.ethz.ch>*Sender*: oldheneel at gmail.com

>>I'd like to define a function that given (the record of a) ring R returns the polynomial ring R[X]. Here is my attempt so far. definition polynomial_ring :: "'a ring ⇒ (('a poly) ring)" where "polynomial_ring R = (|*carrier = {p::('a poly). (∀(n::nat). (coeff p n)∈(carrier R))}*, mult =λp q::('a poly). p*q, one = 1::('a poly), zero = 0::('a poly), add =λp q::('a poly). p+q|)" >>I'm getting an error: Type unification failed: Variable 'a::type not of sort zero Type error in application: incompatible operand type Operator: op ∈ (coeff p n) :: ??'a set ⇒ bool Operand: carrier R :: 'a set >>It seems to be complaining that I need 'a to be of type zero, but (1) I don't know where to supply this info, and (2) I would rather it be automatically supplied by the zero in 'a ring. 2014-07-10 11:34 GMT+01:00 Andreas Lochbihler < andreas.lochbihler at inf.ethz.ch>: > Hi Holden, > > Locales normally do not introduce a record type for the set of parameters > they fix. However, if you refer to the development in HOL/Algebra, there > are record definitions in the theories. For example, the record type is "'a > ring" for the locale "ring". It is defined at the top of > ~~/src/HOL/Algebra/Ring.thy. > > More precisely, the locales in HOL/Algebra use the extensible variant of > the record types, i.e, "('a, 'b) ring_scheme" instead of "'a ring". The > additional type parameter 'b represents all future field extensions of the > record. It depends on your construction whether you can work with arbitrary > extensions or have to stick to the fixed set of operations. > > In Isabelle/jEdit You can find out about the types of the record by > Ctrl-hovering over the fixed variable at the locale declaration. Ctrl-Click > on the type takes you to the record declaration. > > Hope this helps, > Andreas > > > On 10/07/14 10:25, Holden Lee wrote: > >> For example, given a locale like *ring*, I would like to get the type of >> >> its record ('a set (carrier), 'a=>'a=>'a (mult),...), so that I can feed >> it >> into a function that does an algebraic construction on rings. >> >> definition polynomial_ring :: "<ring_record> => <ring_record>" >> >> -Holden >> >>

**Follow-Ups**:**Re: [isabelle] How to extract the record from a locale?***From:*Andreas Lochbihler

**References**:**[isabelle] How to extract the record from a locale?***From:*Holden Lee

**Re: [isabelle] How to extract the record from a locale?***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations
- Next by Date: Re: [isabelle] How to extract the record from a locale?
- Previous by Thread: Re: [isabelle] How to extract the record from a locale?
- Next by Thread: Re: [isabelle] How to extract the record from a locale?
- Cl-isabelle-users July 2014 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