src/HOL/Real.thy
changeset 58834 773b378d9313
parent 58789 387f65e69dd5
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Real.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Real.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -1132,12 +1132,10 @@
     1.4      by (auto simp add: add_divide_distrib algebra_simps)
     1.5  qed
     1.6  
     1.7 -lemma real_of_int_div: "(d :: int) dvd n ==>
     1.8 -    real(n div d) = real n / real d"
     1.9 -  apply (subst real_of_int_div_aux)
    1.10 -  apply simp
    1.11 -  apply (simp add: dvd_eq_mod_eq_0)
    1.12 -done
    1.13 +lemma real_of_int_div:
    1.14 +  fixes d n :: int
    1.15 +  shows "d dvd n \<Longrightarrow> real (n div d) = real n / real d"
    1.16 +  by (simp add: real_of_int_div_aux)
    1.17  
    1.18  lemma real_of_int_div2:
    1.19    "0 <= real (n::int) / real (x) - real (n div x)"
    1.20 @@ -1391,12 +1389,15 @@
    1.21      by (rule dvd_mult_div_cancel)
    1.22    have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
    1.23      by (rule dvd_mult_div_cancel)
    1.24 -  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
    1.25 +  from `n \<noteq> 0` and gcd_l
    1.26 +  have "?gcd * ?l \<noteq> 0" by simp
    1.27 +  then have "?l \<noteq> 0" by (blast dest!: mult_not_zero) 
    1.28    moreover
    1.29    have "\<bar>x\<bar> = real ?k / real ?l"
    1.30    proof -
    1.31      from gcd have "real ?k / real ?l =
    1.32 -        real (?gcd * ?k) / real (?gcd * ?l)" by simp
    1.33 +      real (?gcd * ?k) / real (?gcd * ?l)"
    1.34 +      by (simp only: real_of_nat_mult) simp
    1.35      also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
    1.36      also from x_rat have "\<dots> = \<bar>x\<bar>" ..
    1.37      finally show ?thesis ..