--- 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)"
by (auto simp add: prime_nat_code)