src/HOL/Decision_Procs/Rat_Pair.thy
changeset 67051 e7e54a0b9197
parent 62390 842917225d56
child 67123 3fe40ff1b921
     1.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -51,7 +51,8 @@
     1.4      from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
     1.5      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
     1.6      from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
     1.7 -    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
     1.8 +    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
     1.9 +      by simp
    1.10      from ab consider "b < 0" | "b > 0" by arith
    1.11      then show ?thesis
    1.12      proof cases
    1.13 @@ -198,6 +199,8 @@
    1.14      from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
    1.15      have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
    1.16        by (simp_all add: x y isnormNum_def add: gcd.commute)
    1.17 +    then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
    1.18 +      by (simp_all add: coprime_iff_gcd_eq_1)
    1.19      from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
    1.20        apply -
    1.21        apply algebra
    1.22 @@ -205,11 +208,11 @@
    1.23        apply simp
    1.24        apply algebra
    1.25        done
    1.26 -    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
    1.27 -        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
    1.28 -      have eq1: "b = b'" using pos by arith
    1.29 -      with eq have "a = a'" using pos by simp
    1.30 -      with eq1 show ?thesis by (simp add: x y)
    1.31 +    then have eq1: "b = b'"
    1.32 +      using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
    1.33 +      by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
    1.34 +    with eq have "a = a'" using pos by simp
    1.35 +    with \<open>b = b'\<close> show ?thesis by (simp add: x y)
    1.36    qed
    1.37    show ?lhs if ?rhs
    1.38      using that by simp