# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1469088364 -7200
# Node ID 523b488b15c9d8f4ab960c695abdcc0a407d3b19
# Parent  f01d1e393f3f4f898a4b4404cccfff78ae65afcc
Overhaul of prime/multiplicity/prime_factors

diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -22,17 +22,17 @@
 proof -
   have "p dvd m*n" using dvd_mult_left pk by blast
   then consider "p dvd m" | "p dvd n"
-    using p prime_dvd_mult_eq_nat by blast
+    using p is_prime_dvd_mult_iff by blast
   then show ?thesis
   proof cases
     case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
       then have "\<exists>x. k dvd x * n \<and> m = p * x"
-        using p pk by auto
+        using p pk by (auto simp: mult.assoc)
     then show ?thesis ..
   next
     case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
-      then have "\<exists>y. k dvd m*y \<and> n = p*y"
-        using p pk by auto
+    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
+      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
     then show ?thesis ..
   qed
 qed
@@ -50,11 +50,16 @@
   then show ?case
   proof cases
     case (1 x) 
-      with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
-      by force
+    with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
+    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
+      by (auto intro: mult_dvd_mono)
+    thus ?thesis by blast
   next
     case (2 y) 
-      with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
+    with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
+    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
+      by (auto intro: mult_dvd_mono)
+    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
       by force
   qed
 qed
@@ -73,20 +78,27 @@
 
 subsection\<open>The Exponent Function\<close>
 
+abbreviation (input) "exponent \<equiv> multiplicity"
+
+(*
 definition
   exponent :: "nat => nat => nat"
   where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
+*)
 
-lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
-  by (simp add: exponent_def)
+(*lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
+  by (simp add: exponent_def)*)
 
 lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
   by (induct n) (auto simp: Suc_le_eq le_less_trans)
 
+(*
 text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
 lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
   by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
+*)
 
+(*
 lemma exponent_ge:
   assumes "p ^ k dvd n" "prime p" "0 < n"
     shows "k \<le> exponent p n"
@@ -96,7 +108,9 @@
   with assms show ?thesis
     by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
 qed
+*)
 
+(*
 lemma power_exponent_dvd: "p ^ exponent p s dvd s"
 proof (cases "s = 0")
   case True then show ?thesis by simp
@@ -107,27 +121,35 @@
     apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
     done
 qed
+*)
 
-lemma power_Suc_exponent_Not_dvd:
+(*lemma power_Suc_exponent_Not_dvd:
     "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
   by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
+*)
 
+
+(*
 lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
   apply (simp add: exponent_def)
   apply (rule Greatest_equality, simp)
   apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
   done
+*)
 
+(*
 lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   apply (case_tac "prime p")
   apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
   apply simp
   done
+*)
 
 lemma exponent_equalityI:
   "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
-  by (simp add: exponent_def)
+  by (simp add: multiplicity_def)
 
+(*
 lemma exponent_mult_add: 
   assumes "a > 0" "b > 0"
     shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
@@ -149,15 +171,22 @@
   then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
   qed
 qed
+*)
 
-lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0"
-  apply (case_tac "exponent p n", simp)
-  by (metis dvd_mult_left power_Suc power_exponent_dvd)
+lemma not_dvd_imp_multiplicity_0: 
+  assumes "\<not>p dvd x"
+  shows   "multiplicity p x = 0"
+proof -
+  from assms have "multiplicity p x < 1"
+    by (intro multiplicity_lessI) auto
+  thus ?thesis by simp
+qed
 
 
 subsection\<open>The Main Combinatorial Argument\<close>
 
 lemma exponent_p_a_m_k_equation: 
+  fixes p :: nat
   assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 
     shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
 proof (rule exponent_equalityI [OF iffI])
@@ -188,60 +217,56 @@
 qed
 
 lemma p_not_div_choose_lemma: 
+  fixes p :: nat
   assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
-      and "k < K"
+      and "k < K" and p: "prime p"
     shows "exponent p (j + k choose k) = 0"
-proof (cases "prime p")
-  case False then show ?thesis by simp
+  using \<open>k < K\<close>
+proof (induction k)
+  case 0 then show ?case by simp
 next
-  case True show ?thesis using \<open>k < K\<close> 
-  proof (induction k)
-    case 0 then show ?case by simp
-  next
-    case (Suc k)
-    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
-    then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
-      by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add 
-                mult_pos_pos zero_less_Suc zero_less_mult_pos)
-    then show ?case
-      by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc)
-  qed
+  case (Suc k)
+  then have *: "(Suc (j+k) choose Suc k) > 0" by simp
+  then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
+    by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
+       (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
+  with p * show ?case
+    by (subst (asm) prime_multiplicity_mult_distrib) simp_all
 qed
 
 text\<open>The lemma above, with two changes of variables\<close>
 lemma p_not_div_choose:
   assumes "k < K" and "k \<le> n" 
-      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)"
+      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)" "is_prime p"
     shows "exponent p (n choose k) = 0"
 apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
 apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
-apply (rule TrueI)
+apply (rule TrueI)+
 done
 
 proposition const_p_fac:
-  assumes "m>0"
-    shows "exponent p (p^a * m choose p^a) = exponent p m"
-proof (cases "prime p")
-  case False then show ?thesis by auto
-next
-  case True 
-  with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
+  assumes "m>0" and prime: "is_prime p"
+  shows "exponent p (p^a * m choose p^a) = exponent p m"
+proof-
+  from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
     by (auto simp: prime_gt_0_nat) 
   have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
     apply (rule p_not_div_choose [where K = "p^a"])
-    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono)
+    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono prime)
   have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
   proof -
-    have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)"
-      using p One_nat_def times_binomial_minus1_eq by presburger
-    moreover have "exponent p (p ^ a) = a"
-      by (meson True exponent_power_eq)
-    ultimately show ?thesis
-      using * p 
-      by (metis (no_types, lifting) One_nat_def exponent_1_eq_0 exponent_mult_add mult.commute mult.right_neutral nat_0_less_mult_iff zero_less_binomial)
+    have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))" 
+      (is "_ = ?rhs") using prime 
+      by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
+    also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
+    with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
+      by (subst prime_multiplicity_mult_distrib) auto
+    also have "\<dots> = a + multiplicity p m" 
+      using prime p by (subst prime_multiplicity_mult_distrib) simp_all
+    finally show ?thesis .
   qed
   then show ?thesis
-    using True p exponent_mult_add by auto
+    using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
 qed
 
 end
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
+imports "~~/src/HOL/Number_Theory/Primes" QuotRing Lattice Int
 begin
 
 section \<open>The Ring of Integers\<close>
@@ -240,18 +240,18 @@
  apply (elim exE)
 proof -
   fix a b x
-  assume "a * b = x * int p"
+  assume "a * b = x * p"
   then have "p dvd a * b" by simp
   then have "p dvd a \<or> p dvd b"
     by (metis prime prime_dvd_mult_eq_int)
-  then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
+  then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
     by (metis dvd_def mult.commute)
 next
-  assume "UNIV = {uu. EX x. uu = x * int p}"
-  then obtain x where "1 = x * int p" by best
-  then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
-  then show False
-    by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
+  assume "UNIV = {uu. EX x. uu = x * p}"
+  then obtain x where "1 = x * p" by best
+  then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
+  then show False using prime
+    by (auto dest!: abs_zmult_eq_1 simp: is_prime_def)
 qed
 
 
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -129,11 +129,15 @@
 
 lemma max_p_div_calM:
      "~ (p ^ Suc(exponent p m) dvd card(calM))"
-proof -
-  have "exponent p m = exponent p (card calM)"
-    by (simp add: card_calM const_p_fac zero_less_m)
-  then show ?thesis
-    by (metis Suc_n_not_le_n exponent_ge prime_p zero_less_card_calM)
+proof
+  assume "p ^ Suc (multiplicity p m) dvd card calM"
+  with zero_less_card_calM prime_p 
+  have "Suc (multiplicity p m) \<le> multiplicity p (card calM)"
+    by (intro multiplicity_geI) auto
+  hence "multiplicity p m < multiplicity p (card calM)" by simp
+  also have "multiplicity p m = multiplicity p (card calM)"
+    by (simp add: const_p_fac prime_p zero_less_m card_calM)
+  finally show False by simp
 qed
 
 lemma finite_calM: "finite calM"
@@ -305,7 +309,7 @@
 apply (rule dvd_imp_le)
  apply (rule div_combine [OF prime_p not_dvd_M])
  prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
-apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
+apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
                  zero_less_m)
 done
 
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -1005,7 +1005,14 @@
   have "subset_mset.bdd_above A"
     by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
   with assms show ?thesis by (simp add: in_Sup_multiset_iff)
-qed    
+qed
+
+interpretation subset_mset: distrib_lattice "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
+proof
+  fix A B C :: "'a multiset"
+  show "A #\<union> (B #\<inter> C) = A #\<union> B #\<inter> (A #\<union> C)"
+    by (intro multiset_eqI) simp_all
+qed
 
 
 subsubsection \<open>Filter (with comprehension syntax)\<close>
@@ -1835,6 +1842,12 @@
   "setsum f A = msetsum (image_mset f (mset_set A))"
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
+lemma msetsum_delta: "msetsum (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
+  by (induction A) simp_all
+
+lemma msetsum_delta': "msetsum (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
+  by (induction A) simp_all
+
 end
 
 lemma msetsum_diff:
@@ -1910,6 +1923,12 @@
   "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
 
+lemma msetprod_delta: "msetprod (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
+  by (induction A) (simp_all add: mult_ac)
+
+lemma msetprod_delta': "msetprod (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
+  by (induction A) (simp_all add: mult_ac)
+
 end
 
 syntax (ASCII)
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -67,7 +67,7 @@
 (* Goldblatt: Exercise 5.11(3a) - p 57  *)
 lemma starprime:
   "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
