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.6  
     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.16  
    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.20  
    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.33  
    1.34  subsubsection \<open>Make prime naively executable\<close>
    1.35  
    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