--- a/src/ZF/ex/Primes.thy Wed Apr 27 16:40:27 2005 +0200
+++ b/src/ZF/ex/Primes.thy Wed Apr 27 16:41:03 2005 +0200
@@ -2,33 +2,32 @@
ID: $Id$
Author: Christophe Tabacznyj and Lawrence C Paulson
Copyright 1996 University of Cambridge
+*)
-The "divides" relation, the greatest common divisor and Euclid's algorithm
-*)
+header{*The Divides Relation and Euclid's algorithm for the GCD*}
theory Primes = Main:
constdefs
divides :: "[i,i]=>o" (infixl "dvd" 50)
"m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
- is_gcd :: "[i,i,i]=>o" (* great common divisor *)
+ is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*}
"is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
(\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
- gcd :: "[i,i]=>i" (* gcd by Euclid's algorithm *)
+ gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*}
"gcd(m,n) == transrec(natify(n),
%n f. \<lambda>m \<in> nat.
if n=0 then m else f`(m mod n)`n) ` natify(m)"
- coprime :: "[i,i]=>o" (* coprime relation *)
+ coprime :: "[i,i]=>o" --{*the coprime relation*}
"coprime(m,n) == gcd(m,n) = 1"
- prime :: i (* set of prime numbers *)
+ prime :: i --{*the set of prime numbers*}
"prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
-(************************************************)
-(** Divides Relation **)
-(************************************************)
+
+subsection{*The Divides Relation*}
lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
by (unfold divides_def, assumption)
@@ -42,50 +41,42 @@
lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (fast intro: nat_0I mult_0_right [symmetric])
done
lemma dvd_0_left: "0 dvd m ==> m = 0"
-by (unfold divides_def, force)
+by (simp add: divides_def)
lemma dvd_refl [simp]: "m \<in> nat ==> m dvd m"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (fast intro: nat_1I mult_1_right [symmetric])
done
lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p"
-apply (unfold divides_def)
-apply (fast intro: mult_assoc mult_type)
-done
+by (auto simp add: divides_def intro: mult_assoc mult_type)
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (force dest: mult_eq_self_implies_10
simp add: mult_assoc mult_eq_1_iff)
done
lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k"
-apply (unfold divides_def)
-apply (simp add: mult_assoc, blast)
-done
+by (auto simp add: divides_def mult_assoc)
lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
-apply (unfold divides_def, clarify)
+apply (simp add: divides_def, clarify)
apply (rule_tac x = "i#*k" in bexI)
apply (simp add: mult_ac)
apply (rule mult_type)
done
-(************************************************)
-(** Greatest Common Divisor **)
-(************************************************)
-
-(* GCD by Euclid's Algorithm *)
+subsection{*Euclid's Algorithm for the GCD*}
lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
-apply (unfold gcd_def)
+apply (simp add: gcd_def)
apply (subst transrec, simp)
done
@@ -97,7 +88,7 @@
lemma gcd_non_0_raw:
"[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
-apply (unfold gcd_def)
+apply (simp add: gcd_def)
apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
mod_less_divisor [THEN ltD])
@@ -112,12 +103,12 @@
by (simp (no_asm_simp) add: gcd_non_0)
lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (fast intro: add_mult_distrib_left [symmetric] add_type)
done
lemma dvd_mult: "k dvd n ==> k dvd (m #* n)"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (fast intro: mult_left_commute mult_type)
done
@@ -132,7 +123,7 @@
lemma dvd_mod_imp_dvd_raw:
"[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
-apply (case_tac "b=0")
+apply (case_tac "b=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (blast intro: mod_div_equality [THEN subst]
elim: dvdE
@@ -166,9 +157,9 @@
by (blast intro: gcd_induct_lemma)
+subsection{*Basic Properties of @{term gcd}*}
-(* gcd type *)
-
+text{*type of gcd*}
lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> nat")
apply simp
@@ -178,7 +169,7 @@
done
-(* Property 1: gcd(a,b) divides a and b *)
+text{* Property 1: gcd(a,b) divides a and b *}
lemma gcd_dvd_both:
"[| m \<in> nat; n \<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n"
@@ -197,17 +188,17 @@
apply auto
done
-(* if f divides a and b then f divides gcd(a,b) *)
+text{* if f divides a and b then f divides gcd(a,b) *}
lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
-apply (unfold divides_def)
+apply (simp add: divides_def)
apply (case_tac "b=0")
apply (simp add: DIVISION_BY_ZERO_MOD, auto)
apply (blast intro: mod_mult_distrib2 [symmetric])
done
-(* Property 2: for all a,b,f naturals,
- if f divides a and f divides b then f divides gcd(a,b)*)
+text{* Property 2: for all a,b,f naturals,
+ if f divides a and f divides b then f divides gcd(a,b)*}
lemma gcd_greatest_raw [rule_format]:
"[| m \<in> nat; n \<in> nat; f \<in> nat |]
@@ -226,20 +217,22 @@
by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
-(* GCD PROOF: GCD exists and gcd fits the definition *)
+subsection{*The Greatest Common Divisor*}
+
+text{*The GCD exists and function gcd computes it.*}
lemma is_gcd: "[| m \<in> nat; n \<in> nat |] ==> is_gcd(gcd(m,n), m, n)"
by (simp add: is_gcd_def)
-(* GCD is unique *)
+text{*The GCD is unique*}
lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m\<in>nat; n\<in>nat|] ==> m=n"
-apply (unfold is_gcd_def)
+apply (simp add: is_gcd_def)
apply (blast intro: dvd_anti_sym)
done
lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
-by (unfold is_gcd_def, blast)
+by (simp add: is_gcd_def, blast)
lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)"
apply (rule is_gcd_unique)
@@ -274,7 +267,36 @@
by (simp add: gcd_commute [of 1])
-(* Multiplication laws *)
+subsection{*Addition laws*}
+
+lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
+apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
+apply simp
+apply (case_tac "natify (n) = 0")
+apply (auto simp add: Ord_0_lt_iff gcd_non_0)
+done
+
+lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
+apply (rule gcd_commute [THEN trans])
+apply (subst add_commute, simp)
+apply (rule gcd_commute)
+done
+
+lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
+by (subst add_commute, rule gcd_add2)
+
+lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
+apply (erule nat_induct)
+apply (auto simp add: gcd_add2 add_assoc)
+done
+
+lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
+apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
+apply auto
+done
+
+
+subsection{* Multiplication Laws*}
lemma gcd_mult_distrib2_raw:
"[| k \<in> nat; m \<in> nat; n \<in> nat |]
@@ -310,59 +332,28 @@
lemma prime_imp_relprime:
"[| p \<in> prime; ~ (p dvd n); n \<in> nat |] ==> gcd (p, n) = 1"
-apply (unfold prime_def, clarify)
+apply (simp add: prime_def, clarify)
apply (drule_tac x = "gcd (p,n)" in bspec)
apply auto
apply (cut_tac m = p and n = n in gcd_dvd2, auto)
done
lemma prime_into_nat: "p \<in> prime ==> p \<in> nat"
-by (unfold prime_def, auto)
+by (simp add: prime_def)
lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0"
-by (unfold prime_def, auto)
+by (auto simp add: prime_def)
-(*This theorem leads immediately to a proof of the uniqueness of
- factorization. If p divides a product of primes then it is
- one of those primes.*)
+text{*This theorem leads immediately to a proof of the uniqueness of
+ factorization. If @{term p} divides a product of primes then it is
+ one of those primes.*}
lemma prime_dvd_mult:
"[|p dvd m #* n; p \<in> prime; m \<in> nat; n \<in> nat |] ==> p dvd m \<or> p dvd n"
by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat)
-(** Addition laws **)
-
-lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
-apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
-apply simp
-apply (case_tac "natify (n) = 0")
-apply (auto simp add: Ord_0_lt_iff gcd_non_0)
-done
-
-lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
-apply (rule gcd_commute [THEN trans])
-apply (subst add_commute, simp)
-apply (rule gcd_commute)
-done
-
-lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
-by (subst add_commute, rule gcd_add2)
-
-lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
-apply (erule nat_induct)
-apply (auto simp add: gcd_add2 add_assoc)
-done
-
-lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
-apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
-apply auto
-done
-
-
-(* More multiplication laws *)
-
lemma gcd_mult_cancel_raw:
"[|gcd (k,n) = 1; m \<in> nat; n \<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)"
apply (rule dvd_anti_sym)
@@ -380,7 +371,7 @@
done
-(*** The square root of a prime is irrational: key lemma ***)
+subsection{*The Square Root of a Prime is Irrational: Key Lemma*}
lemma prime_dvd_other_side:
"\<lbrakk>n#*n = p#*(k#*k); p \<in> prime; n \<in> nat\<rbrakk> \<Longrightarrow> p dvd n"