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