src/HOL/Number_Theory/Primes.thy
 changeset 55242 413ec965f95d parent 55238 7ddb889e23bd child 55337 5d45fb978d5a
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Sat Feb 01 22:02:20 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sun Feb 02 19:15:25 2014 +0000
1.3 @@ -32,129 +32,76 @@
1.4  begin
1.5
1.6  declare One_nat_def [simp]
1.7 -
1.8 -class prime = one +
1.9 -  fixes prime :: "'a \<Rightarrow> bool"
1.10 -
1.11 -instantiation nat :: prime
1.12 -begin
1.13 -
1.14 -definition prime_nat :: "nat \<Rightarrow> bool"
1.15 -  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
1.16 -
1.17 -instance ..
1.18 -
1.19 -end
1.20 -
1.21 -instantiation int :: prime
1.22 -begin
1.23 -
1.24 -definition prime_int :: "int \<Rightarrow> bool"
1.25 -  where "prime_int p = prime (nat p)"
1.26 +declare [[coercion int]]
1.27 +declare [[coercion_enabled]]
1.28
1.29 -instance ..
1.30 -
1.31 -end
1.32 -
1.33 -
1.34 -subsection {* Set up Transfer *}
1.35 +definition prime :: "nat \<Rightarrow> bool"
1.36 +  where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
1.37
1.38 -lemma transfer_nat_int_prime:
1.39 -  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
1.40 -  unfolding gcd_int_def lcm_int_def prime_int_def by auto
1.41 -
1.43 -    transfer_nat_int_prime]
1.44 -
1.45 -lemma transfer_int_nat_prime: "prime (int x) = prime x"
1.46 -  unfolding gcd_int_def lcm_int_def prime_int_def by auto
1.47 -
1.49 -    transfer_int_nat_prime]
1.50 +lemmas prime_nat_def = prime_def
1.51
1.52
1.53  subsection {* Primes *}
1.54
1.55 -lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1.56 +lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1.57    apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
1.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)
1.59    done
1.60
1.61 -lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1.62 -  unfolding prime_int_def
1.63 -  apply (frule prime_odd_nat)
1.64 -  apply (auto simp add: even_nat_def)
1.65 -  done
1.66 -
1.67  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
1.68
1.69 -lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
1.70 -  unfolding prime_nat_def by auto
1.71 -
1.72 -lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
1.73 -  unfolding prime_nat_def by auto
1.74 -
1.75 -lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
1.76 +lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
1.77    unfolding prime_nat_def by auto
1.78
1.79 -lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
1.80 +lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
1.81    unfolding prime_nat_def by auto
1.82
1.83 -lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
1.84 -  unfolding prime_nat_def by auto
1.85 -
1.86 -lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
1.87 -  unfolding prime_nat_def by auto
1.88 -
1.89 -lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
1.90 +lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
1.91    unfolding prime_nat_def by auto
1.92
1.93 -lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
1.94 -  unfolding prime_int_def prime_nat_def by auto
1.95 -
1.96 -lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
1.97 -  unfolding prime_int_def prime_nat_def by auto
1.98 -
1.99 -lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
1.100 -  unfolding prime_int_def prime_nat_def by auto
1.101 -
1.102 -lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
1.103 -  unfolding prime_int_def prime_nat_def by auto
1.104 +lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
1.105 +  unfolding prime_nat_def by auto
1.106
1.107 -lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
1.108 -  unfolding prime_int_def prime_nat_def by auto
1.109 -
1.110 +lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
1.111 +  unfolding prime_nat_def by auto
1.112
1.113 -lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
1.114 -    m = 1 \<or> m = p))"
1.115 -  using prime_nat_def [transferred]
1.116 -  apply (cases "p >= 0")
1.117 -  apply blast
1.118 -  apply (auto simp add: prime_ge_0_int)
1.119 -  done
1.120 +lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
1.121 +  unfolding prime_nat_def by auto
1.122
1.123 -lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1.124 +lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1.125    apply (unfold prime_nat_def)
1.126    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
1.127    done
1.128
1.129 -lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1.130 +lemma prime_int_altdef:
1.131 +  "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
1.132 +    m = 1 \<or> m = p))"
1.133 +  apply (simp add: prime_def)
1.134 +  apply (auto simp add: )
1.135 +  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
1.136 +  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
1.137 +  done
1.138 +
1.139 +lemma prime_imp_coprime_int:
1.140 +  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1.141    apply (unfold prime_int_altdef)
1.142    apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
1.143    done
1.144
1.145 -lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.146 +lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.147    by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
1.148
1.149 -lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.150 +lemma prime_dvd_mult_int:
1.151 +  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.152    by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
1.153
1.154 -lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
1.155 +lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
1.156      p dvd m * n = (p dvd m \<or> p dvd n)"
1.157    by (rule iffI, rule prime_dvd_mult_nat, auto)
1.158
1.159 -lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
1.160 -    p dvd m * n = (p dvd m \<or> p dvd n)"
1.161 +lemma prime_dvd_mult_eq_int [simp]:
1.162 +  fixes n::int
1.163 +  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
1.164    by (rule iffI, rule prime_dvd_mult_int, auto)
1.165
1.166  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1.167 @@ -163,25 +110,20 @@
1.168    by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
1.169        n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
1.170
1.171 -lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1.172 -    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1.173 -  unfolding prime_int_altdef dvd_def
1.174 -  apply auto
1.175 -  by (metis div_mult_self1_is_id div_mult_self2_is_id
1.176 -      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
1.177 -
1.178 -lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.179 +lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.180    by (induct n) auto
1.181
1.182 -lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.183 -  by (induct n) (auto simp: prime_ge_0_int)
1.184 +lemma prime_dvd_power_int:
1.185 +  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.186 +  by (induct n) auto
1.187
1.188 -lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
1.189 +lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
1.190      p dvd x^n \<longleftrightarrow> p dvd x"
1.191    by (cases n) (auto elim: prime_dvd_power_nat)
1.192
1.193 -lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
1.194 -    p dvd x^n \<longleftrightarrow> p dvd x"
1.195 +lemma prime_dvd_power_int_iff:
1.196 +  fixes x::int
1.197 +  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
1.198    by (cases n) (auto elim: prime_dvd_power_int)
1.199
1.200
1.201 @@ -190,80 +132,47 @@
1.202  lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
1.204
1.205 -lemma zero_not_prime_int [simp]: "~prime (0::int)"
1.206 -  by (simp add: prime_int_def)
1.207 -
1.208  lemma one_not_prime_nat [simp]: "~prime (1::nat)"
1.210
1.211  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
1.213
1.214 -lemma one_not_prime_int [simp]: "~prime (1::int)"
1.215 -  by (simp add: prime_int_def)
1.216 -
1.217  lemma prime_nat_code [code]:
1.218 -    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
1.219 +    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
1.221    apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
1.222    done
1.223
1.224  lemma prime_nat_simp:
1.225 -    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
1.226 +    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
1.227    by (auto simp add: prime_nat_code)
1.228
1.229  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
1.230
1.231 -lemma prime_int_code [code]:
1.232 -  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
1.233 -proof
1.234 -  assume "?L"
1.235 -  then show "?R"
1.236 -    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
1.237 -next
1.238 -  assume "?R"
1.239 -  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
1.240 -qed
1.241 -
1.242 -lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
1.243 -  by (auto simp add: prime_int_code)
1.244 -
1.245 -lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
1.246 -
1.247  lemma two_is_prime_nat [simp]: "prime (2::nat)"
1.248    by simp
1.249
1.250 -lemma two_is_prime_int [simp]: "prime (2::int)"
1.251 -  by simp
1.252 -
1.253  text{* A bit of regression testing: *}
1.254
1.255  lemma "prime(97::nat)" by simp
1.256 -lemma "prime(97::int)" by simp
1.257  lemma "prime(997::nat)" by eval
1.258 -lemma "prime(997::int)" by eval
1.259
1.260
1.261 -lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.262 +lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.263    by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
1.264
1.265 -lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.266 +lemma prime_imp_power_coprime_int:
1.267 +  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.268    by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
1.269
1.270 -lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.271 +lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.272    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
1.273
1.274 -lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.275 -  by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
1.276 -
1.277  lemma primes_imp_powers_coprime_nat:
1.278 -    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
1.279 +    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
1.280    by (rule coprime_exp2_nat, rule primes_coprime_nat)
1.281
1.282 -lemma primes_imp_powers_coprime_int:
1.283 -    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
1.284 -  by (rule coprime_exp2_int, rule primes_coprime_int)
1.285 -
1.286  lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
1.287    apply (induct n rule: nat_less_induct)
1.288    apply (case_tac "n = 0")
1.289 @@ -276,7 +185,7 @@
1.290  text {* One property of coprimality is easier to prove via prime factors. *}
1.291
1.292  lemma prime_divprod_pow_nat:
1.293 -  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.294 +  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.295    shows "p^n dvd a \<or> p^n dvd b"
1.296  proof-
1.297    { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
1.298 @@ -316,7 +225,7 @@
1.299
1.300  subsection {* Infinitely many primes *}
1.301
1.302 -lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
1.303 +lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
1.304  proof-
1.305    have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
1.306    from prime_factor_nat [OF f1]
```