1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6map load 7 ["pred_setTheory", "pairTheory", "arithmeticTheory", "tuerk_tacticsLib", 8 "containerTheory", "listTheory", "rich_listTheory", "set_lemmataTheory", "bitTheory"]; 9*) 10 11 12open pred_setTheory pairTheory arithmeticTheory tuerk_tacticsLib 13 containerTheory listTheory rich_listTheory set_lemmataTheory 14 bitTheory; 15open Sanity; 16 17val _ = hide "S"; 18val _ = hide "I"; 19 20(* 21show_assums := false; 22show_assums := true; 23show_types := true; 24show_types := false; 25quietdec := false; 26*) 27 28 29 30val _ = new_theory "temporal_deep_mixed"; 31val _ = ParseExtras.temp_loose_equality() 32 33 34(******************************************************************************) 35(* IS_ELEMENT_ITERATOR *) 36(* This described a function that can create a number of new elements *) 37(******************************************************************************) 38 39val IS_ELEMENT_ITERATOR_def = 40Define 41 `IS_ELEMENT_ITERATOR f n S = 42 (!i j. (i < n /\ j < n) ==> ((f i = f j) = (i = j))) /\ 43 (!i. (i < n) ==> ~(f i IN S))` 44 45val IS_ELEMENT_ITERATOR_0 = 46 store_thm 47 ("IS_ELEMENT_ITERATOR_0", 48 49 ``!f S. IS_ELEMENT_ITERATOR f 0 S``, 50 SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def]); 51 52 53val IS_ELEMENT_ITERATOR_SUBSET = 54 store_thm 55 ("IS_ELEMENT_ITERATOR_SUBSET", 56 57 ``!f n S1 S2. (S2 SUBSET S1 /\ IS_ELEMENT_ITERATOR f n S1) ==> IS_ELEMENT_ITERATOR f n S2``, 58 59 SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def, SUBSET_DEF] THEN PROVE_TAC[]); 60 61 62val IS_ELEMENT_ITERATOR_GE = 63 store_thm 64 ("IS_ELEMENT_ITERATOR_GE", 65 66 ``!f n1 n2 S. (n2 <= n1 /\ IS_ELEMENT_ITERATOR f n1 S) ==> IS_ELEMENT_ITERATOR f n2 S``, 67 68 SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def]); 69 70 71val IS_ELEMENT_ITERATOR___IMPLIES___INJ = 72 store_thm 73 ("IS_ELEMENT_ITERATOR___IMPLIES___INJ", 74 75 ``!f n S. 76 IS_ELEMENT_ITERATOR f n S ==> 77 INJ f (count n) UNIV``, 78 79 SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, INJ_DEF, 80 IN_COUNT, IN_UNIV]); 81 82val IS_ELEMENT_ITERATOR___INVERSE = 83 store_thm 84 ("IS_ELEMENT_ITERATOR___INVERSE", 85 86 ``!f n S. 87 IS_ELEMENT_ITERATOR f n S ==> 88 (?g. !m. (m < n) ==> (g (f m) = m))``, 89 90 METIS_TAC[INJ_INVERSE, IN_COUNT, IS_ELEMENT_ITERATOR___IMPLIES___INJ]); 91 92 93val IS_ELEMENT_ITERATOR_EXISTS___DIFF = 94 store_thm 95 ("IS_ELEMENT_ITERATOR_EXISTS___DIFF", 96 97 ``!n S. 98 INFINITE (UNIV DIFF S) ==> 99 ?f. IS_ELEMENT_ITERATOR f n S``, 100 101 REPEAT STRIP_TAC THEN 102 Induct_on `n` THENL [ 103 SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def], 104 105 FULL_SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def] THEN 106 `?e. e IN (UNIV DIFF S) /\ ~(e IN (IMAGE f (count n)))` by PROVE_TAC[IN_INFINITE_NOT_FINITE, FINITE_COUNT, IMAGE_FINITE] THEN 107 `?f'. f' = (\i:num. if (i < n) then (f i) else e)` by METIS_TAC[] THEN 108 EXISTS_TAC ``f':num->'a`` THEN 109 ASM_SIMP_TAC arith_ss [] THEN 110 REPEAT STRIP_TAC THENL [ 111 Cases_on `i < n` THEN 112 Cases_on `j < n` THEN 113 REPEAT STRIP_TAC THENL [ 114 ASM_SIMP_TAC std_ss [], 115 116 `~(i = j)` by DECIDE_TAC THEN 117 ASM_SIMP_TAC std_ss [] THEN 118 `f i IN IMAGE f (count n)` by ( 119 ASM_REWRITE_TAC[IN_UNION, IN_IMAGE, IN_COUNT] THEN 120 PROVE_TAC[]) THEN 121 PROVE_TAC[], 122 123 124 `~(i = j)` by DECIDE_TAC THEN 125 ASM_SIMP_TAC std_ss [] THEN 126 `f j IN IMAGE f (count n)` by ( 127 ASM_REWRITE_TAC[IN_UNION, IN_IMAGE, IN_COUNT] THEN 128 PROVE_TAC[]) THEN 129 PROVE_TAC[], 130 131 132 ASM_REWRITE_TAC[] THEN DECIDE_TAC 133 ], 134 135 136 Cases_on `i < n` THENL [ 137 FULL_SIMP_TAC std_ss [IN_DIFF] THEN PROVE_TAC[], 138 FULL_SIMP_TAC std_ss [IN_DIFF] THEN PROVE_TAC[IN_UNION] 139 ] 140 ] 141 ]); 142 143 144val IS_ELEMENT_ITERATOR_EXISTS = 145 store_thm 146 ("IS_ELEMENT_ITERATOR_EXISTS", 147 148 ``!n S. 149 (FINITE (S:'a set) /\ INFINITE (UNIV:'a set)) ==> 150 ?f. IS_ELEMENT_ITERATOR f n S``, 151 152 PROVE_TAC[FINITE_DIFF_down, IS_ELEMENT_ITERATOR_EXISTS___DIFF]); 153 154 155(************************************************************************) 156(* Variable renamings, i.e. injective functions with some properties *) 157(************************************************************************) 158 159val FINITE_INJ_EXISTS_aux = prove ( 160 ``INFINITE (UNIV:'b set) ==> !S1:'a set. FINITE S1 ==> 161 !S2:'b set. FINITE S2 ==> 162 ?f:'a->'b. (INJ f S1 UNIV /\ (DISJOINT (IMAGE f S1) S2))``, 163 164 DISCH_TAC THEN 165 SET_INDUCT_TAC THENL [ 166 SIMP_TAC std_ss [INJ_EMPTY, IMAGE_EMPTY, DISJOINT_EMPTY], 167 168 REPEAT STRIP_TAC THEN 169 RES_TAC THEN 170 `?x. ~(x IN ((IMAGE f s) UNION S2))` by PROVE_TAC[IMAGE_FINITE, NOT_IN_FINITE, FINITE_UNION] THEN 171 Q_TAC EXISTS_TAC `\z. (if z = e then x else (f z))` THEN 172 UNDISCH_NO_TAC 2 THEN 173 SIMP_ALL_TAC std_ss [INJ_DEF, IN_INSERT, IN_UNIV, IN_IMAGE, IN_UNION, DISJOINT_DISJ_THM] THEN 174 METIS_TAC[] 175 ]); 176 177 178val FINITE_INJ_EXISTS = save_thm ("FINITE_INJ_EXISTS", 179SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, 180 AND_IMP_INTRO] FINITE_INJ_EXISTS_aux); 181 182 183 184val DISJOINT_VARRENAMING_EXISTS = 185 store_thm 186 ("DISJOINT_VARRENAMING_EXISTS", 187 ``!(S1:'a set) (S2:'a set) (S3:'a set). (FINITE S1 /\ FINITE S2 /\ FINITE S3 /\ (DISJOINT S1 S3) /\ INFINITE (UNIV:'a set)) ==> 188 (?f. INJ f UNIV UNIV /\ (DISJOINT (IMAGE f S1) S2) /\ (!x. (x IN S3) ==> (f x = x)))``, 189 190 REPEAT STRIP_TAC THEN 191 UNDISCH_TAC ``DISJOINT S1 S3`` THEN 192 UNDISCH_TAC ``FINITE S1`` THEN 193 SPEC_TAC (``S1:'a set``,``S1:'a set``) THEN 194 SET_INDUCT_TAC THENL [ 195 REPEAT STRIP_TAC THEN 196 EXISTS_TAC ``\x. x`` THEN 197 SIMP_TAC std_ss [INJ_ID, IMAGE_EMPTY, DISJOINT_EMPTY], 198 199 200 REPEAT STRIP_TAC THEN 201 FULL_SIMP_TAC std_ss [DISJOINT_INSERT, IMAGE_INSERT] THEN 202 `?x. ~(x IN (IMAGE f (s :'a set))) /\ ~(x IN (S2:'a set)) /\ ~(x IN (S3:'a set))` by ( 203 `FINITE ((IMAGE f s) UNION S2 UNION S3)` by METIS_TAC[IMAGE_FINITE, FINITE_UNION] THEN 204 PROVE_TAC[NOT_IN_FINITE, IN_UNION] 205 ) THEN 206 EXISTS_TAC ``\z:'a. (if z = e then x:'a else (if (f z) = x then (f e) else (f z)))`` THEN 207 REPEAT STRIP_TAC THENL [ 208 REWRITE_ALL_TAC [INJ_DEF, IN_UNIV] THEN METIS_TAC[], 209 210 FULL_SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, IN_IMAGE] THEN 211 PROVE_TAC[], 212 213 FULL_SIMP_TAC std_ss [], 214 215 `~(x' = e) /\ ~(f x' = x)` by PROVE_TAC[] THEN 216 ASM_SIMP_TAC std_ss [] 217 ] 218 ]); 219 220 221val POW_VARRENAMING_EXISTS = 222 store_thm 223 ("POW_VARRENAMING_EXISTS", 224 ``!(S1:'a set) (S2:'a set). (FINITE S1 /\ FINITE S2 /\ INFINITE (UNIV:'a set)) ==> 225 (?f. INJ f (POW S1) UNIV /\ (DISJOINT (IMAGE f (POW S1)) S2))``, 226 227 REPEAT STRIP_TAC THEN 228 MATCH_MP_TAC FINITE_INJ_EXISTS THEN 229 ASM_REWRITE_TAC[FINITE_POW_IFF]); 230 231 232 233 234 235(******************************************************************************) 236(* LIST_BIGUNION *) 237(******************************************************************************) 238 239val LIST_BIGUNION_def = 240 Define 241 `(LIST_BIGUNION [] = EMPTY) /\ 242 (LIST_BIGUNION (h::l) = (h UNION (LIST_BIGUNION l)))`; 243 244 245val LIST_BIGUNION_APPEND = 246 store_thm 247 ("LIST_BIGUNION_APPEND", 248 ``!l1 l2. LIST_BIGUNION (l1 ++ l2) = (LIST_BIGUNION l1 UNION LIST_BIGUNION l2)``, 249 250 Induct_on `l1` THENL [ 251 SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY], 252 ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_ASSOC] 253 ]); 254 255 256val IN_LIST_BIGUNION = 257 store_thm 258 ("IN_LIST_BIGUNION", 259 260 ``!x l. (x IN LIST_BIGUNION l) = ?el. MEM el l /\ x IN el``, 261 262 Induct_on `l` THENL [ 263 SIMP_TAC list_ss [LIST_BIGUNION_def, NOT_IN_EMPTY], 264 SIMP_TAC list_ss [LIST_BIGUNION_def, IN_UNION] THEN PROVE_TAC[] 265 ]); 266 267(* Perhaps use this everywhere and get rid of LIST_BIGUNION *) 268val LIST_BIGUNION_ALT_DEF = store_thm ("LIST_BIGUNION_ALT_DEF", 269 ``!l. LIST_BIGUNION l = BIGUNION (set l)``, 270 271SIMP_TAC std_ss [EXTENSION, IN_LIST_BIGUNION, IN_BIGUNION] >> 272METIS_TAC[]); 273 274 275 276(******************************************************************************) 277(* Auxiliary arithmetic stuff *) 278(******************************************************************************) 279 280val SUC_MOD_CASES = 281 store_thm ("SUC_MOD_CASES", 282 283 ``!n m. 0 < n ==> 284 ((((SUC m) MOD n) = 0) \/ (((SUC m) MOD n) = (SUC (m MOD n))))``, 285 286 REPEAT STRIP_TAC THEN 287 Cases_on `n = 1` THENL [ 288 ASM_REWRITE_TAC[MOD_1], 289 290 `(SUC m) MOD n = ((SUC (m MOD n)) MOD n)` by ( 291 `1 < n` by DECIDE_TAC THEN 292 `1 = 1 MOD n` by PROVE_TAC[LESS_MOD] THEN 293 ASM_SIMP_TAC std_ss [SUC_ONE_ADD] THEN 294 ONCE_ASM_REWRITE_TAC[] THEN 295 ASM_SIMP_TAC std_ss [MOD_PLUS] 296 ) THEN 297 ASM_REWRITE_TAC[] THEN 298 Cases_on `SUC (m MOD n) < n` THENL [ 299 ASM_SIMP_TAC std_ss [LESS_MOD], 300 301 `m MOD n < n` by PROVE_TAC[DIVISION] THEN 302 `SUC (m MOD n) = n` by DECIDE_TAC THEN 303 ASM_SIMP_TAC std_ss [DIVMOD_ID] 304 ] 305 ]); 306 307 308 309(*****************************) 310(* COND_IMP_EQ *) 311(*****************************) 312 313val COND_IMP_EQ_def = 314 Define `COND_IMP_EQ c A B = if c then A=B else A ==> B` 315 316val COND_IMP_EQ___REWRITE = 317 store_thm ("COND_IMP_EQ___REWRITE", 318 ``!c A B. COND_IMP_EQ c A B = 319 ((A ==> B) /\ (c ==> (A = B)))``, 320 SIMP_TAC std_ss [COND_IMP_EQ_def] THEN 321 METIS_TAC[]); 322 323 324(****************************************************************************************) 325(* INTERVAL_SET and INTERVAL_LIST *) 326(* *) 327(* Similar to count and COUNT_LIST, but have a starting point that might differ from 0 *) 328(****************************************************************************************) 329 330val INTERVAL_SET_def = 331 Define ` 332 INTERVAL_SET (n1:num) (n2:num) = IMAGE (\x. n1 + x) (count ((SUC n2)-n1))` 333 334 335val INTERVAL_LIST_def = 336 Define ` 337 INTERVAL_LIST (n1:num) (n2:num) = 338 MAP (\x. n1 + x) (COUNT_LIST ((SUC n2) - n1))` 339 340 341val INTERVAL_SET_0 = store_thm ("INTERVAL_SET_0", 342 ``!n. INTERVAL_SET 0 n = count (SUC n)``, 343SIMP_TAC std_ss [INTERVAL_SET_def, EXTENSION, IN_IMAGE]); 344 345val INTERVAL_LIST_0 = store_thm ("INTERVAL_LIST_0", 346 ``!n. INTERVAL_LIST 0 n = COUNT_LIST (SUC n)``, 347SIMP_TAC list_ss [INTERVAL_LIST_def, LIST_EQ_REWRITE, EL_MAP]); 348 349 350val LIST_TO_SET___INTERVAL_LIST = 351 store_thm ("LIST_TO_SET___INTERVAL_LIST", 352 ``!m0 m1. ((set (INTERVAL_LIST m0 m1)) = INTERVAL_SET m0 m1)``, 353 354SIMP_TAC std_ss [INTERVAL_LIST_def, INTERVAL_SET_def, 355 LIST_TO_SET_MAP, COUNT_LIST_COUNT]); 356 357 358val FINITE_INTERVAL_SET = 359 store_thm ("FINITE_INTERVAL_SET", 360 ``!n1 n2. FINITE (INTERVAL_SET n1 n2)``, 361 SIMP_TAC std_ss [INTERVAL_SET_def, FINITE_COUNT, 362 IMAGE_FINITE]); 363 364 365val MEM_INTERVAL_LIST = 366 store_thm ("MEM_INTERVAL_LIST", 367 ``!n m0 m1. ((MEM n (INTERVAL_LIST m0 m1)) = (m0 <= n /\ n <= m1))``, 368 369 SIMP_TAC std_ss [INTERVAL_LIST_def, MEM_MAP, MEM_COUNT_LIST] THEN 370 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 371 DECIDE_TAC, 372 DECIDE_TAC, 373 Q.EXISTS_TAC `n - m0` >> DECIDE_TAC 374 ] 375 ); 376 377 378val IN_INTERVAL_SET = 379 store_thm ("IN_INTERVAL_SET", 380 ``!n n1 n2. (n IN INTERVAL_SET n1 n2) = (n1 <= n /\ n <= n2)``, 381 SIMP_TAC std_ss [GSYM LIST_TO_SET___INTERVAL_LIST, MEM_INTERVAL_LIST]); 382 383 384val INTERVAL_SET_SING = 385 store_thm ("INTERVAL_SET_SING", 386 ``!n. (INTERVAL_SET n n) = {n}``, 387 SIMP_TAC std_ss [EXTENSION, IN_SING, IN_INTERVAL_SET] THEN 388 DECIDE_TAC); 389 390 391val INTERVAL_LIST_THM = 392 store_thm ("INTERVAL_LIST_THM", 393 ``!n1 n2. ((n1 <= n2) ==> (INTERVAL_LIST n1 n2 = (n1::INTERVAL_LIST (SUC n1) n2))) /\ 394 ((n2 < n1) ==> (INTERVAL_LIST n1 n2 = []))``, 395 396 SIMP_TAC std_ss [INTERVAL_LIST_def] THEN 397 REPEAT STRIP_TAC THENL [ 398 `(SUC n2 - n1 = SUC (n2 - n1)) /\ (n1 <= n2)` by DECIDE_TAC THEN 399 Q.ABBREV_TAC `a = n2 - n1` THEN 400 FULL_SIMP_TAC list_ss [COUNT_LIST_def, MAP_MAP_o, combinTheory.o_DEF] THEN 401 AP_THM_TAC THEN AP_TERM_TAC THEN 402 SIMP_TAC arith_ss [FUN_EQ_THM], 403 404 `(SUC n2 - n1 = 0) /\ (n2 - n1 = 0) /\ ~(n1 <= n2)` by DECIDE_TAC THEN 405 ASM_SIMP_TAC list_ss [COUNT_LIST_def] 406 ]); 407 408 409 410(************************) 411(* SET_BINARY_ENCODING *) 412(************************) 413 414(* Encode sets of numbers as numbers. Each number in the original set of numbers 415 sets the corresponding bit of the resulting number. *) 416 417val SET_BINARY_ENCODING_def = 418 Define `SET_BINARY_ENCODING = 419 SIGMA (\n:num. (2:num)**n)`; 420 421 422val SET_BINARY_ENCODING_THM = 423 store_thm ("SET_BINARY_ENCODING_THM", 424``(SET_BINARY_ENCODING EMPTY = 0) /\ 425 (!e s. (FINITE s /\ ~(e IN s)) ==> 426 (SET_BINARY_ENCODING (e INSERT s) = (2 ** e) + (SET_BINARY_ENCODING s)))``, 427 428SIMP_TAC std_ss [SET_BINARY_ENCODING_def, SUM_IMAGE_THM] THEN 429PROVE_TAC[DELETE_NON_ELEMENT]); 430 431val SET_BINARY_ENCODING_SING = 432 store_thm ("SET_BINARY_ENCODING_SING", 433``!e. SET_BINARY_ENCODING {e} = 2 ** e``, 434 435SIMP_TAC std_ss [SET_BINARY_ENCODING_def, SUM_IMAGE_SING]); 436 437 438val SET_BINARY_ENCODING___UNION = 439 store_thm ("SET_BINARY_ENCODING___UNION", 440 441``!S1 S2. DISJOINT S1 S2 /\ FINITE S1 /\ FINITE S2 ==> 442(SET_BINARY_ENCODING (S1 UNION S2) = 443(SET_BINARY_ENCODING S1 + SET_BINARY_ENCODING S2))``, 444 445REPEAT STRIP_TAC THEN 446ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_def, SUM_IMAGE_UNION] THEN 447`S1 INTER S2 = EMPTY` by ( 448 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, IN_INTER, EXTENSION, NOT_IN_EMPTY] THEN 449 ASM_REWRITE_TAC[] 450) THEN 451ASM_SIMP_TAC std_ss [SUM_IMAGE_THM]); 452 453 454 455val SET_BINARY_ENCODING___SUBSET = 456 store_thm ("SET_BINARY_ENCODING___SUBSET", `` 457!S1 S2. S1 SUBSET S2 /\ FINITE S2 ==> 458(SET_BINARY_ENCODING S1 <= 459(SET_BINARY_ENCODING S2))``, 460 461REPEAT STRIP_TAC THEN 462Q.ABBREV_TAC `S3 = S2 DIFF S1` THEN 463`S2 = S3 UNION S1` by ( 464 SIMP_ALL_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, SUBSET_DEF] THEN 465 PROVE_TAC[] 466) THEN 467ASM_SIMP_TAC std_ss [] THEN 468 469`SET_BINARY_ENCODING (S3 UNION S1) = 470 SET_BINARY_ENCODING S3 + SET_BINARY_ENCODING S1` by ( 471 472 MATCH_MP_TAC SET_BINARY_ENCODING___UNION THEN 473 Q.UNABBREV_TAC `S3` THEN 474 METIS_TAC[DISJOINT_DIFF, FINITE_DIFF, SUBSET_FINITE] 475) THEN 476ASM_SIMP_TAC std_ss []); 477 478 479 480val SET_BINARY_ENCODING___COUNT = 481 store_thm ("SET_BINARY_ENCODING___COUNT", 482 ``!n. SET_BINARY_ENCODING (count n) = PRE (2**n)``, 483 484 Induct_on `n` THENL [ 485 SIMP_TAC arith_ss [COUNT_ZERO, SET_BINARY_ENCODING_THM], 486 487 SIMP_TAC std_ss [COUNT_SUC, SET_BINARY_ENCODING_THM, 488 FINITE_INSERT, FINITE_COUNT, IN_COUNT] THEN 489 ASM_SIMP_TAC arith_ss [EXP] 490 ] 491 ); 492 493 494val SET_BINARY_ENCODING___REDUCE = 495 store_thm ("SET_BINARY_ENCODING___REDUCE", 496 ``!n S. FINITE S ==> DISJOINT S (count n) ==> 497 ((SET_BINARY_ENCODING S) = (SET_BINARY_ENCODING (IMAGE (\x:num. x - n) S)) * (2 ** n))``, 498 499GEN_TAC THEN 500SET_INDUCT_TAC THENL [ 501 SIMP_TAC std_ss [SET_BINARY_ENCODING_THM, IMAGE_EMPTY], 502 503 REPEAT STRIP_TAC THEN 504 FULL_SIMP_TAC arith_ss [DISJOINT_INSERT, IN_COUNT] THEN 505 `~((e - n) IN (IMAGE (\x. x - n) s))` by ( 506 SIMP_TAC std_ss [IN_IMAGE] THEN 507 GEN_TAC THEN 508 Cases_on `x IN s` THEN ASM_REWRITE_TAC[] THEN 509 FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_INSERT, IN_COUNT] THEN 510 `~(x < n) /\ (e <> x)` by PROVE_TAC[] THEN 511 DECIDE_TAC 512 ) THEN 513 FULL_SIMP_TAC std_ss [SET_BINARY_ENCODING_THM, IMAGE_INSERT, FINITE_INSERT, IMAGE_FINITE] THEN 514 ASM_SIMP_TAC arith_ss [RIGHT_ADD_DISTRIB, GSYM EXP_ADD] 515]); 516 517 518val SET_BINARY_ENCODING___BITS = 519 store_thm ("SET_BINARY_ENCODING___BITS", 520 ``!n S. FINITE S ==> (BIT n (SET_BINARY_ENCODING S) = (n IN S))``, 521 522 REPEAT STRIP_TAC THEN 523 Q.ABBREV_TAC `S1 = S INTER count n` THEN 524 Q.ABBREV_TAC `S2 = S DIFF count (SUC n)` THEN 525 Q.ABBREV_TAC `Sn = S INTER {n}` THEN 526 `FINITE S1 /\ FINITE Sn /\ FINITE S2` by PROVE_TAC[INTER_FINITE, 527 FINITE_SING, FINITE_DIFF] THEN 528 Q.SUBGOAL_THEN `S = S1 UNION Sn UNION S2` SUBST1_TAC THEN1 ( 529 UNABBREV_ALL_TAC THEN 530 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 531 IN_COUNT, IN_SING] THEN 532 REPEAT STRIP_TAC THEN 533 Cases_on `x IN S` THEN ASM_REWRITE_TAC[] THEN 534 DECIDE_TAC 535 ) THEN 536 537 Q.SUBGOAL_THEN `SET_BINARY_ENCODING (S1 UNION Sn UNION S2) = 538 SET_BINARY_ENCODING S1 + SET_BINARY_ENCODING Sn + SET_BINARY_ENCODING S2` 539 SUBST1_TAC THEN1 ( 540 `DISJOINT S1 Sn /\ DISJOINT (S1 UNION Sn) S2` by ( 541 UNABBREV_ALL_TAC THEN 542 ASM_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_INTER, IN_SING, 543 IN_COUNT, IN_UNION, IN_DIFF] THEN 544 REPEAT STRIP_TAC THEN 545 Cases_on `x IN S` THEN ASM_REWRITE_TAC[] THEN 546 DECIDE_TAC 547 ) THEN 548 549 ASM_SIMP_TAC std_ss [FINITE_UNION, SET_BINARY_ENCODING___UNION] 550 ) THEN 551 552 Q.SUBGOAL_THEN `n IN S1 UNION Sn UNION S2 = n IN Sn` SUBST1_TAC THEN1 ( 553 UNABBREV_ALL_TAC THEN 554 ASM_SIMP_TAC arith_ss [IN_UNION, IN_INTER, IN_DIFF, IN_COUNT] 555 ) THEN 556 557 `SET_BINARY_ENCODING S1 < 2**n` by ( 558 MP_TAC (Q.SPECL [`S1`, `count n`] SET_BINARY_ENCODING___SUBSET) THEN 559 `S1 SUBSET count n` by METIS_TAC[INTER_SUBSET] THEN 560 FULL_SIMP_TAC std_ss [SET_BINARY_ENCODING___COUNT, FINITE_COUNT] THEN 561 `~(((2:num) ** n) = 0)` by SIMP_TAC arith_ss [EXP_EQ_0] THEN 562 DECIDE_TAC 563 ) THEN 564 565 `?a. SET_BINARY_ENCODING S2 = a * 2** (SUC n)` by ( 566 MP_TAC (Q.SPECL [`SUC n`, `S2`] SET_BINARY_ENCODING___REDUCE) THEN 567 `DISJOINT S2 (count (SUC n))` by PROVE_TAC[DISJOINT_DIFF] THEN 568 PROVE_TAC[] 569 ) THEN 570 571 Q.ABBREV_TAC `nc = (if n IN Sn then 1 else 0)` THEN 572 573 `SET_BINARY_ENCODING Sn = nc * 2**n` by ( 574 UNABBREV_ALL_TAC THEN 575 Cases_on `n IN S` THENL [ 576 `S INTER {n} = {n}` by ( 577 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_SING] THEN 578 METIS_TAC[] 579 ) THEN 580 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SING, IN_SING], 581 582 `S INTER {n} = EMPTY` by ( 583 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_SING, NOT_IN_EMPTY] 584 ) THEN 585 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_THM, NOT_IN_EMPTY] 586 ] 587 ) THEN 588 589 590 MP_TAC (Q.SPECL [`n`, `n`, `nc + 2*a`, `SET_BINARY_ENCODING S1`] BITS_SUM) THEN 591 ASM_SIMP_TAC arith_ss [RIGHT_ADD_DISTRIB] THEN 592 `2 * (a * 2 ** n) = a * 2 ** SUC n` by ( 593 SIMP_TAC arith_ss [EXP] 594 ) THEN 595 ASM_SIMP_TAC std_ss [BIT_def, BITS_SUM2] THEN 596 DISCH_TAC THEN POP_ASSUM (K ALL_TAC) THEN 597 598 REWRITE_TAC[GSYM BIT_def] THEN 599 Q.UNABBREV_TAC `nc` THEN 600 Cases_on `n IN Sn` THENL [ 601 ASM_SIMP_TAC std_ss [BIT_B], 602 ASM_SIMP_TAC std_ss [BIT_ZERO] 603 ] 604); 605 606 607 608 609 610val SET_BINARY_ENCODING___INJ = 611 store_thm ("SET_BINARY_ENCODING___INJ", 612 ``!S. FINITE S ==> INJ SET_BINARY_ENCODING (POW S) UNIV``, 613 614 SIMP_TAC std_ss [INJ_DEF, IN_UNIV, IN_POW, EXTENSION] THEN 615 PROVE_TAC[SET_BINARY_ENCODING___BITS, SUBSET_FINITE]); 616 617 618 619 620val SET_BINARY_ENCODING_SHIFT_def = 621 Define ` 622 SET_BINARY_ENCODING_SHIFT n1 n2 S = 623 (SET_BINARY_ENCODING (IMAGE (\n. n - n1) S) + n2)`; 624 625 626val SET_BINARY_ENCODING_SHIFT___INJ = 627 store_thm ("SET_BINARY_ENCODING_SHIFT___INJ", 628 ``!S n1 n2. (FINITE S /\ (!n. n IN S ==> n >= n1)) ==> INJ (SET_BINARY_ENCODING_SHIFT n1 n2) (POW S) UNIV``, 629 630 631 SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, INJ_DEF, IN_UNIV] THEN 632 REPEAT STRIP_TAC THEN 633 Q.ABBREV_TAC `f = (\n:num. n - n1)` THEN 634 FULL_SIMP_TAC std_ss [] THEN 635 `(IMAGE f x) IN POW (IMAGE f S) /\ 636 (IMAGE f y) IN POW (IMAGE f S)` by ( 637 FULL_SIMP_TAC std_ss [IN_POW, IMAGE_SUBSET] 638 ) THEN 639 `FINITE (IMAGE f S)` by ASM_SIMP_TAC std_ss [IMAGE_FINITE] THEN 640 `(IMAGE f x = IMAGE f y) <=> (x = y)` suffices_by METIS_TAC[SET_BINARY_ENCODING___INJ, INJ_DEF] THEN 641 642 MATCH_MP_TAC INJECTIVE_IMAGE_EQ THEN 643 REPEAT STRIP_TAC THEN 644 `x' >= n1 /\ y' >= n1` by ( 645 SIMP_ALL_TAC std_ss [IN_POW, IN_UNION, SUBSET_DEF] THEN 646 PROVE_TAC[] 647 ) THEN 648 Q.UNABBREV_TAC `f` THEN 649 FULL_SIMP_TAC arith_ss []); 650 651 652 653 654val SET_BINARY_ENCODING___IMAGE_THM = 655 store_thm ("SET_BINARY_ENCODING___IMAGE_THM", 656 657 ``!n. IMAGE SET_BINARY_ENCODING (POW (INTERVAL_SET 0 n)) = 658 INTERVAL_SET 0 (PRE (2**(SUC n)))``, 659 660 Induct_on `n` THENL [ 661 SIMP_TAC std_ss [INTERVAL_SET_0, EXTENSION, IN_IMAGE, IN_POW, IN_COUNT] THEN 662 `!s. s SUBSET count 1 <=> (s = {}) \/ (s = {0})` by ( 663 SIMP_TAC arith_ss [EXTENSION, SUBSET_DEF, IN_SING, NOT_IN_EMPTY, IN_COUNT] THEN 664 `!n. n < 1 <=> (n = 0)` by DECIDE_TAC THEN 665 METIS_TAC[] 666 ) THEN 667 ASM_SIMP_TAC std_ss [LEFT_AND_OVER_OR, EXISTS_OR_THM, SET_BINARY_ENCODING_THM, 668 SET_BINARY_ENCODING_SING] THEN 669 DECIDE_TAC, 670 671 672 673 Q.SUBGOAL_THEN `(POW (INTERVAL_SET 0 (SUC n))) = 674 ((POW (INTERVAL_SET 0 n)) UNION 675 (IMAGE (\S. (SUC n) INSERT S) (POW (INTERVAL_SET 0 n))))` 676 SUBST1_TAC THEN1 ( 677 SIMP_TAC std_ss [INTERVAL_SET_0, Q.SPEC `SUC n` COUNT_SUC, 678 POW_EQNS, LET_THM] THEN 679 SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_UNION] THEN 680 METIS_TAC[] 681 ) THEN 682 ASM_SIMP_TAC std_ss [IMAGE_UNION] THEN 683 684 685 Q.SUBGOAL_THEN `IMAGE SET_BINARY_ENCODING 686 (IMAGE (\S. SUC n INSERT S) (POW (INTERVAL_SET 0 n))) = 687 IMAGE (\x. 2**(SUC n) + x) (IMAGE SET_BINARY_ENCODING 688 (POW (INTERVAL_SET 0 n)))` SUBST1_TAC THEN1 ( 689 690 SIMP_TAC std_ss [IMAGE_IMAGE, combinTheory.o_DEF] THEN 691 MATCH_MP_TAC IMAGE_CONG THEN 692 SIMP_TAC std_ss [INTERVAL_SET_0, IN_POW] THEN 693 REPEAT STRIP_TAC THEN 694 `~(SUC n IN x)` by ( 695 CCONTR_TAC THEN 696 FULL_SIMP_TAC arith_ss [SUBSET_DEF, IN_COUNT] THEN 697 `SUC n < SUC n` by METIS_TAC[] THEN 698 DECIDE_TAC 699 ) THEN 700 `FINITE x` by METIS_TAC[SUBSET_FINITE, FINITE_COUNT] THEN 701 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_THM] 702 ) THEN 703 704 ASM_REWRITE_TAC[] THEN 705 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 706 SIMP_TAC std_ss [IN_UNION, IN_IMAGE, IN_INTERVAL_SET, EXP] THEN 707 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 708 ASM_SIMP_TAC arith_ss [], 709 ASM_SIMP_TAC arith_ss [], 710 711 RIGHT_DISJ_TAC THEN 712 Q_TAC EXISTS_TAC `x - (2 * 2**n)` THEN 713 FULL_SIMP_TAC arith_ss [] 714 ] 715 ]); 716 717 718 719 720 721val SET_BINARY_ENCODING_SHIFT___IMAGE_THM = 722 store_thm ("SET_BINARY_ENCODING_SHIFT___IMAGE_THM", 723 ``!n1 n2 n3. n1 <= n2 ==> 724 (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n3) (POW (INTERVAL_SET n1 n2)) = 725 INTERVAL_SET n3 (n3 + (PRE (2**(SUC (n2 - n1))))))``, 726 727 REPEAT STRIP_TAC THEN 728 729 Q.SUBGOAL_THEN `INTERVAL_SET n3 (n3 + PRE (2 ** SUC (n2 - n1))) = 730 IMAGE (\x:num. x + n3) (INTERVAL_SET 0 (PRE (2 ** SUC (n2 - n1))))` SUBST1_TAC THEN1 ( 731 732 SIMP_TAC arith_ss [INTERVAL_SET_def, IMAGE_ID] THEN 733 Q.ABBREV_TAC `n4 = PRE (2 ** SUC (n2 - n1))` THEN 734 `SUC (n3 + n4) - n3 = SUC n4` suffices_by METIS_TAC[] THEN 735 DECIDE_TAC 736 ) THEN 737 738 REWRITE_TAC [GSYM SET_BINARY_ENCODING___IMAGE_THM] THEN 739 740 ONCE_REWRITE_TAC[EXTENSION] THEN 741 SIMP_TAC std_ss [IN_IMAGE, SET_BINARY_ENCODING_SHIFT_def, 742 GSYM RIGHT_EXISTS_AND_THM, IN_POW] THEN 743 GEN_TAC THEN 744 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 745 Q.EXISTS_TAC `(IMAGE (\n. n - n1) x')` THEN 746 FULL_SIMP_TAC arith_ss [PULL_EXISTS, SUBSET_DEF, IN_INTERVAL_SET, IN_IMAGE], 747 748 749 Q_TAC EXISTS_TAC `(IMAGE (\n. n + n1) x'')` THEN 750 ASM_SIMP_TAC arith_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF, 751 IMAGE_ID] THEN 752 FULL_SIMP_TAC arith_ss [SUBSET_DEF, IN_INTERVAL_SET, IN_IMAGE, PULL_EXISTS] THEN 753 GEN_TAC THEN STRIP_TAC THEN 754 RES_TAC THEN 755 DECIDE_TAC 756 ]); 757 758 759 760 761 762val SET_BINARY_ENCODING_SHIFT___INSERT = 763 store_thm ("SET_BINARY_ENCODING_SHIFT___INSERT", 764``!i k l S. FINITE S /\ (i <= l) /\ ~(l IN S) /\ (!x. x IN S ==> i <= x) ==> 765(SET_BINARY_ENCODING_SHIFT i k (l INSERT S) = 766 SET_BINARY_ENCODING_SHIFT i (2**(l-i)+k) S)``, 767 768SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT_def, 769 SET_BINARY_ENCODING_def, SUM_IMAGE_THM, IMAGE_INSERT, 770 IMAGE_FINITE] THEN 771REPEAT STRIP_TAC THEN 772AP_TERM_TAC THEN 773SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_DELETE] THEN 774REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 775 PROVE_TAC[], 776 PROVE_TAC[], 777 778 RES_TAC THEN 779 `n = l` by DECIDE_TAC THEN 780 PROVE_TAC[] 781]); 782 783val _ = export_theory(); 784