src/HOL/Number_Theory/Primes.thy
 changeset 63633 2accfb71e33b parent 63535 6887fda4541a child 63635 858a225ebb62
1.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Aug 08 14:13:14 2016 +0200
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Aug 08 17:47:51 2016 +0200
1.3 @@ -55,57 +55,55 @@
1.4  declare [[coercion int]]
1.5  declare [[coercion_enabled]]
1.7 -abbreviation (input) "prime \<equiv> is_prime"
1.8 -
1.9 -lemma is_prime_elem_nat_iff:
1.10 -  "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.11 +lemma prime_elem_nat_iff:
1.12 +  "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.13  proof safe
1.14 -  assume *: "is_prime_elem n"
1.15 +  assume *: "prime_elem n"
1.16    from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
1.17    thus "n > 1" by (cases n) simp_all
1.18    fix m assume m: "m dvd n" "m \<noteq> n"
1.19    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
1.20 -    by (intro irreducibleD' prime_imp_irreducible)
1.21 +    by (intro irreducibleD' prime_elem_imp_irreducible)
1.22    with m show "m = 1" by (auto dest: dvd_antisym)
1.23  next
1.24    assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
1.25 -  thus "is_prime_elem n"
1.26 -    by (auto simp: prime_iff_irreducible irreducible_altdef)
1.27 +  thus "prime_elem n"
1.28 +    by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
1.29  qed
1.31 -lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
1.32 -  by (simp add: is_prime_def)
1.33 +lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
1.34 +  by (simp add: prime_def)
1.36 -lemma is_prime_nat_iff:
1.37 -  "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.38 -  by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
1.39 +lemma prime_nat_iff:
1.40 +  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.41 +  by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
1.43 -lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
1.44 +lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
1.45  proof
1.46 -  assume "is_prime_elem n"
1.47 -  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
1.48 +  assume "prime_elem n"
1.49 +  thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
1.50  next
1.51 -  assume "is_prime_elem (nat (abs n))"
1.52 -  thus "is_prime_elem n"
1.53 -    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
1.54 +  assume "prime_elem (nat (abs n))"
1.55 +  thus "prime_elem n"
1.56 +    by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
1.57  qed
1.59 -lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
1.60 -  by (auto simp: is_prime_elem_int_nat_transfer)
1.61 +lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
1.62 +  by (auto simp: prime_elem_int_nat_transfer)
1.64 -lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
1.65 -  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
1.66 +lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
1.67 +  by (auto simp: prime_elem_int_nat_transfer prime_def)
1.69 -lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
1.70 -  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
1.71 +lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
1.72 +  by (auto simp: prime_elem_int_nat_transfer prime_def)
1.74 -lemma is_prime_int_iff:
1.75 -  "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.76 +lemma prime_int_iff:
1.77 +  "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.78  proof (intro iffI conjI allI impI; (elim conjE)?)
1.79 -  assume *: "is_prime n"
1.80 -  hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
1.81 +  assume *: "prime n"
1.82 +  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
1.83    from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
1.84 -    by (auto simp: is_prime_def zabs_def not_less split: if_splits)
1.85 +    by (auto simp: prime_def zabs_def not_less split: if_splits)
1.86    thus "n > 1" by presburger
1.87    fix m assume "m dvd n" \<open>m \<ge> 0\<close>
1.88    with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
1.89 @@ -121,8 +119,8 @@
1.90      with n(2) have "int m = 1 \<or> int m = n" by auto
1.91      thus "m = 1 \<or> m = nat n" by auto
1.92    qed
1.93 -  ultimately show "is_prime n"
1.94 -    unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
1.95 +  ultimately show "prime n"
1.96 +    unfolding prime_int_nat_transfer prime_nat_iff by auto
1.97  qed
1.100 @@ -131,7 +129,7 @@
1.101    shows   "\<not>n dvd p"
1.102  proof
1.103    assume "n dvd p"
1.104 -  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
1.105 +  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
1.106    from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
1.107      by (cases "n = 0") (auto dest!: dvd_imp_le)
1.108  qed
1.109 @@ -141,7 +139,7 @@
1.110    shows   "\<not>n dvd p"
1.111  proof
1.112    assume "n dvd p"
1.113 -  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
1.114 +  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
1.115    from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
1.116      by (auto dest!: zdvd_imp_le)
1.117  qed
1.118 @@ -153,60 +151,60 @@
1.119    by (intro prime_int_not_dvd) auto
1.121  lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
1.122 -  unfolding is_prime_int_iff by auto
1.123 +  unfolding prime_int_iff by auto
1.125  lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
1.126 -  unfolding is_prime_nat_iff by auto
1.127 +  unfolding prime_nat_iff by auto
1.129  lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
1.130 -  unfolding is_prime_int_iff by auto
1.131 +  unfolding prime_int_iff by auto
1.133  lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
1.134 -  unfolding is_prime_nat_iff by auto
1.135 +  unfolding prime_nat_iff by auto
1.137  lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
1.138 -  unfolding is_prime_nat_iff by auto
1.139 +  unfolding prime_nat_iff by auto
1.141  lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
1.142 -  unfolding is_prime_int_iff by auto
1.143 +  unfolding prime_int_iff by auto
1.145  lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
1.146 -  unfolding is_prime_nat_iff by auto
1.147 +  unfolding prime_nat_iff by auto
1.149  lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
1.150 -  unfolding is_prime_nat_iff by auto
1.151 +  unfolding prime_nat_iff by auto
1.153  lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
1.154 -  unfolding is_prime_int_iff by auto
1.155 +  unfolding prime_int_iff by auto
1.157  lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
1.158 -  unfolding is_prime_nat_iff by auto
1.159 +  unfolding prime_nat_iff by auto
1.161  lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
1.162 -  unfolding is_prime_int_iff by auto
1.163 +  unfolding prime_int_iff by auto
1.165  lemma prime_int_altdef:
1.166    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
1.167      m = 1 \<or> m = p))"
1.168 -  unfolding is_prime_int_iff by blast
1.169 +  unfolding prime_int_iff by blast
1.171  lemma not_prime_eq_prod_nat:
1.172    assumes "m > 1" "\<not>prime (m::nat)"
1.173    shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
1.174    using assms irreducible_altdef[of m]
1.175 -  by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
1.176 +  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
1.179  subsubsection \<open>Make prime naively executable\<close>
1.181  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
1.182 -  unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
1.183 +  unfolding One_nat_def [symmetric] by (rule not_prime_1)
1.185 -lemma is_prime_nat_iff':
1.186 +lemma prime_nat_iff':
1.187    "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
1.188  proof safe
1.189    assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
1.190 -  show "is_prime p" unfolding is_prime_nat_iff
1.191 +  show "prime p" unfolding prime_nat_iff
1.192    proof (intro conjI allI impI)
1.193      fix m assume "m dvd p"
1.194      with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
1.195 @@ -215,25 +213,25 @@
1.196      with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
1.197      ultimately show "m = 1 \<or> m = p" by simp
1.198    qed fact+
1.199 -qed (auto simp: is_prime_nat_iff)
1.200 +qed (auto simp: prime_nat_iff)
1.202  lemma prime_nat_code [code_unfold]:
1.203    "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
1.204 -  by (rule ext, rule is_prime_nat_iff')
1.205 +  by (rule ext, rule prime_nat_iff')
1.207 -lemma is_prime_int_iff':
1.208 +lemma prime_int_iff':
1.209    "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
1.210  proof
1.211    assume "?lhs"
1.212 -  thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
1.213 +  thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
1.214  next
1.215    assume "?rhs"
1.216 -  thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
1.217 +  thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
1.218  qed
1.220  lemma prime_int_code [code_unfold]:
1.221    "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
1.222 -  by (rule ext, rule is_prime_int_iff')
1.223 +  by (rule ext, rule prime_int_iff')
1.225  lemma prime_nat_simp:
1.226      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
1.227 @@ -245,10 +243,10 @@
1.229  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
1.231 -lemma two_is_prime_nat [simp]: "prime (2::nat)"
1.232 +lemma two_prime_nat [simp]: "prime (2::nat)"
1.233    by simp
1.235 -declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
1.236 +declare prime_int_nat_transfer[of "numeral m" for m, simp]
1.239  text\<open>A bit of regression testing:\<close>
1.240 @@ -282,7 +280,7 @@
1.241      then have "p dvd 1" by simp
1.242      then have "p <= 1" by auto
1.243      moreover from \<open>prime p\<close> have "p > 1"
1.244 -      using is_prime_nat_iff by blast
1.245 +      using prime_nat_iff by blast
1.246      ultimately have False by auto}
1.247    then have "n < p" by presburger
1.248    with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
1.249 @@ -313,7 +311,7 @@
1.250  proof -
1.251    from assms have
1.252      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
1.253 -    unfolding is_prime_nat_iff by auto
1.254 +    unfolding prime_nat_iff by auto
1.255    from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
1.256    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
1.257    have "p dvd p * q" by simp
1.258 @@ -332,7 +330,7 @@
1.259  next
1.260    case (Suc k x y)
1.261    from Suc.prems have pxy: "p dvd x*y" by auto
1.262 -  from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
1.263 +  from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
1.264    from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
1.265    {assume px: "p dvd x"
1.266      then obtain d where d: "x = p*d" unfolding dvd_def by blast
1.267 @@ -446,7 +444,7 @@
1.268    shows "\<exists>x y. a*x = Suc (p*y)"
1.269  proof -
1.270    have ap: "coprime a p"
1.271 -    by (metis gcd.commute p pa is_prime_imp_coprime)
1.272 +    by (metis gcd.commute p pa prime_imp_coprime)
1.273    moreover from p have "p \<noteq> 1" by auto
1.274    ultimately have "\<exists>x y. a * x = p * y + 1"
1.275      by (rule coprime_bezout_strong)
1.276 @@ -470,7 +468,7 @@
1.277    fixes n :: int
1.278    shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
1.279    unfolding prime_factors_def
1.280 -  by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
1.281 +  by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
1.283  lemma msetprod_prime_factorization_int:
1.284    fixes n :: int
1.285 @@ -480,7 +478,7 @@
1.287  lemma prime_factorization_exists_nat:
1.288    "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
1.289 -  using prime_factorization_exists[of n] by (auto simp: is_prime_def)
1.290 +  using prime_factorization_exists[of n] by (auto simp: prime_def)
1.292  lemma msetprod_prime_factorization_nat [simp]:
1.293    "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
1.294 @@ -499,7 +497,7 @@
1.295    assumes S_eq: "S = {p. 0 < f p}"
1.296      and "finite S"
1.297      and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
1.298 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
1.299 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
1.300    using assms by (intro prime_factorization_unique'') auto
1.302  lemma prime_factorization_unique_int:
1.303 @@ -507,7 +505,7 @@
1.304    assumes S_eq: "S = {p. 0 < f p}"
1.305      and "finite S"
1.306      and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
1.307 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
1.308 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
1.309    using assms by (intro prime_factorization_unique'') auto
1.311  lemma prime_factors_characterization_nat:
1.312 @@ -536,23 +534,23 @@
1.313    by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
1.315  lemma multiplicity_characterization_nat:
1.316 -  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow>
1.317 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
1.318      n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
1.319    by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
1.321  lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
1.322 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
1.323 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
1.324        multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
1.325    by (intro impI, rule multiplicity_characterization_nat) auto
1.327  lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
1.328 -    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
1.329 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
1.330    by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
1.331       (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
1.333  lemma multiplicity_characterization'_int [rule_format]:
1.334    "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
1.335 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
1.336 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
1.337        multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
1.338    by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
1.340 @@ -561,18 +559,18 @@
1.342  lemma multiplicity_eq_nat:
1.343    fixes x and y::nat
1.344 -  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.345 +  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.346    shows "x = y"
1.347    using multiplicity_eq_imp_eq[of x y] assms by simp
1.349  lemma multiplicity_eq_int:
1.350    fixes x y :: int
1.351 -  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.352 +  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.353    shows "x = y"
1.354    using multiplicity_eq_imp_eq[of x y] assms by simp
1.356  lemma multiplicity_prod_prime_powers:
1.357 -  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
1.358 +  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
1.359    shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
1.360  proof -
1.361    define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
1.362 @@ -592,7 +590,7 @@
1.363    also have "\<dots> = msetprod A"
1.364      by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
1.365    also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
1.366 -    by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
1.367 +    by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
1.368    also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
1.369      by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
1.370    also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
1.371 @@ -600,21 +598,21 @@
1.372  qed
1.374  (* TODO Legacy names *)
1.375 -lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
1.376 -lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
1.377 -lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
1.378 -lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
1.379 -lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
1.380 -lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
1.381 -lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
1.382 -lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
1.383 -lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
1.384 -lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
1.385 -lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
1.386 -lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
1.387 +lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
1.388 +lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
1.389 +lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
1.390 +lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
1.391 +lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
1.392 +lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
1.393 +lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
1.394 +lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
1.395 +lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
1.396 +lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
1.397 +lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
1.398 +lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
1.399  lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
1.400  lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
1.401 -lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
1.402 -lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
1.403 +lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
1.404 +lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
1.406  end
1.407 \ No newline at end of file