gcd_dvd1 and gcd_dvd2 proven simultaneously;
authorwenzelm
Mon Nov 26 23:23:33 2001 +0100 (2001-11-26)
changeset 123009fbce4042034
parent 12299 2c76042c3b06
child 12301 adf0eff5ea62
gcd_dvd1 and gcd_dvd2 proven simultaneously;
src/HOL/Library/Primes.thy
     1.1 --- a/src/HOL/Library/Primes.thy	Mon Nov 26 18:34:17 2001 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Mon Nov 26 23:23:33 2001 +0100
     1.3 @@ -63,16 +63,13 @@
     1.4    conjunctions don't seem provable separately.
     1.5  *}
     1.6  
     1.7 -lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
     1.8 +lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
     1.9 +  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
    1.10    apply (induct m n rule: gcd_induct)
    1.11     apply (simp_all add: gcd_non_0)
    1.12    apply (blast dest: dvd_mod_imp_dvd)
    1.13    done
    1.14  
    1.15 -lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
    1.16 -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
    1.17 -
    1.18 -
    1.19  text {*
    1.20    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    1.21    naturals, if @{term k} divides @{term m} and @{term k} divides