10 Main |
10 Main |
11 "~~/src/HOL/Library/Multiset" |
11 "~~/src/HOL/Library/Multiset" |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Irreducible and prime elements\<close> |
14 subsection \<open>Irreducible and prime elements\<close> |
|
15 |
|
16 (* TODO: Move ? *) |
|
17 lemma (in semiring_gcd) prod_coprime' [rule_format]: |
|
18 "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1" |
|
19 using prod_coprime[of A f a] by (simp add: gcd.commute) |
|
20 |
15 |
21 |
16 context comm_semiring_1 |
22 context comm_semiring_1 |
17 begin |
23 begin |
18 |
24 |
19 definition irreducible :: "'a \<Rightarrow> bool" where |
25 definition irreducible :: "'a \<Rightarrow> bool" where |
462 by (subst prime_elem_dvd_power_iff) simp_all |
469 by (subst prime_elem_dvd_power_iff) simp_all |
463 |
470 |
464 lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" |
471 lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" |
465 by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) |
472 by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) |
466 |
473 |
|
474 lemma prime_dvd_prod_iff: "finite A \<Longrightarrow> prime p \<Longrightarrow> p dvd prod f A \<longleftrightarrow> (\<exists>x\<in>A. p dvd f x)" |
|
475 by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset) |
|
476 |
467 lemma primes_dvd_imp_eq: |
477 lemma primes_dvd_imp_eq: |
468 assumes "prime p" "prime q" "p dvd q" |
478 assumes "prime p" "prime q" "p dvd q" |
469 shows "p = q" |
479 shows "p = q" |
470 proof - |
480 proof - |
471 from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def) |
481 from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def) |
1101 proof (cases "is_unit p") |
1111 proof (cases "is_unit p") |
1102 case False |
1112 case False |
1103 with assms show ?thesis |
1113 with assms show ?thesis |
1104 by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) |
1114 by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) |
1105 qed (insert assms, auto simp: multiplicity_unit_left) |
1115 qed (insert assms, auto simp: multiplicity_unit_left) |
|
1116 |
|
1117 lemma prime_power_inj: |
|
1118 assumes "prime a" "a ^ m = a ^ n" |
|
1119 shows "m = n" |
|
1120 proof - |
|
1121 have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms) |
|
1122 thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all |
|
1123 qed |
|
1124 |
|
1125 lemma prime_power_inj': |
|
1126 assumes "prime p" "prime q" |
|
1127 assumes "p ^ m = q ^ n" "m > 0" "n > 0" |
|
1128 shows "p = q" "m = n" |
|
1129 proof - |
|
1130 from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp |
|
1131 also have "p ^ m = q ^ n" by fact |
|
1132 finally have "p dvd q ^ n" by simp |
|
1133 with assms have "p dvd q" using prime_dvd_power[of p q] by simp |
|
1134 with assms show "p = q" by (simp add: primes_dvd_imp_eq) |
|
1135 with assms show "m = n" by (simp add: prime_power_inj) |
|
1136 qed |
|
1137 |
|
1138 lemma prime_power_eq_one_iff [simp]: "prime p \<Longrightarrow> p ^ n = 1 \<longleftrightarrow> n = 0" |
|
1139 using prime_power_inj[of p n 0] by auto |
|
1140 |
|
1141 lemma one_eq_prime_power_iff [simp]: "prime p \<Longrightarrow> 1 = p ^ n \<longleftrightarrow> n = 0" |
|
1142 using prime_power_inj[of p 0 n] by auto |
|
1143 |
|
1144 lemma prime_power_inj'': |
|
1145 assumes "prime p" "prime q" |
|
1146 shows "p ^ m = q ^ n \<longleftrightarrow> (m = 0 \<and> n = 0) \<or> (p = q \<and> m = n)" |
|
1147 using assms |
|
1148 by (cases "m = 0"; cases "n = 0") |
|
1149 (auto dest: prime_power_inj'[OF assms]) |
1106 |
1150 |
1107 lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" |
1151 lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" |
1108 by (simp add: multiset_eq_iff count_prime_factorization) |
1152 by (simp add: multiset_eq_iff count_prime_factorization) |
1109 |
1153 |
1110 lemma prime_factorization_empty_iff: |
1154 lemma prime_factorization_empty_iff: |
1263 prime_factorization x + prime_factorization y" |
1307 prime_factorization x + prime_factorization y" |
1264 by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime) |
1308 by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime) |
1265 finally show ?thesis . |
1309 finally show ?thesis . |
1266 qed |
1310 qed |
1267 |
1311 |
|
1312 lemma prime_factorization_prod: |
|
1313 assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0" |
|
1314 shows "prime_factorization (prod f A) = (\<Sum>n\<in>A. prime_factorization (f n))" |
|
1315 using assms by (induction A rule: finite_induct) |
|
1316 (auto simp: Sup_multiset_empty prime_factorization_mult) |
|
1317 |
1268 lemma prime_elem_multiplicity_mult_distrib: |
1318 lemma prime_elem_multiplicity_mult_distrib: |
1269 assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0" |
1319 assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0" |
1270 shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" |
1320 shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" |
1271 proof - |
1321 proof - |
1272 have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" |
1322 have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" |
1460 from assms have "multiplicity p x < 1" |
1510 from assms have "multiplicity p x < 1" |
1461 by (intro multiplicity_lessI) auto |
1511 by (intro multiplicity_lessI) auto |
1462 thus ?thesis by simp |
1512 thus ?thesis by simp |
1463 qed |
1513 qed |
1464 |
1514 |
|
1515 lemma inj_on_Prod_primes: |
|
1516 assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p" |
|
1517 assumes "\<And>P. P \<in> A \<Longrightarrow> finite P" |
|
1518 shows "inj_on Prod A" |
|
1519 proof (rule inj_onI) |
|
1520 fix P Q assume PQ: "P \<in> A" "Q \<in> A" "\<Prod>P = \<Prod>Q" |
|
1521 with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q] |
|
1522 have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset) |
|
1523 with assms[of P] assms[of Q] PQ show "P = Q" by simp |
|
1524 qed |
|
1525 |
|
1526 |
1465 |
1527 |
1466 subsection \<open>GCD and LCM computation with unique factorizations\<close> |
1528 subsection \<open>GCD and LCM computation with unique factorizations\<close> |
1467 |
1529 |
1468 definition "gcd_factorial a b = (if a = 0 then normalize b |
1530 definition "gcd_factorial a b = (if a = 0 then normalize b |
1469 else if b = 0 then normalize a |
1531 else if b = 0 then normalize a |
1727 assumes "Lcm A \<noteq> 0" |
1789 assumes "Lcm A \<noteq> 0" |
1728 shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" |
1790 shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" |
1729 using assms |
1791 using assms |
1730 by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) |
1792 by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) |
1731 |
1793 |
|
1794 lemma prime_factors_gcd [simp]: |
|
1795 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (gcd a b) = |
|
1796 prime_factors a \<inter> prime_factors b" |
|
1797 by (subst prime_factorization_gcd) auto |
|
1798 |
|
1799 lemma prime_factors_lcm [simp]: |
|
1800 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (lcm a b) = |
|
1801 prime_factors a \<union> prime_factors b" |
|
1802 by (subst prime_factorization_lcm) auto |
|
1803 |
1732 subclass semiring_gcd |
1804 subclass semiring_gcd |
1733 by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) |
1805 by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) |
1734 (rule gcd_lcm_factorial; assumption)+ |
1806 (rule gcd_lcm_factorial; assumption)+ |
1735 |
1807 |
1736 subclass semiring_Gcd |
1808 subclass semiring_Gcd |