moved Primes.thy from NumberTheory to Library
authorpaulson
Sat Jun 09 08:41:25 2001 +0200 (2001-06-09)
changeset 11363a548865b1b6a
parent 11362 2511e48c5324
child 11364 01020b10c0a7
moved Primes.thy from NumberTheory to Library
src/HOL/IsaMakefile
src/HOL/Library/Primes.thy
src/HOL/NumberTheory/Primes.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 08 08:50:08 2001 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sat Jun 09 08:41:25 2001 +0200
     1.3 @@ -181,7 +181,8 @@
     1.4  
     1.5  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
     1.6    Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
     1.7 -  Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \
     1.8 +  Library/Permutation.thy Library/Primes.thy \
     1.9 +  Library/Quotient.thy Library/Ring_and_Field.thy \
    1.10    Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
    1.11    Library/README.html Library/Continuity.thy \
    1.12    Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
    1.13 @@ -241,7 +242,7 @@
    1.14  HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
    1.15  
    1.16  $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
    1.17 -  Library/Permutation.thy NumberTheory/Fib.thy NumberTheory/Primes.thy \
    1.18 +  Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \
    1.19    NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
    1.20    NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
    1.21    NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Primes.thy	Sat Jun 09 08:41:25 2001 +0200
     2.3 @@ -0,0 +1,230 @@
     2.4 +(*  Title:      HOL/NumberTheory/Primes.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header {* The Greatest Common Divisor and Euclid's algorithm *}
    2.11 +
    2.12 +theory Primes = Main:
    2.13 +
    2.14 +text {*
    2.15 +  (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
    2.16 +
    2.17 +  \bigskip
    2.18 +*}
    2.19 +
    2.20 +consts
    2.21 +  gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
    2.22 +
    2.23 +recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
    2.24 +  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    2.25 +
    2.26 +constdefs
    2.27 +  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
    2.28 +  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
    2.29 +    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
    2.30 +
    2.31 +  coprime :: "nat => nat => bool"
    2.32 +  "coprime m n == gcd (m, n) = 1"
    2.33 +
    2.34 +  prime :: "nat set"
    2.35 +  "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
    2.36 +
    2.37 +
    2.38 +lemma gcd_induct:
    2.39 +  "(!!m. P m 0) ==>
    2.40 +    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    2.41 +  ==> P (m::nat) (n::nat)"
    2.42 +  apply (induct m n rule: gcd.induct)
    2.43 +  apply (case_tac "n = 0")
    2.44 +   apply simp_all
    2.45 +  done
    2.46 +
    2.47 +
    2.48 +lemma gcd_0 [simp]: "gcd (m, 0) = m"
    2.49 +  apply simp
    2.50 +  done
    2.51 +
    2.52 +lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    2.53 +  apply simp
    2.54 +  done
    2.55 +
    2.56 +declare gcd.simps [simp del]
    2.57 +
    2.58 +lemma gcd_1 [simp]: "gcd (m, 1) = 1"
    2.59 +  apply (simp add: gcd_non_0)
    2.60 +  done
    2.61 +
    2.62 +text {*
    2.63 +  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    2.64 +  conjunctions don't seem provable separately.
    2.65 +*}
    2.66 +
    2.67 +lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
    2.68 +  apply (induct m n rule: gcd_induct)
    2.69 +   apply (simp_all add: gcd_non_0)
    2.70 +  apply (blast dest: dvd_mod_imp_dvd)
    2.71 +  done
    2.72 +
    2.73 +lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
    2.74 +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
    2.75 +
    2.76 +
    2.77 +text {*
    2.78 +  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    2.79 +  naturals, if @{term k} divides @{term m} and @{term k} divides
    2.80 +  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    2.81 +*}
    2.82 +
    2.83 +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    2.84 +  apply (induct m n rule: gcd_induct)
    2.85 +   apply (simp_all add: gcd_non_0 dvd_mod)
    2.86 +  done
    2.87 +
    2.88 +lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    2.89 +  apply (blast intro!: gcd_greatest intro: dvd_trans)
    2.90 +  done
    2.91 +
    2.92 +
    2.93 +text {*
    2.94 +  \medskip Function gcd yields the Greatest Common Divisor.
    2.95 +*}
    2.96 +
    2.97 +lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    2.98 +  apply (simp add: is_gcd_def gcd_greatest)
    2.99 +  done
   2.100 +
   2.101 +text {*
   2.102 +  \medskip Uniqueness of GCDs.
   2.103 +*}
   2.104 +
   2.105 +lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   2.106 +  apply (simp add: is_gcd_def)
   2.107 +  apply (blast intro: dvd_anti_sym)
   2.108 +  done
   2.109 +
   2.110 +lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   2.111 +  apply (auto simp add: is_gcd_def)
   2.112 +  done
   2.113 +
   2.114 +
   2.115 +text {*
   2.116 +  \medskip Commutativity
   2.117 +*}
   2.118 +
   2.119 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   2.120 +  apply (auto simp add: is_gcd_def)
   2.121 +  done
   2.122 +
   2.123 +lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   2.124 +  apply (rule is_gcd_unique)
   2.125 +   apply (rule is_gcd)
   2.126 +  apply (subst is_gcd_commute)
   2.127 +  apply (simp add: is_gcd)
   2.128 +  done
   2.129 +
   2.130 +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   2.131 +  apply (rule is_gcd_unique)
   2.132 +   apply (rule is_gcd)
   2.133 +  apply (simp add: is_gcd_def)
   2.134 +  apply (blast intro: dvd_trans)
   2.135 +  done
   2.136 +
   2.137 +lemma gcd_0_left [simp]: "gcd (0, m) = m"
   2.138 +  apply (simp add: gcd_commute [of 0])
   2.139 +  done
   2.140 +
   2.141 +lemma gcd_1_left [simp]: "gcd (1, m) = 1"
   2.142 +  apply (simp add: gcd_commute [of 1])
   2.143 +  done
   2.144 +
   2.145 +
   2.146 +text {*
   2.147 +  \medskip Multiplication laws
   2.148 +*}
   2.149 +
   2.150 +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   2.151 +    -- {* Davenport, page 27 *}
   2.152 +  apply (induct m n rule: gcd_induct)
   2.153 +   apply simp
   2.154 +  apply (case_tac "k = 0")
   2.155 +   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   2.156 +  done
   2.157 +
   2.158 +lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   2.159 +  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   2.160 +  done
   2.161 +
   2.162 +lemma gcd_self [simp]: "gcd (k, k) = k"
   2.163 +  apply (rule gcd_mult [of k 1, simplified])
   2.164 +  done
   2.165 +
   2.166 +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   2.167 +  apply (insert gcd_mult_distrib2 [of m k n])
   2.168 +  apply simp
   2.169 +  apply (erule_tac t = m in ssubst)
   2.170 +  apply simp
   2.171 +  done
   2.172 +
   2.173 +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   2.174 +  apply (blast intro: relprime_dvd_mult dvd_trans)
   2.175 +  done
   2.176 +
   2.177 +lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
   2.178 +  apply (auto simp add: prime_def)
   2.179 +  apply (drule_tac x = "gcd (p, n)" in spec)
   2.180 +  apply auto
   2.181 +  apply (insert gcd_dvd2 [of p n])
   2.182 +  apply simp
   2.183 +  done
   2.184 +
   2.185 +text {*
   2.186 +  This theorem leads immediately to a proof of the uniqueness of
   2.187 +  factorization.  If @{term p} divides a product of primes then it is
   2.188 +  one of those primes.
   2.189 +*}
   2.190 +
   2.191 +lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   2.192 +  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   2.193 +  done
   2.194 +
   2.195 +
   2.196 +text {* \medskip Addition laws *}
   2.197 +
   2.198 +lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   2.199 +  apply (case_tac "n = 0")
   2.200 +   apply (simp_all add: gcd_non_0)
   2.201 +  done
   2.202 +
   2.203 +lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   2.204 +  apply (rule gcd_commute [THEN trans])
   2.205 +  apply (subst add_commute)
   2.206 +  apply (simp add: gcd_add1)
   2.207 +  apply (rule gcd_commute)
   2.208 +  done
   2.209 +
   2.210 +lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   2.211 +  apply (subst add_commute)
   2.212 +  apply (rule gcd_add2)
   2.213 +  done
   2.214 +
   2.215 +lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   2.216 +  apply (induct k)
   2.217 +   apply (simp_all add: gcd_add2 add_assoc)
   2.218 +  done
   2.219 +
   2.220 +
   2.221 +text {* \medskip More multiplication laws *}
   2.222 +
   2.223 +lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   2.224 +  apply (rule dvd_anti_sym)
   2.225 +   apply (rule gcd_greatest)
   2.226 +    apply (rule_tac n = k in relprime_dvd_mult)
   2.227 +     apply (simp add: gcd_assoc)
   2.228 +     apply (simp add: gcd_commute)
   2.229 +    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
   2.230 +  apply (blast intro: gcd_dvd1 dvd_trans)
   2.231 +  done
   2.232 +
   2.233 +end
     3.1 --- a/src/HOL/NumberTheory/Primes.thy	Fri Jun 08 08:50:08 2001 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,230 +0,0 @@
     3.4 -(*  Title:      HOL/NumberTheory/Primes.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Christophe Tabacznyj and Lawrence C Paulson
     3.7 -    Copyright   1996  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -header {* The Greatest Common Divisor and Euclid's algorithm *}
    3.11 -
    3.12 -theory Primes = Main:
    3.13 -
    3.14 -text {*
    3.15 -  (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
    3.16 -
    3.17 -  \bigskip
    3.18 -*}
    3.19 -
    3.20 -consts
    3.21 -  gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
    3.22 -
    3.23 -recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
    3.24 -  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    3.25 -
    3.26 -constdefs
    3.27 -  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
    3.28 -  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
    3.29 -    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
    3.30 -
    3.31 -  coprime :: "nat => nat => bool"
    3.32 -  "coprime m n == gcd (m, n) = 1"
    3.33 -
    3.34 -  prime :: "nat set"
    3.35 -  "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
    3.36 -
    3.37 -
    3.38 -lemma gcd_induct:
    3.39 -  "(!!m. P m 0) ==>
    3.40 -    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    3.41 -  ==> P (m::nat) (n::nat)"
    3.42 -  apply (induct m n rule: gcd.induct)
    3.43 -  apply (case_tac "n = 0")
    3.44 -   apply simp_all
    3.45 -  done
    3.46 -
    3.47 -
    3.48 -lemma gcd_0 [simp]: "gcd (m, 0) = m"
    3.49 -  apply simp
    3.50 -  done
    3.51 -
    3.52 -lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    3.53 -  apply simp
    3.54 -  done
    3.55 -
    3.56 -declare gcd.simps [simp del]
    3.57 -
    3.58 -lemma gcd_1 [simp]: "gcd (m, 1) = 1"
    3.59 -  apply (simp add: gcd_non_0)
    3.60 -  done
    3.61 -
    3.62 -text {*
    3.63 -  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    3.64 -  conjunctions don't seem provable separately.
    3.65 -*}
    3.66 -
    3.67 -lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
    3.68 -  apply (induct m n rule: gcd_induct)
    3.69 -   apply (simp_all add: gcd_non_0)
    3.70 -  apply (blast dest: dvd_mod_imp_dvd)
    3.71 -  done
    3.72 -
    3.73 -lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
    3.74 -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
    3.75 -
    3.76 -
    3.77 -text {*
    3.78 -  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    3.79 -  naturals, if @{term k} divides @{term m} and @{term k} divides
    3.80 -  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    3.81 -*}
    3.82 -
    3.83 -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    3.84 -  apply (induct m n rule: gcd_induct)
    3.85 -   apply (simp_all add: gcd_non_0 dvd_mod)
    3.86 -  done
    3.87 -
    3.88 -lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    3.89 -  apply (blast intro!: gcd_greatest intro: dvd_trans)
    3.90 -  done
    3.91 -
    3.92 -
    3.93 -text {*
    3.94 -  \medskip Function gcd yields the Greatest Common Divisor.
    3.95 -*}
    3.96 -
    3.97 -lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    3.98 -  apply (simp add: is_gcd_def gcd_greatest)
    3.99 -  done
   3.100 -
   3.101 -text {*
   3.102 -  \medskip Uniqueness of GCDs.
   3.103 -*}
   3.104 -
   3.105 -lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   3.106 -  apply (simp add: is_gcd_def)
   3.107 -  apply (blast intro: dvd_anti_sym)
   3.108 -  done
   3.109 -
   3.110 -lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   3.111 -  apply (auto simp add: is_gcd_def)
   3.112 -  done
   3.113 -
   3.114 -
   3.115 -text {*
   3.116 -  \medskip Commutativity
   3.117 -*}
   3.118 -
   3.119 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   3.120 -  apply (auto simp add: is_gcd_def)
   3.121 -  done
   3.122 -
   3.123 -lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   3.124 -  apply (rule is_gcd_unique)
   3.125 -   apply (rule is_gcd)
   3.126 -  apply (subst is_gcd_commute)
   3.127 -  apply (simp add: is_gcd)
   3.128 -  done
   3.129 -
   3.130 -lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   3.131 -  apply (rule is_gcd_unique)
   3.132 -   apply (rule is_gcd)
   3.133 -  apply (simp add: is_gcd_def)
   3.134 -  apply (blast intro: dvd_trans)
   3.135 -  done
   3.136 -
   3.137 -lemma gcd_0_left [simp]: "gcd (0, m) = m"
   3.138 -  apply (simp add: gcd_commute [of 0])
   3.139 -  done
   3.140 -
   3.141 -lemma gcd_1_left [simp]: "gcd (1, m) = 1"
   3.142 -  apply (simp add: gcd_commute [of 1])
   3.143 -  done
   3.144 -
   3.145 -
   3.146 -text {*
   3.147 -  \medskip Multiplication laws
   3.148 -*}
   3.149 -
   3.150 -lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   3.151 -    -- {* Davenport, page 27 *}
   3.152 -  apply (induct m n rule: gcd_induct)
   3.153 -   apply simp
   3.154 -  apply (case_tac "k = 0")
   3.155 -   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   3.156 -  done
   3.157 -
   3.158 -lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   3.159 -  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   3.160 -  done
   3.161 -
   3.162 -lemma gcd_self [simp]: "gcd (k, k) = k"
   3.163 -  apply (rule gcd_mult [of k 1, simplified])
   3.164 -  done
   3.165 -
   3.166 -lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   3.167 -  apply (insert gcd_mult_distrib2 [of m k n])
   3.168 -  apply simp
   3.169 -  apply (erule_tac t = m in ssubst)
   3.170 -  apply simp
   3.171 -  done
   3.172 -
   3.173 -lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   3.174 -  apply (blast intro: relprime_dvd_mult dvd_trans)
   3.175 -  done
   3.176 -
   3.177 -lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
   3.178 -  apply (auto simp add: prime_def)
   3.179 -  apply (drule_tac x = "gcd (p, n)" in spec)
   3.180 -  apply auto
   3.181 -  apply (insert gcd_dvd2 [of p n])
   3.182 -  apply simp
   3.183 -  done
   3.184 -
   3.185 -text {*
   3.186 -  This theorem leads immediately to a proof of the uniqueness of
   3.187 -  factorization.  If @{term p} divides a product of primes then it is
   3.188 -  one of those primes.
   3.189 -*}
   3.190 -
   3.191 -lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   3.192 -  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   3.193 -  done
   3.194 -
   3.195 -
   3.196 -text {* \medskip Addition laws *}
   3.197 -
   3.198 -lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   3.199 -  apply (case_tac "n = 0")
   3.200 -   apply (simp_all add: gcd_non_0)
   3.201 -  done
   3.202 -
   3.203 -lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   3.204 -  apply (rule gcd_commute [THEN trans])
   3.205 -  apply (subst add_commute)
   3.206 -  apply (simp add: gcd_add1)
   3.207 -  apply (rule gcd_commute)
   3.208 -  done
   3.209 -
   3.210 -lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   3.211 -  apply (subst add_commute)
   3.212 -  apply (rule gcd_add2)
   3.213 -  done
   3.214 -
   3.215 -lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   3.216 -  apply (induct k)
   3.217 -   apply (simp_all add: gcd_add2 add_assoc)
   3.218 -  done
   3.219 -
   3.220 -
   3.221 -text {* \medskip More multiplication laws *}
   3.222 -
   3.223 -lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   3.224 -  apply (rule dvd_anti_sym)
   3.225 -   apply (rule gcd_greatest)
   3.226 -    apply (rule_tac n = k in relprime_dvd_mult)
   3.227 -     apply (simp add: gcd_assoc)
   3.228 -     apply (simp add: gcd_commute)
   3.229 -    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
   3.230 -  apply (blast intro: gcd_dvd1 dvd_trans)
   3.231 -  done
   3.232 -
   3.233 -end