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
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)"
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,
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
imports Complex_Main "~~/src/HOL/Library/Polynomial"
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"
using real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)
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?
University of Cambridge
This archive was generated by a fusion of
Pipermail (Mailman edition) and