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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
