author wenzelm Tue, 26 Feb 2008 16:10:54 +0100 changeset 26144 98d23fc02585 parent 26143 314c0bcb7df7 child 26145 95670b6e1fa3
tuned document;
```--- 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 @@
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
```