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.63 +apply (simp add: nat_add_distrib of_nat_nat)
    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.118 -apply (simp add: floor_def del: real_of_int_add)
   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.210 -apply (simp add: floor_def)
   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.217 -apply (simp add: floor_def)
   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.301 -by (simp add: le_floor_eq)
   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.305 -by (simp add: le_floor_eq)
   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.310 -by (simp add: le_floor_eq)
   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.324 -by (simp add: floor_less_eq)
   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.328 -by (simp add: floor_less_eq)
   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.333 -by (simp add: floor_less_eq)
   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.346 -by (simp add: less_floor_eq)
   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.350 -by (simp add: less_floor_eq)
   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.355 -by (simp add: less_floor_eq)
   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.368 -by (simp add: floor_le_eq)
   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.372 -by (simp add: floor_le_eq)
   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.377 -by (simp add: floor_le_eq)
   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.393 -  apply (rule real_of_int_floor_add_one_gt)
   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.401 -  apply (rule real_of_int_floor_add_one_gt)
   1.402 -  apply (rule real_of_int_floor_le)
   1.403 -done
   1.404 -
   1.405 -lemma floor_add_number_of [simp]:
   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.420 -  apply (rule floor_add)
   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.438 -by (simp add: ceiling_def)
   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.443 -by (simp add: ceiling_def)
   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.452 -by (simp add: ceiling_def)
   1.453 +  unfolding real_of_int_def by simp
   1.454  
   1.455  lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
   1.456 -by (simp add: ceiling_def)
   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.460 -apply (simp add: ceiling_def)
   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.482 -apply (simp add: ceiling_def)
   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.497 -by (simp add: ceiling_def)
   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.550 -by (simp add: ceiling_le_eq)
   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.554 -by (simp add: ceiling_le_eq)
   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.559 -by (simp add: ceiling_le_eq)
   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.573 -by (simp add: less_ceiling_eq)
   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.577 -by (simp add: less_ceiling_eq)
   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.582 -by (simp add: less_ceiling_eq)
   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.595 -by (simp add: ceiling_less_eq)
   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.599 -by (simp add: ceiling_less_eq)
   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.604 -by (simp add: ceiling_less_eq)
   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.617 -by (simp add: le_ceiling_eq)
   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.621 -by (simp add: le_ceiling_eq)
   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.626 -by (simp add: le_ceiling_eq)
   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.633 -  apply (subst floor_add)
   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.652 -  apply (rule ceiling_add)
   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 @@
   1.720    apply (subst nat_add_distrib)
   1.721    apply (subgoal_tac "0 = ceiling 0")
   1.722    apply (erule ssubst)
   1.723 -  apply (erule ceiling_mono2)
   1.724 +  apply (erule ceiling_mono)
   1.725    apply simp_all
   1.726  done
   1.727