src/HOL/Real.thy
 changeset 67051 e7e54a0b9197 parent 66912 a99a7cbf0fb5 child 67226 ec32cdaab97b
```     1.1 --- a/src/HOL/Real.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Real.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -1245,7 +1245,7 @@
1.4
1.5  lemma Rats_abs_nat_div_natE:
1.6    assumes "x \<in> \<rat>"
1.7 -  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
1.8 +  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n"
1.9  proof -
1.10    from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
1.11      by (auto simp add: Rats_eq_int_div_nat)
1.12 @@ -1281,6 +1281,8 @@
1.13      with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
1.14      with gcd show ?thesis by auto
1.15    qed
1.16 +  then have "coprime ?k ?l"
1.17 +    by (simp only: coprime_iff_gcd_eq_1)
1.18    ultimately show ?thesis ..
1.19  qed
1.20
1.21 @@ -1415,8 +1417,6 @@
1.22    for m :: nat
1.23    by (metis not_le real_of_nat_less_numeral_iff)
1.24
1.25 -declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
1.26 -
1.27  lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
1.28    by (metis floor_of_int)
1.29
1.30 @@ -1424,7 +1424,7 @@
1.31    by linarith
1.32
1.33  lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
1.34 -  by linarith
1.35 +  by (fact floor_unique)
1.36
1.37  lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
1.38    by linarith
```