*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>, Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Code setup for Fraction_Field*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 4 Sep 2015 11:32:37 +0200*Cc*: prathamesh at imsc.res.in*In-reply-to*: <55DEE024.3070504@informatik.tu-muenchen.de>*References*: <55DED10F.5030507@inf.ethz.ch> <55DEE024.3070504@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.8.0

Hi Florian and Manuel,

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, FlorianBest, Andreas and Prathamesh

**Follow-Ups**:**Re: [isabelle] Code setup for Fraction_Field***From:*Manuel Eberl

**Re: [isabelle] Code setup for Fraction_Field***From:*Jose DivasÃn

- Previous by Date: [isabelle] Export from class target fails to replace operations
- Next by Date: Re: [isabelle] Code setup for Fraction_Field
- Previous by Thread: Re: [isabelle] Export from class target fails to replace operations
- 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