Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proposal to add two lemmas in /HOL/GCD.thy abo...

Email Gateway (Aug 22 2022 at 21:12):

From: Lawrence Paulson <lp15@cam.ac.uk>
These certainly look useful; thanks!
Larry

Email Gateway (Aug 23 2022 at 08:16):

From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Hello,

I propose to add the following lemmas about the multiplicativity of the
gcd function, to be placed after the lemma division_decomp in
/HOL/GCD.thy.

lemma gcd_multiplicative_aux: "gcd c (a * b) dvd gcd c a * gcd c b"
proof -
obtain a' b' where "gcd c (a * b) = a' * b' ∧ a' dvd a ∧ b' dvd b"
using gcd_dvd2 [of c, THEN division_decomp, of a b] by blast
moreover then have "a' dvd gcd c a ∧ b' dvd gcd c b"
by (metis dvd_mult_left dvd_mult_right gcd_dvd1 gcd_greatest)
ultimately show ?thesis
by (simp only: mult_dvd_mono)
qed

lemma gcd_multiplicative:
assumes "coprime a b"
shows "gcd c (a * b) = gcd c a * gcd c b" (is "?gab = ?ga * ?gb")
proof -
have "?ga * ?gb dvd ?gab"
using ‹coprime a b› coprime_divisors [of ?ga a ?gb b] divides_mult
[of ?ga ?gab ?gb] by simp
then show ?thesis
using gcd_multiplicative_aux by (simp add: associated_eqI
normalize_mult)
qed

I'd be happy to hear if the naming or proofs can be improved.

Best,
Christian

Last updated: Nov 21 2024 at 12:39 UTC