-by (transfer, auto simp add: prime_def)
+by (transfer, auto simp add: is_prime_nat_iff)
 
 (* Goldblatt Exercise 5.11(3b) - p 57  *)
 lemma hyperprime_factor_exists [rule_format]:
@@ -276,7 +276,8 @@
 apply clarify
 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
 apply (force simp add: starprime_def)
-apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime imageE insert_iff mem_Collect_eq zero_not_prime_nat)
+  apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime 
+           imageE insert_iff mem_Collect_eq not_is_prime_0)
 done
 
 end
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -295,8 +295,8 @@
     from 2 show ?thesis
       apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
         dest: prime_gt_Suc_0_nat)
-      apply (metis One_nat_def Suc_le_eq less_not_refl prime_def)
-      apply (metis One_nat_def Suc_le_eq aux prime_def)
+      apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
+      apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
       done
   qed
 qed
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -7,8 +7,8 @@
 
 theory Factorial_Ring
 imports 
-  Main 
-  "~~/src/HOL/Number_Theory/Primes"
+  Main
+  "../GCD"
   "~~/src/HOL/Library/Multiset"
 begin
 
@@ -84,6 +84,15 @@
   shows "p \<noteq> 0"
   using assms by (auto intro: ccontr)
 
+
+lemma is_prime_elem_dvd_power: 
+  "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+  by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
+
+lemma is_prime_elem_dvd_power_iff:
+  "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+  by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
+
 lemma is_prime_elem_imp_nonzero [simp]:
   "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
   unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
@@ -94,12 +103,13 @@
 
 end
 
-lemma (in algebraic_semidom) mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
-  by (subst mult.commute) (rule mult_unit_dvd_iff)
-
 context algebraic_semidom
 begin
 
+(* TODO Move *)
+lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
+  by (subst mult.commute) (rule mult_unit_dvd_iff)
+
 lemma prime_imp_irreducible:
   assumes "is_prime_elem p"
   shows   "irreducible p"
@@ -191,6 +201,29 @@
     by (auto simp add: mult_unit_dvd_iff)
 qed
 
+context
+begin
+
+private lemma is_prime_elem_powerD:
+  assumes "is_prime_elem (p ^ n)"
+  shows   "is_prime_elem p \<and> n = 1"
+proof (cases n)
+  case (Suc m)
+  note assms
+  also from Suc have "p ^ n = p * p^m" by simp
+  finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
+  moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
+  ultimately have "is_unit (p ^ m)" by simp
+  with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
+  with Suc assms show ?thesis by simp
+qed (insert assms, simp_all)
+
+lemma is_prime_elem_power_iff:
+  "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
+  by (auto dest: is_prime_elem_powerD)
+
+end
+
 lemma irreducible_mult_unit_left:
   "is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
   by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
@@ -235,6 +268,10 @@
 lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
   by (auto simp add: is_prime_def)
 
+lemma is_prime_power_iff:
+  "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
+  by (auto simp: is_prime_def is_prime_elem_power_iff)
+
 lemma is_prime_elem_not_unit' [simp]:
   "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
   unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
@@ -273,6 +310,20 @@
     by (blast intro: is_prime_elemD2)
 qed
 
+lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
+  by (intro prime_divides_productD) simp_all
+
+lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+  by (auto dest: is_prime_dvd_multD)
+
+lemma is_prime_dvd_power: 
+  "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+  by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
+
+lemma is_prime_dvd_power_iff:
+  "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+  by (intro is_prime_elem_dvd_power_iff) simp_all
+
 lemma prime_dvd_msetprodE:
   assumes "is_prime_elem p"
   assumes dvd: "p dvd msetprod A"
@@ -499,6 +550,50 @@
     by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
 qed (insert assms, auto simp: irreducible_not_unit)
 
+lemma is_prime_elem_imp_coprime:
+  assumes "is_prime_elem p" "\<not>p dvd n"
+  shows   "coprime p n"
+proof (rule coprimeI)
+  fix d assume "d dvd p" "d dvd n"
+  show "is_unit d"
+  proof (rule ccontr)
+    assume "\<not>is_unit d"
+    from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
+      by (rule is_prime_elemD2)
+    from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
+    with \<open>\<not>p dvd n\<close> show False by contradiction
+  qed
+qed
+
+lemma is_prime_imp_coprime:
+  assumes "is_prime p" "\<not>p dvd n"
+  shows   "coprime p n"
+  using assms by (simp add: is_prime_elem_imp_coprime)
+
+lemma is_prime_elem_imp_power_coprime: 
+  "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
+
+lemma is_prime_imp_power_coprime: 
+  "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (simp add: is_prime_elem_imp_power_coprime)
+
+lemma prime_divprod_pow:
+  assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
+  shows   "p^n dvd a \<or> p^n dvd b"
+  using assms
+proof -
+  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
+    by (auto simp: coprime is_prime_elem_def)
+  with p have "coprime (p^n) a \<or> coprime (p^n) b" 
+    by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
+  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
+qed
+
+lemma primes_coprime: 
+  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+  using is_prime_imp_coprime primes_dvd_imp_eq by blast
+
 end
 
 
@@ -683,12 +778,10 @@
   using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
 
 lemma multiplicity_eq_zero_iff:
-  assumes "x \<noteq> 0" "\<not>is_unit p"
   shows   "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   using power_dvd_iff_le_multiplicity[of 1] by auto
 
 lemma multiplicity_gt_zero_iff:
-  assumes "x \<noteq> 0" "\<not>is_unit p"
   shows   "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   using power_dvd_iff_le_multiplicity[of 1] by auto
 
@@ -716,6 +809,19 @@
 lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
   by (simp add: multiplicity_def)
 
+lemma prime_multiplicity_eq_zero_iff:
+  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
+  by (rule multiplicity_eq_zero_iff) simp_all
+
+lemma prime_multiplicity_other:
+  assumes "is_prime p" "is_prime q" "p \<noteq> q"
+  shows   "multiplicity p q = 0"
+  using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
+
+lemma prime_multiplicity_gt_zero_iff:
+  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
+  by (rule multiplicity_gt_zero_iff) simp_all
+
 lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
   by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
 
@@ -1008,7 +1114,7 @@
   also have "multiplicity p \<dots> = multiplicity p x"
     by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
   finally show ?thesis .
-qed simp_all
+qed simp_all   
 
 lemma prime_factorization_cong:
   "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
@@ -1062,6 +1168,10 @@
   finally show ?thesis ..
 qed
 
+lemma prime_factorization_subset_imp_dvd: 
+  "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
+  by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
+
 lemma prime_factorization_divide:
   assumes "b dvd a"
   shows   "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
@@ -1077,6 +1187,204 @@
   by (auto dest: in_prime_factorization_imp_prime)
 
 
