# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391368525 0
# Node ID 413ec965f95dd95aec954589afcfddd426f8de93
# Parent  ef601c60ccbea92851750b3c7a3283aa17b98d65
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.

diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -2831,9 +2831,7 @@
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_closed[simplified], fact+)
-  done
+    by (metis carr(1) carr(2) gcd_closed)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_l:
@@ -2842,9 +2840,7 @@
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_left[simplified], fact+)
-  done
+    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_r:
@@ -2853,9 +2849,7 @@
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_right[simplified], fact+)
-  done
+    by (metis carr gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides:
@@ -2865,9 +2859,7 @@
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet L)
-    apply (rule meet_le[simplified], fact+)
-  done
+    by (metis gcd_isgcd isgcd_def assms)
 qed
 
 lemma (in gcd_condition_monoid) gcd_cong_l:
@@ -3409,13 +3401,7 @@
 
     from aa2carr carr aa1fs aa2fs
       have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
-      apply (intro wfactors_mult_single)
-          apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
-         apply (fast intro: nth_mem[OF len])
-        apply fast
-       apply fast
-      apply assumption
-    done
+        by (metis irrasi wfactors_mult_single)
     with len carr aa1carr aa2carr aa1fs
       have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
       apply (intro wfactors_mult)
@@ -3429,23 +3415,15 @@
     with carr
       have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp
-
     with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
       have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
-      apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'"  "as'"])
-            apply fast+
-          apply (simp, fast)
-    done
+        by (metis as' ee_wfactorsD m_closed)
     then
     have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
-      apply (simp add: m_assoc[symmetric])
-      apply (simp add: m_comm)
-    done
+      by (metis aa1carr aa2carr asicarr m_lcomm)
     from carr asiah
     have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
-      apply (intro mult_cong_l)
-      apply (fast intro: associated_sym, simp+)
-    done
+      by (metis associated_sym m_closed mult_cong_l)
     also note t1
     finally
       have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
@@ -3530,7 +3508,6 @@
       where ascarr[simp]: "set as \<subseteq> carrier G"
       and afs: "wfactors G as a"
       by (auto simp del: carr)
-
   have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
     by (metis afs ascarr assms ee_length wfactors_unique)
   thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
@@ -3549,8 +3526,7 @@
     apply (simp add: factorcount_def)
     apply (rule theI2)
       apply (rule alen)
-     apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
-    apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
+     apply (metis afs alen ascarr)+
   done
 
   from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -239,14 +239,10 @@
 
 lemma multiples_principalideal:
   "principalideal {x * a | x. True } \<Z>"
-apply (subst int_Idl[symmetric], rule principalidealI)
- apply (rule int.genideal_ideal, simp)
-apply fast
-done
-
+by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
 
 lemma prime_primeideal:
-  assumes prime: "prime (nat p)"
+  assumes prime: "prime p"
   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
 apply (rule primeidealI)
    apply (rule int.genideal_ideal, simp)
@@ -257,48 +253,18 @@
  apply (elim exE)
 proof -
   fix a b x
-  have ppos: "0 <= p"
-    by (metis prime linear nat_0_iff zero_not_prime_nat)
-  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
-  proof -
-    fix x
-    assume "nat p dvd nat (abs x)"
-    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
-    thus "p dvd x" by (simp add: ppos)
-  qed
-  assume "a * b = x * p"
+  assume "a * b = x * int p"
   hence "p dvd a * b" by simp
-  hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
-  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
-  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)"
-    by (metis prime prime_dvd_mult_eq_nat) 
-  hence "p dvd a | p dvd b" by (fast intro: unnat)
-  thus "(EX x. a = x * p) | (EX x. b = x * p)"
-  proof
-    assume "p dvd a"
-    hence "EX x. a = p * x" by (simp add: dvd_def)
-    then obtain x
-        where "a = p * x" by fast
-    hence "a = x * p" by simp
-    hence "EX x. a = x * p" by simp
-    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
-  next
-    assume "p dvd b"
-    hence "EX x. b = p * x" by (simp add: dvd_def)
-    then obtain x
-        where "b = p * x" by fast
-    hence "b = x * p" by simp
-    hence "EX x. b = x * p" by simp
-    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
-  qed
+  hence "p dvd a | p dvd b"
+    by (metis prime prime_dvd_mult_eq_int)
+  thus "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
+    by (metis dvd_def mult_commute)
 next
