intrealScript.sml
1(* -------------------------------------------------------------------------
2 A bridging theory between integers and reals
3 ------------------------------------------------------------------------- *)
4Theory intreal
5Ancestors
6 arithmetic integer real
7Libs
8 intLib RealArith hurdUtils realSimps[qualified]
9
10
11(* -------------------------------------------------------------------------
12 Define the inclusion homomorphism real_of_int :int->real.
13 ------------------------------------------------------------------------- *)
14
15Definition real_of_int:
16 real_of_int i =
17 if i < 0 then ~(real_of_num (Num (~i))) else real_of_num (Num i)
18End
19
20Theorem real_of_int_def = real_of_int;
21
22(* -------------------------------------------------------------------------
23 Floor and ceiling (ints)
24 ------------------------------------------------------------------------- *)
25
26Definition INT_FLOOR_def[nocompute]:
27 INT_FLOOR x = LEAST_INT i. x < real_of_int (i + 1)
28End
29Definition INT_CEILING_def[nocompute]:
30 INT_CEILING x = LEAST_INT i. x <= real_of_int i
31End
32
33Overload flr = “INT_FLOOR”
34Overload clg = “INT_CEILING”
35
36val _ = add_rule {
37 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
38 fixity = Closefix,
39 paren_style = OnlyIfNecessary,
40 pp_elements = [TOK UnicodeChars.clgl, TM, TOK UnicodeChars.clgr],
41 term_name = "clgtoks"}
42Overload clgtoks = “INT_CEILING”
43
44val _ = add_rule {
45 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
46 fixity = Closefix,
47 paren_style = OnlyIfNecessary,
48 pp_elements = [TOK UnicodeChars.flrl, TM, TOK UnicodeChars.flrr],
49 term_name = "flrtoks"}
50Overload flrtoks = “INT_FLOOR”
51
52
53(* -------------------------------------------------------------------------
54 is_int
55 ------------------------------------------------------------------------- *)
56
57Definition is_int_def: is_int (x:real) <=> x = real_of_int (INT_FLOOR x)
58End
59
60(* -------------------------------------------------------------------------
61 Theorems
62 ------------------------------------------------------------------------- *)
63
64Theorem real_of_int_monotonic:
65 !i j. i < j ==> real_of_int i < real_of_int j
66Proof
67 Cases \\ Cases \\ srw_tac[][real_of_int] \\ ARITH_TAC
68QED
69
70val real_arch_least1 =
71 REAL_ARCH_LEAST
72 |> Q.SPEC `1r`
73 |> SIMP_RULE (srw_ss()) []
74
75val Num_suc1 = ARITH_PROVE ``Num (&n + 1) = n + 1``
76
77Theorem lem[local]:
78 !n. -&n <= 0r
79Proof simp [REAL_NEG_LE0]
80QED
81
82Theorem lem2[local]:
83 !n. -&(n + 1n) = -&n - 1r
84Proof
85 once_rewrite_tac [GSYM add_ints]
86 \\ simp [real_sub]
87QED
88
89val lem3 = ARITH_PROVE ``-&n + 1 < 0i ==> (Num (&n + -1i) = (n - 1))``
90
91Theorem lem4[local]:
92 !n. n <> 0 ==> (-&(n - 1n) = -&n + 1r)
93Proof
94 strip_tac
95 \\ Cases_on `n = 1` >- simp []
96 \\ metis_tac [REAL_SUB, REAL_NEG_SUB,
97 REAL_ARITH ``-a + b = b - a: real``,
98 DECIDE ``n <> 0 /\ n <> 1 ==> (n - 1 <> 0n)``]
99QED
100
101Theorem lem5[local]:
102 !m n. n + 1 < m ==> -&m + 1 <= -&n - 1r
103Proof
104 REPEAT strip_tac
105 \\ once_rewrite_tac [GSYM REAL_LE_NEG]
106 \\ rewrite_tac [REAL_NEG_SUB, REAL_NEG_ADD,
107 REAL_SUB_RNEG]
108 \\ Cases_on `m`
109 \\ full_simp_tac(srw_ss())[arithmeticTheory.ADD1]
110 \\ REWRITE_TAC [GSYM REAL_ADD,
111 REAL_ARITH ``a + b + -b = a: real``]
112 \\ simp []
113QED
114
115(* cf. INT_FLOOR_BOUNDS' for another form where ‘real_of_int (INT_FLOOR r)’
116 stays in the middle.
117 *)
118Theorem INT_FLOOR_BOUNDS :
119 !r. real_of_int (INT_FLOOR r) <= r /\ r < real_of_int (INT_FLOOR r + 1)
120Proof
121 srw_tac[][INT_FLOOR_def, LEAST_INT_DEF] \\ SELECT_ELIM_TAC \\ (
122 REVERSE conj_tac
123 >- (srw_tac[][REAL_NOT_LT]
124 \\ pop_assum (qspec_then `x - 1` assume_tac)
125 \\ full_simp_tac(srw_ss())[ARITH_PROVE ``a - 1 < a: int``])
126 \\ Cases_on `0 <= r`
127 >- (imp_res_tac real_arch_least1
128 \\ qexists_tac `&n`
129 \\ srw_tac[][real_of_int, REAL_NOT_LT,
130 REWRITE_RULE [GSYM arithmeticTheory.ADD1] Num_suc1,
131 ARITH_PROVE ``~(&n + 1i < 0)``]
132 >- metis_tac [lem, REAL_LE_TRANS]
133 \\ Cases_on `i'`
134 \\ full_simp_tac(srw_ss())[Num_suc1]
135 >| [`n' + 1 <= n` by decide_tac
136 \\ metis_tac [REAL_LE, REAL_LE_TRANS],
137 imp_res_tac
138 (ARITH_PROVE ``n <> 0 /\ ~(-&n + 1i < 0) ==> (n = 1)``)
139 \\ full_simp_tac(srw_ss())[],
140 `1 <= n` by decide_tac
141 \\ metis_tac [REAL_LE, REAL_LE_TRANS]
142 ]
143 )
144 \\ imp_res_tac (REAL_ARITH ``~(0r <= r) ==> 0 <= -r /\ r <> 0``)
145 \\ imp_res_tac real_arch_least1
146 \\ rev_full_simp_tac(srw_ss())[arithmeticTheory.ADD1, INT_NEG_ADD,
147 REAL_ARITH ``r <= 0r ==> (&(n: num) <= -r <=> r <= -&n)``,
148 REAL_ARITH ``r <= 0r ==> (-r < &n <=> -&n < r)``]
149 \\ Cases_on `r = -&n`
150 >| [qexists_tac `~&n`, qexists_tac `~&(SUC n)`]
151 \\ rev_full_simp_tac(srw_ss())[real_of_int, INT_NEG_ADD]
152 \\ (conj_tac
153 >- (srw_tac[][lem3]
154 \\ Cases_on `n`
155 \\ full_simp_tac(srw_ss())[arithmeticTheory.ADD1,
156 REAL_ARITH ``r <= 0r /\ r <> 0 ==> r < 0``,
157 REAL_ARITH ``a <= b - 1 ==> a < b: real``,
158 ARITH_PROVE ``-&(n + 1) + 1 < 0i <=> n <> 0``,
159 REAL_ARITH ``r <= -1r ==> r < 0``,
160 REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``])
161 \\ srw_tac[][REAL_NOT_LT]
162 \\ Cases_on `i'`
163 \\ rev_full_simp_tac(srw_ss())[lem2, lem3, lem4, arithmeticTheory.ADD1]
164 \\ (ARITH_TAC ORELSE
165 imp_res_tac (ARITH_PROVE ``n + 1 < m ==> (-&m + 1 < 0i)``)
166 \\ metis_tac
167 [REAL_LET_TRANS, REAL_LT_IMP_LE, lem5])
168 )
169 )
170QED
171
172Theorem INT_FLOOR:
173 !r i. (INT_FLOOR r = i) <=> real_of_int i <= r /\ r < real_of_int (i + 1)
174Proof
175 REPEAT strip_tac
176 \\ eq_tac
177 >- metis_tac [INT_FLOOR_BOUNDS]
178 \\ srw_tac[][INT_FLOOR_def, LEAST_INT_DEF]
179 \\ SELECT_ELIM_TAC
180 \\ conj_tac
181 >- (
182 SPOSE_NOT_THEN strip_assume_tac
183 \\ res_tac
184 \\ Cases_on `i`
185 \\ Cases_on `i'`
186 \\ full_simp_tac(srw_ss())[real_of_int, ARITH_PROVE ``~(&n + 1i < 0)``]
187 >| [
188 all_tac,
189 Cases_on `-&n' + 1 < 0i`,
190 all_tac,
191 Cases_on `-&n' + 1 < 0i`,
192 Cases_on `-&n + 1 < 0i`
193 ]
194 \\ full_simp_tac(srw_ss())[Num_suc1]
195 \\ imp_res_tac REAL_LET_TRANS
196 \\ full_simp_tac(srw_ss())[INT_NOT_LT]
197 \\ ARITH_TAC
198 )
199 \\ srw_tac[][]
200 \\ Cases_on `i < x`
201 >- res_tac
202 \\ Cases_on `i = x`
203 >- asm_rewrite_tac []
204 \\ `x < i` by ARITH_TAC
205 \\ Cases_on `i`
206 \\ Cases_on `x`
207 \\ full_simp_tac(srw_ss())[real_of_int]
208 >| [
209 Cases_on `&n + 1 < 0i`
210 \\ Cases_on `&n' + 1 < 0i`,
211 Cases_on `&n + 1 < 0i`
212 \\ Cases_on `-&n' + 1 < 0i`,
213 Cases_on `&n + 1 < 0i`,
214 Cases_on `-&n + 1 < 0i`
215 \\ Cases_on `-&n' + 1 < 0i`,
216 Cases_on `-&n + 1 < 0i`
217 ]
218 \\ full_simp_tac(srw_ss())[]
219 \\ imp_res_tac REAL_LET_TRANS
220 \\ full_simp_tac(srw_ss())[INT_NOT_LT]
221 \\ ARITH_TAC
222QED
223
224Theorem int_floor_1[simp]:
225 (INT_FLOOR &n = &n) /\ (INT_FLOOR (-&n) = -&n)
226Proof
227 srw_tac[][INT_FLOOR, real_of_int] \\ ARITH_TAC
228QED
229
230val tac =
231 imp_res_tac arithmeticTheory.DIVISION
232 \\ pop_assum (qspec_then `n` assume_tac)
233 \\ first_assum (qspec_then `n` assume_tac)
234 \\ TRY decide_tac
235
236Theorem int_floor_2[local]:
237 0 < m ==> (INT_FLOOR (&n / &m) = &n / &m)
238Proof
239 strip_tac
240 \\ rewrite_tac [INT_FLOOR]
241 \\ srw_tac[][real_of_int, le_ratr, lt_ratl, Num_suc1]
242 \\ TRY decide_tac
243 >- tac
244 >- ARITH_TAC
245 \\ tac
246QED
247
248val lem1 =
249 metisLib.METIS_PROVE
250 [REAL_POS_NZ, REAL_DIV_REFL, neg_rat]
251 ``!a. 0r < a ==> (-a / a = -1)``
252
253Theorem lem2[local]:
254 !n. 0n < n ==> (-&n / &n = -1i)
255Proof
256 REPEAT strip_tac
257 \\ `0i < &n` by ARITH_TAC
258 \\ simp [int_div]
259QED
260
261Theorem lem3[local]:
262 !n m. 0n < n /\ n < m ==> (-&n / &m = -1i)
263Proof
264 REPEAT strip_tac
265 \\ `0i < &n` by ARITH_TAC
266 \\ simp [int_div, arithmeticTheory.LESS_DIV_EQ_ZERO]
267QED
268
269val tac2 =
270 metis_tac [arithmeticTheory.X_MOD_Y_EQ_X, DECIDE ``x < y ==> ~(y < x:num)``]
271
272Theorem lem4[local]:
273 !n m. 0 < m /\ m < n ==> -&n / &m < -1i
274Proof
275 NTAC 3 strip_tac
276 \\ `&m <> 0i` by ARITH_TAC
277 \\ simp [int_div]
278 \\ srw_tac[][ARITH_PROVE ``a + -1 < -1 <=> a < 0i``]
279 \\ tac
280 >- (SPOSE_NOT_THEN strip_assume_tac
281 \\ `(n DIV m = 0) \/ (n DIV m = 1)` by decide_tac
282 \\ full_simp_tac(srw_ss())[]
283 >- tac2
284 \\ decide_tac
285 )
286 \\ strip_tac
287 \\ full_simp_tac(srw_ss())[]
288 \\ tac2
289QED
290
291Theorem lem5[local]:
292 !n m. 0n < m /\ n <> 0 /\ (n MOD m = 0) /\ n <> m ==> 1 < n DIV m
293Proof
294 srw_tac[][arithmeticTheory.X_LT_DIV]
295 \\ imp_res_tac arithmeticTheory.MOD_EQ_0_DIVISOR
296 \\ Cases_on `d = 0` >- full_simp_tac(srw_ss())[]
297 \\ Cases_on `d = 1` >- full_simp_tac(srw_ss())[]
298 \\ `2 <= d` by decide_tac
299 \\ metis_tac [arithmeticTheory.LESS_MONO_MULT]
300QED
301
302Theorem int_floor_3[local]:
303 0 < m ==> (INT_FLOOR (-&n / &m) = -&n / &m)
304Proof
305 strip_tac
306 \\ rewrite_tac [INT_FLOOR]
307 \\ Cases_on `n = 0`
308 >- simp [real_of_int, arithmeticTheory.ZERO_DIV]
309 \\ Cases_on `n = m`
310 >- simp [lem1, lem2, real_of_int]
311 \\ Cases_on `n < m`
312 >- simp [lem3, real_of_int, le_ratr, lt_ratl]
313 \\ `m < n` by decide_tac
314 \\ simp [lem4, real_of_int, le_ratr, lt_ratl,
315 ARITH_PROVE ``a < -1i ==> a < 0 /\ a + 1 < 0``]
316 \\ simp [int_div]
317 \\ srw_tac[][INT_NEG_ADD, lem5, Num_suc1,
318 ARITH_PROVE ``a + 1 + -1 = a: int``,
319 ARITH_PROVE ``1n < a ==> (Num (&a + -1) = a - 1)``]
320 \\ tac
321QED
322
323Theorem INT_CEILING_IMP[local]:
324 !r i. real_of_int (i - 1) < r /\ r <= real_of_int i ==> (INT_CEILING r = i)
325Proof
326 srw_tac[][INT_CEILING_def, LEAST_INT_DEF]
327 \\ SELECT_ELIM_TAC
328 \\ conj_tac
329 >- (
330 SPOSE_NOT_THEN STRIP_ASSUME_TAC
331 \\ res_tac
332 \\ Cases_on `i`
333 \\ Cases_on `i'`
334 \\ full_simp_tac(srw_ss())[real_of_int]
335 >| [
336 Cases_on `&n - 1 < 0i`,
337 Cases_on `&n - 1 < 0i`,
338 Cases_on `&n - 1 < 0i`,
339 Cases_on `-&n - 1 < 0i`,
340 all_tac
341 ]
342 \\ full_simp_tac(srw_ss())[]
343 \\ imp_res_tac REAL_LTE_TRANS
344 \\ full_simp_tac(srw_ss())[]
345 \\ ARITH_TAC
346 )
347 \\ srw_tac[][]
348 \\ Cases_on `i < x`
349 >- res_tac
350 \\ Cases_on `i = x`
351 >- asm_rewrite_tac []
352 \\ `x < i` by ARITH_TAC
353 \\ Cases_on `i`
354 \\ Cases_on `x`
355 \\ full_simp_tac(srw_ss())[real_of_int]
356 >| [
357 Cases_on `&n - 1 < 0i`,
358 Cases_on `&n - 1 < 0i`,
359 Cases_on `&n - 1 < 0i`,
360 Cases_on `-&n - 1 < 0i`,
361 all_tac
362 ]
363 \\ full_simp_tac(srw_ss())[]
364 \\ imp_res_tac REAL_LTE_TRANS
365 \\ full_simp_tac(srw_ss())[]
366 \\ ARITH_TAC
367QED
368
369Theorem INT_CEILING_INT_FLOOR:
370 !r. INT_CEILING r =
371 let i = INT_FLOOR r in if real_of_int i = r then i else i + 1
372Proof
373 lrw []
374 \\ match_mp_tac INT_CEILING_IMP
375 >- (`INT_FLOOR r - 1 < INT_FLOOR r` by ARITH_TAC
376 \\ imp_res_tac real_of_int_monotonic
377 \\ simp []
378 \\ metis_tac [INT_FLOOR_BOUNDS, REAL_LTE_TRANS])
379 \\ simp [ARITH_PROVE ``a + 1 -1i = a``,
380 REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``,
381 INT_FLOOR_BOUNDS, REAL_LT_IMP_LE]
382QED
383
384(* cf. INT_CEILING_BOUNDS' for another form where ‘real_of_int (INT_CEILING r)’
385 stays in the middle.
386 *)
387Theorem INT_CEILING_BOUNDS :
388 !r. real_of_int (INT_CEILING r - 1) < r /\ r <= real_of_int (INT_CEILING r)
389Proof
390 lrw [INT_CEILING_INT_FLOOR, INT_FLOOR_BOUNDS, REAL_LT_IMP_LE,
391 ARITH_PROVE ``a + 1i - 1 = a``,
392 REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``]
393 \\ pop_assum (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [SYM th])))
394 \\ match_mp_tac real_of_int_monotonic
395 \\ ARITH_TAC
396QED
397
398Theorem INT_CEILING:
399 !r i. (INT_CEILING r = i) <=> real_of_int (i - 1) < r /\ r <= real_of_int i
400Proof
401 metis_tac [INT_CEILING_BOUNDS, INT_CEILING_IMP]
402QED
403
404
405Theorem real_of_int_num[simp]:
406 real_of_int (& n) = &n
407Proof
408 rewrite_tac[real_of_int_def]
409 \\ Cases_on `(&n):int`
410 \\ fs []
411QED
412
413local
414 fun crossprod [] ys = []
415 | crossprod (x::xs) ys = map (fn y => [x, y]) ys @ crossprod xs ys
416 val n = mk_var("n", numSyntax.num) and m = mk_var("m", numSyntax.num)
417 fun nb1 v = mk_comb(numSyntax.numeral_tm, mk_comb(numSyntax.bit1_tm, v))
418 fun nb2 v = mk_comb(numSyntax.numeral_tm, mk_comb(numSyntax.bit2_tm, v))
419 val insts = crossprod [n |-> nb1 n, n |-> nb2 n] [m |-> nb1 m, m |-> nb2 m]
420 val rule =
421 REWRITE_RULE [numeralTheory.numeral_distrib, numeralTheory.numeral_lt]
422 fun r th = LIST_CONJ (map (fn i => rule (INST i th)) insts)
423 val (t1, t2) = Drule.CONJ_PAIR int_floor_1
424 val icif = INT_CEILING_INT_FLOOR
425 open realSyntax
426in
427Theorem INT_FLOOR_EQNS =
428 LIST_CONJ (map GEN_ALL [t1, t2, int_floor_2, int_floor_3])
429Theorem INT_FLOOR_compute[compute,simp] =
430 LIST_CONJ [t1,t2, r int_floor_2, r int_floor_3]
431Theorem INT_CEILING_COMPUTE[compute,simp] =
432 LIST_CONJ [SPEC (realSyntax.term_of_int Arbint.zero) icif
433 |> SIMP_RULE bool_ss [t1, LET_THM, real_of_int_num],
434 SPEC (mk_injected m) icif,
435 SPEC (mk_negated (mk_injected m)) icif,
436 r (SPEC (mk_div (mk_injected m, mk_injected n)) icif),
437 r (SPEC (mk_div(mk_negated (mk_injected m), mk_injected n))
438 icif)]
439val () = () (* makes Theorem syntax work *)
440end (* local *)
441
442Theorem real_of_int_add[simp]:
443 real_of_int (m + n) = real_of_int m + real_of_int n
444Proof
445 Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
446 \\ fs [INT_ADD_CALCULATE]
447 \\ rw [] \\ fs [] \\ fs [GSYM NOT_LESS,add_ints]
448QED
449
450Theorem real_of_int_neg[simp]:
451 real_of_int (-m) = -real_of_int m
452Proof
453 Cases_on `m` \\ fs [real_of_int_def]
454QED
455
456Theorem real_of_int_sub[simp]:
457 real_of_int (m - n) = real_of_int m - real_of_int n
458Proof
459 fs [int_sub,real_sub]
460QED
461
462Theorem real_of_int_mul[simp]:
463 real_of_int (m * n) = real_of_int m * real_of_int n
464Proof
465 Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
466 \\ fs [INT_MUL_CALCULATE]
467QED
468
469Theorem real_of_int_lt[simp]:
470 real_of_int m < real_of_int n <=> m < n
471Proof
472 simp[real_of_int_def] >> map_every Cases_on [‘m’, ‘n’] >>
473 simp[]
474QED
475
476Theorem real_of_int_11[simp]:
477 (real_of_int m = real_of_int n) <=> (m = n)
478Proof
479 simp[real_of_int_def] >> map_every Cases_on [‘m’, ‘n’] >>
480 simp[]
481QED
482
483Theorem real_of_int_le[simp]:
484 real_of_int m <= real_of_int n <=> m <= n
485Proof
486 simp[REAL_LE_LT, INT_LE_LT]
487QED
488
489Theorem INT_FLOOR_MONO:
490 x < y ==> INT_FLOOR x <= INT_FLOOR y
491Proof
492 CCONTR_TAC >> gs[INT_NOT_LE] >>
493 ‘flr y + 1i <= flr x’ by simp[GSYM INT_LT_LE1] >>
494 ‘y < real_of_int (flr y + 1)’ by simp[INT_FLOOR_BOUNDS] >>
495 ‘real_of_int (flr x) <= x’ by simp[INT_FLOOR_BOUNDS] >>
496 metis_tac[REAL_LET_TRANS, REAL_LTE_TRANS,
497 REAL_LT_TRANS,
498 real_of_int_le, REAL_LT_REFL]
499QED
500
501Theorem INT_FLOOR_SUCa[local]:
502 INT_FLOOR r + 1 <= INT_FLOOR (r + 1)
503Proof
504 CCONTR_TAC >> gs[INT_NOT_LE] >>
505 ‘INT_FLOOR (r + 1) + 1 <= INT_FLOOR r + 1’ by gs[INT_LT_LE1] >>
506 ‘real_of_int (flr r) + 1 <= r + 1’ by simp[INT_FLOOR_BOUNDS] >>
507 ‘r + 1 < real_of_int (flr (r + 1) + 1)’ by simp[INT_FLOOR_BOUNDS] >>
508 ‘real_of_int(flr (r + 1) + 1) <= real_of_int (flr r + 1)’ by simp[] >>
509 ‘r + 1 < real_of_int (flr r + 1)’ by metis_tac[REAL_LTE_TRANS] >>
510 metis_tac[real_of_int_num, REAL_LTE_TRANS, REAL_LT_REFL,
511 real_of_int_add]
512QED
513
514Theorem INT_FLOOR_SUCb[local]:
515 INT_FLOOR (r + 1) <= INT_FLOOR r + 1
516Proof
517 CCONTR_TAC >> gs[INT_NOT_LE] >>
518 qabbrev_tac ‘i = (flr r:int) + 1’ >> qabbrev_tac ‘j:int = flr (r + 1)’ >>
519 ‘i + 1 <= j’ by gs[INT_LT_LE1] >>
520 ‘r < real_of_int i’ by simp[INT_FLOOR_BOUNDS, Abbr‘i’] >>
521 ‘real_of_int j <= r + 1’ by simp[INT_FLOOR_BOUNDS, Abbr‘j’] >>
522 ‘r + 1 < real_of_int j’
523 by (irule REAL_LTE_TRANS >>
524 irule_at Any (iffRL real_of_int_le) >> first_assum $ irule_at Any >>
525 simp[]) >>
526 metis_tac[REAL_LTE_TRANS, REAL_LT_REFL]
527QED
528
529Theorem INT_FLOOR_SUC:
530 INT_FLOOR (x + 1) = INT_FLOOR x + 1
531Proof
532 simp[GSYM INT_LE_ANTISYM, INT_FLOOR_SUCb, INT_FLOOR_SUCa]
533QED
534
535Theorem INT_FLOOR_SUB1:
536 INT_FLOOR (x - 1) = INT_FLOOR x - 1
537Proof
538 simp[INT_EQ_SUB_LADD, GSYM INT_FLOOR_SUC,
539 REAL_ARITH “x - 1r + 1 = x”]
540QED
541
542Theorem INT_FLOOR_SUM_NUM[simp]:
543 INT_FLOOR (x + &n) = INT_FLOOR x + &n /\
544 INT_FLOOR (&n + x) = INT_FLOOR x + &n
545Proof
546 csimp[REAL_ADD_COMM] >>
547 Induct_on‘n’>>
548 simp[REAL, GSYM REAL_ADD, Excl "REAL_ADD",
549 INT, REAL_ADD_ASSOC, INT_FLOOR_SUC,
550 INT_ADD_ASSOC
551 ]
552QED
553
554(* Add an alias for better naming *)
555Theorem INT_FLOOR_ADD_NUM = INT_FLOOR_SUM_NUM
556
557Theorem INT_FLOOR_SUB_NUM[simp]:
558 INT_FLOOR (x - &n) = INT_FLOOR x - &n /\
559 INT_FLOOR (&n - x) = INT_FLOOR (-x) + &n
560Proof
561 reverse conj_tac >- simp[real_sub] >>
562 Induct_on ‘n’ >>
563 simp[REAL, Excl "REAL_ADD", GSYM REAL_ADD,
564 REAL_ARITH “x - (y + z) = x - y - z:real”, INT_FLOOR_SUB1,
565 INT] >>
566 ARITH_TAC
567QED
568
569Theorem INT_FLOOR_SUM[simp]:
570 INT_FLOOR (x + real_of_int y) = INT_FLOOR x + y /\
571 INT_FLOOR (real_of_int y + x) = INT_FLOOR x + y
572Proof
573 csimp[REAL_ADD_COMM] >>
574 Cases_on ‘y’ >> simp[GSYM real_sub, GSYM int_sub]
575QED
576
577Theorem INT_NUM_CEILING:
578 !r. 0 <= r ==> &realax$NUM_CEILING r = INT_CEILING r
579Proof
580 rw[INT_CEILING]
581 >- metis_tac[NUM_CEILING_UPPER_BOUND, REAL_LT_SUB_RADD]
582 >> metis_tac[LE_NUM_CEILING]
583QED
584
585Theorem INT_NUM_FLOOR:
586 !r. 0 <= r ==> &realax$NUM_FLOOR r = INT_FLOOR r
587Proof
588 rw[INT_FLOOR]
589 >- metis_tac[NUM_FLOOR_LE]
590 >> metis_tac[NUM_FLOOR_LT, REAL_ADD, REAL_LT_SUB_RADD]
591QED
592
593Theorem ints_exist_in_gaps:
594 !a b. a + 1 < b ==> ?i. a < real_of_int i /\ real_of_int i < b
595Proof
596 rpt strip_tac >> irule_at Any (cj 2 INT_FLOOR_BOUNDS) >> simp[] >>
597 irule REAL_LET_TRANS >> first_assum $ irule_at Any >>
598 simp[INT_FLOOR_BOUNDS]
599QED
600
601(* Alternative definition of is_int by INT_CEILING *)
602Theorem is_int_alt :
603 !x. is_int x <=> x = real_of_int (INT_CEILING x)
604Proof
605 rw [is_int_def]
606 >> EQ_TAC >- rw [INT_CEILING_INT_FLOOR]
607 >> DISCH_TAC
608 >> CCONTR_TAC
609 >> fs [INT_CEILING_INT_FLOOR]
610 >> ‘1 = real_of_int 1’ by rw [real_of_int_num, real_of_num]
611 >> METIS_TAC [REAL_LT_IMP_NE, INT_FLOOR_BOUNDS, real_of_int_add]
612QED
613
614Theorem is_int_thm_lemma[local] :
615 !x. is_int x <=> real_of_int (INT_FLOOR x) = real_of_int (INT_CEILING x)
616Proof
617 Q.X_GEN_TAC ‘x’
618 >> EQ_TAC >- METIS_TAC [is_int_def, is_int_alt]
619 >> DISCH_TAC
620 >> Suff ‘real_of_int (INT_FLOOR x) = x’ >- rw [GSYM is_int_def]
621 >> CCONTR_TAC
622 >> fs [INT_CEILING_INT_FLOOR]
623 >> Suff ‘INT_FLOOR x < INT_FLOOR x + 1’ >- PROVE_TAC [INT_LT_IMP_NE]
624 >> rw [INT_LT_ADDR]
625QED
626
627Theorem is_int_thm :
628 !x. is_int x <=> INT_FLOOR x = INT_CEILING x
629Proof
630 rw [is_int_thm_lemma, real_of_int_11]
631QED
632
633Theorem INT_CEILING_ADD_NUM :
634 INT_CEILING (x + &n) = INT_CEILING x + &n /\
635 INT_CEILING (&n + x) = INT_CEILING x + &n
636Proof
637 CONJ_TAC >> simp [INT_CEILING_INT_FLOOR]
638 >| [ (* goal 1 (of 2) *)
639 Cases_on ‘real_of_int (INT_FLOOR x) = x’ >> simp [] \\
640 ARITH_TAC,
641 (* goal 2 (of 2) *)
642 Cases_on ‘real_of_int (INT_FLOOR x) = x’ >> simp []
643 >- PROVE_TAC [REAL_ADD_COMM] \\
644 ‘&n + x = x + &n’ by PROVE_TAC [REAL_ADD_COMM] >> POP_ORW \\
645 simp [] >> ARITH_TAC ]
646QED
647
648Theorem INT_CEILING_SUB_NUM :
649 INT_CEILING (x - &n) = INT_CEILING x - &n /\
650 INT_CEILING (&n - x) = INT_CEILING (-x) + &n
651Proof
652 CONJ_TAC >> simp [INT_CEILING_INT_FLOOR]
653 >| [ (* goal 1 (of 2) *)
654 Cases_on ‘real_of_int (INT_FLOOR x) = x’ >> simp [real_sub] \\
655 ARITH_TAC,
656 (* goal 2 (of 2) *)
657 Cases_on ‘real_of_int (INT_FLOOR ~x) = ~x’ >> simp [real_sub]
658 >- PROVE_TAC [REAL_ADD_COMM] \\
659 ‘&n + -x = -x + &n’ by PROVE_TAC [REAL_ADD_COMM] >> POP_ORW \\
660 simp [] >> ARITH_TAC ]
661QED
662
663Theorem INT_CEILING_BOUNDS' :
664 !r. r <= real_of_int (INT_CEILING r) /\ real_of_int (INT_CEILING r) < r + 1
665Proof
666 rw [INT_CEILING_BOUNDS]
667 >> Suff ‘real_of_int (INT_CEILING r) - 1 < r’ >- rw [REAL_LT_SUB_RADD]
668 >> Suff ‘real_of_int (INT_CEILING r) - 1 = real_of_int (INT_CEILING r - 1)’
669 >- (Rewr' >> REWRITE_TAC [INT_CEILING_BOUNDS])
670 >> rw [real_of_num, INT_CEILING_SUB_NUM]
671QED
672
673Theorem INT_FLOOR_BOUNDS' :
674 !r. r - 1 < real_of_int (INT_FLOOR r) /\ real_of_int (INT_FLOOR r) <= r
675Proof
676 rw [INT_FLOOR_BOUNDS]
677 >> Suff ‘r < real_of_int (INT_FLOOR r) + 1’ >- rw [REAL_LT_SUB_RADD]
678 >> Suff ‘real_of_int (INT_FLOOR r) + 1 = real_of_int (INT_FLOOR r + 1)’
679 >- (Rewr' >> REWRITE_TAC [INT_FLOOR_BOUNDS])
680 >> rw [real_of_num, INT_CEILING_ADD_NUM]
681QED
682
683Theorem INT_FLOOR':
684 !r i. (INT_FLOOR r = i) <=> r - 1 < real_of_int i /\ real_of_int i <= r
685Proof
686 rw [INT_FLOOR]
687 >> Suff ‘r < real_of_int i + 1 <=> r - 1 < real_of_int i’ >- METIS_TAC []
688 >> simp [REAL_LT_SUB_RADD]
689QED
690
691Theorem INT_CEILING':
692 !r i. (INT_CEILING r = i) <=> r <= real_of_int i /\ real_of_int i < r + 1
693Proof
694 rw [INT_CEILING]
695 >> Suff ‘real_of_int i - 1 < r <=> real_of_int i < r + 1’ >- METIS_TAC []
696 >> simp [REAL_LT_SUB_RADD]
697QED
698
699(* https://proofwiki.org/wiki/Floor_of_Negative_equals_Negative_of_Ceiling *)
700Theorem INT_FLOOR_NEG :
701 !x. INT_FLOOR (~x) = ~INT_CEILING x
702Proof
703 Q.X_GEN_TAC ‘x’
704 >> simp [INT_FLOOR', INT_CEILING_BOUNDS']
705 >> ‘-x - 1 = ~(x + 1)’ by REAL_ARITH_TAC >> POP_ORW
706 >> simp [REAL_LT_NEG, INT_CEILING_BOUNDS']
707QED
708
709Theorem INT_CEILING_NEG :
710 !x. INT_CEILING (~x) = ~INT_FLOOR x
711Proof
712 Q.X_GEN_TAC ‘x’
713 >> simp [INT_CEILING', INT_FLOOR_BOUNDS']
714 >> ‘-x + 1 = ~(x - 1)’ by REAL_ARITH_TAC >> POP_ORW
715 >> simp [REAL_LT_NEG, INT_FLOOR_BOUNDS']
716QED
717
718(*---------------------------------------------------------------------------*
719 * Fractional part *
720 *---------------------------------------------------------------------------*)
721
722 (* ‘frac x’ to mean x mod 1 or ‘x - flr x’, the fractional part of x [1]
723
724 NOTE: For the negative numbers, here it is defined in the same way as for
725 positive numbers [2] (thus ‘frac 3.6 = 0.6’ but ‘frac ~3.6 = 0.4’.)
726 *)
727Definition frac_def :
728 frac x = x - real_of_int (INT_FLOOR x)
729End
730
731Theorem is_int_eq_frac_0 :
732 !x. is_int x <=> frac x = 0
733Proof
734 rw [frac_def, is_int_def, REAL_SUB_0]
735QED
736
737
738(* ----------------------------------------------------------------------
739 More automatic simplifications
740 ---------------------------------------------------------------------- *)
741
742Theorem real_of_int_EQN[simp]:
743 (real_of_int i = &n ⇔ i = &n) ∧
744 (&n = real_of_int i ⇔ i = &n) ∧
745 (real_of_int i = -&n ⇔ i = -&n) ∧
746 (-&n = real_of_int i ⇔ i = -&n)
747Proof
748 Cases_on ‘i’ >> simp[]
749QED
750
751
752
753
754
755val _ = add_ML_dependency "intLib"
756
757(* References:
758
759 [1] Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics. 2nd Eds.
760 Addison-Wesley Publishing Company (1994).
761 [2] https://en.wikipedia.org/wiki/Floor_and_ceiling_functions
762 [3] https://en.wikipedia.org/wiki/Fractional_part
763 *)