+lemma prime_multiplicity_mult_distrib:
+  assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
+  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
+proof -
+  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
+    by (subst count_prime_factorization_prime) (simp_all add: assms)
+  also from assms 
+    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
+      by (intro prime_factorization_mult)
+  also have "count \<dots> (normalize p) = 
+    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
+    by simp
+  also have "\<dots> = multiplicity p x + multiplicity p y" 
+    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
+  finally show ?thesis .
+qed
+
+lemma prime_multiplicity_power_distrib:
+  assumes "is_prime_elem p" "x \<noteq> 0"
+  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
+  by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
+
+lemma prime_multiplicity_msetprod_distrib:
+  assumes "is_prime_elem p" "0 \<notin># A"
+  shows   "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
+  using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
+
+lemma prime_multiplicity_setprod_distrib:
+  assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
+  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
+proof -
+  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
+    using assms by (subst setprod_unfold_msetprod)
+                   (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum 
+                      multiset.map_comp o_def)
+  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
+    by (induction A rule: finite_induct) simp_all
+  finally show ?thesis .
+qed
+
+
+
+definition prime_factors where
+  "prime_factors x = set_mset (prime_factorization x)"
+
+lemma set_mset_prime_factorization:
+  "set_mset (prime_factorization x) = prime_factors x"
+  by (simp add: prime_factors_def)
+
+lemma prime_factorsI:
+  "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
+  by (auto simp: prime_factors_def in_prime_factorization_iff)
+
+lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
+  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
+
+lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
+  by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd)
+
+lemma prime_factors_finite [iff]:
+  "finite (prime_factors n)"
+  unfolding prime_factors_def by simp
+
+lemma prime_factors_altdef_multiplicity:
+  "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
+  by (cases "n = 0")
+     (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff 
+        prime_imp_prime_elem in_prime_factorization_iff)
+
+lemma setprod_prime_factors:
+  assumes "x \<noteq> 0"
+  shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
+proof -
+  have "normalize x = msetprod (prime_factorization x)"
+    by (simp add: msetprod_prime_factorization assms)
+  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
+    by (subst msetprod_multiplicity) (simp_all add: prime_factors_def)
+  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
+    by (intro setprod.cong) 
+      (simp_all add: assms count_prime_factorization_prime prime_factors_prime)
+  finally show ?thesis ..
+qed
+
+(* TODO Move *)
+lemma (in semidom) setprod_zero_iff [simp]:
+  assumes "finite A"
+  shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+  using assms by (induct A) (auto simp: no_zero_divisors)
+(* END TODO *)
+
+lemma prime_factorization_unique'':
+  assumes S_eq: "S = {p. 0 < f p}"
+    and "finite S"
+    and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
+  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+proof
+  define A where "A = Abs_multiset f"
+  from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
+  with S(2) have nz: "n \<noteq> 0" by auto
+  from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
+    unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+  from S_eq count_A have set_mset_A: "set_mset A = S"
+    by (simp only: set_mset_def)
+  from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
+  also have "\<dots> = msetprod A" by (simp add: msetprod_multiplicity S_eq set_mset_A count_A)
+  also from nz have "normalize n = msetprod (prime_factorization n)" 
+    by (simp add: msetprod_prime_factorization)
+  finally have "prime_factorization (msetprod A) = 
+                  prime_factorization (msetprod (prime_factorization n))" by simp
+  also from S(1) have "prime_factorization (msetprod A) = A"
+    by (intro prime_factorization_msetprod_primes) (auto simp: set_mset_A)
+  also have "prime_factorization (msetprod (prime_factorization n)) = prime_factorization n"
+    by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
+  finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
+  
+  show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+  proof safe
+    fix p :: 'a assume p: "is_prime p"
+    have "multiplicity p n = multiplicity p (normalize n)" by simp
+    also have "normalize n = msetprod A" 
+      by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
+    also from p set_mset_A S(1) 
+    have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
+      by (intro prime_multiplicity_msetprod_distrib) auto
+    also from S(1) p
+    have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
+      by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
+    also have "msetsum \<dots> = f p" by (simp add: msetsum_delta' count_A)
+    finally show "f p = multiplicity p n" ..
+  qed
+qed
+
+lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
+  by (rule multiplicity_self) auto
+
+lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
+  by (subst multiplicity_same_power') auto
+
+lemma prime_factors_product: 
+  "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
+  by (simp add: prime_factors_def prime_factorization_mult)
+
+lemma multiplicity_distinct_prime_power:
+  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
+  by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
+
+lemma dvd_imp_multiplicity_le:
+  assumes "a dvd b" "b \<noteq> 0"
+  shows   "multiplicity p a \<le> multiplicity p b"
+proof (cases "is_unit p")
+  case False
+  with assms show ?thesis
+    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
+qed (insert assms, auto simp: multiplicity_unit_left)
+
+lemma dvd_prime_factors [intro]:
+  "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
+  unfolding prime_factors_def
+  by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
+
+(* RENAMED multiplicity_dvd *)
+lemma multiplicity_le_imp_dvd:
+  assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
+  shows   "x dvd y"
+proof (cases "y = 0")
+  case False
+  from assms this have "prime_factorization x \<subseteq># prime_factorization y"
+    by (intro mset_subset_eqI) (auto simp: count_prime_factorization)
+  with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd)
+qed auto
+
+lemma dvd_multiplicity_eq:
+  "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
+  by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
+
+lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
+  by (auto intro: prime_factorsI)
+
+lemma multiplicity_eq_imp_eq:
+  assumes "x \<noteq> 0" "y \<noteq> 0"
+  assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  shows   "normalize x = normalize y"
+  using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
+
+lemma prime_factorization_unique':
+  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)"
+  shows   "M = N"
+proof -
+  have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
+    by (simp only: assms)
+  also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
+    by (subst prime_factorization_msetprod_primes) simp_all
+  also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
+    by (subst prime_factorization_msetprod_primes) simp_all
+  finally show ?thesis .
+qed
+
+
 definition "gcd_factorial a b = (if a = 0 then normalize b
      else if b = 0 then normalize a
      else msetprod (prime_factorization a #\<inter> prime_factorization b))"
@@ -1418,6 +1726,72 @@
   by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
      (rule gcd_lcm_factorial; assumption)+
 
+lemma
+  assumes "x \<noteq> 0" "y \<noteq> 0"
+  shows gcd_eq_factorial': 
+          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. 
+                          p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
+    and lcm_eq_factorial':
+          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. 
+                          p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
+proof -
+  have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
+  also have "\<dots> = ?rhs1"
+    by (auto simp: gcd_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
+          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
+  finally show "gcd x y = ?rhs1" .
+  have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
+  also have "\<dots> = ?rhs2"
+    by (auto simp: lcm_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
+          count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
+  finally show "lcm x y = ?rhs2" .
+qed
+
+lemma
+  assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
+  shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
+    and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
+proof -
+  have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
+  also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)"
+    by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial)
+  finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" .
+  have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
+  also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)"
+    by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial)
+  finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" .
+qed
+
+lemma gcd_lcm_distrib:
+  "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
+proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
+  case True
+  thus ?thesis
+    by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
+next
+  case False
+  hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
+    by (intro associatedI prime_factorization_subset_imp_dvd)
+       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
+          subset_mset.inf_sup_distrib1)
+  thus ?thesis by simp
+qed
+
+lemma lcm_gcd_distrib:
+  "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)"
+proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
+  case True
+  thus ?thesis
+    by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
+next
+  case False
+  hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
+    by (intro associatedI prime_factorization_subset_imp_dvd)
+       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
+          subset_mset.sup_inf_distrib1)
+  thus ?thesis by simp
+qed
+
 end
 
 
@@ -1430,37 +1804,5 @@
 
 end
 
-
-lemma is_prime_elem_nat: "is_prime_elem (n::nat) \<longleftrightarrow> prime n"
-proof
-  assume *: "is_prime_elem n"
-  show "prime n" unfolding prime_def
-  proof safe
-    from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
-    thus "n > 1" by (cases n) simp_all
-  next
-    fix m assume m: "m dvd n" "m \<noteq> n"
-    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
-      by (intro irreducibleD' prime_imp_irreducible)
-    with m show "m = 1" by (auto dest: dvd_antisym)
-  qed
-qed (auto simp: is_prime_elem_def prime_gt_0_nat)
-
-lemma is_prime_nat: "is_prime (n::nat) \<longleftrightarrow> prime n"
-  by (simp add: is_prime_def is_prime_elem_nat)
-
-lemma is_prime_elem_int: "is_prime_elem (n::int) \<longleftrightarrow> prime (nat (abs n))"
-proof (subst is_prime_elem_nat [symmetric], rule iffI)
-  assume "is_prime_elem n"
-  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
-next
-  assume "is_prime_elem (nat (abs n))"
-  thus "is_prime_elem n"
-    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
-qed
-
-lemma is_prime_int: "is_prime (n::int) \<longleftrightarrow> prime n \<and> n \<ge> 0"
-  by (simp add: is_prime_def is_prime_elem_int)
-
 end
 
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -109,10 +109,12 @@
     assume c: "x \<le> (int p - 1) div 2"
     assume d: "0 < y"
     assume e: "y \<le> (int p - 1) div 2"
-    from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
-    have "[x = y](mod p)"
-      by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
-                cong_mult_self_int gcd.commute prime_imp_coprime_int)
+    from p_a_relprime have "\<not>p dvd a"
+      by (simp add: cong_altdef_int)
+    with p_prime have "coprime a (int p)" 
+       by (subst gcd.commute, intro is_prime_imp_coprime) auto
+    with a cong_mult_rcancel_int [of a "int p" x y]
+      have "[x = y] (mod p)" by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
         order_le_less_trans [of x "(int p - 1) div 2" p]
         order_le_less_trans [of y "(int p - 1) div 2" p] 
@@ -137,11 +139,14 @@
   assume d: "0 < y"
   assume e: "y \<le> (int p - 1) div 2"
   assume f: "x \<noteq> y"
-  from a have "[x * a = y * a](mod p)" 
+  from a have a': "[x * a = y * a](mod p)" 
     by (metis cong_int_def)
-  with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
-  have "[x = y](mod p)" 
-    by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int)
+  from p_a_relprime have "\<not>p dvd a"
+    by (simp add: cong_altdef_int)
+  with p_prime have "coprime a (int p)" 
+     by (subst gcd.commute, intro is_prime_imp_coprime) auto
+  with a' cong_mult_rcancel_int [of a "int p" x y]
+    have "[x = y] (mod p)" by simp
   with cong_less_imp_eq_int [of x y p] p_minus_one_l
     order_le_less_trans [of x "(int p - 1) div 2" p]
     order_le_less_trans [of y "(int p - 1) div 2" p] 
@@ -170,7 +175,7 @@
   by (auto simp add: A_def)
 
 lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
-  by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
+  by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int) 
 
 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
   using a_nonzero by (auto simp add: B_def A_greater_zero)
@@ -202,7 +207,7 @@
 
 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
   using p_prime A_ncong_p [OF assms]
-  by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
+  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
 
 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
   by (metis id_def all_A_relprime setprod_coprime)
@@ -266,7 +271,7 @@
     by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
   with p_prime a_nonzero p_a_relprime
   have a: "[y + z = 0] (mod p)"
-    by (metis cong_prime_prod_zero_int)
+    by (auto dest!: cong_prime_prod_zero_int)
   assume b: "y \<in> A" and c: "z \<in> A"
   with A_def have "0 < y + z"
     by auto
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -11,39 +11,17 @@
 subsection\<open>Lemmas about previously defined terms\<close>
 
 lemma prime: 
-  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume "p=0 \<or> p=1" hence ?thesis
-    by (metis one_not_prime_nat zero_not_prime_nat)}
-  moreover
-  {assume p0: "p\<noteq>0" "p\<noteq>1"
-    {assume H: "?lhs"
-      {fix m assume m: "m > 0" "m < p"
-        {assume "m=1" hence "coprime p m" by simp}
-        moreover
-        {assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2)
-          have "coprime p m" by simp}
-        ultimately have "coprime p m" 
-          by (metis H prime_imp_coprime_nat)}
-      hence ?rhs using p0 by auto}
-    moreover
-    { assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m"
-      obtain q where q: "prime q" "q dvd p"
-        by (metis p0(2) prime_factor_nat) 
-      have q0: "q > 0"
-        by (metis prime_gt_0_nat q(1))
-      from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith
-      {assume "q = p" hence ?lhs using q(1) by blast}
-      moreover
-      {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
-        from H qplt q0 have "coprime p q" by arith
-       hence ?lhs using q
-         by (auto dest: gcd_nat.absorb2)}
-      ultimately have ?lhs by blast}
-    ultimately have ?thesis by blast}
-  ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
-qed
+  "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
+  unfolding is_prime_nat_iff
+proof safe
+  fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p" 
+           and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
+  from p m have "m \<noteq> 0" by (intro notI) auto
+  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
+  ultimately have "coprime p m" using * by blast
+  with m show "m = 1" by simp
+qed (auto simp: is_prime_nat_iff simp del: One_nat_def 
+          intro!: is_prime_imp_coprime dest: dvd_imp_le)
 
 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
 proof-
@@ -94,7 +72,7 @@
 qed
 
 lemma cong_solve_unique_nontrivial:
