1 (* Title: IntFloor.thy |
1 (* Title: IntFloor.thy |
2 Author: Jacques D. Fleuriot |
2 Author: Jacques D. Fleuriot |
3 Copyright: 2001,2002 University of Edinburgh |
3 Copyright: 2001,2002 University of Edinburgh |
4 Description: Floor and ceiling operations over reals |
4 Converted to Isar and polished by lcp |
5 *) |
5 *) |
6 |
6 |
7 IntFloor = Integration + |
7 header{*Floor and Ceiling Functions from the Reals to the Integers*} |
|
8 |
|
9 theory IntFloor = Integration: |
8 |
10 |
9 constdefs |
11 constdefs |
10 |
12 |
11 floor :: real => int |
13 floor :: "real => int" |
12 "floor r == (LEAST n. r < real (n + (1::int)))" |
14 "floor r == (LEAST n. r < real (n + (1::int)))" |
13 |
15 |
14 ceiling :: real => int |
16 ceiling :: "real => int" |
15 "ceiling r == - floor (- r)" |
17 "ceiling r == - floor (- r)" |
16 |
18 |
|
19 syntax (xsymbols) |
|
20 floor :: "real => int" ("\<lfloor>_\<rfloor>") |
|
21 ceiling :: "real => int" ("\<lceil>_\<rceil>") |
|
22 |
|
23 |
|
24 |
|
25 lemma number_of_less_real_of_int_iff [simp]: |
|
26 "((number_of n) < real (m::int)) = (number_of n < m)" |
|
27 apply auto |
|
28 apply (rule real_of_int_less_iff [THEN iffD1]) |
|
29 apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
|
30 done |
|
31 |
|
32 lemma number_of_less_real_of_int_iff2 [simp]: |
|
33 "(real (m::int) < (number_of n)) = (m < number_of n)" |
|
34 apply auto |
|
35 apply (rule real_of_int_less_iff [THEN iffD1]) |
|
36 apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
|
37 done |
|
38 |
|
39 lemma number_of_le_real_of_int_iff [simp]: |
|
40 "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)" |
|
41 by (simp add: linorder_not_less [symmetric]) |
|
42 |
|
43 lemma number_of_le_real_of_int_iff2 [simp]: |
|
44 "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)" |
|
45 by (simp add: linorder_not_less [symmetric]) |
|
46 |
|
47 lemma floor_zero [simp]: "floor 0 = 0" |
|
48 apply (simp add: floor_def) |
|
49 apply (rule Least_equality, auto) |
|
50 done |
|
51 |
|
52 lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" |
|
53 by auto |
|
54 |
|
55 lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
|
56 apply (simp only: floor_def) |
|
57 apply (rule Least_equality) |
|
58 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
|
59 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
|
60 apply (simp_all add: real_of_int_real_of_nat) |
|
61 done |
|
62 |
|
63 lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
|
64 apply (simp only: floor_def) |
|
65 apply (rule Least_equality) |
|
66 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
|
67 apply (drule_tac [2] real_of_int_minus [THEN subst]) |
|
68 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
|
69 apply (simp_all add: real_of_int_real_of_nat) |
|
70 done |
|
71 |
|
72 lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
|
73 apply (simp only: floor_def) |
|
74 apply (rule Least_equality) |
|
75 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
|
76 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) |
|
77 done |
|
78 |
|
79 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
|
80 apply (simp only: floor_def) |
|
81 apply (rule Least_equality) |
|
82 apply (drule_tac [2] real_of_int_minus [THEN subst]) |
|
83 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
|
84 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) |
|
85 done |
|
86 |
|
87 lemma reals_Archimedean6: |
|
88 "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
|
89 apply (insert reals_Archimedean2 [of r], safe) |
|
90 apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x" |
|
91 in ex_has_least_nat, auto) |
|
92 apply (rule_tac x = x in exI) |
|
93 apply (case_tac x, simp) |
|
94 apply (rename_tac x') |
|
95 apply (drule_tac x = x' in spec, simp) |
|
96 done |
|
97 |
|
98 lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)" |
|
99 by (drule reals_Archimedean6, auto) |
|
100 |
|
101 lemma reals_Archimedean_6b_int: |
|
102 "0 \<le> r ==> \<exists>n. real n \<le> r & r < real ((n::int) + 1)" |
|
103 apply (drule reals_Archimedean6a, auto) |
|
104 apply (rule_tac x = "int n" in exI) |
|
105 apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) |
|
106 done |
|
107 |
|
108 lemma reals_Archimedean_6c_int: |
|
109 "r < 0 ==> \<exists>n. real n \<le> r & r < real ((n::int) + 1)" |
|
110 apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto) |
|
111 apply (rename_tac n) |
|
112 apply (drule real_le_imp_less_or_eq, auto) |
|
113 apply (rule_tac x = "- n - 1" in exI) |
|
114 apply (rule_tac [2] x = "- n" in exI, auto) |
|
115 done |
|
116 |
|
117 lemma real_lb_ub_int: " \<exists>(n::int). real n \<le> r & r < real ((n::int) + 1)" |
|
118 apply (case_tac "r < 0") |
|
119 apply (blast intro: reals_Archimedean_6c_int) |
|
120 apply (simp only: linorder_not_less) |
|
121 apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) |
|
122 done |
|
123 |
|
124 lemma lemma_floor: |
|
125 assumes a1: "real m \<le> r" and a2: "r < real n + 1" |
|
126 shows "m \<le> (n::int)" |
|
127 proof - |
|
128 have "real m < real n + 1" by (rule order_le_less_trans) |
|
129 also have "... = real(n+1)" by simp |
|
130 finally have "m < n+1" by (simp only: real_of_int_less_iff) |
|
131 thus ?thesis by arith |
|
132 qed |
|
133 |
|
134 lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
|
135 apply (simp add: floor_def Least_def) |
|
136 apply (insert real_lb_ub_int [of r], safe) |
|
137 apply (rule theI2, auto) |
|
138 done |
|
139 |
|
140 lemma floor_le: "x < y ==> floor x \<le> floor y" |
|
141 apply (simp add: floor_def Least_def) |
|
142 apply (insert real_lb_ub_int [of x]) |
|
143 apply (insert real_lb_ub_int [of y], safe) |
|
144 apply (rule theI2) |
|
145 apply (rule_tac [3] theI2, auto) |
|
146 done |
|
147 |
|
148 lemma floor_le2: "x \<le> y ==> floor x \<le> floor y" |
|
149 by (auto dest: real_le_imp_less_or_eq simp add: floor_le) |
|
150 |
|
151 lemma lemma_floor2: "real na < real (x::int) + 1 ==> na \<le> x" |
|
152 by (auto intro: lemma_floor) |
|
153 |
|
154 lemma real_of_int_floor_cancel [simp]: |
|
155 "(real (floor x) = x) = (\<exists>n::int. x = real n)" |
|
156 apply (simp add: floor_def Least_def) |
|
157 apply (insert real_lb_ub_int [of x], erule exE) |
|
158 apply (rule theI2) |
|
159 apply (auto intro: lemma_floor) |
|
160 done |
|
161 |
|
162 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
|
163 apply (simp add: floor_def) |
|
164 apply (rule Least_equality) |
|
165 apply (auto intro: lemma_floor) |
|
166 done |
|
167 |
|
168 lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n" |
|
169 apply (simp add: floor_def) |
|
170 apply (rule Least_equality) |
|
171 apply (auto intro: lemma_floor) |
|
172 done |
|
173 |
|
174 lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" |
|
175 apply (rule inj_int [THEN injD]) |
|
176 apply (simp add: real_of_nat_Suc) |
|
177 apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"]) |
|
178 done |
|
179 |
|
180 lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n" |
|
181 apply (drule order_le_imp_less_or_eq) |
|
182 apply (auto intro: floor_eq3) |
|
183 done |
|
184 |
|
185 lemma floor_number_of_eq [simp]: |
|
186 "floor(number_of n :: real) = (number_of n :: int)" |
|
187 apply (subst real_number_of [symmetric]) |
|
188 apply (rule floor_real_of_int) |
|
189 done |
|
190 |
|
191 lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
|
192 apply (simp add: floor_def Least_def) |
|
193 apply (insert real_lb_ub_int [of r], safe) |
|
194 apply (rule theI2) |
|
195 apply (auto intro: lemma_floor) |
|
196 done |
|
197 |
|
198 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
|
199 apply (insert real_of_int_floor_ge_diff_one [of r]) |
|
200 apply (auto simp del: real_of_int_floor_ge_diff_one) |
|
201 done |
|
202 |
|
203 |
|
204 subsection{*Ceiling Function for Positive Reals*} |
|
205 |
|
206 lemma ceiling_zero [simp]: "ceiling 0 = 0" |
|
207 by (simp add: ceiling_def) |
|
208 |
|
209 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" |
|
210 by (simp add: ceiling_def) |
|
211 |
|
212 lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" |
|
213 by auto |
|
214 |
|
215 lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" |
|
216 by (simp add: ceiling_def) |
|
217 |
|
218 lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" |
|
219 by (simp add: ceiling_def) |
|
220 |
|
221 lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" |
|
222 apply (simp add: ceiling_def) |
|
223 apply (subst le_minus_iff, simp) |
|
224 done |
|
225 |
|
226 lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y" |
|
227 by (simp add: floor_le ceiling_def) |
|
228 |
|
229 lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y" |
|
230 by (simp add: floor_le2 ceiling_def) |
|
231 |
|
232 lemma real_of_int_ceiling_cancel [simp]: |
|
233 "(real (ceiling x) = x) = (\<exists>n::int. x = real n)" |
|
234 apply (auto simp add: ceiling_def) |
|
235 apply (drule arg_cong [where f = uminus], auto) |
|
236 apply (rule_tac x = "-n" in exI, auto) |
|
237 done |
|
238 |
|
239 lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" |
|
240 apply (simp add: ceiling_def) |
|
241 apply (rule minus_equation_iff [THEN iffD1]) |
|
242 apply (simp add: floor_eq [where n = "-(n+1)"]) |
|
243 done |
|
244 |
|
245 lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1" |
|
246 by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"]) |
|
247 |
|
248 lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n" |
|
249 by (simp add: ceiling_def floor_eq2 [where n = "-n"]) |
|
250 |
|
251 lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" |
|
252 by (simp add: ceiling_def) |
|
253 |
|
254 lemma ceiling_number_of_eq [simp]: |
|
255 "ceiling (number_of n :: real) = (number_of n)" |
|
256 apply (subst real_number_of [symmetric]) |
|
257 apply (rule ceiling_real_of_int) |
|
258 done |
|
259 |
|
260 lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r" |
|
261 apply (rule neg_le_iff_le [THEN iffD1]) |
|
262 apply (simp add: ceiling_def diff_minus) |
|
263 done |
|
264 |
|
265 lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" |
|
266 apply (insert real_of_int_ceiling_diff_one_le [of r]) |
|
267 apply (simp del: real_of_int_ceiling_diff_one_le) |
|
268 done |
|
269 |
|
270 ML |
|
271 {* |
|
272 val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff"; |
|
273 val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2"; |
|
274 val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff"; |
|
275 val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2"; |
|
276 val floor_zero = thm "floor_zero"; |
|
277 val floor_real_of_nat_zero = thm "floor_real_of_nat_zero"; |
|
278 val floor_real_of_nat = thm "floor_real_of_nat"; |
|
279 val floor_minus_real_of_nat = thm "floor_minus_real_of_nat"; |
|
280 val floor_real_of_int = thm "floor_real_of_int"; |
|
281 val floor_minus_real_of_int = thm "floor_minus_real_of_int"; |
|
282 val reals_Archimedean6 = thm "reals_Archimedean6"; |
|
283 val reals_Archimedean6a = thm "reals_Archimedean6a"; |
|
284 val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int"; |
|
285 val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int"; |
|
286 val real_lb_ub_int = thm "real_lb_ub_int"; |
|
287 val lemma_floor = thm "lemma_floor"; |
|
288 val real_of_int_floor_le = thm "real_of_int_floor_le"; |
|
289 val floor_le = thm "floor_le"; |
|
290 val floor_le2 = thm "floor_le2"; |
|
291 val lemma_floor2 = thm "lemma_floor2"; |
|
292 val real_of_int_floor_cancel = thm "real_of_int_floor_cancel"; |
|
293 val floor_eq = thm "floor_eq"; |
|
294 val floor_eq2 = thm "floor_eq2"; |
|
295 val floor_eq3 = thm "floor_eq3"; |
|
296 val floor_eq4 = thm "floor_eq4"; |
|
297 val floor_number_of_eq = thm "floor_number_of_eq"; |
|
298 val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one"; |
|
299 val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge"; |
|
300 val ceiling_zero = thm "ceiling_zero"; |
|
301 val ceiling_real_of_nat = thm "ceiling_real_of_nat"; |
|
302 val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero"; |
|
303 val ceiling_floor = thm "ceiling_floor"; |
|
304 val floor_ceiling = thm "floor_ceiling"; |
|
305 val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge"; |
|
306 val ceiling_le = thm "ceiling_le"; |
|
307 val ceiling_le2 = thm "ceiling_le2"; |
|
308 val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel"; |
|
309 val ceiling_eq = thm "ceiling_eq"; |
|
310 val ceiling_eq2 = thm "ceiling_eq2"; |
|
311 val ceiling_eq3 = thm "ceiling_eq3"; |
|
312 val ceiling_real_of_int = thm "ceiling_real_of_int"; |
|
313 val ceiling_number_of_eq = thm "ceiling_number_of_eq"; |
|
314 val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le"; |
|
315 val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one"; |
|
316 *} |
|
317 |
|
318 |
17 end |
319 end |