src/HOL/Number_Theory/Primes.thy
changeset 63535 6887fda4541a
parent 63534 523b488b15c9
child 63633 2accfb71e33b
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Thu Jul 21 10:06:04 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Jul 22 15:39:27 2016 +0200
     1.3 @@ -202,8 +202,8 @@
     1.4  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
     1.5    unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
     1.6  
     1.7 -lemma prime_nat_code [code_unfold]:
     1.8 -  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
     1.9 +lemma is_prime_nat_iff':
    1.10 +  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
    1.11  proof safe
    1.12    assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
    1.13    show "is_prime p" unfolding is_prime_nat_iff
    1.14 @@ -217,8 +217,12 @@
    1.15    qed fact+
    1.16  qed (auto simp: is_prime_nat_iff)
    1.17  
    1.18 -lemma prime_int_code [code_unfold]:
    1.19 -  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
    1.20 +lemma prime_nat_code [code_unfold]:
    1.21 +  "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
    1.22 +  by (rule ext, rule is_prime_nat_iff')
    1.23 +
    1.24 +lemma is_prime_int_iff':
    1.25 +  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
    1.26  proof
    1.27    assume "?lhs"
    1.28    thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
    1.29 @@ -227,6 +231,10 @@
    1.30    thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
    1.31  qed
    1.32  
    1.33 +lemma prime_int_code [code_unfold]:
    1.34 +  "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" 
    1.35 +  by (rule ext, rule is_prime_int_iff')
    1.36 +
    1.37  lemma prime_nat_simp:
    1.38      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
    1.39    by (auto simp add: prime_nat_code)