1.1 --- a/src/HOL/RComplete.thy Thu Mar 04 17:09:44 2010 +0100
1.2 +++ b/src/HOL/RComplete.thy Thu Mar 04 17:28:45 2010 +0100
1.3 @@ -653,6 +653,18 @@
1.4 lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
1.5 by (rule floor_diff_one) (* already declared [simp] *)
1.6
1.7 +lemma le_mult_floor:
1.8 + assumes "0 \<le> (a :: real)" and "0 \<le> b"
1.9 + shows "floor a * floor b \<le> floor (a * b)"
1.10 +proof -
1.11 + have "real (floor a) \<le> a"
1.12 + and "real (floor b) \<le> b" by auto
1.13 + hence "real (floor a * floor b) \<le> a * b"
1.14 + using assms by (auto intro!: mult_mono)
1.15 + also have "a * b < real (floor (a * b) + 1)" by auto
1.16 + finally show ?thesis unfolding real_of_int_less_iff by simp
1.17 +qed
1.18 +
1.19 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
1.20 unfolding real_of_nat_def by simp
1.21
1.22 @@ -821,6 +833,19 @@
1.23 apply simp
1.24 done
1.25
1.26 +lemma less_natfloor:
1.27 + assumes "0 \<le> x" and "x < real (n :: nat)"
1.28 + shows "natfloor x < n"
1.29 +proof (rule ccontr)
1.30 + assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
1.31 + note assms(2)
1.32 + also have "real n \<le> real (natfloor x)"
1.33 + using * unfolding real_of_nat_le_iff .
1.34 + finally have "x < real (natfloor x)" .
1.35 + with real_natfloor_le[OF assms(1)]
1.36 + show False by auto
1.37 +qed
1.38 +
1.39 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
1.40 apply (rule iffI)
1.41 apply (rule order_trans)
1.42 @@ -851,7 +876,7 @@
1.43
1.44 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
1.45 apply (unfold natfloor_def)
1.46 - apply (subst nat_int [THEN sym]);back;
1.47 + apply (subst (2) nat_int [THEN sym])
1.48 apply (subst eq_nat_nat_iff)
1.49 apply simp
1.50 apply simp
1.51 @@ -905,6 +930,83 @@
1.52 apply simp
1.53 done
1.54
1.55 +lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
1.56 + natfloor (x / real y) = natfloor x div y"
1.57 +proof -
1.58 + assume "1 <= (x::real)" and "(y::nat) > 0"
1.59 + have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
1.60 + by simp
1.61 + then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
1.62 + real((natfloor x) mod y)"
1.63 + by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
1.64 + have "x = real(natfloor x) + (x - real(natfloor x))"
1.65 + by simp
1.66 + then have "x = real ((natfloor x) div y) * real y +
1.67 + real((natfloor x) mod y) + (x - real(natfloor x))"
1.68 + by (simp add: a)
1.69 + then have "x / real y = ... / real y"
1.70 + by simp
1.71 + also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
1.72 + real y + (x - real(natfloor x)) / real y"
1.73 + by (auto simp add: algebra_simps add_divide_distrib
1.74 + diff_divide_distrib prems)
1.75 + finally have "natfloor (x / real y) = natfloor(...)" by simp
1.76 + also have "... = natfloor(real((natfloor x) mod y) /
1.77 + real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
1.78 + by (simp add: add_ac)
1.79 + also have "... = natfloor(real((natfloor x) mod y) /
1.80 + real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
1.81 + apply (rule natfloor_add)
1.82 + apply (rule add_nonneg_nonneg)
1.83 + apply (rule divide_nonneg_pos)
1.84 + apply simp
1.85 + apply (simp add: prems)
1.86 + apply (rule divide_nonneg_pos)
1.87 + apply (simp add: algebra_simps)
1.88 + apply (rule real_natfloor_le)
1.89 + apply (insert prems, auto)
1.90 + done
1.91 + also have "natfloor(real((natfloor x) mod y) /
1.92 + real y + (x - real(natfloor x)) / real y) = 0"
1.93 + apply (rule natfloor_eq)
1.94 + apply simp
1.95 + apply (rule add_nonneg_nonneg)
1.96 + apply (rule divide_nonneg_pos)
1.97 + apply force
1.98 + apply (force simp add: prems)
1.99 + apply (rule divide_nonneg_pos)
1.100 + apply (simp add: algebra_simps)
1.101 + apply (rule real_natfloor_le)
1.102 + apply (auto simp add: prems)
1.103 + apply (insert prems, arith)
1.104 + apply (simp add: add_divide_distrib [THEN sym])
1.105 + apply (subgoal_tac "real y = real y - 1 + 1")
1.106 + apply (erule ssubst)
1.107 + apply (rule add_le_less_mono)
1.108 + apply (simp add: algebra_simps)
1.109 + apply (subgoal_tac "1 + real(natfloor x mod y) =
1.110 + real(natfloor x mod y + 1)")
1.111 + apply (erule ssubst)
1.112 + apply (subst real_of_nat_le_iff)
1.113 + apply (subgoal_tac "natfloor x mod y < y")
1.114 + apply arith
1.115 + apply (rule mod_less_divisor)
1.116 + apply auto
1.117 + using real_natfloor_add_one_gt
1.118 + apply (simp add: algebra_simps)
1.119 + done
1.120 + finally show ?thesis by simp
1.121 +qed
1.122 +
1.123 +lemma le_mult_natfloor:
1.124 + assumes "0 \<le> (a :: real)" and "0 \<le> b"
1.125 + shows "natfloor a * natfloor b \<le> natfloor (a * b)"
1.126 + unfolding natfloor_def
1.127 + apply (subst nat_mult_distrib[symmetric])
1.128 + using assms apply simp
1.129 + apply (subst nat_le_eq_zle)
1.130 + using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
1.131 +
1.132 lemma natceiling_zero [simp]: "natceiling 0 = 0"
1.133 by (unfold natceiling_def, simp)
1.134
1.135 @@ -957,7 +1059,7 @@
1.136 apply (unfold natceiling_def)
1.137 apply (case_tac "x < 0")
1.138 apply simp
1.139 - apply (subst nat_int [THEN sym]);back;
1.140 + apply (subst (2) nat_int [THEN sym])
1.141 apply (subst nat_le_eq_zle)
1.142 apply simp
1.143 apply (rule ceiling_le)
1.144 @@ -1042,72 +1144,5 @@
1.145 apply simp
1.146 done
1.147
1.148 -lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
1.149 - natfloor (x / real y) = natfloor x div y"
1.150 -proof -
1.151 - assume "1 <= (x::real)" and "(y::nat) > 0"
1.152 - have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
1.153 - by simp
1.154 - then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
1.155 - real((natfloor x) mod y)"
1.156 - by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
1.157 - have "x = real(natfloor x) + (x - real(natfloor x))"
1.158 - by simp
1.159 - then have "x = real ((natfloor x) div y) * real y +
1.160 - real((natfloor x) mod y) + (x - real(natfloor x))"
1.161 - by (simp add: a)
1.162 - then have "x / real y = ... / real y"
1.163 - by simp
1.164 - also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
1.165 - real y + (x - real(natfloor x)) / real y"
1.166 - by (auto simp add: algebra_simps add_divide_distrib
1.167 - diff_divide_distrib prems)
1.168 - finally have "natfloor (x / real y) = natfloor(...)" by simp
1.169 - also have "... = natfloor(real((natfloor x) mod y) /
1.170 - real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
1.171 - by (simp add: add_ac)
1.172 - also have "... = natfloor(real((natfloor x) mod y) /
1.173 - real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
1.174 - apply (rule natfloor_add)
1.175 - apply (rule add_nonneg_nonneg)
1.176 - apply (rule divide_nonneg_pos)
1.177 - apply simp
1.178 - apply (simp add: prems)
1.179 - apply (rule divide_nonneg_pos)
1.180 - apply (simp add: algebra_simps)
1.181 - apply (rule real_natfloor_le)
1.182 - apply (insert prems, auto)
1.183 - done
1.184 - also have "natfloor(real((natfloor x) mod y) /
1.185 - real y + (x - real(natfloor x)) / real y) = 0"
1.186 - apply (rule natfloor_eq)
1.187 - apply simp
1.188 - apply (rule add_nonneg_nonneg)
1.189 - apply (rule divide_nonneg_pos)
1.190 - apply force
1.191 - apply (force simp add: prems)
1.192 - apply (rule divide_nonneg_pos)
1.193 - apply (simp add: algebra_simps)
1.194 - apply (rule real_natfloor_le)
1.195 - apply (auto simp add: prems)
1.196 - apply (insert prems, arith)
1.197 - apply (simp add: add_divide_distrib [THEN sym])
1.198 - apply (subgoal_tac "real y = real y - 1 + 1")
1.199 - apply (erule ssubst)
1.200 - apply (rule add_le_less_mono)
1.201 - apply (simp add: algebra_simps)
1.202 - apply (subgoal_tac "1 + real(natfloor x mod y) =
1.203 - real(natfloor x mod y + 1)")
1.204 - apply (erule ssubst)
1.205 - apply (subst real_of_nat_le_iff)
1.206 - apply (subgoal_tac "natfloor x mod y < y")
1.207 - apply arith
1.208 - apply (rule mod_less_divisor)
1.209 - apply auto
1.210 - using real_natfloor_add_one_gt
1.211 - apply (simp add: algebra_simps)
1.212 - done
1.213 - finally show ?thesis by simp
1.214 -qed
1.215
1.216 end
2.1 --- a/src/HOL/RealPow.thy Thu Mar 04 17:09:44 2010 +0100
2.2 +++ b/src/HOL/RealPow.thy Thu Mar 04 17:28:45 2010 +0100
2.3 @@ -6,7 +6,7 @@
2.4 header {* Natural powers theory *}
2.5
2.6 theory RealPow
2.7 -imports RealDef
2.8 +imports RealDef RComplete
2.9 begin
2.10
2.11 (* FIXME: declare this in Rings.thy or not at all *)
2.12 @@ -107,6 +107,28 @@
2.13 by (rule power_le_imp_le_base)
2.14 qed
2.15
2.16 +subsection {*Floor*}
2.17 +
2.18 +lemma floor_power:
2.19 + assumes "x = real (floor x)"
2.20 + shows "floor (x ^ n) = floor x ^ n"
2.21 +proof -
2.22 + have *: "x ^ n = real (floor x ^ n)"
2.23 + using assms by (induct n arbitrary: x) simp_all
2.24 + show ?thesis unfolding real_of_int_inject[symmetric]
2.25 + unfolding * floor_real_of_int ..
2.26 +qed
2.27 +
2.28 +lemma natfloor_power:
2.29 + assumes "x = real (natfloor x)"
2.30 + shows "natfloor (x ^ n) = natfloor x ^ n"
2.31 +proof -
2.32 + from assms have "0 \<le> floor x" by auto
2.33 + note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
2.34 + from floor_power[OF this]
2.35 + show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
2.36 + by simp
2.37 +qed
2.38
2.39 subsection {*Various Other Theorems*}
2.40
2.41 @@ -131,4 +153,5 @@
2.42 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
2.43 by (case_tac "n", auto)
2.44
2.45 +
2.46 end