tuned theory text
authorhaftmann
Mon Jun 28 15:32:27 2010 +0200 (2010-06-28)
changeset 37607ebb8b1a79c4c
parent 37606 b47dd044a1f1
child 37608 165cd386288d
tuned theory text
src/HOL/Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Jun 28 15:32:26 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Jun 28 15:32:27 2010 +0200
     1.3 @@ -208,22 +208,20 @@
     1.4  lemma one_not_prime_int [simp]: "~prime (1::int)"
     1.5    by (simp add: prime_int_def)
     1.6  
     1.7 -lemma prime_nat_code[code]:
     1.8 - "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
     1.9 -apply(simp add: Ball_def)
    1.10 +lemma prime_nat_code [code]:
    1.11 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
    1.12 +apply (simp add: Ball_def)
    1.13  apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
    1.14  done
    1.15  
    1.16  lemma prime_nat_simp:
    1.17 - "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
    1.18 -apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
    1.19 -apply(simp add:nat_number One_nat_def)
    1.20 -done
    1.21 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
    1.22 +by (auto simp add: prime_nat_code)
    1.23  
    1.24 -lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
    1.25 +lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
    1.26  
    1.27 -lemma prime_int_code[code]:
    1.28 -  "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
    1.29 +lemma prime_int_code [code]:
    1.30 +  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
    1.31  proof
    1.32    assume "?L" thus "?R"
    1.33      by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
    1.34 @@ -232,12 +230,10 @@
    1.35  qed
    1.36  
    1.37  lemma prime_int_simp:
    1.38 -  "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
    1.39 -apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
    1.40 -apply simp
    1.41 -done
    1.42 +  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
    1.43 +by (auto simp add: prime_int_code)
    1.44  
    1.45 -lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
    1.46 +lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
    1.47  
    1.48  lemma two_is_prime_nat [simp]: "prime (2::nat)"
    1.49  by simp