merge RComplete into RealDef
authorhoelzl
Tue Mar 26 12:20:55 2013 +0100 (2013-03-26)
changeset 5152136fa825e0ea7
parent 51520 e9b361845809
child 51522 bd568f4bf446
merge RComplete into RealDef
src/HOL/Metric_Spaces.thy
src/HOL/NSA/NSA.thy
src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
src/HOL/RComplete.thy
src/HOL/Real.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Metric_Spaces.thy	Tue Mar 26 12:20:54 2013 +0100
     1.2 +++ b/src/HOL/Metric_Spaces.thy	Tue Mar 26 12:20:55 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Metric Spaces *}
     1.5  
     1.6  theory Metric_Spaces
     1.7 -imports RComplete Topological_Spaces
     1.8 +imports RealDef Topological_Spaces
     1.9  begin
    1.10  
    1.11  
     2.1 --- a/src/HOL/NSA/NSA.thy	Tue Mar 26 12:20:54 2013 +0100
     2.2 +++ b/src/HOL/NSA/NSA.thy	Tue Mar 26 12:20:55 2013 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
     2.5  
     2.6  theory NSA
     2.7 -imports HyperDef RComplete
     2.8 +imports HyperDef
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Tue Mar 26 12:20:54 2013 +0100
     3.2 +++ b/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Tue Mar 26 12:20:55 2013 +0100
     3.3 @@ -9,7 +9,6 @@
     3.4  find_unused_assms Divides
     3.5  find_unused_assms GCD
     3.6  find_unused_assms RealDef
     3.7 -find_unused_assms RComplete
     3.8  
     3.9  section {* Set Theory *}
    3.10  
     4.1 --- a/src/HOL/RComplete.thy	Tue Mar 26 12:20:54 2013 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,489 +0,0 @@
     4.4 -(*  Title:      HOL/RComplete.thy
     4.5 -    Author:     Jacques D. Fleuriot, University of Edinburgh
     4.6 -    Author:     Larry Paulson, University of Cambridge
     4.7 -    Author:     Jeremy Avigad, Carnegie Mellon University
     4.8 -    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
     4.9 -*)
    4.10 -
    4.11 -header {* Completeness of the Reals; Floor and Ceiling Functions *}
    4.12 -
    4.13 -theory RComplete
    4.14 -imports RealDef
    4.15 -begin
    4.16 -
    4.17 -subsection {* Completeness of Positive Reals *}
    4.18 -
    4.19 -text {*
    4.20 -  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
    4.21 -*}
    4.22 -
    4.23 -text {*
    4.24 -  \medskip reals Completeness (again!)
    4.25 -*}
    4.26 -
    4.27 -lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
    4.28 -  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
    4.29 -
    4.30 -
    4.31 -subsection {* The Archimedean Property of the Reals *}
    4.32 -
    4.33 -theorem reals_Archimedean:
    4.34 -  assumes x_pos: "0 < x"
    4.35 -  shows "\<exists>n. inverse (real (Suc n)) < x"
    4.36 -  unfolding real_of_nat_def using x_pos
    4.37 -  by (rule ex_inverse_of_nat_Suc_less)
    4.38 -
    4.39 -lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
    4.40 -  unfolding real_of_nat_def by (rule ex_less_of_nat)
    4.41 -
    4.42 -lemma reals_Archimedean3:
    4.43 -  assumes x_greater_zero: "0 < x"
    4.44 -  shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
    4.45 -  unfolding real_of_nat_def using `0 < x`
    4.46 -  by (auto intro: ex_less_of_nat_mult)
    4.47 -
    4.48 -
    4.49 -subsection{*Density of the Rational Reals in the Reals*}
    4.50 -
    4.51 -text{* This density proof is due to Stefan Richter and was ported by TN.  The
    4.52 -original source is \emph{Real Analysis} by H.L. Royden.
    4.53 -It employs the Archimedean property of the reals. *}
    4.54 -
    4.55 -lemma Rats_dense_in_real:
    4.56 -  fixes x :: real
    4.57 -  assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
    4.58 -proof -
    4.59 -  from `x<y` have "0 < y-x" by simp
    4.60 -  with reals_Archimedean obtain q::nat 
    4.61 -    where q: "inverse (real q) < y-x" and "0 < q" by auto
    4.62 -  def p \<equiv> "ceiling (y * real q) - 1"
    4.63 -  def r \<equiv> "of_int p / real q"
    4.64 -  from q have "x < y - inverse (real q)" by simp
    4.65 -  also have "y - inverse (real q) \<le> r"
    4.66 -    unfolding r_def p_def
    4.67 -    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
    4.68 -  finally have "x < r" .
    4.69 -  moreover have "r < y"
    4.70 -    unfolding r_def p_def
    4.71 -    by (simp add: divide_less_eq diff_less_eq `0 < q`
    4.72 -      less_ceiling_iff [symmetric])
    4.73 -  moreover from r_def have "r \<in> \<rat>" by simp
    4.74 -  ultimately show ?thesis by fast
    4.75 -qed
    4.76 -
    4.77 -
    4.78 -subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
    4.79 -
    4.80 -(* FIXME: theorems for negative numerals *)
    4.81 -lemma numeral_less_real_of_int_iff [simp]:
    4.82 -     "((numeral n) < real (m::int)) = (numeral n < m)"
    4.83 -apply auto
    4.84 -apply (rule real_of_int_less_iff [THEN iffD1])
    4.85 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    4.86 -done
    4.87 -
    4.88 -lemma numeral_less_real_of_int_iff2 [simp]:
    4.89 -     "(real (m::int) < (numeral n)) = (m < numeral n)"
    4.90 -apply auto
    4.91 -apply (rule real_of_int_less_iff [THEN iffD1])
    4.92 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    4.93 -done
    4.94 -
    4.95 -lemma numeral_le_real_of_int_iff [simp]:
    4.96 -     "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
    4.97 -by (simp add: linorder_not_less [symmetric])
    4.98 -
    4.99 -lemma numeral_le_real_of_int_iff2 [simp]:
   4.100 -     "(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
   4.101 -by (simp add: linorder_not_less [symmetric])
   4.102 -
   4.103 -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
   4.104 -unfolding real_of_nat_def by simp
   4.105 -
   4.106 -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
   4.107 -unfolding real_of_nat_def by (simp add: floor_minus)
   4.108 -
   4.109 -lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
   4.110 -unfolding real_of_int_def by simp
   4.111 -
   4.112 -lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
   4.113 -unfolding real_of_int_def by (simp add: floor_minus)
   4.114 -
   4.115 -lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
   4.116 -unfolding real_of_int_def by (rule floor_exists)
   4.117 -
   4.118 -lemma lemma_floor:
   4.119 -  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   4.120 -  shows "m \<le> (n::int)"
   4.121 -proof -
   4.122 -  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
   4.123 -  also have "... = real (n + 1)" by simp
   4.124 -  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
   4.125 -  thus ?thesis by arith
   4.126 -qed
   4.127 -
   4.128 -lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   4.129 -unfolding real_of_int_def by (rule of_int_floor_le)
   4.130 -
   4.131 -lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
   4.132 -by (auto intro: lemma_floor)
   4.133 -
   4.134 -lemma real_of_int_floor_cancel [simp]:
   4.135 -    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
   4.136 -  using floor_real_of_int by metis
   4.137 -
   4.138 -lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   4.139 -  unfolding real_of_int_def using floor_unique [of n x] by simp
   4.140 -
   4.141 -lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
   4.142 -  unfolding real_of_int_def by (rule floor_unique)
   4.143 -
   4.144 -lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   4.145 -apply (rule inj_int [THEN injD])
   4.146 -apply (simp add: real_of_nat_Suc)
   4.147 -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
   4.148 -done
   4.149 -
   4.150 -lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   4.151 -apply (drule order_le_imp_less_or_eq)
   4.152 -apply (auto intro: floor_eq3)
   4.153 -done
   4.154 -
   4.155 -lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   4.156 -  unfolding real_of_int_def using floor_correct [of r] by simp
   4.157 -
   4.158 -lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
   4.159 -  unfolding real_of_int_def using floor_correct [of r] by simp
   4.160 -
   4.161 -lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   4.162 -  unfolding real_of_int_def using floor_correct [of r] by simp
   4.163 -
   4.164 -lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
   4.165 -  unfolding real_of_int_def using floor_correct [of r] by simp
   4.166 -
   4.167 -lemma le_floor: "real a <= x ==> a <= floor x"
   4.168 -  unfolding real_of_int_def by (simp add: le_floor_iff)
   4.169 -
   4.170 -lemma real_le_floor: "a <= floor x ==> real a <= x"
   4.171 -  unfolding real_of_int_def by (simp add: le_floor_iff)
   4.172 -
   4.173 -lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
   4.174 -  unfolding real_of_int_def by (rule le_floor_iff)
   4.175 -
   4.176 -lemma floor_less_eq: "(floor x < a) = (x < real a)"
   4.177 -  unfolding real_of_int_def by (rule floor_less_iff)
   4.178 -
   4.179 -lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
   4.180 -  unfolding real_of_int_def by (rule less_floor_iff)
   4.181 -
   4.182 -lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   4.183 -  unfolding real_of_int_def by (rule floor_le_iff)
   4.184 -
   4.185 -lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   4.186 -  unfolding real_of_int_def by (rule floor_add_of_int)
   4.187 -
   4.188 -lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   4.189 -  unfolding real_of_int_def by (rule floor_diff_of_int)
   4.190 -
   4.191 -lemma le_mult_floor:
   4.192 -  assumes "0 \<le> (a :: real)" and "0 \<le> b"
   4.193 -  shows "floor a * floor b \<le> floor (a * b)"
   4.194 -proof -
   4.195 -  have "real (floor a) \<le> a"
   4.196 -    and "real (floor b) \<le> b" by auto
   4.197 -  hence "real (floor a * floor b) \<le> a * b"
   4.198 -    using assms by (auto intro!: mult_mono)
   4.199 -  also have "a * b < real (floor (a * b) + 1)" by auto
   4.200 -  finally show ?thesis unfolding real_of_int_less_iff by simp
   4.201 -qed
   4.202 -
   4.203 -lemma floor_divide_eq_div:
   4.204 -  "floor (real a / real b) = a div b"
   4.205 -proof cases
   4.206 -  assume "b \<noteq> 0 \<or> b dvd a"
   4.207 -  with real_of_int_div3[of a b] show ?thesis
   4.208 -    by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
   4.209 -       (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
   4.210 -              real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
   4.211 -qed (auto simp: real_of_int_div)
   4.212 -
   4.213 -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   4.214 -  unfolding real_of_nat_def by simp
   4.215 -
   4.216 -lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   4.217 -  unfolding real_of_int_def by (rule le_of_int_ceiling)
   4.218 -
   4.219 -lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   4.220 -  unfolding real_of_int_def by simp
   4.221 -
   4.222 -lemma real_of_int_ceiling_cancel [simp]:
   4.223 -     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   4.224 -  using ceiling_real_of_int by metis
   4.225 -
   4.226 -lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   4.227 -  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   4.228 -
   4.229 -lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   4.230 -  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   4.231 -
   4.232 -lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   4.233 -  unfolding real_of_int_def using ceiling_unique [of n x] by simp
   4.234 -
   4.235 -lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   4.236 -  unfolding real_of_int_def using ceiling_correct [of r] by simp
   4.237 -
   4.238 -lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   4.239 -  unfolding real_of_int_def using ceiling_correct [of r] by simp
   4.240 -
   4.241 -lemma ceiling_le: "x <= real a ==> ceiling x <= a"
   4.242 -  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   4.243 -
   4.244 -lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
   4.245 -  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   4.246 -
   4.247 -lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   4.248 -  unfolding real_of_int_def by (rule ceiling_le_iff)
   4.249 -
   4.250 -lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   4.251 -  unfolding real_of_int_def by (rule less_ceiling_iff)
   4.252 -
   4.253 -lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   4.254 -  unfolding real_of_int_def by (rule ceiling_less_iff)
   4.255 -
   4.256 -lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   4.257 -  unfolding real_of_int_def by (rule le_ceiling_iff)
   4.258 -
   4.259 -lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   4.260 -  unfolding real_of_int_def by (rule ceiling_add_of_int)
   4.261 -
   4.262 -lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   4.263 -  unfolding real_of_int_def by (rule ceiling_diff_of_int)
   4.264 -
   4.265 -
   4.266 -subsection {* Versions for the natural numbers *}
   4.267 -
   4.268 -definition
   4.269 -  natfloor :: "real => nat" where
   4.270 -  "natfloor x = nat(floor x)"
   4.271 -
   4.272 -definition
   4.273 -  natceiling :: "real => nat" where
   4.274 -  "natceiling x = nat(ceiling x)"
   4.275 -
   4.276 -lemma natfloor_zero [simp]: "natfloor 0 = 0"
   4.277 -  by (unfold natfloor_def, simp)
   4.278 -
   4.279 -lemma natfloor_one [simp]: "natfloor 1 = 1"
   4.280 -  by (unfold natfloor_def, simp)
   4.281 -
   4.282 -lemma zero_le_natfloor [simp]: "0 <= natfloor x"
   4.283 -  by (unfold natfloor_def, simp)
   4.284 -
   4.285 -lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
   4.286 -  by (unfold natfloor_def, simp)
   4.287 -
   4.288 -lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
   4.289 -  by (unfold natfloor_def, simp)
   4.290 -
   4.291 -lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
   4.292 -  by (unfold natfloor_def, simp)
   4.293 -
   4.294 -lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   4.295 -  unfolding natfloor_def by simp
   4.296 -
   4.297 -lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   4.298 -  unfolding natfloor_def by (intro nat_mono floor_mono)
   4.299 -
   4.300 -lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   4.301 -  apply (unfold natfloor_def)
   4.302 -  apply (subst nat_int [THEN sym])
   4.303 -  apply (rule nat_mono)
   4.304 -  apply (rule le_floor)
   4.305 -  apply simp
   4.306 -done
   4.307 -
   4.308 -lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
   4.309 -  unfolding natfloor_def real_of_nat_def
   4.310 -  by (simp add: nat_less_iff floor_less_iff)
   4.311 -
   4.312 -lemma less_natfloor:
   4.313 -  assumes "0 \<le> x" and "x < real (n :: nat)"
   4.314 -  shows "natfloor x < n"
   4.315 -  using assms by (simp add: natfloor_less_iff)
   4.316 -
   4.317 -lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   4.318 -  apply (rule iffI)
   4.319 -  apply (rule order_trans)
   4.320 -  prefer 2
   4.321 -  apply (erule real_natfloor_le)
   4.322 -  apply (subst real_of_nat_le_iff)
   4.323 -  apply assumption
   4.324 -  apply (erule le_natfloor)
   4.325 -done
   4.326 -
   4.327 -lemma le_natfloor_eq_numeral [simp]:
   4.328 -    "~ neg((numeral n)::int) ==> 0 <= x ==>
   4.329 -      (numeral n <= natfloor x) = (numeral n <= x)"
   4.330 -  apply (subst le_natfloor_eq, assumption)
   4.331 -  apply simp
   4.332 -done
   4.333 -
   4.334 -lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
   4.335 -  apply (case_tac "0 <= x")
   4.336 -  apply (subst le_natfloor_eq, assumption, simp)
   4.337 -  apply (rule iffI)
   4.338 -  apply (subgoal_tac "natfloor x <= natfloor 0")
   4.339 -  apply simp
   4.340 -  apply (rule natfloor_mono)
   4.341 -  apply simp
   4.342 -  apply simp
   4.343 -done
   4.344 -
   4.345 -lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   4.346 -  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
   4.347 -
   4.348 -lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   4.349 -  apply (case_tac "0 <= x")
   4.350 -  apply (unfold natfloor_def)
   4.351 -  apply simp
   4.352 -  apply simp_all
   4.353 -done
   4.354 -
   4.355 -lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
   4.356 -using real_natfloor_add_one_gt by (simp add: algebra_simps)
   4.357 -
   4.358 -lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
   4.359 -  apply (subgoal_tac "z < real(natfloor z) + 1")
   4.360 -  apply arith
   4.361 -  apply (rule real_natfloor_add_one_gt)
   4.362 -done
   4.363 -
   4.364 -lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   4.365 -  unfolding natfloor_def
   4.366 -  unfolding real_of_int_of_nat_eq [symmetric] floor_add
   4.367 -  by (simp add: nat_add_distrib)
   4.368 -
   4.369 -lemma natfloor_add_numeral [simp]:
   4.370 -    "~neg ((numeral n)::int) ==> 0 <= x ==>
   4.371 -      natfloor (x + numeral n) = natfloor x + numeral n"
   4.372 -  by (simp add: natfloor_add [symmetric])
   4.373 -
   4.374 -lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
   4.375 -  by (simp add: natfloor_add [symmetric] del: One_nat_def)
   4.376 -
   4.377 -lemma natfloor_subtract [simp]:
   4.378 -    "natfloor(x - real a) = natfloor x - a"
   4.379 -  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
   4.380 -  by simp
   4.381 -
   4.382 -lemma natfloor_div_nat:
   4.383 -  assumes "1 <= x" and "y > 0"
   4.384 -  shows "natfloor (x / real y) = natfloor x div y"
   4.385 -proof (rule natfloor_eq)
   4.386 -  have "(natfloor x) div y * y \<le> natfloor x"
   4.387 -    by (rule add_leD1 [where k="natfloor x mod y"], simp)
   4.388 -  thus "real (natfloor x div y) \<le> x / real y"
   4.389 -    using assms by (simp add: le_divide_eq le_natfloor_eq)
   4.390 -  have "natfloor x < (natfloor x) div y * y + y"
   4.391 -    apply (subst mod_div_equality [symmetric])
   4.392 -    apply (rule add_strict_left_mono)
   4.393 -    apply (rule mod_less_divisor)
   4.394 -    apply fact
   4.395 -    done
   4.396 -  thus "x / real y < real (natfloor x div y) + 1"
   4.397 -    using assms
   4.398 -    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
   4.399 -qed
   4.400 -
   4.401 -lemma le_mult_natfloor:
   4.402 -  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   4.403 -  by (cases "0 <= a & 0 <= b")
   4.404 -    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
   4.405 -
   4.406 -lemma natceiling_zero [simp]: "natceiling 0 = 0"
   4.407 -  by (unfold natceiling_def, simp)
   4.408 -
   4.409 -lemma natceiling_one [simp]: "natceiling 1 = 1"
   4.410 -  by (unfold natceiling_def, simp)
   4.411 -
   4.412 -lemma zero_le_natceiling [simp]: "0 <= natceiling x"
   4.413 -  by (unfold natceiling_def, simp)
   4.414 -
   4.415 -lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
   4.416 -  by (unfold natceiling_def, simp)
   4.417 -
   4.418 -lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
   4.419 -  by (unfold natceiling_def, simp)
   4.420 -
   4.421 -lemma real_natceiling_ge: "x <= real(natceiling x)"
   4.422 -  unfolding natceiling_def by (cases "x < 0", simp_all)
   4.423 -
   4.424 -lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
   4.425 -  unfolding natceiling_def by simp
   4.426 -
   4.427 -lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   4.428 -  unfolding natceiling_def by (intro nat_mono ceiling_mono)
   4.429 -
   4.430 -lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   4.431 -  unfolding natceiling_def real_of_nat_def
   4.432 -  by (simp add: nat_le_iff ceiling_le_iff)
   4.433 -
   4.434 -lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
   4.435 -  unfolding natceiling_def real_of_nat_def
   4.436 -  by (simp add: nat_le_iff ceiling_le_iff)
   4.437 -
   4.438 -lemma natceiling_le_eq_numeral [simp]:
   4.439 -    "~ neg((numeral n)::int) ==>
   4.440 -      (natceiling x <= numeral n) = (x <= numeral n)"
   4.441 -  by (simp add: natceiling_le_eq)
   4.442 -
   4.443 -lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
   4.444 -  unfolding natceiling_def
   4.445 -  by (simp add: nat_le_iff ceiling_le_iff)
   4.446 -
   4.447 -lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   4.448 -  unfolding natceiling_def
   4.449 -  by (simp add: ceiling_eq2 [where n="int n"])
   4.450 -
   4.451 -lemma natceiling_add [simp]: "0 <= x ==>
   4.452 -    natceiling (x + real a) = natceiling x + a"
   4.453 -  unfolding natceiling_def
   4.454 -  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
   4.455 -  by (simp add: nat_add_distrib)
   4.456 -
   4.457 -lemma natceiling_add_numeral [simp]:
   4.458 -    "~ neg ((numeral n)::int) ==> 0 <= x ==>
   4.459 -      natceiling (x + numeral n) = natceiling x + numeral n"
   4.460 -  by (simp add: natceiling_add [symmetric])
   4.461 -
   4.462 -lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
   4.463 -  by (simp add: natceiling_add [symmetric] del: One_nat_def)
   4.464 -
   4.465 -lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
   4.466 -  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   4.467 -  by simp
   4.468 -
   4.469 -subsection {* Exponentiation with floor *}
   4.470 -
   4.471 -lemma floor_power:
   4.472 -  assumes "x = real (floor x)"
   4.473 -  shows "floor (x ^ n) = floor x ^ n"
   4.474 -proof -
   4.475 -  have *: "x ^ n = real (floor x ^ n)"
   4.476 -    using assms by (induct n arbitrary: x) simp_all
   4.477 -  show ?thesis unfolding real_of_int_inject[symmetric]
   4.478 -    unfolding * floor_real_of_int ..
   4.479 -qed
   4.480 -
   4.481 -lemma natfloor_power:
   4.482 -  assumes "x = real (natfloor x)"
   4.483 -  shows "natfloor (x ^ n) = natfloor x ^ n"
   4.484 -proof -
   4.485 -  from assms have "0 \<le> floor x" by auto
   4.486 -  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
   4.487 -  from floor_power[OF this]
   4.488 -  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
   4.489 -    by simp
   4.490 -qed
   4.491 -
   4.492 -end
     5.1 --- a/src/HOL/Real.thy	Tue Mar 26 12:20:54 2013 +0100
     5.2 +++ b/src/HOL/Real.thy	Tue Mar 26 12:20:55 2013 +0100
     5.3 @@ -1,5 +1,5 @@
     5.4  theory Real
     5.5 -imports RComplete RealVector
     5.6 +imports RealVector
     5.7  begin
     5.8  
     5.9  ML_file "Tools/SMT/smt_real.ML"
     6.1 --- a/src/HOL/RealDef.thy	Tue Mar 26 12:20:54 2013 +0100
     6.2 +++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:55 2013 +0100
     6.3 @@ -1,5 +1,8 @@
     6.4 -(*  Title       : HOL/RealDef.thy
     6.5 -    Author      : Jacques D. Fleuriot, 1998
     6.6 +(*  Title:      HOL/RealDef.thy
     6.7 +    Author:     Jacques D. Fleuriot, University of Edinburgh, 1998
     6.8 +    Author:     Larry Paulson, University of Cambridge
     6.9 +    Author:     Jeremy Avigad, Carnegie Mellon University
    6.10 +    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
    6.11      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    6.12      Construction of Cauchy Reals by Brian Huffman, 2010
    6.13  *)
    6.14 @@ -970,6 +973,13 @@
    6.15  qed
    6.16  end
    6.17  
    6.18 +text {*
    6.19 +  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
    6.20 +*}
    6.21 +
    6.22 +lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
    6.23 +  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper)
    6.24 +
    6.25  
    6.26  subsection {* Hiding implementation details *}
    6.27  
    6.28 @@ -1323,6 +1333,23 @@
    6.29  lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
    6.30  unfolding real_of_nat_def by (rule Ints_of_nat)
    6.31  
    6.32 +subsection {* The Archimedean Property of the Reals *}
    6.33 +
    6.34 +theorem reals_Archimedean:
    6.35 +  assumes x_pos: "0 < x"
    6.36 +  shows "\<exists>n. inverse (real (Suc n)) < x"
    6.37 +  unfolding real_of_nat_def using x_pos
    6.38 +  by (rule ex_inverse_of_nat_Suc_less)
    6.39 +
    6.40 +lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
    6.41 +  unfolding real_of_nat_def by (rule ex_less_of_nat)
    6.42 +
    6.43 +lemma reals_Archimedean3:
    6.44 +  assumes x_greater_zero: "0 < x"
    6.45 +  shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
    6.46 +  unfolding real_of_nat_def using `0 < x`
    6.47 +  by (auto intro: ex_less_of_nat_mult)
    6.48 +
    6.49  
    6.50  subsection{* Rationals *}
    6.51  
    6.52 @@ -1412,6 +1439,35 @@
    6.53    ultimately show ?thesis ..
    6.54  qed
    6.55  
    6.56 +subsection{*Density of the Rational Reals in the Reals*}
    6.57 +
    6.58 +text{* This density proof is due to Stefan Richter and was ported by TN.  The
    6.59 +original source is \emph{Real Analysis} by H.L. Royden.
    6.60 +It employs the Archimedean property of the reals. *}
    6.61 +
    6.62 +lemma Rats_dense_in_real:
    6.63 +  fixes x :: real
    6.64 +  assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
    6.65 +proof -
    6.66 +  from `x<y` have "0 < y-x" by simp
    6.67 +  with reals_Archimedean obtain q::nat 
    6.68 +    where q: "inverse (real q) < y-x" and "0 < q" by auto
    6.69 +  def p \<equiv> "ceiling (y * real q) - 1"
    6.70 +  def r \<equiv> "of_int p / real q"
    6.71 +  from q have "x < y - inverse (real q)" by simp
    6.72 +  also have "y - inverse (real q) \<le> r"
    6.73 +    unfolding r_def p_def
    6.74 +    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
    6.75 +  finally have "x < r" .
    6.76 +  moreover have "r < y"
    6.77 +    unfolding r_def p_def
    6.78 +    by (simp add: divide_less_eq diff_less_eq `0 < q`
    6.79 +      less_ceiling_iff [symmetric])
    6.80 +  moreover from r_def have "r \<in> \<rat>" by simp
    6.81 +  ultimately show ?thesis by fast
    6.82 +qed
    6.83 +
    6.84 +
    6.85  
    6.86  subsection{*Numerals and Arithmetic*}
    6.87  
    6.88 @@ -1576,6 +1632,422 @@
    6.89  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    6.90  by simp
    6.91  
    6.92 +
    6.93 +subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
    6.94 +
    6.95 +(* FIXME: theorems for negative numerals *)
    6.96 +lemma numeral_less_real_of_int_iff [simp]:
    6.97 +     "((numeral n) < real (m::int)) = (numeral n < m)"
    6.98 +apply auto
    6.99 +apply (rule real_of_int_less_iff [THEN iffD1])
   6.100 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
   6.101 +done
   6.102 +
   6.103 +lemma numeral_less_real_of_int_iff2 [simp]:
   6.104 +     "(real (m::int) < (numeral n)) = (m < numeral n)"
   6.105 +apply auto
   6.106 +apply (rule real_of_int_less_iff [THEN iffD1])
   6.107 +apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
   6.108 +done
   6.109 +
   6.110 +lemma numeral_le_real_of_int_iff [simp]:
   6.111 +     "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
   6.112 +by (simp add: linorder_not_less [symmetric])
   6.113 +
   6.114 +lemma numeral_le_real_of_int_iff2 [simp]:
   6.115 +     "(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
   6.116 +by (simp add: linorder_not_less [symmetric])
   6.117 +
   6.118 +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
   6.119 +unfolding real_of_nat_def by simp
   6.120 +
   6.121 +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
   6.122 +unfolding real_of_nat_def by (simp add: floor_minus)
   6.123 +
   6.124 +lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
   6.125 +unfolding real_of_int_def by simp
   6.126 +
   6.127 +lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
   6.128 +unfolding real_of_int_def by (simp add: floor_minus)
   6.129 +
   6.130 +lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
   6.131 +unfolding real_of_int_def by (rule floor_exists)
   6.132 +
   6.133 +lemma lemma_floor:
   6.134 +  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   6.135 +  shows "m \<le> (n::int)"
   6.136 +proof -
   6.137 +  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
   6.138 +  also have "... = real (n + 1)" by simp
   6.139 +  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
   6.140 +  thus ?thesis by arith
   6.141 +qed
   6.142 +
   6.143 +lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   6.144 +unfolding real_of_int_def by (rule of_int_floor_le)
   6.145 +
   6.146 +lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
   6.147 +by (auto intro: lemma_floor)
   6.148 +
   6.149 +lemma real_of_int_floor_cancel [simp]:
   6.150 +    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
   6.151 +  using floor_real_of_int by metis
   6.152 +
   6.153 +lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   6.154 +  unfolding real_of_int_def using floor_unique [of n x] by simp
   6.155 +
   6.156 +lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
   6.157 +  unfolding real_of_int_def by (rule floor_unique)
   6.158 +
   6.159 +lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
   6.160 +apply (rule inj_int [THEN injD])
   6.161 +apply (simp add: real_of_nat_Suc)
   6.162 +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
   6.163 +done
   6.164 +
   6.165 +lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   6.166 +apply (drule order_le_imp_less_or_eq)
   6.167 +apply (auto intro: floor_eq3)
   6.168 +done
   6.169 +
   6.170 +lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   6.171 +  unfolding real_of_int_def using floor_correct [of r] by simp
   6.172 +
   6.173 +lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
   6.174 +  unfolding real_of_int_def using floor_correct [of r] by simp
   6.175 +
   6.176 +lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   6.177 +  unfolding real_of_int_def using floor_correct [of r] by simp
   6.178 +
   6.179 +lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
   6.180 +  unfolding real_of_int_def using floor_correct [of r] by simp
   6.181 +
   6.182 +lemma le_floor: "real a <= x ==> a <= floor x"
   6.183 +  unfolding real_of_int_def by (simp add: le_floor_iff)
   6.184 +
   6.185 +lemma real_le_floor: "a <= floor x ==> real a <= x"
   6.186 +  unfolding real_of_int_def by (simp add: le_floor_iff)
   6.187 +
   6.188 +lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
   6.189 +  unfolding real_of_int_def by (rule le_floor_iff)
   6.190 +
   6.191 +lemma floor_less_eq: "(floor x < a) = (x < real a)"
   6.192 +  unfolding real_of_int_def by (rule floor_less_iff)
   6.193 +
   6.194 +lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
   6.195 +  unfolding real_of_int_def by (rule less_floor_iff)
   6.196 +
   6.197 +lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   6.198 +  unfolding real_of_int_def by (rule floor_le_iff)
   6.199 +
   6.200 +lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   6.201 +  unfolding real_of_int_def by (rule floor_add_of_int)
   6.202 +
   6.203 +lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   6.204 +  unfolding real_of_int_def by (rule floor_diff_of_int)
   6.205 +
   6.206 +lemma le_mult_floor:
   6.207 +  assumes "0 \<le> (a :: real)" and "0 \<le> b"
   6.208 +  shows "floor a * floor b \<le> floor (a * b)"
   6.209 +proof -
   6.210 +  have "real (floor a) \<le> a"
   6.211 +    and "real (floor b) \<le> b" by auto
   6.212 +  hence "real (floor a * floor b) \<le> a * b"
   6.213 +    using assms by (auto intro!: mult_mono)
   6.214 +  also have "a * b < real (floor (a * b) + 1)" by auto
   6.215 +  finally show ?thesis unfolding real_of_int_less_iff by simp
   6.216 +qed
   6.217 +
   6.218 +lemma floor_divide_eq_div:
   6.219 +  "floor (real a / real b) = a div b"
   6.220 +proof cases
   6.221 +  assume "b \<noteq> 0 \<or> b dvd a"
   6.222 +  with real_of_int_div3[of a b] show ?thesis
   6.223 +    by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
   6.224 +       (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
   6.225 +              real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
   6.226 +qed (auto simp: real_of_int_div)
   6.227 +
   6.228 +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   6.229 +  unfolding real_of_nat_def by simp
   6.230 +
   6.231 +lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   6.232 +  unfolding real_of_int_def by (rule le_of_int_ceiling)
   6.233 +
   6.234 +lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   6.235 +  unfolding real_of_int_def by simp
   6.236 +
   6.237 +lemma real_of_int_ceiling_cancel [simp]:
   6.238 +     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   6.239 +  using ceiling_real_of_int by metis
   6.240 +
   6.241 +lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   6.242 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   6.243 +
   6.244 +lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   6.245 +  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   6.246 +
   6.247 +lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   6.248 +  unfolding real_of_int_def using ceiling_unique [of n x] by simp
   6.249 +
   6.250 +lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   6.251 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
   6.252 +
   6.253 +lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   6.254 +  unfolding real_of_int_def using ceiling_correct [of r] by simp
   6.255 +
   6.256 +lemma ceiling_le: "x <= real a ==> ceiling x <= a"
   6.257 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   6.258 +
   6.259 +lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
   6.260 +  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   6.261 +
   6.262 +lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   6.263 +  unfolding real_of_int_def by (rule ceiling_le_iff)
   6.264 +
   6.265 +lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   6.266 +  unfolding real_of_int_def by (rule less_ceiling_iff)
   6.267 +
   6.268 +lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   6.269 +  unfolding real_of_int_def by (rule ceiling_less_iff)
   6.270 +
   6.271 +lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   6.272 +  unfolding real_of_int_def by (rule le_ceiling_iff)
   6.273 +
   6.274 +lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   6.275 +  unfolding real_of_int_def by (rule ceiling_add_of_int)
   6.276 +
   6.277 +lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   6.278 +  unfolding real_of_int_def by (rule ceiling_diff_of_int)
   6.279 +
   6.280 +
   6.281 +subsubsection {* Versions for the natural numbers *}
   6.282 +
   6.283 +definition
   6.284 +  natfloor :: "real => nat" where
   6.285 +  "natfloor x = nat(floor x)"
   6.286 +
   6.287 +definition
   6.288 +  natceiling :: "real => nat" where
   6.289 +  "natceiling x = nat(ceiling x)"
   6.290 +
   6.291 +lemma natfloor_zero [simp]: "natfloor 0 = 0"
   6.292 +  by (unfold natfloor_def, simp)
   6.293 +
   6.294 +lemma natfloor_one [simp]: "natfloor 1 = 1"
   6.295 +  by (unfold natfloor_def, simp)
   6.296 +
   6.297 +lemma zero_le_natfloor [simp]: "0 <= natfloor x"
   6.298 +  by (unfold natfloor_def, simp)
   6.299 +
   6.300 +lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
   6.301 +  by (unfold natfloor_def, simp)
   6.302 +
   6.303 +lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
   6.304 +  by (unfold natfloor_def, simp)
   6.305 +
   6.306 +lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
   6.307 +  by (unfold natfloor_def, simp)
   6.308 +
   6.309 +lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   6.310 +  unfolding natfloor_def by simp
   6.311 +
   6.312 +lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   6.313 +  unfolding natfloor_def by (intro nat_mono floor_mono)
   6.314 +
   6.315 +lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   6.316 +  apply (unfold natfloor_def)
   6.317 +  apply (subst nat_int [THEN sym])
   6.318 +  apply (rule nat_mono)
   6.319 +  apply (rule le_floor)
   6.320 +  apply simp
   6.321 +done
   6.322 +
   6.323 +lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
   6.324 +  unfolding natfloor_def real_of_nat_def
   6.325 +  by (simp add: nat_less_iff floor_less_iff)
   6.326 +
   6.327 +lemma less_natfloor:
   6.328 +  assumes "0 \<le> x" and "x < real (n :: nat)"
   6.329 +  shows "natfloor x < n"
   6.330 +  using assms by (simp add: natfloor_less_iff)
   6.331 +
   6.332 +lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   6.333 +  apply (rule iffI)
   6.334 +  apply (rule order_trans)
   6.335 +  prefer 2
   6.336 +  apply (erule real_natfloor_le)
   6.337 +  apply (subst real_of_nat_le_iff)
   6.338 +  apply assumption
   6.339 +  apply (erule le_natfloor)
   6.340 +done
   6.341 +
   6.342 +lemma le_natfloor_eq_numeral [simp]:
   6.343 +    "~ neg((numeral n)::int) ==> 0 <= x ==>
   6.344 +      (numeral n <= natfloor x) = (numeral n <= x)"
   6.345 +  apply (subst le_natfloor_eq, assumption)
   6.346 +  apply simp
   6.347 +done
   6.348 +
   6.349 +lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
   6.350 +  apply (case_tac "0 <= x")
   6.351 +  apply (subst le_natfloor_eq, assumption, simp)
   6.352 +  apply (rule iffI)
   6.353 +  apply (subgoal_tac "natfloor x <= natfloor 0")
   6.354 +  apply simp
   6.355 +  apply (rule natfloor_mono)
   6.356 +  apply simp
   6.357 +  apply simp
   6.358 +done
   6.359 +
   6.360 +lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   6.361 +  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
   6.362 +
   6.363 +lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   6.364 +  apply (case_tac "0 <= x")
   6.365 +  apply (unfold natfloor_def)
   6.366 +  apply simp
   6.367 +  apply simp_all
   6.368 +done
   6.369 +
   6.370 +lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
   6.371 +using real_natfloor_add_one_gt by (simp add: algebra_simps)
   6.372 +
   6.373 +lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
   6.374 +  apply (subgoal_tac "z < real(natfloor z) + 1")
   6.375 +  apply arith
   6.376 +  apply (rule real_natfloor_add_one_gt)
   6.377 +done
   6.378 +
   6.379 +lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   6.380 +  unfolding natfloor_def
   6.381 +  unfolding real_of_int_of_nat_eq [symmetric] floor_add
   6.382 +  by (simp add: nat_add_distrib)
   6.383 +
   6.384 +lemma natfloor_add_numeral [simp]:
   6.385 +    "~neg ((numeral n)::int) ==> 0 <= x ==>
   6.386 +      natfloor (x + numeral n) = natfloor x + numeral n"
   6.387 +  by (simp add: natfloor_add [symmetric])
   6.388 +
   6.389 +lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
   6.390 +  by (simp add: natfloor_add [symmetric] del: One_nat_def)
   6.391 +
   6.392 +lemma natfloor_subtract [simp]:
   6.393 +    "natfloor(x - real a) = natfloor x - a"
   6.394 +  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
   6.395 +  by simp
   6.396 +
   6.397 +lemma natfloor_div_nat:
   6.398 +  assumes "1 <= x" and "y > 0"
   6.399 +  shows "natfloor (x / real y) = natfloor x div y"
   6.400 +proof (rule natfloor_eq)
   6.401 +  have "(natfloor x) div y * y \<le> natfloor x"
   6.402 +    by (rule add_leD1 [where k="natfloor x mod y"], simp)
   6.403 +  thus "real (natfloor x div y) \<le> x / real y"
   6.404 +    using assms by (simp add: le_divide_eq le_natfloor_eq)
   6.405 +  have "natfloor x < (natfloor x) div y * y + y"
   6.406 +    apply (subst mod_div_equality [symmetric])
   6.407 +    apply (rule add_strict_left_mono)
   6.408 +    apply (rule mod_less_divisor)
   6.409 +    apply fact
   6.410 +    done
   6.411 +  thus "x / real y < real (natfloor x div y) + 1"
   6.412 +    using assms
   6.413 +    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
   6.414 +qed
   6.415 +
   6.416 +lemma le_mult_natfloor:
   6.417 +  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   6.418 +  by (cases "0 <= a & 0 <= b")
   6.419 +    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
   6.420 +
   6.421 +lemma natceiling_zero [simp]: "natceiling 0 = 0"
   6.422 +  by (unfold natceiling_def, simp)
   6.423 +
   6.424 +lemma natceiling_one [simp]: "natceiling 1 = 1"
   6.425 +  by (unfold natceiling_def, simp)
   6.426 +
   6.427 +lemma zero_le_natceiling [simp]: "0 <= natceiling x"
   6.428 +  by (unfold natceiling_def, simp)
   6.429 +
   6.430 +lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
   6.431 +  by (unfold natceiling_def, simp)
   6.432 +
   6.433 +lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
   6.434 +  by (unfold natceiling_def, simp)
   6.435 +
   6.436 +lemma real_natceiling_ge: "x <= real(natceiling x)"
   6.437 +  unfolding natceiling_def by (cases "x < 0", simp_all)
   6.438 +
   6.439 +lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
   6.440 +  unfolding natceiling_def by simp
   6.441 +
   6.442 +lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   6.443 +  unfolding natceiling_def by (intro nat_mono ceiling_mono)
   6.444 +
   6.445 +lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   6.446 +  unfolding natceiling_def real_of_nat_def
   6.447 +  by (simp add: nat_le_iff ceiling_le_iff)
   6.448 +
   6.449 +lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
   6.450 +  unfolding natceiling_def real_of_nat_def
   6.451 +  by (simp add: nat_le_iff ceiling_le_iff)
   6.452 +
   6.453 +lemma natceiling_le_eq_numeral [simp]:
   6.454 +    "~ neg((numeral n)::int) ==>
   6.455 +      (natceiling x <= numeral n) = (x <= numeral n)"
   6.456 +  by (simp add: natceiling_le_eq)
   6.457 +
   6.458 +lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
   6.459 +  unfolding natceiling_def
   6.460 +  by (simp add: nat_le_iff ceiling_le_iff)
   6.461 +
   6.462 +lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   6.463 +  unfolding natceiling_def
   6.464 +  by (simp add: ceiling_eq2 [where n="int n"])
   6.465 +
   6.466 +lemma natceiling_add [simp]: "0 <= x ==>
   6.467 +    natceiling (x + real a) = natceiling x + a"
   6.468 +  unfolding natceiling_def
   6.469 +  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
   6.470 +  by (simp add: nat_add_distrib)
   6.471 +
   6.472 +lemma natceiling_add_numeral [simp]:
   6.473 +    "~ neg ((numeral n)::int) ==> 0 <= x ==>
   6.474 +      natceiling (x + numeral n) = natceiling x + numeral n"
   6.475 +  by (simp add: natceiling_add [symmetric])
   6.476 +
   6.477 +lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
   6.478 +  by (simp add: natceiling_add [symmetric] del: One_nat_def)
   6.479 +
   6.480 +lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
   6.481 +  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   6.482 +  by simp
   6.483 +
   6.484 +subsection {* Exponentiation with floor *}
   6.485 +
   6.486 +lemma floor_power:
   6.487 +  assumes "x = real (floor x)"
   6.488 +  shows "floor (x ^ n) = floor x ^ n"
   6.489 +proof -
   6.490 +  have *: "x ^ n = real (floor x ^ n)"
   6.491 +    using assms by (induct n arbitrary: x) simp_all
   6.492 +  show ?thesis unfolding real_of_int_inject[symmetric]
   6.493 +    unfolding * floor_real_of_int ..
   6.494 +qed
   6.495 +
   6.496 +lemma natfloor_power:
   6.497 +  assumes "x = real (natfloor x)"
   6.498 +  shows "natfloor (x ^ n) = natfloor x ^ n"
   6.499 +proof -
   6.500 +  from assms have "0 \<le> floor x" by auto
   6.501 +  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
   6.502 +  from floor_power[OF this]
   6.503 +  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
   6.504 +    by simp
   6.505 +qed
   6.506 +
   6.507 +
   6.508  subsection {* Implementation of rational real numbers *}
   6.509  
   6.510  text {* Formal constructor *}