# Re: [isabelle] setup_lifting: »No relator for the type … found«

```Hi Florian,

```
When setup_lifting warns you about missing relators, it looks for a corresponding quotient theorem that is registered as [quot_map], something like
```
lemma Quotient_poly_mapping [quot_map]:
assumes Q1: "Quotient R1 Abs1 Rep1 T1"
and Q2: "Quotient R2 Abs2 Rep2 T2"
```
shows "Quotient (poly_mapping_rel R1 R2) (map_poly_mapping Rep1 Abs2) (map_poly_mapping Abs1 Rep2) (poly_mapping_rel T1 T2)"
```
```
If you can prove such a quotient theorem, setup_lifting will generate a parametrised relator for lifting to nat_mapping where the type of the type parameter can change. The lemmas that you have shown will help setup_lifting to prove properties of the relator pcr_nat_mapping.
```

Andreas

```
PS: I do not think that you can prove a quotient theorem like the above, because poly_mapping is not really parametric in its type parameters: 0::'b::zero has to be mapped to zero in the other type, and the finiteness constraint prevents quotients with non-finite equivalence classes.
```
On 19/04/14 09:34, Florian Haftmann wrote:
```
```Hi all,

in the example beneath, on the last setup_lifting command, I get »No
relator for the type poly_mapping found«

I tried my best to glimpse from exisiting lifting examples and the
reference manual what is missing and added poly_mapping_rel with some
characteristic properties (proofs only sketched), but the warning remains.

Any hints?

Thanks a lot,
Florian

```
```typedef ('a, 'b) poly_mapping =
"{f :: 'a ⇒ 'b::zero. finite {x. f x ≠ 0}}"
morphisms lookup Abs_poly_mapping
proof -
have "(λ_::'a. (0 :: 'b)) ∈ ?poly_mapping" by simp
then show ?thesis by (blast intro!: exI)
qed

setup_lifting (no_code) type_definition_poly_mapping

lift_definition poly_mapping_rel :: "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool)
⇒ ('a, 'c::zero) poly_mapping ⇒ ('b, 'd::zero) poly_mapping ⇒ bool"
is "fun_rel"
..

lemma [relator_eq]:
"poly_mapping_rel HOL.eq HOL.eq = HOL.eq"
apply (rule ext)+
apply transfer
done

lemma [relator_mono]:
"C ≤ A ⟹ B ≤ D ⟹ poly_mapping_rel A B ≤ poly_mapping_rel C D"
apply (rule le_funI)+
apply transfer
apply (drule fun_mono)
apply auto
done

lemma [relator_distr]:
"poly_mapping_rel R S OO poly_mapping_rel R' S' ≤ poly_mapping_rel (R OO R') (S OO S')"
"left_unique R ⟹ right_total R ⟹ right_unique R' ⟹ left_total R'
⟹ poly_mapping_rel (R OO R') (S OO S') ≤ poly_mapping_rel R S OO poly_mapping_rel R' S'"
"right_unique R' ⟹ left_total R' ⟹ left_unique S' ⟹ right_total S'
⟹ poly_mapping_rel (R OO R') (S OO S') ≤ poly_mapping_rel R S OO poly_mapping_rel R' S'"
apply (rule le_funI)+
apply transfer apply (auto elim: fun_relE)
apply (rule le_funI)+
apply transfer apply auto defer
apply (rule le_funI)+
apply transfer apply auto sorry

typedef 'a nat_mapping = "UNIV :: (nat, 'a) poly_mapping set" ..

setup_lifting type_definition_nat_mapping
```
```

```
```

```

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