Re: [isabelle] Query about the transfer method



Hi Wenda,

You are completely right about the uses of lift_definition in the
Polynomial theory. The point of lift_definition is to avoid writing
definitions in terms of the Rep/Abs functions for types. Function
"coeff" is the Rep function for the polynomial type, and so it should
be avoided when using lift_definition.

Polynomial.thy was written before lift_definition/transfer existed, so
the original definitions all used "coeff" explicitly. When it was
ported over to use lift_definition (apparently by Florian Haftmann
some time last year), I guess some redundant uses of "coeff" were
overlooked.

If it makes the "transfer" method more useful, it would probably be a
good idea to change the definitions in Polynomial.thy to match the
style of your "plus_poly1". Perhaps Florian is willing to take this
on?

- Brian


On Thu, Sep 18, 2014 at 6:24 AM, Wenda Li <wl302 at cam.ac.uk> wrote:
> 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.