# HG changeset patch # User haftmann # Date 1474021855 -7200 # Node ID 1c3dcb5fe6cbce1ef8feea7b4066974a0e933e1e # Parent b8482e12a2a8adeb21dacd56ab2ff233801ba2c2 prefer abbreviation for trivial set conversion diff -r b8482e12a2a8 -r 1c3dcb5fe6cb src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Fri Sep 16 12:30:55 2016 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Fri Sep 16 12:30:55 2016 +0200 @@ -794,7 +794,7 @@ lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)" proof - have "Lcm_coeff_denoms (fract_poly p) = 1" - by (auto simp: Lcm_1_iff set_coeffs_map_poly) + by (auto simp: set_coeffs_map_poly) hence "fract_content (fract_poly p) = to_fract (content (map_poly (fst \ quot_of_fract \ to_fract) p))" by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff) @@ -1063,7 +1063,7 @@ have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 normalize_field_poly unit_factor_field_poly" .. - from field_poly.in_prime_factorization_imp_prime[of p x] assms + from field_poly.in_prime_factors_imp_prime [of p x] assms show ?thesis unfolding prime_elem_def dvd_field_poly comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast qed @@ -1314,7 +1314,7 @@ moreover from assms have "prod_mset B = [:content p:]" by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization) moreover have "\p. p \# B \ prime_elem p" - by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime) + 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 qed diff -r b8482e12a2a8 -r 1c3dcb5fe6cb src/HOL/Number_Theory/Factorial_Ring.thy --- a/src/HOL/Number_Theory/Factorial_Ring.thy Fri Sep 16 12:30:55 2016 +0200 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Fri Sep 16 12:30:55 2016 +0200 @@ -1,4 +1,3 @@ - (* Title: HOL/Number_Theory/Factorial_Ring.thy Author: Florian Haftmann, TU Muenchen *) @@ -982,6 +981,9 @@ qed simp_all qed +abbreviation prime_factors :: "'a \ 'a set" where + "prime_factors a \ set_mset (prime_factorization a)" + lemma count_prime_factorization_nonprime: "\prime p \ count (prime_factorization x) p = 0" by transfer simp @@ -1080,23 +1082,23 @@ (simp_all add: prime_factorization_unit prime_factorization_times_prime is_unit_normalize normalize_mult) -lemma in_prime_factorization_iff: - "p \# prime_factorization x \ x \ 0 \ p dvd x \ prime p" +lemma in_prime_factors_iff: + "p \ prime_factors x \ x \ 0 \ p dvd x \ prime p" proof - - have "p \# prime_factorization x \ count (prime_factorization x) p > 0" by simp + have "p \ prime_factors x \ count (prime_factorization x) p > 0" by simp also have "\ \ x \ 0 \ p dvd x \ prime p" by (subst count_prime_factorization, cases "x = 0") (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff) finally show ?thesis . qed -lemma in_prime_factorization_imp_prime: - "p \# prime_factorization x \ prime p" - by (simp add: in_prime_factorization_iff) +lemma in_prime_factors_imp_prime [intro]: + "p \ prime_factors x \ prime p" + by (simp add: in_prime_factors_iff) -lemma in_prime_factorization_imp_dvd: - "p \# prime_factorization x \ p dvd x" - by (simp add: in_prime_factorization_iff) +lemma in_prime_factors_imp_dvd [dest]: + "p \ prime_factors x \ p dvd x" + by (simp add: in_prime_factors_iff) lemma multiplicity_self: assumes "p \ 0" "\is_unit p" @@ -1197,10 +1199,10 @@ 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_factorization_imp_prime) + 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_factorization_imp_prime) + by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime) finally show ?thesis . qed @@ -1219,8 +1221,7 @@ have "x dvd y \ prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)" by (simp add: prod_mset_prime_factorization) also have "\ \ prime_factorization x \# prime_factorization y" - by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd - in_prime_factorization_imp_prime) + by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd) finally show ?thesis .. qed @@ -1239,8 +1240,8 @@ with assms show ?thesis by simp qed simp_all -lemma zero_not_in_prime_factorization [simp]: "0 \# prime_factorization x" - by (auto dest: in_prime_factorization_imp_prime) +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: @@ -1283,40 +1284,18 @@ finally show ?thesis . qed - - -definition prime_factors where - "prime_factors x = set_mset (prime_factorization x)" - -lemma set_mset_prime_factorization: - "set_mset (prime_factorization x) = prime_factors x" - by (simp add: prime_factors_def) - lemma prime_factorsI: "x \ 0 \ prime p \ p dvd x \ p \ prime_factors x" - by (auto simp: prime_factors_def in_prime_factorization_iff) - -lemma prime_factors_prime [intro]: "p \ prime_factors x \ prime p" - by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime) + by (auto simp: in_prime_factors_iff) lemma prime_prime_factors: - assumes "prime p" - shows "prime_factors p = {p}" - using assms by (simp add: prime_factors_def) - (drule prime_factorization_prime, simp) - -lemma prime_factors_dvd [dest]: "p \ prime_factors x \ p dvd x" - by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd) - -lemma prime_factors_finite [iff]: - "finite (prime_factors n)" - unfolding prime_factors_def by simp + "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_factors_def prime_multiplicity_gt_zero_iff - prime_imp_prime_elem in_prime_factorization_iff) + (auto simp: prime_multiplicity_gt_zero_iff in_prime_factors_iff) lemma setprod_prime_factors: assumes "x \ 0" @@ -1325,10 +1304,10 @@ have "normalize x = prod_mset (prime_factorization x)" by (simp add: prod_mset_prime_factorization assms) also have "\ = (\p \ prime_factors x. p ^ count (prime_factorization x) p)" - by (subst prod_mset_multiplicity) (simp_all add: prime_factors_def) + by (subst prod_mset_multiplicity) simp_all also have "\ = (\p \ prime_factors x. p ^ multiplicity p x)" by (intro setprod.cong) - (simp_all add: assms count_prime_factorization_prime prime_factors_prime) + (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime) finally show ?thesis .. qed @@ -1361,8 +1340,8 @@ 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 dest: in_prime_factorization_imp_prime) - finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric]) + by (intro prime_factorization_prod_mset_primes) auto + finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric]) show "(\p. prime p \ f p = multiplicity p n)" proof safe @@ -1389,7 +1368,7 @@ lemma prime_factors_product: "x \ 0 \ y \ 0 \ prime_factors (x * y) = prime_factors x \ prime_factors y" - by (simp add: prime_factors_def prime_factorization_mult) + by (simp add: prime_factorization_mult) lemma multiplicity_distinct_prime_power: "prime p \ prime q \ p \ q \ multiplicity p (q ^ n) = 0" @@ -1406,7 +1385,6 @@ lemma dvd_prime_factors [intro]: "y \ 0 \ x dvd y \ prime_factors x \ prime_factors y" - unfolding prime_factors_def by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto (* RENAMED multiplicity_dvd *) @@ -1485,7 +1463,7 @@ prime_factorization (prod_mset (prime_factorization a #\ prime_factorization b))" by (simp add: gcd_factorial_def) also have "\ = prime_factorization a #\ prime_factorization b" - by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime) + by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed @@ -1497,7 +1475,7 @@ prime_factorization (prod_mset (prime_factorization a #\ prime_factorization b))" by (simp add: lcm_factorial_def) also have "\ = prime_factorization a #\ prime_factorization b" - by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime) + by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed @@ -1508,9 +1486,9 @@ from assms obtain x where x: "x \ A - {0}" by auto hence "Inf (prime_factorization ` (A - {0})) \# prime_factorization x" by (intro subset_mset.cInf_lower) simp_all - hence "\y. y \# Inf (prime_factorization ` (A - {0})) \ y \# prime_factorization x" + hence "\y. y \# Inf (prime_factorization ` (A - {0})) \ y \ prime_factors x" by (auto dest: mset_subset_eqD) - with in_prime_factorization_imp_prime[of _ x] + with in_prime_factors_imp_prime[of _ x] have "\p. p \# Inf (prime_factorization ` (A - {0})) \ prime p" by blast with assms show ?thesis by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes) @@ -1527,7 +1505,7 @@ next case False have "\y. y \# Sup (prime_factorization ` A) \ prime y" - by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime) + by (auto simp: in_Sup_multiset_iff assms) with assms False show ?thesis by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes) qed @@ -1551,7 +1529,7 @@ proof - have "normalize (prod_mset (prime_factorization a #\ prime_factorization b)) = prod_mset (prime_factorization a #\ prime_factorization b)" - by (intro normalize_prod_mset_primes) (auto simp: in_prime_factorization_imp_prime) + by (intro normalize_prod_mset_primes) auto thus ?thesis by (simp add: gcd_factorial_def) qed @@ -1564,8 +1542,7 @@ by (simp_all add: prime_factorization_subset_iff_dvd) hence "prime_factorization c \# prime_factorization (prod_mset (prime_factorization a #\ prime_factorization b))" - using False by (subst prime_factorization_prod_mset_primes) - (auto simp: in_prime_factorization_imp_prime) + using False by (subst prime_factorization_prod_mset_primes) auto with False show ?thesis by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric]) qed (auto simp: gcd_factorial_def that) @@ -1594,7 +1571,7 @@ hence "Inf (prime_factorization ` (A - {0})) \# prime_factorization x" by (intro subset_mset.cInf_lower) auto hence "prime p" if "p \# Inf (prime_factorization ` (A - {0}))" for p - using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime) + 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) @@ -1643,7 +1620,7 @@ 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 in_prime_factorization_imp_prime) + (auto simp: in_Sup_multiset_iff) with True show ?thesis by (simp add: Lcm_factorial_def) qed (auto simp: Lcm_factorial_def) @@ -1812,13 +1789,13 @@ proof - have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) also have "\ = ?rhs1" - by (auto simp: gcd_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization - count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong) + by (auto simp: gcd_factorial_def assms prod_mset_multiplicity + count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong) finally show "gcd x y = ?rhs1" . have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) also have "\ = ?rhs2" - by (auto simp: lcm_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization - count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong) + by (auto simp: lcm_factorial_def assms prod_mset_multiplicity + count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong) finally show "lcm x y = ?rhs2" . qed @@ -1880,4 +1857,3 @@ end end - diff -r b8482e12a2a8 -r 1c3dcb5fe6cb src/HOL/Number_Theory/Pocklington.thy --- a/src/HOL/Number_Theory/Pocklington.thy Fri Sep 16 12:30:55 2016 +0200 +++ b/src/HOL/Number_Theory/Pocklington.thy Fri Sep 16 12:30:55 2016 +0200 @@ -658,8 +658,8 @@ also have "\ = prod_mset (mset xs)" by (simp add: xs) also have "\ = foldr op * xs 1" by (induction xs) simp_all finally have "foldr op * xs 1 = n" .. - moreover have "\p\#mset xs. prime p" - by (subst xs) (auto dest: in_prime_factorization_imp_prime) + moreover from xs have "\p\#mset xs. prime p" + by auto ultimately have "primefact xs n" by (auto simp: primefact_def) thus ?thesis .. qed diff -r b8482e12a2a8 -r 1c3dcb5fe6cb src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Fri Sep 16 12:30:55 2016 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Fri Sep 16 12:30:55 2016 +0200 @@ -458,18 +458,17 @@ lemma prime_factors_gt_0_nat: "p \ prime_factors x \ p > (0::nat)" - by (simp add: prime_factors_prime prime_gt_0_nat) + by (simp add: in_prime_factors_imp_prime prime_gt_0_nat) lemma prime_factors_gt_0_int: "p \ prime_factors x \ p > (0::int)" - by (simp add: prime_factors_prime prime_gt_0_int) + by (simp add: in_prime_factors_imp_prime prime_gt_0_int) -lemma prime_factors_ge_0_int [elim]: +lemma prime_factors_ge_0_int [elim]: (* FIXME !? *) fixes n :: int shows "p \ prime_factors n \ p \ 0" - unfolding prime_factors_def - by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime) - + by (drule prime_factors_gt_0_int) simp + lemma prod_mset_prime_factorization_int: fixes n :: int assumes "n > 0" @@ -605,7 +604,7 @@ lemma prime_factors_setprod: assumes "finite A" and "0 \ f ` A" shows "prime_factors (setprod f A) = UNION A (prime_factors \ f)" - using assms by (simp add: prime_factors_def setprod_unfold_prod_mset prime_factorization_prod_mset) + using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset) lemma prime_factors_fact: "prime_factors (fact n) = {p \ {2..n}. prime p}" (is "?M = ?N") @@ -630,8 +629,7 @@ shows "p dvd fact n \ p \ n" using assms by (auto simp add: prime_factorization_subset_iff_dvd [symmetric] - prime_factorization_prime prime_factors_def [symmetric] - prime_factors_fact prime_ge_2_nat) + prime_factorization_prime prime_factors_fact prime_ge_2_nat) (* TODO Legacy names *) lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]