In the Isabelle/HOL, I would like to work with two custom typedefs that build on top of each other, and show that both of them instantiate certain type classes (e.g. from HOL.Rings). I do not understand what definitions or facts are required to properly call setup_lifiting in this case. Moreover, I would like to understand what precise purpose this keyword serves after declaring a typedef (currently I simply try to mimick the structure of existing work) and what the so-called relators are which are used in the process. Neither the locale nor the typeclass PDF tutorials go into much detail on this command.
For explicitness, consider the AFP entry implementing polynomials, which schematically defines monomials as
type_synonym 'v monom_list = "('v × nat)list"
[...]
typedef (overloaded) 'v monom = "Collect (monom_inv :: ...)"
for an adequate invariant monom_inv. The same entry proceeds to define polynomials as
type_synonym ('v,'a)poly = "('v monom × 'a)list"
and also defines a suitable invariant poly_inv.
After the typedef of 'v monom, it appears to be no problem to call setup_lifting type_definition_monom as the necessary relators (?) for the underlying types (in particular lists) are part of the standard library. (Please correct if this is a misunderstanding of what's actually going on.)
However, after a new typedef (overloaded) ('v, 'a) polyq = "Collect (poly_inv :: ...)" (which is not part of the AFP entry cited above), things are different. Now, calling
setup_lifting type_definition_polyq
yields a warning which reads: Generation of a parametrized correspondence relation failed. Reason: No relator for the type "Polynomials.monom" found.
Do I need to address this issue to afterwards call for example instatiation polyq :: (...) comm_semiring_1? If yes, how can I go about defining a relator for the monom type?