Email Gateway (Dec 22 2022 at 12:31): Email Gateway (Dec 22 2022 at 12:31):From: Peter Lammich <lammich@in.tum.de>
Hi List.
The lemma HOL-Computational_Algebra/Primes.not_prime_eq_prod_nat is
stated as follows:
lemma not_prime_eq_prod_nat:
assumes "m > 1" "¬ prime (m::nat)"
shows "∃n k. n = m * k ∧ 1 < m ∧ m < n ∧ 1 < k ∧ k < n"
using assms irreducible_altdef[of m]
by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
I do not understand how that is usable. To me it looks like the sequence
of factors got messed up! As stated, the lemma is almost trivial, and
the second assumption is not needed:
lemma not_prime_eq_prod_nat:
fixes m :: nat
assumes "m > 1" ("¬ prime (m::nat)")
shows "∃n k. n = m * k ∧ 1 < m ∧ m < n ∧ 1 < k ∧ k < n"
using assms
by auto
Unsurprisingly, the lemma is not used in Isabelle nor AFP. I assume that
the lemma was meant as:
lemma not_prime_eq_prod_nat:
assumes "m > 1" "¬ prime (m::nat)"
shows "∃n k. m = n * k ∧ 1 < n ∧ n < m ∧ 1 < k ∧ k < m"
proof -
from assms obtain a b where "1<a" "1<b" "a<m" "b<m" and "m=a*b"
using nat_neq_iff prime_nat_iff by fastforce
thus ?thesis by blast
qed
Last updated: Apr 26 2024 at 01:06 UTC