section ‹Factorial (semi)rings›
theory Factorial_Ring
imports Main Primes "~~/src/HOL/Library/Multiset"
begin
context algebraic_semidom
begin
lemma dvd_mult_imp_div:
assumes "a * c dvd b"
shows "a dvd b div c"
proof (cases "c = 0")
case True then show ?thesis by simp
next
case False
from ‹a * c dvd b› obtain d where "b = a * c * d" ..
with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
qed
end
class factorial_semiring = normalization_semidom +
assumes finite_divisors: "a ≠ 0 ⟹ finite {b. b dvd a ∧ normalize b = b}"
fixes is_prime :: "'a ⇒ bool"
assumes not_is_prime_zero [simp]: "¬ is_prime 0"
and is_prime_not_unit: "is_prime p ⟹ ¬ is_unit p"
and no_prime_divisorsI2: "(⋀b. b dvd a ⟹ ¬ is_prime b) ⟹ is_unit a"
assumes is_primeI: "p ≠ 0 ⟹ ¬ is_unit p ⟹ (⋀a. a dvd p ⟹ ¬ is_unit a ⟹ p dvd a) ⟹ is_prime p"
and is_primeD: "is_prime p ⟹ p dvd a * b ⟹ p dvd a ∨ p dvd b"
begin
lemma not_is_prime_one [simp]:
"¬ is_prime 1"
by (auto dest: is_prime_not_unit)
lemma is_prime_not_zeroI:
assumes "is_prime p"
shows "p ≠ 0"
using assms by (auto intro: ccontr)
lemma is_prime_multD:
assumes "is_prime (a * b)"
shows "is_unit a ∨ is_unit b"
proof -
from assms have "a ≠ 0" "b ≠ 0" by auto
moreover from assms is_primeD [of "a * b"] have "a * b dvd a ∨ a * b dvd b"
by auto
ultimately show ?thesis
using dvd_times_left_cancel_iff [of a b 1]
dvd_times_right_cancel_iff [of b a 1]
by auto
qed
lemma is_primeD2:
assumes "is_prime p" and "a dvd p" and "¬ is_unit a"
shows "p dvd a"
proof -
from ‹a dvd p› obtain b where "p = a * b" ..
with ‹is_prime p› is_prime_multD ‹¬ is_unit a› have "is_unit b" by auto
with ‹p = a * b› show ?thesis
by (auto simp add: mult_unit_dvd_iff)
qed
lemma is_prime_mult_unit_left:
assumes "is_prime p"
and "is_unit a"
shows "is_prime (a * p)"
proof (rule is_primeI)
from assms show "a * p ≠ 0" "¬ is_unit (a * p)"
by (auto simp add: is_unit_mult_iff is_prime_not_unit)
show "a * p dvd b" if "b dvd a * p" "¬ is_unit b" for b
proof -
from that ‹is_unit a› have "b dvd p"
using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
with ‹is_prime p› ‹¬ is_unit b› have "p dvd b"
using is_primeD2 [of p b] by auto
with ‹is_unit a› show ?thesis
using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
qed
qed
lemma is_primeI2:
assumes "p ≠ 0"
assumes "¬ is_unit p"
assumes P: "⋀a b. p dvd a * b ⟹ p dvd a ∨ p dvd b"
shows "is_prime p"
using ‹p ≠ 0› ‹¬ is_unit p› proof (rule is_primeI)
fix a
assume "a dvd p"
then obtain b where "p = a * b" ..
with ‹p ≠ 0› have "b ≠ 0" by simp
moreover from ‹p = a * b› P have "p dvd a ∨ p dvd b" by auto
moreover assume "¬ is_unit a"
ultimately show "p dvd a"
using dvd_times_right_cancel_iff [of b a 1] ‹p = a * b› by auto
qed
lemma not_is_prime_divisorE:
assumes "a ≠ 0" and "¬ is_unit a" and "¬ is_prime a"
obtains b where "b dvd a" and "¬ is_unit b" and "¬ a dvd b"
proof -
from assms have "∃b. b dvd a ∧ ¬ is_unit b ∧ ¬ a dvd b"
by (auto intro: is_primeI)
with that show thesis by blast
qed
lemma is_prime_normalize_iff [simp]:
"is_prime (normalize p) ⟷ is_prime p" (is "?P ⟷ ?Q")
proof
assume ?Q show ?P
by (rule is_primeI) (insert ‹?Q›, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
next
assume ?P show ?Q
by (rule is_primeI)
(insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] ‹?P›, simp_all)
qed
lemma no_prime_divisorsI:
assumes "⋀b. b dvd a ⟹ normalize b = b ⟹ ¬ is_prime b"
shows "is_unit a"
proof (rule no_prime_divisorsI2)
fix b
assume "b dvd a"
then have "normalize b dvd a"
by simp
moreover have "normalize (normalize b) = normalize b"
by simp
ultimately have "¬ is_prime (normalize b)"
by (rule assms)
then show "¬ is_prime b"
by simp
qed
lemma prime_divisorE:
assumes "a ≠ 0" and "¬ is_unit a"
obtains p where "is_prime p" and "p dvd a"
using assms no_prime_divisorsI [of a] by blast
lemma is_prime_associated:
assumes "is_prime p" and "is_prime q" and "q dvd p"
shows "normalize q = normalize p"
using ‹q dvd p› proof (rule associatedI)
from ‹is_prime q› have "¬ is_unit q"
by (simp add: is_prime_not_unit)
with ‹is_prime p› ‹q dvd p› show "p dvd q"
by (blast intro: is_primeD2)
qed
lemma prime_dvd_mult_iff:
assumes "is_prime p"
shows "p dvd a * b ⟷ p dvd a ∨ p dvd b"
using assms by (auto dest: is_primeD)
lemma prime_dvd_msetprod:
assumes "is_prime p"
assumes dvd: "p dvd msetprod A"
obtains a where "a ∈# A" and "p dvd a"
proof -
from dvd have "∃a. a ∈# A ∧ p dvd a"
proof (induct A)
case empty then show ?case
using ‹is_prime p› by (simp add: is_prime_not_unit)
next
case (add A a)
then have "p dvd msetprod A * a" by simp
with ‹is_prime p› consider (A) "p dvd msetprod A" | (B) "p dvd a"
by (blast dest: is_primeD)
then show ?case proof cases
case B then show ?thesis by auto
next
case A
with add.hyps obtain b where "b ∈# A" "p dvd b"
by auto
then show ?thesis by auto
qed
qed
with that show thesis by blast
qed
lemma msetprod_eq_iff:
assumes "∀p∈set_mset P. is_prime p ∧ normalize p = p" and "∀p∈set_mset Q. is_prime p ∧ normalize p = p"
shows "msetprod P = msetprod Q ⟷ P = Q" (is "?R ⟷ ?S")
proof
assume ?S then show ?R by simp
next
assume ?R then show ?S using assms proof (induct P arbitrary: Q)
case empty then have Q: "msetprod Q = 1" by simp
have "Q = {#}"
proof (rule ccontr)
assume "Q ≠ {#}"
then obtain r R where "Q = R + {#r#}"
using multi_nonempty_split by blast
moreover with empty have "is_prime r" by simp
ultimately have "msetprod Q = msetprod R * r"
by simp
with Q have "msetprod R * r = 1"
by simp
then have "is_unit r"
by (metis local.dvd_triv_right)
with ‹is_prime r› show False by (simp add: is_prime_not_unit)
qed
then show ?case by simp
next
case (add P p)
then have "is_prime p" and "normalize p = p"
and "msetprod Q = msetprod P * p" and "p dvd msetprod Q"
by auto (metis local.dvd_triv_right)
with prime_dvd_msetprod
obtain q where "q ∈# Q" and "p dvd q"
by blast
with add.prems have "is_prime q" and "normalize q = q"
by simp_all
from ‹is_prime p› have "p ≠ 0"
by auto
from ‹is_prime q› ‹is_prime p› ‹p dvd q›
have "normalize p = normalize q"
by (rule is_prime_associated)
from ‹normalize p = p› ‹normalize q = q› have "p = q"
unfolding ‹normalize p = normalize q› by simp
with ‹q ∈# Q› have "p ∈# Q" by simp
have "msetprod P = msetprod (Q - {#p#})"
using ‹p ∈# Q› ‹p ≠ 0› ‹msetprod Q = msetprod P * p›
by (simp add: msetprod_minus)
then have "P = Q - {#p#}"
using add.prems(2-3)
by (auto intro: add.hyps dest: in_diffD)
with ‹p ∈# Q› show ?case by simp
qed
qed
lemma prime_dvd_power_iff:
assumes "is_prime p"
shows "p dvd a ^ n ⟷ p dvd a ∧ n > 0"
using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
lemma prime_power_dvd_multD:
assumes "is_prime p"
assumes "p ^ n dvd a * b" and "n > 0" and "¬ p dvd a"
shows "p ^ n dvd b"
using ‹p ^ n dvd a * b› and ‹n > 0› proof (induct n arbitrary: b)
case 0 then show ?case by simp
next
case (Suc n) show ?case
proof (cases "n = 0")
case True with Suc ‹is_prime p› ‹¬ p dvd a› show ?thesis
by (simp add: prime_dvd_mult_iff)
next
case False then have "n > 0" by simp
from ‹is_prime p› have "p ≠ 0" by auto
from Suc.prems have *: "p * p ^ n dvd a * b"
by simp
then have "p dvd a * b"
by (rule dvd_mult_left)
with Suc ‹is_prime p› ‹¬ p dvd a› have "p dvd b"
by (simp add: prime_dvd_mult_iff)
moreover def c ≡ "b div p"
ultimately have b: "b = p * c" by simp
with * have "p * p ^ n dvd p * (a * c)"
by (simp add: ac_simps)
with ‹p ≠ 0› have "p ^ n dvd a * c"
by simp
with Suc.hyps ‹n > 0› have "p ^ n dvd c"
by blast
with ‹p ≠ 0› show ?thesis
by (simp add: b)
qed
qed
lemma is_prime_inj_power:
assumes "is_prime p"
shows "inj (op ^ p)"
proof (rule injI, rule ccontr)
fix m n :: nat
have [simp]: "p ^ q = 1 ⟷ q = 0" (is "?P ⟷ ?Q") for q
proof
assume ?Q then show ?P by simp
next
assume ?P then have "is_unit (p ^ q)" by simp
with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
qed
have *: False if "p ^ m = p ^ n" and "m > n" for m n
proof -
from assms have "p ≠ 0"
by (rule is_prime_not_zeroI)
then have "p ^ n ≠ 0"
by (induct n) simp_all
from that have "m = n + (m - n)" and "m - n > 0" by arith+
then obtain q where "m = n + q" and "q > 0" ..
with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
with ‹p ^ n ≠ 0› have "p ^ q = 1"
using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
with ‹q > 0› show ?thesis by simp
qed
assume "m ≠ n"
then have "m > n ∨ m < n" by arith
moreover assume "p ^ m = p ^ n"
ultimately show False using * [of m n] * [of n m] by auto
qed
definition factorization :: "'a ⇒ 'a multiset option"
where "factorization a = (if a = 0 then None
else Some (setsum (λp. replicate_mset (Max {n. p ^ n dvd a}) p)
{p. p dvd a ∧ is_prime p ∧ normalize p = p}))"
lemma factorization_normalize [simp]:
"factorization (normalize a) = factorization a"
by (simp add: factorization_def)
lemma factorization_0 [simp]:
"factorization 0 = None"
by (simp add: factorization_def)
lemma factorization_eq_None_iff [simp]:
"factorization a = None ⟷ a = 0"
by (simp add: factorization_def)
lemma factorization_eq_Some_iff:
"factorization a = Some P ⟷
normalize a = msetprod P ∧ 0 ∉# P ∧ (∀p ∈ set_mset P. is_prime p ∧ normalize p = p)"
proof (cases "a = 0")
have [simp]: "0 = msetprod P ⟷ 0 ∈# P"
using msetprod_zero_iff [of P] by blast
case True
then show ?thesis by auto
next
case False
let ?prime_factors = "λa. {p. p dvd a ∧ is_prime p ∧ normalize p = p}"
have "?prime_factors a ⊆ {b. b dvd a ∧ normalize b = b}"
by auto
moreover from ‹a ≠ 0› have "finite {b. b dvd a ∧ normalize b = b}"
by (rule finite_divisors)
ultimately have "finite (?prime_factors a)"
by (rule finite_subset)
then show ?thesis using ‹a ≠ 0›
proof (induct "?prime_factors a" arbitrary: a P)
case empty then have
*: "{p. p dvd a ∧ is_prime p ∧ normalize p = p} = {}"
and "a ≠ 0"
by auto
from ‹a ≠ 0› have "factorization a = Some {#}"
by (simp only: factorization_def *) simp
from * have "normalize a = 1"
by (auto intro: is_unit_normalize no_prime_divisorsI)
show ?case (is "?lhs ⟷ ?rhs") proof
assume ?lhs with ‹factorization a = Some {#}› ‹normalize a = 1›
show ?rhs by simp
next
assume ?rhs have "P = {#}"
proof (rule ccontr)
assume "P ≠ {#}"
then obtain q Q where "P = Q + {#q#}"
using multi_nonempty_split by blast
with ‹?rhs› ‹normalize a = 1›
have "1 = q * msetprod Q" and "is_prime q"
by (simp_all add: ac_simps)
then have "is_unit q" by (auto intro: dvdI)
with ‹is_prime q› show False
using is_prime_not_unit by blast
qed
with ‹factorization a = Some {#}› show ?lhs by simp
qed
next
case (insert p F)
from ‹insert p F = ?prime_factors a›
have "?prime_factors a = insert p F"
by simp
then have "p dvd a" and "is_prime p" and "normalize p = p" and "p ≠ 0"
by (auto intro!: is_prime_not_zeroI)
def n ≡ "Max {n. p ^ n dvd a}"
then have "n > 0" and "p ^ n dvd a" and "¬ p ^ Suc n dvd a"
proof -
def N ≡ "{n. p ^ n dvd a}"
then have n_M: "n = Max N" by (simp add: n_def)
from is_prime_inj_power ‹is_prime p› have "inj (op ^ p)" .
then have "inj_on (op ^ p) U" for U
by (rule subset_inj_on) simp
moreover have "op ^ p ` N ⊆ {b. b dvd a ∧ normalize b = b}"
by (auto simp add: normalize_power ‹normalize p = p› N_def)
ultimately have "finite N"
by (rule inj_on_finite) (simp add: finite_divisors ‹a ≠ 0›)
from N_def ‹a ≠ 0› have "0 ∈ N" by (simp add: N_def)
then have "N ≠ {}" by blast
note * = ‹finite N› ‹N ≠ {}›
from N_def ‹p dvd a› have "1 ∈ N" by simp
with * have "Max N > 0"
by (auto simp add: Max_gr_iff)
then show "n > 0" by (simp add: n_M)
from * have "Max N ∈ N" by (rule Max_in)
then have "p ^ Max N dvd a" by (simp add: N_def)
then show "p ^ n dvd a" by (simp add: n_M)
from * have "∀n∈N. n ≤ Max N"
by (simp add: Max_le_iff [symmetric])
then have "p ^ Suc (Max N) dvd a ⟹ Suc (Max N) ≤ Max N"
by (rule bspec) (simp add: N_def)
then have "¬ p ^ Suc (Max N) dvd a"
by auto
then show "¬ p ^ Suc n dvd a"
by (simp add: n_M)
qed
def b ≡ "a div p ^ n"
with ‹p ^ n dvd a› have a: "a = p ^ n * b"
by simp
with ‹¬ p ^ Suc n dvd a› have "¬ p dvd b" and "b ≠ 0"
by (auto elim: dvdE simp add: ac_simps)
have "?prime_factors a = insert p (?prime_factors b)"
proof (rule set_eqI)
fix q
show "q ∈ ?prime_factors a ⟷ q ∈ insert p (?prime_factors b)"
using ‹is_prime p› ‹normalize p = p› ‹n > 0›
by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff)
(auto dest: is_prime_associated)
qed
with ‹¬ p dvd b› have "?prime_factors a - {p} = ?prime_factors b"
by auto
with insert.hyps have "F = ?prime_factors b"
by auto
then have "?prime_factors b = F"
by simp
with ‹?prime_factors a = insert p (?prime_factors b)› have "?prime_factors a = insert p F"
by simp
have equiv: "(∑p∈F. replicate_mset (Max {n. p ^ n dvd a}) p) =
(∑p∈F. replicate_mset (Max {n. p ^ n dvd b}) p)"
using refl proof (rule Groups_Big.setsum.cong)
fix q
assume "q ∈ F"
have "{n. q ^ n dvd a} = {n. q ^ n dvd b}"
proof -
have "q ^ m dvd a ⟷ q ^ m dvd b" (is "?R ⟷ ?S")
for m
proof (cases "m = 0")
case True then show ?thesis by simp
next
case False then have "m > 0" by simp
show ?thesis
proof
assume ?S then show ?R by (simp add: a)
next
assume ?R
then have *: "q ^ m dvd p ^ n * b" by (simp add: a)
from insert.hyps ‹q ∈ F›
have "is_prime q" "normalize q = q" "p ≠ q" "q dvd p ^ n * b"
by (auto simp add: a)
from ‹is_prime q› * ‹m > 0› show ?S
proof (rule prime_power_dvd_multD)
have "¬ q dvd p"
proof
assume "q dvd p"
with ‹is_prime q› ‹is_prime p› have "normalize q = normalize p"
by (blast intro: is_prime_associated)
with ‹normalize p = p› ‹normalize q = q› ‹p ≠ q› show False
by simp
qed
with ‹is_prime q› show "¬ q dvd p ^ n"
by (simp add: prime_dvd_power_iff)
qed
qed
qed
then show ?thesis by auto
qed
then show
"replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q"
by simp
qed
def Q ≡ "the (factorization b)"
with ‹b ≠ 0› have [simp]: "factorization b = Some Q"
by simp
from ‹a ≠ 0› have "factorization a =
Some (∑p∈?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)"
by (simp add: factorization_def)
also have "… =
Some (∑p∈insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)"
by (simp add: ‹?prime_factors a = insert p F›)
also have "… =
Some (replicate_mset n p + (∑p∈F. replicate_mset (Max {n. p ^ n dvd a}) p))"
using ‹finite F› ‹p ∉ F› n_def by simp
also have "… =
Some (replicate_mset n p + (∑p∈F. replicate_mset (Max {n. p ^ n dvd b}) p))"
using equiv by simp
also have "… = Some (replicate_mset n p + the (factorization b))"
using ‹b ≠ 0› by (simp add: factorization_def ‹?prime_factors a = insert p F› ‹?prime_factors b = F›)
finally have fact_a: "factorization a =
Some (replicate_mset n p + Q)"
by simp
moreover have "factorization b = Some Q ⟷
normalize b = msetprod Q ∧
0 ∉# Q ∧
(∀p∈#Q. is_prime p ∧ normalize p = p)"
using ‹F = ?prime_factors b› ‹b ≠ 0› by (rule insert.hyps)
ultimately have
norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and
prime_Q: "∀p∈set_mset Q. is_prime p ∧ normalize p = p"
by (simp_all add: a normalize_mult normalize_power ‹normalize p = p›)
show ?case (is "?lhs ⟷ ?rhs") proof
assume ?lhs with fact_a
have "P = replicate_mset n p + Q" by simp
with ‹n > 0› ‹is_prime p› ‹normalize p = p› prime_Q
show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI)
next
assume ?rhs
with ‹n > 0› ‹is_prime p› ‹normalize p = p› ‹n > 0› prime_Q
have "msetprod P = msetprod (replicate_mset n p + Q)"
and "∀p∈set_mset P. is_prime p ∧ normalize p = p"
and "∀p∈set_mset (replicate_mset n p + Q). is_prime p ∧ normalize p = p"
by (simp_all add: norm_a)
then have "P = replicate_mset n p + Q"
by (simp only: msetprod_eq_iff)
then show ?lhs
by (simp add: fact_a)
qed
qed
qed
lemma factorization_cases [case_names 0 factorization]:
assumes "0": "a = 0 ⟹ P"
assumes factorization: "⋀A. a ≠ 0 ⟹ factorization a = Some A ⟹ msetprod A = normalize a
⟹ 0 ∉# A ⟹ (⋀p. p ∈# A ⟹ normalize p = p) ⟹ (⋀p. p ∈# A ⟹ is_prime p) ⟹ P"
shows P
proof (cases "a = 0")
case True with 0 show P .
next
case False
then have "factorization a ≠ None" by simp
then obtain A where "factorization a = Some A" by blast
moreover from this have "msetprod A = normalize a"
"0 ∉# A" "⋀p. p ∈# A ⟹ normalize p = p" "⋀p. p ∈# A ⟹ is_prime p"
by (auto simp add: factorization_eq_Some_iff)
ultimately show P using ‹a ≠ 0› factorization by blast
qed
lemma factorizationE:
assumes "a ≠ 0"
obtains A u where "factorization a = Some A" "normalize a = msetprod A"
"0 ∉# A" "⋀p. p ∈# A ⟹ is_prime p" "⋀p. p ∈# A ⟹ normalize p = p"
using assms by (cases a rule: factorization_cases) simp_all
lemma prime_dvd_mset_prod_iff:
assumes "is_prime p" "normalize p = p" "⋀p. p ∈# A ⟹ is_prime p" "⋀p. p ∈# A ⟹ normalize p = p"
shows "p dvd msetprod A ⟷ p ∈# A"
using assms proof (induct A)
case empty then show ?case by (auto dest: is_prime_not_unit)
next
case (add A q) then show ?case
using is_prime_associated [of q p]
by (simp_all add: prime_dvd_mult_iff, safe, simp_all)
qed
end
class factorial_semiring_gcd = factorial_semiring + gcd +
assumes gcd_unfold: "gcd a b =
(if a = 0 then normalize b
else if b = 0 then normalize a
else msetprod (the (factorization a) #∩ the (factorization b)))"
and lcm_unfold: "lcm a b =
(if a = 0 ∨ b = 0 then 0
else msetprod (the (factorization a) #∪ the (factorization b)))"
begin
subclass semiring_gcd
proof
fix a b
have comm: "gcd a b = gcd b a" for a b
by (simp add: gcd_unfold ac_simps)
have "gcd a b dvd a" for a b
proof (cases a rule: factorization_cases)
case 0 then show ?thesis by simp
next
case (factorization A) note fact_A = this
then have non_zero: "⋀p. p ∈#A ⟹ p ≠ 0"
using normalize_0 not_is_prime_zero by blast
show ?thesis
proof (cases b rule: factorization_cases)
case 0 then show ?thesis by (simp add: gcd_unfold)
next
case (factorization B) note fact_B = this
have "msetprod (A #∩ B) dvd msetprod A"
using non_zero proof (induct B arbitrary: A)
case empty show ?case by simp
next
case (add B p) show ?case
proof (cases "p ∈# A")
case True then obtain C where "A = C + {#p#}"
by (metis insert_DiffM2)
moreover with True add have "p ≠ 0" and "⋀p. p ∈# C ⟹ p ≠ 0"
by auto
ultimately show ?thesis
using True add.hyps [of C]
by (simp add: inter_union_distrib_left [symmetric])
next
case False with add.prems add.hyps [of A] show ?thesis
by (simp add: inter_add_right1)
qed
qed
with fact_A fact_B show ?thesis by (simp add: gcd_unfold)
qed
qed
then have "gcd a b dvd a" and "gcd b a dvd b"
by simp_all
then show "gcd a b dvd a" and "gcd a b dvd b"
by (simp_all add: comm)
show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c
proof (cases "a = 0 ∨ b = 0 ∨ c = 0")
case True with that show ?thesis by (auto simp add: gcd_unfold)
next
case False then have "a ≠ 0" and "b ≠ 0" and "c ≠ 0"
by simp_all
then obtain A B C where fact:
"factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
and A: "0 ∉# A" "⋀p. p ∈# A ⟹ normalize p = p" "⋀p. p ∈# A ⟹ is_prime p"
and B: "0 ∉# B" "⋀p. p ∈# B ⟹ normalize p = p" "⋀p. p ∈# B ⟹ is_prime p"
and C: "0 ∉# C" "⋀p. p ∈# C ⟹ normalize p = p" "⋀p. p ∈# C ⟹ is_prime p"
by (blast elim!: factorizationE)
moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
by simp_all
ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B"
by simp_all
with A B C have "msetprod C dvd msetprod (A #∩ B)"
proof (induct C arbitrary: A B)
case empty then show ?case by simp
next
case add: (add C p)
from add.prems
have p: "p ≠ 0" "is_prime p" "normalize p = p" by auto
from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B"
by simp_all
then have "p dvd msetprod A" "p dvd msetprod B"
by (auto dest: dvd_mult_imp_div dvd_mult_right)
with p add.prems have "p ∈# A" "p ∈# B"
by (simp_all add: prime_dvd_mset_prod_iff)
then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'"
by (auto dest!: multi_member_split simp add: ac_simps)
with add.prems prems p have "msetprod C dvd msetprod (A' #∩ B')"
by (auto intro: add.hyps simp add: ac_simps)
with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #∩ ({#p#} + B'))"
by (simp add: inter_union_distrib_right [symmetric])
then show ?case by (simp add: ABp ac_simps)
qed
with ‹a ≠ 0› ‹b ≠ 0› that fact have "normalize c dvd gcd a b"
by (simp add: norm [symmetric] gcd_unfold fact)
then show ?thesis by simp
qed
show "normalize (gcd a b) = gcd a b"
apply (simp add: gcd_unfold)
apply safe
apply (rule normalized_msetprodI)
apply (auto elim: factorizationE)
done
show "lcm a b = normalize (a * b) div gcd a b"
by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult
union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union)
qed
end
instantiation nat :: factorial_semiring
begin
definition is_prime_nat :: "nat ⇒ bool"
where
"is_prime_nat p ⟷ (1 < p ∧ (∀n. n dvd p ⟶ n = 1 ∨ n = p))"
lemma is_prime_eq_prime:
"is_prime = prime"
by (simp add: fun_eq_iff prime_def is_prime_nat_def)
instance proof
show "¬ is_prime (0::nat)" by (simp add: is_prime_nat_def)
show "¬ is_unit p" if "is_prime p" for p :: nat
using that by (simp add: is_prime_nat_def)
next
fix p :: nat
assume "p ≠ 0" and "¬ is_unit p"
then have "p > 1" by simp
assume P: "⋀n. n dvd p ⟹ ¬ is_unit n ⟹ p dvd n"
have "n = 1" if "n dvd p" "n ≠ p" for n
proof (rule ccontr)
assume "n ≠ 1"
with that P have "p dvd n" by auto
with ‹n dvd p› have "n = p" by (rule dvd_antisym)
with that show False by simp
qed
with ‹p > 1› show "is_prime p" by (auto simp add: is_prime_nat_def)
next
fix p m n :: nat
assume "is_prime p"
then have "prime p" by (simp add: is_prime_eq_prime)
moreover assume "p dvd m * n"
ultimately show "p dvd m ∨ p dvd n"
by (rule prime_dvd_mult_nat)
next
fix n :: nat
show "is_unit n" if "⋀m. m dvd n ⟹ ¬ is_prime m"
using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
qed simp
end
instantiation int :: factorial_semiring
begin
definition is_prime_int :: "int ⇒ bool"
where
"is_prime_int p ⟷ is_prime (nat ¦p¦)"
lemma is_prime_int_iff [simp]:
"is_prime (int n) ⟷ is_prime n"
by (simp add: is_prime_int_def)
lemma is_prime_nat_abs_iff [simp]:
"is_prime (nat ¦k¦) ⟷ is_prime k"
by (simp add: is_prime_int_def)
instance proof
show "¬ is_prime (0::int)" by (simp add: is_prime_int_def)
show "¬ is_unit p" if "is_prime p" for p :: int
using that is_prime_not_unit [of "nat ¦p¦"] by simp
next
fix p :: int
assume P: "⋀k. k dvd p ⟹ ¬ is_unit k ⟹ p dvd k"
have "nat ¦p¦ dvd n" if "n dvd nat ¦p¦" and "n ≠ Suc 0" for n :: nat
proof -
from that have "int n dvd p" by (simp add: int_dvd_iff)
moreover from that have "¬ is_unit (int n)" by simp
ultimately have "p dvd int n" by (rule P)
with that have "p dvd int n" by auto
then show ?thesis by (simp add: dvd_int_iff)
qed
moreover assume "p ≠ 0" and "¬ is_unit p"
ultimately have "is_prime (nat ¦p¦)" by (intro is_primeI) auto
then show "is_prime p" by simp
next
fix p k l :: int
assume "is_prime p"
then have *: "is_prime (nat ¦p¦)" by simp
assume "p dvd k * l"
then have "nat ¦p¦ dvd nat ¦k * l¦"
by (simp add: dvd_int_unfold_dvd_nat)
then have "nat ¦p¦ dvd nat ¦k¦ * nat ¦l¦"
by (simp add: abs_mult nat_mult_distrib)
with * have "nat ¦p¦ dvd nat ¦k¦ ∨ nat ¦p¦ dvd nat ¦l¦"
using is_primeD [of "nat ¦p¦"] by auto
then show "p dvd k ∨ p dvd l"
by (simp add: dvd_int_unfold_dvd_nat)
next
fix k :: int
assume P: "⋀l. l dvd k ⟹ ¬ is_prime l"
have "is_unit (nat ¦k¦)"
proof (rule no_prime_divisorsI)
fix m
assume "m dvd nat ¦k¦"
then have "int m dvd k" by (simp add: int_dvd_iff)
then have "¬ is_prime (int m)" by (rule P)
then show "¬ is_prime m" by simp
qed
then show "is_unit k" by simp
qed simp
end
end