New proof of gcd_zero after a change to Divides.ML made the old one fail
authorpaulson
Wed Jun 13 16:29:51 2001 +0200 (2001-06-13)
changeset 113742badb9b2a8ec
parent 11373 ef11fb6e6c58
child 11375 a6730c90e753
New proof of gcd_zero after a change to Divides.ML made the old one fail
src/HOL/Library/Primes.thy
     1.1 --- a/src/HOL/Library/Primes.thy	Wed Jun 13 16:28:40 2001 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Wed Jun 13 16:29:51 2001 +0200
     1.3 @@ -72,17 +72,6 @@
     1.4  lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
     1.5  lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
     1.6  
     1.7 -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
     1.8 -proof
     1.9 -  have "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" by simp
    1.10 -  also assume "gcd (m, n) = 0"
    1.11 -  finally have "0 dvd m \<and> 0 dvd n" .
    1.12 -  thus "m = 0 \<and> n = 0" by (simp add: dvd_0_left)
    1.13 -next
    1.14 -  assume "m = 0 \<and> n = 0"
    1.15 -  thus "gcd (m, n) = 0" by simp
    1.16 -qed
    1.17 -
    1.18  
    1.19  text {*
    1.20    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    1.21 @@ -99,6 +88,9 @@
    1.22    apply (blast intro!: gcd_greatest intro: dvd_trans)
    1.23    done
    1.24  
    1.25 +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
    1.26 +  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
    1.27 +
    1.28  
    1.29  text {*
    1.30    \medskip Function gcd yields the Greatest Common Divisor.