<p>The <code>setup_lifting</code> is only useful if you intend to use the lifting-and-transfer framework, for the details of which you can read <a href="https://www21.in.tum.de/%7Ekuncar/documents/huffman-kuncar-cpp2013.pdf" rel="nofollow noreferrer">Huffman and Kuncar's CPP paper</a>. Some recent progress in this framework is mostly related to bounded natural functors, for which you can have a look at this <a href="https://arxiv.org/abs/2104.05348" rel="nofollow noreferrer">paper</a>.</p>
<p>Proposing suitable relators requires insight of the data type. Here <code>setup_lifting</code> gives us some relatively easy relator theorems for free.</p>
<p>(Answer from the Isabelle Zulip Chat.)</p>
How to setup_lifitng with custom types (aka how to define a "relator")?
<p>In the Isabelle/HOL, I would like to work with two custom <code>typedef</code>s that build on top of each other, and show that both of them instantiate certain type classes (e.g. from <code>HOL.Rings</code>). I do not understand what definitions or facts are required to properly call <code>setup_lifiting</code> in this case. Moreover, I would like to understand what precise purpose this keyword serves after declaring a <code>typedef</code> (currently I simply try to mimick the structure of existing work) and what the so-called <em>relators</em> are which are used in the process. Neither the <em>locale</em> nor the <em>typeclass</em> PDF tutorials go into much detail on this command.</p>
<p>For explicitness, consider the <a href="https://www.isa-afp.org/browser_info/current/AFP/Polynomials/Polynomials.html" rel="nofollow noreferrer">AFP entry implementing polynomials</a>, which schematically defines monomials as</p>
<pre><code>type_synonym 'v monom_list = &quot;('v × nat)list&quot; 
[...]
typedef (overloaded) 'v monom = &quot;Collect (monom_inv :: ...)&quot; 
</code></pre>
<p>for an adequate invariant <code>monom_inv</code>. The same entry proceeds to define polynomials as</p>
<pre><code>type_synonym ('v,'a)poly = &quot;('v monom × 'a)list&quot;
</code></pre>
<p>and also defines a suitable invariant <code>poly_inv</code>.</p>
<p>After the typedef of <code>'v monom</code>, it appears to be no problem to call <code>setup_lifting type_definition_monom</code> as the necessary <em>relators</em> (?) 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.)</p>
<p>However, after a new <code>typedef (overloaded) ('v, 'a) polyq = &quot;Collect (poly_inv :: ...)&quot;</code> (which is not part of the AFP entry cited above), things are different. Now, calling</p>
<pre><code>setup_lifting type_definition_polyq
</code></pre>
<p>yields a warning which reads: <em>Generation of a parametrized correspondence relation failed. Reason: No relator for the type &quot;Polynomials.monom&quot; found.</em></p>
<p><strong>Do I need to address this issue to afterwards call for example <code>instatiation polyq :: (...) comm_semiring_1</code>? If yes, how can I go about defining a relator for the <code>monom</code> type?</strong></p>