author eberlm Fri, 22 Jul 2016 15:39:27 +0200 changeset 63535 6887fda4541a parent 63534 523b488b15c9 child 63536 8cecf0100996
Tuned primes
```--- a/src/HOL/Number_Theory/Primes.thy	Thu Jul 21 10:06:04 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Fri Jul 22 15:39:27 2016 +0200
@@ -202,8 +202,8 @@
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
unfolding One_nat_def [symmetric] by (rule not_is_prime_1)

-lemma prime_nat_code [code_unfold]:
-  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+lemma is_prime_nat_iff':
+  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
proof safe
assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
show "is_prime p" unfolding is_prime_nat_iff
@@ -217,8 +217,12 @@
qed fact+
qed (auto simp: is_prime_nat_iff)

-lemma prime_int_code [code_unfold]:
-  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma prime_nat_code [code_unfold]:
+  "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
+  by (rule ext, rule is_prime_nat_iff')
+
+lemma is_prime_int_iff':
+  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
proof
assume "?lhs"
thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
@@ -227,6 +231,10 @@
thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
qed

+lemma prime_int_code [code_unfold]:
+  "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
+  by (rule ext, rule is_prime_int_iff')
+
lemma prime_nat_simp:
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"