--- 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 \<circ> quot_of_fract \<circ> 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 "\<forall>p. p \<in># B \<longrightarrow> 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
--- 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 \<Rightarrow> 'a set" where
+ "prime_factors a \<equiv> set_mset (prime_factorization a)"
+
lemma count_prime_factorization_nonprime:
"\<not>prime p \<Longrightarrow> 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 \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
+lemma in_prime_factors_iff:
+ "p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
proof -
- have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
+ have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> 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 \<in># prime_factorization x \<Longrightarrow> prime p"
- by (simp add: in_prime_factorization_iff)
+lemma in_prime_factors_imp_prime [intro]:
+ "p \<in> prime_factors x \<Longrightarrow> prime p"
+ by (simp add: in_prime_factors_iff)
-lemma in_prime_factorization_imp_dvd:
- "p \<in># prime_factorization x \<Longrightarrow> p dvd x"
- by (simp add: in_prime_factorization_iff)
+lemma in_prime_factors_imp_dvd [dest]:
+ "p \<in> prime_factors x \<Longrightarrow> p dvd x"
+ by (simp add: in_prime_factors_iff)
lemma multiplicity_self:
assumes "p \<noteq> 0" "\<not>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 \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
by (simp add: prod_mset_prime_factorization)
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
- 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 \<notin># prime_factorization x"
- by (auto dest: in_prime_factorization_imp_prime)
+lemma zero_not_in_prime_factors [simp]: "0 \<notin> 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 \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
- by (auto simp: prime_factors_def in_prime_factorization_iff)
-
-lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> 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 \<in> prime_factors x \<Longrightarrow> 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 \<Longrightarrow> prime_factors p = {p}"
+ by (drule prime_factorization_prime) simp
lemma prime_factors_altdef_multiplicity:
"prime_factors n = {p. prime p \<and> 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 \<noteq> 0"
@@ -1325,10 +1304,10 @@
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 add: prime_factors_def)
+ by (subst prod_mset_multiplicity) simp_all
also have "\<dots> = (\<Prod>p \<in> 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 "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
proof safe
@@ -1389,7 +1368,7 @@
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_factors_def prime_factorization_mult)
+ by (simp add: prime_factorization_mult)
lemma multiplicity_distinct_prime_power:
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
@@ -1406,7 +1385,6 @@
lemma dvd_prime_factors [intro]:
"y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> 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 #\<inter> prime_factorization b))"
by (simp add: gcd_factorial_def)
also have "\<dots> = prime_factorization a #\<inter> 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 #\<union> prime_factorization b))"
by (simp add: lcm_factorial_def)
also have "\<dots> = prime_factorization a #\<union> 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 \<in> A - {0}" by auto
hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
by (intro subset_mset.cInf_lower) simp_all
- hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
+ hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> 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 "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> 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 "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> 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 #\<inter> prime_factorization b)) =
prod_mset (prime_factorization a #\<inter> 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 \<subseteq>#
prime_factorization (prod_mset (prime_factorization a #\<inter> 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})) \<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 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 "\<dots> = ?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 "\<dots> = ?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
-
--- 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 "\<dots> = prod_mset (mset xs)" by (simp add: xs)
also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
finally have "foldr op * xs 1 = n" ..
- moreover have "\<forall>p\<in>#mset xs. prime p"
- by (subst xs) (auto dest: in_prime_factorization_imp_prime)
+ moreover from xs have "\<forall>p\<in>#mset xs. prime p"
+ by auto
ultimately have "primefact xs n" by (auto simp: primefact_def)
thus ?thesis ..
qed
--- 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 \<in> prime_factors x \<Longrightarrow> 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 \<in> prime_factors x \<Longrightarrow> 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 \<in> prime_factors n \<Longrightarrow> p \<ge> 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 \<notin> f ` A"
shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> 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 \<in> {2..n}. prime p}" (is "?M = ?N")
@@ -630,8 +629,7 @@
shows "p dvd fact n \<longleftrightarrow> p \<le> 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]