author haftmann Fri Sep 16 12:30:55 2016 +0200 (2016-09-16) changeset 63905 1c3dcb5fe6cb parent 63904 b8482e12a2a8 child 63906 fa799a8e4adc
prefer abbreviation for trivial set conversion
1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 16 12:30:55 2016 +0200
1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 16 12:30:55 2016 +0200
1.3 @@ -794,7 +794,7 @@
1.4  lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
1.5  proof -
1.6    have "Lcm_coeff_denoms (fract_poly p) = 1"
1.7 -    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
1.8 +    by (auto simp: set_coeffs_map_poly)
1.9    hence "fract_content (fract_poly p) =
1.10             to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
1.11      by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
1.12 @@ -1063,7 +1063,7 @@
1.13    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
1.14    have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1
1.15               normalize_field_poly unit_factor_field_poly" ..
1.16 -  from field_poly.in_prime_factorization_imp_prime[of p x] assms
1.17 +  from field_poly.in_prime_factors_imp_prime [of p x] assms
1.18      show ?thesis unfolding prime_elem_def dvd_field_poly
1.19        comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
1.20  qed
1.21 @@ -1314,7 +1314,7 @@
1.22    moreover from assms have "prod_mset B = [:content p:]"
1.23      by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
1.24    moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
1.25 -    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
1.26 +    by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
1.27    ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
1.28  qed
2.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 16 12:30:55 2016 +0200
2.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 16 12:30:55 2016 +0200
2.3 @@ -1,4 +1,3 @@
2.4 -
2.5  (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
2.6      Author:     Florian Haftmann, TU Muenchen
2.7  *)
2.8 @@ -982,6 +981,9 @@
2.9    qed simp_all
2.10  qed
2.12 +abbreviation prime_factors :: "'a \<Rightarrow> 'a set" where
2.13 +  "prime_factors a \<equiv> set_mset (prime_factorization a)"
2.14 +
2.15  lemma count_prime_factorization_nonprime:
2.16    "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
2.17    by transfer simp
2.18 @@ -1080,23 +1082,23 @@
2.19       (simp_all add: prime_factorization_unit prime_factorization_times_prime
2.20                      is_unit_normalize normalize_mult)
2.22 -lemma in_prime_factorization_iff:
2.23 -  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
2.24 +lemma in_prime_factors_iff:
2.25 +  "p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
2.26  proof -
2.27 -  have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
2.28 +  have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
2.29    also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
2.30     by (subst count_prime_factorization, cases "x = 0")
2.31        (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
2.32    finally show ?thesis .
2.33  qed
2.35 -lemma in_prime_factorization_imp_prime:
2.36 -  "p \<in># prime_factorization x \<Longrightarrow> prime p"
2.37 -  by (simp add: in_prime_factorization_iff)
2.38 +lemma in_prime_factors_imp_prime [intro]:
2.39 +  "p \<in> prime_factors x \<Longrightarrow> prime p"
2.40 +  by (simp add: in_prime_factors_iff)
2.42 -lemma in_prime_factorization_imp_dvd:
2.43 -  "p \<in># prime_factorization x \<Longrightarrow> p dvd x"
2.44 -  by (simp add: in_prime_factorization_iff)
2.45 +lemma in_prime_factors_imp_dvd [dest]:
2.46 +  "p \<in> prime_factors x \<Longrightarrow> p dvd x"
2.47 +  by (simp add: in_prime_factors_iff)
2.49  lemma multiplicity_self:
2.50    assumes "p \<noteq> 0" "\<not>is_unit p"
2.51 @@ -1197,10 +1199,10 @@
2.52      by (simp add: prod_mset_prime_factorization assms normalize_mult)
2.53    also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
2.54                 prime_factorization (x * y)"
2.55 -    by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factorization_imp_prime)
2.56 +    by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime)
2.57    also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
2.58                 prime_factorization x + prime_factorization y"
2.59 -    by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factorization_imp_prime)
2.60 +    by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime)
2.61    finally show ?thesis .
2.62  qed
2.64 @@ -1219,8 +1221,7 @@
2.65    have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
2.66      by (simp add: prod_mset_prime_factorization)
2.67    also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
2.68 -    by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd
2.69 -                     in_prime_factorization_imp_prime)
2.70 +    by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd)
2.71    finally show ?thesis ..
2.72  qed
2.74 @@ -1239,8 +1240,8 @@
2.75    with assms show ?thesis by simp
2.76  qed simp_all
2.78 -lemma zero_not_in_prime_factorization [simp]: "0 \<notin># prime_factorization x"
2.79 -  by (auto dest: in_prime_factorization_imp_prime)
2.80 +lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x"
2.81 +  by (auto dest: in_prime_factors_imp_prime)
2.84  lemma prime_elem_multiplicity_mult_distrib:
2.85 @@ -1283,40 +1284,18 @@
2.86    finally show ?thesis .
2.87  qed
2.89 -
2.90 -
2.91 -definition prime_factors where
2.92 -  "prime_factors x = set_mset (prime_factorization x)"
2.93 -
2.94 -lemma set_mset_prime_factorization:
2.95 -  "set_mset (prime_factorization x) = prime_factors x"
2.96 -  by (simp add: prime_factors_def)
2.97 -
2.98  lemma prime_factorsI:
2.99    "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
2.100 -  by (auto simp: prime_factors_def in_prime_factorization_iff)
2.102 -lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> prime p"
2.103 -  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
2.104 +  by (auto simp: in_prime_factors_iff)
2.106  lemma prime_prime_factors:
2.107 -  assumes "prime p"
2.108 -  shows "prime_factors p = {p}"
2.109 -  using assms by (simp add: prime_factors_def)
2.110 -    (drule prime_factorization_prime, simp)
2.112 -lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
2.113 -  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd)
2.115 -lemma prime_factors_finite [iff]:
2.116 -  "finite (prime_factors n)"
2.117 -  unfolding prime_factors_def by simp
2.118 +  "prime p \<Longrightarrow> prime_factors p = {p}"
2.119 +  by (drule prime_factorization_prime) simp
2.121  lemma prime_factors_altdef_multiplicity:
2.122    "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
2.123    by (cases "n = 0")
2.124 -     (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff
2.125 -        prime_imp_prime_elem in_prime_factorization_iff)
2.126 +     (auto simp: prime_multiplicity_gt_zero_iff in_prime_factors_iff)
2.128  lemma setprod_prime_factors:
2.129    assumes "x \<noteq> 0"
2.130 @@ -1325,10 +1304,10 @@
2.131    have "normalize x = prod_mset (prime_factorization x)"
2.132      by (simp add: prod_mset_prime_factorization assms)
2.133    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
2.134 -    by (subst prod_mset_multiplicity) (simp_all add: prime_factors_def)
2.135 +    by (subst prod_mset_multiplicity) simp_all
2.136    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
2.137      by (intro setprod.cong)
2.138 -      (simp_all add: assms count_prime_factorization_prime prime_factors_prime)
2.139 +      (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
2.140    finally show ?thesis ..
2.141  qed
2.143 @@ -1361,8 +1340,8 @@
2.144    also from S(1) have "prime_factorization (prod_mset A) = A"
2.145      by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
2.146    also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
2.147 -    by (intro prime_factorization_prod_mset_primes) (auto dest: in_prime_factorization_imp_prime)
2.148 -  finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
2.149 +    by (intro prime_factorization_prod_mset_primes) auto
2.150 +  finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
2.152    show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
2.153    proof safe
2.154 @@ -1389,7 +1368,7 @@
2.156  lemma prime_factors_product:
2.157    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
2.158 -  by (simp add: prime_factors_def prime_factorization_mult)
2.159 +  by (simp add: prime_factorization_mult)
2.161  lemma multiplicity_distinct_prime_power:
2.162    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
2.163 @@ -1406,7 +1385,6 @@
2.165  lemma dvd_prime_factors [intro]:
2.166    "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
2.167 -  unfolding prime_factors_def
2.168    by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
2.170  (* RENAMED multiplicity_dvd *)
2.171 @@ -1485,7 +1463,7 @@
2.172            prime_factorization (prod_mset (prime_factorization a #\<inter> prime_factorization b))"
2.173      by (simp add: gcd_factorial_def)
2.174    also have "\<dots> = prime_factorization a #\<inter> prime_factorization b"
2.175 -    by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime)
2.176 +    by (subst prime_factorization_prod_mset_primes) auto
2.177    finally show ?thesis .
2.178  qed
2.180 @@ -1497,7 +1475,7 @@
2.181            prime_factorization (prod_mset (prime_factorization a #\<union> prime_factorization b))"
2.182      by (simp add: lcm_factorial_def)
2.183    also have "\<dots> = prime_factorization a #\<union> prime_factorization b"
2.184 -    by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime)
2.185 +    by (subst prime_factorization_prod_mset_primes) auto
2.186    finally show ?thesis .
2.187  qed
2.189 @@ -1508,9 +1486,9 @@
2.190    from assms obtain x where x: "x \<in> A - {0}" by auto
2.191    hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
2.192      by (intro subset_mset.cInf_lower) simp_all
2.193 -  hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
2.194 +  hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> prime_factors x"
2.195      by (auto dest: mset_subset_eqD)
2.196 -  with in_prime_factorization_imp_prime[of _ x]
2.197 +  with in_prime_factors_imp_prime[of _ x]
2.198      have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
2.199    with assms show ?thesis
2.200      by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes)
2.201 @@ -1527,7 +1505,7 @@
2.202  next
2.203    case False
2.204    have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
2.205 -    by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
2.206 +    by (auto simp: in_Sup_multiset_iff assms)
2.207    with assms False show ?thesis
2.208      by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes)
2.209  qed
2.210 @@ -1551,7 +1529,7 @@
2.211  proof -
2.212    have "normalize (prod_mset (prime_factorization a #\<inter> prime_factorization b)) =
2.213            prod_mset (prime_factorization a #\<inter> prime_factorization b)"
2.214 -    by (intro normalize_prod_mset_primes) (auto simp: in_prime_factorization_imp_prime)
2.215 +    by (intro normalize_prod_mset_primes) auto
2.216    thus ?thesis by (simp add: gcd_factorial_def)
2.217  qed
2.219 @@ -1564,8 +1542,7 @@
2.220      by (simp_all add: prime_factorization_subset_iff_dvd)
2.221    hence "prime_factorization c \<subseteq>#
2.222             prime_factorization (prod_mset (prime_factorization a #\<inter> prime_factorization b))"
2.223 -    using False by (subst prime_factorization_prod_mset_primes)
2.224 -                   (auto simp: in_prime_factorization_imp_prime)
2.225 +    using False by (subst prime_factorization_prod_mset_primes) auto
2.226    with False show ?thesis
2.227      by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric])
2.228  qed (auto simp: gcd_factorial_def that)
2.229 @@ -1594,7 +1571,7 @@
2.230    hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
2.231      by (intro subset_mset.cInf_lower) auto
2.232    hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
2.233 -    using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
2.234 +    using that by (auto dest: mset_subset_eqD)
2.235    with False show ?thesis
2.236      by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
2.237  qed (simp_all add: Gcd_factorial_def)
2.238 @@ -1643,7 +1620,7 @@
2.239    hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
2.240             prod_mset (Sup (prime_factorization ` A))"
2.241      by (intro normalize_prod_mset_primes)
2.242 -       (auto simp: in_Sup_multiset_iff in_prime_factorization_imp_prime)
2.243 +       (auto simp: in_Sup_multiset_iff)
2.244    with True show ?thesis by (simp add: Lcm_factorial_def)
2.245  qed (auto simp: Lcm_factorial_def)
2.247 @@ -1812,13 +1789,13 @@
2.248  proof -
2.249    have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
2.250    also have "\<dots> = ?rhs1"
2.251 -    by (auto simp: gcd_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization
2.252 -          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
2.253 +    by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
2.254 +          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
2.255    finally show "gcd x y = ?rhs1" .
2.256    have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
2.257    also have "\<dots> = ?rhs2"
2.258 -    by (auto simp: lcm_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization
2.259 -          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
2.260 +    by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
2.261 +          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
2.262    finally show "lcm x y = ?rhs2" .
2.263  qed
2.265 @@ -1880,4 +1857,3 @@
2.266  end
2.268  end
3.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Fri Sep 16 12:30:55 2016 +0200
3.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Sep 16 12:30:55 2016 +0200
3.3 @@ -658,8 +658,8 @@
3.4    also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
3.5    also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
3.6    finally have "foldr op * xs 1 = n" ..
3.7 -  moreover have "\<forall>p\<in>#mset xs. prime p"
3.8 -    by (subst xs) (auto dest: in_prime_factorization_imp_prime)
3.9 +  moreover from xs have "\<forall>p\<in>#mset xs. prime p"
3.10 +    by auto
3.11    ultimately have "primefact xs n" by (auto simp: primefact_def)
3.12    thus ?thesis ..
3.13  qed
4.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 12:30:55 2016 +0200
4.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 12:30:55 2016 +0200
4.3 @@ -458,18 +458,17 @@
4.5  lemma prime_factors_gt_0_nat:
4.6    "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
4.7 -  by (simp add: prime_factors_prime prime_gt_0_nat)
4.8 +  by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
4.10  lemma prime_factors_gt_0_int:
4.11    "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
4.12 -  by (simp add: prime_factors_prime prime_gt_0_int)
4.13 +  by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
4.15 -lemma prime_factors_ge_0_int [elim]:
4.16 +lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
4.17    fixes n :: int
4.18    shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
4.19 -  unfolding prime_factors_def
4.20 -  by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
4.21 -
4.22 +  by (drule prime_factors_gt_0_int) simp
4.23 +
4.24  lemma prod_mset_prime_factorization_int:
4.25    fixes n :: int
4.26    assumes "n > 0"
4.27 @@ -605,7 +604,7 @@
4.28  lemma prime_factors_setprod:
4.29    assumes "finite A" and "0 \<notin> f ` A"
4.30    shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
4.31 -  using assms by (simp add: prime_factors_def setprod_unfold_prod_mset prime_factorization_prod_mset)
4.32 +  using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset)
4.34  lemma prime_factors_fact:
4.35    "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
4.36 @@ -630,8 +629,7 @@
4.37    shows "p dvd fact n \<longleftrightarrow> p \<le> n"
4.38    using assms
4.39    by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
4.40 -    prime_factorization_prime prime_factors_def [symmetric]
4.41 -    prime_factors_fact prime_ge_2_nat)
4.42 +    prime_factorization_prime prime_factors_fact prime_ge_2_nat)
4.44  (* TODO Legacy names *)
4.45  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]