diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Real.thy --- a/src/HOL/Real.thy Sat Nov 11 18:33:35 2017 +0000 +++ b/src/HOL/Real.thy Sat Nov 11 18:41:08 2017 +0000 @@ -1245,7 +1245,7 @@ lemma Rats_abs_nat_div_natE: assumes "x \ \" - obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "gcd m n = 1" + obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "coprime m n" proof - from \x \ \\ obtain i :: int and n :: nat where "n \ 0" and "x = real_of_int i / real n" by (auto simp add: Rats_eq_int_div_nat) @@ -1281,6 +1281,8 @@ with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp with gcd show ?thesis by auto qed + then have "coprime ?k ?l" + by (simp only: coprime_iff_gcd_eq_1) ultimately show ?thesis .. qed @@ -1415,8 +1417,6 @@ for m :: nat by (metis not_le real_of_nat_less_numeral_iff) -declare of_int_floor_le [simp] (* FIXME duplicate!? *) - lemma of_int_floor_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" by (metis floor_of_int) @@ -1424,7 +1424,7 @@ by linarith lemma floor_eq2: "real_of_int n \ x \ x < real_of_int n + 1 \ \x\ = n" - by linarith + by (fact floor_unique) lemma floor_eq3: "real n < x \ x < real (Suc n) \ nat \x\ = n" by linarith