generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
authorhuffman
Wed Feb 25 11:29:59 2009 -0800 (2009-02-25)
changeset 3009757df8626c23b
parent 30096 c5497842ee35
child 30098 896fed07349e
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
src/HOL/Decision_Procs/MIR.thy
src/HOL/RComplete.thy
src/HOL/Rational.thy
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Feb 25 11:26:01 2009 -0800
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Feb 25 11:29:59 2009 -0800
     1.3 @@ -83,7 +83,7 @@
     1.4    have "real (floor x) \<le> x" by simp 
     1.5    hence "real (floor x) < real (n + 1) " using ub by arith
     1.6    hence "floor x < n+1" by simp
     1.7 -  moreover from lb have "n \<le> floor x" using floor_mono2[where x="real n" and y="x"] 
     1.8 +  moreover from lb have "n \<le> floor x" using floor_mono[where x="real n" and y="x"] 
     1.9      by simp ultimately show "floor x = n" by simp
    1.10  qed
    1.11  
    1.12 @@ -1775,11 +1775,11 @@
    1.13    "(real (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real (floor b) < b))"
    1.14  proof( auto)
    1.15    assume alb: "real a \<le> b" and agb: "\<not> a \<le> floor b"
    1.16 -  from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono2) 
    1.17 +  from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono) 
    1.18    hence "a \<le> floor b" by simp with agb show "False" by simp
    1.19  next
    1.20    assume alb: "a \<le> floor b"
    1.21 -  hence "real a \<le> real (floor b)" by (simp only: floor_mono2)
    1.22 +  hence "real a \<le> real (floor b)" by (simp only: floor_mono)
    1.23    also have "\<dots>\<le> b" by simp  finally show  "real a \<le> b" . 
    1.24  qed
    1.25  
    1.26 @@ -3697,7 +3697,7 @@
    1.27    assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
    1.28    shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j")
    1.29  by (rule bexI[where P="?P" and x="floor x" and A="?N"]) 
    1.30 -(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono2[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
    1.31 +(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
    1.32  
    1.33  lemma rsplit0_complete:
    1.34    assumes xp:"0 \<le> x" and x1:"x < 1"
     2.1 --- a/src/HOL/RComplete.thy	Wed Feb 25 11:26:01 2009 -0800
     2.2 +++ b/src/HOL/RComplete.thy	Wed Feb 25 11:29:59 2009 -0800
     2.3 @@ -380,33 +380,28 @@
     2.4    thus "\<exists>(n::nat). x < real n" ..
     2.5  qed
     2.6  
     2.7 +instance real :: archimedean_field
     2.8 +proof
     2.9 +  fix r :: real
    2.10 +  obtain n :: nat where "r < real n"
    2.11 +    using reals_Archimedean2 ..
    2.12 +  then have "r \<le> of_int (int n)"
    2.13 +    unfolding real_eq_of_nat by simp
    2.14 +  then show "\<exists>z. r \<le> of_int z" ..
    2.15 +qed
    2.16 +
    2.17  lemma reals_Archimedean3:
    2.18    assumes x_greater_zero: "0 < x"
    2.19    shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
    2.20 -proof
    2.21 -  fix y
    2.22 -  have x_not_zero: "x \<noteq> 0" using x_greater_zero by simp
    2.23 -  obtain n where "y * inverse x < real (n::nat)"
    2.24 -    using reals_Archimedean2 ..
    2.25 -  hence "y * inverse x * x < real n * x"
    2.26 -    using x_greater_zero by (simp add: mult_strict_right_mono)
    2.27 -  hence "x * inverse x * y < x * real n"
    2.28 -    by (simp add: algebra_simps)
    2.29 -  hence "y < real (n::nat) * x"
    2.30 -    using x_not_zero by (simp add: algebra_simps)
    2.31 -  thus "\<exists>(n::nat). y < real n * x" ..
    2.32 -qed
    2.33 +  unfolding real_of_nat_def using `0 < x`
    2.34 +  by (auto intro: ex_less_of_nat_mult)
    2.35  
    2.36  lemma reals_Archimedean6:
    2.37       "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
    2.38 -apply (insert reals_Archimedean2 [of r], safe)
    2.39 -apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto)
    2.40 -apply (rule_tac x = x in exI)
    2.41 -apply (case_tac x, simp)
    2.42 -apply (rename_tac x')
    2.43 -apply (drule_tac x = x' in spec, simp)
    2.44 -apply (rule_tac x="LEAST n. r < real n" in exI, safe)
    2.45 -apply (erule LeastI, erule Least_le)
    2.46 +unfolding real_of_nat_def
    2.47 +apply (rule exI [where x="nat (floor r + 1)"])
    2.48 +apply (insert floor_correct [of r])
    2.49 +apply (simp add: nat_add_distrib of_nat_nat)
    2.50  done
    2.51  
    2.52  lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
    2.53 @@ -414,19 +409,11 @@
    2.54  
    2.55  lemma reals_Archimedean_6b_int:
    2.56       "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    2.57 -apply (drule reals_Archimedean6a, auto)
    2.58 -apply (rule_tac x = "int n" in exI)
    2.59 -apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
    2.60 -done
    2.61 +  unfolding real_of_int_def by (rule floor_exists)
    2.62  
    2.63  lemma reals_Archimedean_6c_int:
    2.64       "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    2.65 -apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
    2.66 -apply (rename_tac n)
    2.67 -apply (drule order_le_imp_less_or_eq, auto)
    2.68 -apply (rule_tac x = "- n - 1" in exI)
    2.69 -apply (rule_tac [2] x = "- n" in exI, auto)
    2.70 -done
    2.71 +  unfolding real_of_int_def by (rule floor_exists)
    2.72  
    2.73  
    2.74  subsection{*Density of the Rational Reals in the Reals*}
    2.75 @@ -485,23 +472,6 @@
    2.76  
    2.77  subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
    2.78  
    2.79 -definition
    2.80 -  floor :: "real => int" where
    2.81 -  [code del]: "floor r = (LEAST n::int. r < real (n+1))"
    2.82 -
    2.83 -definition
    2.84 -  ceiling :: "real => int" where
    2.85 -  "ceiling r = - floor (- r)"
    2.86 -
    2.87 -notation (xsymbols)
    2.88 -  floor  ("\<lfloor>_\<rfloor>") and
    2.89 -  ceiling  ("\<lceil>_\<rceil>")
    2.90 -
    2.91 -notation (HTML output)
    2.92 -  floor  ("\<lfloor>_\<rfloor>") and
    2.93 -  ceiling  ("\<lceil>_\<rceil>")
    2.94 -
    2.95 -
    2.96  lemma number_of_less_real_of_int_iff [simp]:
    2.97       "((number_of n) < real (m::int)) = (number_of n < m)"
    2.98  apply auto
    2.99 @@ -524,51 +494,23 @@
   2.100       "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
   2.101  by (simp add: linorder_not_less [symmetric])
   2.102  
   2.103 -lemma floor_zero [simp]: "floor 0 = 0"
   2.104 -apply (simp add: floor_def del: real_of_int_add)
   2.105 -apply (rule Least_equality)
   2.106 -apply simp_all
   2.107 -done
   2.108 -
   2.109 -lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
   2.110 -by auto
   2.111 +lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
   2.112 +by auto (* delete? *)
   2.113  
   2.114  lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
   2.115 -apply (simp only: floor_def)
   2.116 -apply (rule Least_equality)
   2.117 -apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
   2.118 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
   2.119 -apply simp_all
   2.120 -done
   2.121 +unfolding real_of_nat_def by simp
   2.122  
   2.123  lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
   2.124 -apply (simp only: floor_def)
   2.125 -apply (rule Least_equality)
   2.126 -apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
   2.127 -apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
   2.128 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
   2.129 -apply simp_all
   2.130 -done
   2.131 +unfolding real_of_nat_def by simp
   2.132  
   2.133  lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
   2.134 -apply (simp only: floor_def)
   2.135 -apply (rule Least_equality)
   2.136 -apply auto
   2.137 -done
   2.138 +unfolding real_of_int_def by simp
   2.139  
   2.140  lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
   2.141 -apply (simp only: floor_def)
   2.142 -apply (rule Least_equality)
   2.143 -apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
   2.144 -apply auto
   2.145 -done
   2.146 +unfolding real_of_int_def by simp
   2.147  
   2.148  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
   2.149 -apply (case_tac "r < 0")
   2.150 -apply (blast intro: reals_Archimedean_6c_int)
   2.151 -apply (simp only: linorder_not_less)
   2.152 -apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
   2.153 -done
   2.154 +unfolding real_of_int_def by (rule floor_exists)
   2.155  
   2.156  lemma lemma_floor:
   2.157    assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   2.158 @@ -581,48 +523,20 @@
   2.159  qed
   2.160  
   2.161  lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   2.162 -apply (simp add: floor_def Least_def)
   2.163 -apply (insert real_lb_ub_int [of r], safe)
   2.164 -apply (rule theI2)
   2.165 -apply auto
   2.166 -done
   2.167 -
   2.168 -lemma floor_mono: "x < y ==> floor x \<le> floor y"
   2.169 -apply (simp add: floor_def Least_def)
   2.170 -apply (insert real_lb_ub_int [of x])
   2.171 -apply (insert real_lb_ub_int [of y], safe)
   2.172 -apply (rule theI2)
   2.173 -apply (rule_tac [3] theI2)
   2.174 -apply simp
   2.175 -apply (erule conjI)
   2.176 -apply (auto simp add: order_eq_iff int_le_real_less)
   2.177 -done
   2.178 -
   2.179 -lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
   2.180 -by (auto dest: order_le_imp_less_or_eq simp add: floor_mono)
   2.181 +unfolding real_of_int_def by (rule of_int_floor_le)
   2.182  
   2.183  lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
   2.184  by (auto intro: lemma_floor)
   2.185  
   2.186  lemma real_of_int_floor_cancel [simp]:
   2.187      "(real (floor x) = x) = (\<exists>n::int. x = real n)"
   2.188 -apply (simp add: floor_def Least_def)
   2.189 -apply (insert real_lb_ub_int [of x], erule exE)
   2.190 -apply (rule theI2)
   2.191 -apply (auto intro: lemma_floor)
   2.192 -done
   2.193 +  using floor_real_of_int by metis
   2.194  
   2.195  lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   2.196 -apply (simp add: floor_def)
   2.197 -apply (rule Least_equality)
   2.198 -apply (auto intro: lemma_floor)
   2.199 -done
   2.200 +  unfolding real_of_int_def using floor_unique [of n x] by simp
   2.201  
   2.202  lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
   2.203 -apply (simp add: floor_def)
   2.204 -apply (rule Least_equality)
   2.205 -apply (auto intro: lemma_floor)
   2.206 -done
   2.207 +  unfolding real_of_int_def by (rule floor_unique)
   2.208  
   2.209  lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   2.210  apply (rule inj_int [THEN injD])
   2.211 @@ -635,353 +549,205 @@
   2.212  apply (auto intro: floor_eq3)
   2.213  done
   2.214  
   2.215 -lemma floor_number_of_eq [simp]:
   2.216 +lemma floor_number_of_eq:
   2.217       "floor(number_of n :: real) = (number_of n :: int)"
   2.218 -apply (subst real_number_of [symmetric])
   2.219 -apply (rule floor_real_of_int)
   2.220 -done
   2.221 -
   2.222 -lemma floor_one [simp]: "floor 1 = 1"
   2.223 -  apply (rule trans)
   2.224 -  prefer 2
   2.225 -  apply (rule floor_real_of_int)
   2.226 -  apply simp
   2.227 -done
   2.228 +  by (rule floor_number_of) (* already declared [simp] *)
   2.229  
   2.230  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   2.231 -apply (simp add: floor_def Least_def)
   2.232 -apply (insert real_lb_ub_int [of r], safe)
   2.233 -apply (rule theI2)
   2.234 -apply (auto intro: lemma_floor)
   2.235 -done
   2.236 +  unfolding real_of_int_def using floor_correct [of r] by simp
   2.237  
   2.238  lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
   2.239 -apply (simp add: floor_def Least_def)
   2.240 -apply (insert real_lb_ub_int [of r], safe)
   2.241 -apply (rule theI2)
   2.242 -apply (auto intro: lemma_floor)
   2.243 -done
   2.244 +  unfolding real_of_int_def using floor_correct [of r] by simp
   2.245  
   2.246  lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   2.247 -apply (insert real_of_int_floor_ge_diff_one [of r])
   2.248 -apply (auto simp del: real_of_int_floor_ge_diff_one)
   2.249 -done
   2.250 +  unfolding real_of_int_def using floor_correct [of r] by simp
   2.251  
   2.252  lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
   2.253 -apply (insert real_of_int_floor_gt_diff_one [of r])
   2.254 -apply (auto simp del: real_of_int_floor_gt_diff_one)
   2.255 -done
   2.256 +  unfolding real_of_int_def using floor_correct [of r] by simp
   2.257  
   2.258  lemma le_floor: "real a <= x ==> a <= floor x"
   2.259 -  apply (subgoal_tac "a < floor x + 1")
   2.260 -  apply arith
   2.261 -  apply (subst real_of_int_less_iff [THEN sym])
   2.262 -  apply simp
   2.263 -  apply (insert real_of_int_floor_add_one_gt [of x])
   2.264 -  apply arith
   2.265 -done
   2.266 +  unfolding real_of_int_def by (simp add: le_floor_iff)
   2.267  
   2.268  lemma real_le_floor: "a <= floor x ==> real a <= x"
   2.269 -  apply (rule order_trans)
   2.270 -  prefer 2
   2.271 -  apply (rule real_of_int_floor_le)
   2.272 -  apply (subst real_of_int_le_iff)
   2.273 -  apply assumption
   2.274 -done
   2.275 +  unfolding real_of_int_def by (simp add: le_floor_iff)
   2.276  
   2.277  lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
   2.278 -  apply (rule iffI)
   2.279 -  apply (erule real_le_floor)
   2.280 -  apply (erule le_floor)
   2.281 -done
   2.282 +  unfolding real_of_int_def by (rule le_floor_iff)
   2.283  
   2.284 -lemma le_floor_eq_number_of [simp]:
   2.285 +lemma le_floor_eq_number_of:
   2.286      "(number_of n <= floor x) = (number_of n <= x)"
   2.287 -by (simp add: le_floor_eq)
   2.288 +  by (rule number_of_le_floor) (* already declared [simp] *)
   2.289  
   2.290 -lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
   2.291 -by (simp add: le_floor_eq)
   2.292 +lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
   2.293 +  by (rule zero_le_floor) (* already declared [simp] *)
   2.294  
   2.295 -lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
   2.296 -by (simp add: le_floor_eq)
   2.297 +lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
   2.298 +  by (rule one_le_floor) (* already declared [simp] *)
   2.299  
   2.300  lemma floor_less_eq: "(floor x < a) = (x < real a)"
   2.301 -  apply (subst linorder_not_le [THEN sym])+
   2.302 -  apply simp
   2.303 -  apply (rule le_floor_eq)
   2.304 -done
   2.305 +  unfolding real_of_int_def by (rule floor_less_iff)
   2.306  
   2.307 -lemma floor_less_eq_number_of [simp]:
   2.308 +lemma floor_less_eq_number_of:
   2.309      "(floor x < number_of n) = (x < number_of n)"
   2.310 -by (simp add: floor_less_eq)
   2.311 +  by (rule floor_less_number_of) (* already declared [simp] *)
   2.312  
   2.313 -lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
   2.314 -by (simp add: floor_less_eq)
   2.315 +lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
   2.316 +  by (rule floor_less_zero) (* already declared [simp] *)
   2.317  
   2.318 -lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
   2.319 -by (simp add: floor_less_eq)
   2.320 +lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
   2.321 +  by (rule floor_less_one) (* already declared [simp] *)
   2.322  
   2.323  lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
   2.324 -  apply (insert le_floor_eq [of "a + 1" x])
   2.325 -  apply auto
   2.326 -done
   2.327 +  unfolding real_of_int_def by (rule less_floor_iff)
   2.328  
   2.329 -lemma less_floor_eq_number_of [simp]:
   2.330 +lemma less_floor_eq_number_of:
   2.331      "(number_of n < floor x) = (number_of n + 1 <= x)"
   2.332 -by (simp add: less_floor_eq)
   2.333 +  by (rule number_of_less_floor) (* already declared [simp] *)
   2.334  
   2.335 -lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
   2.336 -by (simp add: less_floor_eq)
   2.337 +lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
   2.338 +  by (rule zero_less_floor) (* already declared [simp] *)
   2.339  
   2.340 -lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
   2.341 -by (simp add: less_floor_eq)
   2.342 +lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
   2.343 +  by (rule one_less_floor) (* already declared [simp] *)
   2.344  
   2.345  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   2.346 -  apply (insert floor_less_eq [of x "a + 1"])
   2.347 -  apply auto
   2.348 -done
   2.349 +  unfolding real_of_int_def by (rule floor_le_iff)
   2.350  
   2.351 -lemma floor_le_eq_number_of [simp]:
   2.352 +lemma floor_le_eq_number_of:
   2.353      "(floor x <= number_of n) = (x < number_of n + 1)"
   2.354 -by (simp add: floor_le_eq)
   2.355 +  by (rule floor_le_number_of) (* already declared [simp] *)
   2.356  
   2.357 -lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
   2.358 -by (simp add: floor_le_eq)
   2.359 +lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
   2.360 +  by (rule floor_le_zero) (* already declared [simp] *)
   2.361  
   2.362 -lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
   2.363 -by (simp add: floor_le_eq)
   2.364 +lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
   2.365 +  by (rule floor_le_one) (* already declared [simp] *)
   2.366  
   2.367  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   2.368 -  apply (subst order_eq_iff)
   2.369 -  apply (rule conjI)
   2.370 -  prefer 2
   2.371 -  apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
   2.372 -  apply arith
   2.373 -  apply (subst real_of_int_less_iff [THEN sym])
   2.374 -  apply simp
   2.375 -  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
   2.376 -  apply (subgoal_tac "real (floor x) <= x")
   2.377 -  apply arith
   2.378 -  apply (rule real_of_int_floor_le)
   2.379 -  apply (rule real_of_int_floor_add_one_gt)
   2.380 -  apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
   2.381 -  apply arith
   2.382 -  apply (subst real_of_int_less_iff [THEN sym])
   2.383 -  apply simp
   2.384 -  apply (subgoal_tac "real(floor(x + real a)) <= x + real a")
   2.385 -  apply (subgoal_tac "x < real(floor x) + 1")
   2.386 -  apply arith
   2.387 -  apply (rule real_of_int_floor_add_one_gt)
   2.388 -  apply (rule real_of_int_floor_le)
   2.389 -done
   2.390 -
   2.391 -lemma floor_add_number_of [simp]:
   2.392 -    "floor (x + number_of n) = floor x + number_of n"
   2.393 -  apply (subst floor_add [THEN sym])
   2.394 -  apply simp
   2.395 -done
   2.396 -
   2.397 -lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   2.398 -  apply (subst floor_add [THEN sym])
   2.399 -  apply simp
   2.400 -done
   2.401 +  unfolding real_of_int_def by (rule floor_add_of_int)
   2.402  
   2.403  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   2.404 -  apply (subst diff_minus)+
   2.405 -  apply (subst real_of_int_minus [THEN sym])
   2.406 -  apply (rule floor_add)
   2.407 -done
   2.408 +  unfolding real_of_int_def by (rule floor_diff_of_int)
   2.409  
   2.410 -lemma floor_subtract_number_of [simp]: "floor (x - number_of n) =
   2.411 +lemma floor_subtract_number_of: "floor (x - number_of n) =
   2.412      floor x - number_of n"
   2.413 -  apply (subst floor_subtract [THEN sym])
   2.414 -  apply simp
   2.415 -done
   2.416 +  by (rule floor_diff_number_of) (* already declared [simp] *)
   2.417  
   2.418 -lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
   2.419 -  apply (subst floor_subtract [THEN sym])
   2.420 -  apply simp
   2.421 -done
   2.422 -
   2.423 -lemma ceiling_zero [simp]: "ceiling 0 = 0"
   2.424 -by (simp add: ceiling_def)
   2.425 +lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
   2.426 +  by (rule floor_diff_one) (* already declared [simp] *)
   2.427  
   2.428  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   2.429 -by (simp add: ceiling_def)
   2.430 +  unfolding real_of_nat_def by simp
   2.431  
   2.432 -lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
   2.433 -by auto
   2.434 +lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
   2.435 +by auto (* delete? *)
   2.436  
   2.437  lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
   2.438 -by (simp add: ceiling_def)
   2.439 +  unfolding real_of_int_def by simp
   2.440  
   2.441  lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
   2.442 -by (simp add: ceiling_def)
   2.443 +  unfolding real_of_int_def by simp
   2.444  
   2.445  lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   2.446 -apply (simp add: ceiling_def)
   2.447 -apply (subst le_minus_iff, simp)
   2.448 -done
   2.449 +  unfolding real_of_int_def by (rule le_of_int_ceiling)
   2.450  
   2.451 -lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
   2.452 -by (simp add: floor_mono ceiling_def)
   2.453 -
   2.454 -lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
   2.455 -by (simp add: floor_mono2 ceiling_def)
   2.456 +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   2.457 +  unfolding real_of_int_def by simp
   2.458  
   2.459  lemma real_of_int_ceiling_cancel [simp]:
   2.460       "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   2.461 -apply (auto simp add: ceiling_def)
   2.462 -apply (drule arg_cong [where f = uminus], auto)
   2.463 -apply (rule_tac x = "-n" in exI, auto)
   2.464 -done
   2.465 +  using ceiling_real_of_int by metis
   2.466  
   2.467  lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   2.468 -apply (simp add: ceiling_def)
   2.469 -apply (rule minus_equation_iff [THEN iffD1])
   2.470 -apply (simp add: floor_eq [where n = "-(n+1)"])
   2.471 -done
   2.472 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   2.473  
   2.474  lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   2.475 -by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
   2.476 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   2.477  
   2.478  lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   2.479 -by (simp add: ceiling_def floor_eq2 [where n = "-n"])
   2.480 +  unfolding real_of_int_def using ceiling_unique [of n x] by simp
   2.481  
   2.482 -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   2.483 -by (simp add: ceiling_def)
   2.484 -
   2.485 -lemma ceiling_number_of_eq [simp]:
   2.486 +lemma ceiling_number_of_eq:
   2.487       "ceiling (number_of n :: real) = (number_of n)"
   2.488 -apply (subst real_number_of [symmetric])
   2.489 -apply (rule ceiling_real_of_int)
   2.490 -done
   2.491 -
   2.492 -lemma ceiling_one [simp]: "ceiling 1 = 1"
   2.493 -  by (unfold ceiling_def, simp)
   2.494 +  by (rule ceiling_number_of) (* already declared [simp] *)
   2.495  
   2.496  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   2.497 -apply (rule neg_le_iff_le [THEN iffD1])
   2.498 -apply (simp add: ceiling_def diff_minus)
   2.499 -done
   2.500 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
   2.501  
   2.502  lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   2.503 -apply (insert real_of_int_ceiling_diff_one_le [of r])
   2.504 -apply (simp del: real_of_int_ceiling_diff_one_le)
   2.505 -done
   2.506 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
   2.507  
   2.508  lemma ceiling_le: "x <= real a ==> ceiling x <= a"
   2.509 -  apply (unfold ceiling_def)
   2.510 -  apply (subgoal_tac "-a <= floor(- x)")
   2.511 -  apply simp
   2.512 -  apply (rule le_floor)
   2.513 -  apply simp
   2.514 -done
   2.515 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   2.516  
   2.517  lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
   2.518 -  apply (unfold ceiling_def)
   2.519 -  apply (subgoal_tac "real(- a) <= - x")
   2.520 -  apply simp
   2.521 -  apply (rule real_le_floor)
   2.522 -  apply simp
   2.523 -done
   2.524 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   2.525  
   2.526  lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   2.527 -  apply (rule iffI)
   2.528 -  apply (erule ceiling_le_real)
   2.529 -  apply (erule ceiling_le)
   2.530 -done
   2.531 +  unfolding real_of_int_def by (rule ceiling_le_iff)
   2.532  
   2.533 -lemma ceiling_le_eq_number_of [simp]:
   2.534 +lemma ceiling_le_eq_number_of:
   2.535      "(ceiling x <= number_of n) = (x <= number_of n)"
   2.536 -by (simp add: ceiling_le_eq)
   2.537 +  by (rule ceiling_le_number_of) (* already declared [simp] *)
   2.538  
   2.539 -lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)"
   2.540 -by (simp add: ceiling_le_eq)
   2.541 +lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
   2.542 +  by (rule ceiling_le_zero) (* already declared [simp] *)
   2.543  
   2.544 -lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)"
   2.545 -by (simp add: ceiling_le_eq)
   2.546 +lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
   2.547 +  by (rule ceiling_le_one) (* already declared [simp] *)
   2.548  
   2.549  lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   2.550 -  apply (subst linorder_not_le [THEN sym])+
   2.551 -  apply simp
   2.552 -  apply (rule ceiling_le_eq)
   2.553 -done
   2.554 +  unfolding real_of_int_def by (rule less_ceiling_iff)
   2.555  
   2.556 -lemma less_ceiling_eq_number_of [simp]:
   2.557 +lemma less_ceiling_eq_number_of:
   2.558      "(number_of n < ceiling x) = (number_of n < x)"
   2.559 -by (simp add: less_ceiling_eq)
   2.560 +  by (rule number_of_less_ceiling) (* already declared [simp] *)
   2.561  
   2.562 -lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
   2.563 -by (simp add: less_ceiling_eq)
   2.564 +lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
   2.565 +  by (rule zero_less_ceiling) (* already declared [simp] *)
   2.566  
   2.567 -lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
   2.568 -by (simp add: less_ceiling_eq)
   2.569 +lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
   2.570 +  by (rule one_less_ceiling) (* already declared [simp] *)
   2.571  
   2.572  lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   2.573 -  apply (insert ceiling_le_eq [of x "a - 1"])
   2.574 -  apply auto
   2.575 -done
   2.576 +  unfolding real_of_int_def by (rule ceiling_less_iff)
   2.577  
   2.578 -lemma ceiling_less_eq_number_of [simp]:
   2.579 +lemma ceiling_less_eq_number_of:
   2.580      "(ceiling x < number_of n) = (x <= number_of n - 1)"
   2.581 -by (simp add: ceiling_less_eq)
   2.582 +  by (rule ceiling_less_number_of) (* already declared [simp] *)
   2.583  
   2.584 -lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
   2.585 -by (simp add: ceiling_less_eq)
   2.586 +lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
   2.587 +  by (rule ceiling_less_zero) (* already declared [simp] *)
   2.588  
   2.589 -lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
   2.590 -by (simp add: ceiling_less_eq)
   2.591 +lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
   2.592 +  by (rule ceiling_less_one) (* already declared [simp] *)
   2.593  
   2.594  lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   2.595 -  apply (insert less_ceiling_eq [of "a - 1" x])
   2.596 -  apply auto
   2.597 -done
   2.598 +  unfolding real_of_int_def by (rule le_ceiling_iff)
   2.599  
   2.600 -lemma le_ceiling_eq_number_of [simp]:
   2.601 +lemma le_ceiling_eq_number_of:
   2.602      "(number_of n <= ceiling x) = (number_of n - 1 < x)"
   2.603 -by (simp add: le_ceiling_eq)
   2.604 +  by (rule number_of_le_ceiling) (* already declared [simp] *)
   2.605  
   2.606 -lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
   2.607 -by (simp add: le_ceiling_eq)
   2.608 +lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
   2.609 +  by (rule zero_le_ceiling) (* already declared [simp] *)
   2.610  
   2.611 -lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
   2.612 -by (simp add: le_ceiling_eq)
   2.613 +lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
   2.614 +  by (rule one_le_ceiling) (* already declared [simp] *)
   2.615  
   2.616  lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   2.617 -  apply (unfold ceiling_def, simp)
   2.618 -  apply (subst real_of_int_minus [THEN sym])
   2.619 -  apply (subst floor_add)
   2.620 -  apply simp
   2.621 -done
   2.622 -
   2.623 -lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) =
   2.624 -    ceiling x + number_of n"
   2.625 -  apply (subst ceiling_add [THEN sym])
   2.626 -  apply simp
   2.627 -done
   2.628 -
   2.629 -lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   2.630 -  apply (subst ceiling_add [THEN sym])
   2.631 -  apply simp
   2.632 -done
   2.633 +  unfolding real_of_int_def by (rule ceiling_add_of_int)
   2.634  
   2.635  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   2.636 -  apply (subst diff_minus)+
   2.637 -  apply (subst real_of_int_minus [THEN sym])
   2.638 -  apply (rule ceiling_add)
   2.639 -done
   2.640 +  unfolding real_of_int_def by (rule ceiling_diff_of_int)
   2.641  
   2.642 -lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) =
   2.643 +lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
   2.644      ceiling x - number_of n"
   2.645 -  apply (subst ceiling_subtract [THEN sym])
   2.646 -  apply simp
   2.647 -done
   2.648 +  by (rule ceiling_diff_number_of) (* already declared [simp] *)
   2.649  
   2.650 -lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   2.651 -  apply (subst ceiling_subtract [THEN sym])
   2.652 -  apply simp
   2.653 -done
   2.654 +lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
   2.655 +  by (rule ceiling_diff_one) (* already declared [simp] *)
   2.656 +
   2.657  
   2.658  subsection {* Versions for the natural numbers *}
   2.659  
   2.660 @@ -1015,7 +781,7 @@
   2.661    apply (unfold natfloor_def)
   2.662    apply (subgoal_tac "floor x <= floor 0")
   2.663    apply simp
   2.664 -  apply (erule floor_mono2)
   2.665 +  apply (erule floor_mono)
   2.666  done
   2.667  
   2.668  lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   2.669 @@ -1023,7 +789,7 @@
   2.670    apply (subst natfloor_def)+
   2.671    apply (subst nat_le_eq_zle)
   2.672    apply force
   2.673 -  apply (erule floor_mono2)
   2.674 +  apply (erule floor_mono)
   2.675    apply (subst natfloor_neg)
   2.676    apply simp
   2.677    apply simp
   2.678 @@ -1144,7 +910,7 @@
   2.679    apply (subst real_nat_eq_real)
   2.680    apply (subgoal_tac "ceiling 0 <= ceiling x")
   2.681    apply simp
   2.682 -  apply (rule ceiling_mono2)
   2.683 +  apply (rule ceiling_mono)
   2.684    apply simp
   2.685    apply simp
   2.686  done
   2.687 @@ -1165,7 +931,7 @@
   2.688    apply simp
   2.689    apply (erule order_trans)
   2.690    apply simp
   2.691 -  apply (erule ceiling_mono2)
   2.692 +  apply (erule ceiling_mono)
   2.693    apply (subst natceiling_neg)
   2.694    apply simp_all
   2.695  done
   2.696 @@ -1215,7 +981,7 @@
   2.697    apply (subst eq_nat_nat_iff)
   2.698    apply (subgoal_tac "ceiling 0 <= ceiling x")
   2.699    apply simp
   2.700 -  apply (rule ceiling_mono2)
   2.701 +  apply (rule ceiling_mono)
   2.702    apply force
   2.703    apply force
   2.704    apply (rule ceiling_eq2)
   2.705 @@ -1233,7 +999,7 @@
   2.706    apply (subst nat_add_distrib)
   2.707    apply (subgoal_tac "0 = ceiling 0")
   2.708    apply (erule ssubst)
   2.709 -  apply (erule ceiling_mono2)
   2.710 +  apply (erule ceiling_mono)
   2.711    apply simp_all
   2.712  done
   2.713  
     3.1 --- a/src/HOL/Rational.thy	Wed Feb 25 11:26:01 2009 -0800
     3.2 +++ b/src/HOL/Rational.thy	Wed Feb 25 11:29:59 2009 -0800
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Rational numbers *}
     3.5  
     3.6  theory Rational
     3.7 -imports GCD
     3.8 +imports GCD Archimedean_Field
     3.9  uses ("Tools/rat_arith.ML")
    3.10  begin
    3.11  
    3.12 @@ -563,6 +563,37 @@
    3.13    by (simp add: One_rat_def mult_le_cancel_right)
    3.14  
    3.15  
    3.16 +subsubsection {* Rationals are an Archimedean field *}
    3.17 +
    3.18 +lemma rat_floor_lemma:
    3.19 +  assumes "0 < b"
    3.20 +  shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
    3.21 +proof -
    3.22 +  have "Fract a b = of_int (a div b) + Fract (a mod b) b"
    3.23 +    using `0 < b` by (simp add: of_int_rat)
    3.24 +  moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
    3.25 +    using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff)
    3.26 +  ultimately show ?thesis by simp
    3.27 +qed
    3.28 +
    3.29 +instance rat :: archimedean_field
    3.30 +proof
    3.31 +  fix r :: rat
    3.32 +  show "\<exists>z. r \<le> of_int z"
    3.33 +  proof (induct r)
    3.34 +    case (Fract a b)
    3.35 +    then have "Fract a b \<le> of_int (a div b + 1)"
    3.36 +      using rat_floor_lemma [of b a] by simp
    3.37 +    then show "\<exists>z. Fract a b \<le> of_int z" ..
    3.38 +  qed
    3.39 +qed
    3.40 +
    3.41 +lemma floor_Fract:
    3.42 +  assumes "0 < b" shows "floor (Fract a b) = a div b"
    3.43 +  using rat_floor_lemma [OF `0 < b`, of a]
    3.44 +  by (simp add: floor_unique)
    3.45 +
    3.46 +
    3.47  subsection {* Arithmetic setup *}
    3.48  
    3.49  use "Tools/rat_arith.ML"