Consider the following (contrived) example:

```
datatype 'a rep = Rep ‹'a set›
typedef 'a abs = "{Rep A | A :: 'a set. finite A}"
by blast
setup_lifting type_definition_abs
```

The last line gives the following warning:

```
Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "rep" found.
```

And indeed no relator has been created for `rep`

.

However, the following succeeds:

```
typedef 'a direct = "{A | A :: 'a set. finite A}"
by blast
setup_lifting type_definition_direct
```

This shows that there is a relator for `set`

and that `setup_lifting`

can work with it.

Why isn’t there a relator for `Rep`

? Furthermore, how is this problem fixed most easily? In the real, non-contrived development, there are multiple `set`

fields.

Hmm, let me have a guess: The `set`

type is not a BNF, since its set function is the identity and a given set can have as many elements as the element type, so that an upper bound on the number of elements that is independent of the element type does not exist. However, `datatype`

apparently generates a relator only for those type parameters that aren’t used as parameters of types that aren’t BNFs. Is this correct?

Yes, this is correct. As a workaround, you can define your own relator on rep and register it with the Lifting package. See https://www.isa-afp.org/browser_info/current/AFP/BNF_CC/DDS.html for an example how this is done (there the function space is the culprit why the mapper/relator do not touch the 'a type variable). The relevant theorems for lifting are the ones carrying attributes (`relator_eq`

, `relator_mono`

, `relator_distr`

, `quot_map`

, and potentially also some of the `transfer_rule`

s although I'm not sure there which ones are strictly necessary).

Last updated: Dec 07 2023 at 08:19 UTC