summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 13 Jun 2001 16:29:51 +0200 | |

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

--- a/src/HOL/Library/Primes.thy Wed Jun 13 16:28:40 2001 +0200 +++ b/src/HOL/Library/Primes.thy Wed Jun 13 16:29:51 2001 +0200 @@ -72,17 +72,6 @@ lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard] lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard] -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)" -proof - have "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" by simp - also assume "gcd (m, n) = 0" - finally have "0 dvd m \<and> 0 dvd n" . - thus "m = 0 \<and> n = 0" by (simp add: dvd_0_left) -next - assume "m = 0 \<and> n = 0" - thus "gcd (m, n) = 0" by simp -qed - text {* \medskip Maximality: for all @{term m}, @{term n}, @{term k} @@ -99,6 +88,9 @@ apply (blast intro!: gcd_greatest intro: dvd_trans) done +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)" + by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff) + text {* \medskip Function gcd yields the Greatest Common Divisor.