From: Jakub Kądziołka <kuba@kadziolka.net>

Hello,

I have proven a number of lemmas today that, I believe, should be

included in the distribution.

Regards,

Jakub Kądziołka

P.S. My previous suggestion regarding a HOL-Algebra lemma [1] went without a

response. I'd appreciate someone looking into it.

[1]: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-November/msg00043.html

context factorial_semiring

begin

lemma infinite_unit_divisor_powers:

assumes "y ≠ 0"

assumes "is_unit x"

shows "infinite {n. x^n dvd y}"

proof -

from `is_unit x`

have "is_unit (x^n)" for n

using is_unit_power_iff by auto

hence "x^n dvd y" for n

by auto

hence "{n. x^n dvd y} = UNIV"

by auto

thus ?thesis

by auto

qed

corollary is_unit_iff_infinite_divisor_powers:

assumes "y ≠ 0"

shows "is_unit x ⟷ infinite {n. x^n dvd y}"

using infinite_unit_divisor_powers finite_divisor_powers assms by auto

lemma multiplicity_zero_left [simp]: "multiplicity 0 x = 0"

apply (cases "x = 0")

by (auto intro: not_dvd_imp_multiplicity_0)

lemma multiplicity_dvd_iff_dvd:

assumes "x ≠ 0"

shows "p^k dvd x ⟷ p^k dvd p^multiplicity p x"

proof (cases "is_unit p")

case True

then have "is_unit (p^k)"

using is_unit_power_iff by simp

hence "p^k dvd x"

by auto

moreover from `is_unit p`

have "p^k dvd p^multiplicity p x"

using multiplicity_unit_left is_unit_power_iff by simp

ultimately show ?thesis by simp

next

case False

show ?thesis

proof (cases "p = 0")

case True

then have "p^multiplicity p x = 1"

by simp

moreover have "p^k dvd x ⟹ k = 0"

proof (rule ccontr)

assume "p^k dvd x" and "k ≠ 0"

with `p = 0`

have "p^k = 0" by auto

with `p^k dvd x`

have "0 dvd x" by auto

hence "x = 0" by auto

with `x ≠ 0`

show False by auto

qed

ultimately show ?thesis

by (auto simp add: is_unit_power_iff `¬ is_unit p`

)

next

case False

with `x ≠ 0`

`¬ is_unit p`

show ?thesis

by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)

qed

qed

lemma multiplicity_decomposeI:

assumes "x = p^k * x'" and "¬ p dvd x'" and "p ≠ 0"

shows "multiplicity p x = k"

proof (rule multiplicity_eqI)

from assms show "p^k dvd x" by auto

from assms have "x = x' * p^k" by (simp add: ac_simps)

with `¬ p dvd x'`

and `p ≠ 0`

show "¬ p^Suc k dvd x"

by simp

qed

lemma multiplicity_sum_lt:

assumes "multiplicity p a < multiplicity p b" "a ≠ 0" "b ≠ 0"

shows "multiplicity p (a + b) = multiplicity p a"

proof -

let ?vp = "multiplicity p"

have unit: "¬ is_unit p"

proof

assume "is_unit p"

then have "?vp a = 0" and "?vp b = 0" using multiplicity_unit_left by auto

with assms show False by auto

qed

from multiplicity_decompose' obtain a' where a': "a = p^?vp a * a'" "¬ p dvd a'"

using unit assms by metis

from multiplicity_decompose' obtain b' where b': "b = p^?vp b * b'"

using unit assms by metis

show "?vp (a + b) = ?vp a"

― ‹Use the rule here, after we obtained @{term a'} and @{term b'}, to avoid the

"Result contains obtained parameters" error›

proof (rule multiplicity_decomposeI)

let ?k = "?vp b - ?vp a"

from assms have k: "?k > 0" by simp

with b' have "b = p^?vp a * p^?k * b'"

by (simp flip: power_add)

with a' show *: "a + b = p^?vp a * (a' + p^?k * b')"

by (simp add: ac_simps distrib_left)

moreover show "¬ p dvd a' + p^?k * b'"

using a' k dvd_add_left_iff by auto

show "p ≠ 0" using assms by auto

qed

qed

corollary multiplicity_sum_min:

assumes "multiplicity p a ≠ multiplicity p b" "a ≠ 0" "b ≠ 0"

shows "multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)"

proof -

let ?vp = "multiplicity p"

from assms have "?vp a < ?vp b ∨ ?vp a > ?vp b"

by auto

then show ?thesis

by (metis assms multiplicity_sum_lt min.commute add_commute min.strict_order_iff)

qed

end

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

Hi Jakub,

thanks for contributing this.

I will put it into the distribution after the upcoming Isabelle2021 release.

Cheers,

Florian

signature.asc

Last updated: Dec 08 2021 at 08:24 UTC