Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] superfluous assumption in Gcd_remove0_nat

Email Gateway (Apr 05 2025 at 17:47):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
The finiteness assumption in GCD.Gcd_remove0_nat can (and therefore
should) be omitted. Moreover, the claim holds in any semiring (probably
fits well after the lemma Gcd_Lcm)

lemma "Gcd M = Gcd (M - {0 :: 'a :: semiring_Gcd})"
proof-
  have "(∀ m ∈ M. b dvd m) ⟷ (∀ m ∈ (M - {0}). b dvd m)" for b
    by blast+
  thus ?thesis
    unfolding Gcd_Lcm by presburger
qed

Stepan

Email Gateway (Apr 05 2025 at 18:48):

From: Tobias Nipkow <nipkow@in.tum.de>
Stepan,

Thanks for that, I'll take care of it.

Tobias

On 05/04/2025 19:41, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

The finiteness assumption in GCD.Gcd_remove0_nat can (and therefore should) be
omitted. Moreover, the claim holds in any semiring (probably fits well after the
lemma Gcd_Lcm)

lemma "Gcd M = Gcd (M - {0 :: 'a :: semiring_Gcd})"
proof-
  have "(∀ m ∈ M. b dvd m) ⟷ (∀ m ∈ (M - {0}). b dvd m)" for b
    by blast+
  thus ?thesis
    unfolding Gcd_Lcm by presburger
qed

Stepan

smime.p7s

Last updated: Apr 17 2025 at 20:22 UTC