# HG changeset patch # User haftmann # Date 1474214275 -7200 # Node ID f91766530e13db8aa3510cdc6da199284bcaa600 # Parent c9bba9dba73b19bcf231db707dd1c5f33c13aab0 more generic algebraic lemmas diff -r c9bba9dba73b -r f91766530e13 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Tue Sep 20 14:51:58 2016 +0200 +++ b/src/HOL/GCD.thy Sun Sep 18 17:57:55 2016 +0200 @@ -939,6 +939,25 @@ lemma lcm_proj2_iff: "lcm m n = normalize n \ m dvd n" using lcm_proj1_iff [of n m] by (simp add: ac_simps) +lemma dvd_productE: + assumes "p dvd (a * b)" + obtains x y where "p = x * y" "x dvd a" "y dvd b" +proof (cases "a = 0") + case True + thus ?thesis by (intro that[of p 1]) simp_all +next + case False + define x y where "x = gcd a p" and "y = p div x" + have "p = x * y" by (simp add: x_def y_def) + 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) + 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 + end class ring_gcd = comm_ring_1 + semiring_gcd diff -r c9bba9dba73b -r f91766530e13 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Tue Sep 20 14:51:58 2016 +0200 +++ b/src/HOL/Groups_Big.thy Sun Sep 18 17:57:55 2016 +0200 @@ -1130,8 +1130,8 @@ end -lemma setprod_zero_iff [simp]: - fixes f :: "'b \ 'a::semidom" +lemma (in semidom) setprod_zero_iff [simp]: + fixes f :: "'b \ 'a" assumes "finite A" shows "setprod f A = 0 \ (\a\A. f a = 0)" using assms by (induct A) (auto simp: no_zero_divisors) diff -r c9bba9dba73b -r f91766530e13 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Sep 20 14:51:58 2016 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Sep 18 17:57:55 2016 +0200 @@ -247,6 +247,14 @@ by (auto simp del: count_greater_eq_Suc_zero_iff simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits) +lemma multiset_nonemptyE [elim]: + assumes "A \ {#}" + obtains x where "x \# A" +proof - + have "\x. x \# A" by (rule ccontr) (insert assms, auto) + with that show ?thesis by blast +qed + subsubsection \Union\ @@ -2041,6 +2049,10 @@ lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \ a = b \ A = {#}" by (auto simp: multiset_eq_iff) +lemma image_replicate_mset [simp]: + "image_mset f (replicate_mset n a) = replicate_mset n (f a)" + by (induct n) simp_all + subsection \Big operators\ @@ -2209,14 +2221,20 @@ translations "\i \# A. b" \ "CONST prod_mset (CONST image_mset (\i. b) A)" -lemma (in comm_semiring_1) dvd_prod_mset: +lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd: + assumes "A \# B" + shows "prod_mset A dvd prod_mset B" +proof - + from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add) + also have "prod_mset \ = prod_mset (B - A) * prod_mset A" by simp + also have "prod_mset A dvd \" by simp + finally show ?thesis . +qed + +lemma (in comm_monoid_mult) dvd_prod_mset: assumes "x \# A" shows "x dvd prod_mset A" -proof - - from assms have "A = add_mset x (A - {#x#})" by simp - then obtain B where "A = add_mset x B" .. - then show ?thesis by simp -qed + using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp lemma (in semidom) prod_mset_zero_iff [iff]: "prod_mset A = 0 \ 0 \# A" @@ -2236,10 +2254,22 @@ shows "prod_mset (A - {#a#}) = prod_mset A div a" using assms prod_mset_diff [of "{#a#}" A] by auto +lemma (in algebraic_semidom) is_unit_prod_mset_iff: + "is_unit (prod_mset A) \ (\x \# A. is_unit x)" + by (induct A) (auto simp: is_unit_mult_iff) + +lemma (in normalization_semidom) 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: assumes "\a. a \# A \ normalize a = a" shows "normalize (prod_mset A) = prod_mset A" - using assms by (induct A) (simp_all add: normalize_mult) +proof - + from assms have "image_mset normalize A = A" + by (induct A) simp_all + then show ?thesis by (simp add: normalize_prod_mset) +qed subsection \Alternative representations\ diff -r c9bba9dba73b -r f91766530e13 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Sep 20 14:51:58 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Sep 18 17:57:55 2016 +0200 @@ -112,23 +112,6 @@ by (auto intro!: euclidean_size_times_nonunit simp: ) qed -lemma irreducible_normalized_divisors: - assumes "irreducible x" "y dvd x" "normalize y = y" - shows "y = 1 \ y = normalize x" -proof - - from assms have "is_unit y \ x dvd y" by (auto simp: irreducible_altdef) - thus ?thesis - proof (elim disjE) - assume "is_unit y" - hence "normalize y = 1" by (simp add: is_unit_normalize) - with assms show ?thesis by simp - next - assume "x dvd y" - with \y dvd x\ have "normalize y = normalize x" by (rule associatedI) - with assms show ?thesis by simp - qed -qed - function gcd_eucl :: "'a \ 'a \ 'a" where "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))" @@ -720,4 +703,4 @@ semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+ qed -end \ No newline at end of file +end diff -r c9bba9dba73b -r f91766530e13 src/HOL/Number_Theory/Factorial_Ring.thy --- a/src/HOL/Number_Theory/Factorial_Ring.thy Tue Sep 20 14:51:58 2016 +0200 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Sun Sep 18 17:57:55 2016 +0200 @@ -1,4 +1,5 @@ (* Title: HOL/Number_Theory/Factorial_Ring.thy + Author: Manuel Eberl, TU Muenchen Author: Florian Haftmann, TU Muenchen *) @@ -7,29 +8,11 @@ theory Factorial_Ring imports Main - "../GCD" + "~~/src/HOL/GCD" "~~/src/HOL/Library/Multiset" begin -lemma (in semiring_gcd) dvd_productE: - assumes "p dvd (a * b)" - obtains x y where "p = x * y" "x dvd a" "y dvd b" -proof (cases "a = 0") - case True - thus ?thesis by (intro that[of p 1]) simp_all -next - case False - define x y where "x = gcd a p" and "y = p div x" - have "p = x * y" by (simp add: x_def y_def) - 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) - 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 - +subsection \Irreducible and prime elements\ context comm_semiring_1 begin @@ -83,7 +66,6 @@ shows "p \ 0" using assms by (auto intro: ccontr) - lemma prime_elem_dvd_power: "prime_elem p \ p dvd x ^ n \ p dvd x" by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) @@ -105,10 +87,6 @@ context algebraic_semidom begin -(* TODO Move *) -lemma mult_unit_dvd_iff': "is_unit a \ (a * b) dvd c \ b dvd c" - by (subst mult.commute) (rule mult_unit_dvd_iff) - lemma prime_elem_imp_irreducible: assumes "prime_elem p" shows "irreducible p" @@ -123,6 +101,22 @@ by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)]) qed (insert assms, simp_all add: prime_elem_def) +lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors: + assumes "is_unit x" "irreducible p" + shows "\p dvd x" +proof (rule notI) + assume "p dvd x" + with \is_unit x\ have "is_unit p" + by (auto intro: dvd_trans) + with \irreducible p\ show False + by (simp add: irreducible_not_unit) +qed + +lemma unit_imp_no_prime_divisors: + assumes "is_unit x" "prime_elem p" + shows "\p dvd x" + using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] . + lemma prime_elem_mono: assumes "prime_elem p" "\q dvd 1" "q dvd p" shows "prime_elem q" @@ -306,12 +300,17 @@ qed qed -lemma add_eq_Suc_lem: "a+b = Suc (x+y) \ a \ x \ b \ y" - by arith - lemma prime_elem_power_dvd_cases: - "\p^c dvd m * n; a + b = Suc c; prime_elem p\ \ p ^ a dvd m \ p ^ b dvd n" - using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem) + assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p" + shows "p ^ a dvd m \ p ^ b dvd n" +proof - + from assms obtain r s + where "r + s = c \ p ^ r dvd m \ p ^ s dvd n" + by (blast dest: prime_elem_power_dvd_prod) + moreover with assms have + "a \ r \ b \ s" by arith + ultimately show ?thesis by (auto intro: power_le_dvd) +qed lemma prime_elem_not_unit' [simp]: "ASSUMPTION (prime_elem x) \ \is_unit x" @@ -358,9 +357,29 @@ end + +subsection \Generalized primes: normalized prime elements\ + context normalization_semidom begin +lemma irreducible_normalized_divisors: + assumes "irreducible x" "y dvd x" "normalize y = y" + shows "y = 1 \ y = normalize x" +proof - + from assms have "is_unit y \ x dvd y" by (auto simp: irreducible_altdef) + thus ?thesis + proof (elim disjE) + assume "is_unit y" + hence "normalize y = 1" by (simp add: is_unit_normalize) + with assms show ?thesis by simp + next + assume "x dvd y" + with \y dvd x\ have "normalize y = normalize x" by (rule associatedI) + with assms show ?thesis by simp + qed +qed + lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" using irreducible_mult_unit_left[of "1 div unit_factor x" x] by (cases "x = 0") (simp_all add: unit_div_commute) @@ -443,16 +462,6 @@ "prime p \ n > 0 \ p dvd x ^ n \ p dvd x" by (subst prime_elem_dvd_power_iff) simp_all -lemma prod_mset_subset_imp_dvd: - assumes "A \# B" - shows "prod_mset A dvd prod_mset B" -proof - - from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add) - also have "prod_mset \ = prod_mset (B - A) * prod_mset A" by simp - also have "prod_mset A dvd \" by simp - finally show ?thesis . -qed - lemma prime_dvd_prod_mset_iff: "prime p \ p dvd prod_mset A \ (\x. x \# A \ p dvd x)" by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) @@ -508,26 +517,11 @@ shows "prod_mset A dvd prod_mset B \ A \# B" using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset) -lemma is_unit_prod_mset_iff: - "is_unit (prod_mset A) \ (\x. x \# A \ is_unit x)" - by (induction A) (auto simp: is_unit_mult_iff) - -lemma multiset_emptyI: "(\x. x \# A) \ A = {#}" - by (intro multiset_eqI) (simp_all add: count_eq_zero_iff) - lemma is_unit_prod_mset_primes_iff: assumes "\x. x \# A \ prime x" shows "is_unit (prod_mset A) \ A = {#}" -proof - assume unit: "is_unit (prod_mset A)" - show "A = {#}" - proof (intro multiset_emptyI notI) - fix x assume "x \# A" - with unit have "is_unit x" by (subst (asm) is_unit_prod_mset_iff) blast - moreover from \x \# A\ have "prime x" by (rule assms) - ultimately show False by simp - qed -qed simp_all + by (auto simp add: is_unit_prod_mset_iff) + (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff) lemma prod_mset_primes_irreducible_imp_prime: assumes irred: "irreducible (prod_mset A)" @@ -555,14 +549,6 @@ by (auto intro: prod_mset_subset_imp_dvd) qed -lemma multiset_nonemptyE [elim]: - assumes "A \ {#}" - obtains x where "x \# A" -proof - - have "\x. x \# A" by (rule ccontr) (insert assms, auto) - with that show ?thesis by blast -qed - lemma prod_mset_primes_finite_divisor_powers: assumes A: "\x. x \# A \ prime x" assumes B: "\x. x \# B \ prime x" @@ -585,11 +571,10 @@ ultimately show ?thesis by (rule finite_subset) qed -lemma normalize_prod_mset: - "normalize (prod_mset A) = prod_mset (image_mset normalize A)" - by (induction A) (simp_all add: normalize_mult mult_ac) +end -end + +subsection \In a semiring with GCD, each irreducible element is a prime elements\ context semiring_gcd begin @@ -652,9 +637,83 @@ end +subsection \Factorial semirings: algebraic structures with unique prime factorizations\ + class factorial_semiring = normalization_semidom + assumes prime_factorization_exists: - "x \ 0 \ \A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" + "x \ 0 \ \A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" + +text \Alternative characterization\ + +lemma (in normalization_semidom) factorial_semiring_altI_aux: + assumes finite_divisors: "\x. x \ 0 \ finite {y. y dvd x \ normalize y = y}" + assumes irreducible_imp_prime_elem: "\x. irreducible x \ prime_elem x" + assumes "x \ 0" + shows "\A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" +using \x \ 0\ +proof (induction "card {b. b dvd x \ normalize b = b}" arbitrary: x rule: less_induct) + case (less a) + let ?fctrs = "\a. {b. b dvd a \ normalize b = b}" + show ?case + proof (cases "is_unit a") + case True + thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize) + next + case False + show ?thesis + proof (cases "\b. b dvd a \ \is_unit b \ \a dvd b") + case False + with \\is_unit a\ less.prems have "irreducible a" by (auto simp: irreducible_altdef) + hence "prime_elem a" by (rule irreducible_imp_prime_elem) + thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto + next + case True + then guess b by (elim exE conjE) note b = this + + from b have "?fctrs b \ ?fctrs a" by (auto intro: dvd_trans) + moreover from b have "normalize a \ ?fctrs b" "normalize a \ ?fctrs a" by simp_all + hence "?fctrs b \ ?fctrs a" by blast + ultimately have "?fctrs b \ ?fctrs a" by (subst subset_not_subset_eq) blast + with finite_divisors[OF \a \ 0\] have "card (?fctrs b) < card (?fctrs a)" + by (rule psubset_card_mono) + moreover from \a \ 0\ b have "b \ 0" by auto + ultimately have "\A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize b" + by (intro less) auto + then guess A .. note A = this + + define c where "c = a div b" + from b have c: "a = b * c" by (simp add: c_def) + from less.prems c have "c \ 0" by auto + from b c have "?fctrs c \ ?fctrs a" by (auto intro: dvd_trans) + moreover have "normalize a \ ?fctrs c" + proof safe + assume "normalize a dvd c" + hence "b * c dvd 1 * c" by (simp add: c) + hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+ + with b show False by simp + qed + with \normalize a \ ?fctrs a\ have "?fctrs a \ ?fctrs c" by blast + ultimately have "?fctrs c \ ?fctrs a" by (subst subset_not_subset_eq) blast + with finite_divisors[OF \a \ 0\] have "card (?fctrs c) < card (?fctrs a)" + by (rule psubset_card_mono) + with \c \ 0\ have "\A. (\x. x \# A \ prime_elem x) \ 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) + qed + qed +qed + +lemma factorial_semiring_altI: + assumes finite_divisors: "\x::'a. x \ 0 \ finite {y. y dvd x \ normalize y = y}" + assumes irreducible_imp_prime: "\x::'a. irreducible x \ prime_elem x" + shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)" + by intro_classes (rule factorial_semiring_altI_aux[OF assms]) + +text \Properties\ + +context factorial_semiring begin lemma prime_factorization_exists': @@ -784,24 +843,6 @@ lemma multiplicity_dvd': "n \ multiplicity p x \ p ^ n dvd x" by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd]) -lemma dvd_power_iff: - assumes "x \ 0" - shows "x ^ m dvd x ^ n \ is_unit x \ m \ n" -proof - assume *: "x ^ m dvd x ^ n" - { - assume "m > n" - note * - also have "x ^ n = x ^ n * 1" by simp - also from \m > n\ have "m = n + (m - n)" by simp - also have "x ^ \ = x ^ n * x ^ (m - n)" by (rule power_add) - finally have "x ^ (m - n) dvd 1" - by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all) - with \m > n\ have "is_unit x" by (simp add: is_unit_power_iff) - } - thus "is_unit x \ m \ n" by force -qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd) - context fixes x p :: 'a assumes xp: "x \ 0" "\is_unit p" @@ -965,6 +1006,65 @@ qed qed simp_all +lemma multiplicity_self: + assumes "p \ 0" "\is_unit p" + shows "multiplicity p p = 1" +proof - + from assms have "multiplicity p p = Max {n. p ^ n dvd p}" + by (simp add: multiplicity_eq_Max) + also from assms have "p ^ n dvd p \ n \ 1" for n + using dvd_power_iff[of p n 1] by auto + hence "{n. p ^ n dvd p} = {..1}" by auto + also have "\ = {0,1}" by auto + finally show ?thesis by simp +qed + +lemma multiplicity_times_unit_left: + assumes "is_unit c" + shows "multiplicity (c * p) x = multiplicity p x" +proof - + from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}" + by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff) + thus ?thesis by (simp add: multiplicity_def) +qed + +lemma multiplicity_times_unit_right: + assumes "is_unit c" + shows "multiplicity p (c * x) = multiplicity p x" +proof - + from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}" + by (subst mult.commute) (simp add: dvd_mult_unit_iff) + thus ?thesis by (simp add: multiplicity_def) +qed + +lemma multiplicity_normalize_left [simp]: + "multiplicity (normalize p) x = multiplicity p x" +proof (cases "p = 0") + case [simp]: False + have "normalize p = (1 div unit_factor p) * p" + by (simp add: unit_div_commute is_unit_unit_factor) + also have "multiplicity \ x = multiplicity p x" + by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor) + finally show ?thesis . +qed simp_all + +lemma multiplicity_normalize_right [simp]: + "multiplicity p (normalize x) = multiplicity p x" +proof (cases "x = 0") + case [simp]: False + have "normalize x = (1 div unit_factor x) * x" + by (simp add: unit_div_commute is_unit_unit_factor) + also have "multiplicity p \ = multiplicity p x" + by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor) + finally show ?thesis . +qed simp_all + +lemma multiplicity_prime [simp]: "prime_elem p \ multiplicity p p = 1" + by (rule multiplicity_self) auto + +lemma multiplicity_prime_power [simp]: "prime_elem p \ multiplicity p (p ^ n) = n" + by (subst multiplicity_same_power') auto + lift_definition prime_factorization :: "'a \ 'a multiset" is "\x p. if prime p then multiplicity p x else 0" unfolding multiset_def @@ -996,15 +1096,14 @@ "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)" by transfer simp -lemma unit_imp_no_irreducible_divisors: - assumes "is_unit x" "irreducible p" - shows "\p dvd x" - using assms dvd_unit_imp_unit irreducible_not_unit by blast - -lemma unit_imp_no_prime_divisors: - assumes "is_unit x" "prime_elem p" - shows "\p dvd x" - using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] . +lemma dvd_imp_multiplicity_le: + assumes "a dvd b" "b \ 0" + shows "multiplicity p a \ multiplicity p b" +proof (cases "is_unit p") + case False + with assms show ?thesis + by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) +qed (insert assms, auto simp: multiplicity_unit_left) lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" by (simp add: multiset_eq_iff count_prime_factorization) @@ -1100,18 +1199,17 @@ "p \ prime_factors x \ p dvd x" by (simp add: in_prime_factors_iff) -lemma multiplicity_self: - assumes "p \ 0" "\is_unit p" - shows "multiplicity p p = 1" -proof - - from assms have "multiplicity p p = Max {n. p ^ n dvd p}" - by (simp add: multiplicity_eq_Max) - also from assms have "p ^ n dvd p \ n \ 1" for n - using dvd_power_iff[of p n 1] by auto - hence "{n. p ^ n dvd p} = {..1}" by auto - also have "\ = {0,1}" by auto - finally show ?thesis by simp -qed +lemma prime_factorsI: + "x \ 0 \ prime p \ p dvd x \ p \ prime_factors x" + by (auto simp: in_prime_factors_iff) + +lemma prime_factors_dvd: + "x \ 0 \ prime_factors x = {p. prime p \ p dvd x}" + by (auto intro: prime_factorsI) + +lemma prime_factors_multiplicity: + "prime_factors n = {p. prime p \ multiplicity p n > 0}" + by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff) lemma prime_factorization_prime: assumes "prime p" @@ -1136,44 +1234,6 @@ by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute) qed simp_all -lemma multiplicity_times_unit_left: - assumes "is_unit c" - shows "multiplicity (c * p) x = multiplicity p x" -proof - - from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}" - by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff) - thus ?thesis by (simp add: multiplicity_def) -qed - -lemma multiplicity_times_unit_right: - assumes "is_unit c" - shows "multiplicity p (c * x) = multiplicity p x" -proof - - from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}" - by (subst mult.commute) (simp add: dvd_mult_unit_iff) - thus ?thesis by (simp add: multiplicity_def) -qed - -lemma multiplicity_normalize_left [simp]: "multiplicity (normalize p) x = multiplicity p x" -proof (cases "p = 0") - case [simp]: False - have "normalize p = (1 div unit_factor p) * p" - by (simp add: unit_div_commute is_unit_unit_factor) - also have "multiplicity \ x = multiplicity p x" - by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor) - finally show ?thesis . -qed simp_all - -lemma multiplicity_normalize_right [simp]: "multiplicity p (normalize x) = multiplicity p x" -proof (cases "x = 0") - case [simp]: False - have "normalize x = (1 div unit_factor x) * x" - by (simp add: unit_div_commute is_unit_unit_factor) - also have "multiplicity p \ = multiplicity p x" - by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor) - finally show ?thesis . -qed simp_all - lemma prime_factorization_cong: "normalize x = normalize y \ prime_factorization x = prime_factorization y" by (simp add: multiset_eq_iff count_prime_factorization @@ -1206,6 +1266,51 @@ finally show ?thesis . qed +lemma prime_elem_multiplicity_mult_distrib: + assumes "prime_elem p" "x \ 0" "y \ 0" + shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" +proof - + have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" + by (subst count_prime_factorization_prime) (simp_all add: assms) + also from assms + have "prime_factorization (x * y) = prime_factorization x + prime_factorization y" + by (intro prime_factorization_mult) + also have "count \ (normalize p) = + count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" + by simp + also have "\ = multiplicity p x + multiplicity p y" + by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) + finally show ?thesis . +qed + +lemma prime_elem_multiplicity_prod_mset_distrib: + assumes "prime_elem p" "0 \# A" + shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" + using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) + +lemma prime_elem_multiplicity_power_distrib: + assumes "prime_elem p" "x \ 0" + shows "multiplicity p (x ^ n) = n * multiplicity p x" + using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"] + by simp + +lemma prime_elem_multiplicity_setprod_distrib: + assumes "prime_elem p" "0 \ f ` A" "finite A" + shows "multiplicity p (setprod f A) = (\x\A. multiplicity p (f x))" +proof - + have "multiplicity p (setprod f A) = (\x\#mset_set A. multiplicity p (f x))" + using assms by (subst setprod_unfold_prod_mset) + (simp_all add: prime_elem_multiplicity_prod_mset_distrib setsum_unfold_sum_mset + multiset.map_comp o_def) + also from \finite A\ have "\ = (\x\A. multiplicity p (f x))" + by (induction A rule: finite_induct) simp_all + finally show ?thesis . +qed + +lemma multiplicity_distinct_prime_power: + "prime p \ prime q \ p \ q \ multiplicity p (q ^ n) = 0" + by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) + lemma prime_factorization_prime_power: "prime p \ prime_factorization (p ^ n) = replicate_mset n p" by (induction n) @@ -1243,60 +1348,10 @@ lemma zero_not_in_prime_factors [simp]: "0 \ prime_factors x" by (auto dest: in_prime_factors_imp_prime) - -lemma prime_elem_multiplicity_mult_distrib: - assumes "prime_elem p" "x \ 0" "y \ 0" - shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" -proof - - have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" - by (subst count_prime_factorization_prime) (simp_all add: assms) - also from assms - have "prime_factorization (x * y) = prime_factorization x + prime_factorization y" - by (intro prime_factorization_mult) - also have "count \ (normalize p) = - count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" - by simp - also have "\ = multiplicity p x + multiplicity p y" - by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) - finally show ?thesis . -qed - -lemma prime_elem_multiplicity_power_distrib: - assumes "prime_elem p" "x \ 0" - shows "multiplicity p (x ^ n) = n * multiplicity p x" - by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib) - -lemma prime_elem_multiplicity_prod_mset_distrib: - assumes "prime_elem p" "0 \# A" - shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" - using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) - -lemma prime_elem_multiplicity_setprod_distrib: - assumes "prime_elem p" "0 \ f ` A" "finite A" - shows "multiplicity p (setprod f A) = (\x\A. multiplicity p (f x))" -proof - - have "multiplicity p (setprod f A) = (\x\#mset_set A. multiplicity p (f x))" - using assms by (subst setprod_unfold_prod_mset) - (simp_all add: prime_elem_multiplicity_prod_mset_distrib setsum_unfold_sum_mset - multiset.map_comp o_def) - also from \finite A\ have "\ = (\x\A. multiplicity p (f x))" - by (induction A rule: finite_induct) simp_all - finally show ?thesis . -qed - -lemma prime_factorsI: - "x \ 0 \ prime p \ p dvd x \ p \ prime_factors x" - by (auto simp: in_prime_factors_iff) - lemma prime_prime_factors: "prime p \ prime_factors p = {p}" by (drule prime_factorization_prime) simp -lemma prime_factors_altdef_multiplicity: - "prime_factors n = {p. prime p \ multiplicity p n > 0}" - by (cases "n = 0") - (auto simp: prime_multiplicity_gt_zero_iff in_prime_factors_iff) - lemma setprod_prime_factors: assumes "x \ 0" shows "(\p \ prime_factors x. p ^ multiplicity p x) = normalize x" @@ -1311,13 +1366,6 @@ finally show ?thesis .. qed -(* TODO Move *) -lemma (in semidom) setprod_zero_iff [simp]: - assumes "finite A" - shows "setprod f A = 0 \ (\a\A. f a = 0)" - using assms by (induct A) (auto simp: no_zero_divisors) -(* END TODO *) - lemma prime_factorization_unique'': assumes S_eq: "S = {p. 0 < f p}" and "finite S" @@ -1360,29 +1408,10 @@ qed qed -lemma multiplicity_prime [simp]: "prime_elem p \ multiplicity p p = 1" - by (rule multiplicity_self) auto - -lemma multiplicity_prime_power [simp]: "prime_elem p \ multiplicity p (p ^ n) = n" - by (subst multiplicity_same_power') auto - lemma prime_factors_product: "x \ 0 \ y \ 0 \ prime_factors (x * y) = prime_factors x \ prime_factors y" by (simp add: prime_factorization_mult) -lemma multiplicity_distinct_prime_power: - "prime p \ prime q \ p \ q \ multiplicity p (q ^ n) = 0" - by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) - -lemma dvd_imp_multiplicity_le: - assumes "a dvd b" "b \ 0" - shows "multiplicity p a \ multiplicity p b" -proof (cases "is_unit p") - case False - with assms show ?thesis - by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) -qed (insert assms, auto simp: multiplicity_unit_left) - lemma dvd_prime_factors [intro]: "y \ 0 \ x dvd y \ prime_factors x \ prime_factors y" by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto @@ -1402,9 +1431,6 @@ "x \ 0 \ y \ 0 \ x dvd y \ (\p. multiplicity p x \ multiplicity p y)" by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd) -lemma prime_factors_altdef: "x \ 0 \ prime_factors x = {p. prime p \ p dvd x}" - by (auto intro: prime_factorsI) - lemma multiplicity_eq_imp_eq: assumes "x \ 0" "y \ 0" assumes "\p. prime p \ multiplicity p x = multiplicity p y" @@ -1438,6 +1464,8 @@ qed +subsection \GCD and LCM computation with unique factorizations\ + definition "gcd_factorial a b = (if a = 0 then normalize b else if b = 0 then normalize a else prod_mset (prime_factorization a \# prime_factorization b))" @@ -1674,73 +1702,6 @@ end -lemma (in normalization_semidom) factorial_semiring_altI_aux: - assumes finite_divisors: "\x::'a. x \ 0 \ finite {y. y dvd x \ normalize y = y}" - assumes irreducible_imp_prime_elem: "\x::'a. irreducible x \ prime_elem x" - assumes "(x::'a) \ 0" - shows "\A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" -using \x \ 0\ -proof (induction "card {b. b dvd x \ normalize b = b}" arbitrary: x rule: less_induct) - case (less a) - let ?fctrs = "\a. {b. b dvd a \ normalize b = b}" - show ?case - proof (cases "is_unit a") - case True - thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize) - next - case False - show ?thesis - proof (cases "\b. b dvd a \ \is_unit b \ \a dvd b") - case False - with \\is_unit a\ less.prems have "irreducible a" by (auto simp: irreducible_altdef) - hence "prime_elem a" by (rule irreducible_imp_prime_elem) - thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto - next - case True - then guess b by (elim exE conjE) note b = this - - from b have "?fctrs b \ ?fctrs a" by (auto intro: dvd_trans) - moreover from b have "normalize a \ ?fctrs b" "normalize a \ ?fctrs a" by simp_all - hence "?fctrs b \ ?fctrs a" by blast - ultimately have "?fctrs b \ ?fctrs a" by (subst subset_not_subset_eq) blast - with finite_divisors[OF \a \ 0\] have "card (?fctrs b) < card (?fctrs a)" - by (rule psubset_card_mono) - moreover from \a \ 0\ b have "b \ 0" by auto - ultimately have "\A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize b" - by (intro less) auto - then guess A .. note A = this - - define c where "c = a div b" - from b have c: "a = b * c" by (simp add: c_def) - from less.prems c have "c \ 0" by auto - from b c have "?fctrs c \ ?fctrs a" by (auto intro: dvd_trans) - moreover have "normalize a \ ?fctrs c" - proof safe - assume "normalize a dvd c" - hence "b * c dvd 1 * c" by (simp add: c) - hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+ - with b show False by simp - qed - with \normalize a \ ?fctrs a\ have "?fctrs a \ ?fctrs c" by blast - ultimately have "?fctrs c \ ?fctrs a" by (subst subset_not_subset_eq) blast - with finite_divisors[OF \a \ 0\] have "card (?fctrs c) < card (?fctrs a)" - by (rule psubset_card_mono) - with \c \ 0\ have "\A. (\x. x \# A \ prime_elem x) \ 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) - qed - qed -qed - -lemma factorial_semiring_altI: - assumes finite_divisors: "\