*To*: Brian Huffman <huffman.brian.c at gmail.com>, Wenda Li <wl302 at cam.ac.uk>*Subject*: Re: [isabelle] Query about the transfer method*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 20 Sep 2014 15:52:06 +0200*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAAMXsibjQ3jz7QNfRZfo+hzzyFAiPGVmp6YBA_iBH3iBgm08JA@mail.gmail.com>*Organization*: TU Munich*References*: <1cfb0644a4ccf41b041fe1b3ee48d5c2@cam.ac.uk> <d26bc5cf1bf7b3703d8526fa04f174ea@cam.ac.uk> <CAAMXsibjQ3jz7QNfRZfo+hzzyFAiPGVmp6YBA_iBH3iBgm08JA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.1.1

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

**References**:**[isabelle] Query about the transfer method***From:*Wenda Li

**Re: [isabelle] Query about the transfer method***From:*Wenda Li

**Re: [isabelle] Query about the transfer method***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Query about the transfer method
- Next by Date: [isabelle] Usability Lifting and Transfer
- Previous by Thread: Re: [isabelle] Query about the transfer method
- Next by Thread: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list