src/HOL/Computational_Algebra/Primes.thy
changeset 67091 1393c2340eec
parent 67051 e7e54a0b9197
child 67117 19f627407264
     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -271,7 +271,7 @@
     1.4  subsubsection \<open>Make prime naively executable\<close>
     1.5  
     1.6  lemma prime_nat_iff':
     1.7 -  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
     1.8 +  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
     1.9  proof safe
    1.10    assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
    1.11    show "prime p" unfolding prime_nat_iff
    1.12 @@ -286,7 +286,7 @@
    1.13  qed (auto simp: prime_nat_iff)
    1.14  
    1.15  lemma prime_int_iff':
    1.16 -  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
    1.17 +  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
    1.18  proof
    1.19    assume "?lhs"
    1.20    thus "?rhs"
    1.21 @@ -352,9 +352,9 @@
    1.22  lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
    1.23  proof
    1.24    assume "finite {(p::nat). prime p}"
    1.25 -  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
    1.26 +  with Max_ge have "(\<exists>b. (\<forall>x \<in> {(p::nat). prime p}. x \<le> b))"
    1.27      by auto
    1.28 -  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
    1.29 +  then obtain b where "\<forall>(x::nat). prime x \<longrightarrow> x \<le> b"
    1.30      by auto
    1.31    with bigger_prime [of b] show False
    1.32      by auto