--- a/src/HOL/ex/Primes.thy Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,208 +0,0 @@
-(* Title: HOL/ex/Primes.thy
- ID: $Id$
- Author: Christophe Tabacznyj and Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-The Greatest Common Divisor and Euclid's algorithm
-
-See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)
-*)
-
-theory Primes = Main:
-consts
- gcd :: "nat*nat=>nat" (*Euclid's algorithm *)
-
-recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
- "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
-
-constdefs
- is_gcd :: "[nat,nat,nat]=>bool" (*gcd as a relation*)
- "is_gcd p m n == p dvd m & p dvd n &
- (ALL d. d dvd m & d dvd n --> d dvd p)"
-
- coprime :: "[nat,nat]=>bool"
- "coprime m n == gcd(m,n) = 1"
-
- prime :: "nat set"
- "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
-
-
-(************************************************)
-(** Greatest Common Divisor **)
-(************************************************)
-
-(*** Euclid's Algorithm ***)
-
-
-lemma gcd_induct:
- "[| !!m. P m 0;
- !!m n. [| 0<n; P n (m mod n) |] ==> P m n
- |] ==> P (m::nat) (n::nat)"
- apply (induct_tac m n rule: gcd.induct)
- apply (case_tac "n=0")
- apply (simp_all)
- done
-
-
-lemma gcd_0 [simp]: "gcd(m,0) = m"
- apply (simp);
- done
-
-lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
- apply (simp)
- done;
-
-declare gcd.simps [simp del];
-
-lemma gcd_1 [simp]: "gcd(m,1) = 1"
- apply (simp add: gcd_non_0)
- done
-
-(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
-lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp_all add: gcd_non_0)
- apply (blast dest: dvd_mod_imp_dvd)
- done
-
-lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
-lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
-
-
-(*Maximality: for all m,n,k naturals,
- if k divides m and k divides n then k divides gcd(m,n)*)
-lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp_all add: gcd_non_0 dvd_mod);
- done;
-
-lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
- apply (blast intro!: gcd_greatest intro: dvd_trans);
- done;
-
-(*Function gcd yields the Greatest Common Divisor*)
-lemma is_gcd: "is_gcd (gcd(m,n)) m n"
- apply (simp add: is_gcd_def gcd_greatest)
- done
-
-(*uniqueness of GCDs*)
-lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
- apply (simp add: is_gcd_def);
- apply (blast intro: dvd_anti_sym)
- done
-
-lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
- apply (auto simp add: is_gcd_def);
- done
-
-(** Commutativity **)
-
-lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
- apply (auto simp add: is_gcd_def);
- done
-
-lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
- apply (rule is_gcd_unique)
- apply (rule is_gcd)
- apply (subst is_gcd_commute)
- apply (simp add: is_gcd)
- done
-
-lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
- apply (rule is_gcd_unique)
- apply (rule is_gcd)
- apply (simp add: is_gcd_def);
- apply (blast intro: dvd_trans);
- done
-
-lemma gcd_0_left [simp]: "gcd(0,m) = m"
- apply (simp add: gcd_commute [of 0])
- done
-
-lemma gcd_1_left [simp]: "gcd(1,m) = 1"
- apply (simp add: gcd_commute [of 1])
- done
-
-
-(** Multiplication laws **)
-
-(*Davenport, page 27*)
-lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp)
- apply (case_tac "k=0")
- apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
- done
-
-lemma gcd_self [simp]: "gcd(m,m) = m"
- apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym])
- done
-
-lemma gcd_mult [simp]: "gcd(k, k*n) = k"
- apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
- done
-
-lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
- apply (subgoal_tac "gcd(m*k, m*n) = m")
- apply (erule_tac t="m" in subst);
- apply (simp)
- apply (simp add: gcd_mult_distrib2 [THEN sym]);
- done
-
-lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
- apply (blast intro: relprime_dvd_mult dvd_trans)
- done
-
-lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"
- apply (auto simp add: prime_def)
- apply (drule_tac x="gcd(p,n)" in spec)
- apply auto
- apply (insert gcd_dvd2 [of p n])
- apply (simp)
- done
-
-(*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.*)
-lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
- apply (blast intro: relprime_dvd_mult prime_imp_relprime)
- done
-
-
-(** Addition laws **)
-
-lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
- apply (case_tac "n=0")
- apply (simp_all add: 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)
- apply (simp add: gcd_add1)
- apply (rule gcd_commute)
- done
-
-lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
- apply (subst add_commute)
- apply (rule gcd_add2)
- done
-
-lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
- apply (induct_tac "k")
- apply (simp_all add: gcd_add2 add_assoc)
- done
-
-
-(** More multiplication laws **)
-
-lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
- apply (rule dvd_anti_sym)
- apply (rule gcd_greatest)
- apply (rule_tac n="k" in relprime_dvd_mult)
- apply (simp add: gcd_assoc)
- apply (simp add: gcd_commute)
- apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
- apply (blast intro: gcd_dvd1 dvd_trans);
- done
-
-end