prefer abbreviation for trivial set conversion
authorhaftmann
Fri Sep 16 12:30:55 2016 +0200 (2016-09-16)
changeset 639051c3dcb5fe6cb
parent 63904 b8482e12a2a8
child 63906 fa799a8e4adc
prefer abbreviation for trivial set conversion
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
     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
    1.29  
     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.11  
    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.21  
    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.34  
    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.41  
    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.48  
    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.63  
    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.73  
    2.74 @@ -1239,8 +1240,8 @@
    2.75    with assms show ?thesis by simp
    2.76  qed simp_all
    2.77  
    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.82  
    2.83  
    2.84  lemma prime_elem_multiplicity_mult_distrib:
    2.85 @@ -1283,40 +1284,18 @@
    2.86    finally show ?thesis .
    2.87  qed
    2.88  
    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.101 -
   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.105  
   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.111 -
   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.114 -
   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.120  
   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.127  
   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.142  
   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.151    
   2.152    show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   2.153    proof safe
   2.154 @@ -1389,7 +1368,7 @@
   2.155  
   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.160  
   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.164  
   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.169  
   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.179  
   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.188  
   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.218  
   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.246  
   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.264  
   2.265 @@ -1880,4 +1857,3 @@
   2.266  end
   2.267  
   2.268  end
   2.269 -
     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.4  
     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.9  
    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.14  
    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.33  
    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.43  
    4.44  (* TODO Legacy names *)
    4.45  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]