*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Code setup for Fraction_Field*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 04 Sep 2015 12:19:49 +0200*In-reply-to*: <55E96F1F.6000001@in.tum.de>*References*: <55E96F1F.6000001@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

> In fact, from what I can see, the equivalences are not provable at all > in Isabelle2015, because euclidean_ring_gcd also talks about the set > versions Gcd and Lcm. And in Euclidean_Algorithm, Lcm_eucl and > Gcd_eucl are defined such that they also work for infinite sets > whereas in GCD, Lcm for nat is defined to be 0 for infinite sets. So > what is the plan here? The Lcm of an infinite number of nats /is/ 0. Think about it: We are looking for a natural number that has infinitely many divisors. The only such number is 0. You can think of 1 as the "biggest" element w.r.t. divisibility and 0 as the "smallest" â 1 divides anything and is divided by nothing (except itself); 0 is divided by everything and divides nothing but itself. So I don't really see any reason why this should not work. I'll have a look at it and see what I can do. Cheers, Manuel On 04/09/15 12:01, Andreas Lochbihler wrote: > Hi Manuel, > > On 04/09/15 11:44, Manuel Eberl wrote: >>> 1. I noticed that there are the type classes euclidean_ring and >>> euclidean_ring_gcd. Most of the theorems about gcd which I need are in >>> euclidean_ring_gcd, but not in euclidean_ring itself. Unfortunately, >>> the instantiations for nat, int, etc. are only done for >>> euclidean_ring, not for euclidean_ring_gcd. What are the plans for >>> these type classes? Should I spend any effort on adding instances for >>> euclidean_ring_gcd? Or will this become obsolete with the polishing >>> that is still due? >> >> euclidean_ring_gcd is nothing but euclidean_ring with the additional >> assumption that gcd and Gcd (which are introduced in a syntactical >> typeclass and therefore have no a priori properties associated with >> them) are the same as the euclidean GCD (and the same for LCM). >> >> So, in a sense, there is usually no proof work to be done to make >> anything an instance of euclidean_ring_gcd if you already have >> euclidean_ring; you can just define "gcd = gcd_eucl", "Gcd = Gcd_eucl" >> and so on and you get the instance for free. > That's clear. However, nat and int already have their own > implementation of the GCD... > >> If there is already an existing definition of gcd, you have to prove its >> equivalence to the Euclidean GCD etc., which you can do by showing that >> it fulfils the defining properties of the GCD and that it returns a >> normalised GCD, i.e. "1" and not "-1" for integers. > Well, it is exactly this equivalence proof of which I am uncertain. If > Florian restructures the whole hierarchy such that gcd/lcm definitions > for int and nat are done in terms of gcd_eucl, then the equivalence > proof becomes irrelevant. > > In fact, from what I can see, the equivalences are not provable at all > in Isabelle2015, because euclidean_ring_gcd also talks about the set > versions Gcd and Lcm. And in Euclidean_Algorithm, Lcm_eucl and > Gcd_eucl are defined such that they also work for infinite sets > whereas in GCD, Lcm for nat is defined to be 0 for infinite sets. So > what is the plan here? > > Best, > Andreas > >> On 04/09/15 11:32, Andreas Lochbihler wrote: >>> Hi Florian and Manuel, >>> >>> I have experimented a bit with a normalisation function to be used in >>> the operations over fraction fields and had a look at >>> Euclidean_Algorithm in Number_Theory. >>> >>> >>> >>> 2. I am no longer sure that an invariant-based approach is the optimal >>> thing for fraction field. In the code equation for the arithmetic >>> operation, I don't see any big opportunities to exploit the invariant >>> that nominator and denominator are normalised in some unspecified >>> form. Only the equality tests become simpler (as normal forms are >>> unique and we thus save two multiplications). Instead, it seems much >>> simpler to treat cancellation of common factors as an optimisation >>> without logical significance. For example, we could just add a call to >>> a simplification function before calls to the Fract constructor. The >>> simplification function only has to return an element of the same >>> equivalence class, so for nat and int, we could use a normalisation >>> function based on Euclid's algorithm. For other types, the >>> simplification function could also just be the identity. What do you >>> think? >>> >>> Best, >>> Andreas >>> >>> >>> On 27/08/15 12:02, Florian Haftmann wrote: >>>> Hi Andreas and Prathamesh, >>>> >>>>> We noticed that the code setup for the theory Fraction_Field in >>>>> HOL/Library is broken, at least since Isabelle2013. We would like to >>>>> use >>>>> code generation in his formalisation of knot theory where the >>>>> elements >>>>> of the fraction fields are polynomials over integers. I had a brief >>>>> look >>>>> at the theory Fraction_Field and noticed that there is a smart >>>>> pseudo-constructor Fract, which is declared as code_datatype. So this >>>>> feels as if the code generation was working at some time in the >>>>> distant >>>>> past and got broken somewhen. >>>>> >>>>> Does anyone know about the status of Fraction_Field? >>>> >>>> I dimly remember that initially Fraction_Field just took over the >>>> then-used code setup from the rationals, and maybe it never worked as >>>> intended (would need a closer investigation to find out actually). >>>> >>>> When code generation had been equipped with invariants, I revisited >>>> Fraction_Field to make a code setup close to the rationals but soon >>>> realized thatâ >>>> >>>>> I believe that it would be fairly easy to "fix" the problem of code >>>>> generator setup by deriving a few code equation from the lemmas, but >>>>> this will clearly result in suboptimal code for two reasons. >>>>> First, we >>>>> need tests whether the denominator is 0 all over the place. >>>>> Second, the >>>>> elements of the fraction fields will not be normalised automatically. >>>> >>>> âI need a generalized gcd for that, and so I let everything stand as >>>> it is. >>>> >>>>> For the application on polynomials, this means that we would need >>>>> some >>>>> Euclidean algorithm for cancelling common factors of polynomials. I >>>>> dimly remember that there is some support for the Euclidean >>>>> algorithm in >>>>> the pipeline. What is the status there? >>>> >>>> I think you can build on the corresponding theory in Number_Theory, >>>> but >>>> that needs some further rounds of polishing before I would >>>> recommend to >>>> turn it into a ÂhardÂ dependency. Instead I suggest to put the code >>>> setup into a separate theory ÂExecutable_Fraction_FieldÂ. This is >>>> what >>>> we did 8 years ago when code generation was still highly experimentalâ >>>> >>>> Hope this helps, >>>> Florian >>>> >>>>> >>>>> Best, >>>>> Andreas and Prathamesh >>>>> >>>>> >>>> >> >>

- Previous by Date: Re: [isabelle] Code setup for Fraction_Field
- Next by Date: Re: [isabelle] Code setup for Fraction_Field
- Previous by Thread: Re: [isabelle] Code setup for Fraction_Field
- Next by Thread: Re: [isabelle] Code setup for Fraction_Field
- Cl-isabelle-users September 2015 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