author paulson Sun Feb 02 19:15:25 2014 +0000 (2014-02-02) changeset 55242 413ec965f95d 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 file | annotate | diff | revisions src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions src/HOL/Number_Theory/UniqueFactorization.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions
```     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
```