Re: [isabelle] Query about the transfer method



Hi Wenda & al.

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

the issue is related to the fact that lifting always operates on
expressions of a certain type, not on expressions consisting of certain
»transferable« operations.  Hence, if an expression you want to lift
contains operations not defined using lift_definition, you get
unexpected (unusable) results from transfer.

There are a couple of subissues actually arising here, which should not
bother you at the moment and I will set them out in a separate thread.
For the moment just note that you can often help yourself using the
following pattern

lemma …
unfolding (*) proof transfer
  …
qed

where in * you place equational theorems which unfold the
»untransferable« operations to »transferable« ones.

> 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?

I am currently absorbed in preparing a co-work for an AFP submission
concerning multivariate polynomials.  After that the future of
Polynomial.thy can come on the agenda again.

Cheers,
	Florian

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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