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