## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] Some lemmas on factorial rings

#### Email Gateway (Jan 13 2021 at 23:21):

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  went without a
response. I'd appreciate someone looking into it.

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'"
with a' show *: "a + b = p^?vp a * (a' + p^?k * b')"

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

#### Email Gateway (Jan 14 2021 at 15:28):

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