author wenzelm Sun Sep 18 16:59:15 2016 +0200 (2016-09-18) changeset 63911 d00d4f399f05 parent 63910 e4fdf9580372 child 63912 9f8325206465
tuned proofs;
 src/HOL/Rat.thy file | annotate | diff | revisions
```     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
```