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.42 -declare transfer_morphism_nat_int[transfer add return:
    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.48 -declare transfer_morphism_int_nat[transfer add return:
    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.203    by (simp add: prime_nat_def)
   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.209    by (simp add: prime_nat_def)
   1.210  
   1.211  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   1.212    by (simp add: prime_nat_def)
   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.220    apply (simp add: Ball_def)
   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]