[isabelle-dev] [isabelle] Code setup for Fraction_Field

[Andreas Lochbihler]

Hi Florian,

I am continuing this thread on isabelle-dev as you have suggested.

>>> 3. For fraction fields over polynomials over rings (rather than
>>> fields), one can use subresultants, but I have not been able to find
>>> them formalised in Isabelle. Are they hidden somewhere? If not, are
>>> there any plans to formalise them?
>>
>> Are subresultants really necessary for this?
>>
>> definition ppdivmod_rel :: "'a::idom poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly
>> ⇒ 'a ⇒ bool"
>> where
>>    "ppdivmod_rel x y q r m ⟷ (
>>        smult m x = q * y + r ∧ (if y = 0 then q = 0 else r = 0 ∨ degree r
>> < degree y)
>>        ∧  ( m= (if x=0 ∨ y=0 then 1 else (lead_coeff y) ^ (degree x + 1 -
>> degree y))))"
>
> I am somehow lost how the »algebraic stack« is supposed to look like in
> the whole example.  Something like Fraction over Poly over Int?
Yes, that's the idea.

> Since Poly over Int forms a factorial ring but not an euclidean ring,
> the question is how to generalize normalization of quotients a / b
> accordingly.  It won't work naturally with type classes:
>
> 	Poly over Rat --> normalization via gcd / eucl
> 	Poly over Poly over Rat --> somehow different
>
> Hence, some type class magic would be needed to detect whether to use
> the rather efficient euclidean algorithm or something different – or
> even refrain from normalization at all!?
The type class magic needed for this sort of decision is pretty simple, it's described in 
my paper on AFP/Containers from ITP 2013. You just have to wrap a gcd function in "_ 
option" such that the normalisation algorithm for fraction fields can check whether 
normalisation via gcd is possible or whether something else is needed. If fraction field 
is implemented via code_abstype with the invariant that only normalised fractions occur, 
then the decision about the normalisation algorithm is logically relevant, as the 
normalisation function shows up in the code equations of the form

   fract_of (p + q) =
   normalize_fract (<implementation of addition> (fract_of p) (fract_of q))

However, if we do not require normalised fractions and instead use a quotient-like code 
setup for fraction fields with code_datatype, the decision about normalisation need *not* 
be logically relevant. The code equations then look like the following:

   Fract a b + Fract c d =
   normalise_fract (<implementation of addition> (a, b) (c, d)))

The function normalise_fract can be a type class parameter, so one can define it 
differently for different types. As it returns the quotiented value, the decision whether 
to normalise and how to normalise is no longer logically relevant. So the choice could 
depend on extra-logical tricks (like inspecting the name of types).

Best,
Andreas