author haftmann Mon Jun 28 15:32:27 2010 +0200 (2010-06-28) changeset 37607 ebb8b1a79c4c parent 37606 b47dd044a1f1 child 37608 165cd386288d
tuned theory text
```     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.6
1.7 -lemma prime_nat_code[code]:
1.8 - "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
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.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.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
```