-  assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
+  assumes p: "prime (p::nat)" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
 proof-
   from pa have ap: "coprime a p"
@@ -107,12 +85,12 @@
     with y(2) have th: "p dvd a"
       by (auto dest: cong_dvd_eq_nat)
     have False
-      by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
+      by (metis gcd_nat.absorb1 not_is_prime_1 p pa th)}
   with y show ?thesis unfolding Ex1_def using neq0_conv by blast
 qed
 
 lemma cong_unique_inverse_prime:
-  assumes "prime p" and "0 < x" and "x < p"
+  assumes "prime (p::nat)" and "0 < x" and "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
   by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
 
@@ -445,28 +423,28 @@
 subsection\<open>Another trivial primality characterization\<close>
 
 lemma prime_prime_factor:
-  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
+  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof (cases "n=0 \<or> n=1")
   case True
   then show ?thesis
-     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
+     by (metis bigger_prime dvd_0_right not_is_prime_1 not_is_prime_0)
 next
   case False
   show ?thesis
   proof
     assume "prime n"
     then show ?rhs
-      by (metis one_not_prime_nat prime_def)
+      by (metis  not_is_prime_1 is_prime_nat_iff)
   next
     assume ?rhs
     with False show "prime n"
-      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_def)
+      by (auto simp: is_prime_nat_iff) (metis One_nat_def prime_factor_nat is_prime_nat_iff)
   qed
 qed
 
 lemma prime_divisor_sqrt:
-  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
+  "prime (n::nat) \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
 proof -
   {assume "n=0 \<or> n=1" hence ?thesis
     by auto}
@@ -497,17 +475,17 @@
         with H[rule_format, of e] h have "e=1" by simp
         with e have "d = n" by simp}
       ultimately have "d=1 \<or> d=n"  by blast}
-    ultimately have ?thesis unfolding prime_def using np n(2) by blast}
+    ultimately have ?thesis unfolding is_prime_nat_iff using np n(2) by blast}
   ultimately show ?thesis by auto
 qed
 
 lemma prime_prime_factor_sqrt:
