# HG changeset patch # User paulson # Date 992068885 -7200 # Node ID a548865b1b6abcd91eab6e5067591b5ef6838406 # Parent 2511e48c532449ff393b39d20ed3c3a07b5b6c19 moved Primes.thy from NumberTheory to Library diff -r 2511e48c5324 -r a548865b1b6a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jun 08 08:50:08 2001 +0200 +++ b/src/HOL/IsaMakefile Sat Jun 09 08:41:25 2001 +0200 @@ -181,7 +181,8 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ - Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \ + Library/Permutation.thy Library/Primes.thy \ + Library/Quotient.thy Library/Ring_and_Field.thy \ Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \ Library/README.html Library/Continuity.thy \ Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \ @@ -241,7 +242,7 @@ HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ - Library/Permutation.thy NumberTheory/Fib.thy NumberTheory/Primes.thy \ + Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \ NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \ NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \ NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \ diff -r 2511e48c5324 -r a548865b1b6a src/HOL/Library/Primes.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Primes.thy Sat Jun 09 08:41:25 2001 +0200 @@ -0,0 +1,230 @@ +(* Title: HOL/NumberTheory/Primes.thy + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge +*) + +header {* The Greatest Common Divisor and Euclid's algorithm *} + +theory Primes = Main: + +text {* + (See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)) + + \bigskip +*} + +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" -- {* @{term gcd} as a relation *} + "is_gcd p m n == p dvd m \ p dvd n \ + (\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 \ (\m. m dvd p --> m = 1 \ m = p)}" + + +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 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 + +text {* + \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The + conjunctions don't seem provable separately. +*} + +lemma gcd_dvd_both: "gcd (m, n) dvd m \ gcd (m, n) dvd n" + apply (induct 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, standard] +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard] + + +text {* + \medskip Maximality: for all @{term m}, @{term n}, @{term k} + naturals, if @{term k} divides @{term m} and @{term k} divides + @{term n} then @{term k} divides @{term "gcd (m, n)"}. +*} + +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" + apply (induct 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 + + +text {* + \medskip 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 + +text {* + \medskip 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 + + +text {* + \medskip 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 + + +text {* + \medskip Multiplication laws +*} + +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" + -- {* Davenport, page 27 *} + apply (induct 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_mult [simp]: "gcd (k, k * n) = k" + apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) + done + +lemma gcd_self [simp]: "gcd (k, k) = k" + apply (rule gcd_mult [of k 1, simplified]) + done + +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" + apply (insert gcd_mult_distrib2 [of m k n]) + apply simp + apply (erule_tac t = m in ssubst) + apply simp + done + +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (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 + +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 \ prime ==> p dvd m * n ==> p dvd m \ p dvd n" + apply (blast intro: relprime_dvd_mult prime_imp_relprime) + done + + +text {* \medskip 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 k) + apply (simp_all add: gcd_add2 add_assoc) + done + + +text {* \medskip 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 diff -r 2511e48c5324 -r a548865b1b6a src/HOL/NumberTheory/Primes.thy --- a/src/HOL/NumberTheory/Primes.thy Fri Jun 08 08:50:08 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,230 +0,0 @@ -(* Title: HOL/NumberTheory/Primes.thy - ID: $Id$ - Author: Christophe Tabacznyj and Lawrence C Paulson - Copyright 1996 University of Cambridge -*) - -header {* The Greatest Common Divisor and Euclid's algorithm *} - -theory Primes = Main: - -text {* - (See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)) - - \bigskip -*} - -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" -- {* @{term gcd} as a relation *} - "is_gcd p m n == p dvd m \ p dvd n \ - (\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 \ (\m. m dvd p --> m = 1 \ m = p)}" - - -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 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 - -text {* - \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The - conjunctions don't seem provable separately. -*} - -lemma gcd_dvd_both: "gcd (m, n) dvd m \ gcd (m, n) dvd n" - apply (induct 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, standard] -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard] - - -text {* - \medskip Maximality: for all @{term m}, @{term n}, @{term k} - naturals, if @{term k} divides @{term m} and @{term k} divides - @{term n} then @{term k} divides @{term "gcd (m, n)"}. -*} - -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" - apply (induct 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 - - -text {* - \medskip 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 - -text {* - \medskip 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 - - -text {* - \medskip 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 - - -text {* - \medskip Multiplication laws -*} - -lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" - -- {* Davenport, page 27 *} - apply (induct 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_mult [simp]: "gcd (k, k * n) = k" - apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) - done - -lemma gcd_self [simp]: "gcd (k, k) = k" - apply (rule gcd_mult [of k 1, simplified]) - done - -lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" - apply (insert gcd_mult_distrib2 [of m k n]) - apply simp - apply (erule_tac t = m in ssubst) - apply simp - done - -lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (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 - -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 \ prime ==> p dvd m * n ==> p dvd m \ p dvd n" - apply (blast intro: relprime_dvd_mult prime_imp_relprime) - done - - -text {* \medskip 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 k) - apply (simp_all add: gcd_add2 add_assoc) - done - - -text {* \medskip 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