Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lemma pos_mod_bound

Email Gateway (Aug 19 2022 at 15:51):

From: Lars Noschinski <noschinl@in.tum.de>
Hi,

I noticed that there are two variants of the Lemma pos_mod_bound around,
namely

Divides.pos_mod_bound

and

semiring_numeral_div_class.pos_mod_bound

The former takes the shorter name, but the latter is more general
(applicable for 'a :: semiring_numeral_div, not only for int). Apart
from the types, the lemmas are exactly the same.

Can we change the setup so that the shorter name refers to the more
general theorem in future releases?

-- Lars

Email Gateway (Aug 19 2022 at 15:52):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

that is something which could seriously be done.

I guess especially the divisibility matter in HOL-Main is full of rule
duplication which would deserve a systematic cleanup.

Cheers,
Florian
signature.asc

Last updated: Apr 26 2024 at 20:16 UTC