src/HOL/Library/Primes.thy
 changeset 16663 13e9c402308b parent 15628 9f912f8fd2df child 16762 aafd23b47a5d
```     1.1 --- a/src/HOL/Library/Primes.thy	Fri Jul 01 14:55:05 2005 +0200
1.2 +++ b/src/HOL/Library/Primes.thy	Fri Jul 01 17:41:10 2005 +0200
1.3 @@ -29,8 +29,8 @@
1.4    coprime :: "nat => nat => bool"
1.5    "coprime m n == gcd (m, n) = 1"
1.6
1.7 -  prime :: "nat set"
1.8 -  "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
1.9 +  prime :: "nat \<Rightarrow> bool"
1.10 +  "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
1.11
1.12
1.13  lemma gcd_induct:
1.14 @@ -172,7 +172,7 @@
1.15    apply (blast intro: relprime_dvd_mult dvd_trans)
1.16    done
1.17
1.18 -lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
1.19 +lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
1.20    apply (auto simp add: prime_def)
1.21    apply (drule_tac x = "gcd (p, n)" in spec)
1.22    apply auto
1.23 @@ -180,7 +180,7 @@
1.24    apply simp
1.25    done
1.26
1.27 -lemma two_is_prime: "2 \<in> prime"
1.28 +lemma two_is_prime: "prime 2"
1.29    apply (auto simp add: prime_def)
1.30    apply (case_tac m)
1.31     apply (auto dest!: dvd_imp_le)
1.32 @@ -192,13 +192,13 @@
1.33    one of those primes.
1.34  *}
1.35
1.36 -lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
1.37 +lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
1.38    by (blast intro: relprime_dvd_mult prime_imp_relprime)
1.39
1.40 -lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
1.41 +lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
1.42    by (auto dest: prime_dvd_mult)
1.43
1.44 -lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
1.45 +lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
1.46    by (rule prime_dvd_square) (simp_all add: power2_eq_square)
1.47
1.48
```