tuned document;
authorwenzelm
Tue Feb 26 16:10:54 2008 +0100 (2008-02-26)
changeset 2614498d23fc02585
parent 26143 314c0bcb7df7
child 26145 95670b6e1fa3
tuned document;
src/HOL/Library/Primes.thy
     1.1 --- a/src/HOL/Library/Primes.thy	Tue Feb 26 11:18:43 2008 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Tue Feb 26 16:10:54 2008 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4  
     1.5  definition
     1.6    coprime :: "nat => nat => bool" where
     1.7 -  "coprime m n = (gcd (m, n) = 1)"
     1.8 +  "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)"
     1.9  
    1.10  definition
    1.11    prime :: "nat \<Rightarrow> bool" where
    1.12 -  "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    1.13 +  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    1.14  
    1.15  
    1.16  lemma two_is_prime: "prime 2"
    1.17 @@ -93,7 +93,7 @@
    1.18    ultimately show ?thesis by blast  
    1.19  qed
    1.20  
    1.21 -(* Elementary theory of divisibility                                         *)
    1.22 +text {* Elementary theory of divisibility *}
    1.23  lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
    1.24  lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
    1.25    using dvd_anti_sym[of x y] by auto
    1.26 @@ -178,7 +178,7 @@
    1.27  lemma divides_rexp: 
    1.28    "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
    1.29  
    1.30 -(* The Bezout theorem is a bit ugly for N; it'd be easier for Z              *)
    1.31 +text {* The Bezout theorem is a bit ugly for N; it'd be easier for Z *}
    1.32  lemma ind_euclid: 
    1.33    assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
    1.34    and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
    1.35 @@ -255,7 +255,7 @@
    1.36  apply auto
    1.37  done
    1.38  
    1.39 -(* We can get a stronger version with a nonzeroness assumption.              *)
    1.40 +text {* We can get a stronger version with a nonzeroness assumption. *}
    1.41  
    1.42  lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
    1.43    shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
    1.44 @@ -308,7 +308,7 @@
    1.45   ultimately show ?thesis by blast
    1.46  qed
    1.47  
    1.48 -(* Greatest common divisor.                                                  *)
    1.49 +text {* Greatest common divisor. *}
    1.50  lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd(a,b)"
    1.51  proof(auto)
    1.52    assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
    1.53 @@ -407,7 +407,7 @@
    1.54      by (simp add: gcd_commute)}
    1.55  qed
    1.56  
    1.57 -(* Coprimality                                                               *)
    1.58 +text {* Coprimality *}
    1.59  
    1.60  lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
    1.61  using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
    1.62 @@ -607,7 +607,8 @@
    1.63    from n' k show ?thesis unfolding dvd_def by auto
    1.64  qed
    1.65  
    1.66 -(* A binary form of the Chinese Remainder Theorem.                           *)
    1.67 +
    1.68 +text {* A binary form of the Chinese Remainder Theorem. *}
    1.69  
    1.70  lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
    1.71    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
    1.72 @@ -625,8 +626,9 @@
    1.73    thus ?thesis by blast
    1.74  qed
    1.75  
    1.76 -(* Primality                                                                 *)
    1.77 -(* A few useful theorems about primes                                        *)
    1.78 +text {* Primality *}
    1.79 +
    1.80 +text {* A few useful theorems about primes *}
    1.81  
    1.82  lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
    1.83  lemma prime_1[simp]: "~ prime 1"  by (simp add: prime_def)
    1.84 @@ -824,7 +826,8 @@
    1.85  lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
    1.86  lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
    1.87  
    1.88 -(* One property of coprimality is easier to prove via prime factors.         *)
    1.89 +
    1.90 +text {* One property of coprimality is easier to prove via prime factors. *}
    1.91  
    1.92  lemma prime_divprod_pow: 
    1.93    assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
    1.94 @@ -946,7 +949,7 @@
    1.95  ultimately show ?ths by blast
    1.96  qed
    1.97  
    1.98 -(* More useful lemmas.                                                       *)
    1.99 +text {* More useful lemmas. *}
   1.100  lemma prime_product: 
   1.101    "prime (p*q) \<Longrightarrow> p = 1 \<or> q  = 1" unfolding prime_def by auto
   1.102