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)
```