Email Gateway (Jan 13 2021 at 23:21): Email Gateway (Jan 13 2021 at 23:21):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
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: Jul 15 2022 at 23:21 UTC