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

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

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

> 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

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