1(* ------------------------------------------------------------------------- 2 A bridging theory between integers and reals 3 ------------------------------------------------------------------------- *) 4 5open HolKernel boolLib bossLib 6open intLib 7 8local open realSimps in end 9 10val _ = new_theory "intreal" 11 12(* ------------------------------------------------------------------------- 13 Define the inclusion homomorphism real_of_int :int->real. 14 ------------------------------------------------------------------------- *) 15 16val real_of_int = Lib.with_flag (boolLib.def_suffix, "") Define 17 `real_of_int i = 18 if i < 0 then ~(real_of_num (Num (~i))) else real_of_num (Num i)` 19 20val real_of_int_def = save_thm("real_of_int_def", real_of_int); 21 22(* ------------------------------------------------------------------------- 23 Floor and ceiling (ints) 24 ------------------------------------------------------------------------- *) 25 26val INT_FLOOR_def = zDefine `INT_FLOOR x = LEAST_INT i. x < real_of_int (i + 1)` 27val INT_CEILING_def = zDefine `INT_CEILING x = LEAST_INT i. x <= real_of_int i` 28 29val _ = Parse.overload_on ("flr", ``INT_FLOOR``) 30val _ = Parse.overload_on ("clg", ``INT_CEILING``) 31 32(* ------------------------------------------------------------------------- 33 is_int 34 ------------------------------------------------------------------------- *) 35 36val is_int_def = Define `is_int (x:real) = (x = real_of_int (INT_FLOOR x))` 37 38(* ------------------------------------------------------------------------- 39 Theorems 40 ------------------------------------------------------------------------- *) 41 42val real_of_int_monotonic = Q.store_thm("real_of_int_monotonic", 43 `!i j. i < j ==> real_of_int i < real_of_int j`, 44 Cases \\ Cases \\ srw_tac[][real_of_int] \\ intLib.ARITH_TAC) 45 46val real_arch_least1 = 47 realTheory.REAL_ARCH_LEAST 48 |> Q.SPEC `1r` 49 |> SIMP_RULE (srw_ss()) [] 50 51val Num_suc1 = intLib.ARITH_PROVE ``Num (&n + 1) = n + 1`` 52 53val lem = Q.prove( `!n. -&n <= 0r`, simp [realTheory.REAL_NEG_LE0]) 54 55val lem2 = Q.prove( 56 `!n. -&(n + 1n) = -&n - 1r`, 57 once_rewrite_tac [GSYM realTheory.add_ints] 58 \\ simp [realTheory.real_sub] 59 ) 60 61val lem3 = intLib.ARITH_PROVE ``-&n + 1 < 0i ==> (Num (&n + -1i) = (n - 1))`` 62 63val lem4 = Q.prove( 64 `!n. n <> 0 ==> (-&(n - 1n) = -&n + 1r)`, 65 strip_tac 66 \\ Cases_on `n = 1` >- simp [] 67 \\ metis_tac [realTheory.REAL_SUB, realTheory.REAL_NEG_SUB, 68 RealArith.REAL_ARITH ``-a + b = b - a: real``, 69 DECIDE ``n <> 0 /\ n <> 1 ==> (n - 1 <> 0n)``] 70 ) 71 72val lem5 = Q.prove( 73 `!m n. n + 1 < m ==> -&m + 1 <= -&n - 1r`, 74 REPEAT strip_tac 75 \\ once_rewrite_tac [GSYM realTheory.REAL_LE_NEG] 76 \\ rewrite_tac [realTheory.REAL_NEG_SUB, realTheory.REAL_NEG_ADD, 77 realTheory.REAL_SUB_RNEG] 78 \\ Cases_on `m` 79 \\ full_simp_tac(srw_ss())[arithmeticTheory.ADD1] 80 \\ REWRITE_TAC [GSYM realTheory.REAL_ADD, 81 RealArith.REAL_ARITH ``a + b + -b = a: real``] 82 \\ simp [] 83 ) 84 85val INT_FLOOR_BOUNDS = Q.store_thm("INT_FLOOR_BOUNDS", 86 `!r. real_of_int (INT_FLOOR r) <= r /\ r < real_of_int (INT_FLOOR r + 1)`, 87 srw_tac[][INT_FLOOR_def, integerTheory.LEAST_INT_DEF] \\ SELECT_ELIM_TAC \\ ( 88 REVERSE conj_tac 89 >- (srw_tac[][realTheory.REAL_NOT_LT] 90 \\ pop_assum (qspec_then `x - 1` assume_tac) 91 \\ full_simp_tac(srw_ss())[intLib.ARITH_PROVE ``a - 1 < a: int``]) 92 \\ Cases_on `0 <= r` 93 >- (imp_res_tac real_arch_least1 94 \\ qexists_tac `&n` 95 \\ srw_tac[][real_of_int, realTheory.REAL_NOT_LT, 96 REWRITE_RULE [GSYM arithmeticTheory.ADD1] Num_suc1, 97 intLib.ARITH_PROVE ``~(&n + 1i < 0)``] 98 >- metis_tac [lem, realTheory.REAL_LE_TRANS] 99 \\ Cases_on `i'` 100 \\ full_simp_tac(srw_ss())[Num_suc1] 101 >| [`n' + 1 <= n` by decide_tac 102 \\ metis_tac [realTheory.REAL_LE, realTheory.REAL_LE_TRANS], 103 imp_res_tac 104 (intLib.ARITH_PROVE ``n <> 0 /\ ~(-&n + 1i < 0) ==> (n = 1)``) 105 \\ full_simp_tac(srw_ss())[], 106 `1 <= n` by decide_tac 107 \\ metis_tac [realTheory.REAL_LE, realTheory.REAL_LE_TRANS] 108 ] 109 ) 110 \\ imp_res_tac (RealArith.REAL_ARITH ``~(0r <= r) ==> 0 <= -r /\ r <> 0``) 111 \\ imp_res_tac real_arch_least1 112 \\ rev_full_simp_tac(srw_ss())[arithmeticTheory.ADD1, integerTheory.INT_NEG_ADD, 113 RealArith.REAL_ARITH ``r <= 0r ==> (&(n: num) <= -r <=> r <= -&n)``, 114 RealArith.REAL_ARITH ``r <= 0r ==> (-r < &n <=> -&n < r)``] 115 \\ Cases_on `r = -&n` 116 >| [qexists_tac `~&n`, qexists_tac `~&(SUC n)`] 117 \\ rev_full_simp_tac(srw_ss())[real_of_int, integerTheory.INT_NEG_ADD] 118 \\ (conj_tac 119 >- (srw_tac[][lem3] 120 \\ Cases_on `n` 121 \\ full_simp_tac(srw_ss())[arithmeticTheory.ADD1, 122 RealArith.REAL_ARITH ``r <= 0r /\ r <> 0 ==> r < 0``, 123 RealArith.REAL_ARITH ``a <= b - 1 ==> a < b: real``, 124 intLib.ARITH_PROVE ``-&(n + 1) + 1 < 0i <=> n <> 0``, 125 RealArith.REAL_ARITH ``r <= -1r ==> r < 0``, 126 RealArith.REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``]) 127 \\ srw_tac[][realTheory.REAL_NOT_LT] 128 \\ Cases_on `i'` 129 \\ rev_full_simp_tac(srw_ss())[lem2, lem3, lem4, arithmeticTheory.ADD1] 130 \\ (intLib.ARITH_TAC ORELSE 131 imp_res_tac (intLib.ARITH_PROVE ``n + 1 < m ==> (-&m + 1 < 0i)``) 132 \\ metis_tac 133 [realTheory.REAL_LET_TRANS, realTheory.REAL_LT_IMP_LE, lem5]) 134 ) 135 ) 136 ) 137 138Theorem INT_FLOOR: 139 !r i. (INT_FLOOR r = i) <=> real_of_int i <= r /\ r < real_of_int (i + 1) 140Proof 141 REPEAT strip_tac 142 \\ eq_tac 143 >- metis_tac [INT_FLOOR_BOUNDS] 144 \\ srw_tac[][INT_FLOOR_def, integerTheory.LEAST_INT_DEF] 145 \\ SELECT_ELIM_TAC 146 \\ conj_tac 147 >- ( 148 SPOSE_NOT_THEN strip_assume_tac 149 \\ res_tac 150 \\ Cases_on `i` 151 \\ Cases_on `i'` 152 \\ full_simp_tac(srw_ss())[real_of_int, intLib.ARITH_PROVE ``~(&n + 1i < 0)``] 153 >| [ 154 all_tac, 155 Cases_on `-&n' + 1 < 0i`, 156 all_tac, 157 Cases_on `-&n' + 1 < 0i`, 158 Cases_on `-&n + 1 < 0i` 159 ] 160 \\ full_simp_tac(srw_ss())[Num_suc1] 161 \\ imp_res_tac realTheory.REAL_LET_TRANS 162 \\ full_simp_tac(srw_ss())[integerTheory.INT_NOT_LT] 163 \\ intLib.ARITH_TAC 164 ) 165 \\ srw_tac[][] 166 \\ Cases_on `i < x` 167 >- res_tac 168 \\ Cases_on `i = x` 169 >- asm_rewrite_tac [] 170 \\ `x < i` by intLib.ARITH_TAC 171 \\ Cases_on `i` 172 \\ Cases_on `x` 173 \\ full_simp_tac(srw_ss())[real_of_int] 174 >| [ 175 Cases_on `&n + 1 < 0i` 176 \\ Cases_on `&n' + 1 < 0i`, 177 Cases_on `&n + 1 < 0i` 178 \\ Cases_on `-&n' + 1 < 0i`, 179 Cases_on `&n + 1 < 0i`, 180 Cases_on `-&n + 1 < 0i` 181 \\ Cases_on `-&n' + 1 < 0i`, 182 Cases_on `-&n + 1 < 0i` 183 ] 184 \\ full_simp_tac(srw_ss())[] 185 \\ imp_res_tac realTheory.REAL_LET_TRANS 186 \\ full_simp_tac(srw_ss())[integerTheory.INT_NOT_LT] 187 \\ intLib.ARITH_TAC 188QED 189 190val int_floor_1 = Q.prove( 191 `(INT_FLOOR &n = &n) /\ (INT_FLOOR (-&n) = -&n)`, 192 srw_tac[][INT_FLOOR, real_of_int] \\ intLib.ARITH_TAC) 193 194val tac = 195 imp_res_tac arithmeticTheory.DIVISION 196 \\ pop_assum (qspec_then `n` assume_tac) 197 \\ first_assum (qspec_then `n` assume_tac) 198 \\ TRY decide_tac 199 200val int_floor_2 = Q.prove( 201 `0 < m ==> (INT_FLOOR (&n / &m) = &n / &m)`, 202 strip_tac 203 \\ rewrite_tac [INT_FLOOR] 204 \\ srw_tac[][real_of_int, realTheory.le_ratr, realTheory.lt_ratl, Num_suc1] 205 \\ TRY decide_tac 206 >- tac 207 >- intLib.ARITH_TAC 208 \\ tac 209 ) 210 211val lem1 = 212 metisLib.METIS_PROVE 213 [realTheory.REAL_POS_NZ, realTheory.REAL_DIV_REFL, realTheory.neg_rat] 214 ``!a. 0r < a ==> (-a / a = -1)`` 215 216val lem2 = Q.prove( 217 `!n. 0n < n ==> (-&n / &n = -1i)`, 218 REPEAT strip_tac 219 \\ `0i < &n` by intLib.ARITH_TAC 220 \\ simp [integerTheory.int_div] 221 ) 222 223val lem3 = Q.prove( 224 `!n m. 0n < n /\ n < m ==> (-&n / &m = -1i)`, 225 REPEAT strip_tac 226 \\ `0i < &n` by intLib.ARITH_TAC 227 \\ simp [integerTheory.int_div, arithmeticTheory.LESS_DIV_EQ_ZERO] 228 ) 229 230val tac2 = 231 metis_tac [arithmeticTheory.X_MOD_Y_EQ_X, DECIDE ``x < y ==> ~(y < x:num)``] 232 233val lem4 = Q.prove( 234 `!n m. 0 < m /\ m < n ==> -&n / &m < -1i`, 235 NTAC 3 strip_tac 236 \\ `&m <> 0i` by intLib.ARITH_TAC 237 \\ simp [integerTheory.int_div] 238 \\ srw_tac[][intLib.ARITH_PROVE ``a + -1 < -1 <=> a < 0i``] 239 \\ tac 240 >- (SPOSE_NOT_THEN strip_assume_tac 241 \\ `(n DIV m = 0) \/ (n DIV m = 1)` by decide_tac 242 \\ full_simp_tac(srw_ss())[] 243 >- tac2 244 \\ decide_tac 245 ) 246 \\ strip_tac 247 \\ full_simp_tac(srw_ss())[] 248 \\ tac2 249 ) 250 251val lem5 = Q.prove( 252 `!n m. 0n < m /\ n <> 0 /\ (n MOD m = 0) /\ n <> m ==> 1 < n DIV m`, 253 srw_tac[][arithmeticTheory.X_LT_DIV] 254 \\ imp_res_tac arithmeticTheory.MOD_EQ_0_DIVISOR 255 \\ Cases_on `d = 0` >- full_simp_tac(srw_ss())[] 256 \\ Cases_on `d = 1` >- full_simp_tac(srw_ss())[] 257 \\ `2 <= d` by decide_tac 258 \\ metis_tac [arithmeticTheory.LESS_MONO_MULT] 259 ) 260 261val int_floor_3 = Q.prove( 262 `0 < m ==> (INT_FLOOR (-&n / &m) = -&n / &m)`, 263 strip_tac 264 \\ rewrite_tac [INT_FLOOR] 265 \\ Cases_on `n = 0` 266 >- simp [real_of_int, arithmeticTheory.ZERO_DIV] 267 \\ Cases_on `n = m` 268 >- simp [lem1, lem2, real_of_int] 269 \\ Cases_on `n < m` 270 >- simp [lem3, real_of_int, realTheory.le_ratr, realTheory.lt_ratl] 271 \\ `m < n` by decide_tac 272 \\ simp [lem4, real_of_int, realTheory.le_ratr, realTheory.lt_ratl, 273 intLib.ARITH_PROVE ``a < -1i ==> a < 0 /\ a + 1 < 0``] 274 \\ simp [integerTheory.int_div] 275 \\ srw_tac[][integerTheory.INT_NEG_ADD, lem5, Num_suc1, 276 intLib.ARITH_PROVE ``a + 1 + -1 = a: int``, 277 intLib.ARITH_PROVE ``1n < a ==> (Num (&a + -1) = a - 1)``] 278 \\ tac 279 ) 280 281val INT_CEILING_IMP = Q.prove ( 282 `!r i. real_of_int (i - 1) < r /\ r <= real_of_int i ==> (INT_CEILING r = i)`, 283 srw_tac[][INT_CEILING_def, integerTheory.LEAST_INT_DEF] 284 \\ SELECT_ELIM_TAC 285 \\ conj_tac 286 >- ( 287 SPOSE_NOT_THEN STRIP_ASSUME_TAC 288 \\ res_tac 289 \\ Cases_on `i` 290 \\ Cases_on `i'` 291 \\ full_simp_tac(srw_ss())[real_of_int] 292 >| [ 293 Cases_on `&n - 1 < 0i`, 294 Cases_on `&n - 1 < 0i`, 295 Cases_on `&n - 1 < 0i`, 296 Cases_on `-&n - 1 < 0i`, 297 all_tac 298 ] 299 \\ full_simp_tac(srw_ss())[] 300 \\ imp_res_tac realTheory.REAL_LTE_TRANS 301 \\ full_simp_tac(srw_ss())[] 302 \\ intLib.ARITH_TAC 303 ) 304 \\ srw_tac[][] 305 \\ Cases_on `i < x` 306 >- res_tac 307 \\ Cases_on `i = x` 308 >- asm_rewrite_tac [] 309 \\ `x < i` by intLib.ARITH_TAC 310 \\ Cases_on `i` 311 \\ Cases_on `x` 312 \\ full_simp_tac(srw_ss())[real_of_int] 313 >| [ 314 Cases_on `&n - 1 < 0i`, 315 Cases_on `&n - 1 < 0i`, 316 Cases_on `&n - 1 < 0i`, 317 Cases_on `-&n - 1 < 0i`, 318 all_tac 319 ] 320 \\ full_simp_tac(srw_ss())[] 321 \\ imp_res_tac realTheory.REAL_LTE_TRANS 322 \\ full_simp_tac(srw_ss())[] 323 \\ intLib.ARITH_TAC 324 ) 325 326val INT_CEILING_INT_FLOOR = Q.store_thm("INT_CEILING_INT_FLOOR", 327 `!r. INT_CEILING r = 328 let i = INT_FLOOR r in if real_of_int i = r then i else i + 1`, 329 lrw [] 330 \\ match_mp_tac INT_CEILING_IMP 331 >- (`INT_FLOOR r - 1 < INT_FLOOR r` by intLib.ARITH_TAC 332 \\ imp_res_tac real_of_int_monotonic 333 \\ simp [] 334 \\ metis_tac [INT_FLOOR_BOUNDS, realTheory.REAL_LTE_TRANS]) 335 \\ simp [intLib.ARITH_PROVE ``a + 1 -1i = a``, 336 RealArith.REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``, 337 INT_FLOOR_BOUNDS, realTheory.REAL_LT_IMP_LE] 338 ) 339 340val INT_CEILING_BOUNDS = Q.store_thm("INT_CEILING_BOUNDS", 341 `!r. real_of_int (INT_CEILING r - 1) < r /\ r <= real_of_int (INT_CEILING r)`, 342 lrw [INT_CEILING_INT_FLOOR, INT_FLOOR_BOUNDS, realTheory.REAL_LT_IMP_LE, 343 intLib.ARITH_PROVE ``a + 1i - 1 = a``, 344 RealArith.REAL_ARITH ``a <= b /\ a <> b ==> a < b: real``] 345 \\ pop_assum (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [SYM th]))) 346 \\ match_mp_tac real_of_int_monotonic 347 \\ intLib.ARITH_TAC 348 ) 349 350Theorem INT_CEILING: 351 !r i. (INT_CEILING r = i) <=> real_of_int (i - 1) < r /\ r <= real_of_int i 352Proof 353 metis_tac [INT_CEILING_BOUNDS, INT_CEILING_IMP] 354QED 355 356local 357 val rule = 358 REWRITE_RULE [numeralTheory.numeral_distrib, numeralTheory.numeral_lt] 359 val r1 = rule o Q.INST [`m` |-> `NUMERAL (BIT1 m)`] 360 val r2 = rule o Q.INST [`m` |-> `NUMERAL (BIT2 m)`] 361 val (t1, t2) = Drule.CONJ_PAIR int_floor_1 362in 363 val INT_FLOOR_EQNS = Theory.save_thm("INT_FLOOR_EQNS", 364 Drule.LIST_CONJ (List.map Drule.GEN_ALL [t1, t2, int_floor_2, int_floor_3])) 365 val INT_FLOOR_compute = Theory.save_thm ("INT_FLOOR_compute", 366 Drule.LIST_CONJ 367 [t1,t2, r1 int_floor_2, r2 int_floor_2, r1 int_floor_3, r2 int_floor_3]) 368 val () = computeLib.add_persistent_funs 369 ["INT_FLOOR_compute", "INT_CEILING_INT_FLOOR"] 370end 371 372open arithmeticTheory 373val real_of_int_num = store_thm("real_of_int_num[simp]", 374 ``real_of_int (& n) = &n``, 375 rewrite_tac[real_of_int_def] 376 \\ Cases_on `(&n):int` 377 \\ fs []); 378 379val real_of_int_add = store_thm("real_of_int_add[simp]", 380 ``real_of_int (m + n) = real_of_int m + real_of_int n``, 381 Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw [] 382 \\ fs [integerTheory.INT_ADD_CALCULATE] 383 \\ rw [] \\ fs [] \\ fs [GSYM NOT_LESS,realTheory.add_ints]); 384 385val real_of_int_neg = store_thm("real_of_int_neg[simp]", 386 ``real_of_int (-m) = -real_of_int m``, 387 Cases_on `m` \\ fs [real_of_int_def]); 388 389val real_of_int_sub = store_thm("real_of_int_sub[simp]", 390 ``real_of_int (m - n) = real_of_int m - real_of_int n``, 391 fs [integerTheory.int_sub,realTheory.real_sub]); 392 393val real_of_int_mul = store_thm("real_of_int_mul[simp]", 394 ``real_of_int (m * n) = real_of_int m * real_of_int n``, 395 Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw [] 396 \\ fs [integerTheory.INT_MUL_CALCULATE]); 397 398val real_of_int_lt = store_thm("real_of_int_lt[simp]", 399 ���real_of_int m < real_of_int n <=> m < n���, 400 simp[real_of_int_def] >> map_every Cases_on [���m���, ���n���] >> 401 simp[]); 402 403val real_of_int_11 = store_thm("real_of_int_11[simp]", 404 ���(real_of_int m = real_of_int n) <=> (m = n)���, 405 simp[real_of_int_def] >> map_every Cases_on [���m���, ���n���] >> 406 simp[]); 407 408val real_of_int_le = store_thm("real_of_int_le[simp]", 409 ���real_of_int m <= real_of_int n <=> m <= n���, 410 simp[realTheory.REAL_LE_LT, integerTheory.INT_LE_LT]); 411 412val _ = export_theory () 413