Re: [isabelle] Code setup for Fraction_Field



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









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