author | huffman |
Fri, 19 Aug 2011 11:49:53 -0700 | |
changeset 44310 | ba3d031b5dbb |
parent 43733 | a6ca7b83612f |
child 47108 | 2a1953f0d20d |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Archimedean_Field.thy |
2 |
Author: Brian Huffman |
|
30096 | 3 |
*) |
4 |
||
5 |
header {* Archimedean Fields, Floor and Ceiling Functions *} |
|
6 |
||
7 |
theory Archimedean_Field |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
11 |
subsection {* Class of Archimedean fields *} |
|
12 |
||
13 |
text {* Archimedean fields have no infinite elements. *} |
|
14 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
30102
diff
changeset
|
15 |
class archimedean_field = linordered_field + number_ring + |
30096 | 16 |
assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" |
17 |
||
18 |
lemma ex_less_of_int: |
|
19 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z" |
|
20 |
proof - |
|
21 |
from ex_le_of_int obtain z where "x \<le> of_int z" .. |
|
22 |
then have "x < of_int (z + 1)" by simp |
|
23 |
then show ?thesis .. |
|
24 |
qed |
|
25 |
||
26 |
lemma ex_of_int_less: |
|
27 |
fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x" |
|
28 |
proof - |
|
29 |
from ex_less_of_int obtain z where "- x < of_int z" .. |
|
30 |
then have "of_int (- z) < x" by simp |
|
31 |
then show ?thesis .. |
|
32 |
qed |
|
33 |
||
34 |
lemma ex_less_of_nat: |
|
35 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n" |
|
36 |
proof - |
|
37 |
obtain z where "x < of_int z" using ex_less_of_int .. |
|
38 |
also have "\<dots> \<le> of_int (int (nat z))" by simp |
|
39 |
also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq) |
|
40 |
finally show ?thesis .. |
|
41 |
qed |
|
42 |
||
43 |
lemma ex_le_of_nat: |
|
44 |
fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n" |
|
45 |
proof - |
|
46 |
obtain n where "x < of_nat n" using ex_less_of_nat .. |
|
47 |
then have "x \<le> of_nat n" by simp |
|
48 |
then show ?thesis .. |
|
49 |
qed |
|
50 |
||
51 |
text {* Archimedean fields have no infinitesimal elements. *} |
|
52 |
||
53 |
lemma ex_inverse_of_nat_Suc_less: |
|
54 |
fixes x :: "'a::archimedean_field" |
|
55 |
assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x" |
|
56 |
proof - |
|
57 |
from `0 < x` have "0 < inverse x" |
|
58 |
by (rule positive_imp_inverse_positive) |
|
59 |
obtain n where "inverse x < of_nat n" |
|
60 |
using ex_less_of_nat .. |
|
61 |
then obtain m where "inverse x < of_nat (Suc m)" |
|
62 |
using `0 < inverse x` by (cases n) (simp_all del: of_nat_Suc) |
|
63 |
then have "inverse (of_nat (Suc m)) < inverse (inverse x)" |
|
64 |
using `0 < inverse x` by (rule less_imp_inverse_less) |
|
65 |
then have "inverse (of_nat (Suc m)) < x" |
|
66 |
using `0 < x` by (simp add: nonzero_inverse_inverse_eq) |
|
67 |
then show ?thesis .. |
|
68 |
qed |
|
69 |
||
70 |
lemma ex_inverse_of_nat_less: |
|
71 |
fixes x :: "'a::archimedean_field" |
|
72 |
assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x" |
|
73 |
using ex_inverse_of_nat_Suc_less [OF `0 < x`] by auto |
|
74 |
||
75 |
lemma ex_less_of_nat_mult: |
|
76 |
fixes x :: "'a::archimedean_field" |
|
77 |
assumes "0 < x" shows "\<exists>n. y < of_nat n * x" |
|
78 |
proof - |
|
79 |
obtain n where "y / x < of_nat n" using ex_less_of_nat .. |
|
80 |
with `0 < x` have "y < of_nat n * x" by (simp add: pos_divide_less_eq) |
|
81 |
then show ?thesis .. |
|
82 |
qed |
|
83 |
||
84 |
||
85 |
subsection {* Existence and uniqueness of floor function *} |
|
86 |
||
87 |
lemma exists_least_lemma: |
|
88 |
assumes "\<not> P 0" and "\<exists>n. P n" |
|
89 |
shows "\<exists>n. \<not> P n \<and> P (Suc n)" |
|
90 |
proof - |
|
91 |
from `\<exists>n. P n` have "P (Least P)" by (rule LeastI_ex) |
|
92 |
with `\<not> P 0` obtain n where "Least P = Suc n" |
|
93 |
by (cases "Least P") auto |
|
94 |
then have "n < Least P" by simp |
|
95 |
then have "\<not> P n" by (rule not_less_Least) |
|
96 |
then have "\<not> P n \<and> P (Suc n)" |
|
97 |
using `P (Least P)` `Least P = Suc n` by simp |
|
98 |
then show ?thesis .. |
|
99 |
qed |
|
100 |
||
101 |
lemma floor_exists: |
|
102 |
fixes x :: "'a::archimedean_field" |
|
103 |
shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
104 |
proof (cases) |
|
105 |
assume "0 \<le> x" |
|
106 |
then have "\<not> x < of_nat 0" by simp |
|
107 |
then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)" |
|
108 |
using ex_less_of_nat by (rule exists_least_lemma) |
|
109 |
then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" .. |
|
110 |
then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp |
|
111 |
then show ?thesis .. |
|
112 |
next |
|
113 |
assume "\<not> 0 \<le> x" |
|
114 |
then have "\<not> - x \<le> of_nat 0" by simp |
|
115 |
then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" |
|
116 |
using ex_le_of_nat by (rule exists_least_lemma) |
|
117 |
then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" .. |
|
118 |
then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp |
|
119 |
then show ?thesis .. |
|
120 |
qed |
|
121 |
||
122 |
lemma floor_exists1: |
|
123 |
fixes x :: "'a::archimedean_field" |
|
124 |
shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
125 |
proof (rule ex_ex1I) |
|
126 |
show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)" |
|
127 |
by (rule floor_exists) |
|
128 |
next |
|
129 |
fix y z assume |
|
130 |
"of_int y \<le> x \<and> x < of_int (y + 1)" |
|
131 |
"of_int z \<le> x \<and> x < of_int (z + 1)" |
|
132 |
then have |
|
133 |
"of_int y \<le> x" "x < of_int (y + 1)" |
|
134 |
"of_int z \<le> x" "x < of_int (z + 1)" |
|
135 |
by simp_all |
|
136 |
from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`] |
|
137 |
le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`] |
|
138 |
show "y = z" by (simp del: of_int_add) |
|
139 |
qed |
|
140 |
||
141 |
||
142 |
subsection {* Floor function *} |
|
143 |
||
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
144 |
class floor_ceiling = archimedean_field + |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
145 |
fixes floor :: "'a \<Rightarrow> int" |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
146 |
assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" |
30096 | 147 |
|
148 |
notation (xsymbols) |
|
149 |
floor ("\<lfloor>_\<rfloor>") |
|
150 |
||
151 |
notation (HTML output) |
|
152 |
floor ("\<lfloor>_\<rfloor>") |
|
153 |
||
154 |
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z" |
|
155 |
using floor_correct [of x] floor_exists1 [of x] by auto |
|
156 |
||
157 |
lemma of_int_floor_le: "of_int (floor x) \<le> x" |
|
158 |
using floor_correct .. |
|
159 |
||
160 |
lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x" |
|
161 |
proof |
|
162 |
assume "z \<le> floor x" |
|
163 |
then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp |
|
164 |
also have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
|
165 |
finally show "of_int z \<le> x" . |
|
166 |
next |
|
167 |
assume "of_int z \<le> x" |
|
168 |
also have "x < of_int (floor x + 1)" using floor_correct .. |
|
169 |
finally show "z \<le> floor x" by (simp del: of_int_add) |
|
170 |
qed |
|
171 |
||
172 |
lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z" |
|
173 |
by (simp add: not_le [symmetric] le_floor_iff) |
|
174 |
||
175 |
lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x" |
|
176 |
using le_floor_iff [of "z + 1" x] by auto |
|
177 |
||
178 |
lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1" |
|
179 |
by (simp add: not_less [symmetric] less_floor_iff) |
|
180 |
||
181 |
lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y" |
|
182 |
proof - |
|
183 |
have "of_int (floor x) \<le> x" by (rule of_int_floor_le) |
|
184 |
also note `x \<le> y` |
|
185 |
finally show ?thesis by (simp add: le_floor_iff) |
|
186 |
qed |
|
187 |
||
188 |
lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y" |
|
189 |
by (auto simp add: not_le [symmetric] floor_mono) |
|
190 |
||
191 |
lemma floor_of_int [simp]: "floor (of_int z) = z" |
|
192 |
by (rule floor_unique) simp_all |
|
193 |
||
194 |
lemma floor_of_nat [simp]: "floor (of_nat n) = int n" |
|
195 |
using floor_of_int [of "of_nat n"] by simp |
|
196 |
||
197 |
text {* Floor with numerals *} |
|
198 |
||
199 |
lemma floor_zero [simp]: "floor 0 = 0" |
|
200 |
using floor_of_int [of 0] by simp |
|
201 |
||
202 |
lemma floor_one [simp]: "floor 1 = 1" |
|
203 |
using floor_of_int [of 1] by simp |
|
204 |
||
205 |
lemma floor_number_of [simp]: "floor (number_of v) = number_of v" |
|
206 |
using floor_of_int [of "number_of v"] by simp |
|
207 |
||
208 |
lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x" |
|
209 |
by (simp add: le_floor_iff) |
|
210 |
||
211 |
lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x" |
|
212 |
by (simp add: le_floor_iff) |
|
213 |
||
214 |
lemma number_of_le_floor [simp]: "number_of v \<le> floor x \<longleftrightarrow> number_of v \<le> x" |
|
215 |
by (simp add: le_floor_iff) |
|
216 |
||
217 |
lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x" |
|
218 |
by (simp add: less_floor_iff) |
|
219 |
||
220 |
lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x" |
|
221 |
by (simp add: less_floor_iff) |
|
222 |
||
223 |
lemma number_of_less_floor [simp]: |
|
224 |
"number_of v < floor x \<longleftrightarrow> number_of v + 1 \<le> x" |
|
225 |
by (simp add: less_floor_iff) |
|
226 |
||
227 |
lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1" |
|
228 |
by (simp add: floor_le_iff) |
|
229 |
||
230 |
lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2" |
|
231 |
by (simp add: floor_le_iff) |
|
232 |
||
233 |
lemma floor_le_number_of [simp]: |
|
234 |
"floor x \<le> number_of v \<longleftrightarrow> x < number_of v + 1" |
|
235 |
by (simp add: floor_le_iff) |
|
236 |
||
237 |
lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0" |
|
238 |
by (simp add: floor_less_iff) |
|
239 |
||
240 |
lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1" |
|
241 |
by (simp add: floor_less_iff) |
|
242 |
||
243 |
lemma floor_less_number_of [simp]: |
|
244 |
"floor x < number_of v \<longleftrightarrow> x < number_of v" |
|
245 |
by (simp add: floor_less_iff) |
|
246 |
||
247 |
text {* Addition and subtraction of integers *} |
|
248 |
||
249 |
lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z" |
|
250 |
using floor_correct [of x] by (simp add: floor_unique) |
|
251 |
||
252 |
lemma floor_add_number_of [simp]: |
|
253 |
"floor (x + number_of v) = floor x + number_of v" |
|
254 |
using floor_add_of_int [of x "number_of v"] by simp |
|
255 |
||
256 |
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" |
|
257 |
using floor_add_of_int [of x 1] by simp |
|
258 |
||
259 |
lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z" |
|
260 |
using floor_add_of_int [of x "- z"] by (simp add: algebra_simps) |
|
261 |
||
262 |
lemma floor_diff_number_of [simp]: |
|
263 |
"floor (x - number_of v) = floor x - number_of v" |
|
264 |
using floor_diff_of_int [of x "number_of v"] by simp |
|
265 |
||
266 |
lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1" |
|
267 |
using floor_diff_of_int [of x 1] by simp |
|
268 |
||
269 |
||
270 |
subsection {* Ceiling function *} |
|
271 |
||
272 |
definition |
|
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
43704
diff
changeset
|
273 |
ceiling :: "'a::floor_ceiling \<Rightarrow> int" where |
43733
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
274 |
"ceiling x = - floor (- x)" |
30096 | 275 |
|
276 |
notation (xsymbols) |
|
277 |
ceiling ("\<lceil>_\<rceil>") |
|
278 |
||
279 |
notation (HTML output) |
|
280 |
ceiling ("\<lceil>_\<rceil>") |
|
281 |
||
282 |
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)" |
|
283 |
unfolding ceiling_def using floor_correct [of "- x"] by simp |
|
284 |
||
285 |
lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z" |
|
286 |
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp |
|
287 |
||
288 |
lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)" |
|
289 |
using ceiling_correct .. |
|
290 |
||
291 |
lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z" |
|
292 |
unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto |
|
293 |
||
294 |
lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x" |
|
295 |
by (simp add: not_le [symmetric] ceiling_le_iff) |
|
296 |
||
297 |
lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1" |
|
298 |
using ceiling_le_iff [of x "z - 1"] by simp |
|
299 |
||
300 |
lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x" |
|
301 |
by (simp add: not_less [symmetric] ceiling_less_iff) |
|
302 |
||
303 |
lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y" |
|
304 |
unfolding ceiling_def by (simp add: floor_mono) |
|
305 |
||
306 |
lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y" |
|
307 |
by (auto simp add: not_le [symmetric] ceiling_mono) |
|
308 |
||
309 |
lemma ceiling_of_int [simp]: "ceiling (of_int z) = z" |
|
310 |
by (rule ceiling_unique) simp_all |
|
311 |
||
312 |
lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n" |
|
313 |
using ceiling_of_int [of "of_nat n"] by simp |
|
314 |
||
315 |
text {* Ceiling with numerals *} |
|
316 |
||
317 |
lemma ceiling_zero [simp]: "ceiling 0 = 0" |
|
318 |
using ceiling_of_int [of 0] by simp |
|
319 |
||
320 |
lemma ceiling_one [simp]: "ceiling 1 = 1" |
|
321 |
using ceiling_of_int [of 1] by simp |
|
322 |
||
323 |
lemma ceiling_number_of [simp]: "ceiling (number_of v) = number_of v" |
|
324 |
using ceiling_of_int [of "number_of v"] by simp |
|
325 |
||
326 |
lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0" |
|
327 |
by (simp add: ceiling_le_iff) |
|
328 |
||
329 |
lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1" |
|
330 |
by (simp add: ceiling_le_iff) |
|
331 |
||
332 |
lemma ceiling_le_number_of [simp]: |
|
333 |
"ceiling x \<le> number_of v \<longleftrightarrow> x \<le> number_of v" |
|
334 |
by (simp add: ceiling_le_iff) |
|
335 |
||
336 |
lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1" |
|
337 |
by (simp add: ceiling_less_iff) |
|
338 |
||
339 |
lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0" |
|
340 |
by (simp add: ceiling_less_iff) |
|
341 |
||
342 |
lemma ceiling_less_number_of [simp]: |
|
343 |
"ceiling x < number_of v \<longleftrightarrow> x \<le> number_of v - 1" |
|
344 |
by (simp add: ceiling_less_iff) |
|
345 |
||
346 |
lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x" |
|
347 |
by (simp add: le_ceiling_iff) |
|
348 |
||
349 |
lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x" |
|
350 |
by (simp add: le_ceiling_iff) |
|
351 |
||
352 |
lemma number_of_le_ceiling [simp]: |
|
353 |
"number_of v \<le> ceiling x\<longleftrightarrow> number_of v - 1 < x" |
|
354 |
by (simp add: le_ceiling_iff) |
|
355 |
||
356 |
lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x" |
|
357 |
by (simp add: less_ceiling_iff) |
|
358 |
||
359 |
lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x" |
|
360 |
by (simp add: less_ceiling_iff) |
|
361 |
||
362 |
lemma number_of_less_ceiling [simp]: |
|
363 |
"number_of v < ceiling x \<longleftrightarrow> number_of v < x" |
|
364 |
by (simp add: less_ceiling_iff) |
|
365 |
||
366 |
text {* Addition and subtraction of integers *} |
|
367 |
||
368 |
lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z" |
|
369 |
using ceiling_correct [of x] by (simp add: ceiling_unique) |
|
370 |
||
371 |
lemma ceiling_add_number_of [simp]: |
|
372 |
"ceiling (x + number_of v) = ceiling x + number_of v" |
|
373 |
using ceiling_add_of_int [of x "number_of v"] by simp |
|
374 |
||
375 |
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" |
|
376 |
using ceiling_add_of_int [of x 1] by simp |
|
377 |
||
378 |
lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z" |
|
379 |
using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps) |
|
380 |
||
381 |
lemma ceiling_diff_number_of [simp]: |
|
382 |
"ceiling (x - number_of v) = ceiling x - number_of v" |
|
383 |
using ceiling_diff_of_int [of x "number_of v"] by simp |
|
384 |
||
385 |
lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1" |
|
386 |
using ceiling_diff_of_int [of x 1] by simp |
|
387 |
||
388 |
||
389 |
subsection {* Negation *} |
|
390 |
||
30102 | 391 |
lemma floor_minus: "floor (- x) = - ceiling x" |
30096 | 392 |
unfolding ceiling_def by simp |
393 |
||
30102 | 394 |
lemma ceiling_minus: "ceiling (- x) = - floor x" |
30096 | 395 |
unfolding ceiling_def by simp |
396 |
||
397 |
end |