src/HOL/RComplete.thy
 changeset 30240 5b25fee0362c parent 29667 53103fc8ffa3 child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/RComplete.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/RComplete.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -1,8 +1,8 @@
1.4 -(*  Title       : HOL/RComplete.thy
1.5 -    Author      : Jacques D. Fleuriot, University of Edinburgh
1.6 -    Author      : Larry Paulson, University of Cambridge
1.7 -    Author      : Jeremy Avigad, Carnegie Mellon University
1.8 -    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
1.9 +(*  Title:      HOL/RComplete.thy
1.10 +    Author:     Jacques D. Fleuriot, University of Edinburgh
1.11 +    Author:     Larry Paulson, University of Cambridge
1.12 +    Author:     Jeremy Avigad, Carnegie Mellon University
1.13 +    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
1.14  *)
1.15
1.16  header {* Completeness of the Reals; Floor and Ceiling Functions *}
1.17 @@ -380,33 +380,28 @@
1.18    thus "\<exists>(n::nat). x < real n" ..
1.19  qed
1.20
1.21 +instance real :: archimedean_field
1.22 +proof
1.23 +  fix r :: real
1.24 +  obtain n :: nat where "r < real n"
1.25 +    using reals_Archimedean2 ..
1.26 +  then have "r \<le> of_int (int n)"
1.27 +    unfolding real_eq_of_nat by simp
1.28 +  then show "\<exists>z. r \<le> of_int z" ..
1.29 +qed
1.30 +
1.31  lemma reals_Archimedean3:
1.32    assumes x_greater_zero: "0 < x"
1.33    shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
1.34 -proof
1.35 -  fix y
1.36 -  have x_not_zero: "x \<noteq> 0" using x_greater_zero by simp
1.37 -  obtain n where "y * inverse x < real (n::nat)"
1.38 -    using reals_Archimedean2 ..
1.39 -  hence "y * inverse x * x < real n * x"
1.40 -    using x_greater_zero by (simp add: mult_strict_right_mono)
1.41 -  hence "x * inverse x * y < x * real n"
1.42 -    by (simp add: algebra_simps)
1.43 -  hence "y < real (n::nat) * x"
1.44 -    using x_not_zero by (simp add: algebra_simps)
1.45 -  thus "\<exists>(n::nat). y < real n * x" ..
1.46 -qed
1.47 +  unfolding real_of_nat_def using `0 < x`
1.48 +  by (auto intro: ex_less_of_nat_mult)
1.49
1.50  lemma reals_Archimedean6:
1.51       "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
1.52 -apply (insert reals_Archimedean2 [of r], safe)
1.53 -apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto)
1.54 -apply (rule_tac x = x in exI)
1.55 -apply (case_tac x, simp)
1.56 -apply (rename_tac x')
1.57 -apply (drule_tac x = x' in spec, simp)
1.58 -apply (rule_tac x="LEAST n. r < real n" in exI, safe)
1.59 -apply (erule LeastI, erule Least_le)
1.60 +unfolding real_of_nat_def
1.61 +apply (rule exI [where x="nat (floor r + 1)"])
1.62 +apply (insert floor_correct [of r])
1.64  done
1.65
1.66  lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
1.67 @@ -414,19 +409,11 @@
1.68
1.69  lemma reals_Archimedean_6b_int:
1.70       "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
1.71 -apply (drule reals_Archimedean6a, auto)
1.72 -apply (rule_tac x = "int n" in exI)
1.73 -apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
1.74 -done
1.75 +  unfolding real_of_int_def by (rule floor_exists)
1.76
1.77  lemma reals_Archimedean_6c_int:
1.78       "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
1.79 -apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
1.80 -apply (rename_tac n)
1.81 -apply (drule order_le_imp_less_or_eq, auto)
1.82 -apply (rule_tac x = "- n - 1" in exI)
1.83 -apply (rule_tac [2] x = "- n" in exI, auto)
1.84 -done
1.85 +  unfolding real_of_int_def by (rule floor_exists)
1.86
1.87
1.88  subsection{*Density of the Rational Reals in the Reals*}
1.89 @@ -485,23 +472,6 @@
1.90
1.91  subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
1.92
1.93 -definition
1.94 -  floor :: "real => int" where
1.95 -  [code del]: "floor r = (LEAST n::int. r < real (n+1))"
1.96 -
1.97 -definition
1.98 -  ceiling :: "real => int" where
1.99 -  "ceiling r = - floor (- r)"
1.100 -
1.101 -notation (xsymbols)
1.102 -  floor  ("\<lfloor>_\<rfloor>") and
1.103 -  ceiling  ("\<lceil>_\<rceil>")
1.104 -
1.105 -notation (HTML output)
1.106 -  floor  ("\<lfloor>_\<rfloor>") and
1.107 -  ceiling  ("\<lceil>_\<rceil>")
1.108 -
1.109 -
1.110  lemma number_of_less_real_of_int_iff [simp]:
1.111       "((number_of n) < real (m::int)) = (number_of n < m)"
1.112  apply auto
1.113 @@ -524,51 +494,23 @@
1.114       "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
1.115  by (simp add: linorder_not_less [symmetric])
1.116
1.117 -lemma floor_zero [simp]: "floor 0 = 0"
1.119 -apply (rule Least_equality)
1.120 -apply simp_all
1.121 -done
1.122 -
1.123 -lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
1.124 -by auto
1.125 +lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
1.126 +by auto (* delete? *)
1.127
1.128  lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
1.129 -apply (simp only: floor_def)
1.130 -apply (rule Least_equality)
1.131 -apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
1.132 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
1.133 -apply simp_all
1.134 -done
1.135 +unfolding real_of_nat_def by simp
1.136
1.137  lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
1.138 -apply (simp only: floor_def)
1.139 -apply (rule Least_equality)
1.140 -apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
1.141 -apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
1.142 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
1.143 -apply simp_all
1.144 -done
1.145 +unfolding real_of_nat_def by (simp add: floor_minus)
1.146
1.147  lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
1.148 -apply (simp only: floor_def)
1.149 -apply (rule Least_equality)
1.150 -apply auto
1.151 -done
1.152 +unfolding real_of_int_def by simp
1.153
1.154  lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
1.155 -apply (simp only: floor_def)
1.156 -apply (rule Least_equality)
1.157 -apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
1.158 -apply auto
1.159 -done
1.160 +unfolding real_of_int_def by (simp add: floor_minus)
1.161
1.162  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
1.163 -apply (case_tac "r < 0")
1.164 -apply (blast intro: reals_Archimedean_6c_int)
1.165 -apply (simp only: linorder_not_less)
1.166 -apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
1.167 -done
1.168 +unfolding real_of_int_def by (rule floor_exists)
1.169
1.170  lemma lemma_floor:
1.171    assumes a1: "real m \<le> r" and a2: "r < real n + 1"
1.172 @@ -581,48 +523,20 @@
1.173  qed
1.174
1.175  lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
1.176 -apply (simp add: floor_def Least_def)
1.177 -apply (insert real_lb_ub_int [of r], safe)
1.178 -apply (rule theI2)
1.179 -apply auto
1.180 -done
1.181 -
1.182 -lemma floor_mono: "x < y ==> floor x \<le> floor y"
1.183 -apply (simp add: floor_def Least_def)
1.184 -apply (insert real_lb_ub_int [of x])
1.185 -apply (insert real_lb_ub_int [of y], safe)
1.186 -apply (rule theI2)
1.187 -apply (rule_tac [3] theI2)
1.188 -apply simp
1.189 -apply (erule conjI)
1.190 -apply (auto simp add: order_eq_iff int_le_real_less)
1.191 -done
1.192 -
1.193 -lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
1.194 -by (auto dest: order_le_imp_less_or_eq simp add: floor_mono)
1.195 +unfolding real_of_int_def by (rule of_int_floor_le)
1.196
1.197  lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
1.198  by (auto intro: lemma_floor)
1.199
1.200  lemma real_of_int_floor_cancel [simp]:
1.201      "(real (floor x) = x) = (\<exists>n::int. x = real n)"
1.202 -apply (simp add: floor_def Least_def)
1.203 -apply (insert real_lb_ub_int [of x], erule exE)
1.204 -apply (rule theI2)
1.205 -apply (auto intro: lemma_floor)
1.206 -done
1.207 +  using floor_real_of_int by metis
1.208
1.209  lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
1.211 -apply (rule Least_equality)
1.212 -apply (auto intro: lemma_floor)
1.213 -done
1.214 +  unfolding real_of_int_def using floor_unique [of n x] by simp
1.215
1.216  lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
1.218 -apply (rule Least_equality)
1.219 -apply (auto intro: lemma_floor)
1.220 -done
1.221 +  unfolding real_of_int_def by (rule floor_unique)
1.222
1.223  lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
1.224  apply (rule inj_int [THEN injD])
1.225 @@ -635,353 +549,205 @@
1.226  apply (auto intro: floor_eq3)
1.227  done
1.228
1.229 -lemma floor_number_of_eq [simp]:
1.230 +lemma floor_number_of_eq:
1.231       "floor(number_of n :: real) = (number_of n :: int)"
1.232 -apply (subst real_number_of [symmetric])
1.233 -apply (rule floor_real_of_int)
1.234 -done
1.235 -
1.236 -lemma floor_one [simp]: "floor 1 = 1"
1.237 -  apply (rule trans)
1.238 -  prefer 2
1.239 -  apply (rule floor_real_of_int)
1.240 -  apply simp
1.241 -done
1.242 +  by (rule floor_number_of) (* already declared [simp] *)
1.243
1.244  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
1.245 -apply (simp add: floor_def Least_def)
1.246 -apply (insert real_lb_ub_int [of r], safe)
1.247 -apply (rule theI2)
1.248 -apply (auto intro: lemma_floor)
1.249 -done
1.250 +  unfolding real_of_int_def using floor_correct [of r] by simp
1.251
1.252  lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
1.253 -apply (simp add: floor_def Least_def)
1.254 -apply (insert real_lb_ub_int [of r], safe)
1.255 -apply (rule theI2)
1.256 -apply (auto intro: lemma_floor)
1.257 -done
1.258 +  unfolding real_of_int_def using floor_correct [of r] by simp
1.259
1.260  lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
1.261 -apply (insert real_of_int_floor_ge_diff_one [of r])
1.262 -apply (auto simp del: real_of_int_floor_ge_diff_one)
1.263 -done
1.264 +  unfolding real_of_int_def using floor_correct [of r] by simp
1.265
1.266  lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
1.267 -apply (insert real_of_int_floor_gt_diff_one [of r])
1.268 -apply (auto simp del: real_of_int_floor_gt_diff_one)
1.269 -done
1.270 +  unfolding real_of_int_def using floor_correct [of r] by simp
1.271
1.272  lemma le_floor: "real a <= x ==> a <= floor x"
1.273 -  apply (subgoal_tac "a < floor x + 1")
1.274 -  apply arith
1.275 -  apply (subst real_of_int_less_iff [THEN sym])
1.276 -  apply simp
1.277 -  apply (insert real_of_int_floor_add_one_gt [of x])
1.278 -  apply arith
1.279 -done
1.280 +  unfolding real_of_int_def by (simp add: le_floor_iff)
1.281
1.282  lemma real_le_floor: "a <= floor x ==> real a <= x"
1.283 -  apply (rule order_trans)
1.284 -  prefer 2
1.285 -  apply (rule real_of_int_floor_le)
1.286 -  apply (subst real_of_int_le_iff)
1.287 -  apply assumption
1.288 -done
1.289 +  unfolding real_of_int_def by (simp add: le_floor_iff)
1.290
1.291  lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
1.292 -  apply (rule iffI)
1.293 -  apply (erule real_le_floor)
1.294 -  apply (erule le_floor)
1.295 -done
1.296 +  unfolding real_of_int_def by (rule le_floor_iff)
1.297
1.298 -lemma le_floor_eq_number_of [simp]:
1.299 +lemma le_floor_eq_number_of:
1.300      "(number_of n <= floor x) = (number_of n <= x)"
1.302 +  by (rule number_of_le_floor) (* already declared [simp] *)
1.303
1.304 -lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
1.306 +lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
1.307 +  by (rule zero_le_floor) (* already declared [simp] *)
1.308
1.309 -lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
1.311 +lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
1.312 +  by (rule one_le_floor) (* already declared [simp] *)
1.313
1.314  lemma floor_less_eq: "(floor x < a) = (x < real a)"
1.315 -  apply (subst linorder_not_le [THEN sym])+
1.316 -  apply simp
1.317 -  apply (rule le_floor_eq)
1.318 -done
1.319 +  unfolding real_of_int_def by (rule floor_less_iff)
1.320
1.321 -lemma floor_less_eq_number_of [simp]:
1.322 +lemma floor_less_eq_number_of:
1.323      "(floor x < number_of n) = (x < number_of n)"
1.325 +  by (rule floor_less_number_of) (* already declared [simp] *)
1.326
1.327 -lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
1.329 +lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
1.330 +  by (rule floor_less_zero) (* already declared [simp] *)
1.331
1.332 -lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
1.334 +lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
1.335 +  by (rule floor_less_one) (* already declared [simp] *)
1.336
1.337  lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
1.338 -  apply (insert le_floor_eq [of "a + 1" x])
1.339 -  apply auto
1.340 -done
1.341 +  unfolding real_of_int_def by (rule less_floor_iff)
1.342
1.343 -lemma less_floor_eq_number_of [simp]:
1.344 +lemma less_floor_eq_number_of:
1.345      "(number_of n < floor x) = (number_of n + 1 <= x)"
1.347 +  by (rule number_of_less_floor) (* already declared [simp] *)
1.348
1.349 -lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
1.351 +lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
1.352 +  by (rule zero_less_floor) (* already declared [simp] *)
1.353
1.354 -lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
1.356 +lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
1.357 +  by (rule one_less_floor) (* already declared [simp] *)
1.358
1.359  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
1.360 -  apply (insert floor_less_eq [of x "a + 1"])
1.361 -  apply auto
1.362 -done
1.363 +  unfolding real_of_int_def by (rule floor_le_iff)
1.364
1.365 -lemma floor_le_eq_number_of [simp]:
1.366 +lemma floor_le_eq_number_of:
1.367      "(floor x <= number_of n) = (x < number_of n + 1)"
1.369 +  by (rule floor_le_number_of) (* already declared [simp] *)
1.370
1.371 -lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
1.373 +lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
1.374 +  by (rule floor_le_zero) (* already declared [simp] *)
1.375
1.376 -lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
1.378 +lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
1.379 +  by (rule floor_le_one) (* already declared [simp] *)
1.380
1.381  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
1.382 -  apply (subst order_eq_iff)
1.383 -  apply (rule conjI)
1.384 -  prefer 2
1.385 -  apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
1.386 -  apply arith
1.387 -  apply (subst real_of_int_less_iff [THEN sym])
1.388 -  apply simp
1.389 -  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
1.390 -  apply (subgoal_tac "real (floor x) <= x")
1.391 -  apply arith
1.392 -  apply (rule real_of_int_floor_le)
1.394 -  apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
1.395 -  apply arith
1.396 -  apply (subst real_of_int_less_iff [THEN sym])
1.397 -  apply simp
1.398 -  apply (subgoal_tac "real(floor(x + real a)) <= x + real a")
1.399 -  apply (subgoal_tac "x < real(floor x) + 1")
1.400 -  apply arith
1.402 -  apply (rule real_of_int_floor_le)
1.403 -done
1.404 -
1.406 -    "floor (x + number_of n) = floor x + number_of n"
1.407 -  apply (subst floor_add [THEN sym])
1.408 -  apply simp
1.409 -done
1.410 -
1.411 -lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
1.412 -  apply (subst floor_add [THEN sym])
1.413 -  apply simp
1.414 -done
1.415 +  unfolding real_of_int_def by (rule floor_add_of_int)
1.416
1.417  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
1.418 -  apply (subst diff_minus)+
1.419 -  apply (subst real_of_int_minus [THEN sym])
1.421 -done
1.422 +  unfolding real_of_int_def by (rule floor_diff_of_int)
1.423
1.424 -lemma floor_subtract_number_of [simp]: "floor (x - number_of n) =
1.425 +lemma floor_subtract_number_of: "floor (x - number_of n) =
1.426      floor x - number_of n"
1.427 -  apply (subst floor_subtract [THEN sym])
1.428 -  apply simp
1.429 -done
1.430 +  by (rule floor_diff_number_of) (* already declared [simp] *)
1.431
1.432 -lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
1.433 -  apply (subst floor_subtract [THEN sym])
1.434 -  apply simp
1.435 -done
1.436 -
1.437 -lemma ceiling_zero [simp]: "ceiling 0 = 0"
1.439 +lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
1.440 +  by (rule floor_diff_one) (* already declared [simp] *)
1.441
1.442  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
1.444 +  unfolding real_of_nat_def by simp
1.445
1.446 -lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
1.447 -by auto
1.448 +lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
1.449 +by auto (* delete? *)
1.450
1.451  lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
1.453 +  unfolding real_of_int_def by simp
1.454
1.455  lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
1.457 +  unfolding real_of_int_def by simp
1.458
1.459  lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
1.461 -apply (subst le_minus_iff, simp)
1.462 -done
1.463 +  unfolding real_of_int_def by (rule le_of_int_ceiling)
1.464
1.465 -lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
1.466 -by (simp add: floor_mono ceiling_def)
1.467 -
1.468 -lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
1.469 -by (simp add: floor_mono2 ceiling_def)
1.470 +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
1.471 +  unfolding real_of_int_def by simp
1.472
1.473  lemma real_of_int_ceiling_cancel [simp]:
1.474       "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
1.475 -apply (auto simp add: ceiling_def)
1.476 -apply (drule arg_cong [where f = uminus], auto)
1.477 -apply (rule_tac x = "-n" in exI, auto)
1.478 -done
1.479 +  using ceiling_real_of_int by metis
1.480
1.481  lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
1.483 -apply (rule minus_equation_iff [THEN iffD1])
1.484 -apply (simp add: floor_eq [where n = "-(n+1)"])
1.485 -done
1.486 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
1.487
1.488  lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
1.489 -by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
1.490 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
1.491
1.492  lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
1.493 -by (simp add: ceiling_def floor_eq2 [where n = "-n"])
1.494 +  unfolding real_of_int_def using ceiling_unique [of n x] by simp
1.495
1.496 -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
1.498 -
1.499 -lemma ceiling_number_of_eq [simp]:
1.500 +lemma ceiling_number_of_eq:
1.501       "ceiling (number_of n :: real) = (number_of n)"
1.502 -apply (subst real_number_of [symmetric])
1.503 -apply (rule ceiling_real_of_int)
1.504 -done
1.505 -
1.506 -lemma ceiling_one [simp]: "ceiling 1 = 1"
1.507 -  by (unfold ceiling_def, simp)
1.508 +  by (rule ceiling_number_of) (* already declared [simp] *)
1.509
1.510  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
1.511 -apply (rule neg_le_iff_le [THEN iffD1])
1.512 -apply (simp add: ceiling_def diff_minus)
1.513 -done
1.514 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
1.515
1.516  lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
1.517 -apply (insert real_of_int_ceiling_diff_one_le [of r])
1.518 -apply (simp del: real_of_int_ceiling_diff_one_le)
1.519 -done
1.520 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
1.521
1.522  lemma ceiling_le: "x <= real a ==> ceiling x <= a"
1.523 -  apply (unfold ceiling_def)
1.524 -  apply (subgoal_tac "-a <= floor(- x)")
1.525 -  apply simp
1.526 -  apply (rule le_floor)
1.527 -  apply simp
1.528 -done
1.529 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
1.530
1.531  lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
1.532 -  apply (unfold ceiling_def)
1.533 -  apply (subgoal_tac "real(- a) <= - x")
1.534 -  apply simp
1.535 -  apply (rule real_le_floor)
1.536 -  apply simp
1.537 -done
1.538 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
1.539
1.540  lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
1.541 -  apply (rule iffI)
1.542 -  apply (erule ceiling_le_real)
1.543 -  apply (erule ceiling_le)
1.544 -done
1.545 +  unfolding real_of_int_def by (rule ceiling_le_iff)
1.546
1.547 -lemma ceiling_le_eq_number_of [simp]:
1.548 +lemma ceiling_le_eq_number_of:
1.549      "(ceiling x <= number_of n) = (x <= number_of n)"
1.551 +  by (rule ceiling_le_number_of) (* already declared [simp] *)
1.552
1.553 -lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)"
1.555 +lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
1.556 +  by (rule ceiling_le_zero) (* already declared [simp] *)
1.557
1.558 -lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)"
1.560 +lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
1.561 +  by (rule ceiling_le_one) (* already declared [simp] *)
1.562
1.563  lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
1.564 -  apply (subst linorder_not_le [THEN sym])+
1.565 -  apply simp
1.566 -  apply (rule ceiling_le_eq)
1.567 -done
1.568 +  unfolding real_of_int_def by (rule less_ceiling_iff)
1.569
1.570 -lemma less_ceiling_eq_number_of [simp]:
1.571 +lemma less_ceiling_eq_number_of:
1.572      "(number_of n < ceiling x) = (number_of n < x)"
1.574 +  by (rule number_of_less_ceiling) (* already declared [simp] *)
1.575
1.576 -lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
1.578 +lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
1.579 +  by (rule zero_less_ceiling) (* already declared [simp] *)
1.580
1.581 -lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
1.583 +lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
1.584 +  by (rule one_less_ceiling) (* already declared [simp] *)
1.585
1.586  lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
1.587 -  apply (insert ceiling_le_eq [of x "a - 1"])
1.588 -  apply auto
1.589 -done
1.590 +  unfolding real_of_int_def by (rule ceiling_less_iff)
1.591
1.592 -lemma ceiling_less_eq_number_of [simp]:
1.593 +lemma ceiling_less_eq_number_of:
1.594      "(ceiling x < number_of n) = (x <= number_of n - 1)"
1.596 +  by (rule ceiling_less_number_of) (* already declared [simp] *)
1.597
1.598 -lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
1.600 +lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
1.601 +  by (rule ceiling_less_zero) (* already declared [simp] *)
1.602
1.603 -lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
1.605 +lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
1.606 +  by (rule ceiling_less_one) (* already declared [simp] *)
1.607
1.608  lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
1.609 -  apply (insert less_ceiling_eq [of "a - 1" x])
1.610 -  apply auto
1.611 -done
1.612 +  unfolding real_of_int_def by (rule le_ceiling_iff)
1.613
1.614 -lemma le_ceiling_eq_number_of [simp]:
1.615 +lemma le_ceiling_eq_number_of:
1.616      "(number_of n <= ceiling x) = (number_of n - 1 < x)"
1.618 +  by (rule number_of_le_ceiling) (* already declared [simp] *)
1.619
1.620 -lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
1.622 +lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
1.623 +  by (rule zero_le_ceiling) (* already declared [simp] *)
1.624
1.625 -lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
1.627 +lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
1.628 +  by (rule one_le_ceiling) (* already declared [simp] *)
1.629
1.630  lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
1.631 -  apply (unfold ceiling_def, simp)
1.632 -  apply (subst real_of_int_minus [THEN sym])
1.634 -  apply simp
1.635 -done
1.636 -
1.637 -lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) =
1.638 -    ceiling x + number_of n"
1.639 -  apply (subst ceiling_add [THEN sym])
1.640 -  apply simp
1.641 -done
1.642 -
1.643 -lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
1.644 -  apply (subst ceiling_add [THEN sym])
1.645 -  apply simp
1.646 -done
1.647 +  unfolding real_of_int_def by (rule ceiling_add_of_int)
1.648
1.649  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
1.650 -  apply (subst diff_minus)+
1.651 -  apply (subst real_of_int_minus [THEN sym])
1.653 -done
1.654 +  unfolding real_of_int_def by (rule ceiling_diff_of_int)
1.655
1.656 -lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) =
1.657 +lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
1.658      ceiling x - number_of n"
1.659 -  apply (subst ceiling_subtract [THEN sym])
1.660 -  apply simp
1.661 -done
1.662 +  by (rule ceiling_diff_number_of) (* already declared [simp] *)
1.663
1.664 -lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
1.665 -  apply (subst ceiling_subtract [THEN sym])
1.666 -  apply simp
1.667 -done
1.668 +lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
1.669 +  by (rule ceiling_diff_one) (* already declared [simp] *)
1.670 +
1.671
1.672  subsection {* Versions for the natural numbers *}
1.673
1.674 @@ -1015,7 +781,7 @@
1.675    apply (unfold natfloor_def)
1.676    apply (subgoal_tac "floor x <= floor 0")
1.677    apply simp
1.678 -  apply (erule floor_mono2)
1.679 +  apply (erule floor_mono)
1.680  done
1.681
1.682  lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
1.683 @@ -1023,7 +789,7 @@
1.684    apply (subst natfloor_def)+
1.685    apply (subst nat_le_eq_zle)
1.686    apply force
1.687 -  apply (erule floor_mono2)
1.688 +  apply (erule floor_mono)
1.689    apply (subst natfloor_neg)
1.690    apply simp
1.691    apply simp
1.692 @@ -1144,7 +910,7 @@
1.693    apply (subst real_nat_eq_real)
1.694    apply (subgoal_tac "ceiling 0 <= ceiling x")
1.695    apply simp
1.696 -  apply (rule ceiling_mono2)
1.697 +  apply (rule ceiling_mono)
1.698    apply simp
1.699    apply simp
1.700  done
1.701 @@ -1165,7 +931,7 @@
1.702    apply simp
1.703    apply (erule order_trans)
1.704    apply simp
1.705 -  apply (erule ceiling_mono2)
1.706 +  apply (erule ceiling_mono)
1.707    apply (subst natceiling_neg)
1.708    apply simp_all
1.709  done
1.710 @@ -1215,7 +981,7 @@
1.711    apply (subst eq_nat_nat_iff)
1.712    apply (subgoal_tac "ceiling 0 <= ceiling x")
1.713    apply simp
1.714 -  apply (rule ceiling_mono2)
1.715 +  apply (rule ceiling_mono)
1.716    apply force
1.717    apply force
1.718    apply (rule ceiling_eq2)
1.719 @@ -1233,7 +999,7 @@