Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
authorpaulson <lp15@cam.ac.uk>
Sun Feb 02 19:15:25 2014 +0000 (2014-02-02)
changeset 55242413ec965f95d
parent 55241 ef601c60ccbe
child 55243 66709d41601e
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sat Feb 01 22:02:20 2014 +0100
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Feb 02 19:15:25 2014 +0000
     1.3 @@ -2831,9 +2831,7 @@
     1.4  proof -
     1.5    interpret weak_lower_semilattice "division_rel G" by simp
     1.6    show ?thesis
     1.7 -    apply (simp add: somegcd_meet[OF carr])
     1.8 -    apply (rule meet_closed[simplified], fact+)
     1.9 -  done
    1.10 +    by (metis carr(1) carr(2) gcd_closed)
    1.11  qed
    1.12  
    1.13  lemma (in gcd_condition_monoid) gcd_divides_l:
    1.14 @@ -2842,9 +2840,7 @@
    1.15  proof -
    1.16    interpret weak_lower_semilattice "division_rel G" by simp
    1.17    show ?thesis
    1.18 -    apply (simp add: somegcd_meet[OF carr])
    1.19 -    apply (rule meet_left[simplified], fact+)
    1.20 -  done
    1.21 +    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
    1.22  qed
    1.23  
    1.24  lemma (in gcd_condition_monoid) gcd_divides_r:
    1.25 @@ -2853,9 +2849,7 @@
    1.26  proof -
    1.27    interpret weak_lower_semilattice "division_rel G" by simp
    1.28    show ?thesis
    1.29 -    apply (simp add: somegcd_meet[OF carr])
    1.30 -    apply (rule meet_right[simplified], fact+)
    1.31 -  done
    1.32 +    by (metis carr gcd_isgcd isgcd_def)
    1.33  qed
    1.34  
    1.35  lemma (in gcd_condition_monoid) gcd_divides:
    1.36 @@ -2865,9 +2859,7 @@
    1.37  proof -
    1.38    interpret weak_lower_semilattice "division_rel G" by simp
    1.39    show ?thesis
    1.40 -    apply (simp add: somegcd_meet L)
    1.41 -    apply (rule meet_le[simplified], fact+)
    1.42 -  done
    1.43 +    by (metis gcd_isgcd isgcd_def assms)
    1.44  qed
    1.45  
    1.46  lemma (in gcd_condition_monoid) gcd_cong_l:
    1.47 @@ -3409,13 +3401,7 @@
    1.48  
    1.49      from aa2carr carr aa1fs aa2fs
    1.50        have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
    1.51 -      apply (intro wfactors_mult_single)
    1.52 -          apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
    1.53 -         apply (fast intro: nth_mem[OF len])
    1.54 -        apply fast
    1.55 -       apply fast
    1.56 -      apply assumption
    1.57 -    done
    1.58 +        by (metis irrasi wfactors_mult_single)
    1.59      with len carr aa1carr aa2carr aa1fs
    1.60        have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
    1.61        apply (intro wfactors_mult)
    1.62 @@ -3429,23 +3415,15 @@
    1.63      with carr
    1.64        have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
    1.65        by simp
    1.66 -
    1.67      with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
    1.68        have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
    1.69 -      apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'"  "as'"])
    1.70 -            apply fast+
    1.71 -          apply (simp, fast)
    1.72 -    done
    1.73 +        by (metis as' ee_wfactorsD m_closed)
    1.74      then
    1.75      have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
    1.76 -      apply (simp add: m_assoc[symmetric])
    1.77 -      apply (simp add: m_comm)
    1.78 -    done
    1.79 +      by (metis aa1carr aa2carr asicarr m_lcomm)
    1.80      from carr asiah
    1.81      have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
    1.82 -      apply (intro mult_cong_l)
    1.83 -      apply (fast intro: associated_sym, simp+)
    1.84 -    done
    1.85 +      by (metis associated_sym m_closed mult_cong_l)
    1.86      also note t1
    1.87      finally
    1.88        have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
    1.89 @@ -3530,7 +3508,6 @@
    1.90        where ascarr[simp]: "set as \<subseteq> carrier G"
    1.91        and afs: "wfactors G as a"
    1.92        by (auto simp del: carr)
    1.93 -
    1.94    have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
    1.95      by (metis afs ascarr assms ee_length wfactors_unique)
    1.96    thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
    1.97 @@ -3549,8 +3526,7 @@
    1.98      apply (simp add: factorcount_def)
    1.99      apply (rule theI2)
   1.100        apply (rule alen)
   1.101 -     apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
   1.102 -    apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
   1.103 +     apply (metis afs alen ascarr)+
   1.104    done
   1.105  
   1.106    from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Feb 01 22:02:20 2014 +0100
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Sun Feb 02 19:15:25 2014 +0000
     2.3 @@ -239,14 +239,10 @@
     2.4  
     2.5  lemma multiples_principalideal:
     2.6    "principalideal {x * a | x. True } \<Z>"
     2.7 -apply (subst int_Idl[symmetric], rule principalidealI)
     2.8 - apply (rule int.genideal_ideal, simp)
     2.9 -apply fast
    2.10 -done
    2.11 -
    2.12 +by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
    2.13  
    2.14  lemma prime_primeideal:
    2.15 -  assumes prime: "prime (nat p)"
    2.16 +  assumes prime: "prime p"
    2.17    shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
    2.18  apply (rule primeidealI)
    2.19     apply (rule int.genideal_ideal, simp)
    2.20 @@ -257,48 +253,18 @@
    2.21   apply (elim exE)
    2.22  proof -
    2.23    fix a b x
    2.24 -  have ppos: "0 <= p"
    2.25 -    by (metis prime linear nat_0_iff zero_not_prime_nat)
    2.26 -  have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
    2.27 -  proof -
    2.28 -    fix x
    2.29 -    assume "nat p dvd nat (abs x)"
    2.30 -    hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
    2.31 -    thus "p dvd x" by (simp add: ppos)
    2.32 -  qed
    2.33 -  assume "a * b = x * p"
    2.34 +  assume "a * b = x * int p"
    2.35    hence "p dvd a * b" by simp
    2.36 -  hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
    2.37 -  hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
    2.38 -  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)"
    2.39 -    by (metis prime prime_dvd_mult_eq_nat) 
    2.40 -  hence "p dvd a | p dvd b" by (fast intro: unnat)
    2.41 -  thus "(EX x. a = x * p) | (EX x. b = x * p)"
    2.42 -  proof
    2.43 -    assume "p dvd a"
    2.44 -    hence "EX x. a = p * x" by (simp add: dvd_def)
    2.45 -    then obtain x
    2.46 -        where "a = p * x" by fast
    2.47 -    hence "a = x * p" by simp
    2.48 -    hence "EX x. a = x * p" by simp
    2.49 -    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
    2.50 -  next
    2.51 -    assume "p dvd b"
    2.52 -    hence "EX x. b = p * x" by (simp add: dvd_def)
    2.53 -    then obtain x
    2.54 -        where "b = p * x" by fast
    2.55 -    hence "b = x * p" by simp
    2.56 -    hence "EX x. b = x * p" by simp
    2.57 -    thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
    2.58 -  qed
    2.59 +  hence "p dvd a | p dvd b"
    2.60 +    by (metis prime prime_dvd_mult_eq_int)
    2.61 +  thus "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
    2.62 +    by (metis dvd_def mult_commute)
    2.63  next
    2.64 -  assume "UNIV = {uu. EX x. uu = x * p}"
    2.65 -  then obtain x where "1 = x * p" by best
    2.66 -  then have "p * x = 1" by (metis mult_commute)
    2.67 -  hence "\<bar>p * x\<bar> = 1" by simp
    2.68 -  hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
    2.69 -  then  show "False" 
    2.70 -    by (metis prime abs_of_pos one_not_prime_int prime_gt_0_int prime_int_def) 
    2.71 +  assume "UNIV = {uu. EX x. uu = x * int p}"
    2.72 +  then obtain x where "1 = x * int p" by best
    2.73 +  hence "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
    2.74 +  then show False
    2.75 +    by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
    2.76  qed
    2.77  
    2.78  
    2.79 @@ -454,7 +420,7 @@
    2.80  done
    2.81  
    2.82  lemma ZFact_prime_is_domain:
    2.83 -  assumes pprime: "prime (nat p)"
    2.84 +  assumes pprime: "prime p"
    2.85    shows "domain (ZFact p)"
    2.86  apply (unfold ZFact_def)
    2.87  apply (rule primeideal.quotient_is_domain)
     3.1 --- a/src/HOL/Number_Theory/Cong.thy	Sat Feb 01 22:02:20 2014 +0100
     3.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sun Feb 02 19:15:25 2014 +0000
     3.3 @@ -261,7 +261,8 @@
     3.4    by (simp add: cong_altdef_int)
     3.5  
     3.6  lemma cong_square_int:
     3.7 -   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
     3.8 +  fixes a::int
     3.9 +  shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk>
    3.10      \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
    3.11    apply (simp only: cong_altdef_int)
    3.12    apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
     4.1 --- a/src/HOL/Number_Theory/Primes.thy	Sat Feb 01 22:02:20 2014 +0100
     4.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sun Feb 02 19:15:25 2014 +0000
     4.3 @@ -32,129 +32,76 @@
     4.4  begin
     4.5  
     4.6  declare One_nat_def [simp]
     4.7 -
     4.8 -class prime = one +
     4.9 -  fixes prime :: "'a \<Rightarrow> bool"
    4.10 -
    4.11 -instantiation nat :: prime
    4.12 -begin
    4.13 -
    4.14 -definition prime_nat :: "nat \<Rightarrow> bool"
    4.15 -  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    4.16 -
    4.17 -instance ..
    4.18 -
    4.19 -end
    4.20 -
    4.21 -instantiation int :: prime
    4.22 -begin
    4.23 -
    4.24 -definition prime_int :: "int \<Rightarrow> bool"
    4.25 -  where "prime_int p = prime (nat p)"
    4.26 +declare [[coercion int]]
    4.27 +declare [[coercion_enabled]]
    4.28  
    4.29 -instance ..
    4.30 -
    4.31 -end
    4.32 -
    4.33 -
    4.34 -subsection {* Set up Transfer *}
    4.35 +definition prime :: "nat \<Rightarrow> bool"
    4.36 +  where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    4.37  
    4.38 -lemma transfer_nat_int_prime:
    4.39 -  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
    4.40 -  unfolding gcd_int_def lcm_int_def prime_int_def by auto
    4.41 -
    4.42 -declare transfer_morphism_nat_int[transfer add return:
    4.43 -    transfer_nat_int_prime]
    4.44 -
    4.45 -lemma transfer_int_nat_prime: "prime (int x) = prime x"
    4.46 -  unfolding gcd_int_def lcm_int_def prime_int_def by auto
    4.47 -
    4.48 -declare transfer_morphism_int_nat[transfer add return:
    4.49 -    transfer_int_nat_prime]
    4.50 +lemmas prime_nat_def = prime_def
    4.51  
    4.52  
    4.53  subsection {* Primes *}
    4.54  
    4.55 -lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    4.56 +lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    4.57    apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    4.58    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)
    4.59    done
    4.60  
    4.61 -lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    4.62 -  unfolding prime_int_def
    4.63 -  apply (frule prime_odd_nat)
    4.64 -  apply (auto simp add: even_nat_def)
    4.65 -  done
    4.66 -
    4.67  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    4.68  
    4.69 -lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    4.70 -  unfolding prime_nat_def by auto
    4.71 -
    4.72 -lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
    4.73 -  unfolding prime_nat_def by auto
    4.74 -
    4.75 -lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
    4.76 +lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
    4.77    unfolding prime_nat_def by auto
    4.78  
    4.79 -lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
    4.80 +lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
    4.81    unfolding prime_nat_def by auto
    4.82  
    4.83 -lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
    4.84 -  unfolding prime_nat_def by auto
    4.85 -
    4.86 -lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
    4.87 -  unfolding prime_nat_def by auto
    4.88 -
    4.89 -lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
    4.90 +lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
    4.91    unfolding prime_nat_def by auto
    4.92  
    4.93 -lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
    4.94 -  unfolding prime_int_def prime_nat_def by auto
    4.95 -
    4.96 -lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
    4.97 -  unfolding prime_int_def prime_nat_def by auto
    4.98 -
    4.99 -lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   4.100 -  unfolding prime_int_def prime_nat_def by auto
   4.101 -
   4.102 -lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   4.103 -  unfolding prime_int_def prime_nat_def by auto
   4.104 +lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
   4.105 +  unfolding prime_nat_def by auto
   4.106  
   4.107 -lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   4.108 -  unfolding prime_int_def prime_nat_def by auto
   4.109 -
   4.110 +lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
   4.111 +  unfolding prime_nat_def by auto
   4.112  
   4.113 -lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   4.114 -    m = 1 \<or> m = p))"
   4.115 -  using prime_nat_def [transferred]
   4.116 -  apply (cases "p >= 0")
   4.117 -  apply blast
   4.118 -  apply (auto simp add: prime_ge_0_int)
   4.119 -  done
   4.120 +lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
   4.121 +  unfolding prime_nat_def by auto
   4.122  
   4.123 -lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   4.124 +lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   4.125    apply (unfold prime_nat_def)
   4.126    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   4.127    done
   4.128  
   4.129 -lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   4.130 +lemma prime_int_altdef: 
   4.131 +  "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
   4.132 +    m = 1 \<or> m = p))"
   4.133 +  apply (simp add: prime_def)
   4.134 +  apply (auto simp add: )
   4.135 +  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
   4.136 +  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
   4.137 +  done
   4.138 +
   4.139 +lemma prime_imp_coprime_int:
   4.140 +  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   4.141    apply (unfold prime_int_altdef)
   4.142    apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   4.143    done
   4.144  
   4.145 -lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   4.146 +lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   4.147    by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   4.148  
   4.149 -lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   4.150 +lemma prime_dvd_mult_int: 
   4.151 +  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   4.152    by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   4.153  
   4.154 -lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   4.155 +lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
   4.156      p dvd m * n = (p dvd m \<or> p dvd n)"
   4.157    by (rule iffI, rule prime_dvd_mult_nat, auto)
   4.158  
   4.159 -lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   4.160 -    p dvd m * n = (p dvd m \<or> p dvd n)"
   4.161 +lemma prime_dvd_mult_eq_int [simp]:
   4.162 +  fixes n::int 
   4.163 +  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
   4.164    by (rule iffI, rule prime_dvd_mult_int, auto)
   4.165  
   4.166  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   4.167 @@ -163,25 +110,20 @@
   4.168    by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   4.169        n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   4.170  
   4.171 -lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   4.172 -    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   4.173 -  unfolding prime_int_altdef dvd_def
   4.174 -  apply auto
   4.175 -  by (metis div_mult_self1_is_id div_mult_self2_is_id
   4.176 -      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
   4.177 -
   4.178 -lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   4.179 +lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   4.180    by (induct n) auto
   4.181  
   4.182 -lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   4.183 -  by (induct n) (auto simp: prime_ge_0_int)
   4.184 +lemma prime_dvd_power_int:
   4.185 +  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   4.186 +  by (induct n) auto
   4.187  
   4.188 -lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
   4.189 +lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
   4.190      p dvd x^n \<longleftrightarrow> p dvd x"
   4.191    by (cases n) (auto elim: prime_dvd_power_nat)
   4.192  
   4.193 -lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
   4.194 -    p dvd x^n \<longleftrightarrow> p dvd x"
   4.195 +lemma prime_dvd_power_int_iff:
   4.196 +  fixes x::int 
   4.197 +  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
   4.198    by (cases n) (auto elim: prime_dvd_power_int)
   4.199  
   4.200  
   4.201 @@ -190,80 +132,47 @@
   4.202  lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   4.203    by (simp add: prime_nat_def)
   4.204  
   4.205 -lemma zero_not_prime_int [simp]: "~prime (0::int)"
   4.206 -  by (simp add: prime_int_def)
   4.207 -
   4.208  lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   4.209    by (simp add: prime_nat_def)
   4.210  
   4.211  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   4.212    by (simp add: prime_nat_def)
   4.213  
   4.214 -lemma one_not_prime_int [simp]: "~prime (1::int)"
   4.215 -  by (simp add: prime_int_def)
   4.216 -
   4.217  lemma prime_nat_code [code]:
   4.218 -    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   4.219 +    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   4.220    apply (simp add: Ball_def)
   4.221    apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   4.222    done
   4.223  
   4.224  lemma prime_nat_simp:
   4.225 -    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   4.226 +    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   4.227    by (auto simp add: prime_nat_code)
   4.228  
   4.229  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   4.230  
   4.231 -lemma prime_int_code [code]:
   4.232 -  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   4.233 -proof
   4.234 -  assume "?L"
   4.235 -  then show "?R"
   4.236 -    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   4.237 -next
   4.238 -  assume "?R"
   4.239 -  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
   4.240 -qed
   4.241 -
   4.242 -lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   4.243 -  by (auto simp add: prime_int_code)
   4.244 -
   4.245 -lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
   4.246 -
   4.247  lemma two_is_prime_nat [simp]: "prime (2::nat)"
   4.248    by simp
   4.249  
   4.250 -lemma two_is_prime_int [simp]: "prime (2::int)"
   4.251 -  by simp
   4.252 -
   4.253  text{* A bit of regression testing: *}
   4.254  
   4.255  lemma "prime(97::nat)" by simp
   4.256 -lemma "prime(97::int)" by simp
   4.257  lemma "prime(997::nat)" by eval
   4.258 -lemma "prime(997::int)" by eval
   4.259  
   4.260  
   4.261 -lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   4.262 +lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   4.263    by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   4.264  
   4.265 -lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   4.266 +lemma prime_imp_power_coprime_int:
   4.267 +  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   4.268    by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
   4.269  
   4.270 -lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   4.271 +lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   4.272    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   4.273  
   4.274 -lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   4.275 -  by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
   4.276 -
   4.277  lemma primes_imp_powers_coprime_nat:
   4.278 -    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   4.279 +    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   4.280    by (rule coprime_exp2_nat, rule primes_coprime_nat)
   4.281  
   4.282 -lemma primes_imp_powers_coprime_int:
   4.283 -    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   4.284 -  by (rule coprime_exp2_int, rule primes_coprime_int)
   4.285 -
   4.286  lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   4.287    apply (induct n rule: nat_less_induct)
   4.288    apply (case_tac "n = 0")
   4.289 @@ -276,7 +185,7 @@
   4.290  text {* One property of coprimality is easier to prove via prime factors. *}
   4.291  
   4.292  lemma prime_divprod_pow_nat:
   4.293 -  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   4.294 +  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   4.295    shows "p^n dvd a \<or> p^n dvd b"
   4.296  proof-
   4.297    { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   4.298 @@ -316,7 +225,7 @@
   4.299  
   4.300  subsection {* Infinitely many primes *}
   4.301  
   4.302 -lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   4.303 +lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
   4.304  proof-
   4.305    have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   4.306    from prime_factor_nat [OF f1]
     5.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 01 22:02:20 2014 +0100
     5.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 19:15:25 2014 +0000
     5.3 @@ -14,7 +14,6 @@
     5.4    MiscAlgebra
     5.5  begin
     5.6  
     5.7 -
     5.8  (*
     5.9  
    5.10    A locale for residue rings
    5.11 @@ -235,13 +234,14 @@
    5.12  (* prime residues *)
    5.13  
    5.14  locale residues_prime =
    5.15 -  fixes p :: int and R (structure)
    5.16 +  fixes p and R (structure)
    5.17    assumes p_prime [intro]: "prime p"
    5.18    defines "R == residue_ring p"
    5.19  
    5.20  sublocale residues_prime < residues p
    5.21    apply (unfold R_def residues_def)
    5.22    using p_prime apply auto
    5.23 +  apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
    5.24    done
    5.25  
    5.26  context residues_prime
    5.27 @@ -357,26 +357,26 @@
    5.28    done
    5.29  
    5.30  lemma fermat_theorem:
    5.31 +  fixes a::int
    5.32    assumes "prime p" and "~ (p dvd a)"
    5.33 -  shows "[a^(nat p - 1) = 1] (mod p)"
    5.34 +  shows "[a^(p - 1) = 1] (mod p)"
    5.35  proof -
    5.36    from assms have "[a^phi p = 1] (mod p)"
    5.37      apply (intro euler_theorem)
    5.38 -    (* auto should get this next part. matching across
    5.39 -       substitutions is needed. *)
    5.40 -    apply (frule prime_gt_1_int, arith)
    5.41 -    apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
    5.42 +    apply (metis of_nat_0_le_iff)
    5.43 +    apply (metis gcd_int.commute prime_imp_coprime_int)
    5.44      done
    5.45    also have "phi p = nat p - 1"
    5.46      by (rule phi_prime, rule assms)
    5.47 -  finally show ?thesis .
    5.48 +  finally show ?thesis
    5.49 +    by (metis nat_int) 
    5.50  qed
    5.51  
    5.52  lemma fermat_theorem_nat:
    5.53    assumes "prime p" and "~ (p dvd a)"
    5.54    shows "[a^(p - 1) = 1] (mod p)"
    5.55  using fermat_theorem [of p a] assms
    5.56 -by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
    5.57 +by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
    5.58  
    5.59  
    5.60  subsection {* Wilson's theorem *}
    5.61 @@ -445,18 +445,20 @@
    5.62      apply auto
    5.63      done
    5.64    also have "\<dots> = fact (p - 1) mod p"
    5.65 -    apply (subst fact_altdef_int)
    5.66 -    apply (insert assms, force)
    5.67 -    apply (subst res_prime_units_eq, rule refl)
    5.68 +    apply (subst fact_altdef_nat)
    5.69 +    apply (insert assms)
    5.70 +    apply (subst res_prime_units_eq)
    5.71 +    apply (simp add: int_setprod zmod_int setprod_int_eq)
    5.72      done
    5.73    finally have "fact (p - 1) mod p = \<ominus> \<one>".
    5.74 -  then show ?thesis by (simp add: res_to_cong_simps)
    5.75 +  then show ?thesis
    5.76 +    by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
    5.77  qed
    5.78  
    5.79 -lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
    5.80 -  apply (frule prime_gt_1_int)
    5.81 +lemma wilson_theorem: "prime p \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
    5.82 +  apply (frule prime_gt_1_nat)
    5.83    apply (case_tac "p = 2")
    5.84 -  apply (subst fact_altdef_int, simp)
    5.85 +  apply (subst fact_altdef_nat, simp)
    5.86    apply (subst cong_int_def)
    5.87    apply simp
    5.88    apply (rule residues_prime.wilson_theorem1)
     6.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sat Feb 01 22:02:20 2014 +0100
     6.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Feb 02 19:15:25 2014 +0000
     6.3 @@ -242,7 +242,7 @@
     6.4  lemma prime_factors_prime_int [intro]:
     6.5    assumes "n >= 0" and "p : prime_factors (n::int)"
     6.6    shows "prime p"
     6.7 -  apply (rule prime_factors_prime_nat [transferred, of n p])
     6.8 +  apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
     6.9    using assms apply auto
    6.10    done
    6.11  
    6.12 @@ -252,8 +252,7 @@
    6.13    done
    6.14  
    6.15  lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
    6.16 -    p > (0::int)"
    6.17 -  apply (frule (1) prime_factors_prime_int)
    6.18 +    int p > (0::int)"
    6.19    apply auto
    6.20    done
    6.21  
    6.22 @@ -307,7 +306,7 @@
    6.23      apply force
    6.24      apply force
    6.25      using assms
    6.26 -    apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity)
    6.27 +    apply (simp add: set_of_def msetprod_multiplicity)
    6.28      done
    6.29    with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
    6.30      by (simp add: Abs_multiset_inverse)
    6.31 @@ -354,14 +353,15 @@
    6.32    done
    6.33  
    6.34  lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
    6.35 -    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    6.36 +    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    6.37        prime_factors n = S"
    6.38    apply simp
    6.39    apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
    6.40    apply (simp only:)
    6.41    apply (subst primes_characterization'_int)
    6.42    apply auto
    6.43 -  apply (auto simp add: prime_ge_0_int)
    6.44 +  apply (metis nat_int)
    6.45 +  apply (metis le_cases nat_le_0 zero_not_prime_nat)
    6.46    done
    6.47  
    6.48  lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
    6.49 @@ -390,14 +390,15 @@
    6.50    done
    6.51  
    6.52  lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
    6.53 -    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    6.54 +    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    6.55        p >= 0 \<Longrightarrow> multiplicity p n = f p"
    6.56    apply simp
    6.57    apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
    6.58    apply (simp only:)
    6.59    apply (subst multiplicity_characterization'_int)
    6.60    apply auto
    6.61 -  apply (auto simp add: prime_ge_0_int)
    6.62 +  apply (metis nat_int)
    6.63 +  apply (metis le_cases nat_le_0 zero_not_prime_nat)
    6.64    done
    6.65  
    6.66  lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
    6.67 @@ -415,25 +416,20 @@
    6.68  lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
    6.69    by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
    6.70  
    6.71 -lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
    6.72 +lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
    6.73    apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
    6.74    apply auto
    6.75    by (metis (full_types) less_not_refl)
    6.76  
    6.77 -lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
    6.78 -  unfolding prime_int_def multiplicity_int_def by auto
    6.79 -
    6.80 -lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
    6.81 +lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p^n) = n"
    6.82    apply (cases "n = 0")
    6.83    apply auto
    6.84    apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
    6.85    apply auto
    6.86    by (metis (full_types) less_not_refl)
    6.87  
    6.88 -lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
    6.89 -  apply (frule prime_ge_0_int)
    6.90 -  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
    6.91 -  done
    6.92 +lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p ( (int p)^n) = n"
    6.93 +  by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
    6.94  
    6.95  lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
    6.96    apply (cases "n = 0")
    6.97 @@ -442,9 +438,6 @@
    6.98    apply (auto simp add: set_of_def multiplicity_nat_def)
    6.99    done
   6.100  
   6.101 -lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
   6.102 -  unfolding multiplicity_int_def prime_int_def by auto
   6.103 -
   6.104  lemma multiplicity_not_factor_nat [simp]: 
   6.105      "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
   6.106    apply (subst (asm) prime_factors_altdef_nat)
   6.107 @@ -584,18 +577,17 @@
   6.108  (* Here the issue with transfer is the implicit quantifier over S *)
   6.109  
   6.110  lemma multiplicity_prod_prime_powers_int:
   6.111 -    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   6.112 +    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow>
   6.113         multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   6.114    apply (subgoal_tac "int ` nat ` S = S")
   6.115    apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
   6.116      and S = "nat ` S", transferred])
   6.117    apply auto
   6.118 -  apply (metis prime_int_def)
   6.119 -  apply (metis prime_ge_0_int)
   6.120 -  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
   6.121 +  apply (metis linear nat_0_iff zero_not_prime_nat)
   6.122 +  apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
   6.123    done
   6.124  
   6.125 -lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
   6.126 +lemma multiplicity_distinct_prime_power_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow>
   6.127      p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   6.128    apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   6.129    apply (erule ssubst)
   6.130 @@ -603,14 +595,10 @@
   6.131    apply auto
   6.132    done
   6.133  
   6.134 -lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
   6.135 -    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   6.136 -  apply (frule prime_ge_0_int [of q])
   6.137 -  apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
   6.138 -  prefer 4
   6.139 -  apply assumption
   6.140 -  apply auto
   6.141 -  done
   6.142 +lemma multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow>
   6.143 +    p ~= q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
   6.144 +  by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
   6.145 +
   6.146  
   6.147  lemma dvd_multiplicity_nat:
   6.148      "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
   6.149 @@ -670,11 +658,12 @@
   6.150    by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
   6.151        multiplicity_nonprime_nat neq0_conv)
   6.152  
   6.153 -lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   6.154 +lemma multiplicity_dvd'_int: 
   6.155 +  fixes x::int and y::int
   6.156 +  shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   6.157      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   6.158 -  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
   6.159 -      multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
   6.160 -      less_le)
   6.161 +by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int 
   6.162 +          zero_le_imp_eq_int zero_less_imp_eq_int)
   6.163  
   6.164  lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   6.165      (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
   6.166 @@ -700,11 +689,7 @@
   6.167  lemma prime_factors_altdef2_int: 
   6.168    assumes "(n::int) > 0" 
   6.169    shows "(p : prime_factors n) = (prime p & p dvd n)"
   6.170 -  apply (cases "p >= 0")
   6.171 -  apply (rule prime_factors_altdef2_nat [transferred])
   6.172 -  using assms apply auto
   6.173 -  apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
   6.174 -  done
   6.175 +using assms by (simp add:  prime_factors_altdef2_nat [transferred])
   6.176  
   6.177  lemma multiplicity_eq_nat:
   6.178    fixes x and y::nat 
     7.1 --- a/src/HOL/Set_Interval.thy	Sat Feb 01 22:02:20 2014 +0100
     7.2 +++ b/src/HOL/Set_Interval.thy	Sun Feb 02 19:15:25 2014 +0000
     7.3 @@ -1635,4 +1635,18 @@
     7.4      transfer_int_nat_set_function_closures
     7.5  ]
     7.6  
     7.7 +lemma setprod_int_plus_eq: "setprod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
     7.8 +  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
     7.9 +
    7.10 +lemma setprod_int_eq: "setprod int {i..j} =  \<Prod>{int i..int j}"
    7.11 +proof (cases "i \<le> j")
    7.12 +  case True
    7.13 +  then show ?thesis
    7.14 +    by (metis Nat.le_iff_add setprod_int_plus_eq)
    7.15 +next
    7.16 +  case False
    7.17 +  then show ?thesis
    7.18 +    by auto
    7.19 +qed
    7.20 +
    7.21  end