[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.