tuned proofs;
authorwenzelm
Sun Sep 18 16:59:15 2016 +0200 (2016-09-18)
changeset 63911d00d4f399f05
parent 63910 e4fdf9580372
child 63912 9f8325206465
tuned proofs;
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Rat.thy	Sun Sep 18 15:19:50 2016 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sun Sep 18 16:59:15 2016 +0200
     1.3 @@ -339,12 +339,11 @@
     1.4    then show ?thesis
     1.5    proof (rule ex1I)
     1.6      fix p
     1.7 -    obtain c d :: int where p: "p = (c, d)"
     1.8 -      by (cases p)
     1.9 -    assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
    1.10 -    with p have Fract': "r = Fract c d" "d > 0" "coprime c d"
    1.11 +    assume r: "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
    1.12 +    obtain c d where p: "p = (c, d)" by (cases p)
    1.13 +    with r have Fract': "r = Fract c d" "d > 0" "coprime c d"
    1.14        by simp_all
    1.15 -    have "c = a \<and> d = b"
    1.16 +    have "(c, d) = (a, b)"
    1.17      proof (cases "a = 0")
    1.18        case True
    1.19        with Fract Fract' show ?thesis
    1.20 @@ -382,9 +381,9 @@
    1.21    moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
    1.22      by (rule normalize_coprime) simp
    1.23    ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
    1.24 -  with quotient_of_unique
    1.25 -  have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
    1.26 -    coprime (fst p) (snd p)) = normalize (a, b)" by (rule the1_equality)
    1.27 +  then have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
    1.28 +    coprime (fst p) (snd p)) = normalize (a, b)"
    1.29 +    by (rule the1_equality [OF quotient_of_unique])
    1.30    then show ?thesis by (simp add: quotient_of_def)
    1.31  qed
    1.32