author | nipkow |
Wed, 28 Jan 2009 16:29:16 +0100 | |
changeset 29667 | 53103fc8ffa3 |
parent 28952 | 15a4b2cf8c34 |
child 30097 | 57df8626c23b |
child 30240 | 5b25fee0362c |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset
|
1 |
(* Title : HOL/RComplete.thy |
16893 | 2 |
Author : Jacques D. Fleuriot, University of Edinburgh |
3 |
Author : Larry Paulson, University of Cambridge |
|
4 |
Author : Jeremy Avigad, Carnegie Mellon University |
|
5 |
Author : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen |
|
6 |
*) |
|
5078 | 7 |
|
16893 | 8 |
header {* Completeness of the Reals; Floor and Ceiling Functions *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
9 |
|
15131 | 10 |
theory RComplete |
15140 | 11 |
imports Lubs RealDef |
15131 | 12 |
begin |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
13 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
14 |
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
16893 | 15 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
16 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
17 |
|
16893 | 18 |
subsection {* Completeness of Positive Reals *} |
19 |
||
20 |
text {* |
|
21 |
Supremum property for the set of positive reals |
|
22 |
||
23 |
Let @{text "P"} be a non-empty set of positive reals, with an upper |
|
24 |
bound @{text "y"}. Then @{text "P"} has a least upper bound |
|
25 |
(written @{text "S"}). |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
26 |
|
16893 | 27 |
FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}? |
28 |
*} |
|
29 |
||
30 |
lemma posreal_complete: |
|
31 |
assumes positive_P: "\<forall>x \<in> P. (0::real) < x" |
|
32 |
and not_empty_P: "\<exists>x. x \<in> P" |
|
33 |
and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" |
|
34 |
shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
|
35 |
proof (rule exI, rule allI) |
|
36 |
fix y |
|
37 |
let ?pP = "{w. real_of_preal w \<in> P}" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
38 |
|
16893 | 39 |
show "(\<exists>x\<in>P. y < x) = (y < real_of_preal (psup ?pP))" |
40 |
proof (cases "0 < y") |
|
41 |
assume neg_y: "\<not> 0 < y" |
|
42 |
show ?thesis |
|
43 |
proof |
|
44 |
assume "\<exists>x\<in>P. y < x" |
|
45 |
have "\<forall>x. y < real_of_preal x" |
|
46 |
using neg_y by (rule real_less_all_real2) |
|
47 |
thus "y < real_of_preal (psup ?pP)" .. |
|
48 |
next |
|
49 |
assume "y < real_of_preal (psup ?pP)" |
|
50 |
obtain "x" where x_in_P: "x \<in> P" using not_empty_P .. |
|
51 |
hence "0 < x" using positive_P by simp |
|
52 |
hence "y < x" using neg_y by simp |
|
53 |
thus "\<exists>x \<in> P. y < x" using x_in_P .. |
|
54 |
qed |
|
55 |
next |
|
56 |
assume pos_y: "0 < y" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
57 |
|
16893 | 58 |
then obtain py where y_is_py: "y = real_of_preal py" |
59 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
60 |
||
23389 | 61 |
obtain a where "a \<in> P" using not_empty_P .. |
62 |
with positive_P have a_pos: "0 < a" .. |
|
16893 | 63 |
then obtain pa where "a = real_of_preal pa" |
64 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
23389 | 65 |
hence "pa \<in> ?pP" using `a \<in> P` by auto |
16893 | 66 |
hence pP_not_empty: "?pP \<noteq> {}" by auto |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
67 |
|
16893 | 68 |
obtain sup where sup: "\<forall>x \<in> P. x < sup" |
69 |
using upper_bound_Ex .. |
|
23389 | 70 |
from this and `a \<in> P` have "a < sup" .. |
16893 | 71 |
hence "0 < sup" using a_pos by arith |
72 |
then obtain possup where "sup = real_of_preal possup" |
|
73 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
74 |
hence "\<forall>X \<in> ?pP. X \<le> possup" |
|
75 |
using sup by (auto simp add: real_of_preal_lessI) |
|
76 |
with pP_not_empty have psup: "\<And>Z. (\<exists>X \<in> ?pP. Z < X) = (Z < psup ?pP)" |
|
77 |
by (rule preal_complete) |
|
78 |
||
79 |
show ?thesis |
|
80 |
proof |
|
81 |
assume "\<exists>x \<in> P. y < x" |
|
82 |
then obtain x where x_in_P: "x \<in> P" and y_less_x: "y < x" .. |
|
83 |
hence "0 < x" using pos_y by arith |
|
84 |
then obtain px where x_is_px: "x = real_of_preal px" |
|
85 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
86 |
||
87 |
have py_less_X: "\<exists>X \<in> ?pP. py < X" |
|
88 |
proof |
|
89 |
show "py < px" using y_is_py and x_is_px and y_less_x |
|
90 |
by (simp add: real_of_preal_lessI) |
|
91 |
show "px \<in> ?pP" using x_in_P and x_is_px by simp |
|
92 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
93 |
|
16893 | 94 |
have "(\<exists>X \<in> ?pP. py < X) ==> (py < psup ?pP)" |
95 |
using psup by simp |
|
96 |
hence "py < psup ?pP" using py_less_X by simp |
|
97 |
thus "y < real_of_preal (psup {w. real_of_preal w \<in> P})" |
|
98 |
using y_is_py and pos_y by (simp add: real_of_preal_lessI) |
|
99 |
next |
|
100 |
assume y_less_psup: "y < real_of_preal (psup ?pP)" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
101 |
|
16893 | 102 |
hence "py < psup ?pP" using y_is_py |
103 |
by (simp add: real_of_preal_lessI) |
|
104 |
then obtain "X" where py_less_X: "py < X" and X_in_pP: "X \<in> ?pP" |
|
105 |
using psup by auto |
|
106 |
then obtain x where x_is_X: "x = real_of_preal X" |
|
107 |
by (simp add: real_gt_zero_preal_Ex) |
|
108 |
hence "y < x" using py_less_X and y_is_py |
|
109 |
by (simp add: real_of_preal_lessI) |
|
110 |
||
111 |
moreover have "x \<in> P" using x_is_X and X_in_pP by simp |
|
112 |
||
113 |
ultimately show "\<exists> x \<in> P. y < x" .. |
|
114 |
qed |
|
115 |
qed |
|
116 |
qed |
|
117 |
||
118 |
text {* |
|
119 |
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. |
|
120 |
*} |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
121 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
122 |
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
16893 | 123 |
apply (frule isLub_isUb) |
124 |
apply (frule_tac x = y in isLub_isUb) |
|
125 |
apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
|
126 |
done |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
127 |
|
5078 | 128 |
|
16893 | 129 |
text {* |
130 |
\medskip Completeness theorem for the positive reals (again). |
|
131 |
*} |
|
132 |
||
133 |
lemma posreals_complete: |
|
134 |
assumes positive_S: "\<forall>x \<in> S. 0 < x" |
|
135 |
and not_empty_S: "\<exists>x. x \<in> S" |
|
136 |
and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u" |
|
137 |
shows "\<exists>t. isLub (UNIV::real set) S t" |
|
138 |
proof |
|
139 |
let ?pS = "{w. real_of_preal w \<in> S}" |
|
140 |
||
141 |
obtain u where "isUb UNIV S u" using upper_bound_Ex .. |
|
142 |
hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def) |
|
143 |
||
144 |
obtain x where x_in_S: "x \<in> S" using not_empty_S .. |
|
145 |
hence x_gt_zero: "0 < x" using positive_S by simp |
|
146 |
have "x \<le> u" using sup and x_in_S .. |
|
147 |
hence "0 < u" using x_gt_zero by arith |
|
148 |
||
149 |
then obtain pu where u_is_pu: "u = real_of_preal pu" |
|
150 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
151 |
||
152 |
have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu" |
|
153 |
proof |
|
154 |
fix pa |
|
155 |
assume "pa \<in> ?pS" |
|
156 |
then obtain a where "a \<in> S" and "a = real_of_preal pa" |
|
157 |
by simp |
|
158 |
moreover hence "a \<le> u" using sup by simp |
|
159 |
ultimately show "pa \<le> pu" |
|
160 |
using sup and u_is_pu by (simp add: real_of_preal_le_iff) |
|
161 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
162 |
|
16893 | 163 |
have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)" |
164 |
proof |
|
165 |
fix y |
|
166 |
assume y_in_S: "y \<in> S" |
|
167 |
hence "0 < y" using positive_S by simp |
|
168 |
then obtain py where y_is_py: "y = real_of_preal py" |
|
169 |
by (auto simp add: real_gt_zero_preal_Ex) |
|
170 |
hence py_in_pS: "py \<in> ?pS" using y_in_S by simp |
|
171 |
with pS_less_pu have "py \<le> psup ?pS" |
|
172 |
by (rule preal_psup_le) |
|
173 |
thus "y \<le> real_of_preal (psup ?pS)" |
|
174 |
using y_is_py by (simp add: real_of_preal_le_iff) |
|
175 |
qed |
|
176 |
||
177 |
moreover { |
|
178 |
fix x |
|
179 |
assume x_ub_S: "\<forall>y\<in>S. y \<le> x" |
|
180 |
have "real_of_preal (psup ?pS) \<le> x" |
|
181 |
proof - |
|
182 |
obtain "s" where s_in_S: "s \<in> S" using not_empty_S .. |
|
183 |
hence s_pos: "0 < s" using positive_S by simp |
|
184 |
||
185 |
hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex) |
|
186 |
then obtain "ps" where s_is_ps: "s = real_of_preal ps" .. |
|
187 |
hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp |
|
188 |
||
189 |
from x_ub_S have "s \<le> x" using s_in_S .. |
|
190 |
hence "0 < x" using s_pos by simp |
|
191 |
hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex) |
|
192 |
then obtain "px" where x_is_px: "x = real_of_preal px" .. |
|
193 |
||
194 |
have "\<forall>pe \<in> ?pS. pe \<le> px" |
|
195 |
proof |
|
196 |
fix pe |
|
197 |
assume "pe \<in> ?pS" |
|
198 |
hence "real_of_preal pe \<in> S" by simp |
|
199 |
hence "real_of_preal pe \<le> x" using x_ub_S by simp |
|
200 |
thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff) |
|
201 |
qed |
|
202 |
||
203 |
moreover have "?pS \<noteq> {}" using ps_in_pS by auto |
|
204 |
ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub) |
|
205 |
thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff) |
|
206 |
qed |
|
207 |
} |
|
208 |
ultimately show "isLub UNIV S (real_of_preal (psup ?pS))" |
|
209 |
by (simp add: isLub_def leastP_def isUb_def setle_def setge_def) |
|
210 |
qed |
|
211 |
||
212 |
text {* |
|
213 |
\medskip reals Completeness (again!) |
|
214 |
*} |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
215 |
|
16893 | 216 |
lemma reals_complete: |
217 |
assumes notempty_S: "\<exists>X. X \<in> S" |
|
218 |
and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y" |
|
219 |
shows "\<exists>t. isLub (UNIV :: real set) S t" |
|
220 |
proof - |
|
221 |
obtain X where X_in_S: "X \<in> S" using notempty_S .. |
|
222 |
obtain Y where Y_isUb: "isUb (UNIV::real set) S Y" |
|
223 |
using exists_Ub .. |
|
224 |
let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}" |
|
225 |
||
226 |
{ |
|
227 |
fix x |
|
228 |
assume "isUb (UNIV::real set) S x" |
|
229 |
hence S_le_x: "\<forall> y \<in> S. y <= x" |
|
230 |
by (simp add: isUb_def setle_def) |
|
231 |
{ |
|
232 |
fix s |
|
233 |
assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}" |
|
234 |
hence "\<exists> x \<in> S. s = x + -X + 1" .. |
|
235 |
then obtain x1 where "x1 \<in> S" and "s = x1 + (-X) + 1" .. |
|
236 |
moreover hence "x1 \<le> x" using S_le_x by simp |
|
237 |
ultimately have "s \<le> x + - X + 1" by arith |
|
238 |
} |
|
239 |
then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)" |
|
240 |
by (auto simp add: isUb_def setle_def) |
|
241 |
} note S_Ub_is_SHIFT_Ub = this |
|
242 |
||
243 |
hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp |
|
244 |
hence "\<exists>Z. isUb UNIV ?SHIFT Z" .. |
|
245 |
moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto |
|
246 |
moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT" |
|
247 |
using X_in_S and Y_isUb by auto |
|
248 |
ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t" |
|
249 |
using posreals_complete [of ?SHIFT] by blast |
|
250 |
||
251 |
show ?thesis |
|
252 |
proof |
|
253 |
show "isLub UNIV S (t + X + (-1))" |
|
254 |
proof (rule isLubI2) |
|
255 |
{ |
|
256 |
fix x |
|
257 |
assume "isUb (UNIV::real set) S x" |
|
258 |
hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)" |
|
259 |
using S_Ub_is_SHIFT_Ub by simp |
|
260 |
hence "t \<le> (x + (-X) + 1)" |
|
261 |
using t_is_Lub by (simp add: isLub_le_isUb) |
|
262 |
hence "t + X + -1 \<le> x" by arith |
|
263 |
} |
|
264 |
then show "(t + X + -1) <=* Collect (isUb UNIV S)" |
|
265 |
by (simp add: setgeI) |
|
266 |
next |
|
267 |
show "isUb UNIV S (t + X + -1)" |
|
268 |
proof - |
|
269 |
{ |
|
270 |
fix y |
|
271 |
assume y_in_S: "y \<in> S" |
|
272 |
have "y \<le> t + X + -1" |
|
273 |
proof - |
|
274 |
obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty .. |
|
275 |
hence "\<exists> x \<in> S. u = x + - X + 1" by simp |
|
276 |
then obtain "x" where x_and_u: "u = x + - X + 1" .. |
|
277 |
have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2) |
|
278 |
||
279 |
show ?thesis |
|
280 |
proof cases |
|
281 |
assume "y \<le> x" |
|
282 |
moreover have "x = u + X + - 1" using x_and_u by arith |
|
283 |
moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith |
|
284 |
ultimately show "y \<le> t + X + -1" by arith |
|
285 |
next |
|
286 |
assume "~(y \<le> x)" |
|
287 |
hence x_less_y: "x < y" by arith |
|
288 |
||
289 |
have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp |
|
290 |
hence "0 < x + (-X) + 1" by simp |
|
291 |
hence "0 < y + (-X) + 1" using x_less_y by arith |
|
292 |
hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp |
|
293 |
hence "y + (-X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2) |
|
294 |
thus ?thesis by simp |
|
295 |
qed |
|
296 |
qed |
|
297 |
} |
|
298 |
then show ?thesis by (simp add: isUb_def setle_def) |
|
299 |
qed |
|
300 |
qed |
|
301 |
qed |
|
302 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
303 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
304 |
|
16893 | 305 |
subsection {* The Archimedean Property of the Reals *} |
306 |
||
307 |
theorem reals_Archimedean: |
|
308 |
assumes x_pos: "0 < x" |
|
309 |
shows "\<exists>n. inverse (real (Suc n)) < x" |
|
310 |
proof (rule ccontr) |
|
311 |
assume contr: "\<not> ?thesis" |
|
312 |
have "\<forall>n. x * real (Suc n) <= 1" |
|
313 |
proof |
|
314 |
fix n |
|
315 |
from contr have "x \<le> inverse (real (Suc n))" |
|
316 |
by (simp add: linorder_not_less) |
|
317 |
hence "x \<le> (1 / (real (Suc n)))" |
|
318 |
by (simp add: inverse_eq_divide) |
|
319 |
moreover have "0 \<le> real (Suc n)" |
|
320 |
by (rule real_of_nat_ge_zero) |
|
321 |
ultimately have "x * real (Suc n) \<le> (1 / real (Suc n)) * real (Suc n)" |
|
322 |
by (rule mult_right_mono) |
|
323 |
thus "x * real (Suc n) \<le> 1" by simp |
|
324 |
qed |
|
325 |
hence "{z. \<exists>n. z = x * (real (Suc n))} *<= 1" |
|
326 |
by (simp add: setle_def, safe, rule spec) |
|
327 |
hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (real (Suc n))} 1" |
|
328 |
by (simp add: isUbI) |
|
329 |
hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} Y" .. |
|
330 |
moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}" by auto |
|
331 |
ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * real (Suc n)} t" |
|
332 |
by (simp add: reals_complete) |
|
333 |
then obtain "t" where |
|
334 |
t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * real (Suc n)} t" .. |
|
335 |
||
336 |
have "\<forall>n::nat. x * real n \<le> t + - x" |
|
337 |
proof |
|
338 |
fix n |
|
339 |
from t_is_Lub have "x * real (Suc n) \<le> t" |
|
340 |
by (simp add: isLubD2) |
|
341 |
hence "x * (real n) + x \<le> t" |
|
342 |
by (simp add: right_distrib real_of_nat_Suc) |
|
343 |
thus "x * (real n) \<le> t + - x" by arith |
|
344 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
345 |
|
16893 | 346 |
hence "\<forall>m. x * real (Suc m) \<le> t + - x" by simp |
347 |
hence "{z. \<exists>n. z = x * (real (Suc n))} *<= (t + - x)" |
|
348 |
by (auto simp add: setle_def) |
|
349 |
hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (real (Suc n))} (t + (-x))" |
|
350 |
by (simp add: isUbI) |
|
351 |
hence "t \<le> t + - x" |
|
352 |
using t_is_Lub by (simp add: isLub_le_isUb) |
|
353 |
thus False using x_pos by arith |
|
354 |
qed |
|
355 |
||
356 |
text {* |
|
357 |
There must be other proofs, e.g. @{text "Suc"} of the largest |
|
358 |
integer in the cut representing @{text "x"}. |
|
359 |
*} |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
360 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
361 |
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)" |
16893 | 362 |
proof cases |
363 |
assume "x \<le> 0" |
|
364 |
hence "x < real (1::nat)" by simp |
|
365 |
thus ?thesis .. |
|
366 |
next |
|
367 |
assume "\<not> x \<le> 0" |
|
368 |
hence x_greater_zero: "0 < x" by simp |
|
369 |
hence "0 < inverse x" by simp |
|
370 |
then obtain n where "inverse (real (Suc n)) < inverse x" |
|
371 |
using reals_Archimedean by blast |
|
372 |
hence "inverse (real (Suc n)) * x < inverse x * x" |
|
373 |
using x_greater_zero by (rule mult_strict_right_mono) |
|
374 |
hence "inverse (real (Suc n)) * x < 1" |
|
23008 | 375 |
using x_greater_zero by simp |
16893 | 376 |
hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" |
377 |
by (rule mult_strict_left_mono) simp |
|
378 |
hence "x < real (Suc n)" |
|
29667 | 379 |
by (simp add: algebra_simps) |
16893 | 380 |
thus "\<exists>(n::nat). x < real n" .. |
381 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
382 |
|
16893 | 383 |
lemma reals_Archimedean3: |
384 |
assumes x_greater_zero: "0 < x" |
|
385 |
shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x" |
|
386 |
proof |
|
387 |
fix y |
|
388 |
have x_not_zero: "x \<noteq> 0" using x_greater_zero by simp |
|
389 |
obtain n where "y * inverse x < real (n::nat)" |
|
390 |
using reals_Archimedean2 .. |
|
391 |
hence "y * inverse x * x < real n * x" |
|
392 |
using x_greater_zero by (simp add: mult_strict_right_mono) |
|
393 |
hence "x * inverse x * y < x * real n" |
|
29667 | 394 |
by (simp add: algebra_simps) |
16893 | 395 |
hence "y < real (n::nat) * x" |
29667 | 396 |
using x_not_zero by (simp add: algebra_simps) |
16893 | 397 |
thus "\<exists>(n::nat). y < real n * x" .. |
398 |
qed |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
399 |
|
16819 | 400 |
lemma reals_Archimedean6: |
401 |
"0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
|
402 |
apply (insert reals_Archimedean2 [of r], safe) |
|
23012 | 403 |
apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto) |
16819 | 404 |
apply (rule_tac x = x in exI) |
405 |
apply (case_tac x, simp) |
|
406 |
apply (rename_tac x') |
|
407 |
apply (drule_tac x = x' in spec, simp) |
|
23012 | 408 |
apply (rule_tac x="LEAST n. r < real n" in exI, safe) |
409 |
apply (erule LeastI, erule Least_le) |
|
16819 | 410 |
done |
411 |
||
412 |
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)" |
|
16893 | 413 |
by (drule reals_Archimedean6) auto |
16819 | 414 |
|
415 |
lemma reals_Archimedean_6b_int: |
|
416 |
"0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)" |
|
417 |
apply (drule reals_Archimedean6a, auto) |
|
418 |
apply (rule_tac x = "int n" in exI) |
|
419 |
apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) |
|
420 |
done |
|
421 |
||
422 |
lemma reals_Archimedean_6c_int: |
|
423 |
"r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)" |
|
424 |
apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto) |
|
425 |
apply (rename_tac n) |
|
22998 | 426 |
apply (drule order_le_imp_less_or_eq, auto) |
16819 | 427 |
apply (rule_tac x = "- n - 1" in exI) |
428 |
apply (rule_tac [2] x = "- n" in exI, auto) |
|
429 |
done |
|
430 |
||
431 |
||
28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
432 |
subsection{*Density of the Rational Reals in the Reals*} |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
433 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
434 |
text{* This density proof is due to Stefan Richter and was ported by TN. The |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
435 |
original source is \emph{Real Analysis} by H.L. Royden. |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
436 |
It employs the Archimedean property of the reals. *} |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
437 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
438 |
lemma Rats_dense_in_nn_real: fixes x::real |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
439 |
assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
440 |
proof - |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
441 |
from `x<y` have "0 < y-x" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
442 |
with reals_Archimedean obtain q::nat |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
443 |
where q: "inverse (real q) < y-x" and "0 < real q" by auto |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
444 |
def p \<equiv> "LEAST n. y \<le> real (Suc n)/real q" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
445 |
from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
446 |
with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n") |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
447 |
by (simp add: pos_less_divide_eq[THEN sym]) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
448 |
also from assms have "\<not> y \<le> real (0::nat) / real q" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
449 |
ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
450 |
by (unfold p_def) (rule Least_Suc) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
451 |
also from ex have "?P (LEAST x. ?P x)" by (rule LeastI) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
452 |
ultimately have suc: "y \<le> real (Suc p) / real q" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
453 |
def r \<equiv> "real p/real q" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
454 |
have "x = y-(y-x)" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
455 |
also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
456 |
also have "\<dots> = real p / real q" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
457 |
by (simp only: inverse_eq_divide real_diff_def real_of_nat_Suc |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
458 |
minus_divide_left add_divide_distrib[THEN sym]) simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
459 |
finally have "x<r" by (unfold r_def) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
460 |
have "p<Suc p" .. also note main[THEN sym] |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
461 |
finally have "\<not> ?P p" by (rule not_less_Least) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
462 |
hence "r<y" by (simp add: r_def) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
463 |
from r_def have "r \<in> \<rat>" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
464 |
with `x<r` `r<y` show ?thesis by fast |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
465 |
qed |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
466 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
467 |
theorem Rats_dense_in_real: fixes x y :: real |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
468 |
assumes "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
469 |
proof - |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
470 |
from reals_Archimedean2 obtain n::nat where "-x < real n" by auto |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
471 |
hence "0 \<le> x + real n" by arith |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
472 |
also from `x<y` have "x + real n < y + real n" by arith |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
473 |
ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
474 |
by(rule Rats_dense_in_nn_real) |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
475 |
then obtain r where "r \<in> \<rat>" and r2: "x + real n < r" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
476 |
and r3: "r < y + real n" |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
477 |
by blast |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
478 |
have "r - real n = r + real (int n)/real (-1::int)" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
479 |
also from `r\<in>\<rat>` have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
480 |
also from r2 have "x < r - real n" by arith |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
481 |
moreover from r3 have "r - real n < y" by arith |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
482 |
ultimately show ?thesis by fast |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
483 |
qed |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
484 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
485 |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
486 |
subsection{*Floor and Ceiling Functions from the Reals to the Integers*} |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
487 |
|
19765 | 488 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
489 |
floor :: "real => int" where |
28562 | 490 |
[code del]: "floor r = (LEAST n::int. r < real (n+1))" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
491 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
492 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
493 |
ceiling :: "real => int" where |
19765 | 494 |
"ceiling r = - floor (- r)" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
495 |
|
21210 | 496 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
497 |
floor ("\<lfloor>_\<rfloor>") and |
19765 | 498 |
ceiling ("\<lceil>_\<rceil>") |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
499 |
|
21210 | 500 |
notation (HTML output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
501 |
floor ("\<lfloor>_\<rfloor>") and |
19765 | 502 |
ceiling ("\<lceil>_\<rceil>") |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
503 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
504 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
505 |
lemma number_of_less_real_of_int_iff [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
506 |
"((number_of n) < real (m::int)) = (number_of n < m)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
507 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
508 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
509 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
510 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
511 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
512 |
lemma number_of_less_real_of_int_iff2 [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
513 |
"(real (m::int) < (number_of n)) = (m < number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
514 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
515 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
516 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
517 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
518 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
519 |
lemma number_of_le_real_of_int_iff [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
520 |
"((number_of n) \<le> real (m::int)) = (number_of n \<le> m)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
521 |
by (simp add: linorder_not_less [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
522 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
523 |
lemma number_of_le_real_of_int_iff2 [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
524 |
"(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
525 |
by (simp add: linorder_not_less [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
526 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
527 |
lemma floor_zero [simp]: "floor 0 = 0" |
16819 | 528 |
apply (simp add: floor_def del: real_of_int_add) |
529 |
apply (rule Least_equality) |
|
530 |
apply simp_all |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
531 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
532 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
533 |
lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
534 |
by auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
535 |
|
24355 | 536 |
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
537 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
538 |
apply (rule Least_equality) |
23309 | 539 |
apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
540 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
23309 | 541 |
apply simp_all |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
542 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
543 |
|
24355 | 544 |
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
545 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
546 |
apply (rule Least_equality) |
23309 | 547 |
apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst]) |
16819 | 548 |
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
549 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
23309 | 550 |
apply simp_all |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
551 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
552 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
553 |
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
554 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
555 |
apply (rule Least_equality) |
23309 | 556 |
apply auto |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
557 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
558 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
559 |
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
560 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
561 |
apply (rule Least_equality) |
16819 | 562 |
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) |
23309 | 563 |
apply auto |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
564 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
565 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
566 |
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
567 |
apply (case_tac "r < 0") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
568 |
apply (blast intro: reals_Archimedean_6c_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
569 |
apply (simp only: linorder_not_less) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
570 |
apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
571 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
572 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
573 |
lemma lemma_floor: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
574 |
assumes a1: "real m \<le> r" and a2: "r < real n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
575 |
shows "m \<le> (n::int)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
576 |
proof - |
23389 | 577 |
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) |
578 |
also have "... = real (n + 1)" by simp |
|
579 |
finally have "m < n + 1" by (simp only: real_of_int_less_iff) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
580 |
thus ?thesis by arith |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
581 |
qed |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
582 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
583 |
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
584 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
585 |
apply (insert real_lb_ub_int [of r], safe) |
16819 | 586 |
apply (rule theI2) |
587 |
apply auto |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
588 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
589 |
|
16819 | 590 |
lemma floor_mono: "x < y ==> floor x \<le> floor y" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
591 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
592 |
apply (insert real_lb_ub_int [of x]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
593 |
apply (insert real_lb_ub_int [of y], safe) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
594 |
apply (rule theI2) |
16819 | 595 |
apply (rule_tac [3] theI2) |
596 |
apply simp |
|
597 |
apply (erule conjI) |
|
598 |
apply (auto simp add: order_eq_iff int_le_real_less) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
599 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
600 |
|
16819 | 601 |
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y" |
22998 | 602 |
by (auto dest: order_le_imp_less_or_eq simp add: floor_mono) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
603 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
604 |
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
605 |
by (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
606 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
607 |
lemma real_of_int_floor_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
608 |
"(real (floor x) = x) = (\<exists>n::int. x = real n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
609 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
610 |
apply (insert real_lb_ub_int [of x], erule exE) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
611 |
apply (rule theI2) |
16893 | 612 |
apply (auto intro: lemma_floor) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
613 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
614 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
615 |
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
616 |
apply (simp add: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
617 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
618 |
apply (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
619 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
620 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
621 |
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
622 |
apply (simp add: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
623 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
624 |
apply (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
625 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
626 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
627 |
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
628 |
apply (rule inj_int [THEN injD]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
629 |
apply (simp add: real_of_nat_Suc) |
15539 | 630 |
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
631 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
632 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
633 |
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
634 |
apply (drule order_le_imp_less_or_eq) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
635 |
apply (auto intro: floor_eq3) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
636 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
637 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
638 |
lemma floor_number_of_eq [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
639 |
"floor(number_of n :: real) = (number_of n :: int)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
640 |
apply (subst real_number_of [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
641 |
apply (rule floor_real_of_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
642 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
643 |
|
16819 | 644 |
lemma floor_one [simp]: "floor 1 = 1" |
645 |
apply (rule trans) |
|
646 |
prefer 2 |
|
647 |
apply (rule floor_real_of_int) |
|
648 |
apply simp |
|
649 |
done |
|
650 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
651 |
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
652 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
653 |
apply (insert real_lb_ub_int [of r], safe) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
654 |
apply (rule theI2) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
655 |
apply (auto intro: lemma_floor) |
16819 | 656 |
done |
657 |
||
658 |
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" |
|
659 |
apply (simp add: floor_def Least_def) |
|
660 |
apply (insert real_lb_ub_int [of r], safe) |
|
661 |
apply (rule theI2) |
|
662 |
apply (auto intro: lemma_floor) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
663 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
664 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
665 |
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
666 |
apply (insert real_of_int_floor_ge_diff_one [of r]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
667 |
apply (auto simp del: real_of_int_floor_ge_diff_one) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
668 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
669 |
|
16819 | 670 |
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" |
671 |
apply (insert real_of_int_floor_gt_diff_one [of r]) |
|
672 |
apply (auto simp del: real_of_int_floor_gt_diff_one) |
|
673 |
done |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
674 |
|
16819 | 675 |
lemma le_floor: "real a <= x ==> a <= floor x" |
676 |
apply (subgoal_tac "a < floor x + 1") |
|
677 |
apply arith |
|
678 |
apply (subst real_of_int_less_iff [THEN sym]) |
|
679 |
apply simp |
|
16893 | 680 |
apply (insert real_of_int_floor_add_one_gt [of x]) |
16819 | 681 |
apply arith |
682 |
done |
|
683 |
||
684 |
lemma real_le_floor: "a <= floor x ==> real a <= x" |
|
685 |
apply (rule order_trans) |
|
686 |
prefer 2 |
|
687 |
apply (rule real_of_int_floor_le) |
|
688 |
apply (subst real_of_int_le_iff) |
|
689 |
apply assumption |
|
690 |
done |
|
691 |
||
692 |
lemma le_floor_eq: "(a <= floor x) = (real a <= x)" |
|
693 |
apply (rule iffI) |
|
694 |
apply (erule real_le_floor) |
|
695 |
apply (erule le_floor) |
|
696 |
done |
|
697 |
||
16893 | 698 |
lemma le_floor_eq_number_of [simp]: |
16819 | 699 |
"(number_of n <= floor x) = (number_of n <= x)" |
700 |
by (simp add: le_floor_eq) |
|
701 |
||
702 |
lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)" |
|
703 |
by (simp add: le_floor_eq) |
|
704 |
||
705 |
lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)" |
|
706 |
by (simp add: le_floor_eq) |
|
707 |
||
708 |
lemma floor_less_eq: "(floor x < a) = (x < real a)" |
|
709 |
apply (subst linorder_not_le [THEN sym])+ |
|
710 |
apply simp |
|
711 |
apply (rule le_floor_eq) |
|
712 |
done |
|
713 |
||
16893 | 714 |
lemma floor_less_eq_number_of [simp]: |
16819 | 715 |
"(floor x < number_of n) = (x < number_of n)" |
716 |
by (simp add: floor_less_eq) |
|
717 |
||
718 |
lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)" |
|
719 |
by (simp add: floor_less_eq) |
|
720 |
||
721 |
lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)" |
|
722 |
by (simp add: floor_less_eq) |
|
723 |
||
724 |
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" |
|
725 |
apply (insert le_floor_eq [of "a + 1" x]) |
|
726 |
apply auto |
|
727 |
done |
|
728 |
||
16893 | 729 |
lemma less_floor_eq_number_of [simp]: |
16819 | 730 |
"(number_of n < floor x) = (number_of n + 1 <= x)" |
731 |
by (simp add: less_floor_eq) |
|
732 |
||
733 |
lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)" |
|
734 |
by (simp add: less_floor_eq) |
|
735 |
||
736 |
lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)" |
|
737 |
by (simp add: less_floor_eq) |
|
738 |
||
739 |
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" |
|
740 |
apply (insert floor_less_eq [of x "a + 1"]) |
|
741 |
apply auto |
|
742 |
done |
|
743 |
||
16893 | 744 |
lemma floor_le_eq_number_of [simp]: |
16819 | 745 |
"(floor x <= number_of n) = (x < number_of n + 1)" |
746 |
by (simp add: floor_le_eq) |
|
747 |
||
748 |
lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)" |
|
749 |
by (simp add: floor_le_eq) |
|
750 |
||
751 |
lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)" |
|
752 |
by (simp add: floor_le_eq) |
|
753 |
||
754 |
lemma floor_add [simp]: "floor (x + real a) = floor x + a" |
|
755 |
apply (subst order_eq_iff) |
|
756 |
apply (rule conjI) |
|
757 |
prefer 2 |
|
758 |
apply (subgoal_tac "floor x + a < floor (x + real a) + 1") |
|
759 |
apply arith |
|
760 |
apply (subst real_of_int_less_iff [THEN sym]) |
|
761 |
apply simp |
|
762 |
apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1") |
|
763 |
apply (subgoal_tac "real (floor x) <= x") |
|
764 |
apply arith |
|
765 |
apply (rule real_of_int_floor_le) |
|
766 |
apply (rule real_of_int_floor_add_one_gt) |
|
767 |
apply (subgoal_tac "floor (x + real a) < floor x + a + 1") |
|
768 |
apply arith |
|
16893 | 769 |
apply (subst real_of_int_less_iff [THEN sym]) |
16819 | 770 |
apply simp |
16893 | 771 |
apply (subgoal_tac "real(floor(x + real a)) <= x + real a") |
16819 | 772 |
apply (subgoal_tac "x < real(floor x) + 1") |
773 |
apply arith |
|
774 |
apply (rule real_of_int_floor_add_one_gt) |
|
775 |
apply (rule real_of_int_floor_le) |
|
776 |
done |
|
777 |
||
16893 | 778 |
lemma floor_add_number_of [simp]: |
16819 | 779 |
"floor (x + number_of n) = floor x + number_of n" |
780 |
apply (subst floor_add [THEN sym]) |
|
781 |
apply simp |
|
782 |
done |
|
783 |
||
784 |
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" |
|
785 |
apply (subst floor_add [THEN sym]) |
|
786 |
apply simp |
|
787 |
done |
|
788 |
||
789 |
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a" |
|
790 |
apply (subst diff_minus)+ |
|
791 |
apply (subst real_of_int_minus [THEN sym]) |
|
792 |
apply (rule floor_add) |
|
793 |
done |
|
794 |
||
16893 | 795 |
lemma floor_subtract_number_of [simp]: "floor (x - number_of n) = |
16819 | 796 |
floor x - number_of n" |
797 |
apply (subst floor_subtract [THEN sym]) |
|
798 |
apply simp |
|
799 |
done |
|
800 |
||
801 |
lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1" |
|
802 |
apply (subst floor_subtract [THEN sym]) |
|
803 |
apply simp |
|
804 |
done |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
805 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
806 |
lemma ceiling_zero [simp]: "ceiling 0 = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
807 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
808 |
|
24355 | 809 |
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
810 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
811 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
812 |
lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
813 |
by auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
814 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
815 |
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
816 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
817 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
818 |
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
819 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
820 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
821 |
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
822 |
apply (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
823 |
apply (subst le_minus_iff, simp) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
824 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
825 |
|
16819 | 826 |
lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y" |
827 |
by (simp add: floor_mono ceiling_def) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
828 |
|
16819 | 829 |
lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y" |
830 |
by (simp add: floor_mono2 ceiling_def) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
831 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
832 |
lemma real_of_int_ceiling_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
833 |
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
834 |
apply (auto simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
835 |
apply (drule arg_cong [where f = uminus], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
836 |
apply (rule_tac x = "-n" in exI, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
837 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
838 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
839 |
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
840 |
apply (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
841 |
apply (rule minus_equation_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
842 |
apply (simp add: floor_eq [where n = "-(n+1)"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
843 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
844 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
845 |
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
846 |
by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
847 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
848 |
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
849 |
by (simp add: ceiling_def floor_eq2 [where n = "-n"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
850 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
851 |
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
852 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
853 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
854 |
lemma ceiling_number_of_eq [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
855 |
"ceiling (number_of n :: real) = (number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
856 |
apply (subst real_number_of [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
857 |
apply (rule ceiling_real_of_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
858 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
859 |
|
16819 | 860 |
lemma ceiling_one [simp]: "ceiling 1 = 1" |
861 |
by (unfold ceiling_def, simp) |
|
862 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
863 |
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
864 |
apply (rule neg_le_iff_le [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
865 |
apply (simp add: ceiling_def diff_minus) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
866 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
867 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
868 |
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
869 |
apply (insert real_of_int_ceiling_diff_one_le [of r]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
870 |
apply (simp del: real_of_int_ceiling_diff_one_le) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
871 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
872 |
|
16819 | 873 |
lemma ceiling_le: "x <= real a ==> ceiling x <= a" |
874 |
apply (unfold ceiling_def) |
|
875 |
apply (subgoal_tac "-a <= floor(- x)") |
|
876 |
apply simp |
|
877 |
apply (rule le_floor) |
|
878 |
apply simp |
|
879 |
done |
|
880 |
||
881 |
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" |
|
882 |
apply (unfold ceiling_def) |
|
883 |
apply (subgoal_tac "real(- a) <= - x") |
|
884 |
apply simp |
|
885 |
apply (rule real_le_floor) |
|
886 |
apply simp |
|
887 |
done |
|
888 |
||
889 |
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" |
|
890 |
apply (rule iffI) |
|
891 |
apply (erule ceiling_le_real) |
|
892 |
apply (erule ceiling_le) |
|
893 |
done |
|
894 |
||
16893 | 895 |
lemma ceiling_le_eq_number_of [simp]: |
16819 | 896 |
"(ceiling x <= number_of n) = (x <= number_of n)" |
897 |
by (simp add: ceiling_le_eq) |
|
898 |
||
16893 | 899 |
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" |
16819 | 900 |
by (simp add: ceiling_le_eq) |
901 |
||
16893 | 902 |
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" |
16819 | 903 |
by (simp add: ceiling_le_eq) |
904 |
||
905 |
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" |
|
906 |
apply (subst linorder_not_le [THEN sym])+ |
|
907 |
apply simp |
|
908 |
apply (rule ceiling_le_eq) |
|
909 |
done |
|
910 |
||
16893 | 911 |
lemma less_ceiling_eq_number_of [simp]: |
16819 | 912 |
"(number_of n < ceiling x) = (number_of n < x)" |
913 |
by (simp add: less_ceiling_eq) |
|
914 |
||
915 |
lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)" |
|
916 |
by (simp add: less_ceiling_eq) |
|
917 |
||
918 |
lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)" |
|
919 |
by (simp add: less_ceiling_eq) |
|
920 |
||
921 |
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)" |
|
922 |
apply (insert ceiling_le_eq [of x "a - 1"]) |
|
923 |
apply auto |
|
924 |
done |
|
925 |
||
16893 | 926 |
lemma ceiling_less_eq_number_of [simp]: |
16819 | 927 |
"(ceiling x < number_of n) = (x <= number_of n - 1)" |
928 |
by (simp add: ceiling_less_eq) |
|
929 |
||
930 |
lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)" |
|
931 |
by (simp add: ceiling_less_eq) |
|
932 |
||
933 |
lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)" |
|
934 |
by (simp add: ceiling_less_eq) |
|
935 |
||
936 |
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)" |
|
937 |
apply (insert less_ceiling_eq [of "a - 1" x]) |
|
938 |
apply auto |
|
939 |
done |
|
940 |
||
16893 | 941 |
lemma le_ceiling_eq_number_of [simp]: |
16819 | 942 |
"(number_of n <= ceiling x) = (number_of n - 1 < x)" |
943 |
by (simp add: le_ceiling_eq) |
|
944 |
||
945 |
lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)" |
|
946 |
by (simp add: le_ceiling_eq) |
|
947 |
||
948 |
lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)" |
|
949 |
by (simp add: le_ceiling_eq) |
|
950 |
||
951 |
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" |
|
952 |
apply (unfold ceiling_def, simp) |
|
953 |
apply (subst real_of_int_minus [THEN sym]) |
|
954 |
apply (subst floor_add) |
|
955 |
apply simp |
|
956 |
done |
|
957 |
||
16893 | 958 |
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = |
16819 | 959 |
ceiling x + number_of n" |
960 |
apply (subst ceiling_add [THEN sym]) |
|
961 |
apply simp |
|
962 |
done |
|
963 |
||
964 |
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" |
|
965 |
apply (subst ceiling_add [THEN sym]) |
|
966 |
apply simp |
|
967 |
done |
|
968 |
||
969 |
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a" |
|
970 |
apply (subst diff_minus)+ |
|
971 |
apply (subst real_of_int_minus [THEN sym]) |
|
972 |
apply (rule ceiling_add) |
|
973 |
done |
|
974 |
||
16893 | 975 |
lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) = |
16819 | 976 |
ceiling x - number_of n" |
977 |
apply (subst ceiling_subtract [THEN sym]) |
|
978 |
apply simp |
|
979 |
done |
|
980 |
||
981 |
lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1" |
|
982 |
apply (subst ceiling_subtract [THEN sym]) |
|
983 |
apply simp |
|
984 |
done |
|
985 |
||
986 |
subsection {* Versions for the natural numbers *} |
|
987 |
||
19765 | 988 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
989 |
natfloor :: "real => nat" where |
19765 | 990 |
"natfloor x = nat(floor x)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
991 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
992 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
993 |
natceiling :: "real => nat" where |
19765 | 994 |
"natceiling x = nat(ceiling x)" |
16819 | 995 |
|
996 |
lemma natfloor_zero [simp]: "natfloor 0 = 0" |
|
997 |
by (unfold natfloor_def, simp) |
|
998 |
||
999 |
lemma natfloor_one [simp]: "natfloor 1 = 1" |
|
1000 |
by (unfold natfloor_def, simp) |
|
1001 |
||
1002 |
lemma zero_le_natfloor [simp]: "0 <= natfloor x" |
|
1003 |
by (unfold natfloor_def, simp) |
|
1004 |
||
1005 |
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n" |
|
1006 |
by (unfold natfloor_def, simp) |
|
1007 |
||
1008 |
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" |
|
1009 |
by (unfold natfloor_def, simp) |
|
1010 |
||
1011 |
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" |
|
1012 |
by (unfold natfloor_def, simp) |
|
1013 |
||
1014 |
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" |
|
1015 |
apply (unfold natfloor_def) |
|
1016 |
apply (subgoal_tac "floor x <= floor 0") |
|
1017 |
apply simp |
|
1018 |
apply (erule floor_mono2) |
|
1019 |
done |
|
1020 |
||
1021 |
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" |
|
1022 |
apply (case_tac "0 <= x") |
|
1023 |
apply (subst natfloor_def)+ |
|
1024 |
apply (subst nat_le_eq_zle) |
|
1025 |
apply force |
|
16893 | 1026 |
apply (erule floor_mono2) |
16819 | 1027 |
apply (subst natfloor_neg) |
1028 |
apply simp |
|
1029 |
apply simp |
|
1030 |
done |
|
1031 |
||
1032 |
lemma le_natfloor: "real x <= a ==> x <= natfloor a" |
|
1033 |
apply (unfold natfloor_def) |
|
1034 |
apply (subst nat_int [THEN sym]) |
|
1035 |
apply (subst nat_le_eq_zle) |
|
1036 |
apply simp |
|
1037 |
apply (rule le_floor) |
|
1038 |
apply simp |
|
1039 |
done |
|
1040 |
||
1041 |
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" |
|
1042 |
apply (rule iffI) |
|
1043 |
apply (rule order_trans) |
|
1044 |
prefer 2 |
|
1045 |
apply (erule real_natfloor_le) |
|
1046 |
apply (subst real_of_nat_le_iff) |
|
1047 |
apply assumption |
|
1048 |
apply (erule le_natfloor) |
|
1049 |
done |
|
1050 |
||
16893 | 1051 |
lemma le_natfloor_eq_number_of [simp]: |
16819 | 1052 |
"~ neg((number_of n)::int) ==> 0 <= x ==> |
1053 |
(number_of n <= natfloor x) = (number_of n <= x)" |
|
1054 |
apply (subst le_natfloor_eq, assumption) |
|
1055 |
apply simp |
|
1056 |
done |
|
1057 |
||
16820 | 1058 |
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" |
16819 | 1059 |
apply (case_tac "0 <= x") |
1060 |
apply (subst le_natfloor_eq, assumption, simp) |
|
1061 |
apply (rule iffI) |
|
16893 | 1062 |
apply (subgoal_tac "natfloor x <= natfloor 0") |
16819 | 1063 |
apply simp |
1064 |
apply (rule natfloor_mono) |
|
1065 |
apply simp |
|
1066 |
apply simp |
|
1067 |
done |
|
1068 |
||
1069 |
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" |
|
1070 |
apply (unfold natfloor_def) |
|
1071 |
apply (subst nat_int [THEN sym]);back; |
|
1072 |
apply (subst eq_nat_nat_iff) |
|
1073 |
apply simp |
|
1074 |
apply simp |
|
1075 |
apply (rule floor_eq2) |
|
1076 |
apply auto |
|
1077 |
done |
|
1078 |
||
1079 |
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" |
|
1080 |
apply (case_tac "0 <= x") |
|
1081 |
apply (unfold natfloor_def) |
|
1082 |
apply simp |
|
1083 |
apply simp_all |
|
1084 |
done |
|
1085 |
||
1086 |
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" |
|
29667 | 1087 |
using real_natfloor_add_one_gt by (simp add: algebra_simps) |
16819 | 1088 |
|
1089 |
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" |
|
1090 |
apply (subgoal_tac "z < real(natfloor z) + 1") |
|
1091 |
apply arith |
|
1092 |
apply (rule real_natfloor_add_one_gt) |
|
1093 |
done |
|
1094 |
||
1095 |
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" |
|
1096 |
apply (unfold natfloor_def) |
|
24355 | 1097 |
apply (subgoal_tac "real a = real (int a)") |
16819 | 1098 |
apply (erule ssubst) |
23309 | 1099 |
apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq) |
16819 | 1100 |
apply simp |
1101 |
done |
|
1102 |
||
16893 | 1103 |
lemma natfloor_add_number_of [simp]: |
1104 |
"~neg ((number_of n)::int) ==> 0 <= x ==> |
|
16819 | 1105 |
natfloor (x + number_of n) = natfloor x + number_of n" |
1106 |
apply (subst natfloor_add [THEN sym]) |
|
1107 |
apply simp_all |
|
1108 |
done |
|
1109 |
||
1110 |
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" |
|
1111 |
apply (subst natfloor_add [THEN sym]) |
|
1112 |
apply assumption |
|
1113 |
apply simp |
|
1114 |
done |
|
1115 |
||
16893 | 1116 |
lemma natfloor_subtract [simp]: "real a <= x ==> |
16819 | 1117 |
natfloor(x - real a) = natfloor x - a" |
1118 |
apply (unfold natfloor_def) |
|
24355 | 1119 |
apply (subgoal_tac "real a = real (int a)") |
16819 | 1120 |
apply (erule ssubst) |
23309 | 1121 |
apply (simp del: real_of_int_of_nat_eq) |
16819 | 1122 |
apply simp |
1123 |
done |
|
1124 |
||
1125 |
lemma natceiling_zero [simp]: "natceiling 0 = 0" |
|
1126 |
by (unfold natceiling_def, simp) |
|
1127 |
||
1128 |
lemma natceiling_one [simp]: "natceiling 1 = 1" |
|
1129 |
by (unfold natceiling_def, simp) |
|
1130 |
||
1131 |
lemma zero_le_natceiling [simp]: "0 <= natceiling x" |
|
1132 |
by (unfold natceiling_def, simp) |
|
1133 |
||
1134 |
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n" |
|
1135 |
by (unfold natceiling_def, simp) |
|
1136 |
||
1137 |
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" |
|
1138 |
by (unfold natceiling_def, simp) |
|
1139 |
||
1140 |
lemma real_natceiling_ge: "x <= real(natceiling x)" |
|
1141 |
apply (unfold natceiling_def) |
|
1142 |
apply (case_tac "x < 0") |
|
1143 |
apply simp |
|
1144 |
apply (subst real_nat_eq_real) |
|
1145 |
apply (subgoal_tac "ceiling 0 <= ceiling x") |
|
1146 |
apply simp |
|
1147 |
apply (rule ceiling_mono2) |
|
1148 |
apply simp |
|
1149 |
apply simp |
|
1150 |
done |
|
1151 |
||
1152 |
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" |
|
1153 |
apply (unfold natceiling_def) |
|
1154 |
apply simp |
|
1155 |
done |
|
1156 |
||
1157 |
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" |
|
1158 |
apply (case_tac "0 <= x") |
|
1159 |
apply (subst natceiling_def)+ |
|
1160 |
apply (subst nat_le_eq_zle) |
|
1161 |
apply (rule disjI2) |
|
1162 |
apply (subgoal_tac "real (0::int) <= real(ceiling y)") |
|
1163 |
apply simp |
|
1164 |
apply (rule order_trans) |
|
1165 |
apply simp |
|
1166 |
apply (erule order_trans) |
|
1167 |
apply simp |
|
1168 |
apply (erule ceiling_mono2) |
|
1169 |
apply (subst natceiling_neg) |
|
1170 |
apply simp_all |
|
1171 |
done |
|
1172 |
||
1173 |
lemma natceiling_le: "x <= real a ==> natceiling x <= a" |
|
1174 |
apply (unfold natceiling_def) |
|
1175 |
apply (case_tac "x < 0") |
|
1176 |
apply simp |
|
1177 |
apply (subst nat_int [THEN sym]);back; |
|
1178 |
apply (subst nat_le_eq_zle) |
|
1179 |
apply simp |
|
1180 |
apply (rule ceiling_le) |
|
1181 |
apply simp |
|
1182 |
done |
|
1183 |
||
1184 |
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)" |
|
1185 |
apply (rule iffI) |
|
1186 |
apply (rule order_trans) |
|
1187 |
apply (rule real_natceiling_ge) |
|
1188 |
apply (subst real_of_nat_le_iff) |
|
1189 |
apply assumption |
|
1190 |
apply (erule natceiling_le) |
|
1191 |
done |
|
1192 |
||
16893 | 1193 |
lemma natceiling_le_eq_number_of [simp]: |
16820 | 1194 |
"~ neg((number_of n)::int) ==> 0 <= x ==> |
1195 |
(natceiling x <= number_of n) = (x <= number_of n)" |
|
16819 | 1196 |
apply (subst natceiling_le_eq, assumption) |
1197 |
apply simp |
|
1198 |
done |
|
1199 |
||
16820 | 1200 |
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" |
16819 | 1201 |
apply (case_tac "0 <= x") |
1202 |
apply (subst natceiling_le_eq) |
|
1203 |
apply assumption |
|
1204 |
apply simp |
|
1205 |
apply (subst natceiling_neg) |
|
1206 |
apply simp |
|
1207 |
apply simp |
|
1208 |
done |
|
1209 |
||
1210 |
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" |
|
1211 |
apply (unfold natceiling_def) |
|
19850 | 1212 |
apply (simplesubst nat_int [THEN sym]) back back |
16819 | 1213 |
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") |
1214 |
apply (erule ssubst) |
|
1215 |
apply (subst eq_nat_nat_iff) |
|
1216 |
apply (subgoal_tac "ceiling 0 <= ceiling x") |
|
1217 |
apply simp |
|
1218 |
apply (rule ceiling_mono2) |
|
1219 |
apply force |
|
1220 |
apply force |
|
1221 |
apply (rule ceiling_eq2) |
|
1222 |
apply (simp, simp) |
|
1223 |
apply (subst nat_add_distrib) |
|
1224 |
apply auto |
|
1225 |
done |
|
1226 |
||
16893 | 1227 |
lemma natceiling_add [simp]: "0 <= x ==> |
16819 | 1228 |
natceiling (x + real a) = natceiling x + a" |
1229 |
apply (unfold natceiling_def) |
|
24355 | 1230 |
apply (subgoal_tac "real a = real (int a)") |
16819 | 1231 |
apply (erule ssubst) |
23309 | 1232 |
apply (simp del: real_of_int_of_nat_eq) |
16819 | 1233 |
apply (subst nat_add_distrib) |
1234 |
apply (subgoal_tac "0 = ceiling 0") |
|
1235 |
apply (erule ssubst) |
|
1236 |
apply (erule ceiling_mono2) |
|
1237 |
apply simp_all |
|
1238 |
done |
|
1239 |
||
16893 | 1240 |
lemma natceiling_add_number_of [simp]: |
1241 |
"~ neg ((number_of n)::int) ==> 0 <= x ==> |
|
16820 | 1242 |
natceiling (x + number_of n) = natceiling x + number_of n" |
16819 | 1243 |
apply (subst natceiling_add [THEN sym]) |
1244 |
apply simp_all |
|
1245 |
done |
|
1246 |
||
1247 |
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" |
|
1248 |
apply (subst natceiling_add [THEN sym]) |
|
1249 |
apply assumption |
|
1250 |
apply simp |
|
1251 |
done |
|
1252 |
||
16893 | 1253 |
lemma natceiling_subtract [simp]: "real a <= x ==> |
16819 | 1254 |
natceiling(x - real a) = natceiling x - a" |
1255 |
apply (unfold natceiling_def) |
|
24355 | 1256 |
apply (subgoal_tac "real a = real (int a)") |
16819 | 1257 |
apply (erule ssubst) |
23309 | 1258 |
apply (simp del: real_of_int_of_nat_eq) |
16819 | 1259 |
apply simp |
1260 |
done |
|
1261 |
||
25162 | 1262 |
lemma natfloor_div_nat: "1 <= x ==> y > 0 ==> |
16819 | 1263 |
natfloor (x / real y) = natfloor x div y" |
1264 |
proof - |
|
25162 | 1265 |
assume "1 <= (x::real)" and "(y::nat) > 0" |
16819 | 1266 |
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" |
1267 |
by simp |
|
16893 | 1268 |
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + |
16819 | 1269 |
real((natfloor x) mod y)" |
1270 |
by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) |
|
1271 |
have "x = real(natfloor x) + (x - real(natfloor x))" |
|
1272 |
by simp |
|
16893 | 1273 |
then have "x = real ((natfloor x) div y) * real y + |
16819 | 1274 |
real((natfloor x) mod y) + (x - real(natfloor x))" |
1275 |
by (simp add: a) |
|
1276 |
then have "x / real y = ... / real y" |
|
1277 |
by simp |
|
16893 | 1278 |
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
16819 | 1279 |
real y + (x - real(natfloor x)) / real y" |
29667 | 1280 |
by (auto simp add: algebra_simps add_divide_distrib |
16819 | 1281 |
diff_divide_distrib prems) |
1282 |
finally have "natfloor (x / real y) = natfloor(...)" by simp |
|
16893 | 1283 |
also have "... = natfloor(real((natfloor x) mod y) / |
16819 | 1284 |
real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
1285 |
by (simp add: add_ac) |
|
16893 | 1286 |
also have "... = natfloor(real((natfloor x) mod y) / |
16819 | 1287 |
real y + (x - real(natfloor x)) / real y) + (natfloor x) div y" |
1288 |
apply (rule natfloor_add) |
|
1289 |
apply (rule add_nonneg_nonneg) |
|
1290 |
apply (rule divide_nonneg_pos) |
|
1291 |
apply simp |
|
1292 |
apply (simp add: prems) |
|
1293 |
apply (rule divide_nonneg_pos) |
|
29667 | 1294 |
apply (simp add: algebra_simps) |
16819 | 1295 |
apply (rule real_natfloor_le) |
1296 |
apply (insert prems, auto) |
|
1297 |
done |
|
16893 | 1298 |
also have "natfloor(real((natfloor x) mod y) / |
16819 | 1299 |
real y + (x - real(natfloor x)) / real y) = 0" |
1300 |
apply (rule natfloor_eq) |
|
1301 |
apply simp |
|
1302 |
apply (rule add_nonneg_nonneg) |
|
1303 |
apply (rule divide_nonneg_pos) |
|
1304 |
apply force |
|
1305 |
apply (force simp add: prems) |
|
1306 |
apply (rule divide_nonneg_pos) |
|
29667 | 1307 |
apply (simp add: algebra_simps) |
16819 | 1308 |
apply (rule real_natfloor_le) |
1309 |
apply (auto simp add: prems) |
|
1310 |
apply (insert prems, arith) |
|
1311 |
apply (simp add: add_divide_distrib [THEN sym]) |
|
1312 |
apply (subgoal_tac "real y = real y - 1 + 1") |
|
1313 |
apply (erule ssubst) |
|
1314 |
apply (rule add_le_less_mono) |
|
29667 | 1315 |
apply (simp add: algebra_simps) |
1316 |
apply (subgoal_tac "1 + real(natfloor x mod y) = |
|
16819 | 1317 |
real(natfloor x mod y + 1)") |
1318 |
apply (erule ssubst) |
|
1319 |
apply (subst real_of_nat_le_iff) |
|
1320 |
apply (subgoal_tac "natfloor x mod y < y") |
|
1321 |
apply arith |
|
1322 |
apply (rule mod_less_divisor) |
|
1323 |
apply auto |
|
29667 | 1324 |
using real_natfloor_add_one_gt |
1325 |
apply (simp add: algebra_simps) |
|
16819 | 1326 |
done |
25140 | 1327 |
finally show ?thesis by simp |
16819 | 1328 |
qed |
1329 |
||
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
1330 |
end |