Email Gateway (Aug 19 2022 at 16:08): Email Gateway (Aug 19 2022 at 16:08):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear all,
In Isabelle there is the class gcd:
class gcd = zero + one + dvd +
fixes gcd :: "'a => 'a => 'a"
and lcm :: "'a => 'a => 'a"
Polynomials (
http://isabelle.in.tum.de/library/HOL/HOL-Library/Polynomial.html) have
been instantiated to such a class defining a gcd for polynomials, but
saying nothing about lcm:
instantiation poly :: (field) gcdbegin
function gcd_poly :: "'a::field poly => 'a poly => 'a poly"where
"gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"| "y ≠
0 ==> gcd (x::'a poly) y = gcd y (x mod y)"by auto
termination "gcd :: _ poly => _"by (relation "measure (λ(x, y). if y =
0 then 0 else Suc (degree y))")
(auto dest: degree_mod_less)
declare gcd_poly.simps [simp del]
instance ..
end
So, I am wondering why there is no definition of lcm for polynomials, but
polynomials have been made a gcd instance.
In addition, gcd of polynomials can be computed:
value "gcd [:2,3,6,5::real :] [:4,6,12,10:]" returns "[:2 / 5, 3 / 5, 6 /
5, 1:]" :: "real poly"
On the contrary, lcm can't be computed (since it has not been defined).
The problem arose when I was trying to instantiate polynomials to the
euclidean_ring_gcd class developed by Manuel Eberl (
http://isabelle.in.tum.de/repos/isabelle/file/5f88c142676d/src/HOL/Number_Theory/Euclidean_Algorithm.thy).
There I have to prove that "(lcm::'a poly⇒ 'a poly ⇒ 'a poly) = lcm_eucl",
but I can't prove it since I don't know anything about lcm for polynomials.
If lcm for polynomials is defined in the instance to the gcd class (for
example, by means of the below definition), then lcm could be computed and
the statement "(lcm::'a poly⇒ 'a poly ⇒ 'a poly) = lcm_eucl" can be proved.
definition lcm_poly :: "'a::field poly ⇒ 'a poly ⇒ 'a poly"
where "lcm_poly x xa = x * xa div (gcd x xa * [:coeff (x * xa) (degree (x *
xa)):])"
Cheers,
Jose
Email Gateway (Aug 19 2022 at 16:09):From: Jose Divasón <jose.divasonm@unirioja.es>
Thank you both!!
I was working with my local clone of Polynomial.thy, but it's nice to see
such a trick. I have already seen the new lcm definition in the repository
version.
Cheers,
Jose
Email Gateway (Aug 19 2022 at 16:15):From: Manuel Eberl <eberlm@in.tum.de>
I assume lcm does not exist because no one ever needed it. This was
actually one of the main reasons why I chose to overhaul the whole GCD
stuff in HOL – many results I needed about the GCD of polynomials were
missing.
For an instantiation of GCD for polynomials, see Polynomial.thy on my
Github repo: https://github.com/3of8/isabellehol_gcd
I know that the whole thing with gcd and gcd_eucl is a bit complicated;
this was because we wanted to keep the existing gcd/lcm constants purely
syntactical, as before.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 16:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
So, I am wondering why there is no definition of lcm for polynomials, but
polynomials have been made a gcd instance.
this is indeed an omission.
You can add a lcm definition either by making your local clone of
Polynomial.thy, or by a low-level trick:
defs
lcm_gcd_inst_def: "gcd_poly_inst.lcm_poly a b == a * b div smult
(coeff a (degree a) * coeff b (degree b)) (gcd a b)"
lemma lcm_gcd_def:
"lcm a b = a * b div smult (coeff a (degree a) * coeff b (degree b))
(gcd a b)"
apply (tactic ‹ALLGOALS (CONVERSION (Axclass.unoverload_conv @{theory}))›)
unfolding lcm_gcd_inst_def
apply (tactic ‹ALLGOALS (CONVERSION (Axclass.overload_conv @{theory}))›)
..
I am currently underway to incorporate a proper lcm definition into
Polynomial.thy, so in future releases this issue is resolved.
Hope this helps,
Florian
signature.asc
Last updated: Apr 20 2024 at 01:05 UTC