Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Some lemmas on factorial rings

view this post on Zulip Email Gateway (Jan 13 2021 at 23:21):

From: Jakub Kądziołka <>

I have proven a number of lemmas today that, I believe, should be
included in the distribution.

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.


context factorial_semiring

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

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
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
ultimately show ?thesis
by (auto simp add: is_unit_power_iff ¬ is_unit p)
case False
with x ≠ 0 ¬ is_unit p show ?thesis
by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)

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

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"
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

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

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)


view this post on Zulip Email Gateway (Jan 14 2021 at 15:28):

From: Florian Haftmann <>
Hi Jakub,

thanks for contributing this.

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


Last updated: Dec 08 2021 at 08:24 UTC