1.1 --- a/src/HOL/Rational.thy Fri Nov 20 00:06:04 2009 -0800
1.2 +++ b/src/HOL/Rational.thy Fri Nov 20 09:22:14 2009 +0100
1.3 @@ -359,17 +359,11 @@
1.4 from gcd2 have gcd4: "gcd b' a' = 1"
1.5 by (simp add: gcd_commute_int[of a' b'])
1.6 have one: "num dvd b'"
1.7 - by (rule coprime_dvd_mult_int[OF gcd3], simp add: dvd_def, rule exI[of _ a'], simp add: eq2 algebra_simps)
1.8 - have two: "b' dvd num" by (rule coprime_dvd_mult_int[OF gcd4], simp add: dvd_def, rule exI[of _ den], simp add: eq2 algebra_simps)
1.9 - from one two
1.10 - obtain k k' where k: "num = b' * k" and k': "b' = num * k'"
1.11 - unfolding dvd_def by auto
1.12 - hence "num = num * (k * k')" by (simp add: algebra_simps)
1.13 - with num0 have prod: "k * k' = 1" by auto
1.14 - from zero_less_mult_iff[of b' k] b'p num k have kp: "k > 0"
1.15 - by auto
1.16 - from prod pos_zmult_eq_1_iff[OF kp, of k'] have "k = 1" by auto
1.17 - with k have numb': "num = b'" by auto
1.18 + by (metis coprime_dvd_mult_int[OF gcd3] dvd_triv_right eq2)
1.19 + have two: "b' dvd num"
1.20 + by (metis coprime_dvd_mult_int[OF gcd4] dvd_triv_left eq2 zmult_commute)
1.21 + from zdvd_antisym_abs[OF one two] b'p num
1.22 + have numb': "num = b'" by auto
1.23 with eq2 b'0 have "a' = den" by auto
1.24 with numb' adiv bdiv Pair show ?thesis by simp
1.25 qed