src/HOL/RComplete.thy
changeset 41550 efa734d9b221
parent 37887 2ae085b07f2f
child 44667 ee5772ca7d16
     1.1 --- a/src/HOL/RComplete.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -517,10 +517,10 @@
     1.4    apply simp
     1.5  done
     1.6  
     1.7 -lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
     1.8 -  natfloor (x / real y) = natfloor x div y"
     1.9 +lemma natfloor_div_nat:
    1.10 +  assumes "1 <= x" and "y > 0"
    1.11 +  shows "natfloor (x / real y) = natfloor x div y"
    1.12  proof -
    1.13 -  assume "1 <= (x::real)" and "(y::nat) > 0"
    1.14    have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
    1.15      by simp
    1.16    then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
    1.17 @@ -535,8 +535,7 @@
    1.18      by simp
    1.19    also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
    1.20      real y + (x - real(natfloor x)) / real y"
    1.21 -    by (auto simp add: algebra_simps add_divide_distrib
    1.22 -      diff_divide_distrib prems)
    1.23 +    by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib)
    1.24    finally have "natfloor (x / real y) = natfloor(...)" by simp
    1.25    also have "... = natfloor(real((natfloor x) mod y) /
    1.26      real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
    1.27 @@ -547,11 +546,11 @@
    1.28      apply (rule add_nonneg_nonneg)
    1.29      apply (rule divide_nonneg_pos)
    1.30      apply simp
    1.31 -    apply (simp add: prems)
    1.32 +    apply (simp add: assms)
    1.33      apply (rule divide_nonneg_pos)
    1.34      apply (simp add: algebra_simps)
    1.35      apply (rule real_natfloor_le)
    1.36 -    apply (insert prems, auto)
    1.37 +    using assms apply auto
    1.38      done
    1.39    also have "natfloor(real((natfloor x) mod y) /
    1.40      real y + (x - real(natfloor x)) / real y) = 0"
    1.41 @@ -560,13 +559,13 @@
    1.42      apply (rule add_nonneg_nonneg)
    1.43      apply (rule divide_nonneg_pos)
    1.44      apply force
    1.45 -    apply (force simp add: prems)
    1.46 +    apply (force simp add: assms)
    1.47      apply (rule divide_nonneg_pos)
    1.48      apply (simp add: algebra_simps)
    1.49      apply (rule real_natfloor_le)
    1.50 -    apply (auto simp add: prems)
    1.51 -    apply (insert prems, arith)
    1.52 -    apply (simp add: add_divide_distrib [THEN sym])
    1.53 +    apply (auto simp add: assms)
    1.54 +    using assms apply arith
    1.55 +    using assms apply (simp add: add_divide_distrib [THEN sym])
    1.56      apply (subgoal_tac "real y = real y - 1 + 1")
    1.57      apply (erule ssubst)
    1.58      apply (rule add_le_less_mono)