-  assume "UNIV = {uu. EX x. uu = x * p}"
-  then obtain x where "1 = x * p" by best
-  then have "p * x = 1" by (metis mult_commute)
-  hence "\<bar>p * x\<bar> = 1" by simp
-  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
-  then  show "False" 
-    by (metis prime abs_of_pos one_not_prime_int prime_gt_0_int prime_int_def) 
+  assume "UNIV = {uu. EX x. uu = x * int p}"
+  then obtain x where "1 = x * int p" by best
+  hence "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
+  then show False
+    by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
 qed
 
 
@@ -454,7 +420,7 @@
 done
 
 lemma ZFact_prime_is_domain:
-  assumes pprime: "prime (nat p)"
+  assumes pprime: "prime p"
   shows "domain (ZFact p)"
 apply (unfold ZFact_def)
 apply (rule primeideal.quotient_is_domain)
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -261,7 +261,8 @@
   by (simp add: cong_altdef_int)
 
 lemma cong_square_int:
-   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
+  fixes a::int
+  shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk>
     \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   apply (simp only: cong_altdef_int)
   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -32,129 +32,76 @@
 begin
 
 declare One_nat_def [simp]
-
-class prime = one +
-  fixes prime :: "'a \<Rightarrow> bool"
-
-instantiation nat :: prime
-begin
-
-definition prime_nat :: "nat \<Rightarrow> bool"
-  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
-
-instance ..
-
-end
-
-instantiation int :: prime
-begin
-
-definition prime_int :: "int \<Rightarrow> bool"
-  where "prime_int p = prime (nat p)"
+declare [[coercion int]]
+declare [[coercion_enabled]]
 
-instance ..
-
-end
-
-
-subsection {* Set up Transfer *}
+definition prime :: "nat \<Rightarrow> bool"
+  where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
-lemma transfer_nat_int_prime:
-  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
-  unfolding gcd_int_def lcm_int_def prime_int_def by auto
-
-declare transfer_morphism_nat_int[transfer add return:
-    transfer_nat_int_prime]
-
-lemma transfer_int_nat_prime: "prime (int x) = prime x"
-  unfolding gcd_int_def lcm_int_def prime_int_def by auto
-
-declare transfer_morphism_int_nat[transfer add return:
-    transfer_int_nat_prime]
+lemmas prime_nat_def = prime_def
 
 
 subsection {* Primes *}
 
-lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
   apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
   done
 
-lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
-  unfolding prime_int_def
-  apply (frule prime_odd_nat)
-  apply (auto simp add: even_nat_def)
-  done
-
 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
 
-lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
-  unfolding prime_nat_def by auto
-
-lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
-  unfolding prime_nat_def by auto
-
-lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
+lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
   unfolding prime_nat_def by auto
 
-lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
+lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
   unfolding prime_nat_def by auto
 
-lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
-  unfolding prime_nat_def by auto
-
-lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
-  unfolding prime_nat_def by auto
-
-lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
+lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
   unfolding prime_nat_def by auto
 
-lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
-  unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
-  unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
-  unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
-  unfolding prime_int_def prime_nat_def by auto
+lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
+  unfolding prime_nat_def by auto
 
-lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
-  unfolding prime_int_def prime_nat_def by auto
-
+lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
+  unfolding prime_nat_def by auto
 
-lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
-    m = 1 \<or> m = p))"
-  using prime_nat_def [transferred]
-  apply (cases "p >= 0")
-  apply blast
-  apply (auto simp add: prime_ge_0_int)
-  done
+lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
+  unfolding prime_nat_def by auto
 
-lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   apply (unfold prime_nat_def)
   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   done
 
-lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+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 int_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_int gcd_dvd2_int gcd_ge_0_int)
   done
 
-lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+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_nat prime_imp_coprime_nat)
 
-lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+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_int prime_imp_coprime_int)
 
-lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
+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]: "prime (p::int) \<Longrightarrow>
-    p dvd m * n = (p dvd m \<or> p dvd n)"
+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)
 
 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
@@ -163,25 +110,20 @@
   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
 
-lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
-    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
-  unfolding prime_int_altdef dvd_def
-  apply auto
-  by (metis div_mult_self1_is_id div_mult_self2_is_id
-      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
-
-lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+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: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
-  by (induct n) (auto simp: prime_ge_0_int)
+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::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
+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: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
-    p dvd x^n \<longleftrightarrow> p dvd x"
+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)
 
 
@@ -190,80 +132,47 @@
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   by (simp add: prime_nat_def)
 
-lemma zero_not_prime_int [simp]: "~prime (0::int)"
-  by (simp add: prime_int_def)
-
 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   by (simp add: prime_nat_def)
 
 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   by (simp add: prime_nat_def)
 
