1(* ------------------------------------------------------------------------- *) 2(* Pattern Theory. *) 3(* List patterns to be investigated by similar lists. *) 4(* List sub-patterns to be investigated with period and order. *) 5(* ------------------------------------------------------------------------- *) 6 7(* 8 9This is applying the new cycle theory to the original Necklace Proof, 10i.e. using the idea of action, but not explicitly mentioning it. 11 12Cycle Theory 13============ 14 15Necklaces are represented by linear lists of length n. 16 17Since they are necklaces, it is natural to join them end to end. For example, 18the following "cycling" necklaces are considered equivalent: 19 20+--+--+--+--+--+--+--+ 21|2 |4 |0 |3 |1 |2 |3 | 22+--+--+--+--+--+--+--+ 23|4 |0 |3 |1 |2 |3 |2 | 24+--+--+--+--+--+--+--+ 25|0 |3 |1 |2 |3 |2 |4 | 26+--+--+--+--+--+--+--+ 27|3 |1 |2 |3 |2 |4 |0 | 28+--+--+--+--+--+--+--+ 29|1 |2 |3 |2 |4 |0 |3 | 30+--+--+--+--+--+--+--+ 31|2 |3 |2 |4 |0 |3 |1 | 32+--+--+--+--+--+--+--+ 33|3 |2 |4 |0 |3 |1 |2 | (next cycle identical to first) 34+--+--+--+--+--+--+--+ 35 36We shall define and investigate the "cycle" operation on a list. 37 38We shall consider a "similar" relation between lists via cycling. 39 40We shall prove that "similar" is reflexive, symmetric and transitive. 41 42Hence "similar" is an equivalence relation, giving partitions via 43equivalent classes on necklaces of length n. 44 45Cycle Order Theory 46================== 47 48The basic cycle theory considers necklaces of length n, ignoring its colors. 49 50Ignoring colors, there are only two ways that guarantee cycling to the original: 51(1) with 0 steps: cycle 0 l = l 52(2) with n steps: cycle n l = l where n = length of the list. 53 54With colors, necklaces have patterns, which may consist of sub-patterns. 55 56This give rise to the concept of order: the least number of steps to cycle 57the necklace to its original. The trivial case of 0 steps is excluded to 58make the least number interesting. 59 60The main result of this investigation are: 61(a) the order k must divide the length n. 62(b) the order k of a list is the cardinality of the list's associate, 63 the equivalent class of "similar" relation with the given list. 64 65Example of order/associate: 66 67Take LENGTH l = 4, e.g. l = [2;3;2;3] 68 69 cycle 0 l = [2;3;2;3] 70 cycle 1 l = [3;2;3;2] 71 cycle 2 l = [2;3;2;3] 72 cycle 3 l = [3;2;3;2] 73 cycle 4 l = [2;3;2;3] 74 75 So, similar in this set is true: 76 similar l l 77 similar l1 l2 ==> similar l2 l1 78 similar l1 l2 /\ similar l2 l3 ==> similar l1 l3 79 80 However, the size of this set is 2, not LENGTH l = 4. 81 82 Hence for n = 4 (length of necklace), a = 2 (colors) 83 The set of multicoloured necklaces = M, with CARD M = a^n - a = 2^4 - 2 = 16 - 2 = 14. 84 85 Let the colors be {0,1}. The 14 multicoloured necklaces are: 86 87 #01 [0;0;0;1] cycle with: #02, #04, #08, size of set = 4. 88 #02 [0;0;1;0] (see #01) 89 #03 [0;0;1;1] cycle with: #06, #12, #09, size of set = 4. 90 #04 [0;1;0;0] (see #01) 91 #05 [0;1;0;1] cycle with: #10, size of set = 2. 92 #06 [0;1;1;0] (see #03) 93 #07 [0;1;1;1] cycle with: #14, #13, #11, size of set = 4. 94 #08 [1;0;0;0] (see #01) 95 #09 [1;0;0;1] (see #03) 96 #10 [1;0;1;0] (see #05) 97 #11 [1;0;1;1] (see #07) 98 #12 [1;1;0;0] (see #03) 99 #13 [1;1;0;1] (see #07) 100 #14 [1;1;1;0] (see #07) 101 102 That is, similar partitions the set, but the partitions are of different sizes. 103 Note that: 4 + 4 + 2 + 4 = 14 = a^n - a. 104 105*) 106 107(*===========================================================================*) 108 109(*===========================================================================*) 110 111(* add all dependent libraries for script *) 112open HolKernel boolLib bossLib Parse; 113 114(* declare new theory at start *) 115val _ = new_theory "pattern"; 116 117(* ------------------------------------------------------------------------- *) 118 119 120(* open dependent theories *) 121(* val _ = load "cycleTheory"; *) 122open arithmeticTheory pred_setTheory listTheory; 123open helperNumTheory helperSetTheory; 124open helperListTheory; (* for LENGTH_NON_NIL *) 125 126open cycleTheory; 127 128open dividesTheory; (* for prime_def, NOT_PRIME_0 *) 129 130 131(* ------------------------------------------------------------------------- *) 132(* Pattern Theory Documentation *) 133(* ------------------------------------------------------------------------- *) 134(* Overloading: 135 l1 == l2 = similar l1 l2 (infix) 136 closed R s = !x y. x IN s /\ R x y ==> y IN s 137*) 138(* 139 140 Pattern Theory: 141 similar_def |- !l1 l2. l1 == l2 <=> ?n. l2 = cycle n l1 142 similar_nil |- !ls. ls == [] \/ [] == ls <=> ls = [] 143 similar_length |- !l1 l2. l1 == l2 ==> LENGTH l1 = LENGTH l2 144 similar_refl |- !ls. ls == ls 145 similar_sym |- !l1 l2. l1 == l2 ==> l2 == l1 146 similar_trans |- !l1 l2 l3. l1 == l2 /\ l2 == l3 ==> l1 == l3 147 148 Similar associates: 149 associate_def |- !x. associate x = {y | x == y} 150 associate_element |- !x y. y IN associate x <=> x == y 151 associate_nil |- associate [] = {[]} 152 associate_has_self |- !x. x IN associate x 153 associate_nonempty |- !x. associate x <> {} 154 associate_eq_similar_class 155 |- !x s. x IN s /\ closed similar s ==> 156 associate x = equiv_class similar s x 157 associate_as_image |- !ls. ls <> [] ==> 158 associate ls = IMAGE (\n. cycle n ls) (count (LENGTH ls)) 159 associate_finite |- !ls. FINITE (associate ls) 160 associate_card_upper|- !ls. ls <> [] ==> CARD (associate ls) <= LENGTH ls 161 162 Period of a list: 163 period_def |- !ls k. period ls k <=> 0 < k /\ cycle k ls = ls 164 cycle_period_exists |- !ls. ls <> [] ==> period ls (LENGTH ls) 165 cycle_period_multiple 166 |- !n k ls. 0 < n /\ period ls k ==> period ls (n * k) 167 cycle_period_similar|- !k x y. period x k /\ x == y ==> period y k 168 169 Order of a list: 170 order_def |- !ls. order ls = LEAST k. period ls k 171 cycle_order_period |- !ls. ls <> [] ==> period ls (order ls) 172 cycle_order_minimal |- !k ls. ls <> [] /\ k < order ls ==> ~period ls k 173 cycle_order_property|- !ls. ls <> [] ==> 0 < order ls /\ cycle (order ls) ls = ls 174 cycle_order_eqn |- !n ls. ls <> [] ==> 175 (n = order ls <=> 0 < n /\ cycle n ls = ls /\ 176 !j. 0 < j /\ j < n ==> cycle j ls <> ls) 177 cycle_order_multiple|- !n ls. cycle (n * order ls) ls = ls 178 cycle_mod_order |- !n ls. cycle n ls = cycle (n MOD order ls) ls 179 cycle_order_divides_length 180 |- !ls. ls <> [] ==> LENGTH ls MOD order ls = 0 181 cycle_order_similar |- !x y. x == y ==> order x = order y 182 183 Deduction of associate cardinality: 184 associate_eq_order_image 185 |- !ls. ls <> [] ==> 186 associate ls = IMAGE (\n. cycle n ls) (count (order ls)) 187 associate_order_map_surj 188 |- !ls. ls <> [] ==> 189 SURJ (\n. cycle n ls) (count (order ls)) (associate ls) 190 associate_order_map_inj_imp 191 |- !m n ls. ls <> [] /\ m < order ls /\ n < order ls /\ m <= n /\ 192 cycle m ls = cycle n ls ==> m = n 193 associate_order_map_inj 194 |- !ls. ls <> [] ==> 195 INJ (\n. cycle n ls) (count (order ls)) (associate ls) 196 associate_order_map_bij 197 |- !ls. ls <> [] ==> 198 BIJ (\n. cycle n ls) (count (order ls)) (associate ls) 199 associate_card_eq_order 200 |- !ls. ls <> [] ==> CARD (associate ls) = order ls 201 associate_card_divides_length 202 |- !ls. ls <> [] ==> LENGTH ls MOD CARD (associate ls) = 0 203 204 Cycle 1 and Order 1: 205 cycle_1_eq_order_1 |- !ls. ls <> [] ==> (cycle 1 ls = ls <=> order ls = 1) 206 cycle_order_prime_length 207 |- !ls. prime (LENGTH ls) ==> 208 order ls = 1 \/ order ls = LENGTH ls 209 associate_card_prime_length 210 |- !ls. prime (LENGTH ls) ==> 211 CARD (associate ls) = 1 \/ CARD (associate ls) = LENGTH ls 212 213*) 214 215(* ------------------------------------------------------------------------- *) 216(* Two lists are similar if they are related through cycle. *) 217(* ------------------------------------------------------------------------- *) 218 219(* Define similar to relate two lists *) 220val similar_def = zDefine` 221 similar l1 l2 = ?n. l2 = cycle n l1 222`; 223(* Note: use zDefine as this is not effective. *) 224 225(* set infix and overload for similar *) 226val _ = set_fixity "==" (Infixl 480); 227val _ = overload_on ("==", ``similar``); 228 229(* ------------------------------------------------------------------------- *) 230(* Know about Similar between Cycles. *) 231(* ------------------------------------------------------------------------- *) 232 233(* Idea: only NIL can be similar to NIL. *) 234 235(* Theorem: ls == [] \/ [] == ls <=> ls = [] *) 236(* Proof: 237 ls == [] \/ [] == ls 238 <=> ?n. [] = cycle n ls \/ ?n. ls = cycle n [] by similar_def 239 <=> ls = [] by cycle_eq_nil, any n 240*) 241Theorem similar_nil: 242 !ls. ls == [] \/ [] == ls <=> ls = [] 243Proof 244 metis_tac[similar_def, cycle_eq_nil] 245QED 246 247(* Idea: only same length lists can be similar to each other. *) 248 249(* Theorem: l1 == l2 ==> LENGTH l1 = LENGTH l2 *) 250(* Proof: 251 l1 == l2 252 ==> ?n. l2 = cycle n l1 by similar_def 253 ==> LENGTH l2 = LENGTH l1 by cycle_same_length 254*) 255Theorem similar_length: 256 !l1 l2. l1 == l2 ==> LENGTH l1 = LENGTH l2 257Proof 258 metis_tac[similar_def, cycle_same_length] 259QED 260 261(* ------------------------------------------------------------------------- *) 262(* Show that Similar is an equivalence relation. *) 263(* ------------------------------------------------------------------------- *) 264 265(* Idea: similar is reflexive. *) 266 267(* Theorem: ls == ls *) 268(* Proof: 269 ls == ls 270 <=> ?n. ls = cycle n ls by similar_def 271 Take n = 0, 272 cycle 0 ls = ls by cycle_0 273*) 274Theorem similar_refl: 275 !ls. ls == ls 276Proof 277 metis_tac[similar_def, cycle_0] 278QED 279 280(* Idea: similar is symmetric. *) 281 282(* Theorem: l1 == l2 ==> l2 == l1 *) 283(* Proof: 284 If l1 = [], 285 Then l2 = [] by similar_nil 286 so l2 == [] by similar_nil 287 If l1 <> [], 288 Let k = LENGTH l1. 289 Then k <> 0 by LENGTH_NIL, l1 <> [] 290 Note l1 == l2 means 291 ?n. l2 = cycle n l1 by similar_def 292 and n MOD k < k by MOD_LESS, 0 < k 293 Let m = k - (n MOD k). 294 cycle m l2 295 = cycle m (cycle (n MOD k) l1) by cycle_mod_length 296 = l1 by cycle_inv 297 Hence l2 == l1 by similar_def 298*) 299Theorem similar_sym: 300 !l1 l2. (l1 == l2) ==> (l2 == l1) 301Proof 302 rw[similar_def] >> 303 Cases_on `l1 = []` >- 304 metis_tac[cycle_eq_nil] >> 305 qabbrev_tac `k = LENGTH l1` >> 306 qexists_tac `k - (n MOD k)` >> 307 `0 < k` by fs[LENGTH_NON_NIL, Abbr`k`] >> 308 `n MOD k < k` by rw[MOD_LESS] >> 309 `n MOD k <= k` by decide_tac >> 310 metis_tac[cycle_mod_length, cycle_inv] 311QED 312 313(* Idea: similar is transitive. *) 314 315(* Theorem: l1 == l2 /\ l2 == l3 ==> l1 == l3 *) 316(* Proof: 317 Note l1 == l2 ==> ?n1. l2 = cycle n1 l1 by similar_def 318 and l2 == l3 ==> ?n2. l3 = cycle n2 l2 by similar_def 319 l3 = cycle n2 l2 320 = cycle n2 (cycle n1 l1) 321 = cycle (n2 + n1) l1 by cycle_add 322 Thus l1 == l3 by similar_def 323*) 324Theorem similar_trans: 325 !l1 l2 l3. (l1 == l2) /\ (l2 == l3) ==> (l1 == l3) 326Proof 327 metis_tac[similar_def, cycle_add] 328QED 329 330(* ------------------------------------------------------------------------- *) 331(* Similar associates. *) 332(* ------------------------------------------------------------------------- *) 333 334(* Define the associate of list: all those that are similar to the list. *) 335val associate_def = zDefine ` 336 associate x = {y | x == y } 337`; 338(* Note: use zDefine as this is not effective. *) 339 340(* Theorem: y IN associate x <=> x == y *) 341(* Proof: by associate_def. *) 342Theorem associate_element: 343 !x y. y IN associate x <=> x == y 344Proof 345 simp[associate_def] 346QED 347 348(* ------------------------------------------------------------------------- *) 349(* Know the associates. *) 350(* ------------------------------------------------------------------------- *) 351 352(* Idea: associate NIL is singleton {NIL}. *) 353 354(* Theorem: associate [] = {[]} *) 355(* Proof: 356 associate [] 357 = {y | [] == y} by associate_def 358 = {[]} by similar_nil 359*) 360Theorem associate_nil: 361 associate [] = {[]} 362Proof 363 rw[associate_def, EXTENSION] >> 364 metis_tac[similar_nil] 365QED 366 367(* Idea: associate x has x itself. *) 368 369(* Theorem: x IN associate x *) 370(* Proof: 371 Note x == x by similar_refl 372 so x IN associate x by associate_element 373*) 374Theorem associate_has_self: 375 !x. x IN associate x 376Proof 377 metis_tac[similar_refl, associate_element] 378QED 379 380(* Idea: associate x is non-EMPTY. *) 381 382(* Theorem: associate x <> {} *) 383(* Proof: 384 Note x IN associate x by associate_has_self 385 ==> associate x <> {} by MEMBER_NOT_EMPTY 386*) 387Theorem associate_nonempty: 388 !x. associate x <> {} 389Proof 390 metis_tac[associate_has_self, MEMBER_NOT_EMPTY] 391QED 392 393(* ------------------------------------------------------------------------- *) 394(* Associates as equivalent classes. *) 395(* ------------------------------------------------------------------------- *) 396 397(* Overload a closed relation R on set s *) 398val _ = overload_on("closed", ``\R s. !x y. x IN s /\ R x y ==> y IN s``); 399 400(* Idea: associates are equivalent classes of similar, for sets closed under similar. *) 401 402(* Theorem: x IN s /\ (closed similar s) ==> 403 associate x = equiv_class similar s x *) 404(* Proof: 405 By EXTENSION, this is to show: 406 x IN s /\ closed $== s ==> (y IN associate x <=> y IN s /\ x == y) 407 But y IN associate x <=> x == y by associate_element 408 and x == y ==> y IN s by closed notation 409 Hence true. 410*) 411Theorem associate_eq_similar_class: 412 !x s. x IN s /\ (closed similar s) ==> 413 associate x = equiv_class similar s x 414Proof 415 rw[associate_def, EXTENSION] >> 416 metis_tac[] 417QED 418 419(* ------------------------------------------------------------------------- *) 420(* To show: associates are FINITE. *) 421(* ------------------------------------------------------------------------- *) 422 423(* Idea: the map (\n. cycle n ls): count (LENGTH ls) -> (associate ls) 424 is surjective. *) 425 426(* Theorem: ls <> [] ==> 427 associate ls = IMAGE (\n. cycle n ls) (count (LENGTH ls)) *) 428(* Proof: 429 Let k = LENGTH ls, then 0 < k by LENGTH_NIL 430 and n MOD k < k by MOD_LESS, 0 < k 431 By associate_def, similar_def this is to prove: 432 (1) ls <> [] ==> ?n'. (cycle n ls = cycle n' ls) /\ n' < k 433 Take n' = n MOD k, then true by cycle_mod_length 434 (2) ls <> [] /\ n < k ==> ?n'. cycle n ls = cycle n' ls 435 Take n' = n LENGTH ls, then true by cycle_mod_length 436*) 437Theorem associate_as_image: 438 !ls. ls <> [] ==> 439 associate ls = IMAGE (\n. cycle n ls) (count (LENGTH ls)) 440Proof 441 rw[associate_def, similar_def, EXTENSION, EQ_IMP_THM] >- 442 metis_tac[cycle_mod_length, LENGTH_NIL, MOD_LESS, NOT_ZERO] >> 443 metis_tac[cycle_mod_length] 444QED 445 446(* Idea: (associate ls) is FINITE. *) 447 448(* Theorem: FINITE (associate ls) *) 449(* Proof: 450 If ls = [], 451 associate [] = {[]) by associate_nil 452 hence FINITE. 453 If ls <> [], 454 Let k = LENGTH ls. 455 associate ls 456 = IMAGE (\n. cycle n ls) (count k) 457 by associate_as_image 458 Note FINITE (count k) by FINITE_COUNT 459 so FINITE (associate ls) by IMAGE_FINITE 460*) 461Theorem associate_finite: 462 !ls. FINITE (associate ls) 463Proof 464 rpt strip_tac >> 465 Cases_on `ls` >- 466 rw[associate_nil] >> 467 rw[associate_as_image] 468QED 469 470(* ------------------------------------------------------------------------- *) 471(* To give an estimate of CARD (associate ls). *) 472(* ------------------------------------------------------------------------- *) 473 474(* Idea: size of (associate ls) <= LENGTH ls. *) 475 476(* Theorem: ls <> [] ==> CARD (associate ls) <= LENGTH ls *) 477(* Proof: 478 Let k = LENGTH ls. 479 Note FINITE (count k) by FINITE_COUNT 480 CARD (associate ls) 481 = CARD (IMAGE (\n. cycle n ls) (count k)) by associate_as_image 482 <= CARD (count k) by CARD_IMAGE 483 = k by CARD_COUNT 484*) 485Theorem associate_card_upper: 486 !ls. ls <> [] ==> CARD (associate ls) <= LENGTH ls 487Proof 488 metis_tac[associate_as_image, FINITE_COUNT, CARD_IMAGE, CARD_COUNT] 489QED 490 491(* ------------------------------------------------------------------------- *) 492(* Cycle sub-patterns *) 493(* ------------------------------------------------------------------------- *) 494 495(* We know: cycle_0 cycle 0 ls = ls. 496 and: cycle_back cycle (LENGTH ls) ls = ls. 497 Is there some 0 < k < LENGTH ls such that cycle k ls = ls ? 498 If there is such a k, it is very special, 499 by the DIVISION algorithm and nature of cycle. 500*) 501 502(* ------------------------------------------------------------------------- *) 503(* Period of a list. *) 504(* ------------------------------------------------------------------------- *) 505 506(* Define period k for a list ls, as a predicate. *) 507Definition period_def: 508 period ls k <=> 0 < k /\ cycle k ls = ls 509End 510(* Note: 511 . 0 is excluded as a period. 512 . Since LENGTH [] = 0, [] cannot have a period. 513*) 514 515(* Idea: a non-NIL list has a period: its length. *) 516 517(* Theorem: ls <> [] ==> period ls (LENGTH ls) *) 518(* Proof: 519 Let k = LENGTH ls. 520 By period_def, this is to show: 521 (1) 0 < k, true by LENGTH_NON_NIL 522 (2) cycle k ls = ls, true by cycle_back 523*) 524Theorem cycle_period_exists: 525 !ls. ls <> [] ==> period ls (LENGTH ls) 526Proof 527 simp[period_def, LENGTH_NON_NIL, cycle_back] 528QED 529 530(* Idea: if list ls has period k, then multiples of k are also periods. *) 531 532(* Theorem: 0 < n /\ period ls k ==> period ls (n * k) *) 533(* Proof: 534 Note 0 < k /\ cycle k ls = ls by period_def 535 By period_def, this is to show: 536 (1) 0 < n * k, true by LESS_MULT2 537 (2) cycle (n * k) ls = ls, true by cycle_multiple_back 538*) 539Theorem cycle_period_multiple: 540 !n k ls. 0 < n /\ period ls k ==> period ls (n * k) 541Proof 542 rw[period_def] >> 543 metis_tac[cycle_multiple_back, MULT_COMM] 544QED 545 546(* Idea: if list x has period k, and x == y, then k is also a period of y. *) 547 548(* Theorem: period x k /\ x == y ==> period y k *) 549(* Proof: 550 Note 0 < k /\ (cycle n x = x) by period_def 551 and ?n. y = cycle n x by similar_def 552 cycle k (cycle n x) 553 = cycle (k + n) x by cycle_add 554 = cycle (n + k) x by ADD_COMM 555 = cycle n (cycle k x) by cycle_add 556 = cycle n x by k being a period 557*) 558Theorem cycle_period_similar: 559 !k x y. period x k /\ x == y ==> period y k 560Proof 561 rw[period_def, similar_def] >> 562 metis_tac[cycle_add, ADD_COMM] 563QED 564 565(* ------------------------------------------------------------------------- *) 566(* Order of a list - or minimal period of a list. *) 567(* ------------------------------------------------------------------------- *) 568 569(* Define order as minimal period of a list. *) 570Definition order_def: 571 order ls = LEAST k. period ls k 572End 573 574(* 575> EVAL ``order [2;3;2;3]``; = 2 576> EVAL ``order [2;3;2;3;2]``; = 5 577*) 578 579(* Idea: the list order is indeed a period. *) 580 581(* Theorem: ls <> [] ==> period ls (order ls) *) 582(* Proof: 583 Let k = LENGTH ls. 584 Note period ls k by cycle_period_exists 585 so period ls ($LEAST (period ls k)) by LEAST_INTRO 586 or period ls (order ls) by order_def 587*) 588Theorem cycle_order_period: 589 !ls. ls <> [] ==> period ls (order ls) 590Proof 591 rw[order_def] >> 592 metis_tac[cycle_period_exists, whileTheory.LEAST_INTRO] 593QED 594 595(* Idea: if k < list order, k is not a period. *) 596 597(* Theorem: ls <> [] /\ k < order ls ==> ~(period ls k) *) 598(* Proof: 599 Let m = LENGTH ls. 600 Note period ls m by cycle_period_exists 601 k < order ls 602 ==> k < $LEAST (period ls m) by order_def 603 ==> ~(period ls k) by LESS_LEAST 604*) 605Theorem cycle_order_minimal: 606 !k ls. ls <> [] /\ k < order ls ==> ~(period ls k) 607Proof 608 rw[order_def] >> 609 metis_tac[cycle_period_exists, whileTheory.LESS_LEAST] 610QED 611 612(* Idea: the list order is positive and a period. *) 613 614(* Theorem: ls <> [] ==> 0 < order ls /\ cycle (order ls) ls = ls *) 615(* Proof: 616 Note period ls (order ls) by cycle_order_period 617 so 0 < order ls /\ 618 cycle (order ls) ls = ls by period_def 619*) 620Theorem cycle_order_property: 621 !ls. ls <> [] ==> 0 < order ls /\ cycle (order ls) ls = ls 622Proof 623 metis_tac[cycle_order_period, period_def] 624QED 625 626(* Idea: a criterion to determine list order. *) 627 628(* Theorem: ls <> [] ==> (n = order ls <=> 629 0 < n /\ cycle n ls = ls /\ !j. 0 < j /\ j < n ==> cycle j ls <> ls) *) 630(* Proof: 631 If part: n = order ls ==> 0 < n /\ cycle n ls = ls /\ 632 (!j. 0 < j /\ j < n ==> cycle j ls <> ls) 633 Note 0 < n /\ cycle n ls = ls by cycle_order_property 634 and !j. 0 < j /\ j < n 635 ==> ~period ls j by cycle_order_minimal 636 ==> cycle j ls <> ls by period_def 637 Only-if part: 0 < n /\ cycle n ls = ls /\ 638 (!j. 0 < j /\ j < n ==> cycle j ls <> ls) ==> n = order ls 639 By order_def, period_def, and eliminating LEAST by LEAST_ELIM_TAC, 640 this is to show: 641 (1) 0 < n /\ cycle n ls = ls ==> ?n'. 0 < n' /\ (cycle n' ls = ls) 642 Take n' = n, then true. 643 (2) (!m. m < n' ==> (m = 0) \/ cycle m ls <> ls) /\ 644 0 < n' /\ cycle n' ls = ls ==> n = n' 645 By contradiction, suppose n <> n'. 646 Then n < n' or n' < n. 647 If n < n', then cycle n ls <> ls by second given implication 648 which contradicts cycle n ls = ls. 649 If n' < n. then cycle n ls <> ls by first given implication 650 which contradicts cycle n' ls = ls. 651*) 652Theorem cycle_order_eqn: 653 !n ls. ls <> [] ==> (n = order ls <=> 654 0 < n /\ cycle n ls = ls /\ !j. 0 < j /\ j < n ==> cycle j ls <> ls) 655Proof 656 (rw[EQ_IMP_THM] >> simp[cycle_order_property]) >- 657 metis_tac[cycle_order_minimal, period_def] >> 658 rw[order_def] >> 659 numLib.LEAST_ELIM_TAC >> 660 rw[period_def] >- 661 metis_tac[] >> 662 spose_not_then strip_assume_tac >> 663 `n < n' \/ n' < n` by decide_tac >- 664 metis_tac[NOT_ZERO] >> 665 metis_tac[] 666QED 667 668(* Idea: cycle through multiples of order is still itself. *) 669 670(* Theorem: cycle (n * (order ls)) ls = ls. *) 671(* Proof: 672 If ls = [], 673 This is true by cycle_nil 674 Otherwise ls <> [], 675 If n = 0, 676 cycle (0 * (order ls)) ls 677 = cycle 0 ls by MULT 678 = ls by cycle_0 679 If n <> 0, 0 < n. 680 Let p = order ls. 681 Note period ls p by cycle_order_period 682 ==> period ls (n * p) by cycle_period_multiple 683 so cycle (n * p) ls = ls by period_def 684*) 685Theorem cycle_order_multiple: 686 !n ls. cycle (n * (order ls)) ls = ls 687Proof 688 rpt strip_tac >> 689 Cases_on `ls = []` >- 690 simp[cycle_nil] >> 691 Cases_on `n = 0` >- 692 simp[cycle_0] >> 693 metis_tac[cycle_order_period, cycle_period_multiple, period_def, NOT_ZERO] 694QED 695 696(* Idea: the number of cycles can be reduced by multiples of order. *) 697 698(* Theorem: cycle n ls = cycle (n MOD (order ls)) ls *) 699(* Proof: 700 If ls = [], 701 This is true by cycle_nil 702 Otherwise ls <> [], 703 Let k = order ls. 704 Then 0 < k by cycle_order_property 705 Let q = n DIV k, r = n MOD k. 706 Then n = q * k + r by DIVISION, 0 < k 707 cycle n ls 708 = cycle (r + q * k) ls by above 709 = cycle r (cycle (q * k) ls) by cycle_add 710 = cycle r ls by cycle_order_multiple 711*) 712Theorem cycle_mod_order: 713 !n ls. cycle n ls = cycle (n MOD (order ls)) ls 714Proof 715 rpt strip_tac >> 716 Cases_on `ls = []` >- 717 simp[cycle_nil] >> 718 qabbrev_tac `k = order ls` >> 719 qabbrev_tac `q = n DIV k` >> 720 qabbrev_tac `r = n MOD k` >> 721 `0 < k` by metis_tac[cycle_order_property] >> 722 `n = q * k + r` by rw[DIVISION, Abbr`q`, Abbr`r`] >> 723 `_ = r + q * k` by decide_tac >> 724 metis_tac[cycle_add, cycle_order_multiple] 725QED 726 727(* Idea: the list order divides its length. *) 728 729(* Theorem: ls <> [] ==> LENGTH ls MOD (order ls) = 0 *) 730(* Proof: 731 Let n = LENGTH ls = n, k = order ls, q = n DIV k, r = n MOD k. 732 Then cycle k ls = ls by cycle_order_period 733 and n = q * k + r with r < k by DIVISION, [1] 734 cycle r ls 735 = cycle r (cycle (q * k) ls) by cycle_period_multiple 736 = cycle (r + q * k) ls by cycle_add 737 = cycle n ls by arithmetic, [1] 738 = ls by cycle_back 739 If r <> 0, 740 then cycle r ls = ls by cycle_order_multiple 741 so period ls r by period_def, 0 < r 742 This contradicts 743 r < k ==> ~period ls r by cycle_order_minimal 744 Thus r = 0, or r = n MOD k = 0 by MOD_UNIQUE 745*) 746Theorem cycle_order_divides_length: 747 !ls. ls <> [] ==> LENGTH ls MOD (order ls) = 0 748Proof 749 rpt strip_tac >> 750 qabbrev_tac `n = LENGTH ls` >> 751 qabbrev_tac `k = order ls` >> 752 `0 < k /\ cycle k ls = ls` by rw[cycle_order_property, Abbr`k`] >> 753 qabbrev_tac `q = n DIV k` >> 754 qabbrev_tac `r = n MOD k` >> 755 `n = q * k + r /\ r < k` by rw[DIVISION, Abbr`q`, Abbr`r`] >> 756 (Cases_on `r = 0` >> simp[]) >> 757 `cycle r ls = ls` by metis_tac[cycle_order_multiple, cycle_add, cycle_back, ADD_COMM] >> 758 metis_tac[cycle_order_minimal, period_def, NOT_ZERO] 759QED 760 761(* ------------------------------------------------------------------------- *) 762(* Similar lists have the same order. *) 763(* ------------------------------------------------------------------------- *) 764 765(* Idea: if list x has order k, and x == y, then k is also a order of y. *) 766 767(* Theorem: x == y ==> order x k = order y k *) 768(* Proof: 769 If x = [] or y = [], 770 then x = y = [] by similar_nil 771 hence true. 772 Otherwise x <> [] and y <> []. 773 Let a = order x, b = order y. 774 Note x == y ==> y == x by similar_sym 775 so period x b and period y a by cycle_order_period, cycle_period_similar 776 if a < b, a contradiction by cycle_order_minimal 777 if b < a, a contradiction by cycle_order_minimal 778 thus a = b. 779*) 780Theorem cycle_order_similar: 781 !x y. x == y ==> order x = order y 782Proof 783 rpt strip_tac >> 784 Cases_on `(x = []) \/ (y = [])` >- 785 metis_tac[similar_nil] >> 786 `y == x` by rw[similar_sym] >> 787 `period x (order y) /\ period y (order x)` by metis_tac[cycle_order_period, cycle_period_similar] >> 788 qabbrev_tac `a = order x` >> 789 qabbrev_tac `b = order y` >> 790 (`a = b \/ a < b \/ b < a` by decide_tac >> metis_tac[cycle_order_minimal]) 791QED 792 793(* ------------------------------------------------------------------------- *) 794(* Deduction of associate cardinality. *) 795(* ------------------------------------------------------------------------- *) 796 797(* Idea: for k = order ls, associate ls = IMAGE (\n. cycle n ls) (count k). *) 798 799(* Theorem: ls <> [] ==> 800 associate ls = IMAGE (\n. cycle n ls) (count (order ls)) *) 801(* Proof: 802 Let k = order ls. 803 By SUBSET_ANTISYM, this is to show: 804 (1) (associate ls) SUBSET IMAGE (\n. cycle n ls) (count (order ls)) 805 x IN associate ls 806 <=> ls == x by associate_def 807 <=> ?n. x = cycle n ls by similar_def 808 = cycle (n MOD k) ls 809 by cycle_mod_order 810 Now 0 < k by cycle_order_property 811 so n MOD k < k by MOD_LESS 812 ==> x IN IMAGE (\n. cycle n ls) (count k) 813 by IN_IMAGE 814 (2) IMAGE (\n. cycle n ls) (count (order ls)) SUBSET (associate ls) 815 x IN IMAGE (\n. cycle n ls) (count k) 816 <=> ?n. n IN (count k) /\ (x = cycle n ls) 817 by IN_IMAGE 818 ==> ?n. x = cycle n ls 819 <=> ls == x by similar_def 820 <=> x IN associate ls by associate_def 821*) 822Theorem associate_eq_order_image: 823 !ls. ls <> [] ==> 824 associate ls = IMAGE (\n. cycle n ls) (count (order ls)) 825Proof 826 rpt strip_tac >> 827 irule SUBSET_ANTISYM >> 828 rw[SUBSET_DEF, associate_def, similar_def] >| [ 829 qabbrev_tac `k = order ls` >> 830 `0 < k` by rw[cycle_order_property, Abbr`k`] >> 831 `n MOD k < k` by rw[MOD_LESS] >> 832 metis_tac[cycle_mod_order], 833 metis_tac[] 834 ] 835QED 836 837(* Idea: for order k, (\n. cycle n ls) (count k) (associate ls) is surjective. *) 838 839(* Theorem: ls <> [] ==> 840 SURJ (\n. cycle n ls) (count (order ls)) (associate ls) *) 841(* Proof: 842 Let k = order ls, f = (\n. cycle n ls). 843 Note IMAGE f (count k) = associate ls by associate_eq_order_image, ls <> [] 844 so SURJ f (count k) (associate ls) by IMAGE_SURJ 845*) 846Theorem associate_order_map_surj: 847 !ls. ls <> [] ==> 848 SURJ (\n. cycle n ls) (count (order ls)) (associate ls) 849Proof 850 simp[IMAGE_SURJ, associate_eq_order_image] 851QED 852 853(* Idea: for order k, x < k and y < k and x <= y, 854 cycle x ls = cycle y ls ==> x = y. *) 855 856(* Theorem: ls <> [] /\ m < order ls /\ n < order ls /\ 857 m <= n /\ cycle m ls = cycle n ls ==> m = n *) 858(* Proof: 859 Let k = order ls, then 0 < k by cycle_order_property 860 Let d = n - m, then n = d + m by arithmetic 861 Suppose d <> 0. 862 Then 0 < d, and d <= n < k, so d < k. 863 cycle d (cycle n ls) 864 = cycle d (cycle m ls) by given 865 = cycle (d + m) ls by cycle_add 866 = cycle n ls by n = d + m 867 Thus period (cycle n ls) d by period_def 868 But ls == cycle n ls by similar_def 869 so cycle n ls == ls by similar_sym 870 ==> period ls d by cycle_period_similar 871 With 0 < d < k, a contradiction by cycle_order_minimal, ls <> [] 872*) 873Theorem associate_order_map_inj_imp: 874 !m n ls. ls <> [] /\ m < order ls /\ n < order ls /\ 875 m <= n /\ cycle m ls = cycle n ls ==> m = n 876Proof 877 rpt strip_tac >> 878 qabbrev_tac `k = order ls` >> 879 `0 < k` by rw[cycle_order_property, Abbr`k`] >> 880 `n = (n - m) + m` by decide_tac >> 881 qabbrev_tac `d = n - m` >> 882 (Cases_on `d = 0` >> simp[]) >> 883 `0 < d /\ d < k` by decide_tac >> 884 `cycle d (cycle n ls) = cycle d (cycle m ls)` by rw[] >> 885 `_ = cycle n ls` by fs[cycle_add] >> 886 `ls == cycle n ls` by metis_tac[similar_def] >> 887 `period (cycle n ls) d` by rw[period_def] >> 888 `period ls d` by metis_tac[cycle_period_similar, similar_sym] >> 889 metis_tac[cycle_order_minimal] 890QED 891 892(* Idea: for k = order ls, 893 (\n. cycle n ls) (count k) (associate ls) is injective. *) 894 895(* Theorem: ls <> [] ==> INJ (\n. cycle n ls) (count (order ls)) (associate ls) *) 896(* Proof: 897 By associate_def, similar_def, INJ_DEF, this is to show: 898 (1) n < order ls ==> ?n'. cycle n ls = cycle n' ls 899 Take n' = n, hence true. 900 (2) n < order ls /\ n' < order ls /\ cycle n ls = cycle n' ls ==> n = n' 901 If n <= n', n = n' by associate_order_map_inj_imp, ls <> [] 902 If n' <= n, n' = n by associate_order_map_inj_imp, ls <> [] 903 Thus n = n'. 904*) 905Theorem associate_order_map_inj: 906 !ls. ls <> [] ==> INJ (\n. cycle n ls) (count (order ls)) (associate ls) 907Proof 908 rw[associate_def, similar_def, INJ_DEF] >- 909 metis_tac[] >> 910 `n <= n' \/ n' <= n` by decide_tac >- 911 metis_tac[associate_order_map_inj_imp] >> 912 metis_tac[associate_order_map_inj_imp] 913QED 914 915(* Idea: for k = order ls, (\n. cycle n ls) (count k) (associate ls) is bijective. *) 916 917(* Theorem: ls <> [] ==> BIJ (\n. cycle n ls) (count (order ls)) (associate ls) *) 918(* Proof: by BIJ_DEF, associate_order_map_inj, associate_order_map_surj. *) 919Theorem associate_order_map_bij: 920 !ls. ls <> [] ==> 921 BIJ (\n. cycle n ls) (count (order ls)) (associate ls) 922Proof 923 simp[BIJ_DEF, associate_order_map_inj, associate_order_map_surj] 924QED 925 926(* Theorem: CARD (associate ls) = order ls *) 927(* Proof: 928 Let k = order ls, f = (\n. cycle n ls). 929 Note FINITE (count k) by FINITE_COUNT 930 and FINITE (associate ls) by associate_finite 931 and BIJ f (count k) (associate ls) by associate_order_map_bij 932 CARD (associate ls) 933 = CARD (count k) by FINITE_BIJ_CARD_EQ 934 = k by CARD_COUNT 935*) 936Theorem associate_card_eq_order: 937 !ls. ls <> [] ==> CARD (associate ls) = order ls 938Proof 939 rpt strip_tac >> 940 qabbrev_tac `k = order ls` >> 941 `FINITE (count k)` by rw[] >> 942 `FINITE (associate ls)` by rw[associate_finite] >> 943 `BIJ (\n. cycle n ls) (count k) (associate ls)` by rw[associate_order_map_bij, Abbr`k`] >> 944 metis_tac[FINITE_BIJ_CARD_EQ, CARD_COUNT] 945QED 946 947(* Idea: CARD (associate ls) divides LENGTH ls. *) 948 949(* Theorem: ls <> [] ==> (LENGTH ls) MOD (CARD (associate ls)) = 0 *) 950(* Proof: 951 Let k = order ls. 952 Note (LENGTH ls) MOD k = 0 by cycle_order_divides_length 953 and CARD (associate ls) = k by associate_card_eq_order 954 Thus CARD (associate ls) divides LENGTH ls by above 955*) 956Theorem associate_card_divides_length: 957 !ls. ls <> [] ==> (LENGTH ls) MOD (CARD (associate ls)) = 0 958Proof 959 simp[cycle_order_divides_length, associate_card_eq_order] 960QED 961 962(* ------------------------------------------------------------------------- *) 963(* Cycle 1 and Order 1. *) 964(* ------------------------------------------------------------------------- *) 965 966(* Idea: a list with cycle 1 ls = ls iff order 1. *) 967 968(* Theorem: ls <> [] ==> (cycle 1 ls = ls <=> order ls = 1) *) 969(* Proof: 970 If part: cycle 1 ls = ls ==> order ls = 1 971 This is true by cycle_order_eqn 972 Only-if part: order ls = 1 ==> cycle 1 ls = ls 973 This is true by cycle_order_property 974*) 975Theorem cycle_1_eq_order_1: 976 !ls. ls <> [] ==> (cycle 1 ls = ls <=> order ls = 1) 977Proof 978 rw[EQ_IMP_THM] >| [ 979 `0 < 1 /\ (!j. 0 < j /\ j < 1) ==> (cycle j ls <> ls)` by rw[] >> 980 fs[cycle_order_eqn], 981 metis_tac[cycle_order_property] 982 ] 983QED 984 985(* ------------------------------------------------------------------------- *) 986(* Finally, primes enter into the picture. *) 987(* ------------------------------------------------------------------------- *) 988 989(* Idea: if length of a list is prime p, its order is either 1 or p. *) 990 991(* Theorem: prime (LENGTH ls) ==> order ls = 1 \/ order ls = LENGTH ls *) 992(* Proof: 993 Note LENGTH ls <> 0 by NOT_PRIME_0 994 so ls <> [] by LENGTH_NIL 995 Let k = order ls. 996 Then 0 < k by cycle_order_property 997 and (LENGTH ls) MOD k = 0 by cycle_order_divides_length 998 or k divides (LENGTH ls) by DIVIDES_MOD_0 999 ==> k = 1 or k = LENGTH ls by prime_def 1000*) 1001Theorem cycle_order_prime_length: 1002 !ls. prime (LENGTH ls) ==> order ls = 1 \/ order ls = LENGTH ls 1003Proof 1004 rpt strip_tac >> 1005 `ls <> []` by metis_tac[LENGTH_NIL, NOT_PRIME_0] >> 1006 qabbrev_tac `k = order ls` >> 1007 `0 < k` by rw[cycle_order_property, Abbr`k`] >> 1008 `k divides (LENGTH ls)` by fs[cycle_order_divides_length, DIVIDES_MOD_0, Abbr`k`] >> 1009 metis_tac[prime_def] 1010QED 1011 1012(* Idea: if length of a list is prime p, its associate size is 1 or p. *) 1013 1014(* Theorem: prime (LENGTH ls) ==> 1015 CARD (associate ls) = 1 \/ CARD (associate ls) = LENGTH ls *) 1016(* Proof: 1017 Note LENGTH ls <> 0 by NOT_PRIME_0 1018 so ls <> [] by LENGTH_NIL 1019 Thus CARD (associate ls) = order ls by associate_card_eq_order 1020 the result follows by cycle_order_prime_length 1021*) 1022Theorem associate_card_prime_length: 1023 !ls. prime (LENGTH ls) ==> 1024 CARD (associate ls) = 1 \/ CARD (associate ls) = LENGTH ls 1025Proof 1026 rpt strip_tac >> 1027 `ls <> []` by metis_tac[LENGTH_NIL, NOT_PRIME_0] >> 1028 simp[cycle_order_prime_length, associate_card_eq_order] 1029QED 1030 1031 1032(* ------------------------------------------------------------------------- *) 1033 1034(* export theory at end *) 1035val _ = export_theory(); 1036 1037(*===========================================================================*) 1038