*To*: Holden Lee <hl422 at cam.ac.uk>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How to extract the record from a locale?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 10 Jul 2014 14:43:29 +0200*In-reply-to*: <CAKSvo_Z1AOzoXsxXYywzkKQsaJu-P5vprDqnc=qfE5MHeo2k+A@mail.gmail.com>*References*: <CAKSvo_Z-jH2QNwrWX=ODS0K=HYPZpzzaD7-w9gEufHvJY2gVOg@mail.gmail.com> <53BE6C4C.8020201@inf.ethz.ch> <CAKSvo_Z1AOzoXsxXYywzkKQsaJu-P5vprDqnc=qfE5MHeo2k+A@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Hi Holden,

Best, Andreas On 10/07/14 13:38, Holden Lee wrote:

I'd like to define a function that given (the record of a) ring R returnsthe 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 setIt seems to be complaining that I need 'a to be of type zero, but (1) Idon'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

**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

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

- Previous by Date: Re: [isabelle] How to extract the record from a locale?
- Next by Date: [isabelle] proof by contradiction
- Previous by Thread: Re: [isabelle] How to extract the record from a locale?
- Next by Thread: [isabelle] proof by contradiction
- 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