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



Hi Holden,

You are trying to mix the two flavours of algebra formalisations, which does not work so well. HOL/Algebra uses locales parametries by carriers and the operations. The other flavour with type classes is the one available in HOL/Main already. Library/Polynomial belongs to the type class flavour, i.e., it takes the ring operations from the type classes. There is no way to have it take 0 from the ring that you provide as a parameter.

You might want to look at HOL/Algebra/UnivPoly, which formalises univariate polynomials with locales. The function UP, e.g., transforms a ring into the ring of polynomials over it.

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






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