-lemma one_not_prime_int [simp]: "~prime (1::int)"
-  by (simp add: prime_int_def)
-
 lemma prime_nat_code [code]:
-    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+    "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_nat_def dvd_triv_right not_prime_eq_prod_nat)
   done
 
 lemma prime_nat_simp:
-    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
+    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   by (auto simp add: prime_nat_code)
 
 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
 
-lemma prime_int_code [code]:
-  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
-proof
-  assume "?L"
-  then show "?R"
-    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
-next
-  assume "?R"
-  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
-qed
-
-lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
-  by (auto simp add: prime_int_code)
-
-lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
-
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   by simp
 
-lemma two_is_prime_int [simp]: "prime (2::int)"
-  by simp
-
 text{* A bit of regression testing: *}
 
 lemma "prime(97::nat)" by simp
-lemma "prime(97::int)" by simp
 lemma "prime(997::nat)" by eval
-lemma "prime(997::int)" by eval
 
 
-lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
 
-lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+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_int gcd_int.commute prime_imp_coprime_int)
 
-lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+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_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
-  by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
-
 lemma primes_imp_powers_coprime_nat:
-    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   by (rule coprime_exp2_nat, rule primes_coprime_nat)
 
-lemma primes_imp_powers_coprime_int:
-    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
-  by (rule coprime_exp2_int, rule primes_coprime_int)
-
 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   apply (induct n rule: nat_less_induct)
   apply (case_tac "n = 0")
@@ -276,7 +185,7 @@
 text {* One property of coprimality is easier to prove via prime factors. *}
 
 lemma prime_divprod_pow_nat:
-  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
+  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
@@ -316,7 +225,7 @@
 
 subsection {* Infinitely many primes *}
 
-lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
+lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
 proof-
   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   from prime_factor_nat [OF f1]
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -14,7 +14,6 @@
   MiscAlgebra
 begin
 
-
 (*
 
   A locale for residue rings
@@ -235,13 +234,14 @@
 (* prime residues *)
 
 locale residues_prime =
-  fixes p :: int and R (structure)
+  fixes p and R (structure)
   assumes p_prime [intro]: "prime p"
   defines "R == residue_ring p"
 
 sublocale residues_prime < residues p
   apply (unfold R_def residues_def)
   using p_prime apply auto
+  apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
   done
 
 context residues_prime
@@ -357,26 +357,26 @@
   done
 
 lemma fermat_theorem:
+  fixes a::int
   assumes "prime p" and "~ (p dvd a)"
-  shows "[a^(nat p - 1) = 1] (mod p)"
+  shows "[a^(p - 1) = 1] (mod p)"
 proof -
   from assms have "[a^phi p = 1] (mod p)"
     apply (intro euler_theorem)
-    (* auto should get this next part. matching across
-       substitutions is needed. *)
-    apply (frule prime_gt_1_int, arith)
-    apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
+    apply (metis of_nat_0_le_iff)
+    apply (metis gcd_int.commute prime_imp_coprime_int)
     done
   also have "phi p = nat p - 1"
     by (rule phi_prime, rule assms)
-  finally show ?thesis .
+  finally show ?thesis
+    by (metis nat_int) 
 qed
 
 lemma fermat_theorem_nat:
   assumes "prime p" and "~ (p dvd a)"
   shows "[a^(p - 1) = 1] (mod p)"
 using fermat_theorem [of p a] assms
-by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
+by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
 
 
 subsection {* Wilson's theorem *}
@@ -445,18 +445,20 @@
     apply auto
     done
   also have "\<dots> = fact (p - 1) mod p"
-    apply (subst fact_altdef_int)
-    apply (insert assms, force)
-    apply (subst res_prime_units_eq, rule refl)
+    apply (subst fact_altdef_nat)
+    apply (insert assms)
+    apply (subst res_prime_units_eq)
+    apply (simp add: int_setprod zmod_int setprod_int_eq)
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>".
-  then show ?thesis by (simp add: res_to_cong_simps)
+  then show ?thesis
+    by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
 qed
 
-lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
-  apply (frule prime_gt_1_int)
+lemma wilson_theorem: "prime p \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
+  apply (frule prime_gt_1_nat)
   apply (case_tac "p = 2")
-  apply (subst fact_altdef_int, simp)
+  apply (subst fact_altdef_nat, simp)
   apply (subst cong_int_def)
   apply simp
   apply (rule residues_prime.wilson_theorem1)
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -242,7 +242,7 @@
 lemma prime_factors_prime_int [intro]:
   assumes "n >= 0" and "p : prime_factors (n::int)"
   shows "prime p"
-  apply (rule prime_factors_prime_nat [transferred, of n p])
+  apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
   using assms apply auto
   done
 
@@ -252,8 +252,7 @@
   done
 
 lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
-    p > (0::int)"
-  apply (frule (1) prime_factors_prime_int)
+    int p > (0::int)"
   apply auto
   done
 
@@ -307,7 +306,7 @@
     apply force
     apply force
     using assms
-    apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity)
+    apply (simp add: set_of_def msetprod_multiplicity)
     done
   with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
     by (simp add: Abs_multiset_inverse)
@@ -354,14 +353,15 @@
   done
 
 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
       prime_factors n = S"
   apply simp
   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   apply (simp only:)
   apply (subst primes_characterization'_int)
   apply auto
-  apply (auto simp add: prime_ge_0_int)
+  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> 
@@ -390,14 +390,15 @@
   done
 
 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
       p >= 0 \<Longrightarrow> multiplicity p n = f p"
   apply simp
   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   apply (simp only:)
   apply (subst multiplicity_characterization'_int)
   apply auto
-  apply (auto simp add: prime_ge_0_int)
+  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"
@@ -415,25 +416,20 @@
 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::nat) \<Longrightarrow> multiplicity p p = 1"
+lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
   apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
   apply auto
   by (metis (full_types) less_not_refl)
 
-lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
-  unfolding prime_int_def multiplicity_int_def by auto
-
-lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
+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 = "(%q. if q = p then n else 0)"])
   apply auto
   by (metis (full_types) less_not_refl)
 
-lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
-  apply (frule prime_ge_0_int)
-  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
-  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]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
   apply (cases "n = 0")
@@ -442,9 +438,6 @@
   apply (auto simp add: set_of_def multiplicity_nat_def)
   done
 
-lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
-  unfolding multiplicity_int_def prime_int_def by auto
-
 lemma multiplicity_not_factor_nat [simp]: 
     "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
   apply (subst (asm) prime_factors_altdef_nat)
@@ -584,18 +577,17 @@
 (* Here the issue with transfer is the implicit quantifier over S *)
 
 lemma multiplicity_prod_prime_powers_int:
-    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
+    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow>
        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   apply (subgoal_tac "int ` nat ` S = S")
   apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
     and S = "nat ` S", transferred])
   apply auto
-  apply (metis prime_int_def)
-  apply (metis prime_ge_0_int)
-  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
+  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::nat) \<Longrightarrow> prime q \<Longrightarrow>
+lemma multiplicity_distinct_prime_power_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow>
     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   apply (erule ssubst)
@@ -603,14 +595,10 @@
   apply auto
   done
 
-lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
-    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
-  apply (frule prime_ge_0_int [of q])
-  apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
-  prefer 4
-  apply assumption
-  apply auto
-  done
+lemma multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow>
+    p ~= 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:
     "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
@@ -670,11 +658,12 @@
   by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
       multiplicity_nonprime_nat neq0_conv)
 
-lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+lemma multiplicity_dvd'_int: 
+  fixes x::int and y::int
+  shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
-      multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
-      less_le)
+by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int 
+          zero_le_imp_eq_int zero_less_imp_eq_int)
 
 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -700,11 +689,7 @@
 lemma prime_factors_altdef2_int: 
   assumes "(n::int) > 0" 
   shows "(p : prime_factors n) = (prime p & p dvd n)"
-  apply (cases "p >= 0")
-  apply (rule prime_factors_altdef2_nat [transferred])
-  using assms apply auto
-  apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
-  done
+using assms by (simp add:  prime_factors_altdef2_nat [transferred])
 
 lemma multiplicity_eq_nat:
   fixes x and y::nat 
diff -r ef601c60ccbe -r 413ec965f95d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Feb 02 19:15:25 2014 +0000
@@ -1635,4 +1635,18 @@
     transfer_int_nat_set_function_closures
 ]
 
+lemma setprod_int_plus_eq: "setprod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
+  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
+
+lemma setprod_int_eq: "setprod int {i..j} =  \<Prod>{int i..int j}"
+proof (cases "i \<le> j")
+  case True
+  then show ?thesis
+    by (metis Nat.le_iff_add setprod_int_plus_eq)
+next
+  case False
+  then show ?thesis
+    by auto
+qed
+
 end