is_prime -> prime
authoreberlm <eberlm@in.tum.de>
Mon Aug 08 17:47:51 2016 +0200 (2016-08-08)
changeset 636332accfb71e33b
parent 63627 6ddb43c6b711
child 63634 8711db9f078a
is_prime -> prime
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Polynomial_Factorial.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Proofs/Extraction/Euclid.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Aug 08 14:13:14 2016 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Mon Aug 08 17:47:51 2016 +0200
     1.3 @@ -2250,7 +2250,7 @@
     1.4  
     1.5  subsection \<open>Irreducible Elements are Prime\<close>
     1.6  
     1.7 -lemma (in factorial_monoid) irreducible_is_prime:
     1.8 +lemma (in factorial_monoid) irreducible_prime:
     1.9    assumes pirr: "irreducible G p"
    1.10      and pcarr: "p \<in> carrier G"
    1.11    shows "prime G p"
    1.12 @@ -2340,7 +2340,7 @@
    1.13  
    1.14  
    1.15  \<comment>"A version using @{const factors}, more complicated"
    1.16 -lemma (in factorial_monoid) factors_irreducible_is_prime:
    1.17 +lemma (in factorial_monoid) factors_irreducible_prime:
    1.18    assumes pirr: "irreducible G p"
    1.19      and pcarr: "p \<in> carrier G"
    1.20    shows "prime G p"
    1.21 @@ -3638,7 +3638,7 @@
    1.22  done
    1.23  
    1.24  sublocale factorial_monoid \<subseteq> primeness_condition_monoid
    1.25 -  by standard (rule irreducible_is_prime)
    1.26 +  by standard (rule irreducible_prime)
    1.27  
    1.28  
    1.29  lemma (in factorial_monoid) primeness_condition:
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Mon Aug 08 14:13:14 2016 +0200
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Mon Aug 08 17:47:51 2016 +0200
     2.3 @@ -15,8 +15,8 @@
     2.4  
     2.5  text\<open>needed in this form to prove Sylow's theorem\<close>
     2.6  corollary (in algebraic_semidom) div_combine: 
     2.7 -  "\<lbrakk>is_prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
     2.8 -  by (metis add_Suc_right mult.commute prime_power_dvd_cases)
     2.9 +  "\<lbrakk>prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
    2.10 +  by (metis add_Suc_right mult.commute prime_elem_power_dvd_cases)
    2.11  
    2.12  lemma exponent_p_a_m_k_equation: 
    2.13    fixes p :: nat
    2.14 @@ -61,16 +61,16 @@
    2.15    case (Suc k)
    2.16    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
    2.17    then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)"
    2.18 -    by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
    2.19 +    by (subst Suc_times_binomial_eq [symmetric], subst prime_elem_multiplicity_mult_distrib)
    2.20         (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
    2.21    with p * show ?case
    2.22 -    by (subst (asm) prime_multiplicity_mult_distrib) simp_all
    2.23 +    by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
    2.24  qed
    2.25  
    2.26  text\<open>The lemma above, with two changes of variables\<close>
    2.27  lemma p_not_div_choose:
    2.28    assumes "k < K" and "k \<le> n" 
    2.29 -      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p"
    2.30 +      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p"
    2.31      shows "multiplicity p (n choose k) = 0"
    2.32  apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
    2.33  apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
    2.34 @@ -78,7 +78,7 @@
    2.35  done
    2.36  
    2.37  proposition const_p_fac:
    2.38 -  assumes "m>0" and prime: "is_prime p"
    2.39 +  assumes "m>0" and prime: "prime p"
    2.40    shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
    2.41  proof-
    2.42    from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
    2.43 @@ -93,13 +93,13 @@
    2.44        by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
    2.45      also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
    2.46      with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
    2.47 -      by (subst prime_multiplicity_mult_distrib) auto
    2.48 +      by (subst prime_elem_multiplicity_mult_distrib) auto
    2.49      also have "\<dots> = a + multiplicity p m" 
    2.50 -      using prime p by (subst prime_multiplicity_mult_distrib) simp_all
    2.51 +      using prime p by (subst prime_elem_multiplicity_mult_distrib) simp_all
    2.52      finally show ?thesis .
    2.53    qed
    2.54    then show ?thesis
    2.55 -    using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
    2.56 +    using prime p by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
    2.57  qed
    2.58  
    2.59  end
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Mon Aug 08 14:13:14 2016 +0200
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Mon Aug 08 17:47:51 2016 +0200
     3.3 @@ -99,7 +99,7 @@
     3.4    assumes I_notcarr: "carrier R \<noteq> I"
     3.5      and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
     3.6  
     3.7 -lemma (in primeideal) is_primeideal: "primeideal I R"
     3.8 +lemma (in primeideal) primeideal: "primeideal I R"
     3.9    by (rule primeideal_axioms)
    3.10  
    3.11  lemma primeidealI:
    3.12 @@ -769,7 +769,7 @@
    3.13  qed
    3.14  
    3.15  text \<open>In a cring every maximal ideal is prime\<close>
    3.16 -lemma (in cring) maximalideal_is_prime:
    3.17 +lemma (in cring) maximalideal_prime:
    3.18    assumes "maximalideal I R"
    3.19    shows "primeideal I R"
    3.20  proof -
     4.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Aug 08 14:13:14 2016 +0200
     4.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Aug 08 17:47:51 2016 +0200
     4.3 @@ -251,7 +251,7 @@
     4.4    then obtain x where "1 = x * p" by best
     4.5    then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
     4.6    then show False using prime
     4.7 -    by (auto dest!: abs_zmult_eq_1 simp: is_prime_def)
     4.8 +    by (auto dest!: abs_zmult_eq_1 simp: prime_def)
     4.9  qed
    4.10  
    4.11  
     5.1 --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Mon Aug 08 14:13:14 2016 +0200
     5.2 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Mon Aug 08 17:47:51 2016 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4  (* Goldblatt: Exercise 5.11(3a) - p 57  *)
     5.5  lemma starprime:
     5.6    "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
     5.7 -by (transfer, auto simp add: is_prime_nat_iff)
     5.8 +by (transfer, auto simp add: prime_nat_iff)
     5.9  
    5.10  (* Goldblatt Exercise 5.11(3b) - p 57  *)
    5.11  lemma hyperprime_factor_exists [rule_format]:
    5.12 @@ -277,7 +277,7 @@
    5.13  apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
    5.14  apply (force simp add: starprime_def)
    5.15    apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime 
    5.16 -           imageE insert_iff mem_Collect_eq not_is_prime_0)
    5.17 +           imageE insert_iff mem_Collect_eq not_prime_0)
    5.18  done
    5.19  
    5.20  end
     6.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Mon Aug 08 14:13:14 2016 +0200
     6.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Mon Aug 08 17:47:51 2016 +0200
     6.3 @@ -295,8 +295,8 @@
     6.4      from 2 show ?thesis
     6.5        apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
     6.6          dest: prime_gt_Suc_0_nat)
     6.7 -      apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
     6.8 -      apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
     6.9 +      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_iff)
    6.10 +      apply (metis One_nat_def Suc_le_eq aux prime_nat_iff)
    6.11        done
    6.12    qed
    6.13  qed
     7.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Aug 08 14:13:14 2016 +0200
     7.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Aug 08 17:47:51 2016 +0200
     7.3 @@ -411,7 +411,7 @@
     7.4    interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
     7.5      by standard (rule lcm_gcd_eucl_facts; assumption)+
     7.6    fix p assume p: "irreducible p"
     7.7 -  thus "is_prime_elem p" by (rule irreducible_imp_prime_gcd)
     7.8 +  thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd)
     7.9  qed
    7.10  
    7.11  lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial"
     8.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Aug 08 14:13:14 2016 +0200
     8.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Aug 08 17:47:51 2016 +0200
     8.3 @@ -54,51 +54,51 @@
     8.4  lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
     8.5    by (simp add: irreducible_def)
     8.6  
     8.7 -definition is_prime_elem :: "'a \<Rightarrow> bool" where
     8.8 -  "is_prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
     8.9 +definition prime_elem :: "'a \<Rightarrow> bool" where
    8.10 +  "prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
    8.11  
    8.12 -lemma not_is_prime_elem_zero [simp]: "\<not>is_prime_elem 0"
    8.13 -  by (simp add: is_prime_elem_def)
    8.14 +lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0"
    8.15 +  by (simp add: prime_elem_def)
    8.16  
    8.17 -lemma is_prime_elem_not_unit: "is_prime_elem p \<Longrightarrow> \<not>p dvd 1"
    8.18 -  by (simp add: is_prime_elem_def)
    8.19 +lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1"
    8.20 +  by (simp add: prime_elem_def)
    8.21  
    8.22 -lemma is_prime_elemI:
    8.23 -    "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> is_prime_elem p"
    8.24 -  by (simp add: is_prime_elem_def)
    8.25 +lemma prime_elemI:
    8.26 +    "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> prime_elem p"
    8.27 +  by (simp add: prime_elem_def)
    8.28  
    8.29 -lemma prime_divides_productD:
    8.30 -    "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
    8.31 -  by (simp add: is_prime_elem_def)
    8.32 +lemma prime_elem_dvd_multD:
    8.33 +    "prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
    8.34 +  by (simp add: prime_elem_def)
    8.35  
    8.36 -lemma prime_dvd_mult_iff:
    8.37 -  "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
    8.38 -  by (auto simp: is_prime_elem_def)
    8.39 +lemma prime_elem_dvd_mult_iff:
    8.40 +  "prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
    8.41 +  by (auto simp: prime_elem_def)
    8.42  
    8.43 -lemma not_is_prime_elem_one [simp]:
    8.44 -  "\<not> is_prime_elem 1"
    8.45 -  by (auto dest: is_prime_elem_not_unit)
    8.46 +lemma not_prime_elem_one [simp]:
    8.47 +  "\<not> prime_elem 1"
    8.48 +  by (auto dest: prime_elem_not_unit)
    8.49  
    8.50 -lemma is_prime_elem_not_zeroI:
    8.51 -  assumes "is_prime_elem p"
    8.52 +lemma prime_elem_not_zeroI:
    8.53 +  assumes "prime_elem p"
    8.54    shows "p \<noteq> 0"
    8.55    using assms by (auto intro: ccontr)
    8.56  
    8.57  
    8.58 -lemma is_prime_elem_dvd_power: 
    8.59 -  "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    8.60 -  by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
    8.61 +lemma prime_elem_dvd_power: 
    8.62 +  "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    8.63 +  by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
    8.64  
    8.65 -lemma is_prime_elem_dvd_power_iff:
    8.66 -  "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    8.67 -  by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
    8.68 +lemma prime_elem_dvd_power_iff:
    8.69 +  "prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    8.70 +  by (auto dest: prime_elem_dvd_power intro: dvd_trans)
    8.71  
    8.72 -lemma is_prime_elem_imp_nonzero [simp]:
    8.73 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
    8.74 -  unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
    8.75 +lemma prime_elem_imp_nonzero [simp]:
    8.76 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0"
    8.77 +  unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
    8.78  
    8.79 -lemma is_prime_elem_imp_not_one [simp]:
    8.80 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 1"
    8.81 +lemma prime_elem_imp_not_one [simp]:
    8.82 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1"
    8.83    unfolding ASSUMPTION_def by auto
    8.84  
    8.85  end
    8.86 @@ -110,42 +110,42 @@
    8.87  lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
    8.88    by (subst mult.commute) (rule mult_unit_dvd_iff)
    8.89  
    8.90 -lemma prime_imp_irreducible:
    8.91 -  assumes "is_prime_elem p"
    8.92 +lemma prime_elem_imp_irreducible:
    8.93 +  assumes "prime_elem p"
    8.94    shows   "irreducible p"
    8.95  proof (rule irreducibleI)
    8.96    fix a b
    8.97    assume p_eq: "p = a * b"
    8.98    with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
    8.99    from p_eq have "p dvd a * b" by simp
   8.100 -  with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
   8.101 +  with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
   8.102    with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
   8.103    thus "a dvd 1 \<or> b dvd 1"
   8.104      by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
   8.105 -qed (insert assms, simp_all add: is_prime_elem_def)
   8.106 +qed (insert assms, simp_all add: prime_elem_def)
   8.107  
   8.108 -lemma is_prime_elem_mono:
   8.109 -  assumes "is_prime_elem p" "\<not>q dvd 1" "q dvd p"
   8.110 -  shows   "is_prime_elem q"
   8.111 +lemma prime_elem_mono:
   8.112 +  assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
   8.113 +  shows   "prime_elem q"
   8.114  proof -
   8.115    from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
   8.116    hence "p dvd q * r" by simp
   8.117 -  with \<open>is_prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_divides_productD)
   8.118 +  with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD)
   8.119    hence "p dvd q"
   8.120    proof
   8.121      assume "p dvd r"
   8.122      then obtain s where s: "r = p * s" by (elim dvdE)
   8.123      from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
   8.124 -    with \<open>is_prime_elem p\<close> have "q dvd 1"
   8.125 +    with \<open>prime_elem p\<close> have "q dvd 1"
   8.126        by (subst (asm) mult_cancel_left) auto
   8.127      with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
   8.128    qed
   8.129  
   8.130    show ?thesis
   8.131 -  proof (rule is_prime_elemI)
   8.132 +  proof (rule prime_elemI)
   8.133      fix a b assume "q dvd (a * b)"
   8.134      with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
   8.135 -    with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
   8.136 +    with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
   8.137      with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
   8.138    qed (insert assms, auto)
   8.139  qed
   8.140 @@ -178,12 +178,12 @@
   8.141    "irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)"
   8.142    using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
   8.143  
   8.144 -lemma is_prime_elem_multD:
   8.145 -  assumes "is_prime_elem (a * b)"
   8.146 +lemma prime_elem_multD:
   8.147 +  assumes "prime_elem (a * b)"
   8.148    shows "is_unit a \<or> is_unit b"
   8.149  proof -
   8.150 -  from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: is_prime_elem_not_zeroI)
   8.151 -  moreover from assms prime_divides_productD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
   8.152 +  from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI)
   8.153 +  moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
   8.154      by auto
   8.155    ultimately show ?thesis
   8.156      using dvd_times_left_cancel_iff [of a b 1]
   8.157 @@ -191,36 +191,62 @@
   8.158      by auto
   8.159  qed
   8.160  
   8.161 -lemma is_prime_elemD2:
   8.162 -  assumes "is_prime_elem p" and "a dvd p" and "\<not> is_unit a"
   8.163 +lemma prime_elemD2:
   8.164 +  assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a"
   8.165    shows "p dvd a"
   8.166  proof -
   8.167    from \<open>a dvd p\<close> obtain b where "p = a * b" ..
   8.168 -  with \<open>is_prime_elem p\<close> is_prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
   8.169 +  with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
   8.170    with \<open>p = a * b\<close> show ?thesis
   8.171      by (auto simp add: mult_unit_dvd_iff)
   8.172  qed
   8.173  
   8.174 +lemma prime_elem_dvd_msetprodE:
   8.175 +  assumes "prime_elem p"
   8.176 +  assumes dvd: "p dvd msetprod A"
   8.177 +  obtains a where "a \<in># A" and "p dvd a"
   8.178 +proof -
   8.179 +  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   8.180 +  proof (induct A)
   8.181 +    case empty then show ?case
   8.182 +    using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
   8.183 +  next
   8.184 +    case (add A a)
   8.185 +    then have "p dvd msetprod A * a" by simp
   8.186 +    with \<open>prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
   8.187 +      by (blast dest: prime_elem_dvd_multD)
   8.188 +    then show ?case proof cases
   8.189 +      case B then show ?thesis by auto
   8.190 +    next
   8.191 +      case A
   8.192 +      with add.hyps obtain b where "b \<in># A" "p dvd b"
   8.193 +        by auto
   8.194 +      then show ?thesis by auto
   8.195 +    qed
   8.196 +  qed
   8.197 +  with that show thesis by blast
   8.198 +qed
   8.199 +
   8.200  context
   8.201  begin
   8.202  
   8.203 -private lemma is_prime_elem_powerD:
   8.204 -  assumes "is_prime_elem (p ^ n)"
   8.205 -  shows   "is_prime_elem p \<and> n = 1"
   8.206 +private lemma prime_elem_powerD:
   8.207 +  assumes "prime_elem (p ^ n)"
   8.208 +  shows   "prime_elem p \<and> n = 1"
   8.209  proof (cases n)
   8.210    case (Suc m)
   8.211    note assms
   8.212    also from Suc have "p ^ n = p * p^m" by simp
   8.213 -  finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
   8.214 -  moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
   8.215 +  finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD)
   8.216 +  moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
   8.217    ultimately have "is_unit (p ^ m)" by simp
   8.218    with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
   8.219    with Suc assms show ?thesis by simp
   8.220  qed (insert assms, simp_all)
   8.221  
   8.222 -lemma is_prime_elem_power_iff:
   8.223 -  "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
   8.224 -  by (auto dest: is_prime_elem_powerD)
   8.225 +lemma prime_elem_power_iff:
   8.226 +  "prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1"
   8.227 +  by (auto dest: prime_elem_powerD)
   8.228  
   8.229  end
   8.230  
   8.231 @@ -229,17 +255,17 @@
   8.232    by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
   8.233          mult_unit_dvd_iff dvd_mult_unit_iff)
   8.234  
   8.235 -lemma is_prime_elem_mult_unit_left:
   8.236 -  "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
   8.237 -  by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
   8.238 +lemma prime_elem_mult_unit_left:
   8.239 +  "is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p"
   8.240 +  by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
   8.241  
   8.242 -lemma prime_dvd_cases:
   8.243 -  assumes pk: "p*k dvd m*n" and p: "is_prime_elem p"
   8.244 +lemma prime_elem_dvd_cases:
   8.245 +  assumes pk: "p*k dvd m*n" and p: "prime_elem p"
   8.246    shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
   8.247  proof -
   8.248    have "p dvd m*n" using dvd_mult_left pk by blast
   8.249    then consider "p dvd m" | "p dvd n"
   8.250 -    using p prime_dvd_mult_iff by blast
   8.251 +    using p prime_elem_dvd_mult_iff by blast
   8.252    then show ?thesis
   8.253    proof cases
   8.254      case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
   8.255 @@ -254,8 +280,8 @@
   8.256    qed
   8.257  qed
   8.258  
   8.259 -lemma prime_power_dvd_prod:
   8.260 -  assumes pc: "p^c dvd m*n" and p: "is_prime_elem p"
   8.261 +lemma prime_elem_power_dvd_prod:
   8.262 +  assumes pc: "p^c dvd m*n" and p: "prime_elem p"
   8.263    shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
   8.264  using pc
   8.265  proof (induct c arbitrary: m n)
   8.266 @@ -263,7 +289,7 @@
   8.267  next
   8.268    case (Suc c)
   8.269    consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
   8.270 -    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
   8.271 +    using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
   8.272    then show ?case
   8.273    proof cases
   8.274      case (1 x) 
   8.275 @@ -284,217 +310,40 @@
   8.276  lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
   8.277    by arith
   8.278  
   8.279 -lemma prime_power_dvd_cases:
   8.280 -     "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
   8.281 -  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
   8.282 -
   8.283 -end
   8.284 -
   8.285 -context normalization_semidom
   8.286 -begin
   8.287 -
   8.288 -lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
   8.289 -  using irreducible_mult_unit_left[of "1 div unit_factor x" x]
   8.290 -  by (cases "x = 0") (simp_all add: unit_div_commute)
   8.291 -
   8.292 -lemma is_prime_elem_normalize_iff [simp]: "is_prime_elem (normalize x) = is_prime_elem x"
   8.293 -  using is_prime_elem_mult_unit_left[of "1 div unit_factor x" x]
   8.294 -  by (cases "x = 0") (simp_all add: unit_div_commute)
   8.295 -
   8.296 -definition is_prime :: "'a \<Rightarrow> bool" where
   8.297 -  "is_prime p \<longleftrightarrow> is_prime_elem p \<and> normalize p = p"
   8.298 -
   8.299 -lemma not_is_prime_0 [simp]: "\<not>is_prime 0" by (simp add: is_prime_def)
   8.300 -
   8.301 -lemma not_is_prime_unit: "is_unit x \<Longrightarrow> \<not>is_prime x"
   8.302 -  using is_prime_elem_not_unit[of x] by (auto simp add: is_prime_def)
   8.303 -
   8.304 -lemma not_is_prime_1 [simp]: "\<not>is_prime 1" by (simp add: not_is_prime_unit)
   8.305 -
   8.306 -lemma is_primeI: "is_prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> is_prime x"
   8.307 -  by (simp add: is_prime_def)
   8.308 -
   8.309 -lemma prime_imp_prime_elem [dest]: "is_prime p \<Longrightarrow> is_prime_elem p"
   8.310 -  by (simp add: is_prime_def)
   8.311 -
   8.312 -lemma normalize_is_prime: "is_prime p \<Longrightarrow> normalize p = p"
   8.313 -  by (simp add: is_prime_def)
   8.314 -
   8.315 -lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
   8.316 -  by (auto simp add: is_prime_def)
   8.317 -
   8.318 -lemma is_prime_power_iff:
   8.319 -  "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
   8.320 -  by (auto simp: is_prime_def is_prime_elem_power_iff)
   8.321 -
   8.322 -lemma is_prime_elem_not_unit' [simp]:
   8.323 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
   8.324 -  unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
   8.325 -
   8.326 -lemma is_prime_imp_nonzero [simp]:
   8.327 -  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 0"
   8.328 -  unfolding ASSUMPTION_def is_prime_def by auto
   8.329 -
   8.330 -lemma is_prime_imp_not_one [simp]:
   8.331 -  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 1"
   8.332 -  unfolding ASSUMPTION_def by auto
   8.333 -
   8.334 -lemma is_prime_not_unit' [simp]:
   8.335 -  "ASSUMPTION (is_prime x) \<Longrightarrow> \<not>is_unit x"
   8.336 -  unfolding ASSUMPTION_def is_prime_def by auto
   8.337 -
   8.338 -lemma is_prime_normalize' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> normalize x = x"
   8.339 -  unfolding ASSUMPTION_def is_prime_def by simp
   8.340 -
   8.341 -lemma unit_factor_is_prime: "is_prime x \<Longrightarrow> unit_factor x = 1"
   8.342 -  using unit_factor_normalize[of x] unfolding is_prime_def by auto
   8.343 -
   8.344 -lemma unit_factor_is_prime' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> unit_factor x = 1"
   8.345 -  unfolding ASSUMPTION_def by (rule unit_factor_is_prime)
   8.346 -
   8.347 -lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> is_prime_elem x"
   8.348 -  by (simp add: is_prime_def ASSUMPTION_def)
   8.349 -
   8.350 - lemma is_prime_elem_associated:
   8.351 -  assumes "is_prime_elem p" and "is_prime_elem q" and "q dvd p"
   8.352 -  shows "normalize q = normalize p"
   8.353 -using \<open>q dvd p\<close> proof (rule associatedI)
   8.354 -  from \<open>is_prime_elem q\<close> have "\<not> is_unit q"
   8.355 -    by (simp add: is_prime_elem_not_unit)
   8.356 -  with \<open>is_prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
   8.357 -    by (blast intro: is_prime_elemD2)
   8.358 -qed
   8.359 -
   8.360 -lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
   8.361 -  by (intro prime_divides_productD) simp_all
   8.362 -
   8.363 -lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   8.364 -  by (auto dest: is_prime_dvd_multD)
   8.365 -
   8.366 -lemma is_prime_dvd_power: 
   8.367 -  "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   8.368 -  by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
   8.369 -
   8.370 -lemma is_prime_dvd_power_iff:
   8.371 -  "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
   8.372 -  by (intro is_prime_elem_dvd_power_iff) simp_all
   8.373 +lemma prime_elem_power_dvd_cases:
   8.374 +     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
   8.375 +  using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem)
   8.376  
   8.377 -lemma prime_dvd_msetprodE:
   8.378 -  assumes "is_prime_elem p"
   8.379 -  assumes dvd: "p dvd msetprod A"
   8.380 -  obtains a where "a \<in># A" and "p dvd a"
   8.381 -proof -
   8.382 -  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   8.383 -  proof (induct A)
   8.384 -    case empty then show ?case
   8.385 -    using \<open>is_prime_elem p\<close> by (simp add: is_prime_elem_not_unit)
   8.386 -  next
   8.387 -    case (add A a)
   8.388 -    then have "p dvd msetprod A * a" by simp
   8.389 -    with \<open>is_prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
   8.390 -      by (blast dest: prime_divides_productD)
   8.391 -    then show ?case proof cases
   8.392 -      case B then show ?thesis by auto
   8.393 -    next
   8.394 -      case A
   8.395 -      with add.hyps obtain b where "b \<in># A" "p dvd b"
   8.396 -        by auto
   8.397 -      then show ?thesis by auto
   8.398 -    qed
   8.399 -  qed
   8.400 -  with that show thesis by blast
   8.401 -qed
   8.402 -
   8.403 -lemma msetprod_subset_imp_dvd:
   8.404 -  assumes "A \<subseteq># B"
   8.405 -  shows   "msetprod A dvd msetprod B"
   8.406 -proof -
   8.407 -  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
   8.408 -  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
   8.409 -  also have "msetprod A dvd \<dots>" by simp
   8.410 -  finally show ?thesis .
   8.411 -qed
   8.412 -
   8.413 -lemma prime_dvd_msetprod_iff: "is_prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
   8.414 -  by (induction A) (simp_all add: prime_dvd_mult_iff prime_imp_prime_elem, blast+)
   8.415 +lemma prime_elem_not_unit' [simp]:
   8.416 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
   8.417 +  unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
   8.418  
   8.419 -lemma primes_dvd_imp_eq:
   8.420 -  assumes "is_prime p" "is_prime q" "p dvd q"
   8.421 -  shows   "p = q"
   8.422 -proof -
   8.423 -  from assms have "irreducible q" by (simp add: prime_imp_irreducible is_prime_def)
   8.424 -  from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
   8.425 -  with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
   8.426 -  with assms show "p = q" by simp
   8.427 -qed
   8.428 -
   8.429 -lemma prime_dvd_msetprod_primes_iff:
   8.430 -  assumes "is_prime p" "\<And>q. q \<in># A \<Longrightarrow> is_prime q"
   8.431 -  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
   8.432 -proof -
   8.433 -  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
   8.434 -  also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
   8.435 -  finally show ?thesis .
   8.436 -qed
   8.437 -
   8.438 -lemma msetprod_primes_dvd_imp_subset:
   8.439 -  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
   8.440 -  shows   "A \<subseteq># B"
   8.441 -using assms
   8.442 -proof (induction A arbitrary: B)
   8.443 -  case empty
   8.444 -  thus ?case by simp
   8.445 -next
   8.446 -  case (add A p B)
   8.447 -  hence p: "is_prime p" by simp
   8.448 -  define B' where "B' = B - {#p#}"
   8.449 -  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
   8.450 -  with add.prems have "p \<in># B"
   8.451 -    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
   8.452 -  hence B: "B = B' + {#p#}" by (simp add: B'_def)
   8.453 -  from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   8.454 -  thus ?case by (simp add: B)
   8.455 -qed
   8.456 -
   8.457 -lemma normalize_msetprod_primes:
   8.458 -  "(\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
   8.459 -proof (induction A)
   8.460 -  case (add A p)
   8.461 -  hence "is_prime p" by simp
   8.462 -  hence "normalize p = p" by simp
   8.463 -  with add show ?case by (simp add: normalize_mult)
   8.464 -qed simp_all
   8.465 -
   8.466 -lemma msetprod_dvd_msetprod_primes_iff:
   8.467 -  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
   8.468 -  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
   8.469 -  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
   8.470 -
   8.471 -lemma prime_dvd_power_iff:
   8.472 -  assumes "is_prime_elem p"
   8.473 +lemma prime_elem_dvd_power_iff:
   8.474 +  assumes "prime_elem p"
   8.475    shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   8.476 -  using assms by (induct n) (auto dest: is_prime_elem_not_unit prime_divides_productD)
   8.477 +  using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
   8.478  
   8.479  lemma prime_power_dvd_multD:
   8.480 -  assumes "is_prime_elem p"
   8.481 +  assumes "prime_elem p"
   8.482    assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   8.483    shows "p ^ n dvd b"
   8.484 -using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
   8.485 +  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> 
   8.486 +proof (induct n arbitrary: b)
   8.487    case 0 then show ?case by simp
   8.488  next
   8.489    case (Suc n) show ?case
   8.490    proof (cases "n = 0")
   8.491 -    case True with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   8.492 -      by (simp add: prime_dvd_mult_iff)
   8.493 +    case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   8.494 +      by (simp add: prime_elem_dvd_mult_iff)
   8.495    next
   8.496      case False then have "n > 0" by simp
   8.497 -    from \<open>is_prime_elem p\<close> have "p \<noteq> 0" by auto
   8.498 +    from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto
   8.499      from Suc.prems have *: "p * p ^ n dvd a * b"
   8.500        by simp
   8.501      then have "p dvd a * b"
   8.502        by (rule dvd_mult_left)
   8.503 -    with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   8.504 -      by (simp add: prime_dvd_mult_iff)
   8.505 +    with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   8.506 +      by (simp add: prime_elem_dvd_mult_iff)
   8.507      moreover define c where "c = b div p"
   8.508      ultimately have b: "b = p * c" by simp
   8.509      with * have "p * p ^ n dvd p * (a * c)"
   8.510 @@ -508,6 +357,158 @@
   8.511    qed
   8.512  qed
   8.513  
   8.514 +end
   8.515 +
   8.516 +context normalization_semidom
   8.517 +begin
   8.518 +
   8.519 +lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
   8.520 +  using irreducible_mult_unit_left[of "1 div unit_factor x" x]
   8.521 +  by (cases "x = 0") (simp_all add: unit_div_commute)
   8.522 +
   8.523 +lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
   8.524 +  using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
   8.525 +  by (cases "x = 0") (simp_all add: unit_div_commute)
   8.526 +
   8.527 +lemma prime_elem_associated:
   8.528 +  assumes "prime_elem p" and "prime_elem q" and "q dvd p"
   8.529 +  shows "normalize q = normalize p"
   8.530 +using \<open>q dvd p\<close> proof (rule associatedI)
   8.531 +  from \<open>prime_elem q\<close> have "\<not> is_unit q"
   8.532 +    by (auto simp add: prime_elem_not_unit)
   8.533 +  with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
   8.534 +    by (blast intro: prime_elemD2)
   8.535 +qed
   8.536 +
   8.537 +definition prime :: "'a \<Rightarrow> bool" where
   8.538 +  "prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p"
   8.539 +
   8.540 +lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def)
   8.541 +
   8.542 +lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x"
   8.543 +  using prime_elem_not_unit[of x] by (auto simp add: prime_def)
   8.544 +
   8.545 +lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit)
   8.546 +
   8.547 +lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x"
   8.548 +  by (simp add: prime_def)
   8.549 +
   8.550 +lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p"
   8.551 +  by (simp add: prime_def)
   8.552 +
   8.553 +lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p"
   8.554 +  by (simp add: prime_def)
   8.555 +
   8.556 +lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p"
   8.557 +  by (auto simp add: prime_def)
   8.558 +
   8.559 +lemma prime_power_iff:
   8.560 +  "prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1"
   8.561 +  by (auto simp: prime_def prime_elem_power_iff)
   8.562 +
   8.563 +lemma prime_imp_nonzero [simp]:
   8.564 +  "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0"
   8.565 +  unfolding ASSUMPTION_def prime_def by auto
   8.566 +
   8.567 +lemma prime_imp_not_one [simp]:
   8.568 +  "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1"
   8.569 +  unfolding ASSUMPTION_def by auto
   8.570 +
   8.571 +lemma prime_not_unit' [simp]:
   8.572 +  "ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x"
   8.573 +  unfolding ASSUMPTION_def prime_def by auto
   8.574 +
   8.575 +lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x"
   8.576 +  unfolding ASSUMPTION_def prime_def by simp
   8.577 +
   8.578 +lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1"
   8.579 +  using unit_factor_normalize[of x] unfolding prime_def by auto
   8.580 +
   8.581 +lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1"
   8.582 +  unfolding ASSUMPTION_def by (rule unit_factor_prime)
   8.583 +
   8.584 +lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x"
   8.585 +  by (simp add: prime_def ASSUMPTION_def)
   8.586 +
   8.587 +lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
   8.588 +  by (intro prime_elem_dvd_multD) simp_all
   8.589 +
   8.590 +lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   8.591 +  by (auto dest: prime_dvd_multD)
   8.592 +
   8.593 +lemma prime_dvd_power: 
   8.594 +  "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   8.595 +  by (auto dest!: prime_elem_dvd_power simp: prime_def)
   8.596 +
   8.597 +lemma prime_dvd_power_iff:
   8.598 +  "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
   8.599 +  by (subst prime_elem_dvd_power_iff) simp_all
   8.600 +
   8.601 +lemma msetprod_subset_imp_dvd:
   8.602 +  assumes "A \<subseteq># B"
   8.603 +  shows   "msetprod A dvd msetprod B"
   8.604 +proof -
   8.605 +  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
   8.606 +  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
   8.607 +  also have "msetprod A dvd \<dots>" by simp
   8.608 +  finally show ?thesis .
   8.609 +qed
   8.610 +
   8.611 +lemma prime_dvd_msetprod_iff: "prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
   8.612 +  by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
   8.613 +
   8.614 +lemma primes_dvd_imp_eq:
   8.615 +  assumes "prime p" "prime q" "p dvd q"
   8.616 +  shows   "p = q"
   8.617 +proof -
   8.618 +  from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
   8.619 +  from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
   8.620 +  with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
   8.621 +  with assms show "p = q" by simp
   8.622 +qed
   8.623 +
   8.624 +lemma prime_dvd_msetprod_primes_iff:
   8.625 +  assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
   8.626 +  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
   8.627 +proof -
   8.628 +  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
   8.629 +  also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
   8.630 +  finally show ?thesis .
   8.631 +qed
   8.632 +
   8.633 +lemma msetprod_primes_dvd_imp_subset:
   8.634 +  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
   8.635 +  shows   "A \<subseteq># B"
   8.636 +using assms
   8.637 +proof (induction A arbitrary: B)
   8.638 +  case empty
   8.639 +  thus ?case by simp
   8.640 +next
   8.641 +  case (add A p B)
   8.642 +  hence p: "prime p" by simp
   8.643 +  define B' where "B' = B - {#p#}"
   8.644 +  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
   8.645 +  with add.prems have "p \<in># B"
   8.646 +    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
   8.647 +  hence B: "B = B' + {#p#}" by (simp add: B'_def)
   8.648 +  from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   8.649 +  thus ?case by (simp add: B)
   8.650 +qed
   8.651 +
   8.652 +lemma normalize_msetprod_primes:
   8.653 +  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
   8.654 +proof (induction A)
   8.655 +  case (add A p)
   8.656 +  hence "prime p" by simp
   8.657 +  hence "normalize p = p" by simp
   8.658 +  with add show ?case by (simp add: normalize_mult)
   8.659 +qed simp_all
   8.660 +
   8.661 +lemma msetprod_dvd_msetprod_primes_iff:
   8.662 +  assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
   8.663 +  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
   8.664 +  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
   8.665 +
   8.666  lemma is_unit_msetprod_iff:
   8.667    "is_unit (msetprod A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
   8.668    by (induction A) (auto simp: is_unit_mult_iff)
   8.669 @@ -516,7 +517,7 @@
   8.670    by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
   8.671  
   8.672  lemma is_unit_msetprod_primes_iff:
   8.673 -  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
   8.674 +  assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
   8.675    shows   "is_unit (msetprod A) \<longleftrightarrow> A = {#}"
   8.676  proof
   8.677    assume unit: "is_unit (msetprod A)"
   8.678 @@ -524,16 +525,16 @@
   8.679    proof (intro multiset_emptyI notI)
   8.680      fix x assume "x \<in># A"
   8.681      with unit have "is_unit x" by (subst (asm) is_unit_msetprod_iff) blast
   8.682 -    moreover from \<open>x \<in># A\<close> have "is_prime x" by (rule assms)
   8.683 +    moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
   8.684      ultimately show False by simp
   8.685    qed
   8.686  qed simp_all
   8.687  
   8.688  lemma msetprod_primes_irreducible_imp_prime:
   8.689    assumes irred: "irreducible (msetprod A)"
   8.690 -  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
   8.691 -  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
   8.692 -  assumes C: "\<And>x. x \<in># C \<Longrightarrow> is_prime x"
   8.693 +  assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   8.694 +  assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   8.695 +  assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
   8.696    assumes dvd: "msetprod A dvd msetprod B * msetprod C"
   8.697    shows   "msetprod A dvd msetprod B \<or> msetprod A dvd msetprod C"
   8.698  proof -
   8.699 @@ -564,8 +565,8 @@
   8.700  qed
   8.701  
   8.702  lemma msetprod_primes_finite_divisor_powers:
   8.703 -  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
   8.704 -  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
   8.705 +  assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   8.706 +  assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   8.707    assumes "A \<noteq> {#}"
   8.708    shows   "finite {n. msetprod A ^ n dvd msetprod B}"
   8.709  proof -
   8.710 @@ -594,10 +595,10 @@
   8.711  context semiring_gcd
   8.712  begin
   8.713  
   8.714 -lemma irreducible_imp_prime_gcd:
   8.715 +lemma irreducible_imp_prime_elem_gcd:
   8.716    assumes "irreducible x"
   8.717 -  shows   "is_prime_elem x"
   8.718 -proof (rule is_prime_elemI)
   8.719 +  shows   "prime_elem x"
   8.720 +proof (rule prime_elemI)
   8.721    fix a b assume "x dvd a * b"
   8.722    from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
   8.723    from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
   8.724 @@ -605,77 +606,77 @@
   8.725      by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
   8.726  qed (insert assms, auto simp: irreducible_not_unit)
   8.727  
   8.728 -lemma is_prime_elem_imp_coprime:
   8.729 -  assumes "is_prime_elem p" "\<not>p dvd n"
   8.730 +lemma prime_elem_imp_coprime:
   8.731 +  assumes "prime_elem p" "\<not>p dvd n"
   8.732    shows   "coprime p n"
   8.733  proof (rule coprimeI)
   8.734    fix d assume "d dvd p" "d dvd n"
   8.735    show "is_unit d"
   8.736    proof (rule ccontr)
   8.737      assume "\<not>is_unit d"
   8.738 -    from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
   8.739 -      by (rule is_prime_elemD2)
   8.740 +    from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
   8.741 +      by (rule prime_elemD2)
   8.742      from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
   8.743      with \<open>\<not>p dvd n\<close> show False by contradiction
   8.744    qed
   8.745  qed
   8.746  
   8.747 -lemma is_prime_imp_coprime:
   8.748 -  assumes "is_prime p" "\<not>p dvd n"
   8.749 +lemma prime_imp_coprime:
   8.750 +  assumes "prime p" "\<not>p dvd n"
   8.751    shows   "coprime p n"
   8.752 -  using assms by (simp add: is_prime_elem_imp_coprime)
   8.753 +  using assms by (simp add: prime_elem_imp_coprime)
   8.754  
   8.755 -lemma is_prime_elem_imp_power_coprime: 
   8.756 -  "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   8.757 -  by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
   8.758 +lemma prime_elem_imp_power_coprime: 
   8.759 +  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   8.760 +  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
   8.761  
   8.762 -lemma is_prime_imp_power_coprime: 
   8.763 -  "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   8.764 -  by (simp add: is_prime_elem_imp_power_coprime)
   8.765 +lemma prime_imp_power_coprime: 
   8.766 +  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   8.767 +  by (simp add: prime_elem_imp_power_coprime)
   8.768  
   8.769 -lemma prime_divprod_pow:
   8.770 -  assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   8.771 +lemma prime_elem_divprod_pow:
   8.772 +  assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   8.773    shows   "p^n dvd a \<or> p^n dvd b"
   8.774    using assms
   8.775  proof -
   8.776    from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
   8.777 -    by (auto simp: coprime is_prime_elem_def)
   8.778 +    by (auto simp: coprime prime_elem_def)
   8.779    with p have "coprime (p^n) a \<or> coprime (p^n) b" 
   8.780 -    by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
   8.781 +    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
   8.782    with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
   8.783  qed
   8.784  
   8.785  lemma primes_coprime: 
   8.786 -  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   8.787 -  using is_prime_imp_coprime primes_dvd_imp_eq by blast
   8.788 +  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   8.789 +  using prime_imp_coprime primes_dvd_imp_eq by blast
   8.790  
   8.791  end
   8.792  
   8.793  
   8.794  class factorial_semiring = normalization_semidom +
   8.795    assumes prime_factorization_exists:
   8.796 -            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
   8.797 +            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
   8.798  begin
   8.799  
   8.800  lemma prime_factorization_exists':
   8.801    assumes "x \<noteq> 0"
   8.802 -  obtains A where "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "msetprod A = normalize x"
   8.803 +  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "msetprod A = normalize x"
   8.804  proof -
   8.805    from prime_factorization_exists[OF assms] obtain A
   8.806 -    where A: "\<And>x. x \<in># A \<Longrightarrow> is_prime_elem x" "msetprod A = normalize x" by blast
   8.807 +    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "msetprod A = normalize x" by blast
   8.808    define A' where "A' = image_mset normalize A"
   8.809    have "msetprod A' = normalize (msetprod A)"
   8.810      by (simp add: A'_def normalize_msetprod)
   8.811    also note A(2)
   8.812    finally have "msetprod A' = normalize x" by simp
   8.813 -  moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> is_prime x" by (auto simp: is_prime_def A'_def)
   8.814 +  moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
   8.815    ultimately show ?thesis by (intro that[of A']) blast
   8.816  qed
   8.817  
   8.818 -lemma irreducible_imp_prime:
   8.819 +lemma irreducible_imp_prime_elem:
   8.820    assumes "irreducible x"
   8.821 -  shows   "is_prime_elem x"
   8.822 -proof (rule is_prime_elemI)
   8.823 +  shows   "prime_elem x"
   8.824 +proof (rule prime_elemI)
   8.825    fix a b assume dvd: "x dvd a * b"
   8.826    from assms have "x \<noteq> 0" by auto
   8.827    show "x dvd a \<or> x dvd b"
   8.828 @@ -708,12 +709,12 @@
   8.829  
   8.830  lemma finite_prime_divisors:
   8.831    assumes "x \<noteq> 0"
   8.832 -  shows   "finite {p. is_prime p \<and> p dvd x}"
   8.833 +  shows   "finite {p. prime p \<and> p dvd x}"
   8.834  proof -
   8.835    from prime_factorization_exists'[OF assms] guess A . note A = this
   8.836 -  have "{p. is_prime p \<and> p dvd x} \<subseteq> set_mset A"
   8.837 +  have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
   8.838    proof safe
   8.839 -    fix p assume p: "is_prime p" and dvd: "p dvd x"
   8.840 +    fix p assume p: "prime p" and dvd: "p dvd x"
   8.841      from dvd have "p dvd normalize x" by simp
   8.842      also from A have "normalize x = msetprod A" by simp
   8.843      finally show "p \<in># A" using p A by (subst (asm) prime_dvd_msetprod_primes_iff)
   8.844 @@ -722,23 +723,23 @@
   8.845    ultimately show ?thesis by (rule finite_subset)
   8.846  qed
   8.847  
   8.848 -lemma prime_iff_irreducible: "is_prime_elem x \<longleftrightarrow> irreducible x"
   8.849 -  by (blast intro: irreducible_imp_prime prime_imp_irreducible)
   8.850 +lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
   8.851 +  by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
   8.852  
   8.853  lemma prime_divisor_exists:
   8.854    assumes "a \<noteq> 0" "\<not>is_unit a"
   8.855 -  shows   "\<exists>b. b dvd a \<and> is_prime b"
   8.856 +  shows   "\<exists>b. b dvd a \<and> prime b"
   8.857  proof -
   8.858    from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   8.859    moreover from A and assms have "A \<noteq> {#}" by auto
   8.860    then obtain x where "x \<in># A" by blast
   8.861 -  with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
   8.862 +  with A(1) have *: "x dvd msetprod A" "prime x" by (auto simp: dvd_msetprod)
   8.863    with A have "x dvd a" by simp
   8.864    with * show ?thesis by blast
   8.865  qed
   8.866  
   8.867  lemma prime_divisors_induct [case_names zero unit factor]:
   8.868 -  assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
   8.869 +  assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
   8.870    shows   "P x"
   8.871  proof (cases "x = 0")
   8.872    case False
   8.873 @@ -746,7 +747,7 @@
   8.874    from A(1) have "P (unit_factor x * msetprod A)"
   8.875    proof (induction A)
   8.876      case (add A p)
   8.877 -    from add.prems have "is_prime p" by simp
   8.878 +    from add.prems have "prime p" by simp
   8.879      moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
   8.880      ultimately have "P (p * (unit_factor x * msetprod A))" by (rule assms(3))
   8.881      thus ?case by (simp add: mult_ac)
   8.882 @@ -755,18 +756,18 @@
   8.883  qed (simp_all add: assms(1))
   8.884  
   8.885  lemma no_prime_divisors_imp_unit:
   8.886 -  assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime_elem b"
   8.887 +  assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b"
   8.888    shows "is_unit a"
   8.889  proof (rule ccontr)
   8.890    assume "\<not>is_unit a"
   8.891    from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
   8.892 -  with assms(2)[of b] show False by (simp add: is_prime_def)
   8.893 +  with assms(2)[of b] show False by (simp add: prime_def)
   8.894  qed
   8.895  
   8.896  lemma prime_divisorE:
   8.897    assumes "a \<noteq> 0" and "\<not> is_unit a"
   8.898 -  obtains p where "is_prime p" and "p dvd a"
   8.899 -  using assms no_prime_divisors_imp_unit unfolding is_prime_def by blast
   8.900 +  obtains p where "prime p" and "p dvd a"
   8.901 +  using assms no_prime_divisors_imp_unit unfolding prime_def by blast
   8.902  
   8.903  definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
   8.904    "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
   8.905 @@ -864,17 +865,17 @@
   8.906  lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
   8.907    by (simp add: multiplicity_def)
   8.908  
   8.909 -lemma prime_multiplicity_eq_zero_iff:
   8.910 -  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   8.911 +lemma prime_elem_multiplicity_eq_zero_iff:
   8.912 +  "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   8.913    by (rule multiplicity_eq_zero_iff) simp_all
   8.914  
   8.915  lemma prime_multiplicity_other:
   8.916 -  assumes "is_prime p" "is_prime q" "p \<noteq> q"
   8.917 +  assumes "prime p" "prime q" "p \<noteq> q"
   8.918    shows   "multiplicity p q = 0"
   8.919 -  using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
   8.920 +  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
   8.921  
   8.922  lemma prime_multiplicity_gt_zero_iff:
   8.923 -  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   8.924 +  "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   8.925    by (rule multiplicity_gt_zero_iff) simp_all
   8.926  
   8.927  lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
   8.928 @@ -943,8 +944,8 @@
   8.929    "p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
   8.930    by (simp add: multiplicity_same_power')
   8.931  
   8.932 -lemma multiplicity_prime_times_other:
   8.933 -  assumes "is_prime_elem p" "\<not>p dvd q"
   8.934 +lemma multiplicity_prime_elem_times_other:
   8.935 +  assumes "prime_elem p" "\<not>p dvd q"
   8.936    shows   "multiplicity p (q * x) = multiplicity p x"
   8.937  proof (cases "x = 0")
   8.938    case False
   8.939 @@ -959,38 +960,38 @@
   8.940      from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
   8.941      from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
   8.942      also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
   8.943 -    also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_dvd_mult_iff) fact+
   8.944 +    also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
   8.945      also from assms y have "\<dots> \<longleftrightarrow> False" by simp
   8.946      finally show "\<not>(p ^ Suc n dvd q * x)" by blast
   8.947    qed
   8.948  qed simp_all
   8.949  
   8.950  lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
   8.951 -  "\<lambda>x p. if is_prime p then multiplicity p x else 0"
   8.952 +  "\<lambda>x p. if prime p then multiplicity p x else 0"
   8.953    unfolding multiset_def
   8.954  proof clarify
   8.955    fix x :: 'a
   8.956 -  show "finite {p. 0 < (if is_prime p then multiplicity p x else 0)}" (is "finite ?A")
   8.957 +  show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
   8.958    proof (cases "x = 0")
   8.959      case False
   8.960 -    from False have "?A \<subseteq> {p. is_prime p \<and> p dvd x}"
   8.961 +    from False have "?A \<subseteq> {p. prime p \<and> p dvd x}"
   8.962        by (auto simp: multiplicity_gt_zero_iff)
   8.963 -    moreover from False have "finite {p. is_prime p \<and> p dvd x}"
   8.964 +    moreover from False have "finite {p. prime p \<and> p dvd x}"
   8.965        by (rule finite_prime_divisors)
   8.966      ultimately show ?thesis by (rule finite_subset)
   8.967    qed simp_all
   8.968  qed
   8.969  
   8.970  lemma count_prime_factorization_nonprime:
   8.971 -  "\<not>is_prime p \<Longrightarrow> count (prime_factorization x) p = 0"
   8.972 +  "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
   8.973    by transfer simp
   8.974  
   8.975  lemma count_prime_factorization_prime:
   8.976 -  "is_prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
   8.977 +  "prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
   8.978    by transfer simp
   8.979  
   8.980  lemma count_prime_factorization:
   8.981 -  "count (prime_factorization x) p = (if is_prime p then multiplicity p x else 0)"
   8.982 +  "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
   8.983    by transfer simp
   8.984  
   8.985  lemma unit_imp_no_irreducible_divisors:
   8.986 @@ -999,9 +1000,9 @@
   8.987    using assms dvd_unit_imp_unit irreducible_not_unit by blast
   8.988  
   8.989  lemma unit_imp_no_prime_divisors:
   8.990 -  assumes "is_unit x" "is_prime_elem p"
   8.991 +  assumes "is_unit x" "prime_elem p"
   8.992    shows   "\<not>p dvd x"
   8.993 -  using unit_imp_no_irreducible_divisors[OF assms(1) prime_imp_irreducible[OF assms(2)]] .
   8.994 +  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
   8.995  
   8.996  lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
   8.997    by (simp add: multiset_eq_iff count_prime_factorization)
   8.998 @@ -1013,7 +1014,7 @@
   8.999    {
  8.1000      assume x: "x \<noteq> 0" "\<not>is_unit x"
  8.1001      {
  8.1002 -      fix p assume p: "is_prime p"
  8.1003 +      fix p assume p: "prime p"
  8.1004        have "count (prime_factorization x) p = 0" by (simp add: *)
  8.1005        also from p have "count (prime_factorization x) p = multiplicity p x"
  8.1006          by (rule count_prime_factorization_prime)
  8.1007 @@ -1029,7 +1030,7 @@
  8.1008    proof
  8.1009      assume x: "is_unit x"
  8.1010      {
  8.1011 -      fix p assume p: "is_prime p"
  8.1012 +      fix p assume p: "prime p"
  8.1013        from p x have "multiplicity p x = 0"
  8.1014          by (subst multiplicity_eq_zero_iff)
  8.1015             (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
  8.1016 @@ -1044,7 +1045,7 @@
  8.1017  proof (rule multiset_eqI)
  8.1018    fix p :: 'a
  8.1019    show "count (prime_factorization x) p = count {#} p"
  8.1020 -  proof (cases "is_prime p")
  8.1021 +  proof (cases "prime p")
  8.1022      case True
  8.1023      with assms have "multiplicity p x = 0"
  8.1024        by (subst multiplicity_eq_zero_iff)
  8.1025 @@ -1057,17 +1058,17 @@
  8.1026    by (simp add: prime_factorization_unit)
  8.1027  
  8.1028  lemma prime_factorization_times_prime:
  8.1029 -  assumes "x \<noteq> 0" "is_prime p"
  8.1030 +  assumes "x \<noteq> 0" "prime p"
  8.1031    shows   "prime_factorization (p * x) = {#p#} + prime_factorization x"
  8.1032  proof (rule multiset_eqI)
  8.1033    fix q :: 'a
  8.1034 -  consider "\<not>is_prime q" | "p = q" | "is_prime q" "p \<noteq> q" by blast
  8.1035 +  consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast
  8.1036    thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
  8.1037    proof cases
  8.1038 -    assume q: "is_prime q" "p \<noteq> q"
  8.1039 +    assume q: "prime q" "p \<noteq> q"
  8.1040      with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
  8.1041      with q assms show ?thesis
  8.1042 -      by (simp add: multiplicity_prime_times_other count_prime_factorization)
  8.1043 +      by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
  8.1044    qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
  8.1045  qed
  8.1046  
  8.1047 @@ -1080,17 +1081,17 @@
  8.1048                      is_unit_normalize normalize_mult)
  8.1049  
  8.1050  lemma in_prime_factorization_iff:
  8.1051 -  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
  8.1052 +  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  8.1053  proof -
  8.1054    have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
  8.1055 -  also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
  8.1056 +  also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  8.1057     by (subst count_prime_factorization, cases "x = 0")
  8.1058        (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
  8.1059    finally show ?thesis .
  8.1060  qed
  8.1061  
  8.1062  lemma in_prime_factorization_imp_prime:
  8.1063 -  "p \<in># prime_factorization x \<Longrightarrow> is_prime p"
  8.1064 +  "p \<in># prime_factorization x \<Longrightarrow> prime p"
  8.1065    by (simp add: in_prime_factorization_iff)
  8.1066  
  8.1067  lemma in_prime_factorization_imp_dvd:
  8.1068 @@ -1111,18 +1112,18 @@
  8.1069  qed
  8.1070  
  8.1071  lemma prime_factorization_prime:
  8.1072 -  assumes "is_prime p"
  8.1073 +  assumes "prime p"
  8.1074    shows   "prime_factorization p = {#p#}"
  8.1075  proof (rule multiset_eqI)
  8.1076    fix q :: 'a
  8.1077 -  consider "\<not>is_prime q" | "q = p" | "is_prime q" "q \<noteq> p" by blast
  8.1078 +  consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast
  8.1079    thus "count (prime_factorization p) q = count {#p#} q"
  8.1080      by cases (insert assms, auto dest: primes_dvd_imp_eq
  8.1081                  simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
  8.1082  qed
  8.1083  
  8.1084  lemma prime_factorization_msetprod_primes:
  8.1085 -  assumes "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
  8.1086 +  assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
  8.1087    shows   "prime_factorization (msetprod A) = A"
  8.1088    using assms
  8.1089  proof (induction A)
  8.1090 @@ -1204,7 +1205,7 @@
  8.1091  qed
  8.1092  
  8.1093  lemma prime_factorization_prime_power:
  8.1094 -  "is_prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
  8.1095 +  "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
  8.1096    by (induction n)
  8.1097       (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
  8.1098  
  8.1099 @@ -1242,8 +1243,8 @@
  8.1100    by (auto dest: in_prime_factorization_imp_prime)
  8.1101  
  8.1102  
  8.1103 -lemma prime_multiplicity_mult_distrib:
  8.1104 -  assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
  8.1105 +lemma prime_elem_multiplicity_mult_distrib:
  8.1106 +  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
  8.1107    shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
  8.1108  proof -
  8.1109    have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
  8.1110 @@ -1259,23 +1260,23 @@
  8.1111    finally show ?thesis .
  8.1112  qed
  8.1113  
  8.1114 -lemma prime_multiplicity_power_distrib:
  8.1115 -  assumes "is_prime_elem p" "x \<noteq> 0"
  8.1116 +lemma prime_elem_multiplicity_power_distrib:
  8.1117 +  assumes "prime_elem p" "x \<noteq> 0"
  8.1118    shows   "multiplicity p (x ^ n) = n * multiplicity p x"
  8.1119 -  by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
  8.1120 +  by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
  8.1121  
  8.1122 -lemma prime_multiplicity_msetprod_distrib:
  8.1123 -  assumes "is_prime_elem p" "0 \<notin># A"
  8.1124 +lemma prime_elem_multiplicity_msetprod_distrib:
  8.1125 +  assumes "prime_elem p" "0 \<notin># A"
  8.1126    shows   "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
  8.1127 -  using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
  8.1128 +  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
  8.1129  
  8.1130 -lemma prime_multiplicity_setprod_distrib:
  8.1131 -  assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
  8.1132 +lemma prime_elem_multiplicity_setprod_distrib:
  8.1133 +  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
  8.1134    shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
  8.1135  proof -
  8.1136    have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
  8.1137      using assms by (subst setprod_unfold_msetprod)
  8.1138 -                   (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum 
  8.1139 +                   (simp_all add: prime_elem_multiplicity_msetprod_distrib setsum_unfold_msetsum 
  8.1140                        multiset.map_comp o_def)
  8.1141    also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
  8.1142      by (induction A rule: finite_induct) simp_all
  8.1143 @@ -1292,10 +1293,10 @@
  8.1144    by (simp add: prime_factors_def)
  8.1145  
  8.1146  lemma prime_factorsI:
  8.1147 -  "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
  8.1148 +  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
  8.1149    by (auto simp: prime_factors_def in_prime_factorization_iff)
  8.1150  
  8.1151 -lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
  8.1152 +lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> prime p"
  8.1153    by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
  8.1154  
  8.1155  lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
  8.1156 @@ -1306,7 +1307,7 @@
  8.1157    unfolding prime_factors_def by simp
  8.1158  
  8.1159  lemma prime_factors_altdef_multiplicity:
  8.1160 -  "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
  8.1161 +  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
  8.1162    by (cases "n = 0")
  8.1163       (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff 
  8.1164          prime_imp_prime_elem in_prime_factorization_iff)
  8.1165 @@ -1335,8 +1336,8 @@
  8.1166  lemma prime_factorization_unique'':
  8.1167    assumes S_eq: "S = {p. 0 < f p}"
  8.1168      and "finite S"
  8.1169 -    and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
  8.1170 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  8.1171 +    and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
  8.1172 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  8.1173  proof
  8.1174    define A where "A = Abs_multiset f"
  8.1175    from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
  8.1176 @@ -1357,15 +1358,15 @@
  8.1177      by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
  8.1178    finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
  8.1179    
  8.1180 -  show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  8.1181 +  show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  8.1182    proof safe
  8.1183 -    fix p :: 'a assume p: "is_prime p"
  8.1184 +    fix p :: 'a assume p: "prime p"
  8.1185      have "multiplicity p n = multiplicity p (normalize n)" by simp
  8.1186      also have "normalize n = msetprod A" 
  8.1187        by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
  8.1188      also from p set_mset_A S(1) 
  8.1189      have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
  8.1190 -      by (intro prime_multiplicity_msetprod_distrib) auto
  8.1191 +      by (intro prime_elem_multiplicity_msetprod_distrib) auto
  8.1192      also from S(1) p
  8.1193      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
  8.1194        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
  8.1195 @@ -1374,10 +1375,10 @@
  8.1196    qed
  8.1197  qed
  8.1198  
  8.1199 -lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
  8.1200 +lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
  8.1201    by (rule multiplicity_self) auto
  8.1202  
  8.1203 -lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
  8.1204 +lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
  8.1205    by (subst multiplicity_same_power') auto
  8.1206  
  8.1207  lemma prime_factors_product: 
  8.1208 @@ -1385,8 +1386,8 @@
  8.1209    by (simp add: prime_factors_def prime_factorization_mult)
  8.1210  
  8.1211  lemma multiplicity_distinct_prime_power:
  8.1212 -  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
  8.1213 -  by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
  8.1214 +  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
  8.1215 +  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
  8.1216  
  8.1217  lemma dvd_imp_multiplicity_le:
  8.1218    assumes "a dvd b" "b \<noteq> 0"
  8.1219 @@ -1404,7 +1405,7 @@
  8.1220  
  8.1221  (* RENAMED multiplicity_dvd *)
  8.1222  lemma multiplicity_le_imp_dvd:
  8.1223 -  assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  8.1224 +  assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  8.1225    shows   "x dvd y"
  8.1226  proof (cases "y = 0")
  8.1227    case False
  8.1228 @@ -1417,17 +1418,17 @@
  8.1229    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
  8.1230    by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
  8.1231  
  8.1232 -lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
  8.1233 +lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
  8.1234    by (auto intro: prime_factorsI)
  8.1235  
  8.1236  lemma multiplicity_eq_imp_eq:
  8.1237    assumes "x \<noteq> 0" "y \<noteq> 0"
  8.1238 -  assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  8.1239 +  assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  8.1240    shows   "normalize x = normalize y"
  8.1241    using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
  8.1242  
  8.1243  lemma prime_factorization_unique':
  8.1244 -  assumes "\<forall>p \<in># M. is_prime p" "\<forall>p \<in># N. is_prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
  8.1245 +  assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
  8.1246    shows   "M = N"
  8.1247  proof -
  8.1248    have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
  8.1249 @@ -1504,7 +1505,7 @@
  8.1250    hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
  8.1251      by (auto dest: mset_subset_eqD)
  8.1252    with in_prime_factorization_imp_prime[of _ x]
  8.1253 -    have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> is_prime p" by blast
  8.1254 +    have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
  8.1255    with assms show ?thesis
  8.1256      by (simp add: Gcd_factorial_def prime_factorization_msetprod_primes)
  8.1257  qed
  8.1258 @@ -1519,7 +1520,7 @@
  8.1259    finally show ?thesis by (simp add: Lcm_factorial_def)
  8.1260  next
  8.1261    case False
  8.1262 -  have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> is_prime y"
  8.1263 +  have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
  8.1264      by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
  8.1265    with assms False show ?thesis
  8.1266      by (simp add: Lcm_factorial_def prime_factorization_msetprod_primes)
  8.1267 @@ -1586,7 +1587,7 @@
  8.1268    then obtain x where "x \<in> A" "x \<noteq> 0" by blast
  8.1269    hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
  8.1270      by (intro subset_mset.cInf_lower) auto
  8.1271 -  hence "is_prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
  8.1272 +  hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
  8.1273      using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
  8.1274    with False show ?thesis
  8.1275      by (auto simp add: Gcd_factorial_def normalize_msetprod_primes)
  8.1276 @@ -1692,9 +1693,9 @@
  8.1277  
  8.1278  lemma (in normalization_semidom) factorial_semiring_altI_aux:
  8.1279    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
  8.1280 -  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
  8.1281 +  assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
  8.1282    assumes "(x::'a) \<noteq> 0"
  8.1283 -  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
  8.1284 +  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
  8.1285  using \<open>x \<noteq> 0\<close>
  8.1286  proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
  8.1287    case (less a)
  8.1288 @@ -1709,7 +1710,7 @@
  8.1289      proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
  8.1290        case False
  8.1291        with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
  8.1292 -      hence "is_prime_elem a" by (rule irreducible_imp_prime)
  8.1293 +      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
  8.1294        thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
  8.1295      next
  8.1296        case True
  8.1297 @@ -1722,7 +1723,7 @@
  8.1298        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
  8.1299          by (rule psubset_card_mono)
  8.1300        moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
  8.1301 -      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize b"
  8.1302 +      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize b"
  8.1303          by (intro less) auto
  8.1304        then guess A .. note A = this
  8.1305  
  8.1306 @@ -1741,7 +1742,7 @@
  8.1307        ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
  8.1308        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
  8.1309          by (rule psubset_card_mono)
  8.1310 -      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize c"
  8.1311 +      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize c"
  8.1312          by (intro less) auto
  8.1313        then guess B .. note B = this
  8.1314  
  8.1315 @@ -1752,7 +1753,7 @@
  8.1316  
  8.1317  lemma factorial_semiring_altI:
  8.1318    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
  8.1319 -  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
  8.1320 +  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
  8.1321    shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
  8.1322    by intro_classes (rule factorial_semiring_altI_aux[OF assms])
  8.1323  
  8.1324 @@ -1816,7 +1817,7 @@
  8.1325  qed
  8.1326  
  8.1327  lemma
  8.1328 -  assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
  8.1329 +  assumes "x \<noteq> 0" "y \<noteq> 0" "prime p"
  8.1330    shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
  8.1331      and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
  8.1332  proof -
     9.1 --- a/src/HOL/Number_Theory/Gauss.thy	Mon Aug 08 14:13:14 2016 +0200
     9.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Mon Aug 08 17:47:51 2016 +0200
     9.3 @@ -112,7 +112,7 @@
     9.4      from p_a_relprime have "\<not>p dvd a"
     9.5        by (simp add: cong_altdef_int)
     9.6      with p_prime have "coprime a (int p)" 
     9.7 -       by (subst gcd.commute, intro is_prime_imp_coprime) auto
     9.8 +       by (subst gcd.commute, intro prime_imp_coprime) auto
     9.9      with a cong_mult_rcancel_int [of a "int p" x y]
    9.10        have "[x = y] (mod p)" by simp
    9.11      with cong_less_imp_eq_int [of x y p] p_minus_one_l
    9.12 @@ -144,7 +144,7 @@
    9.13    from p_a_relprime have "\<not>p dvd a"
    9.14      by (simp add: cong_altdef_int)
    9.15    with p_prime have "coprime a (int p)" 
    9.16 -     by (subst gcd.commute, intro is_prime_imp_coprime) auto
    9.17 +     by (subst gcd.commute, intro prime_imp_coprime) auto
    9.18    with a' cong_mult_rcancel_int [of a "int p" x y]
    9.19      have "[x = y] (mod p)" by simp
    9.20    with cong_less_imp_eq_int [of x y p] p_minus_one_l
    9.21 @@ -207,7 +207,7 @@
    9.22  
    9.23  lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
    9.24    using p_prime A_ncong_p [OF assms]
    9.25 -  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
    9.26 +  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
    9.27  
    9.28  lemma A_prod_relprime: "gcd (setprod id A) p = 1"
    9.29    by (metis id_def all_A_relprime setprod_coprime)
    10.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Mon Aug 08 14:13:14 2016 +0200
    10.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Aug 08 17:47:51 2016 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4  
    10.5  lemma prime: 
    10.6    "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
    10.7 -  unfolding is_prime_nat_iff
    10.8 +  unfolding prime_nat_iff
    10.9  proof safe
   10.10    fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p" 
   10.11             and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
   10.12 @@ -20,8 +20,8 @@
   10.13    moreover from p m have "m < p" by (auto dest: dvd_imp_le)
   10.14    ultimately have "coprime p m" using * by blast
   10.15    with m show "m = 1" by simp
   10.16 -qed (auto simp: is_prime_nat_iff simp del: One_nat_def 
   10.17 -          intro!: is_prime_imp_coprime dest: dvd_imp_le)
   10.18 +qed (auto simp: prime_nat_iff simp del: One_nat_def 
   10.19 +          intro!: prime_imp_coprime dest: dvd_imp_le)
   10.20  
   10.21  lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
   10.22  proof-
   10.23 @@ -85,7 +85,7 @@
   10.24      with y(2) have th: "p dvd a"
   10.25        by (auto dest: cong_dvd_eq_nat)
   10.26      have False
   10.27 -      by (metis gcd_nat.absorb1 not_is_prime_1 p pa th)}
   10.28 +      by (metis gcd_nat.absorb1 not_prime_1 p pa th)}
   10.29    with y show ?thesis unfolding Ex1_def using neq0_conv by blast
   10.30  qed
   10.31  
   10.32 @@ -428,18 +428,18 @@
   10.33  proof (cases "n=0 \<or> n=1")
   10.34    case True
   10.35    then show ?thesis
   10.36 -     by (metis bigger_prime dvd_0_right not_is_prime_1 not_is_prime_0)
   10.37 +     by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0)
   10.38  next
   10.39    case False
   10.40    show ?thesis
   10.41    proof
   10.42      assume "prime n"
   10.43      then show ?rhs
   10.44 -      by (metis  not_is_prime_1 is_prime_nat_iff)
   10.45 +      by (metis  not_prime_1 prime_nat_iff)
   10.46    next
   10.47      assume ?rhs
   10.48      with False show "prime n"
   10.49 -      by (auto simp: is_prime_nat_iff) (metis One_nat_def prime_factor_nat is_prime_nat_iff)
   10.50 +      by (auto simp: prime_nat_iff) (metis One_nat_def prime_factor_nat prime_nat_iff)
   10.51    qed
   10.52  qed
   10.53  
   10.54 @@ -475,7 +475,7 @@
   10.55          with H[rule_format, of e] h have "e=1" by simp
   10.56          with e have "d = n" by simp}
   10.57        ultimately have "d=1 \<or> d=n"  by blast}
   10.58 -    ultimately have ?thesis unfolding is_prime_nat_iff using np n(2) by blast}
   10.59 +    ultimately have ?thesis unfolding prime_nat_iff using np n(2) by blast}
   10.60    ultimately show ?thesis by auto
   10.61  qed
   10.62  
   10.63 @@ -485,7 +485,7 @@
   10.64  proof-
   10.65    {assume "n=0 \<or> n=1" 
   10.66     hence ?thesis
   10.67 -     by (metis not_is_prime_0 not_is_prime_1)}
   10.68 +     by (metis not_prime_0 not_prime_1)}
   10.69    moreover
   10.70    {assume n: "n\<noteq>0" "n\<noteq>1"
   10.71      {assume H: ?lhs
   10.72 @@ -539,7 +539,7 @@
   10.73      from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
   10.74      from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
   10.75      have P0: "P \<noteq> 0" using P(1)
   10.76 -      by (metis not_is_prime_0) 
   10.77 +      by (metis not_prime_0) 
   10.78      from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
   10.79      from d s t P0  have s': "ord p (a^r) * t = s"
   10.80        by (metis mult.commute mult_cancel1 mult.assoc) 
   10.81 @@ -559,7 +559,7 @@
   10.82    hence o: "ord p (a^r) = q" using d by simp
   10.83    from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
   10.84    {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
   10.85 -    from pp[unfolded is_prime_nat_iff] d have dp: "d = p" by blast
   10.86 +    from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
   10.87      from n have "n \<noteq> 0" by simp
   10.88      then have False using d dp pn
   10.89        by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
   10.90 @@ -675,7 +675,7 @@
   10.91    from Cons.prems[unfolded primefact_def]
   10.92    have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p"  and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all
   10.93    {assume "p dvd q"
   10.94 -    with p(1) q(1) have "p = q" unfolding is_prime_nat_iff by auto
   10.95 +    with p(1) q(1) have "p = q" unfolding prime_nat_iff by auto
   10.96      hence ?case by simp}
   10.97    moreover
   10.98    { assume h: "p dvd foldr op * qs 1"
   10.99 @@ -730,7 +730,7 @@
  10.100      from psp primefact_contains[OF pfpsq p]
  10.101      have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
  10.102        by (simp add: list_all_iff)
  10.103 -    from p is_prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
  10.104 +    from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
  10.105        by auto
  10.106      from div_mult1_eq[of r q p] p(2)
  10.107      have eq1: "r* (q div p) = (n - 1) div p"
    11.1 --- a/src/HOL/Number_Theory/Polynomial_Factorial.thy	Mon Aug 08 14:13:14 2016 +0200
    11.2 +++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy	Mon Aug 08 17:47:51 2016 +0200
    11.3 @@ -812,9 +812,9 @@
    11.4  subsection \<open>More properties of content and primitive part\<close>
    11.5  
    11.6  lemma lift_prime_elem_poly:
    11.7 -  assumes "is_prime_elem (c :: 'a :: semidom)"
    11.8 -  shows   "is_prime_elem [:c:]"
    11.9 -proof (rule is_prime_elemI)
   11.10 +  assumes "prime_elem (c :: 'a :: semidom)"
   11.11 +  shows   "prime_elem [:c:]"
   11.12 +proof (rule prime_elemI)
   11.13    fix a b assume *: "[:c:] dvd a * b"
   11.14    from * have dvd: "c dvd coeff (a * b) n" for n
   11.15      by (subst (asm) const_poly_dvd_iff) blast
   11.16 @@ -862,25 +862,25 @@
   11.17        ultimately have "c dvd coeff a i * coeff b m"
   11.18          by (simp add: dvd_add_left_iff)
   11.19        with assms coeff_m show "c dvd coeff a i"
   11.20 -        by (simp add: prime_dvd_mult_iff)
   11.21 +        by (simp add: prime_elem_dvd_mult_iff)
   11.22      qed
   11.23      hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
   11.24    }
   11.25    thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
   11.26 -qed (insert assms, simp_all add: is_prime_elem_def one_poly_def)
   11.27 +qed (insert assms, simp_all add: prime_elem_def one_poly_def)
   11.28  
   11.29  lemma prime_elem_const_poly_iff:
   11.30    fixes c :: "'a :: semidom"
   11.31 -  shows   "is_prime_elem [:c:] \<longleftrightarrow> is_prime_elem c"
   11.32 +  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
   11.33  proof
   11.34 -  assume A: "is_prime_elem [:c:]"
   11.35 -  show "is_prime_elem c"
   11.36 -  proof (rule is_prime_elemI)
   11.37 +  assume A: "prime_elem [:c:]"
   11.38 +  show "prime_elem c"
   11.39 +  proof (rule prime_elemI)
   11.40      fix a b assume "c dvd a * b"
   11.41      hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
   11.42 -    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_divides_productD)
   11.43 +    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
   11.44      thus "c dvd a \<or> c dvd b" by simp
   11.45 -  qed (insert A, auto simp: is_prime_elem_def is_unit_poly_iff)
   11.46 +  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
   11.47  qed (auto intro: lift_prime_elem_poly)
   11.48  
   11.49  context
   11.50 @@ -897,16 +897,16 @@
   11.51    hence "f * g \<noteq> 0" by auto
   11.52    {
   11.53      assume "\<not>is_unit (content (f * g))"
   11.54 -    with False have "\<exists>p. p dvd content (f * g) \<and> is_prime p"
   11.55 +    with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
   11.56        by (intro prime_divisor_exists) simp_all
   11.57 -    then obtain p where "p dvd content (f * g)" "is_prime p" by blast
   11.58 +    then obtain p where "p dvd content (f * g)" "prime p" by blast
   11.59      from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
   11.60        by (simp add: const_poly_dvd_iff_dvd_content)
   11.61 -    moreover from \<open>is_prime p\<close> have "is_prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
   11.62 +    moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
   11.63      ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
   11.64 -      by (simp add: prime_dvd_mult_iff)
   11.65 +      by (simp add: prime_elem_dvd_mult_iff)
   11.66      with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
   11.67 -    with \<open>is_prime p\<close> have False by simp
   11.68 +    with \<open>prime p\<close> have False by simp
   11.69    }
   11.70    hence "is_unit (content (f * g))" by blast
   11.71    hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
   11.72 @@ -1033,12 +1033,12 @@
   11.73  
   11.74  private lemma field_poly_irreducible_imp_prime:
   11.75    assumes "irreducible (p :: 'a :: field poly)"
   11.76 -  shows   "is_prime_elem p"
   11.77 +  shows   "prime_elem p"
   11.78  proof -
   11.79    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   11.80 -  from field_poly.irreducible_imp_prime[of p] assms
   11.81 -    show ?thesis unfolding irreducible_def is_prime_elem_def dvd_field_poly
   11.82 -      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.is_prime_elem_def[OF A] by blast
   11.83 +  from field_poly.irreducible_imp_prime_elem[of p] assms
   11.84 +    show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
   11.85 +      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
   11.86  qed
   11.87  
   11.88  private lemma field_poly_msetprod_prime_factorization:
   11.89 @@ -1053,14 +1053,14 @@
   11.90  
   11.91  private lemma field_poly_in_prime_factorization_imp_prime:
   11.92    assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
   11.93 -  shows   "is_prime_elem p"
   11.94 +  shows   "prime_elem p"
   11.95  proof -
   11.96    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   11.97    have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
   11.98               normalize_field_poly unit_factor_field_poly" ..
   11.99    from field_poly.in_prime_factorization_imp_prime[of p x] assms
  11.100 -    show ?thesis unfolding is_prime_elem_def dvd_field_poly
  11.101 -      comm_semiring_1.is_prime_elem_def[OF A] normalization_semidom.is_prime_def[OF B] by blast
  11.102 +    show ?thesis unfolding prime_elem_def dvd_field_poly
  11.103 +      comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
  11.104  qed
  11.105  
  11.106  
  11.107 @@ -1144,24 +1144,24 @@
  11.108  private lemma irreducible_imp_prime_poly:
  11.109    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  11.110    assumes "irreducible p"
  11.111 -  shows   "is_prime_elem p"
  11.112 +  shows   "prime_elem p"
  11.113  proof (cases "degree p = 0")
  11.114    case True
  11.115    with assms show ?thesis
  11.116      by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
  11.117 -             intro!: irreducible_imp_prime elim!: degree_eq_zeroE)
  11.118 +             intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
  11.119  next
  11.120    case False
  11.121    from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
  11.122      by (simp_all add: nonconst_poly_irreducible_iff)
  11.123 -  from irred have prime: "is_prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
  11.124 +  from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
  11.125    show ?thesis
  11.126 -  proof (rule is_prime_elemI)
  11.127 +  proof (rule prime_elemI)
  11.128      fix q r assume "p dvd q * r"
  11.129      hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
  11.130      hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
  11.131      from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
  11.132 -      by (rule prime_divides_productD)
  11.133 +      by (rule prime_elem_dvd_multD)
  11.134      with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
  11.135    qed (insert assms, auto simp: irreducible_def)
  11.136  qed
  11.137 @@ -1196,9 +1196,9 @@
  11.138      by (simp add: nonconst_poly_irreducible_iff)
  11.139  qed
  11.140  
  11.141 -lemma is_prime_elem_primitive_part_fract:
  11.142 +lemma prime_elem_primitive_part_fract:
  11.143    fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
  11.144 -  shows "irreducible p \<Longrightarrow> is_prime_elem (primitive_part_fract p)"
  11.145 +  shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
  11.146    by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
  11.147  
  11.148  lemma irreducible_linear_field_poly:
  11.149 @@ -1214,8 +1214,8 @@
  11.150      by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
  11.151  qed (insert assms, auto simp: is_unit_poly_iff)
  11.152  
  11.153 -lemma is_prime_elem_linear_field_poly:
  11.154 -  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> is_prime_elem [:a,b:]"
  11.155 +lemma prime_elem_linear_field_poly:
  11.156 +  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
  11.157    by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
  11.158  
  11.159  lemma irreducible_linear_poly:
  11.160 @@ -1224,9 +1224,9 @@
  11.161    by (auto intro!: irreducible_linear_field_poly 
  11.162             simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
  11.163  
  11.164 -lemma is_prime_elem_linear_poly:
  11.165 +lemma prime_elem_linear_poly:
  11.166    fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
  11.167 -  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> is_prime_elem [:a,b:]"
  11.168 +  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
  11.169    by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
  11.170  
  11.171    
  11.172 @@ -1235,7 +1235,7 @@
  11.173  private lemma poly_prime_factorization_exists_content_1:
  11.174    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  11.175    assumes "p \<noteq> 0" "content p = 1"
  11.176 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
  11.177 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  11.178  proof -
  11.179    let ?P = "field_poly.prime_factorization (fract_poly p)"
  11.180    define c where "c = msetprod (image_mset fract_content ?P)"
  11.181 @@ -1282,8 +1282,8 @@
  11.182      by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
  11.183    finally have "msetprod A = normalize p" ..
  11.184    
  11.185 -  have "is_prime_elem p" if "p \<in># A" for p
  11.186 -    using that by (auto simp: A_def is_prime_elem_primitive_part_fract prime_imp_irreducible 
  11.187 +  have "prime_elem p" if "p \<in># A" for p
  11.188 +    using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
  11.189                          dest!: field_poly_in_prime_factorization_imp_prime )
  11.190    from this and \<open>msetprod A = normalize p\<close> show ?thesis
  11.191      by (intro exI[of _ A]) blast
  11.192 @@ -1292,15 +1292,15 @@
  11.193  lemma poly_prime_factorization_exists:
  11.194    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
  11.195    assumes "p \<noteq> 0"
  11.196 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
  11.197 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
  11.198  proof -
  11.199    define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
  11.200 -  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
  11.201 +  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
  11.202      by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
  11.203    then guess A by (elim exE conjE) note A = this
  11.204    moreover from assms have "msetprod B = [:content p:]"
  11.205      by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
  11.206 -  moreover have "\<forall>p. p \<in># B \<longrightarrow> is_prime_elem p"
  11.207 +  moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
  11.208      by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
  11.209    ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
  11.210  qed
    12.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Aug 08 14:13:14 2016 +0200
    12.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Aug 08 17:47:51 2016 +0200
    12.3 @@ -55,57 +55,55 @@
    12.4  declare [[coercion int]]
    12.5  declare [[coercion_enabled]]
    12.6  
    12.7 -abbreviation (input) "prime \<equiv> is_prime"
    12.8 -
    12.9 -lemma is_prime_elem_nat_iff:
   12.10 -  "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.11 +lemma prime_elem_nat_iff:
   12.12 +  "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.13  proof safe
   12.14 -  assume *: "is_prime_elem n"
   12.15 +  assume *: "prime_elem n"
   12.16    from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
   12.17    thus "n > 1" by (cases n) simp_all
   12.18    fix m assume m: "m dvd n" "m \<noteq> n"
   12.19    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
   12.20 -    by (intro irreducibleD' prime_imp_irreducible)
   12.21 +    by (intro irreducibleD' prime_elem_imp_irreducible)
   12.22    with m show "m = 1" by (auto dest: dvd_antisym)
   12.23  next
   12.24    assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
   12.25 -  thus "is_prime_elem n"
   12.26 -    by (auto simp: prime_iff_irreducible irreducible_altdef)
   12.27 +  thus "prime_elem n"
   12.28 +    by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
   12.29  qed
   12.30  
   12.31 -lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
   12.32 -  by (simp add: is_prime_def)
   12.33 +lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
   12.34 +  by (simp add: prime_def)
   12.35  
   12.36 -lemma is_prime_nat_iff:
   12.37 -  "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.38 -  by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
   12.39 +lemma prime_nat_iff:
   12.40 +  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.41 +  by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
   12.42  
   12.43 -lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
   12.44 +lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
   12.45  proof
   12.46 -  assume "is_prime_elem n"
   12.47 -  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
   12.48 +  assume "prime_elem n"
   12.49 +  thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
   12.50  next
   12.51 -  assume "is_prime_elem (nat (abs n))"
   12.52 -  thus "is_prime_elem n"
   12.53 -    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
   12.54 +  assume "prime_elem (nat (abs n))"
   12.55 +  thus "prime_elem n"
   12.56 +    by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
   12.57  qed
   12.58  
   12.59 -lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
   12.60 -  by (auto simp: is_prime_elem_int_nat_transfer)
   12.61 +lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
   12.62 +  by (auto simp: prime_elem_int_nat_transfer)
   12.63  
   12.64 -lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
   12.65 -  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
   12.66 +lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
   12.67 +  by (auto simp: prime_elem_int_nat_transfer prime_def)
   12.68  
   12.69 -lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
   12.70 -  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
   12.71 +lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
   12.72 +  by (auto simp: prime_elem_int_nat_transfer prime_def)
   12.73  
   12.74 -lemma is_prime_int_iff:
   12.75 -  "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.76 +lemma prime_int_iff:
   12.77 +  "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   12.78  proof (intro iffI conjI allI impI; (elim conjE)?)
   12.79 -  assume *: "is_prime n"
   12.80 -  hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
   12.81 +  assume *: "prime n"
   12.82 +  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
   12.83    from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
   12.84 -    by (auto simp: is_prime_def zabs_def not_less split: if_splits)
   12.85 +    by (auto simp: prime_def zabs_def not_less split: if_splits)
   12.86    thus "n > 1" by presburger
   12.87    fix m assume "m dvd n" \<open>m \<ge> 0\<close>
   12.88    with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
   12.89 @@ -121,8 +119,8 @@
   12.90      with n(2) have "int m = 1 \<or> int m = n" by auto
   12.91      thus "m = 1 \<or> m = nat n" by auto
   12.92    qed
   12.93 -  ultimately show "is_prime n" 
   12.94 -    unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
   12.95 +  ultimately show "prime n" 
   12.96 +    unfolding prime_int_nat_transfer prime_nat_iff by auto
   12.97  qed
   12.98  
   12.99  
  12.100 @@ -131,7 +129,7 @@
  12.101    shows   "\<not>n dvd p"
  12.102  proof
  12.103    assume "n dvd p"
  12.104 -  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
  12.105 +  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
  12.106    from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
  12.107      by (cases "n = 0") (auto dest!: dvd_imp_le)
  12.108  qed
  12.109 @@ -141,7 +139,7 @@
  12.110    shows   "\<not>n dvd p"
  12.111  proof
  12.112    assume "n dvd p"
  12.113 -  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
  12.114 +  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
  12.115    from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
  12.116      by (auto dest!: zdvd_imp_le)
  12.117  qed
  12.118 @@ -153,60 +151,60 @@
  12.119    by (intro prime_int_not_dvd) auto
  12.120  
  12.121  lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
  12.122 -  unfolding is_prime_int_iff by auto
  12.123 +  unfolding prime_int_iff by auto
  12.124  
  12.125  lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
  12.126 -  unfolding is_prime_nat_iff by auto
  12.127 +  unfolding prime_nat_iff by auto
  12.128  
  12.129  lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
  12.130 -  unfolding is_prime_int_iff by auto
  12.131 +  unfolding prime_int_iff by auto
  12.132  
  12.133  lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
  12.134 -  unfolding is_prime_nat_iff by auto
  12.135 +  unfolding prime_nat_iff by auto
  12.136  
  12.137  lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
  12.138 -  unfolding is_prime_nat_iff by auto
  12.139 +  unfolding prime_nat_iff by auto
  12.140  
  12.141  lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
  12.142 -  unfolding is_prime_int_iff by auto
  12.143 +  unfolding prime_int_iff by auto
  12.144  
  12.145  lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
  12.146 -  unfolding is_prime_nat_iff by auto
  12.147 +  unfolding prime_nat_iff by auto
  12.148  
  12.149  lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
  12.150 -  unfolding is_prime_nat_iff by auto
  12.151 +  unfolding prime_nat_iff by auto
  12.152  
  12.153  lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
  12.154 -  unfolding is_prime_int_iff by auto
  12.155 +  unfolding prime_int_iff by auto
  12.156  
  12.157  lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
  12.158 -  unfolding is_prime_nat_iff by auto
  12.159 +  unfolding prime_nat_iff by auto
  12.160  
  12.161  lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
  12.162 -  unfolding is_prime_int_iff by auto
  12.163 +  unfolding prime_int_iff by auto
  12.164  
  12.165  lemma prime_int_altdef:
  12.166    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
  12.167      m = 1 \<or> m = p))"
  12.168 -  unfolding is_prime_int_iff by blast
  12.169 +  unfolding prime_int_iff by blast
  12.170  
  12.171  lemma not_prime_eq_prod_nat:
  12.172    assumes "m > 1" "\<not>prime (m::nat)"
  12.173    shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
  12.174    using assms irreducible_altdef[of m]
  12.175 -  by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
  12.176 +  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
  12.177  
  12.178  
  12.179  subsubsection \<open>Make prime naively executable\<close>
  12.180  
  12.181  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  12.182 -  unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
  12.183 +  unfolding One_nat_def [symmetric] by (rule not_prime_1)
  12.184  
  12.185 -lemma is_prime_nat_iff':
  12.186 +lemma prime_nat_iff':
  12.187    "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
  12.188  proof safe
  12.189    assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
  12.190 -  show "is_prime p" unfolding is_prime_nat_iff
  12.191 +  show "prime p" unfolding prime_nat_iff
  12.192    proof (intro conjI allI impI)
  12.193      fix m assume "m dvd p"
  12.194      with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
  12.195 @@ -215,25 +213,25 @@
  12.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)
  12.197      ultimately show "m = 1 \<or> m = p" by simp
  12.198    qed fact+
  12.199 -qed (auto simp: is_prime_nat_iff)
  12.200 +qed (auto simp: prime_nat_iff)
  12.201  
  12.202  lemma prime_nat_code [code_unfold]:
  12.203    "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
  12.204 -  by (rule ext, rule is_prime_nat_iff')
  12.205 +  by (rule ext, rule prime_nat_iff')
  12.206  
  12.207 -lemma is_prime_int_iff':
  12.208 +lemma prime_int_iff':
  12.209    "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
  12.210  proof
  12.211    assume "?lhs"
  12.212 -  thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
  12.213 +  thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
  12.214  next
  12.215    assume "?rhs"
  12.216 -  thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
  12.217 +  thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
  12.218  qed
  12.219  
  12.220  lemma prime_int_code [code_unfold]:
  12.221    "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" 
  12.222 -  by (rule ext, rule is_prime_int_iff')
  12.223 +  by (rule ext, rule prime_int_iff')
  12.224  
  12.225  lemma prime_nat_simp:
  12.226      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
  12.227 @@ -245,10 +243,10 @@
  12.228  
  12.229  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
  12.230  
  12.231 -lemma two_is_prime_nat [simp]: "prime (2::nat)"
  12.232 +lemma two_prime_nat [simp]: "prime (2::nat)"
  12.233    by simp
  12.234  
  12.235 -declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
  12.236 +declare prime_int_nat_transfer[of "numeral m" for m, simp]
  12.237  
  12.238  
  12.239  text\<open>A bit of regression testing:\<close>
  12.240 @@ -282,7 +280,7 @@
  12.241      then have "p dvd 1" by simp
  12.242      then have "p <= 1" by auto
  12.243      moreover from \<open>prime p\<close> have "p > 1"
  12.244 -      using is_prime_nat_iff by blast
  12.245 +      using prime_nat_iff by blast
  12.246      ultimately have False by auto}
  12.247    then have "n < p" by presburger
  12.248    with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
  12.249 @@ -313,7 +311,7 @@
  12.250  proof -
  12.251    from assms have
  12.252      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
  12.253 -    unfolding is_prime_nat_iff by auto
  12.254 +    unfolding prime_nat_iff by auto
  12.255    from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
  12.256    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
  12.257    have "p dvd p * q" by simp
  12.258 @@ -332,7 +330,7 @@
  12.259  next
  12.260    case (Suc k x y)
  12.261    from Suc.prems have pxy: "p dvd x*y" by auto
  12.262 -  from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
  12.263 +  from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
  12.264    from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
  12.265    {assume px: "p dvd x"
  12.266      then obtain d where d: "x = p*d" unfolding dvd_def by blast
  12.267 @@ -446,7 +444,7 @@
  12.268    shows "\<exists>x y. a*x = Suc (p*y)"
  12.269  proof -
  12.270    have ap: "coprime a p"
  12.271 -    by (metis gcd.commute p pa is_prime_imp_coprime)
  12.272 +    by (metis gcd.commute p pa prime_imp_coprime)
  12.273    moreover from p have "p \<noteq> 1" by auto
  12.274    ultimately have "\<exists>x y. a * x = p * y + 1"
  12.275      by (rule coprime_bezout_strong)
  12.276 @@ -470,7 +468,7 @@
  12.277    fixes n :: int
  12.278    shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
  12.279    unfolding prime_factors_def 
  12.280 -  by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
  12.281 +  by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
  12.282  
  12.283  lemma msetprod_prime_factorization_int:
  12.284    fixes n :: int
  12.285 @@ -480,7 +478,7 @@
  12.286  
  12.287  lemma prime_factorization_exists_nat:
  12.288    "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
  12.289 -  using prime_factorization_exists[of n] by (auto simp: is_prime_def)
  12.290 +  using prime_factorization_exists[of n] by (auto simp: prime_def)
  12.291  
  12.292  lemma msetprod_prime_factorization_nat [simp]: 
  12.293    "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
  12.294 @@ -499,7 +497,7 @@
  12.295    assumes S_eq: "S = {p. 0 < f p}"
  12.296      and "finite S"
  12.297      and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
  12.298 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  12.299 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  12.300    using assms by (intro prime_factorization_unique'') auto
  12.301  
  12.302  lemma prime_factorization_unique_int:
  12.303 @@ -507,7 +505,7 @@
  12.304    assumes S_eq: "S = {p. 0 < f p}"
  12.305      and "finite S"
  12.306      and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
  12.307 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
  12.308 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  12.309    using assms by (intro prime_factorization_unique'') auto
  12.310  
  12.311  lemma prime_factors_characterization_nat:
  12.312 @@ -536,23 +534,23 @@
  12.313    by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
  12.314  
  12.315  lemma multiplicity_characterization_nat:
  12.316 -  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow>
  12.317 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
  12.318      n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
  12.319    by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
  12.320  
  12.321  lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
  12.322 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
  12.323 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
  12.324        multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
  12.325    by (intro impI, rule multiplicity_characterization_nat) auto
  12.326  
  12.327  lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
  12.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"
  12.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"
  12.330    by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
  12.331       (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
  12.332  
  12.333  lemma multiplicity_characterization'_int [rule_format]:
  12.334    "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
  12.335 -    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
  12.336 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
  12.337        multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
  12.338    by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
  12.339  
  12.340 @@ -561,18 +559,18 @@
  12.341  
  12.342  lemma multiplicity_eq_nat:
  12.343    fixes x and y::nat
  12.344 -  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.345 +  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.346    shows "x = y"
  12.347    using multiplicity_eq_imp_eq[of x y] assms by simp
  12.348  
  12.349  lemma multiplicity_eq_int:
  12.350    fixes x y :: int
  12.351 -  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.352 +  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  12.353    shows "x = y"
  12.354    using multiplicity_eq_imp_eq[of x y] assms by simp
  12.355  
  12.356  lemma multiplicity_prod_prime_powers:
  12.357 -  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
  12.358 +  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
  12.359    shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
  12.360  proof -
  12.361    define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
  12.362 @@ -592,7 +590,7 @@
  12.363    also have "\<dots> = msetprod A"
  12.364      by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
  12.365    also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
  12.366 -    by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
  12.367 +    by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
  12.368    also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
  12.369      by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
  12.370    also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
  12.371 @@ -600,21 +598,21 @@
  12.372  qed
  12.373  
  12.374  (* TODO Legacy names *)
  12.375 -lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
  12.376 -lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
  12.377 -lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
  12.378 -lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
  12.379 -lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
  12.380 -lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
  12.381 -lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
  12.382 -lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
  12.383 -lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
  12.384 -lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
  12.385 -lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
  12.386 -lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
  12.387 +lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
  12.388 +lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
  12.389 +lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
  12.390 +lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
  12.391 +lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
  12.392 +lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
  12.393 +lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
  12.394 +lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
  12.395 +lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
  12.396 +lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
  12.397 +lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
  12.398 +lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
  12.399  lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
  12.400  lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
  12.401 -lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
  12.402 -lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
  12.403 +lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
  12.404 +lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
  12.405  
  12.406  end
  12.407 \ No newline at end of file
    13.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Aug 08 14:13:14 2016 +0200
    13.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Aug 08 17:47:51 2016 +0200
    13.3 @@ -280,7 +280,7 @@
    13.4    qed
    13.5    then show ?thesis
    13.6      using \<open>2 \<le> p\<close>
    13.7 -    by (simp add: is_prime_nat_iff)
    13.8 +    by (simp add: prime_nat_iff)
    13.9         (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
   13.10                not_numeral_le_zero one_dvd)
   13.11  qed
    14.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Mon Aug 08 14:13:14 2016 +0200
    14.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Mon Aug 08 17:47:51 2016 +0200
    14.3 @@ -28,7 +28,7 @@
    14.4    by (induct m) auto
    14.5  
    14.6  lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
    14.7 -  apply (simp add: is_prime_nat_iff)
    14.8 +  apply (simp add: prime_nat_iff)
    14.9    apply (rule iffI)
   14.10    apply blast
   14.11    apply (erule conjE)