--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Tue Jan 21 11:02:27 2020 +0100
@@ -67,7 +67,7 @@
by (simp add: gcd.simps [of b 0] gcd.simps [of b a])
qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- where "lcm a b = normalize (a * b) div gcd a b"
+ where "lcm a b = normalize (a * b div gcd a b)"
qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment> \<open>Somewhat complicated definition of Lcm that has the advantage of working
for infinite sets as well\<close>
@@ -106,7 +106,7 @@
by (induct a b rule: eucl_induct)
(simp_all add: local.gcd_0 local.gcd_mod)
next
- show "lcm a b = normalize (a * b) div gcd a b" for a b
+ show "lcm a b = normalize (a * b div gcd a b)" for a b
by (fact local.lcm_def)
qed
@@ -234,31 +234,30 @@
from y have x: "x = y * z" by (simp add: z_def)
with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
have normalized_factors_product:
- "{p. p dvd a * b \<and> normalize p = p} =
- (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
+ "{p. p dvd a * b \<and> normalize p = p} \<subseteq>
+ (\<lambda>(x,y). normalize (x * y)) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
for a b
proof safe
fix p assume p: "p dvd a * b" "normalize p = p"
from p(1) obtain x y where xy: "p = x * y" "x dvd a" "y dvd b"
by (rule dvd_productE)
define x' y' where "x' = normalize x" and "y' = normalize y"
- have "p = x' * y'"
- by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
- moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b"
- by (simp_all add: x'_def y'_def)
- ultimately show "p \<in> (\<lambda>(x, y). x * y) `
- ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
- by blast
- qed (auto simp: normalize_mult mult_dvd_mono)
+ have "p = normalize (x' * y')"
+ using p by (simp add: xy x'_def y'_def)
+ moreover have "x' dvd a \<and> normalize x' = x'" and "y' dvd b \<and> normalize y' = y'"
+ using xy by (auto simp: x'_def y'_def)
+ ultimately show "p \<in> (\<lambda>(x, y). normalize (x * y)) `
+ ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" by fast
+ qed
from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
- have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
+ have "?fctrs x \<subseteq> (\<lambda>(p,p'). normalize (p * p')) ` (?fctrs y \<times> ?fctrs z)"
by (subst x) (rule normalized_factors_product)
- also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
+ moreover have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
- hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
+ hence "finite ((\<lambda>(p,p'). normalize (p * p')) ` (?fctrs y \<times> ?fctrs z))"
by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
(auto simp: x)
- finally show ?thesis .
+ ultimately show ?thesis by (rule finite_subset)
qed
qed
next
@@ -566,6 +565,26 @@
end
+class normalization_euclidean_semiring_multiplicative =
+ normalization_euclidean_semiring + normalization_semidom_multiplicative
+begin
+
+subclass factorial_semiring_multiplicative ..
+
+end
+
+class field_gcd =
+ field + unique_euclidean_ring + euclidean_ring_gcd + normalization_semidom_multiplicative
+begin
+
+subclass normalization_euclidean_semiring_multiplicative ..
+
+subclass normalization_euclidean_semiring ..
+
+subclass semiring_gcd_mult_normalize ..
+
+end
+
subsection \<open>Typical instances\<close>
@@ -603,6 +622,8 @@
by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
qed
+instance nat :: normalization_euclidean_semiring_multiplicative ..
+
lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
unfolding One_nat_def [symmetric] using prime_factorization_1 .
@@ -652,4 +673,6 @@
by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
qed
+instance int :: normalization_euclidean_semiring_multiplicative ..
+
end
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Tue Jan 21 11:02:27 2020 +0100
@@ -35,6 +35,20 @@
lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
by (simp add: irreducible_def)
+lemma irreducible_mono:
+ assumes irr: "irreducible b" and "a dvd b" "\<not>a dvd 1"
+ shows "irreducible a"
+proof (rule irreducibleI)
+ fix c d assume "a = c * d"
+ from assms obtain k where [simp]: "b = a * k" by auto
+ from \<open>a = c * d\<close> have "b = c * d * k"
+ by simp
+ hence "c dvd 1 \<or> (d * k) dvd 1"
+ using irreducibleD[OF irr, of c "d * k"] by (auto simp: mult.assoc)
+ thus "c dvd 1 \<or> d dvd 1"
+ by auto
+qed (use assms in \<open>auto simp: irreducible_def\<close>)
+
definition prime_elem :: "'a \<Rightarrow> bool" where
"prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
@@ -83,6 +97,82 @@
end
+
+lemma (in normalization_semidom) irreducible_cong:
+ assumes "normalize a = normalize b"
+ shows "irreducible a \<longleftrightarrow> irreducible b"
+proof (cases "a = 0 \<or> a dvd 1")
+ case True
+ hence "\<not>irreducible a" by (auto simp: irreducible_def)
+ from True have "normalize a = 0 \<or> normalize a dvd 1"
+ by auto
+ also note assms
+ finally have "b = 0 \<or> b dvd 1" by simp
+ hence "\<not>irreducible b" by (auto simp: irreducible_def)
+ with \<open>\<not>irreducible a\<close> show ?thesis by simp
+next
+ case False
+ hence b: "b \<noteq> 0" "\<not>is_unit b" using assms
+ by (auto simp: is_unit_normalize[of b])
+ show ?thesis
+ proof
+ assume "irreducible a"
+ thus "irreducible b"
+ by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD2\<close>)
+ next
+ assume "irreducible b"
+ thus "irreducible a"
+ by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD1\<close>)
+ qed
+qed
+
+lemma (in normalization_semidom) associatedE1:
+ assumes "normalize a = normalize b"
+ obtains u where "is_unit u" "a = u * b"
+proof (cases "a = 0")
+ case [simp]: False
+ from assms have [simp]: "b \<noteq> 0" by auto
+ show ?thesis
+ proof (rule that)
+ show "is_unit (unit_factor a div unit_factor b)"
+ by auto
+ have "unit_factor a div unit_factor b * b = unit_factor a * (b div unit_factor b)"
+ using \<open>b \<noteq> 0\<close> unit_div_commute unit_div_mult_swap unit_factor_is_unit by metis
+ also have "b div unit_factor b = normalize b" by simp
+ finally show "a = unit_factor a div unit_factor b * b"
+ by (metis assms unit_factor_mult_normalize)
+ qed
+next
+ case [simp]: True
+ hence [simp]: "b = 0"
+ using assms[symmetric] by auto
+ show ?thesis
+ by (intro that[of 1]) auto
+qed
+
+lemma (in normalization_semidom) associatedE2:
+ assumes "normalize a = normalize b"
+ obtains u where "is_unit u" "b = u * a"
+proof -
+ from assms have "normalize b = normalize a"
+ by simp
+ then obtain u where "is_unit u" "b = u * a"
+ by (elim associatedE1)
+ thus ?thesis using that by blast
+qed
+
+
+(* TODO Move *)
+lemma (in normalization_semidom) normalize_power_normalize:
+ "normalize (normalize x ^ n) = normalize (x ^ n)"
+proof (induction n)
+ case (Suc n)
+ have "normalize (normalize x ^ Suc n) = normalize (x * normalize (normalize x ^ n))"
+ by simp
+ also note Suc.IH
+ finally show ?case by simp
+qed auto
+
context algebraic_semidom
begin
@@ -506,15 +596,6 @@
thus ?case by (simp add: B)
qed
-lemma normalize_prod_mset_primes:
- "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
-proof (induction A)
- case (add p A)
- hence "prime p" by simp
- hence "normalize p = p" by simp
- with add show ?case by (simp add: normalize_mult)
-qed simp_all
-
lemma prod_mset_dvd_prod_mset_primes_iff:
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
shows "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
@@ -647,7 +728,7 @@
class factorial_semiring = normalization_semidom +
assumes prime_factorization_exists:
- "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
+ "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize x"
text \<open>Alternative characterization\<close>
@@ -655,7 +736,7 @@
assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
assumes "x \<noteq> 0"
- shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
+ shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize x"
using \<open>x \<noteq> 0\<close>
proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
case (less a)
@@ -683,7 +764,7 @@
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
by (rule psubset_card_mono)
moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
- ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
+ ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize b"
by (intro less) auto
then guess A .. note A = this
@@ -702,11 +783,22 @@
ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
by (rule psubset_card_mono)
- with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
+ with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize c"
by (intro less) auto
then guess B .. note B = this
- from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
+ show ?thesis
+ proof (rule exI[of _ "A + B"]; safe)
+ have "normalize (prod_mset (A + B)) =
+ normalize (normalize (prod_mset A) * normalize (prod_mset B))"
+ by simp
+ also have "\<dots> = normalize (b * c)"
+ by (simp only: A B) auto
+ also have "b * c = a"
+ using c by simp
+ finally show "normalize (prod_mset (A + B)) = normalize a" .
+ next
+ qed (use A B in auto)
qed
qed
qed
@@ -724,15 +816,15 @@
lemma prime_factorization_exists':
assumes "x \<noteq> 0"
- obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x"
+ obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "normalize (prod_mset A) = normalize x"
proof -
from prime_factorization_exists[OF assms] obtain A
- where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast
+ where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "normalize (prod_mset A) = normalize x" by blast
define A' where "A' = image_mset normalize A"
- have "prod_mset A' = normalize (prod_mset A)"
- by (simp add: A'_def normalize_prod_mset)
+ have "normalize (prod_mset A') = normalize (prod_mset A)"
+ by (simp add: A'_def normalize_prod_mset_normalize)
also note A(2)
- finally have "prod_mset A' = normalize x" by simp
+ finally have "normalize (prod_mset A') = normalize x" by simp
moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
ultimately show ?thesis by (intro that[of A']) blast
qed
@@ -749,9 +841,19 @@
hence "a \<noteq> 0" "b \<noteq> 0" by blast+
note nz = \<open>x \<noteq> 0\<close> this
from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
- from assms ABC have "irreducible (prod_mset A)" by simp
- from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
- show ?thesis by (simp add: normalize_mult [symmetric])
+
+ have "irreducible (prod_mset A)"
+ by (subst irreducible_cong[OF ABC(2)]) fact
+ moreover have "normalize (prod_mset A) dvd
+ normalize (normalize (prod_mset B) * normalize (prod_mset C))"
+ unfolding ABC using dvd by simp
+ hence "prod_mset A dvd prod_mset B * prod_mset C"
+ unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
+ ultimately have "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C"
+ by (intro prod_mset_primes_irreducible_imp_prime) (use ABC in auto)
+ hence "normalize (prod_mset A) dvd normalize (prod_mset B) \<or>
+ normalize (prod_mset A) dvd normalize (prod_mset C)" by simp
+ thus ?thesis unfolding ABC by simp
qed auto
qed (insert assms, simp_all add: irreducible_def)
@@ -768,7 +870,13 @@
from nz[THEN prime_factorization_exists'] guess A B . note AB = this
from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
- show ?thesis by (simp add: normalize_power [symmetric])
+ have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp
+ also have "{n. prod_mset A ^ n dvd prod_mset B} =
+ {n. normalize (normalize (prod_mset A) ^ n) dvd normalize (prod_mset B)}"
+ unfolding normalize_power_normalize by simp
+ also have "\<dots> = {n. x ^ n dvd y}"
+ unfolding AB unfolding normalize_power_normalize by simp
+ finally show ?thesis .
qed
lemma finite_prime_divisors:
@@ -780,8 +888,11 @@
proof safe
fix p assume p: "prime p" and dvd: "p dvd x"
from dvd have "p dvd normalize x" by simp
- also from A have "normalize x = prod_mset A" by simp
- finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff)
+ also from A have "normalize x = normalize (prod_mset A)" by simp
+ finally have "p dvd prod_mset A"
+ by simp
+ thus "p \<in># A" using p A
+ by (subst (asm) prime_dvd_prod_mset_primes_iff)
qed
moreover have "finite (set_mset A)" by simp
ultimately show ?thesis by (rule finite_subset)
@@ -797,8 +908,9 @@
from prime_factorization_exists'[OF assms(1)] guess A . note A = this
moreover from A and assms have "A \<noteq> {#}" by auto
then obtain x where "x \<in># A" by blast
- with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset)
- with A have "x dvd a" by simp
+ with A(1) have *: "x dvd normalize (prod_mset A)" "prime x"
+ by (auto simp: dvd_prod_mset)
+ hence "x dvd a" unfolding A by simp
with * show ?thesis by blast
qed
@@ -808,15 +920,18 @@
proof (cases "x = 0")
case False
from prime_factorization_exists'[OF this] guess A . note A = this
- from A(1) have "P (unit_factor x * prod_mset A)"
+ from A obtain u where u: "is_unit u" "x = u * prod_mset A"
+ by (elim associatedE2)
+
+ from A(1) have "P (u * prod_mset A)"
proof (induction A)
case (add p A)
from add.prems have "prime p" by simp
- moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all
- ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3))
+ moreover from add.prems have "P (u * prod_mset A)" by (intro add.IH) simp_all
+ ultimately have "P (p * (u * prod_mset A))" by (rule assms(3))
thus ?case by (simp add: mult_ac)
- qed (simp_all add: assms False)
- with A show ?thesis by simp
+ qed (simp_all add: assms False u)
+ with A u show ?thesis by simp
qed (simp_all add: assms(1))
lemma no_prime_divisors_imp_unit:
@@ -1213,13 +1328,19 @@
qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
qed
-lemma prod_mset_prime_factorization:
+lemma prod_mset_prime_factorization_weak:
assumes "x \<noteq> 0"
- shows "prod_mset (prime_factorization x) = normalize x"
+ shows "normalize (prod_mset (prime_factorization x)) = normalize x"
using assms
- by (induction x rule: prime_divisors_induct)
- (simp_all add: prime_factorization_unit prime_factorization_times_prime
- is_unit_normalize normalize_mult)
+proof (induction x rule: prime_divisors_induct)
+ case (factor p x)
+ have "normalize (prod_mset (prime_factorization (p * x))) =
+ normalize (p * normalize (prod_mset (prime_factorization x)))"
+ using factor.prems factor.hyps by (simp add: prime_factorization_times_prime)
+ also have "normalize (prod_mset (prime_factorization x)) = normalize x"
+ by (rule factor.IH) (use factor in auto)
+ finally show ?case by simp
+qed (auto simp: prime_factorization_unit is_unit_normalize)
lemma in_prime_factors_iff:
"p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
@@ -1287,28 +1408,43 @@
proof
assume "prime_factorization x = prime_factorization y"
hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
- with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
+ hence "normalize (prod_mset (prime_factorization x)) =
+ normalize (prod_mset (prime_factorization y))"
+ by (simp only: )
+ with assms show "normalize x = normalize y"
+ by (simp add: prod_mset_prime_factorization_weak)
qed (rule prime_factorization_cong)
-lemma prime_factorization_eqI:
+lemma prime_factorization_normalize [simp]:
+ "prime_factorization (normalize x) = prime_factorization x"
+ by (cases "x = 0", simp, subst prime_factorization_unique) auto
+
+lemma prime_factorization_eqI_strong:
assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n"
shows "prime_factorization n = P"
using prime_factorization_prod_mset_primes[of P] assms by simp
+lemma prime_factorization_eqI:
+ assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "normalize (prod_mset P) = normalize n"
+ shows "prime_factorization n = P"
+proof -
+ have "P = prime_factorization (normalize (prod_mset P))"
+ using prime_factorization_prod_mset_primes[of P] assms(1) by simp
+ with assms(2) show ?thesis by simp
+qed
+
lemma prime_factorization_mult:
assumes "x \<noteq> 0" "y \<noteq> 0"
shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
proof -
- have "prime_factorization (prod_mset (prime_factorization (x * y))) =
- prime_factorization (prod_mset (prime_factorization x + prime_factorization y))"
- by (simp add: prod_mset_prime_factorization assms normalize_mult)
- also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
- prime_factorization (x * y)"
- by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime)
- also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
- prime_factorization x + prime_factorization y"
- by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime)
- finally show ?thesis .
+ have "normalize (prod_mset (prime_factorization x) * prod_mset (prime_factorization y)) =
+ normalize (normalize (prod_mset (prime_factorization x)) *
+ normalize (prod_mset (prime_factorization y)))"
+ by (simp only: normalize_mult_normalize_left normalize_mult_normalize_right)
+ also have "\<dots> = normalize (x * y)"
+ by (subst (1 2) prod_mset_prime_factorization_weak) (use assms in auto)
+ finally show ?thesis
+ by (intro prime_factorization_eqI) auto
qed
lemma prime_factorization_prod:
@@ -1367,15 +1503,13 @@
by (induction n)
(simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
-lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
- by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
-
lemma prime_factorization_subset_iff_dvd:
assumes [simp]: "x \<noteq> 0" "y \<noteq> 0"
shows "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y"
proof -
- have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
- by (simp add: prod_mset_prime_factorization)
+ have "x dvd y \<longleftrightarrow>
+ normalize (prod_mset (prime_factorization x)) dvd normalize (prod_mset (prime_factorization y))"
+ using assms by (subst (1 2) prod_mset_prime_factorization_weak) auto
also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd)
finally show ?thesis ..
@@ -1403,63 +1537,6 @@
"prime p \<Longrightarrow> prime_factors p = {p}"
by (drule prime_factorization_prime) simp
-lemma prod_prime_factors:
- assumes "x \<noteq> 0"
- shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
-proof -
- have "normalize x = prod_mset (prime_factorization x)"
- by (simp add: prod_mset_prime_factorization assms)
- also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
- by (subst prod_mset_multiplicity) simp_all
- also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
- by (intro prod.cong)
- (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
- finally show ?thesis ..
-qed
-
-lemma prime_factorization_unique'':
- assumes S_eq: "S = {p. 0 < f p}"
- and "finite S"
- and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
- shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
-proof
- define A where "A = Abs_multiset f"
- from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
- with S(2) have nz: "n \<noteq> 0" by auto
- from S_eq \<open>finite S\<close> have count_A: "count A = f"
- unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
- from S_eq count_A have set_mset_A: "set_mset A = S"
- by (simp only: set_mset_def)
- from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
- also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
- also from nz have "normalize n = prod_mset (prime_factorization n)"
- by (simp add: prod_mset_prime_factorization)
- finally have "prime_factorization (prod_mset A) =
- prime_factorization (prod_mset (prime_factorization n))" by simp
- also from S(1) have "prime_factorization (prod_mset A) = A"
- by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
- also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
- by (intro prime_factorization_prod_mset_primes) auto
- finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
-
- show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
- proof safe
- fix p :: 'a assume p: "prime p"
- have "multiplicity p n = multiplicity p (normalize n)" by simp
- also have "normalize n = prod_mset A"
- by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
- also from p set_mset_A S(1)
- have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
- by (intro prime_elem_multiplicity_prod_mset_distrib) auto
- also from S(1) p
- have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
- by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
- also have "sum_mset \<dots> = f p"
- by (simp add: semiring_1_class.sum_mset_delta' count_A)
- finally show "f p = multiplicity p n" ..
- qed
-qed
-
lemma prime_factors_product:
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
by (simp add: prime_factorization_mult)
@@ -1502,6 +1579,20 @@
finally show ?thesis .
qed
+lemma prime_factorization_unique'':
+ assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "normalize (\<Prod>i \<in># M. i) = normalize (\<Prod>i \<in># N. i)"
+ shows "M = N"
+proof -
+ have "prime_factorization (normalize (\<Prod>i \<in># M. i)) =
+ prime_factorization (normalize (\<Prod>i \<in># N. i))"
+ by (simp only: assms)
+ also from assms have "prime_factorization (normalize (\<Prod>i \<in># M. i)) = M"
+ by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all
+ also from assms have "prime_factorization (normalize (\<Prod>i \<in># N. i)) = N"
+ by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all
+ finally show ?thesis .
+qed
+
lemma multiplicity_cong:
"(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
by (simp add: multiplicity_def)
@@ -1526,26 +1617,30 @@
with assms[of P] assms[of Q] PQ show "P = Q" by simp
qed
-lemma divides_primepow:
+lemma divides_primepow_weak:
assumes "prime p" and "a dvd p ^ n"
- obtains m where "m \<le> n" and "normalize a = p ^ m"
+ obtains m where "m \<le> n" and "normalize a = normalize (p ^ m)"
proof -
from assms have "a \<noteq> 0"
by auto
with assms
- have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
- by (simp add: prod_mset_prime_factorization)
+ have "normalize (prod_mset (prime_factorization a)) dvd
+ normalize (prod_mset (prime_factorization (p ^ n)))"
+ by (subst (1 2) prod_mset_prime_factorization_weak) auto
then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
with assms have "prime_factorization a \<subseteq># replicate_mset n p"
by (simp add: prime_factorization_prime_power)
then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
by (rule msubseteq_replicate_msetE)
- then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
+ then have *: "normalize (prod_mset (prime_factorization a)) =
+ normalize (prod_mset (replicate_mset m p))" by metis
+ also have "normalize (prod_mset (prime_factorization a)) = normalize a"
+ using \<open>a \<noteq> 0\<close> by (simp add: prod_mset_prime_factorization_weak)
+ also have "prod_mset (replicate_mset m p) = p ^ m"
by simp
- with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
- by (simp add: prod_mset_prime_factorization)
- with \<open>m \<le> n\<close> show thesis ..
+ finally show ?thesis using \<open>m \<le> n\<close>
+ by (intro that[of m])
qed
lemma divide_out_primepow_ex:
@@ -1568,37 +1663,24 @@
obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms
prime_factorsI by metis
-
-lemma Ex_other_prime_factor:
- assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
- shows "\<exists>q\<in>prime_factors n. q \<noteq> p"
-proof (rule ccontr)
- assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
- have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
- using assms(1) by (intro prod_prime_factors [symmetric]) auto
- also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
- using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
- finally have "normalize n = p ^ multiplicity p n" by auto
- with assms show False by auto
-qed
subsection \<open>GCD and LCM computation with unique factorizations\<close>
definition "gcd_factorial a b = (if a = 0 then normalize b
else if b = 0 then normalize a
- else prod_mset (prime_factorization a \<inter># prime_factorization b))"
+ else normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)))"
definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
- else prod_mset (prime_factorization a \<union># prime_factorization b))"
+ else normalize (prod_mset (prime_factorization a \<union># prime_factorization b)))"
definition "Gcd_factorial A =
- (if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))"
+ (if A \<subseteq> {0} then 0 else normalize (prod_mset (Inf (prime_factorization ` (A - {0})))))"
definition "Lcm_factorial A =
(if A = {} then 1
else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then
- prod_mset (Sup (prime_factorization ` A))
+ normalize (prod_mset (Sup (prime_factorization ` A)))
else
0)"
@@ -1672,13 +1754,11 @@
lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b"
by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1)
-lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b"
-proof -
- have "normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)) =
- prod_mset (prime_factorization a \<inter># prime_factorization b)"
- by (intro normalize_prod_mset_primes) auto
- thus ?thesis by (simp add: gcd_factorial_def)
-qed
+lemma normalize_gcd_factorial [simp]: "normalize (gcd_factorial a b) = gcd_factorial a b"
+ by (simp add: gcd_factorial_def)
+
+lemma normalize_lcm_factorial [simp]: "normalize (lcm_factorial a b) = lcm_factorial a b"
+ by (simp add: lcm_factorial_def)
lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c
proof (cases "a = 0 \<or> b = 0")
@@ -1695,33 +1775,39 @@
qed (auto simp: gcd_factorial_def that)
lemma lcm_factorial_gcd_factorial:
- "lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b
+ "lcm_factorial a b = normalize (a * b div gcd_factorial a b)" for a b
proof (cases "a = 0 \<or> b = 0")
case False
let ?p = "prime_factorization"
- from False have "prod_mset (?p (a * b)) div gcd_factorial a b =
- prod_mset (?p a + ?p b - ?p a \<inter># ?p b)"
- by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def
- prime_factorization_mult subset_mset.le_infI1)
- also from False have "prod_mset (?p (a * b)) = normalize (a * b)"
- by (intro prod_mset_prime_factorization) simp_all
- also from False have "prod_mset (?p a + ?p b - ?p a \<inter># ?p b) = lcm_factorial a b"
- by (simp add: union_diff_inter_eq_sup lcm_factorial_def)
- finally show ?thesis ..
+ have 1: "normalize x * normalize y dvd z \<longleftrightarrow> x * y dvd z" for x y z :: 'a
+ proof -
+ have "normalize (normalize x * normalize y) dvd z \<longleftrightarrow> x * y dvd z"
+ unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
+ thus ?thesis unfolding normalize_dvd_iff by simp
+ qed
+
+ have "?p (a * b) = (?p a \<union># ?p b) + (?p a \<inter># ?p b)"
+ using False by (subst prime_factorization_mult) (auto intro!: multiset_eqI)
+ hence "normalize (prod_mset (?p (a * b))) =
+ normalize (prod_mset ((?p a \<union># ?p b) + (?p a \<inter># ?p b)))"
+ by (simp only:)
+ hence *: "normalize (a * b) = normalize (lcm_factorial a b * gcd_factorial a b)" using False
+ by (subst (asm) prod_mset_prime_factorization_weak)
+ (auto simp: lcm_factorial_def gcd_factorial_def)
+
+ have [simp]: "gcd_factorial a b dvd a * b" "lcm_factorial a b dvd a * b"
+ using associatedD2[OF *] by auto
+ from False have [simp]: "gcd_factorial a b \<noteq> 0" "lcm_factorial a b \<noteq> 0"
+ by (auto simp: gcd_factorial_def lcm_factorial_def)
+
+ show ?thesis
+ by (rule associated_eqI)
+ (use * in \<open>auto simp: dvd_div_iff_mult div_dvd_iff_mult dest: associatedD1 associatedD2\<close>)
qed (auto simp: lcm_factorial_def)
lemma normalize_Gcd_factorial:
"normalize (Gcd_factorial A) = Gcd_factorial A"
-proof (cases "A \<subseteq> {0}")
- case False
- then obtain x where "x \<in> A" "x \<noteq> 0" by blast
- hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
- by (intro subset_mset.cInf_lower) auto
- hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
- using that by (auto dest: mset_subset_eqD)
- with False show ?thesis
- by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
-qed (simp_all add: Gcd_factorial_def)
+ by (simp add: Gcd_factorial_def)
lemma Gcd_factorial_eq_0_iff:
"Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}"
@@ -1761,14 +1847,7 @@
lemma normalize_Lcm_factorial:
"normalize (Lcm_factorial A) = Lcm_factorial A"
-proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
- case True
- hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
- prod_mset (Sup (prime_factorization ` A))"
- by (intro normalize_prod_mset_primes)
- (auto simp: in_Sup_multiset_iff)
- with True show ?thesis by (simp add: Lcm_factorial_def)
-qed (auto simp: Lcm_factorial_def)
+ by (simp add: Lcm_factorial_def)
lemma Lcm_factorial_eq_0_iff:
"Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)"
@@ -1870,21 +1949,23 @@
lemma
assumes "x \<noteq> 0" "y \<noteq> 0"
shows gcd_eq_factorial':
- "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
+ "gcd x y = normalize (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
and lcm_eq_factorial':
- "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
+ "lcm x y = normalize (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
proof -
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
also have "\<dots> = ?rhs1"
by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
- count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
+ count_prime_factorization_prime
+ intro!: arg_cong[of _ _ normalize] dest: in_prime_factors_imp_prime intro!: prod.cong)
finally show "gcd x y = ?rhs1" .
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
also have "\<dots> = ?rhs2"
by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
- count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
+ count_prime_factorization_prime intro!: arg_cong[of _ _ normalize]
+ dest: in_prime_factors_imp_prime intro!: prod.cong)
finally show "lcm x y = ?rhs2" .
qed
@@ -1944,4 +2025,107 @@
end
+
+class factorial_semiring_multiplicative =
+ factorial_semiring + normalization_semidom_multiplicative
+begin
+
+lemma normalize_prod_mset_primes:
+ "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
+proof (induction A)
+ case (add p A)
+ hence "prime p" by simp
+ hence "normalize p = p" by simp
+ with add show ?case by (simp add: normalize_mult)
+qed simp_all
+
+lemma prod_mset_prime_factorization:
+ assumes "x \<noteq> 0"
+ shows "prod_mset (prime_factorization x) = normalize x"
+ using assms
+ by (induction x rule: prime_divisors_induct)
+ (simp_all add: prime_factorization_unit prime_factorization_times_prime
+ is_unit_normalize normalize_mult)
+
+lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
+ by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
+
+lemma prod_prime_factors:
+ assumes "x \<noteq> 0"
+ shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
+proof -
+ have "normalize x = prod_mset (prime_factorization x)"
+ by (simp add: prod_mset_prime_factorization assms)
+ also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
+ by (subst prod_mset_multiplicity) simp_all
+ also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
+ by (intro prod.cong)
+ (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
+ finally show ?thesis ..
+qed
+
+lemma prime_factorization_unique'':
+ assumes S_eq: "S = {p. 0 < f p}"
+ and "finite S"
+ and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
+proof
+ define A where "A = Abs_multiset f"
+ from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
+ with S(2) have nz: "n \<noteq> 0" by auto
+ from S_eq \<open>finite S\<close> have count_A: "count A = f"
+ unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+ from S_eq count_A have set_mset_A: "set_mset A = S"
+ by (simp only: set_mset_def)
+ from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
+ also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
+ also from nz have "normalize n = prod_mset (prime_factorization n)"
+ by (simp add: prod_mset_prime_factorization)
+ finally have "prime_factorization (prod_mset A) =
+ prime_factorization (prod_mset (prime_factorization n))" by simp
+ also from S(1) have "prime_factorization (prod_mset A) = A"
+ by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
+ also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
+ by (intro prime_factorization_prod_mset_primes) auto
+ finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
+
+ show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
+ proof safe
+ fix p :: 'a assume p: "prime p"
+ have "multiplicity p n = multiplicity p (normalize n)" by simp
+ also have "normalize n = prod_mset A"
+ by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
+ also from p set_mset_A S(1)
+ have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
+ by (intro prime_elem_multiplicity_prod_mset_distrib) auto
+ also from S(1) p
+ have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
+ by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
+ also have "sum_mset \<dots> = f p"
+ by (simp add: semiring_1_class.sum_mset_delta' count_A)
+ finally show "f p = multiplicity p n" ..
+ qed
+qed
+
+lemma divides_primepow:
+ assumes "prime p" and "a dvd p ^ n"
+ obtains m where "m \<le> n" and "normalize a = p ^ m"
+ using divides_primepow_weak[OF assms] that assms
+ by (auto simp add: normalize_power)
+
+lemma Ex_other_prime_factor:
+ assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
+ shows "\<exists>q\<in>prime_factors n. q \<noteq> p"
+proof (rule ccontr)
+ assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
+ have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
+ using assms(1) by (intro prod_prime_factors [symmetric]) auto
+ also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
+ using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
+ finally have "normalize n = p ^ multiplicity p n" by auto
+ with assms show False by auto
+qed
+
end
+
+end
--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy Tue Jan 21 11:02:27 2020 +0100
@@ -24,7 +24,8 @@
end
-instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instantiation real ::
+ "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
@@ -55,7 +56,11 @@
end
-instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance real :: field_gcd ..
+
+
+instantiation rat ::
+ "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
@@ -86,7 +91,11 @@
end
-instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance rat :: field_gcd ..
+
+
+instantiation complex ::
+ "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
@@ -117,4 +126,6 @@
end
+instance complex :: field_gcd ..
+
end
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Jan 21 11:02:27 2020 +0100
@@ -2906,7 +2906,7 @@
qed (rule fps_divide_times_eq, simp_all add: fps_divide_def)
-instantiation fps :: (field) normalization_semidom
+instantiation fps :: (field) normalization_semidom_multiplicative
begin
definition fps_normalize_def [simp]:
@@ -2914,10 +2914,17 @@
instance proof
fix f g :: "'a fps"
- show "unit_factor (f * g) = unit_factor f * unit_factor g"
- using fps_unit_factor_mult by simp
+ assume "is_unit f"
+ thus "unit_factor (f * g) = f * unit_factor g"
+ using fps_unit_factor_mult[of f g] by simp
+next
+ fix f g :: "'a fps"
show "unit_factor f * normalize f = f"
by (simp add: fps_shift_times_fps_X_power)
+next
+ fix f g :: "'a fps"
+ show "unit_factor (f * g) = unit_factor f * unit_factor g"
+ using fps_unit_factor_mult[of f g] by simp
qed (simp_all add: fps_divide_def Let_def)
end
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy Tue Jan 21 11:02:27 2020 +0100
@@ -12,7 +12,7 @@
definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
"quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
-definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \<times> 'a \<Rightarrow> 'a \<times> 'a" where
+definition normalize_quot :: "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} \<times> 'a \<Rightarrow> 'a \<times> 'a" where
"normalize_quot =
(\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))"
@@ -118,7 +118,8 @@
using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto
-lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \<Rightarrow> 'a \<times> 'a"
+lift_definition quot_of_fract ::
+ "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract \<Rightarrow> 'a \<times> 'a"
is normalize_quot
by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Jan 21 11:02:27 2020 +0100
@@ -48,7 +48,7 @@
by (simp add: One_nat_def [symmetric] del: One_nat_def)
lemma is_nth_power_conv_multiplicity:
- fixes x :: "'a :: factorial_semiring"
+ fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}"
assumes "n > 0"
shows "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
proof (cases "x = 0")
--- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Jan 21 11:02:27 2020 +0100
@@ -3445,10 +3445,18 @@
assume "p \<noteq> 0"
then show "is_unit (unit_factor p)"
by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
+next
+ fix a b :: "'a poly" assume "is_unit a"
+ thus "unit_factor (a * b) = a * unit_factor b"
+ by (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult elim!: is_unit_polyE)
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
end
+instance poly :: ("{semidom_divide_unit_factor,idom_divide,normalization_semidom_multiplicative}")
+ normalization_semidom_multiplicative
+ by intro_classes (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult)
+
lemma normalize_poly_eq_map_poly: "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
proof -
have "[:unit_factor (lead_coeff p):] dvd p"
@@ -3489,7 +3497,9 @@
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
-lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
+lemma normalize_smult:
+ fixes c :: "'a :: {normalization_semidom_multiplicative, idom_divide}"
+ shows "normalize (smult c p) = smult (normalize c) (normalize p)"
proof -
have "smult c p = [:c:] * p" by simp
also have "normalize \<dots> = smult (normalize c) (normalize p)"
@@ -4488,8 +4498,10 @@
then show "content p = 1" by simp
qed auto
-lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
- by (simp add: content_def coeffs_smult Gcd_fin_mult)
+lemma content_smult [simp]:
+ fixes c :: "'a :: {normalization_semidom_multiplicative, semiring_gcd}"
+ shows "content (smult c p) = normalize c * content p"
+ by (simp add: content_def coeffs_smult Gcd_fin_mult normalize_mult)
lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
by (auto simp: content_def simp: poly_eq_iff coeffs_def)
@@ -4528,6 +4540,7 @@
qed
lemma content_primitive_part [simp]:
+ fixes p :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly"
assumes "p \<noteq> 0"
shows "content (primitive_part p) = 1"
proof -
@@ -4544,7 +4557,7 @@
qed
lemma content_decompose:
- obtains p' :: "'a::semiring_gcd poly"
+ obtains p' :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly"
where "p = smult (content p) p'" "content p' = 1"
proof (cases "p = 0")
case True
@@ -4581,7 +4594,8 @@
qed
lemma smult_content_normalize_primitive_part [simp]:
- "smult (content p) (normalize (primitive_part p)) = normalize p"
+ fixes p :: "'a :: {normalization_semidom_multiplicative, semiring_gcd, idom_divide} poly"
+ shows "smult (content p) (normalize (primitive_part p)) = normalize p"
proof -
have "smult (content p) (normalize (primitive_part p)) =
normalize ([:content p:] * primitive_part p)"
@@ -4623,7 +4637,7 @@
qed (insert assms, auto)
lemma content_mult:
- fixes p q :: "'a :: {factorial_semiring, semiring_gcd} poly"
+ fixes p q :: "'a :: {factorial_semiring, semiring_gcd, normalization_semidom_multiplicative} poly"
shows "content (p * q) = content p * content q"
proof (cases "p * q = 0")
case False
@@ -4646,7 +4660,8 @@
end
lemma primitive_part_mult:
- fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+ fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+ normalization_semidom_multiplicative} poly"
shows "primitive_part (p * q) = primitive_part p * primitive_part q"
proof -
have "primitive_part (p * q) = p * q div [:content (p * q):]"
@@ -4659,7 +4674,8 @@
qed
lemma primitive_part_smult:
- fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+ normalization_semidom_multiplicative} poly"
shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
proof -
have "smult a p = [:a:] * p" by simp
@@ -4669,17 +4685,19 @@
qed
lemma primitive_part_dvd_primitive_partI [intro]:
- fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+ fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+ normalization_semidom_multiplicative} poly"
shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
by (auto elim!: dvdE simp: primitive_part_mult)
lemma content_prod_mset:
- fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
+ fixes A :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative}
+ poly multiset"
shows "content (prod_mset A) = prod_mset (image_mset content A)"
by (induction A) (simp_all add: content_mult mult_ac)
lemma content_prod_eq_1_iff:
- fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
+ fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly"
shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
proof safe
assume A: "content (p * q) = 1"
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Tue Jan 21 11:02:27 2020 +0100
@@ -160,7 +160,7 @@
using fract_poly_dvd[of p 1] by simp
lemma fract_poly_smult_eqE:
- fixes c :: "'a :: {idom_divide,ring_gcd} fract"
+ fixes c :: "'a :: {idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract"
assumes "fract_poly p = smult c (fract_poly q)"
obtains a b
where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
@@ -180,16 +180,16 @@
subsection \<open>Fractional content\<close>
abbreviation (input) Lcm_coeff_denoms
- :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
+ :: "'a :: {semiring_Gcd,idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a"
where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
definition fract_content ::
- "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
+ "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a fract" where
"fract_content p =
(let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)"
definition primitive_part_fract ::
- "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
+ "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a poly" where
"primitive_part_fract p =
primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
@@ -201,7 +201,10 @@
unfolding fract_content_def Let_def Zero_fract_def
by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
-lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
+lemma content_primitive_part_fract [simp]:
+ fixes p :: "'a :: {semiring_gcd_mult_normalize,
+ factorial_semiring, ring_gcd, semiring_Gcd,idom_divide} fract poly"
+ shows "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
unfolding primitive_part_fract_def
by (rule content_primitive_part)
(auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)
@@ -256,7 +259,8 @@
qed
lemma content_decompose_fract:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,
+ semiring_gcd_mult_normalize} fract poly"
obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
proof (cases "p = 0")
case True
@@ -347,7 +351,8 @@
qed (auto intro: lift_prime_elem_poly)
lemma fract_poly_dvdD:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,
+ semiring_gcd_mult_normalize} poly"
assumes "fract_poly p dvd fract_poly q" "content p = 1"
shows "p dvd q"
proof -
@@ -372,7 +377,7 @@
begin
interpretation field_poly:
- normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
+ normalization_euclidean_semiring_multiplicative where zero = "0 :: 'a :: field poly"
and one = 1 and plus = plus and minus = minus
and times = times
and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
@@ -392,7 +397,7 @@
by (simp add: irreducible_dict)
show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
by (simp add: prime_elem_dict)
- show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
+ show "class.normalization_euclidean_semiring_multiplicative divide plus minus (0 :: 'a poly) times 1
modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
(\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
proof (standard, fold dvd_dict)
@@ -407,13 +412,17 @@
fix p :: "'a poly" assume "p \<noteq> 0"
then show "is_unit [:lead_coeff p:]"
by (simp add: is_unit_pCons_iff)
+ next
+ fix a b :: "'a poly" assume "is_unit a"
+ thus "[:lead_coeff (a * b):] = a * [:lead_coeff b:]"
+ by (auto elim!: is_unit_polyE)
qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
qed
lemma field_poly_irreducible_imp_prime:
"prime_elem p" if "irreducible p" for p :: "'a :: field poly"
using that by (fact field_poly.irreducible_imp_prime_elem)
-
+find_theorems name:prod_mset_prime_factorization
lemma field_poly_prod_mset_prime_factorization:
"prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
if "p \<noteq> 0" for p :: "'a :: field poly"
@@ -429,7 +438,7 @@
subsection \<open>Primality and irreducibility in polynomial rings\<close>
lemma nonconst_poly_irreducible_iff:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "degree p \<noteq> 0"
shows "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
proof safe
@@ -507,7 +516,7 @@
qed
private lemma irreducible_imp_prime_poly:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "irreducible p"
shows "prime_elem p"
proof (cases "degree p = 0")
@@ -542,7 +551,7 @@
qed
lemma irreducible_primitive_part_fract:
- fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+ fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly"
assumes "irreducible p"
shows "irreducible (primitive_part_fract p)"
proof -
@@ -561,7 +570,7 @@
qed
lemma prime_elem_primitive_part_fract:
- fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+ fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly"
shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
@@ -583,13 +592,13 @@
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
lemma irreducible_linear_poly:
- fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
+ fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}"
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
by (auto intro!: irreducible_linear_field_poly
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons)
lemma prime_elem_linear_poly:
- fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
+ fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}"
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
@@ -597,7 +606,7 @@
subsection \<open>Prime factorisation of polynomials\<close>
private lemma poly_prime_factorization_exists_content_1:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "p \<noteq> 0" "content p = 1"
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
proof -
@@ -657,19 +666,25 @@
qed
lemma poly_prime_factorization_exists:
- fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+ fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "p \<noteq> 0"
- shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
+ shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> normalize (prod_mset A) = normalize p"
proof -
define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
then guess A by (elim exE conjE) note A = this
- moreover from assms have "prod_mset B = [:content p:]"
- by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
+ have "normalize (prod_mset (A + B)) = normalize (prod_mset A * normalize (prod_mset B))"
+ by simp
+ also from assms have "normalize (prod_mset B) = normalize [:content p:]"
+ by (simp add: prod_mset_const_poly normalize_const_poly prod_mset_prime_factorization_weak B_def)
+ also have "prod_mset A = normalize (primitive_part p)"
+ using A by simp
+ finally have "normalize (prod_mset (A + B)) = normalize (primitive_part p * [:content p:])"
+ by simp
moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
- ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
+ ultimately show ?thesis using A by (intro exI[of _ "A + B"]) (auto)
qed
end
@@ -677,10 +692,10 @@
subsection \<open>Typeclass instances\<close>
-instance poly :: (factorial_ring_gcd) factorial_semiring
+instance poly :: ("{factorial_ring_gcd,semiring_gcd_mult_normalize}") factorial_semiring
by standard (rule poly_prime_factorization_exists)
-instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
+instantiation poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") factorial_ring_gcd
begin
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
@@ -699,7 +714,10 @@
end
-instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") semiring_gcd_mult_normalize ..
+
+instantiation poly :: ("{field,factorial_ring_gcd,semiring_gcd_mult_normalize}")
+ "{unique_euclidean_ring, normalization_euclidean_semiring}"
begin
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
@@ -724,14 +742,15 @@
end
-instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
+instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd,
+ semiring_gcd_mult_normalize}") euclidean_ring_gcd
by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
subsection \<open>Polynomial GCD\<close>
lemma gcd_poly_decompose:
- fixes p q :: "'a :: factorial_ring_gcd poly"
+ fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
shows "gcd p q =
smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
proof (rule sym, rule gcdI)
@@ -755,7 +774,7 @@
lemma gcd_poly_pseudo_mod:
- fixes p q :: "'a :: factorial_ring_gcd poly"
+ fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
proof -
@@ -834,12 +853,14 @@
by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
lemma lcm_poly_code [code]:
- fixes p q :: "'a :: factorial_ring_gcd poly"
- shows "lcm p q = normalize (p * q) div gcd p q"
+ fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
+ shows "lcm p q = normalize (p * q div gcd p q)"
by (fact lcm_gcd)
-lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
-lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+lemmas Gcd_poly_set_eq_fold [code] =
+ Gcd_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
+lemmas Lcm_poly_set_eq_fold [code] =
+ Lcm_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
text \<open>Example:
@{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
--- a/src/HOL/GCD.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/GCD.thy Tue Jan 21 11:02:27 2020 +0100
@@ -166,7 +166,7 @@
and gcd_dvd2 [iff]: "gcd a b dvd b"
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
- and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
+ and lcm_gcd: "lcm a b = normalize (a * b div gcd a b)"
begin
lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
@@ -272,211 +272,6 @@
lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
by (fact gcd.right_idem)
-lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
-proof (cases "c = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
- by (auto intro: gcd_greatest)
- moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
- by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
- ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
- by (auto intro: associated_eqI)
- then show ?thesis
- by (simp add: normalize_mult)
-qed
-
-lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
- using gcd_mult_left [of c a b] by (simp add: ac_simps)
-
-lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
- by (simp add: gcd_mult_left mult.assoc [symmetric])
-
-lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
- using mult_gcd_left [of c a b] by (simp add: ac_simps)
-
-lemma dvd_lcm1 [iff]: "a dvd lcm a b"
-proof -
- have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
- by (simp add: lcm_gcd normalize_mult div_mult_swap)
- then show ?thesis
- by (simp add: lcm_gcd)
-qed
-
-lemma dvd_lcm2 [iff]: "b dvd lcm a b"
-proof -
- have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
- by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
- then show ?thesis
- by (simp add: lcm_gcd)
-qed
-
-lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
- by (rule dvd_trans) (assumption, blast)
-
-lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
- by (rule dvd_trans) (assumption, blast)
-
-lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
- using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
-
-lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
- using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
-
-lemma lcm_least:
- assumes "a dvd c" and "b dvd c"
- shows "lcm a b dvd c"
-proof (cases "c = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have *: "is_unit (unit_factor c)"
- by simp
- show ?thesis
- proof (cases "gcd a b = 0")
- case True
- with assms show ?thesis by simp
- next
- case False
- then have "a \<noteq> 0 \<or> b \<noteq> 0"
- by simp
- with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
- by (simp_all add: mult_dvd_mono)
- then have "normalize (a * b) dvd gcd (a * c) (b * c)"
- by (auto intro: gcd_greatest simp add: ac_simps)
- then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
- using * by (simp add: dvd_mult_unit_iff)
- then have "normalize (a * b) dvd gcd a b * c"
- by (simp add: mult_gcd_right [of a b c])
- then have "normalize (a * b) div gcd a b dvd c"
- using False by (simp add: div_dvd_iff_mult ac_simps)
- then show ?thesis
- by (simp add: lcm_gcd)
- qed
-qed
-
-lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
- by (blast intro!: lcm_least intro: dvd_trans)
-
-lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
- by (simp add: lcm_gcd dvd_normalize_div)
-
-lemma lcm_0_left [simp]: "lcm 0 a = 0"
- by (simp add: lcm_gcd)
-
-lemma lcm_0_right [simp]: "lcm a 0 = 0"
- by (simp add: lcm_gcd)
-
-lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
- (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?P
- then have "0 dvd lcm a b"
- by simp
- then have "0 dvd normalize (a * b) div gcd a b"
- by (simp add: lcm_gcd)
- then have "0 * gcd a b dvd normalize (a * b)"
- using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
- then have "normalize (a * b) = 0"
- by simp
- then show ?Q
- by simp
-next
- assume ?Q
- then show ?P
- by auto
-qed
-
-lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
- by (auto intro: associated_eqI)
-
-lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
- by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
-
-sublocale lcm: abel_semigroup lcm
-proof
- fix a b c
- show "lcm a b = lcm b a"
- by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
- have "lcm (lcm a b) c dvd lcm a (lcm b c)"
- and "lcm a (lcm b c) dvd lcm (lcm a b) c"
- by (auto intro: lcm_least
- dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
- dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
- dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
- dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
- then show "lcm (lcm a b) c = lcm a (lcm b c)"
- by (rule associated_eqI) simp_all
-qed
-
-sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
-proof
- show "lcm a a = normalize a" for a
- proof -
- have "lcm a a dvd a"
- by (rule lcm_least) simp_all
- then show ?thesis
- by (auto intro: associated_eqI)
- qed
- show "lcm (normalize a) b = lcm a b" for a b
- using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
- by (auto intro: associated_eqI)
- show "lcm 1 a = normalize a" for a
- by (rule associated_eqI) simp_all
-qed simp_all
-
-lemma lcm_self: "lcm a a = normalize a"
- by (fact lcm.idem_normalize)
-
-lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
- by (fact lcm.left_idem)
-
-lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
- by (fact lcm.right_idem)
-
-lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
- by (simp add: lcm_gcd normalize_mult)
-
-lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
- using gcd_mult_lcm [of a b] by (simp add: ac_simps)
-
-lemma gcd_lcm:
- assumes "a \<noteq> 0" and "b \<noteq> 0"
- shows "gcd a b = normalize (a * b) div lcm a b"
-proof -
- from assms have "lcm a b \<noteq> 0"
- by (simp add: lcm_eq_0_iff)
- have "gcd a b * lcm a b = normalize a * normalize b"
- by simp
- then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
- by (simp_all add: normalize_mult)
- with \<open>lcm a b \<noteq> 0\<close> show ?thesis
- using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
-qed
-
-lemma lcm_1_left: "lcm 1 a = normalize a"
- by (fact lcm.top_left_normalize)
-
-lemma lcm_1_right: "lcm a 1 = normalize a"
- by (fact lcm.top_right_normalize)
-
-lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
- by (cases "c = 0")
- (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
- simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
-
-lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
- using lcm_mult_left [of c a b] by (simp add: ac_simps)
-
-lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
- by (simp add: lcm_mult_left mult.assoc [symmetric])
-
-lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
- using mult_lcm_left [of c a b] by (simp add: ac_simps)
-
lemma gcdI:
assumes "c dvd a" and "c dvd b"
and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
@@ -520,21 +315,199 @@
lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
using gcd_proj1_iff [of n m] by (simp add: ac_simps)
-lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
- by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
-
-lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
-proof-
- have "normalize k * gcd a b = gcd (k * a) (k * b)"
- by (simp add: gcd_mult_distrib')
- then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
+lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize (c * gcd a b)"
+proof (cases "c = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
+ by (auto intro: gcd_greatest)
+ moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
+ by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
+ ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
+ by (auto intro: associated_eqI)
+ then show ?thesis
+ by (simp add: normalize_mult)
+qed
+
+lemma gcd_mult_right: "gcd (a * c) (b * c) = normalize (gcd b a * c)"
+ using gcd_mult_left [of c a b] by (simp add: ac_simps)
+
+lemma dvd_lcm1 [iff]: "a dvd lcm a b"
+ by (metis div_mult_swap dvd_mult2 dvd_normalize_iff dvd_refl gcd_dvd2 lcm_gcd)
+
+lemma dvd_lcm2 [iff]: "b dvd lcm a b"
+ by (metis dvd_div_mult dvd_mult dvd_normalize_iff dvd_refl gcd_dvd1 lcm_gcd)
+
+lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
+ by (rule dvd_trans) (assumption, blast)
+
+lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
+ by (rule dvd_trans) (assumption, blast)
+
+lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
+ using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
+
+lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
+ using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
+
+lemma lcm_least:
+ assumes "a dvd c" and "b dvd c"
+ shows "lcm a b dvd c"
+proof (cases "c = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ then have *: "is_unit (unit_factor c)"
+ by simp
+ show ?thesis
+ proof (cases "gcd a b = 0")
+ case True
+ with assms show ?thesis by simp
+ next
+ case False
+ have "a * b dvd normalize (c * gcd a b)"
+ using assms by (subst gcd_mult_left [symmetric]) (auto intro!: gcd_greatest simp: mult_ac)
+ with False have "(a * b div gcd a b) dvd c"
+ by (subst div_dvd_iff_mult) auto
+ thus ?thesis by (simp add: lcm_gcd)
+ qed
+qed
+
+lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
+ by (blast intro!: lcm_least intro: dvd_trans)
+
+lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
+ by (simp add: lcm_gcd dvd_normalize_div)
+
+lemma lcm_0_left [simp]: "lcm 0 a = 0"
+ by (simp add: lcm_gcd)
+
+lemma lcm_0_right [simp]: "lcm a 0 = 0"
+ by (simp add: lcm_gcd)
+
+lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+ (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ then have "0 dvd lcm a b"
+ by simp
+ also have "lcm a b dvd (a * b)"
by simp
- then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
- by (simp only: ac_simps)
+ finally show ?Q
+ by auto
+next
+ assume ?Q
+ then show ?P
+ by auto
+qed
+
+lemma zero_eq_lcm_iff: "0 = lcm a b \<longleftrightarrow> a = 0 \<or> b = 0"
+ using lcm_eq_0_iff[of a b] by auto
+
+lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
+ by (auto intro: associated_eqI)
+
+lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
+ using lcm_eq_0_iff[of a b] by (cases "lcm a b = 0") (auto simp: lcm_gcd)
+
+sublocale lcm: abel_semigroup lcm
+proof
+ fix a b c
+ show "lcm a b = lcm b a"
+ by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
+ have "lcm (lcm a b) c dvd lcm a (lcm b c)"
+ and "lcm a (lcm b c) dvd lcm (lcm a b) c"
+ by (auto intro: lcm_least
+ dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
+ dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
+ dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
+ dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
+ then show "lcm (lcm a b) c = lcm a (lcm b c)"
+ by (rule associated_eqI) simp_all
+qed
+
+sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
+proof
+ show "lcm a a = normalize a" for a
+ proof -
+ have "lcm a a dvd a"
+ by (rule lcm_least) simp_all
+ then show ?thesis
+ by (auto intro: associated_eqI)
+ qed
+ show "lcm (normalize a) b = lcm a b" for a b
+ using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
+ by (auto intro: associated_eqI)
+ show "lcm 1 a = normalize a" for a
+ by (rule associated_eqI) simp_all
+qed simp_all
+
+lemma lcm_self: "lcm a a = normalize a"
+ by (fact lcm.idem_normalize)
+
+lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
+ by (fact lcm.left_idem)
+
+lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
+ by (fact lcm.right_idem)
+
+lemma gcd_lcm:
+ assumes "a \<noteq> 0" and "b \<noteq> 0"
+ shows "gcd a b = normalize (a * b div lcm a b)"
+proof -
+ from assms have [simp]: "a * b div gcd a b \<noteq> 0"
+ by (subst dvd_div_eq_0_iff) auto
+ let ?u = "unit_factor (a * b div gcd a b)"
+ have "gcd a b * normalize (a * b div gcd a b) =
+ gcd a b * ((a * b div gcd a b) * (1 div ?u))"
+ by simp
+ also have "\<dots> = a * b div ?u"
+ by (subst mult.assoc [symmetric]) auto
+ also have "\<dots> dvd a * b"
+ by (subst div_unit_dvd_iff) auto
+ finally have "gcd a b dvd ((a * b) div lcm a b)"
+ by (intro dvd_mult_imp_div) (auto simp: lcm_gcd)
+ moreover have "a * b div lcm a b dvd a" and "a * b div lcm a b dvd b"
+ using assms by (subst div_dvd_iff_mult; simp add: lcm_eq_0_iff mult.commute[of b "lcm a b"])+
+ ultimately have "normalize (gcd a b) = normalize (a * b div lcm a b)"
+ apply -
+ apply (rule associated_eqI)
+ using assms
+ apply (auto simp: div_dvd_iff_mult zero_eq_lcm_iff)
+ done
+ thus ?thesis by simp
+qed
+
+lemma lcm_1_left: "lcm 1 a = normalize a"
+ by (fact lcm.top_left_normalize)
+
+lemma lcm_1_right: "lcm a 1 = normalize a"
+ by (fact lcm.top_right_normalize)
+
+lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize (c * lcm a b)"
+proof (cases "c = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ then have *: "lcm (c * a) (c * b) dvd c * lcm a b"
+ by (auto intro: lcm_least)
+ moreover have "lcm a b dvd lcm (c * a) (c * b) div c"
+ by (intro lcm_least) (auto intro!: dvd_mult_imp_div simp: mult_ac)
+ hence "c * lcm a b dvd lcm (c * a) (c * b)"
+ using False by (subst (asm) dvd_div_iff_mult) (auto simp: mult_ac intro: dvd_lcmI1)
+ ultimately have "normalize (lcm (c * a) (c * b)) = normalize (c * lcm a b)"
+ by (auto intro: associated_eqI)
then show ?thesis
- by simp
+ by (simp add: normalize_mult)
qed
+lemma lcm_mult_right: "lcm (a * c) (b * c) = normalize (lcm b a * c)"
+ using lcm_mult_left [of c a b] by (simp add: ac_simps)
+
lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
@@ -554,30 +527,6 @@
lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
by (fact lcm.normalize_right_idem)
-lemma gcd_mult_unit1:
- assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
-proof -
- have "gcd (b * a) c dvd b"
- using assms local.dvd_mult_unit_iff by blast
- then show ?thesis
- by (rule gcdI) simp_all
-qed
-
-lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
- using gcd.commute gcd_mult_unit1 by auto
-
-lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
- by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
-
-lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
- by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
-
-lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
- by (fact gcd.normalize_left_idem)
-
-lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
- by (fact gcd.normalize_right_idem)
-
lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
by standard (simp_all add: fun_eq_iff ac_simps)
@@ -605,18 +554,6 @@
by (rule dvd_trans)
qed
-lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
- by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
-
-lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
- using gcd_add1 [of n m] by (simp add: ac_simps)
-
-lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
- by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
-
-lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
- by (simp add: lcm_gcd)
-
declare unit_factor_lcm [simp]
lemma lcmI:
@@ -636,11 +573,11 @@
lemma lcm_proj1_if_dvd:
assumes "b dvd a" shows "lcm a b = normalize a"
-proof (cases "a = 0")
- case False
- then show ?thesis
- using assms gcd_proj2_if_dvd lcm_mult_gcd local.lcm_gcd by auto
-qed auto
+proof -
+ have "normalize (lcm a b) = normalize a"
+ by (rule associatedI) (use assms in auto)
+ thus ?thesis by simp
+qed
lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
@@ -667,21 +604,6 @@
lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
using lcm_proj1_iff [of n m] by (simp add: ac_simps)
-lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
- by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
-
-lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
-proof-
- have "normalize k * lcm a b = lcm (k * a) (k * b)"
- by (simp add: lcm_mult_distrib')
- then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
- by simp
- then have "normalize k * unit_factor k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
- by (simp only: ac_simps)
- then show ?thesis
- by simp
-qed
-
lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
by (simp add: gcd_dvdI1 gcd_dvdI2)
@@ -701,12 +623,45 @@
moreover have "x dvd a" by (simp add: x_def)
moreover from assms have "p dvd gcd (b * a) (b * p)"
by (intro gcd_greatest) (simp_all add: mult.commute)
- hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
+ hence "p dvd b * gcd a p" by (subst (asm) gcd_mult_left) auto
with False have "y dvd b"
by (simp add: x_def y_def div_dvd_iff_mult assms)
ultimately show ?thesis by (rule that)
qed
+lemma gcd_mult_unit1:
+ assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
+proof -
+ have "gcd (b * a) c dvd b"
+ using assms dvd_mult_unit_iff by blast
+ then show ?thesis
+ by (rule gcdI) simp_all
+qed
+
+lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
+ using gcd.commute gcd_mult_unit1 by auto
+
+lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
+ by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
+
+lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
+ by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
+
+lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
+ by (fact gcd.normalize_left_idem)
+
+lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
+ by (fact gcd.normalize_right_idem)
+
+lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
+ by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
+
+lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
+ using gcd_add1 [of n m] by (simp add: ac_simps)
+
+lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
+ by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
+
end
class ring_gcd = comm_ring_1 + semiring_gcd
@@ -831,9 +786,9 @@
lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
proof -
have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d"
- by (meson UnE local.Lcm_least local.dvd_Lcm local.dvd_trans)
+ by (meson UnE Lcm_least dvd_Lcm dvd_trans)
then show ?thesis
- by (meson Lcm_subset local.lcm_unique local.normalize_Lcm sup.cobounded1 sup.cobounded2)
+ by (meson Lcm_subset lcm_unique normalize_Lcm sup.cobounded1 sup.cobounded2)
qed
lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
@@ -982,7 +937,7 @@
lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
by (blast dest: dvd_GcdD intro: Gcd_greatest)
-lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
+lemma Gcd_mult: "Gcd ((*) c ` A) = normalize (c * Gcd A)"
proof (cases "c = 0")
case True
then show ?thesis by auto
@@ -993,17 +948,11 @@
(auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
then have "Gcd ((*) c ` A) dvd c * Gcd A"
by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
- also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
- by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
- also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
- by (simp add: dvd_mult_unit_iff)
- finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
- moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
+ moreover have "c * Gcd A dvd Gcd ((*) c ` A)"
by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
- ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
+ ultimately have "normalize (Gcd ((*) c ` A)) = normalize (c * Gcd A)"
by (rule associatedI)
- then show ?thesis
- by (simp add: normalize_mult)
+ then show ?thesis by simp
qed
lemma Lcm_eqI:
@@ -1021,7 +970,7 @@
lemma Lcm_mult:
assumes "A \<noteq> {}"
- shows "Lcm ((*) c ` A) = normalize c * Lcm A"
+ shows "Lcm ((*) c ` A) = normalize (c * Lcm A)"
proof (cases "c = 0")
case True
with assms have "(*) c ` A = {0}"
@@ -1041,17 +990,11 @@
(auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
by auto
- also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
- by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
- also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
- by (simp add: mult_unit_dvd_iff)
- finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
- moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
+ moreover have "Lcm ((*) c ` A) dvd c * Lcm A"
by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
- ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
+ ultimately have "normalize (c * Lcm A) = normalize (Lcm ((*) c ` A))"
by (rule associatedI)
- then show ?thesis
- by (simp add: normalize_mult)
+ then show ?thesis by simp
qed
lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
@@ -1175,23 +1118,11 @@
by (simp add: Lcm_fin_dvd_iff)
lemma Gcd_fin_mult:
- "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
-using that proof induct
- case empty
- then show ?case
- by simp
-next
- case (insert a A)
- have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
- by simp
- also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
- by (simp add: normalize_mult)
- finally show ?case
- using insert by (simp add: gcd_mult_distrib')
-qed
+ "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A)" if "finite A"
+ using that by induction (auto simp: gcd_mult_left)
lemma Lcm_fin_mult:
- "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
+ "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A)" if "A \<noteq> {}"
proof (cases "b = 0")
case True
moreover from that have "times 0 ` A = {0}"
@@ -1210,19 +1141,8 @@
by simp
next
case True
- then show ?thesis using that proof (induct A rule: finite_ne_induct)
- case (singleton a)
- then show ?case
- by (simp add: normalize_mult)
- next
- case (insert a A)
- have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
- by simp
- also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
- by (simp add: normalize_mult)
- finally show ?case
- using insert by (simp add: lcm_mult_distrib')
- qed
+ then show ?thesis using that
+ by (induct A rule: finite_ne_induct) (auto simp: lcm_mult_left)
qed
qed
@@ -1413,9 +1333,9 @@
case False
then have unit: "is_unit (unit_factor b)"
by simp
- from \<open>coprime a c\<close> mult_gcd_left [of b a c]
+ from \<open>coprime a c\<close>
have "gcd (b * a) (b * c) * unit_factor b = b"
- by (simp add: ac_simps)
+ by (subst gcd_mult_left) (simp add: ac_simps)
moreover from \<open>a dvd b * c\<close>
have "a dvd gcd (b * a) (b * c) * unit_factor b"
by (simp add: dvd_mult_unit_iff unit)
@@ -1479,9 +1399,9 @@
by simp
with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
also from assms have "a div gcd a b = a'"
- using dvd_div_eq_mult local.gcd_dvd1 by blast
+ using dvd_div_eq_mult gcd_dvd1 by blast
also from assms have "b div gcd a b = b'"
- using dvd_div_eq_mult local.gcd_dvd1 by blast
+ using dvd_div_eq_mult gcd_dvd1 by blast
finally show ?thesis .
qed
@@ -1574,24 +1494,6 @@
ultimately show ?rhs ..
qed
-lemma coprime_crossproduct':
- fixes a b c d
- assumes "b \<noteq> 0"
- assumes unit_factors: "unit_factor b = unit_factor d"
- assumes coprime: "coprime a b" "coprime c d"
- shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
- assume eq: "a * d = b * c"
- hence "normalize a * normalize d = normalize c * normalize b"
- by (simp only: normalize_mult [symmetric] mult_ac)
- with coprime have "normalize b = normalize d"
- by (subst (asm) coprime_crossproduct) simp_all
- from this and unit_factors show "b = d"
- by (rule normalize_unit_factor_eqI)
- from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
- with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
lemma gcd_mult_left_left_cancel:
"gcd (c * a) b = gcd a b" if "coprime b c"
proof -
@@ -1619,8 +1521,8 @@
using that gcd_mult_right_left_cancel [of a c b]
by (simp add: ac_simps)
-lemma gcd_exp [simp]:
- "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+lemma gcd_exp_weak:
+ "gcd (a ^ n) (b ^ n) = normalize (gcd a b ^ n)"
proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
case True
then show ?thesis
@@ -1633,11 +1535,10 @@
by simp
then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
by simp
- then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+ then have "normalize (gcd a b ^ n) = normalize (gcd a b ^ n * \<dots>)"
by simp
- also note gcd_mult_distrib
- also have "unit_factor (gcd a b ^ n) = 1"
- using False by (auto simp: unit_factor_power unit_factor_gcd)
+ also have "\<dots> = gcd (gcd a b ^ n * (a div gcd a b) ^ n) (gcd a b ^ n * (b div gcd a b) ^ n)"
+ by (rule gcd_mult_left [symmetric])
also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
by (simp add: ac_simps div_power dvd_power_same)
also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
@@ -1737,6 +1638,87 @@
end
+subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>
+
+class semiring_gcd_mult_normalize = semiring_gcd + normalization_semidom_multiplicative
+begin
+
+lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
+ by (simp add: gcd_mult_left normalize_mult mult.assoc [symmetric])
+
+lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
+ using mult_gcd_left [of c a b] by (simp add: ac_simps)
+
+lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
+ by (subst gcd_mult_left) (simp_all add: normalize_mult)
+
+lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
+proof-
+ have "normalize k * gcd a b = gcd (k * a) (k * b)"
+ by (simp add: gcd_mult_distrib')
+ then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
+ by simp
+ then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
+ by (simp only: ac_simps)
+ then show ?thesis
+ by simp
+qed
+
+lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
+ by (simp add: lcm_gcd normalize_mult dvd_normalize_div)
+
+lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
+ using gcd_mult_lcm [of a b] by (simp add: ac_simps)
+
+lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
+ by (simp add: lcm_mult_left mult.assoc [symmetric] normalize_mult)
+
+lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
+ using mult_lcm_left [of c a b] by (simp add: ac_simps)
+
+lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
+ by (simp add: lcm_gcd dvd_normalize_div normalize_mult)
+
+lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
+ by (subst lcm_mult_left) (simp add: normalize_mult)
+
+lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+proof-
+ have "normalize k * lcm a b = lcm (k * a) (k * b)"
+ by (simp add: lcm_mult_distrib')
+ then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
+ by simp
+ then have "normalize k * unit_factor k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+ by (simp only: ac_simps)
+ then show ?thesis
+ by simp
+qed
+
+lemma coprime_crossproduct':
+ fixes a b c d
+ assumes "b \<noteq> 0"
+ assumes unit_factors: "unit_factor b = unit_factor d"
+ assumes coprime: "coprime a b" "coprime c d"
+ shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+ assume eq: "a * d = b * c"
+ hence "normalize a * normalize d = normalize c * normalize b"
+ by (simp only: normalize_mult [symmetric] mult_ac)
+ with coprime have "normalize b = normalize d"
+ by (subst (asm) coprime_crossproduct) simp_all
+ from this and unit_factors show "b = d"
+ by (rule normalize_unit_factor_eqI)
+ from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+ with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
+lemma gcd_exp [simp]:
+ "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+ using gcd_exp_weak[of a n b] by (simp add: normalize_power)
+
+end
+
+
subsection \<open>GCD and LCM on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
instantiation nat :: gcd
@@ -1946,13 +1928,13 @@
instance int :: ring_gcd
proof
fix k l r :: int
- show "gcd k l dvd k" "gcd k l dvd l"
+ show [simp]: "gcd k l dvd k" "gcd k l dvd l"
using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
by simp_all
- show "lcm k l = normalize (k * l) div gcd k l"
+ show "lcm k l = normalize (k * l div gcd k l)"
using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
- by (simp add: nat_eq_iff of_nat_div abs_mult)
+ by (simp add: nat_eq_iff of_nat_div abs_mult abs_div)
assume "r dvd k" "r dvd l"
then show "r dvd gcd k l"
using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
@@ -2010,15 +1992,11 @@
lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
for k m n :: nat
\<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
-proof (induct m n rule: gcd_nat_induct)
- case (step m n)
- then show ?case
- by (metis gcd_mult_distrib' gcd_red_nat)
-qed auto
+ by (simp add: gcd_mult_left)
lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
for k m n :: int
- using gcd_mult_distrib' [of k m n] by simp
+ by (simp add: gcd_mult_left abs_mult)
text \<open>\medskip Addition laws.\<close>
@@ -2400,15 +2378,15 @@
lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
for a b :: int
- by (simp add: abs_mult lcm_gcd)
+ by (simp add: abs_mult lcm_gcd abs_div)
lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
for m n :: nat
- by simp
+ by (simp add: lcm_gcd)
lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
for m n :: int
- by simp
+ by (simp add: lcm_gcd abs_div abs_mult)
lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
for m n :: nat
@@ -2553,6 +2531,9 @@
for N :: "nat set"
by (rule Gcd_eq_1_I) auto
+instance nat :: semiring_gcd_mult_normalize
+ by intro_classes (auto simp: unit_factor_nat_def)
+
text \<open>Alternative characterizations of Gcd:\<close>
@@ -2695,7 +2676,10 @@
by (rule Lcm_least) (use that in auto)
then show ?thesis by simp
qed
-qed simp_all
+qed (simp_all add: sgn_mult)
+
+instance int :: semiring_gcd_mult_normalize
+ by intro_classes (auto simp: sgn_mult)
subsection \<open>GCD and LCM on \<^typ>\<open>integer\<close>\<close>
--- a/src/HOL/Library/Multiset.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Jan 21 11:02:27 2020 +0100
@@ -2495,15 +2495,26 @@
shows "prod_mset (A - {#a#}) = prod_mset A div a"
using assms prod_mset_diff [of "{#a#}" A] by auto
+lemma (in normalization_semidom) normalize_prod_mset_normalize:
+ "normalize (prod_mset (image_mset normalize A)) = normalize (prod_mset A)"
+proof (induction A)
+ case (add x A)
+ have "normalize (prod_mset (image_mset normalize (add_mset x A))) =
+ normalize (x * normalize (prod_mset (image_mset normalize A)))"
+ by simp
+ also note add.IH
+ finally show ?case by simp
+qed auto
+
lemma (in algebraic_semidom) is_unit_prod_mset_iff:
"is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x \<in># A. is_unit x)"
by (induct A) (auto simp: is_unit_mult_iff)
-lemma (in normalization_semidom) normalize_prod_mset:
+lemma (in normalization_semidom_multiplicative) normalize_prod_mset:
"normalize (prod_mset A) = prod_mset (image_mset normalize A)"
by (induct A) (simp_all add: normalize_mult)
-lemma (in normalization_semidom) normalized_prod_msetI:
+lemma (in normalization_semidom_multiplicative) normalized_prod_msetI:
assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
shows "normalize (prod_mset A) = prod_mset A"
proof -
--- a/src/HOL/Number_Theory/Prime_Powers.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy Tue Jan 21 11:02:27 2020 +0100
@@ -95,6 +95,7 @@
by (auto simp: primepow_def aprimedivisor_prime_power prime_factorization_prime_power)
lemma primepow_decompose:
+ fixes n :: "'a :: factorial_semiring_multiplicative"
assumes "primepow n"
shows "aprimedivisor n ^ multiplicity (aprimedivisor n) n = n"
proof -
@@ -133,11 +134,13 @@
lemma primepow_gt_0_nat: "primepow n \<Longrightarrow> n > (0::nat)"
using primepow_gt_Suc_0[of n] by simp
-lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1"
+lemma unit_factor_primepow:
+ fixes p :: "'a :: factorial_semiring_multiplicative"
+ shows "primepow p \<Longrightarrow> unit_factor p = 1"
by (auto simp: primepow_def unit_factor_power)
lemma aprimedivisor_primepow:
- assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring)"
+ assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring_multiplicative)"
shows "aprimedivisor (p * n) = p" "aprimedivisor n = p"
proof -
from assms have [simp]: "n \<noteq> 0" by auto
@@ -187,8 +190,9 @@
lemma primepow_power_iff:
+ fixes p :: "'a :: factorial_semiring_multiplicative"
assumes "unit_factor p = 1"
- shows "primepow (p ^ n) \<longleftrightarrow> primepow (p :: 'a :: factorial_semiring) \<and> n > 0"
+ shows "primepow (p ^ n) \<longleftrightarrow> primepow p \<and> n > 0"
proof safe
assume "primepow (p ^ n)"
hence n: "n \<noteq> 0" by (auto intro!: Nat.gr0I)
@@ -218,11 +222,11 @@
by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])
lemma primepow_prime_power [simp]:
- "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
+ "prime (p :: 'a :: factorial_semiring_multiplicative) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
by (subst primepow_power_iff) auto
lemma aprimedivisor_vimage:
- assumes "prime (p :: 'a :: factorial_semiring)"
+ assumes "prime (p :: 'a :: factorial_semiring_multiplicative)"
shows "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
proof safe
fix q assume q: "q \<in> primepow_factors n"
@@ -267,7 +271,7 @@
qed
lemma bij_betw_primepows:
- "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring)
+ "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring_multiplicative)
(Collect prime \<times> UNIV) (Collect primepow)"
proof (rule bij_betwI [where ?g = "(\<lambda>n. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"],
goal_cases)
@@ -310,14 +314,14 @@
qed
lemma primepow_mult_aprimedivisorI:
- assumes "primepow (n :: 'a :: factorial_semiring)"
+ assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
shows "primepow (aprimedivisor n * n)"
by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
subst primepow_prime_power)
(insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
lemma primepow_factors_altdef:
- fixes x :: "'a :: factorial_semiring"
+ fixes x :: "'a :: factorial_semiring_multiplicative"
assumes "x \<noteq> 0"
shows "primepow_factors x = {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}"
proof (intro equalityI subsetI)
@@ -330,7 +334,7 @@
qed (auto simp: primepow_factors_def prime_factors_multiplicity multiplicity_dvd')
lemma finite_primepow_factors:
- assumes "x \<noteq> (0 :: 'a :: factorial_semiring)"
+ assumes "x \<noteq> (0 :: 'a :: factorial_semiring_multiplicative)"
shows "finite (primepow_factors x)"
proof -
have "finite (SIGMA p:prime_factors x. {0<..multiplicity p x})"
@@ -342,7 +346,7 @@
qed
lemma aprimedivisor_primepow_factors_conv_prime_factorization:
- assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring)"
+ assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring_multiplicative)"
shows "image_mset aprimedivisor (mset_set (primepow_factors n)) = prime_factorization n"
(is "?lhs = ?rhs")
proof (intro multiset_eqI)
@@ -403,6 +407,7 @@
using assms by (auto simp: primepow_def dest!: prime_dvd_power[rotated] dest: primes_dvd_imp_eq)
lemma sum_prime_factorization_conv_sum_primepow_factors:
+ fixes n :: "'a :: factorial_semiring_multiplicative"
assumes "n \<noteq> 0"
shows "(\<Sum>q\<in>primepow_factors n. f (aprimedivisor q)) = (\<Sum>p\<in>#prime_factorization n. f p)"
proof -
@@ -414,7 +419,7 @@
qed
lemma multiplicity_aprimedivisor_Suc_0_iff:
- assumes "primepow (n :: 'a :: factorial_semiring)"
+ assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
shows "multiplicity (aprimedivisor n) n = Suc 0 \<longleftrightarrow> prime n"
by (subst (3) primepow_decompose [OF assms, symmetric])
(insert assms, auto simp add: prime_power_iff intro!: prime_aprimedivisor')
--- a/src/HOL/Power.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Power.thy Tue Jan 21 11:02:27 2020 +0100
@@ -377,7 +377,7 @@
end
-context normalization_semidom
+context normalization_semidom_multiplicative
begin
lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"
--- a/src/HOL/Rings.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Rings.thy Tue Jan 21 11:02:27 2020 +0100
@@ -1290,9 +1290,17 @@
assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
- and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+ and unit_factor_mult_unit_left: "a dvd 1 \<Longrightarrow> unit_factor (a * b) = a * unit_factor b"
\<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
-
+begin
+
+lemma unit_factor_mult_unit_right: "a dvd 1 \<Longrightarrow> unit_factor (b * a) = unit_factor b * a"
+ using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac)
+
+lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right
+
+end
+
class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
fixes normalize :: "'a \<Rightarrow> 'a"
assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
@@ -1434,47 +1442,41 @@
then show ?lhs by simp
qed
-lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
-proof (cases "a = 0 \<or> b = 0")
- case True
- then show ?thesis by auto
-next
- case False
- have "unit_factor (a * b) * normalize (a * b) = a * b"
- by (rule unit_factor_mult_normalize)
- then have "normalize (a * b) = a * b div unit_factor (a * b)"
- by simp
- also have "\<dots> = a * b div unit_factor (b * a)"
- by (simp add: ac_simps)
- also have "\<dots> = a * b div unit_factor b div unit_factor a"
- using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
- also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
- using False by (subst unit_div_mult_swap) simp_all
- also have "\<dots> = normalize a * normalize b"
- using False
- by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
- finally show ?thesis .
-qed
-
lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
by (cases "a = 0") (auto intro: is_unit_unit_factor)
lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
by (rule is_unit_normalize) simp
+lemma normalize_mult_unit_left [simp]:
+ assumes "a dvd 1"
+ shows "normalize (a * b) = normalize b"
+proof (cases "b = 0")
+ case False
+ have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)"
+ using assms by (subst unit_factor_mult_unit_left) auto
+ also have "\<dots> = a * b" by simp
+ also have "b = unit_factor b * normalize b" by simp
+ hence "a * b = a * unit_factor b * normalize b"
+ by (simp only: mult_ac)
+ finally show ?thesis
+ using assms False by auto
+qed auto
+
+lemma normalize_mult_unit_right [simp]:
+ assumes "b dvd 1"
+ shows "normalize (a * b) = normalize a"
+ using assms by (subst mult.commute) auto
+
lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
proof (cases "a = 0")
- case True
- then show ?thesis by simp
-next
case False
have "normalize a = normalize (unit_factor a * normalize a)"
by simp
- also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
- by (simp only: normalize_mult)
- finally show ?thesis
- using False by simp_all
-qed
+ also from False have "\<dots> = normalize (normalize a)"
+ by (subst normalize_mult_unit_left) auto
+ finally show ?thesis ..
+qed auto
lemma unit_factor_normalize [simp]:
assumes "a \<noteq> 0"
@@ -1492,30 +1494,6 @@
by simp
qed
-lemma dvd_unit_factor_div:
- assumes "b dvd a"
- shows "unit_factor (a div b) = unit_factor a div unit_factor b"
-proof -
- from assms have "a = a div b * b"
- by simp
- then have "unit_factor a = unit_factor (a div b * b)"
- by simp
- then show ?thesis
- by (cases "b = 0") (simp_all add: unit_factor_mult)
-qed
-
-lemma dvd_normalize_div:
- assumes "b dvd a"
- shows "normalize (a div b) = normalize a div normalize b"
-proof -
- from assms have "a = a div b * b"
- by simp
- then have "normalize a = normalize (a div b * b)"
- by simp
- then show ?thesis
- by (cases "b = 0") (simp_all add: normalize_mult)
-qed
-
lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
proof -
have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
@@ -1582,7 +1560,7 @@
then have "is_unit c" and "is_unit d"
by auto
with a b show ?thesis
- by (simp add: normalize_mult is_unit_normalize)
+ by (simp add: is_unit_normalize)
qed
lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
@@ -1643,9 +1621,70 @@
by simp
qed
+lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)"
+ by (rule associated_eqI) (auto intro!: mult_dvd_mono)
+
+lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)"
+ by (rule associated_eqI) (auto intro!: mult_dvd_mono)
+
end
+class normalization_semidom_multiplicative = normalization_semidom +
+ assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+begin
+
+lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
+proof (cases "a = 0 \<or> b = 0")
+ case True
+ then show ?thesis by auto
+next
+ case False
+ have "unit_factor (a * b) * normalize (a * b) = a * b"
+ by (rule unit_factor_mult_normalize)
+ then have "normalize (a * b) = a * b div unit_factor (a * b)"
+ by simp
+ also have "\<dots> = a * b div unit_factor (b * a)"
+ by (simp add: ac_simps)
+ also have "\<dots> = a * b div unit_factor b div unit_factor a"
+ using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
+ also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
+ using False by (subst unit_div_mult_swap) simp_all
+ also have "\<dots> = normalize a * normalize b"
+ using False
+ by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
+ finally show ?thesis .
+qed
+
+lemma dvd_unit_factor_div:
+ assumes "b dvd a"
+ shows "unit_factor (a div b) = unit_factor a div unit_factor b"
+proof -
+ from assms have "a = a div b * b"
+ by simp
+ then have "unit_factor a = unit_factor (a div b * b)"
+ by simp
+ then show ?thesis
+ by (cases "b = 0") (simp_all add: unit_factor_mult)
+qed
+
+lemma dvd_normalize_div:
+ assumes "b dvd a"
+ shows "normalize (a div b) = normalize a div normalize b"
+proof -
+ from assms have "a = a div b * b"
+ by simp
+ then have "normalize a = normalize (a div b * b)"
+ by simp
+ then show ?thesis
+ by (cases "b = 0") (simp_all add: normalize_mult)
+qed
+
+end
+
+
+
+
text \<open>Syntactic division remainder operator\<close>
class modulo = dvd + divide +