src/HOL/Computational_Algebra/Primes.thy
 changeset 66837 6ba663ff2b1c parent 66453 cc19f7ca2ed6 child 67051 e7e54a0b9197
1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:47 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:48 2017 +0200
1.3 @@ -58,6 +58,9 @@
1.4  declare [[coercion int]]
1.5  declare [[coercion_enabled]]
1.7 +lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
1.8 +  using not_prime_1 [where ?'a = nat] by simp
1.9 +
1.10  lemma prime_elem_nat_iff:
1.11    "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.12  proof safe
1.13 @@ -97,9 +100,17 @@
1.14  lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
1.15    by (auto simp: prime_elem_int_nat_transfer prime_def)
1.17 -lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
1.18 +lemma prime_int_nat_transfer: "prime (k::int) \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
1.19    by (auto simp: prime_elem_int_nat_transfer prime_def)
1.21 +lemma prime_elem_iff_prime_abs:
1.22 +  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
1.23 +  by (auto intro: primeI)
1.24 +
1.25 +lemma prime_nat_iff_prime:
1.26 +  "prime (nat k) \<longleftrightarrow> prime k"
1.27 +  by (cases "k \<ge> 0") (simp_all add: prime_int_nat_transfer)
1.28 +
1.29  lemma prime_int_iff:
1.30    "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.31  proof (intro iffI conjI allI impI; (elim conjE)?)
1.32 @@ -259,9 +270,6 @@
1.34  subsubsection \<open>Make prime naively executable\<close>
1.36 -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
1.37 -  unfolding One_nat_def [symmetric] by (rule not_prime_1)
1.38 -
1.39  lemma prime_nat_iff':
1.40    "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
1.41  proof safe