Re: [isabelle] Query about the transfer method



Dear Isabelle experts,

I have investigated my previous problem. The problem can be solved by providing an alternative plus operation for polynomials:

lift_definition plus_poly1 :: "'a::comm_monoid_add poly ⇒ 'a poly ⇒ 'a poly"
  is "%p q n. p n + q n" sorry

lemma real_poly_plus: "real_poly (plus_poly1 p q) = plus_poly1 (real_poly p) (real_poly q)"
  apply transfer
  (*as desired*)

Compared to the original plus operation for polynomials:

lift_definition plus_poly :: "'a poly ⇒ 'a poly ⇒ 'a poly"
  is "%p q n. coeff p n + coeff q n"

then only difference between plus_poly1 and plus_poly is that plus_poly1 takes its arguments as representation types for polynomials (i.e. "nat => 'a") while plus_poly takes its arguments as abstract types (i.e. "'a poly"). In my case, plus_poly1 works much better for the transfer method than plus_poly.

Therefore, it occurs to me when we are using lift_defition, shall we try to use representation types and avoid abstract types? I have checked Int.thy, Rat.thy and Real.thy, and they all fit my hypothesis, while definitions in Polynomial.thy confuse me.

Many thanks for any help,
Wenda

On 2014-09-16 13:14, Wenda Li wrote:
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.