# HG changeset patch
# User haftmann
# Date 1481984533 -3600
# Node ID 6621d91d3c8a87bb99ccd39e2a81b38f781eb2aa
# Parent  c1932a4a227f3d2fad4f569b4c75d0b4e04d1a14
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat

diff -r c1932a4a227f -r 6621d91d3c8a src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -241,12 +241,18 @@
     "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
   by (auto simp add: prime_int_code)
 
-lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
+lemma prime_int_numeral_eq [simp]:
+  "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
+  by (simp add: prime_int_nat_transfer)
 
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
-  by simp
+  by (simp add: prime_nat_simp)
 
-declare prime_int_nat_transfer[of "numeral m" for m, simp]
+lemma prime_nat_numeral_eq [simp]:
+  "prime (numeral m :: nat) \<longleftrightarrow>
+    (1::nat) < numeral m \<and>
+    (\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)"
+  by (fact prime_nat_simp) -- \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
 
 
 text\<open>A bit of regression testing:\<close>