-  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
+  "prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   (is "?lhs \<longleftrightarrow>?rhs")
 proof-
   {assume "n=0 \<or> n=1" 
    hence ?thesis
-     by (metis one_not_prime_nat zero_not_prime_nat)}
+     by (metis not_is_prime_0 not_is_prime_1)}
   moreover
   {assume n: "n\<noteq>0" "n\<noteq>1"
     {assume H: ?lhs
@@ -535,10 +513,10 @@
 lemma pocklington_lemma:
   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
-  and pp: "prime p" and pn: "p dvd n"
+  and pp: "prime (p::nat)" and pn: "p dvd n"
   shows "[p = 1] (mod q)"
 proof -
-  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by (auto intro: prime_gt_0_nat)
+  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp by (auto intro: prime_gt_0_nat)
   obtain k where k: "a ^ (q * r) - 1 = n*k"
     by (metis an cong_to_1_nat dvd_def nqr)
   from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
@@ -561,7 +539,7 @@
     from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
     from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
     have P0: "P \<noteq> 0" using P(1)
-      by (metis zero_not_prime_nat) 
+      by (metis not_is_prime_0) 
     from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
     from d s t P0  have s': "ord p (a^r) * t = s"
       by (metis mult.commute mult_cancel1 mult.assoc) 
@@ -581,7 +559,7 @@
   hence o: "ord p (a^r) = q" using d by simp
   from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
   {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
-    from pp[unfolded prime_def] d have dp: "d = p" by blast
+    from pp[unfolded is_prime_nat_iff] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
     then have False using d dp pn
       by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
@@ -667,36 +645,28 @@
 
 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
-definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
+definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
 
-lemma primefact: assumes n: "n \<noteq> 0"
+lemma primefact: 
+  assumes n: "n \<noteq> (0::nat)"
   shows "\<exists>ps. primefact ps n"
-using n
-proof(induct n rule: nat_less_induct)
-  fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0"
-  let ?ths = "\<exists>ps. primefact ps n"
-  {assume "n = 1"
-    hence "primefact [] n" by (simp add: primefact_def)
-    hence ?ths by blast }
-  moreover
-  {assume n1: "n \<noteq> 1"
-    with n have n2: "n \<ge> 2" by arith
-    obtain p where p: "prime p" "p dvd n"
-      by (metis n1 prime_factor_nat) 
-    from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
-    from n m have m0: "m > 0" "m\<noteq>0" by auto
-    have "1 < p"
-      by (metis p(1) prime_def)
-    with m0 m have mn: "m < n" by auto
-    from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
-    from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
-    hence ?ths by blast}
-  ultimately show ?ths by blast
+proof -
+  have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
+  then guess xs .. note xs = this
+  from assms have "n = msetprod (prime_factorization n)" 
+    by (simp add: msetprod_prime_factorization)
+  also have "\<dots> = msetprod (mset xs)" by (simp add: xs)
+  also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
+  finally have "foldr op * xs 1 = n" ..
+  moreover have "\<forall>p\<in>#mset xs. prime p"
+    by (subst xs) (auto dest: in_prime_factorization_imp_prime)
+  ultimately have "primefact xs n" by (auto simp: primefact_def)
+  thus ?thesis ..
 qed
 
 lemma primefact_contains:
   assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n"
-  shows "p \<in> set ps"
+  shows "(p::nat) \<in> set ps"
   using pf p pn
 proof(induct ps arbitrary: p n)
   case Nil thus ?case by (auto simp add: primefact_def)
@@ -705,7 +675,7 @@
   from Cons.prems[unfolded primefact_def]
   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
   {assume "p dvd q"
-    with p(1) q(1) have "p = q" unfolding prime_def by auto
+    with p(1) q(1) have "p = q" unfolding is_prime_nat_iff by auto
     hence ?case by simp}
   moreover
   { assume h: "p dvd foldr op * qs 1"
@@ -760,7 +730,7 @@
     from psp primefact_contains[OF pfpsq p]
     have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
       by (simp add: list_all_iff)
-    from p prime_def have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
+    from p is_prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" 
       by auto
     from div_mult1_eq[of r q p] p(2)
     have eq1: "r* (q div p) = (n - 1) div p"
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -1,5 +1,6 @@
 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
-                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
+                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
+                Manuel Eberl
 
 
 This file deals with properties of primes. Definitions and lemmas are
@@ -22,211 +23,246 @@
 natural numbers and the integers, and added a number of new theorems.
 
 Tobias Nipkow cleaned up a lot.
+
+Florian Haftmann and Manuel Eberl put primality and prime factorisation
+onto an algebraic foundation and thus generalised these concepts to 
+other rings, such as polynomials. (see also the Factorial_Ring theory).
+
+There were also previous formalisations of unique factorisation by 
+Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
 *)
 
 
 section \<open>Primes\<close>
 
 theory Primes
-imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
+imports "~~/src/HOL/Binomial" Euclidean_Algorithm
 begin
 
+(* As a simp or intro rule,
+
+     prime p \<Longrightarrow> p > 0
+
+   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
+   leads to the backchaining
+
+     x > 0
+     prime x
+     x \<in># M   which is, unfortunately,
+     count M x > 0
+*)
+
 declare [[coercion int]]
 declare [[coercion_enabled]]
 
-definition prime :: "nat \<Rightarrow> bool"
-  where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
+abbreviation (input) "prime \<equiv> is_prime"
+
+lemma is_prime_elem_nat_iff:
+  "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+proof safe
+  assume *: "is_prime_elem n"
+  from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
+  thus "n > 1" by (cases n) simp_all
+  fix m assume m: "m dvd n" "m \<noteq> n"
+  from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
+    by (intro irreducibleD' prime_imp_irreducible)
+  with m show "m = 1" by (auto dest: dvd_antisym)
+next
+  assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
+  thus "is_prime_elem n"
+    by (auto simp: prime_iff_irreducible irreducible_altdef)
+qed
+
+lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
+  by (simp add: is_prime_def)
 
-subsection \<open>Primes\<close>
+lemma is_prime_nat_iff:
+  "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+  by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
 
-lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
-  using nat_dvd_1_iff_1 odd_one prime_def by blast
+lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
+proof
+  assume "is_prime_elem n"
+  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
+next
+  assume "is_prime_elem (nat (abs n))"
+  thus "is_prime_elem n"
+    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
+qed
+
+lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
+  by (auto simp: is_prime_elem_int_nat_transfer)
+
+lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
+  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
+
+lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
+  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
 
-lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
-  unfolding prime_def by auto
+lemma is_prime_int_iff:
+  "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+proof (intro iffI conjI allI impI; (elim conjE)?)
+  assume *: "is_prime n"
+  hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
+  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
+    by (auto simp: is_prime_def zabs_def not_less split: if_splits)
+  thus "n > 1" by presburger
+  fix m assume "m dvd n" \<open>m \<ge> 0\<close>
+  with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
+  with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
+    using associated_iff_dvd[of m n] by auto
+next
+  assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
+  hence "nat n > 1" by simp
+  moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
+  proof (intro allI impI)
+    fix m assume "m dvd nat n"
+    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
+    with n(2) have "int m = 1 \<or> int m = n" by auto
+    thus "m = 1 \<or> m = nat n" by auto
+  qed
+  ultimately show "is_prime n" 
+    unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
+qed
 
-lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
-  unfolding prime_def by auto
+
+lemma prime_nat_not_dvd:
+  assumes "prime p" "p > n" "n \<noteq> (1::nat)"
+  shows   "\<not>n dvd p"
+proof
+  assume "n dvd p"
+  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
+    by (cases "n = 0") (auto dest!: dvd_imp_le)
+qed
 
-lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
-  unfolding prime_def by auto
+lemma prime_int_not_dvd:
+  assumes "prime p" "p > n" "n > (1::int)"
+  shows   "\<not>n dvd p"
+proof
+  assume "n dvd p"
+  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
+    by (auto dest!: zdvd_imp_le)
+qed
+
+lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
+  by (intro prime_nat_not_dvd) auto
+
+lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
+  by (intro prime_int_not_dvd) auto
 
-lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
-  unfolding prime_def by auto
+lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
+  unfolding is_prime_int_iff by auto
+
+lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
+  unfolding is_prime_nat_iff by auto
+
+lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
+  unfolding is_prime_int_iff by auto
+
+lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
+  unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
+  unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
+  unfolding is_prime_int_iff by auto
+
+lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
+  unfolding is_prime_nat_iff by auto
 
 lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
-  unfolding prime_def by auto
+  unfolding is_prime_nat_iff by auto
 
-lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
-  unfolding prime_def by auto
+lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
+  unfolding is_prime_int_iff by auto
 
-lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
-  apply (unfold prime_def)
-  apply (metis gcd_dvd1 gcd_dvd2)
-  done
+lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
+  unfolding is_prime_nat_iff by auto
+
+lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
+  unfolding is_prime_int_iff by auto
 
 lemma prime_int_altdef:
   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
     m = 1 \<or> m = p))"
-  apply (simp add: prime_def)
-  apply (auto simp add: )
-  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
-  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
-  done
-
-lemma prime_imp_coprime_int:
-  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
-  apply (unfold prime_int_altdef)
-  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
-  done
-
-lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
-  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
-
-lemma prime_dvd_mult_int:
-  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
-  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
-
-lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
-    p dvd m * n = (p dvd m \<or> p dvd n)"
-  by (rule iffI, rule prime_dvd_mult_nat, auto)
-
-lemma prime_dvd_mult_eq_int [simp]:
-  fixes n::int
-  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
-  by (rule iffI, rule prime_dvd_mult_int, auto)
+  unfolding is_prime_int_iff by blast
 
 lemma not_prime_eq_prod_nat:
-  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
-    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
-  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
-  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
-
-lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
-  by (induct n) auto
-
-lemma prime_dvd_power_int:
-  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
-  by (induct n) auto
-
-lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
-    p dvd x^n \<longleftrightarrow> p dvd x"
-  by (cases n) (auto elim: prime_dvd_power_nat)
-
-lemma prime_dvd_power_int_iff:
-  fixes x::int
-  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
-  by (cases n) (auto elim: prime_dvd_power_int)
+  assumes "m > 1" "\<not>prime (m::nat)"
+  shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
+  using assms irreducible_altdef[of m]
+  by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
 
 
 subsubsection \<open>Make prime naively executable\<close>
 
-lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
-  by (simp add: prime_def)
-
-lemma one_not_prime_nat [simp]: "~prime (1::nat)"
-  by (simp add: prime_def)
+lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
+  unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
 
-lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
-  by (simp add: prime_def)
+lemma prime_nat_code [code_unfold]:
+  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+proof safe
+  assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
+  show "is_prime p" unfolding is_prime_nat_iff
+  proof (intro conjI allI impI)
+    fix m assume "m dvd p"
+    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
+    hence "m \<ge> 1" by simp
+    moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
+    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
+    ultimately show "m = 1 \<or> m = p" by simp
+  qed fact+
+qed (auto simp: is_prime_nat_iff)
 
-lemma prime_nat_code [code]:
-    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
-  apply (simp add: Ball_def)
-  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
-  done
+lemma prime_int_code [code_unfold]:
+  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume "?lhs"
+  thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
+next
+  assume "?rhs"
+  thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
+qed
 
 lemma prime_nat_simp:
     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   by (auto simp add: prime_nat_code)
 
+lemma prime_int_simp:
+    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
+  by (auto simp add: prime_int_code)
+
 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
 
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   by simp
 
+declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
+
+
 text\<open>A bit of regression testing:\<close>
 
 lemma "prime(97::nat)" by simp
 lemma "prime(997::nat)" by eval
-
-
-lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
-  by (metis coprime_exp gcd.commute prime_imp_coprime_nat)
-
-lemma prime_imp_power_coprime_int:
-  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
-  by (metis coprime_exp gcd.commute prime_imp_coprime_int)
-
-lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
-  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
-
-lemma primes_imp_powers_coprime_nat:
-    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
-  by (rule coprime_exp2_nat, rule primes_coprime_nat)
-
-lemma prime_factor_nat:
-  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
-proof (induct n rule: nat_less_induct)
-  case (1 n) show ?case
-  proof (cases "n = 0")
-    case True then show ?thesis
-    by (auto intro: two_is_prime_nat)
-  next
-    case False with "1.prems" have "n > 1" by simp
-    with "1.hyps" show ?thesis
-    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
-  qed
-qed
-
-text \<open>One property of coprimality is easier to prove via prime factors.\<close>
+lemma "prime(97::int)" by simp
+lemma "prime(997::int)" by eval
 
-lemma prime_divprod_pow_nat:
-  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
-  shows "p^n dvd a \<or> p^n dvd b"
-proof-
-  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
-      apply (cases "n=0", simp_all)
-      apply (cases "a=1", simp_all)
-      done }
-  moreover
-  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
-    then obtain m where m: "n = Suc m" by (cases n) auto
-    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
-    also note pab
-    finally have pab': "p dvd a * b".
-    from prime_dvd_mult_nat[OF p pab']
-    have "p dvd a \<or> p dvd b" .
-    moreover
-    { assume pa: "p dvd a"
-      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
-      with p have "coprime b p"
-        by (subst gcd.commute, intro prime_imp_coprime_nat)
-      then have pnb: "coprime (p^n) b"
-        by (subst gcd.commute, rule coprime_exp)
-      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
-    moreover
-    { assume pb: "p dvd b"
-      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
-      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
-        by auto
-      with p have "coprime a p"
-        by (subst gcd.commute, intro prime_imp_coprime_nat)
-      then have pna: "coprime (p^n) a"
-        by (subst gcd.commute, rule coprime_exp)
-      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
-    ultimately have ?thesis by blast }
-  ultimately show ?thesis by blast
-qed
+lemma prime_factor_nat: 
+  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
+  using prime_divisor_exists[of n]
+  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
 
 
 subsection \<open>Infinitely many primes\<close>
 
-lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
+lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
 proof-
   have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
   from prime_factor_nat [OF f1]
-  obtain p where "prime p" and "p dvd fact n + 1" by auto
+  obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   { assume "p \<le> n"
     from \<open>prime p\<close> have "p \<ge> 1"
@@ -238,7 +274,7 @@
     then have "p dvd 1" by simp
     then have "p <= 1" by auto
     moreover from \<open>prime p\<close> have "p > 1"
-      using prime_def by blast
+      using is_prime_nat_iff by blast
     ultimately have False by auto}
   then have "n < p" by presburger
   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
@@ -269,7 +305,7 @@
 proof -
   from assms have
     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
-    unfolding prime_def by auto
+    unfolding is_prime_nat_iff by auto
   from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   have "p dvd p * q" by simp
@@ -277,30 +313,8 @@
   then show ?thesis by (simp add: Q)
 qed
 
-lemma prime_exp:
-  fixes p::nat
-  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
-proof(induct n)
-  case 0 thus ?case by simp
-next
-  case (Suc n)
-  {assume "p = 0" hence ?case by simp}
-  moreover
-  {assume "p=1" hence ?case by simp}
-  moreover
-  {assume p: "p \<noteq> 0" "p\<noteq>1"
-    {assume pp: "prime (p^Suc n)"
-      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
-      with p have n: "n = 0"
-        by (metis One_nat_def nat_power_eq_Suc_0_iff)
-      with pp have "prime p \<and> Suc n = 1" by simp}
-    moreover
-    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
-    ultimately have ?case by blast}
-  ultimately show ?case by blast
-qed
-
-lemma prime_power_mult:
+(* TODO: Generalise? *)
+lemma prime_power_mult_nat:
   fixes p::nat
   assumes p: "prime p" and xy: "x * y = p ^ k"
   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
@@ -310,7 +324,7 @@
 next
   case (Suc k x y)
   from Suc.prems have pxy: "p dvd x*y" by auto
-  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
+  from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
   {assume px: "p dvd x"
     then obtain d where d: "x = p*d" unfolding dvd_def by blast
@@ -330,7 +344,7 @@
   ultimately show ?case  using pxyc by blast
 qed
 
-lemma prime_power_exp:
+lemma prime_power_exp_nat:
   fixes p::nat
   assumes p: "prime p" and n: "n \<noteq> 0"
     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
@@ -342,20 +356,20 @@
   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
   moreover
   {assume n: "n \<noteq> 0"
-    from prime_power_mult[OF p th]
+    from prime_power_mult_nat[OF p th]
     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
     from Suc.hyps[OF n ij(2)] have ?case .}
   ultimately show ?case by blast
 qed
 
-lemma divides_primepow:
+lemma divides_primepow_nat:
   fixes p::nat
   assumes p: "prime p"
   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
 proof
   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
     unfolding dvd_def  apply (auto simp add: mult.commute) by blast
-  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
+  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
   hence "i \<le> k" by arith
@@ -369,6 +383,7 @@
   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
 qed
 
+
 subsection \<open>Chinese Remainder Theorem Variants\<close>
 
 lemma bezout_gcd_nat:
@@ -392,6 +407,7 @@
 
 text \<open>A binary form of the Chinese Remainder Theorem.\<close>
 
+(* TODO: Generalise? *)
 lemma chinese_remainder:
   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
@@ -422,11 +438,175 @@
   shows "\<exists>x y. a*x = Suc (p*y)"
 proof -
   have ap: "coprime a p"
-    by (metis gcd.commute p pa prime_imp_coprime_nat)
+    by (metis gcd.commute p pa is_prime_imp_coprime)
   moreover from p have "p \<noteq> 1" by auto
   ultimately have "\<exists>x y. a * x = p * y + 1"
     by (rule coprime_bezout_strong)
   then show ?thesis by simp    
 qed
+(* END TODO *)
 
-end
+
+
+subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
+
+lemma prime_factors_gt_0_nat:
+  "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
+  by (simp add: prime_factors_prime prime_gt_0_nat)
+
+lemma prime_factors_gt_0_int:
+  "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
+  by (simp add: prime_factors_prime prime_gt_0_int)
+
+lemma prime_factors_ge_0_int [elim]:
+  fixes n :: int
+  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
+  unfolding prime_factors_def 
+  by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
+
+lemma msetprod_prime_factorization_int:
+  fixes n :: int
+  assumes "n > 0"
+  shows   "msetprod (prime_factorization n) = n"
+  using assms by (simp add: msetprod_prime_factorization)
+
+lemma prime_factorization_exists_nat:
+  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
+  using prime_factorization_exists[of n] by (auto simp: is_prime_def)
+
+lemma msetprod_prime_factorization_nat [simp]: 
+  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
+  by (subst msetprod_prime_factorization) simp_all
+
+lemma prime_factorization_nat:
+    "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
+  by (simp add: setprod_prime_factors)
+
+lemma prime_factorization_int:
+    "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
+  by (simp add: setprod_prime_factors)
+
+lemma prime_factorization_unique_nat:
+  fixes f :: "nat \<Rightarrow> _"
+  assumes S_eq: "S = {p. 0 < f p}"
+    and "finite S"
+    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
+  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+  using assms by (intro prime_factorization_unique'') auto
+
+lemma prime_factorization_unique_int:
+  fixes f :: "int \<Rightarrow> _"
+  assumes S_eq: "S = {p. 0 < f p}"
+    and "finite S"
+    and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
+  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+  using assms by (intro prime_factorization_unique'') auto
+
+lemma prime_factors_characterization_nat:
+  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
+    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
+  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
+
+lemma prime_factors_characterization'_nat:
+  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
+  by (rule prime_factors_characterization_nat) auto
+
+lemma prime_factors_characterization_int:
+  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
+    \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
+  by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
+
+(* TODO Move *)
+lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
+  by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
+
+lemma primes_characterization'_int [rule_format]:
+  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
+      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
+  by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
+
+lemma multiplicity_characterization_nat:
+  "S = {p. 0 < f (p::nat)} \<Longrightarrow> 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"
+  by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
+
+lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
+      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
+  by (intro impI, rule multiplicity_characterization_nat) auto
+
+lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+    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"
+  by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
+     (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
+
+lemma multiplicity_characterization'_int [rule_format]:
+  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
+      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
+  by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
+
+lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
+  unfolding One_nat_def [symmetric] by (rule multiplicity_one)
+
+lemma multiplicity_eq_nat:
+  fixes x and y::nat
+  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  shows "x = y"
+  using multiplicity_eq_imp_eq[of x y] assms by simp
+
+lemma multiplicity_eq_int:
+  fixes x y :: int
+  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  shows "x = y"
+  using multiplicity_eq_imp_eq[of x y] assms by simp
+
+lemma multiplicity_prod_prime_powers:
+  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
+  shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
+proof -
+  define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
+  define A where "A = Abs_multiset g"
+  have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
+  from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
+    by (simp add: multiset_def)
+  from assms have count_A: "count A x = g x" for x unfolding A_def
+    by simp
+  have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
+    unfolding set_mset_def count_A by (auto simp: g_def)
+  with assms have prime: "prime x" if "x \<in># A" for x using that by auto
+  from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
+    by (intro setprod.cong) (auto simp: g_def)
+  also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
+    by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
+  also have "\<dots> = msetprod A"
+    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
+  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
+    by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
+  also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
+    by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
+  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
+  finally show ?thesis .
+qed
+
+(* TODO Legacy names *)
+lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
+lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
+lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
+lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
+lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
+lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
+lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
+lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
+lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
+lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
+lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
+lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
+
+end
\ No newline at end of file
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -202,9 +202,9 @@
 subsection \<open>Prime residues\<close>
 
 locale residues_prime =
-  fixes p and R (structure)
+  fixes p :: nat and R (structure)
   assumes p_prime [intro]: "prime p"
-  defines "R \<equiv> residue_ring p"
+  defines "R \<equiv> residue_ring (int p)"
 
 sublocale residues_prime < residues p
   apply (unfold R_def residues_def)
@@ -223,7 +223,7 @@
   apply (erule notE)
   apply (subst gcd.commute)
   apply (rule prime_imp_coprime_int)
-  apply (rule p_prime)
+  apply (simp add: p_prime)
   apply (rule notI)
   apply (frule zdvd_imp_le)
   apply auto
@@ -280,7 +280,7 @@
   qed
   then show ?thesis
     using \<open>2 \<le> p\<close>
-    by (simp add: prime_def)
+    by (simp add: is_prime_nat_iff)
        (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
               not_numeral_le_zero one_dvd)
 qed
@@ -347,19 +347,21 @@
   apply auto
   done
 
-lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
+lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
   apply (rule residues_prime.phi_prime)
+  apply simp
   apply (erule residues_prime.intro)
   done
 
 lemma fermat_theorem:
   fixes a :: int
-  assumes "prime p"
+  assumes "prime (int p)"
     and "\<not> p dvd a"
   shows "[a^(p - 1) = 1] (mod p)"
 proof -
   from assms have "[a ^ phi p = 1] (mod p)"
-    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
+    by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
+             simp: gcd.commute[of _ "int p"])
   also have "phi p = nat p - 1"
     by (rule phi_prime) (rule assms)
   finally show ?thesis
@@ -367,7 +369,7 @@
 qed
 
 lemma fermat_theorem_nat:
-  assumes "prime p" and "\<not> p dvd a"
+  assumes "prime (int p)" and "\<not> p dvd a"
   shows "[a ^ (p - 1) = 1] (mod p)"
   using fermat_theorem [of p a] assms
   by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -12,817 +12,4 @@
 imports Cong "~~/src/HOL/Library/Multiset"
 begin
 
-(* As a simp or intro rule,
-
-     prime p \<Longrightarrow> p > 0
-
-   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
-   leads to the backchaining
-
-     x > 0
-     prime x
-     x \<in># M   which is, unfortunately,
-     count M x > 0
-*)
-
-(* Here is a version of set product for multisets. Is it worth moving
-   to multiset.thy? If so, one should similarly define msetsum for abelian
-   semirings, using of_nat. Also, is it worth developing bounded quantifiers
-   "\<forall>i \<in># M. P i"?
-*)
-
-
-subsection \<open>Unique factorization: multiset version\<close>
-
-lemma multiset_prime_factorization_exists:
-  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
-proof (induct n rule: nat_less_induct)
-  fix n :: nat
-  assume ih: "\<forall>m < n. 0 < m \<longrightarrow> (\<exists>M. (\<forall>p\<in>set_mset M. prime p) \<and> m = (\<Prod>i \<in># M. i))"
-  assume "n > 0"
-  then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
-    by arith
-  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i\<in>#M. i)"
-  proof cases
-    case 1
-    then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"
-      by auto
-    then show ?thesis ..
-  next
-    case 2
-    then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)"
-      by auto
-    then show ?thesis ..
-  next
-    case 3
-    with not_prime_eq_prod_nat
-    obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
-      by blast
-    with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)"
-        and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)"
-      by blast
-    then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)"
-      by (auto simp add: n msetprod_Un)
-    then show ?thesis ..
-  qed
-qed
-
-lemma multiset_prime_factorization_unique_aux:
-  fixes a :: nat
-  assumes "\<forall>p\<in>set_mset M. prime p"
-    and "\<forall>p\<in>set_mset N. prime p"
-    and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)"
-  shows "count M a \<le> count N a"
-proof (cases "a \<in> set_mset M")
-  case True
-  with assms have a: "prime a"
-    by auto
-  with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)"
-    by (auto simp add: msetprod_multiplicity)
-  also have "\<dots> dvd (\<Prod>i \<in># N. i)"
-    by (rule assms)
-  also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)"
-    by (simp add: msetprod_multiplicity)
-  also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
-  proof (cases "a \<in> set_mset N")
-    case True
-    then have b: "set_mset N = {a} \<union> (set_mset N - {a})"
-      by auto
-    then show ?thesis
-      by (subst (1) b, subst setprod.union_disjoint, auto)
-  next
-    case False
-    then show ?thesis
-      by (auto simp add: not_in_iff)
-  qed
-  finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
-  moreover
-  have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
-    apply (subst gcd.commute)
-    apply (rule setprod_coprime)
-    apply (rule primes_imp_powers_coprime_nat)
-    using assms True
-    apply auto
-    done
-  ultimately have "a ^ count M a dvd a ^ count N a"
-    by (elim coprime_dvd_mult)
-  with a show ?thesis
-    using power_dvd_imp_le prime_def by blast
-next
-  case False
-  then show ?thesis
-    by (auto simp add: not_in_iff)
-qed
-
-lemma multiset_prime_factorization_unique:
-  assumes "\<forall>p::nat \<in> set_mset M. prime p"
-    and "\<forall>p \<in> set_mset N. prime p"
-    and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
-  shows "M = N"
-proof -
-  have "count M a = count N a" for a
-  proof -
-    from assms have "count M a \<le> count N a"
-      by (intro multiset_prime_factorization_unique_aux, auto)
-    moreover from assms have "count N a \<le> count M a"
-      by (intro multiset_prime_factorization_unique_aux, auto)
-    ultimately show ?thesis
-      by auto
-  qed
-  then show ?thesis
-    by (simp add: multiset_eq_iff)
-qed
-
-definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset"
-where
-  "multiset_prime_factorization n =
-    (if n > 0
-     then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i)
-     else {#})"
-
-lemma multiset_prime_factorization: "n > 0 \<Longrightarrow>
-    (\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and>
-       n = (\<Prod>i \<in># (multiset_prime_factorization n). i)"
-  apply (unfold multiset_prime_factorization_def)
-  apply clarsimp
-  apply (frule multiset_prime_factorization_exists)
-  apply clarify
-  apply (rule theI)
-  apply (insert multiset_prime_factorization_unique)
-  apply auto
-  done
-
-
-subsection \<open>Prime factors and multiplicity for nat and int\<close>
-
-class unique_factorization =
-  fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
-    and prime_factors :: "'a \<Rightarrow> 'a set"
-
-text \<open>Definitions for the natural numbers.\<close>
-instantiation nat :: unique_factorization
-begin
-
-definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
-
-definition prime_factors_nat :: "nat \<Rightarrow> nat set"
-  where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
-
-instance ..
-
 end
-
-text \<open>Definitions for the integers.\<close>
-instantiation int :: unique_factorization
-begin
-
-definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
-  where "multiplicity_int p n = multiplicity (nat p) (nat n)"
-
-definition prime_factors_int :: "int \<Rightarrow> int set"
-  where "prime_factors_int n = int ` (prime_factors (nat n))"
-
-instance ..
-
-end
-
-
-subsection \<open>Set up transfer\<close>
-
-lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
-  unfolding prime_factors_int_def
-  apply auto
-  apply (subst transfer_int_nat_set_return_embed)
-  apply assumption
-  done
-
-lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)"
-  by (auto simp add: nat_set_def prime_factors_int_def)
-
-lemma transfer_nat_int_multiplicity:
-  "p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n"
-  by (auto simp add: multiplicity_int_def)
-
-declare transfer_morphism_nat_int[transfer add return:
-  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
-  transfer_nat_int_multiplicity]
-
-lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
-  unfolding prime_factors_int_def by auto
-
-lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)"
-  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
-
-lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n"
-  by (auto simp add: multiplicity_int_def)
-
-declare transfer_morphism_int_nat[transfer add return:
-  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
-  transfer_int_nat_multiplicity]
-
-
-subsection \<open>Properties of prime factors and multiplicity for nat and int\<close>
-
-lemma prime_factors_ge_0_int [elim]:
-  fixes n :: int
-  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
-  unfolding prime_factors_int_def by auto
-
-lemma prime_factors_prime_nat [intro]:
-  fixes n :: nat
-  shows "p \<in> prime_factors n \<Longrightarrow> prime p"
-  apply (cases "n = 0")
-  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
-  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
-  done
-
-lemma prime_factors_prime_int [intro]:
-  fixes n :: int
-  assumes "n \<ge> 0" and "p \<in> prime_factors n"
-  shows "prime p"
-  apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
-  using assms apply auto
-  done
-
-lemma prime_factors_gt_0_nat:
-  fixes p :: nat
-  shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
-    using prime_factors_prime_nat by force
-
-lemma prime_factors_gt_0_int:
-  shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
-    by (simp add: prime_factors_gt_0_nat)
-
-lemma prime_factors_finite_nat [iff]:
-  fixes n :: nat
-  shows "finite (prime_factors n)"
-  unfolding prime_factors_nat_def by auto
-
-lemma prime_factors_finite_int [iff]:
-  fixes n :: int
-  shows "finite (prime_factors n)"
-  unfolding prime_factors_int_def by auto
-
-lemma prime_factors_altdef_nat:
-  fixes n :: nat
-  shows "prime_factors n = {p. multiplicity p n > 0}"
-  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
-
-lemma prime_factors_altdef_int:
-  fixes n :: int
-  shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}"
-  apply (unfold prime_factors_int_def multiplicity_int_def)
-  apply (subst prime_factors_altdef_nat)
-  apply (auto simp add: image_def)
-  done
-
-lemma prime_factorization_nat:
-  fixes n :: nat
-  shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
-  apply (frule multiset_prime_factorization)
-  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
-  done
-
-lemma prime_factorization_int:
-  fixes n :: int
-  assumes "n > 0"
-  shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
-  apply (rule prime_factorization_nat [transferred, of n])
-  using assms apply auto
-  done
-
-lemma prime_factorization_unique_nat:
-  fixes f :: "nat \<Rightarrow> _"
-  assumes S_eq: "S = {p. 0 < f p}"
-    and "finite S"
-    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
-  shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
-proof -
-  from assms have "f \<in> multiset"
-    by (auto simp add: multiset_def)
-  moreover from assms have "n > 0" 
-    by (auto intro: prime_gt_0_nat)
-  ultimately have "multiset_prime_factorization n = Abs_multiset f"
-    apply (unfold multiset_prime_factorization_def)
-    apply (subst if_P, assumption)
-    apply (rule the1_equality)
-    apply (rule ex_ex1I)
-    apply (rule multiset_prime_factorization_exists, assumption)
-    apply (rule multiset_prime_factorization_unique)
-    apply force
-    apply force
-    apply force
-    using S S_eq  apply (simp add: set_mset_def msetprod_multiplicity)
-    done
-  with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
-    by simp
-  with S_eq show ?thesis
-    by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
-qed
-
-lemma prime_factors_characterization_nat:
-  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
-    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
-  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
-
-lemma prime_factors_characterization'_nat:
-  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
-    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
-      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
-  by (rule prime_factors_characterization_nat) auto
-
-(* A minor glitch:*)
-thm prime_factors_characterization'_nat
-    [where f = "\<lambda>x. f (int (x::nat))",
-      transferred direction: nat "op \<le> (0::int)", rule_format]
-
-(*
-  Transfer isn't smart enough to know that the "0 < f p" should
-  remain a comparison between nats. But the transfer still works.
-*)
-
-lemma primes_characterization'_int [rule_format]:
-  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
-      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
-  using prime_factors_characterization'_nat
-    [where f = "\<lambda>x. f (int (x::nat))",
-    transferred direction: nat "op \<le> (0::int)"]
-  by auto
-
-lemma prime_factors_characterization_int:
-  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
-    \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
-  apply simp
-  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
-  apply (simp only:)
-  apply (subst primes_characterization'_int)
-  apply simp_all
-  apply (metis nat_int)
-  apply (metis le_cases nat_le_0 zero_not_prime_nat)
-  done
-
-lemma multiplicity_characterization_nat:
-  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow>
-    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
-  apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
-  apply auto
-  done
-
-lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
-    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
-      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
-  apply (intro impI)
-  apply (rule multiplicity_characterization_nat)
-  apply auto
-  done
-
-lemma multiplicity_characterization'_int [rule_format]:
-  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
-    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
-      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
-  apply (insert multiplicity_characterization'_nat
-    [where f = "\<lambda>x. f (int (x::nat))",
-      transferred direction: nat "op \<le> (0::int)", rule_format])
-  apply auto
-  done
-
-lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
-    finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow>
-      p \<ge> 0 \<Longrightarrow> multiplicity p n = f p"
-  apply simp
-  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
-  apply (simp only:)
-  apply (subst multiplicity_characterization'_int)
-  apply simp_all
-  apply (metis nat_int)
-  apply (metis le_cases nat_le_0 zero_not_prime_nat)
-  done
-
-lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
-  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
-
-lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
-  by (simp add: multiplicity_int_def)
-
-lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0"
-  by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto)
-
-lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
-  by (metis One_nat_def multiplicity_one_nat')
-
-lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
-  by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
-
-lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
-  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"])
-  apply auto
-  apply (metis (full_types) less_not_refl)
-  done
-
-lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n"
-  apply (cases "n = 0")
-  apply auto
-  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"])
-  apply auto
-  apply (metis (full_types) less_not_refl)
-  done
-
-lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = n"
-  by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
-
-lemma multiplicity_nonprime_nat [simp]:
-  fixes p n :: nat
-  shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
-  apply (cases "n = 0")
-  apply auto
-  apply (frule multiset_prime_factorization)
-  apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
-  done
-
-lemma multiplicity_not_factor_nat [simp]:
-  fixes p n :: nat
-  shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
-  apply (subst (asm) prime_factors_altdef_nat)
-  apply auto
-  done
-
-lemma multiplicity_not_factor_int [simp]:
-  fixes n :: int
-  shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
-  apply (subst (asm) prime_factors_altdef_int)
-  apply auto
-  done
-
-(*FIXME: messy*)
-lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
-    (prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and>
-    (\<forall>p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
-  apply (rule prime_factorization_unique_nat)
-  apply (simp only: prime_factors_altdef_nat)
-  apply auto
-  apply (subst power_add)
-  apply (subst setprod.distrib)
-  apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"])
-  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union>
-      (prime_factors l - prime_factors k)")
-  apply (erule ssubst)
-  apply (subst setprod.union_disjoint)
-  apply auto
-  apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
-  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union>
-      (prime_factors k - prime_factors l)")
-  apply (erule ssubst)
-  apply (subst setprod.union_disjoint)
-  apply auto
-  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
-      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
-  apply auto
-  apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
-  done
-
-(* transfer doesn't have the same problem here with the right
-   choice of rules. *)
-
-lemma multiplicity_product_aux_int:
-  assumes "(k::int) > 0" and "l > 0"
-  shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and>
-    (\<forall>p \<ge> 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
-  apply (rule multiplicity_product_aux_nat [transferred, of l k])
-  using assms apply auto
-  done
-
-lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
-    prime_factors k \<union> prime_factors l"
-  by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
-
-lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
-    prime_factors k \<union> prime_factors l"
-  by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
-
-lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
-    multiplicity p k + multiplicity p l"
-  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric])
-
-lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
-    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
-  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric])
-
-lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
-    multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
-  apply (induct set: finite)
-  apply auto
-  apply (subst multiplicity_product_nat)
-  apply auto
-  done
-
-(* Transfer is delicate here for two reasons: first, because there is
-   an implicit quantifier over functions (f), and, second, because the
-   product over the multiplicity should not be translated to an integer
-   product.
-
-   The way to handle the first is to use quantifier rules for functions.
-   The way to handle the second is to turn off the offending rule.
-*)
-
-lemma transfer_nat_int_sum_prod_closure3: "(\<Sum>x \<in> A. int (f x)) \<ge> 0" "(\<Prod>x \<in> A. int (f x)) \<ge> 0"
-  apply (rule setsum_nonneg; auto)
-  apply (rule setprod_nonneg; auto)
-  done
-
-declare transfer_morphism_nat_int[transfer
-  add return: transfer_nat_int_sum_prod_closure3
-  del: transfer_nat_int_sum_prod2 (1)]
-
-lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
-    multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
-  apply (frule multiplicity_setprod_nat
-    [where f = "\<lambda>x. nat(int(nat(f x)))",
-      transferred direction: nat "op \<le> (0::int)"])
-  apply auto
-  apply (subst (asm) setprod.cong)
-  apply (rule refl)
-  apply (rule if_P)
-  apply auto
-  apply (rule setsum.cong)
-  apply auto
-  done
-
-declare transfer_morphism_nat_int[transfer
-  add return: transfer_nat_int_sum_prod2 (1)]
-
-lemma multiplicity_prod_prime_powers_nat:
-    "finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow>
-       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
-  apply (subgoal_tac "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ (\<lambda>x. if x \<in> S then f x else 0) p)")
-  apply (erule ssubst)
-  apply (subst multiplicity_characterization_nat)
-  prefer 5 apply (rule refl)
-  apply (rule refl)
-  apply auto
-  apply (subst setprod.mono_neutral_right)
-  apply assumption
-  prefer 3
-  apply (rule setprod.cong)
-  apply (rule refl)
-  apply auto
-  done
-
-(* Here the issue with transfer is the implicit quantifier over S *)
-
-lemma multiplicity_prod_prime_powers_int:
-    "(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow>
-       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
-  apply (subgoal_tac "int ` nat ` S = S")
-  apply (frule multiplicity_prod_prime_powers_nat
-    [where f = "\<lambda>x. f(int x)" and S = "nat ` S", transferred])
-  apply auto
-  apply (metis linear nat_0_iff zero_not_prime_nat)
-  apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
-  done
-
-lemma multiplicity_distinct_prime_power_nat:
-    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
-  apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}")
-  apply (erule ssubst)
-  apply (subst multiplicity_prod_prime_powers_nat)
-  apply auto
-  done
-
-lemma multiplicity_distinct_prime_power_int:
-    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
-  by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
-
-lemma dvd_multiplicity_nat:
-  fixes x y :: nat
-  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
-  apply (cases "x = 0")
-  apply (auto simp add: dvd_def multiplicity_product_nat)
-  done
-
-lemma dvd_multiplicity_int:
-  fixes p x y :: int
-  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
-  apply (cases "x = 0")
-  apply (auto simp add: dvd_def)
-  apply (subgoal_tac "0 < k")
-  apply (auto simp add: multiplicity_product_int)
-  apply (erule zero_less_mult_pos)
-  apply arith
-  done
-
-lemma dvd_prime_factors_nat [intro]:
-  fixes x y :: nat
-  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
-  apply (simp only: prime_factors_altdef_nat)
-  apply auto
-  apply (metis dvd_multiplicity_nat le_0_eq neq0_conv)
-  done
-
-lemma dvd_prime_factors_int [intro]:
-  fixes x y :: int
-  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
-  apply (auto simp add: prime_factors_altdef_int)
-  apply (metis dvd_multiplicity_int le_0_eq neq0_conv)
-  done
-
-lemma multiplicity_dvd_nat:
-  fixes x y :: nat
-  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (subst prime_factorization_nat [of x], assumption)
-  apply (subst prime_factorization_nat [of y], assumption)
-  apply (rule setprod_dvd_setprod_subset2)
-  apply force
-  apply (subst prime_factors_altdef_nat)+
-  apply auto
-  apply (metis gr0I le_0_eq less_not_refl)
-  apply (metis le_imp_power_dvd)
-  done
-
-lemma multiplicity_dvd_int:
-  fixes x y :: int
-  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (subst prime_factorization_int [of x], assumption)
-  apply (subst prime_factorization_int [of y], assumption)
-  apply (rule setprod_dvd_setprod_subset2)
-  apply force
-  apply (subst prime_factors_altdef_int)+
-  apply auto
-  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
-  done
-
-lemma multiplicity_dvd'_nat:
-  fixes x y :: nat
-  assumes "0 < x"
-  assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y"
-  shows "x dvd y"
-  using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0)
-
-lemma multiplicity_dvd'_int:
-  fixes x y :: int
-  shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
-    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int
-    zero_le_imp_eq_int zero_less_imp_eq_int)
-
-lemma dvd_multiplicity_eq_nat:
-  fixes x y :: nat
-  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
-  by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
-
-lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
-    (x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)"
-  by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
-
-lemma prime_factors_altdef2_nat:
-  fixes n :: nat
-  shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
-  apply (cases "prime p")
-  apply auto
-  apply (subst prime_factorization_nat [where n = n], assumption)
-  apply (rule dvd_trans)
-  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
-  apply (subst (asm) prime_factors_altdef_nat, force)
-  apply rule
-  apply auto
-  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0
-    le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
-  done
-
-lemma prime_factors_altdef2_int:
-  fixes n :: int
-  assumes "n > 0"
-  shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
-  using assms by (simp add:  prime_factors_altdef2_nat [transferred])
-
-lemma multiplicity_eq_nat:
-  fixes x and y::nat
-  assumes [arith]: "x > 0" "y > 0"
-    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
-  shows "x = y"
-  apply (rule dvd_antisym)
-  apply (auto intro: multiplicity_dvd'_nat)
-  done
-
-lemma multiplicity_eq_int:
-  fixes x y :: int
-  assumes [arith]: "x > 0" "y > 0"
-    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
-  shows "x = y"
-  apply (rule dvd_antisym [transferred])
-  apply (auto intro: multiplicity_dvd'_int)
-  done
-
-
-subsection \<open>An application\<close>
-
-lemma gcd_eq_nat:
-  fixes x y :: nat
-  assumes pos [arith]: "x > 0" "y > 0"
-  shows "gcd x y =
-    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
-  (is "_ = ?z")
-proof -
-  have [arith]: "?z > 0" 
-    using prime_factors_gt_0_nat by auto
-  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
-    apply (subst multiplicity_prod_prime_powers_nat)
-    apply auto
-    done
-  have "?z dvd x"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
-  moreover have "?z dvd y"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
-  moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
-  proof (cases "w = 0")
-    case True
-    then show ?thesis by simp
-  next
-    case False
-    then show ?thesis
-      apply auto
-      apply (erule multiplicity_dvd'_nat)
-      apply (auto intro: dvd_multiplicity_nat simp add: aux)
-      done
-  qed
-  ultimately have "?z = gcd x y"
-    by (subst gcd_unique_nat [symmetric], blast)
-  then show ?thesis
-    by auto
-qed
-
-lemma lcm_eq_nat:
-  assumes pos [arith]: "x > 0" "y > 0"
-  shows "lcm (x::nat) y =
-    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
-  (is "_ = ?z")
-proof -
-  have [arith]: "?z > 0"
-    by (auto intro: prime_gt_0_nat)
-  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
-    apply (subst multiplicity_prod_prime_powers_nat)
-    apply auto
-    done
-  have "x dvd ?z"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
-  moreover have "y dvd ?z"
-    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
-  moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w
-  proof (cases "w = 0")
-    case True
-    then show ?thesis by auto
-  next
-    case False
-    then show ?thesis
-      apply auto
-      apply (rule multiplicity_dvd'_nat)
-      apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux)
-      done
-  qed
-  ultimately have "?z = lcm x y"
-    by (subst lcm_unique_nat [symmetric], blast)
-  then show ?thesis
-    by auto
-qed
-
-lemma multiplicity_gcd_nat:
-  fixes p x y :: nat
-  assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
-  apply (subst gcd_eq_nat)
-  apply auto
-  apply (subst multiplicity_prod_prime_powers_nat)
-  apply auto
-  done
-
-lemma multiplicity_lcm_nat:
-  fixes p x y :: nat
-  assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
-  apply (subst lcm_eq_nat)
-  apply auto
-  apply (subst multiplicity_prod_prime_powers_nat)
-  apply auto
-  done
-
-lemma gcd_lcm_distrib_nat:
-  fixes x y z :: nat
-  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
-  apply (cases "x = 0 | y = 0 | z = 0")
-  apply auto
-  apply (rule multiplicity_eq_nat)
-  apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
-  done
-
-lemma gcd_lcm_distrib_int:
-  fixes x y z :: int
-  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
-  apply (subst (1 2 3) gcd_abs_int)
-  apply (subst lcm_abs_int)
-  apply (subst (2) abs_of_nonneg)
-  apply force
-  apply (rule gcd_lcm_distrib_nat [transferred])
-  apply auto
-  done
-
-end
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -27,8 +27,8 @@
 lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k"
   by (induct m) auto
 
-lemma prime_eq: "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
-  apply (simp add: prime_def)
+lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
+  apply (simp add: is_prime_nat_iff)
   apply (rule iffI)
   apply blast
   apply (erule conjE)
@@ -45,7 +45,7 @@
   apply simp
   done
 
-lemma prime_eq': "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
+lemma prime_eq': "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
 
 lemma not_prime_ex_mk:
@@ -207,7 +207,7 @@
 
 text \<open>Euclid's theorem: there are infinitely many primes.\<close>
 
-lemma Euclid: "\<exists>p. prime p \<and> n < p"
+lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
 proof -
   let ?k = "fact n + (1::nat)"
   have "1 < ?k" by simp
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/ex/Sqrt.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -14,7 +14,7 @@
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -59,7 +59,7 @@
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
diff -r f01d1e393f3f -r 523b488b15c9 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -17,7 +17,7 @@
 subsection \<open>Preliminaries\<close>
 
 lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
-  by (force simp add: prime_def)
+  by (force simp add: is_prime_nat_iff)
 
 lemma prime_dvd_other_side:
     "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
   apply (erule disjE)
    apply (frule mult_le_mono, assumption)
    apply auto
-  apply (force simp add: prime_def)
+  apply (force simp add: is_prime_nat_iff)
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"