author | paulson |

Wed Jun 13 16:29:51 2001 +0200 (2001-06-13) | |

changeset 11374 | 2badb9b2a8ec |

parent 11373 | ef11fb6e6c58 |

child 11375 | a6730c90e753 |

New proof of gcd_zero after a change to Divides.ML made the old one fail

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.