Re: [isabelle] How to extract the record from a locale?

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,

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


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