Email Gateway (Aug 19 2022 at 15:19): Email Gateway (Aug 19 2022 at 15:19):From: Holden Lee <hl422@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 15:19):From: Andreas Lochbihler <andreas.lochbihler@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
Email Gateway (Aug 19 2022 at 15:20):From: Holden Lee <hl422@cam.ac.uk>
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@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,
AndreasOn 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
Email Gateway (Aug 19 2022 at 15:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 20 2024 at 08:16 UTC