# HG changeset patch
# User wenzelm
# Date 1204038654 -3600
# Node ID 98d23fc025855d58087add53873814c4c65ef69e
# Parent  314c0bcb7df746d3ef4b5faf13d39cd0c5a8d690
tuned document;

diff -r 314c0bcb7df7 -r 98d23fc02585 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Tue Feb 26 11:18:43 2008 +0100
+++ b/src/HOL/Library/Primes.thy	Tue Feb 26 16:10:54 2008 +0100
@@ -12,11 +12,11 @@
 
 definition
   coprime :: "nat => nat => bool" where
-  "coprime m n = (gcd (m, n) = 1)"
+  "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)"
 
 definition
   prime :: "nat \<Rightarrow> bool" where
-  "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
@@ -93,7 +93,7 @@
   ultimately show ?thesis by blast  
 qed
 
-(* Elementary theory of divisibility                                         *)
+text {* Elementary theory of divisibility *}
 lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
 lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
   using dvd_anti_sym[of x y] by auto
@@ -178,7 +178,7 @@
 lemma divides_rexp: 
   "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
 
-(* The Bezout theorem is a bit ugly for N; it'd be easier for Z              *)
+text {* The Bezout theorem is a bit ugly for N; it'd be easier for Z *}
 lemma ind_euclid: 
   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
@@ -255,7 +255,7 @@
 apply auto
 done
 
-(* We can get a stronger version with a nonzeroness assumption.              *)
+text {* We can get a stronger version with a nonzeroness assumption. *}
 
 lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
@@ -308,7 +308,7 @@
  ultimately show ?thesis by blast
 qed
 
-(* Greatest common divisor.                                                  *)
+text {* Greatest common divisor. *}
 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)"
 proof(auto)
   assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
@@ -407,7 +407,7 @@
     by (simp add: gcd_commute)}
 qed
 
-(* Coprimality                                                               *)
+text {* Coprimality *}
 
 lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
 using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
@@ -607,7 +607,8 @@
   from n' k show ?thesis unfolding dvd_def by auto
 qed
 
-(* A binary form of the Chinese Remainder Theorem.                           *)
+
+text {* A binary form of the Chinese Remainder Theorem. *}
 
 lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
@@ -625,8 +626,9 @@
   thus ?thesis by blast
 qed
 
-(* Primality                                                                 *)
-(* A few useful theorems about primes                                        *)
+text {* Primality *}
+
+text {* A few useful theorems about primes *}
 
 lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
 lemma prime_1[simp]: "~ prime 1"  by (simp add: prime_def)
@@ -824,7 +826,8 @@
 lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
 lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
 
-(* One property of coprimality is easier to prove via prime factors.         *)
+
+text {* One property of coprimality is easier to prove via prime factors. *}
 
 lemma prime_divprod_pow: 
   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
@@ -946,7 +949,7 @@
 ultimately show ?ths by blast
 qed
 
-(* More useful lemmas.                                                       *)
+text {* More useful lemmas. *}
 lemma prime_product: 
   "prime (p*q) \<Longrightarrow> p = 1 \<or> q  = 1" unfolding prime_def by auto