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.6  
     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.30  
    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.35  
    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.42  
    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.58  
    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.63  
    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.68  
    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.73  
    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.98  
    1.99  
   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.120  
   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.124  
   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.128  
   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.132  
   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.136  
   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.140  
   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.144  
   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.148  
   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.152  
   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.156  
   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.160  
   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.164  
   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.170  
   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.177  
   1.178  
   1.179  subsubsection \<open>Make prime naively executable\<close>
   1.180  
   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.184  
   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.201  
   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.206  
   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.219  
   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.224  
   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.228  
   1.229  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   1.230  
   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.234  
   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.237  
   1.238  
   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.282  
   1.283  lemma msetprod_prime_factorization_int:
   1.284    fixes n :: int
   1.285 @@ -480,7 +478,7 @@
   1.286  
   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.291  
   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.301  
   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.310  
   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.314  
   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.320  
   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.326  
   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.332  
   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.339  
   1.340 @@ -561,18 +559,18 @@
   1.341  
   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.348  
   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.355  
   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.373  
   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.405  
   1.406  end
   1.407 \ No newline at end of file