# [isabelle] Query about the transfer method

```Dear Isabelle experts,

```
I have defined a function to convert rational polynomials to real ones, and want to prove this function respects some other operations on polynomials.
```
theory Scratch1
imports Complex_Main "~~/src/HOL/Library/Polynomial"
begin

lift_definition real_poly:: "rat poly ⇒ real poly" is
"%p. real_of_rat o p " unfolding almost_everywhere_zero_def by auto

lemma real_poly_plus: "real_poly (p + q) = real_poly p + real_poly q"
(*apply transfer*)
using real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)

end

```
Although the lemma real_poly_plus can be proved by "using real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)", I really want to use the transfer method to convert goals from abstract types to representation types as many lemmas related to "of_rat" do. However, after "apply transfer" the lemma real_poly_plus becomes:
```
1. !!p q. almost_everywhere_zero p ==>
```
almost_everywhere_zero q ==> real_of_rat ∘ ?ad16 p q = ?ae16 (real_of_rat ∘ p) (real_of_rat ∘ q) 2. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =) (pcr_poly op =))) ?ad16 op + 3. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =) (pcr_poly op =))) ?ae16 op +
```
```
which I don't know how to proceed. Is there anything I can do to use the transfer method properly in my case?
```

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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