1(* ------------------------------------------------------------------------- *) 2(* The Iteration Period *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "iterate"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17val _ = load("helperFunctionTheory"); 18(* open helperTheory; -- skip helper, so no FUNPOW_closure *) 19open helperFunctionTheory; 20open helperSetTheory; 21open helperNumTheory; 22 23(* arithmeticTheory -- load by default *) 24open arithmeticTheory pred_setTheory; 25open dividesTheory; (* for divides_def *) 26 27 28(* ------------------------------------------------------------------------- *) 29(* Iteration Period Documentation *) 30(* ------------------------------------------------------------------------- *) 31(* 32 33 Helper Theorems: 34 35 FUNPOW Theorems: 36 LINV_permutes |- !f s. f PERMUTES s ==> LINV f s PERMUTES s 37 FUNPOW_permutes |- !f s n. f PERMUTES s ==> FUNPOW f n PERMUTES s 38 FUNPOW_LINV_permutes|- !f s n. f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s 39 FUNPOW_LINV_closure |- !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n x IN s 40 FUNPOW_LINV_EQ |- !f s x n. f PERMUTES s /\ x IN s ==> 41 FUNPOW f n (FUNPOW (LINV f s) n x) = x 42 FUNPOW_EQ_LINV |- !f s x n. f PERMUTES s /\ x IN s ==> 43 FUNPOW (LINV f s) n (FUNPOW f n x) = x 44 FUNPOW_SUB_LINV1 |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 45 FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x) 46 FUNPOW_SUB_LINV2 |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 47 FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x) 48 FUNPOW_LINV_SUB1 |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 49 FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x) 50 FUNPOW_LINV_SUB2 |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 51 FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x) 52 FUNPOW_LINV_INV |- !f s x y n. f PERMUTES s /\ x IN s /\ y IN s ==> 53 (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x) 54 55 Iteration Period: 56 iterate_period_def |- !f x. iterate_period f x = 57 case OLEAST k. 0 < k /\ FUNPOW f k x = x of 58 NONE => 0 59 | SOME k => k 60 iterate_period_property 61 |- !f x. FUNPOW f (iterate_period f x) x = x 62 iterate_period_minimal 63 |- !f x n. 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x 64 iterate_period_thm |- !f x n. 0 < n ==> 65 (iterate_period f x = n <=> 66 FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) 67 iterate_fix_0 |- !f x n. n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0 68 iterate_not_distinct|- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 69 ?h k. FUNPOW f h x = FUNPOW f k x /\ h <> k 70 iterate_period_exists 71 |- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 72 ?n. 0 < n /\ n = iterate_period f x 73 iterate_mod_period |- !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==> 74 FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x 75 iterate_reduce |- !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==> 76 ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x 77 iterate_period_eq_0 |- !f x. iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x 78 iterate_period_eq_1 |- !f x. iterate_period f x = 1 <=> f x = x 79 iterate_period_eq_2 |- !f x. iterate_period f x = 2 <=> f x <> x /\ f (f x) = x 80 iterate_period_multiple 81 |- !f x n. FUNPOW f n x = x <=> ?k. n = k * iterate_period f x 82 iterate_period_mod |- !f x n p. 0 < p /\ p = iterate_period f x ==> 83 (FUNPOW f n x = x <=> n MOD p = 0) 84 iterate_period_mod_eq 85 |- !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\ 86 p = iterate_period f x ==> 87 (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) 88 iterate_period_funpow_inj 89 |- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ 90 p = iterate_period f x ==> 91 INJ (\j. FUNPOW f j x) (count p) s 92 iterate_period_upper|- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ 93 p = iterate_period f x ==> p <= CARD s 94 iterate_period_inv |- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 95 iterate_period (LINV f s) x = iterate_period f x 96 iterate_period_inv_alt 97 |- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ 98 p = iterate_period f x ==> 99 iterate_period (LINV f s) x = p 100 iterate_period_iterate 101 |- !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\ 102 y = FUNPOW f j x ==> 103 iterate_period f y = iterate_period f x 104*) 105 106(* ------------------------------------------------------------------------- *) 107(* Helper Theorems *) 108(* ------------------------------------------------------------------------- *) 109 110(* ------------------------------------------------------------------------- *) 111(* FUNPOW Theorems *) 112(* ------------------------------------------------------------------------- *) 113 114(* Theorem: f PERMUTES s ==> (LINV f s) PERMUTES s *) 115(* Proof: by BIJ_LINV_BIJ *) 116Theorem LINV_permutes: 117 !f s. f PERMUTES s ==> (LINV f s) PERMUTES s 118Proof 119 rw[BIJ_LINV_BIJ] 120QED 121 122(* Theorem: f PERMUTES s ==> (FUNPOW f n) PERMUTES s *) 123(* Proof: 124 By induction on n. 125 Base: FUNPOW f 0 PERMUTES s 126 Note FUNPOW f 0 = I by FUN_EQ_THM, FUNPOW_0 127 and I PERMUTES s by BIJ_I_SAME 128 thus true. 129 Step: f PERMUTES s /\ FUNPOW f n PERMUTES s ==> 130 FUNPOW f (SUC n) PERMUTES s 131 Note FUNPOW f (SUC n) 132 = f o (FUNPOW f n) by FUN_EQ_THM, FUNPOW_SUC 133 Thus true by BIJ_COMPOSE 134*) 135Theorem FUNPOW_permutes: 136 !f s n. f PERMUTES s ==> (FUNPOW f n) PERMUTES s 137Proof 138 rpt strip_tac >> 139 Induct_on `n` >| [ 140 `FUNPOW f 0 = I` by rw[FUN_EQ_THM] >> 141 simp[BIJ_I_SAME], 142 `FUNPOW f (SUC n) = f o (FUNPOW f n)` by rw[FUN_EQ_THM, FUNPOW_SUC] >> 143 metis_tac[BIJ_COMPOSE] 144 ] 145QED 146 147(* Theorem: f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s *) 148(* Proof: by LINV_permutes, FUNPOW_permutes *) 149Theorem FUNPOW_LINV_permutes: 150 !f s n. f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s 151Proof 152 simp[LINV_permutes, FUNPOW_permutes] 153QED 154 155(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW f n x IN s *) 156(* Proof: 157 By induction on n. 158 Base: FUNPOW (LINV f s) 0 x IN s 159 Since FUNPOW (LINV f s) 0 x = x by FUNPOW_0 160 This is trivially true. 161 Step: FUNPOW (LINV f s) n x IN s ==> FUNPOW (LINV f s) (SUC n) x IN s 162 FUNPOW (LINV f s) (SUC n) x 163 = (LINV f s) (FUNPOW (LINV f s) n x) by FUNPOW_SUC 164 But FUNPOW (LINV f s) n x IN s by induction hypothesis 165 and (LINV f s) PERMUTES s by LINV_permutes 166 so (LINV f s) (FUNPOW (LINV f s) n x) IN s 167 by BIJ_ELEMENT 168*) 169Theorem FUNPOW_LINV_closure: 170 !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n x IN s 171Proof 172 rpt strip_tac >> 173 Induct_on `n` >- 174 rw[] >> 175 `(LINV f s) PERMUTES s` by rw[LINV_permutes] >> 176 prove_tac[FUNPOW_SUC, BIJ_ELEMENT] 177QED 178 179(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW f n (FUNPOW (LINV f s) n x) = x *) 180(* Proof: 181 By induction on n. 182 Base: FUNPOW f 0 (FUNPOW (LINV f s) 0 x) = x 183 FUNPOW f 0 (FUNPOW (LINV f s) 0 x) 184 = FUNPOW f 0 x by FUNPOW_0 185 = x by FUNPOW_0 186 Step: FUNPOW f n (FUNPOW (LINV f s) n x) = x ==> 187 FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x) = x 188 Note (FUNPOW (LINV f s) n x) IN s by FUNPOW_LINV_closure 189 FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x) 190 = FUNPOW f (SUC n) ((LINV f s) (FUNPOW (LINV f s) n x)) by FUNPOW_SUC 191 = FUNPOW f n (f ((LINV f s) (FUNPOW (LINV f s) n x))) by FUNPOW 192 = FUNPOW f n (FUNPOW (LINV f s) n x) by BIJ_LINV_THM 193 = x by induction hypothesis 194*) 195Theorem FUNPOW_LINV_EQ: 196 !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW f n (FUNPOW (LINV f s) n x) = x 197Proof 198 rpt strip_tac >> 199 Induct_on `n` >- 200 rw[] >> 201 `FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x) 202 = FUNPOW f (SUC n) ((LINV f s) (FUNPOW (LINV f s) n x))` by rw[FUNPOW_SUC] >> 203 `_ = FUNPOW f n (f ((LINV f s) (FUNPOW (LINV f s) n x)))` by rw[FUNPOW] >> 204 `_ = FUNPOW f n (FUNPOW (LINV f s) n x)` by metis_tac[BIJ_LINV_THM, FUNPOW_LINV_closure] >> 205 simp[] 206QED 207 208(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n (FUNPOW f n x) = x *) 209(* Proof: 210 By induction on n. 211 Base: FUNPOW (LINV f s) 0 (FUNPOW f 0 x) = x 212 FUNPOW (LINV f s) 0 (FUNPOW f 0 x) 213 = FUNPOW (LINV f s) 0 x by FUNPOW_0 214 = x by FUNPOW_0 215 Step: FUNPOW (LINV f s) n (FUNPOW f n x) = x ==> 216 FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x) = x 217 Note (FUNPOW f n x) IN s by FUNPOW_closure 218 FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x) 219 = FUNPOW (LINV f s) (SUC n) (f (FUNPOW f n x)) by FUNPOW_SUC 220 = FUNPOW (LINV f s) n ((LINV f s) (f (FUNPOW f n x))) by FUNPOW 221 = FUNPOW (LINV f s) n (FUNPOW f n x) by BIJ_LINV_THM 222 = x by induction hypothesis 223*) 224Theorem FUNPOW_EQ_LINV: 225 !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n (FUNPOW f n x) = x 226Proof 227 rpt strip_tac >> 228 Induct_on `n` >- 229 rw[] >> 230 `FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x) 231 = FUNPOW (LINV f s) (SUC n) (f (FUNPOW f n x))` by rw[FUNPOW_SUC] >> 232 `_ = FUNPOW (LINV f s) n ((LINV f s) (f (FUNPOW f n x)))` by rw[FUNPOW] >> 233 `_ = FUNPOW (LINV f s) n (FUNPOW f n x)` by metis_tac[BIJ_LINV_THM, FUNPOW_closure] >> 234 simp[] 235QED 236 237(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==> 238 FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x) *) 239(* Proof: 240 FUNPOW f n (FUNPOW (LINV f s) m x) 241 = FUNPOW f (n - m + m) (FUNPOW (LINV f s) m x) by SUB_ADD, m <= n 242 = FUNPOW f (n - m) (FUNPOW f m (FUNPOW (LINV f s) m x)) by FUNPOW_ADD 243 = FUNPOW f (n - m) x by FUNPOW_LINV_EQ 244*) 245Theorem FUNPOW_SUB_LINV1: 246 !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 247 FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x) 248Proof 249 rpt strip_tac >> 250 `FUNPOW f n (FUNPOW (LINV f s) m x) 251 = FUNPOW f (n - m + m) (FUNPOW (LINV f s) m x)` by simp[] >> 252 `_ = FUNPOW f (n - m) (FUNPOW f m (FUNPOW (LINV f s) m x))` by rw[FUNPOW_ADD] >> 253 `_ = FUNPOW f (n - m) x` by rw[FUNPOW_LINV_EQ] >> 254 simp[] 255QED 256 257(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==> 258 FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x) *) 259(* Proof: 260 Note FUNPOW f (n - m) x IN s by FUNPOW_closure 261 FUNPOW (LINV f s) m (FUNPOW f n x) 262 = FUNPOW (LINV f s) m (FUNPOW f (n - m + m) x) by SUB_ADD, m <= n 263 = FUNPOW (LINV f s) m (FUNPOW f (m + (n - m)) x) by ADD_COMM 264 = FUNPOW (LINV f s) m (FUNPOW f m (FUNPOW f (n - m) x)) by FUNPOW_ADD 265 = FUNPOW f (n - m) x by FUNPOW_EQ_LINV 266*) 267Theorem FUNPOW_SUB_LINV2: 268 !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 269 FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x) 270Proof 271 rpt strip_tac >> 272 `FUNPOW (LINV f s) m (FUNPOW f n x) 273 = FUNPOW (LINV f s) m (FUNPOW f (n - m + m) x)` by simp[] >> 274 `_ = FUNPOW (LINV f s) m (FUNPOW f (m + (n - m)) x)` by metis_tac[ADD_COMM] >> 275 `_ = FUNPOW (LINV f s) m (FUNPOW f m (FUNPOW f (n - m) x))` by rw[FUNPOW_ADD] >> 276 `_ = FUNPOW f (n - m) x` by rw[FUNPOW_EQ_LINV, FUNPOW_closure] >> 277 simp[] 278QED 279 280(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==> 281 FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x) *) 282(* Proof: 283 FUNPOW (LINV f s) n (FUNPOW f m x) 284 = FUNPOW (LINV f s) (n - m + m) (FUNPOW f m x) by SUB_ADD, m <= n 285 = FUNPOW (LINV f s) (n - m) (FUNPOW (LINV f s) m (FUNPOW f m x)) by FUNPOW_ADD 286 = FUNPOW (LINV f s) (n - m) x by FUNPOW_EQ_LINV 287*) 288Theorem FUNPOW_LINV_SUB1: 289 !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 290 FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x) 291Proof 292 rpt strip_tac >> 293 `FUNPOW (LINV f s) n (FUNPOW f m x) 294 = FUNPOW (LINV f s) (n - m + m) (FUNPOW f m x)` by simp[] >> 295 `_ = FUNPOW (LINV f s) (n - m) (FUNPOW (LINV f s) m (FUNPOW f m x))` by rw[FUNPOW_ADD] >> 296 `_ = FUNPOW (LINV f s) (n - m) x` by rw[FUNPOW_EQ_LINV] >> 297 simp[] 298QED 299 300(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==> 301 FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x) *) 302(* Proof: 303 Note FUNPOW (LINV f s) (n - m) x IN s by FUNPOW_LINV_closure 304 FUNPOW f m (FUNPOW (LINV f s) n x) 305 = FUNPOW f m (FUNPOW (LINV f s) (n - m + m) x) by SUB_ADD, m <= n 306 = FUNPOW f m (FUNPOW (LINV f s) (m + (n - m)) x) by ADD_COMM 307 = FUNPOW f m (FUNPOW (LINV f s) m (FUNPOW (LINV f s) (n - m) x)) by FUNPOW_ADD 308 = FUNPOW (LINV f s) (n - m) x by FUNPOW_LINV_EQ 309*) 310Theorem FUNPOW_LINV_SUB2: 311 !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==> 312 FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x) 313Proof 314 rpt strip_tac >> 315 `FUNPOW f m (FUNPOW (LINV f s) n x) 316 = FUNPOW f m (FUNPOW (LINV f s) (n - m + m) x)` by simp[] >> 317 `_ = FUNPOW f m (FUNPOW (LINV f s) (m + (n - m)) x)` by metis_tac[ADD_COMM] >> 318 `_ = FUNPOW f m (FUNPOW (LINV f s) m (FUNPOW (LINV f s) (n - m) x))` by rw[FUNPOW_ADD] >> 319 `_ = FUNPOW (LINV f s) (n - m) x` by rw[FUNPOW_LINV_EQ, FUNPOW_LINV_closure] >> 320 simp[] 321QED 322 323(* Theorem: f PERMUTES s /\ x IN s /\ y IN s ==> 324 (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x) *) 325(* Proof: 326 If part: x = FUNPOW f n y ==> y = FUNPOW (LINV f s) n x) 327 FUNPOW (LINV f s) n x) 328 = FUNPOW (LINV f s) n (FUNPOW f n y)) by x = FUNPOW f n y 329 = y by FUNPOW_EQ_LINV 330 Only-if part: y = FUNPOW (LINV f s) n x) ==> x = FUNPOW f n y 331 FUNPOW f n y 332 = FUNPOW f n (FUNPOW (LINV f s) n x)) by y = FUNPOW (LINV f s) n x) 333 = x by FUNPOW_LINV_EQ 334*) 335Theorem FUNPOW_LINV_INV: 336 !f s x y n. f PERMUTES s /\ x IN s /\ y IN s ==> 337 (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x) 338Proof 339 rw[EQ_IMP_THM] >- 340 rw[FUNPOW_EQ_LINV] >> 341 rw[FUNPOW_LINV_EQ] 342QED 343 344(* ------------------------------------------------------------------------- *) 345(* Iteration Period *) 346(* ------------------------------------------------------------------------- *) 347 348(* Define period = optional LEAST index for FUNPOW f k x to return to x. *) 349val iterate_period_def = zDefine` 350 iterate_period (f:'a -> 'a) (x:'a) = 351 case OLEAST k. 0 < k /\ FUNPOW f k x = x of 352 NONE => 0 353 | SOME k => k 354`; 355(* use zDefine here since this is not computationally effective. *) 356 357(* Theorem: FUNPOW f (iterate_period f x) x = x *) 358(* Proof: 359 If iterate_period f x k returns SOME k, 360 FUNPOW f (iterate_period f x) x 361 = FUNPOW f k x by iterate_period_def 362 = x by definition condition 363 Otherwise iterate_period f x k returns NONE, 364 FUNPOW f (iterate_period f x) x 365 = FUNPOW f 0 x by iterate_period_def 366 = x by FUNPOW_0 367*) 368Theorem iterate_period_property: 369 !f x. FUNPOW f (iterate_period f x) x = x 370Proof 371 rpt strip_tac >> 372 simp[iterate_period_def] >> 373 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 374 simp[] 375QED 376 377(* Theorem: 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x *) 378(* Proof: by iterate_period_def, and definition of OLEAST. *) 379Theorem iterate_period_minimal: 380 !f x n. 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x 381Proof 382 ntac 2 strip_tac >> 383 simp[iterate_period_def] >> 384 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 385 rw_tac std_ss[] >> 386 metis_tac[] 387QED 388 389(* Theorem: 0 < n ==> (iterate_period f x = n <=> 390 FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) *) 391(* Proof: 392 If part: iterate_period f x = n ==> 393 FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) 394 This is to show: 395 (1) FUNPOW f n x = x, true by iterate_period_property 396 (2) !m. 0 < m /\ m < n ==> FUNPOW f m x <> x, true by iterate_period_minimal 397 Only-if part: FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) ==> 398 iterate_period f x = n 399 Expanding by iterate_period_def, this is to show: 400 (1) 0 < n /\ !n'. ~(0 < n') \/ FUNPOW f n' x <> x ==> 0 = n 401 Putting n' = n, the assumption is contradictory. 402 (2) 0 < n /\ 0 < n' /\ !m. m < n' ==> ~(0 < m) \/ FUNPOW f m x <> x ==> n' = n 403 The assumptions implies ~(n' < n), and ~(n < n'), hence n' = n. 404*) 405Theorem iterate_period_thm: 406 !f x n. 0 < n ==> 407 (iterate_period f x = n <=> 408 FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) 409Proof 410 rw[EQ_IMP_THM] >- 411 simp[iterate_period_property] >- 412 simp[iterate_period_minimal] >> 413 simp[iterate_period_def] >> 414 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 415 rw_tac std_ss[] >- 416 metis_tac[] >> 417 `~(n' < n) /\ ~(n < n')` by metis_tac[] >> 418 decide_tac 419QED 420 421(* Theorem: n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0 *) 422(* Proof: by iterate_period_minimal, ~(0 < n), so n = 0. *) 423Theorem iterate_fix_0: 424 !f x n. n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0 425Proof 426 metis_tac[iterate_period_minimal, NOT_ZERO] 427QED 428 429(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 430 ?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k) *) 431(* Proof: 432 By contradiction, suppose !h k. FUNPOW f h x = FUNPOW f k x ==> (h = k). 433 Since s is FINITE, let c = CARD s. 434 Let fun = (\n. FUNPOW f n x), t = count (SUC c). 435 Then INJ fun t s since: 436 (1) !n. fun n x IN s by INJ_DEF, FUNPOW_closure, x IN s 437 (2) !h k. fun h x = fun k x ==> h = k by assumption 438 But c < SUC c 439 and SUC c = CARD (count (SUC c)) = CARD t by CARD_COUNT 440 This contradicts the Pigeonhole Principle by PHP 441*) 442Theorem iterate_not_distinct: 443 !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 444 ?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k) 445Proof 446 spose_not_then strip_assume_tac >> 447 qabbrev_tac `c = CARD s` >> 448 `INJ (\n. FUNPOW f n x) (count (SUC c)) s` by rw[INJ_DEF, FUNPOW_closure] >> 449 `c < SUC c` by decide_tac >> 450 metis_tac[CARD_COUNT, PHP] 451QED 452 453(* Unfortunately, this is too weak in this case. 454Say the actual period is 3, so FUNPOW f 3 x = x. 455That means h k can be 1, 4, or 1, 7, or 4, 61. 456There is no guarantee that their difference is the period. 457This is because the group is (Z, +), which is INFINITE. 458Next one is stronger. 459*) 460 461(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 462 ?n. 0 < n /\ n = iterate_period f x *) 463(* Proof: 464 Note FINITE s /\ f PERMUTES s /\ x IN s 465 ==> ?h k. FUNPOW f h x = FUNPOW f k x /\ 466 (h < k) by use of iterate_not_distinct 467 Let n = (k - h), then 0 < n by h < k 468 FUNPOW f n x 469 = FUNPOW f (k - h) x by n = k - h, above 470 = FUNPOW (LINV f s) h (FUNPOW f k x) by FUNPOW_SUB_LINV2, h <= k, x IN s 471 = FUNPOW (LINV f s) h (FUNPOW f h x) by FUNPOW f h x = FUNPOW f k x 472 = x by FUNPOW_EQ_LINV 473 474 Let t = {n | 0 < n /\ FUNPOW f n x = x}, m = MIN_SET t. 475 Thus n IN t, so t <> EMPTY by MEMBER_NOT_EMPTY 476 and m IN t by MIN_SET_IN_SET, t <> EMPTY 477 ==> 0 < m /\ (FUNPOW f m x = x) by m IN t 478 479 Claim: !j. 0 < j /\ j < m ==> (FUNPOW f j x <> x) 480 Proof: By contradiction, 481 suppose ?j. 0 < j /\ j < m /\ (FUNPOW f j x = x). 482 Then j IN t, and m <= j by MIN_SET_PROPERTY, t <> EMPTY 483 This contradicts j < m. 484 485 Thus m = iterate_period f x, and 0 < m. 486*) 487Theorem iterate_period_exists: 488 !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 489 ?n. 0 < n /\ n = iterate_period f x 490Proof 491 rpt strip_tac >> 492 `?h k. FUNPOW f h x = FUNPOW f k x /\ (h < k)` by 493 (`?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k)` by metis_tac[iterate_not_distinct] >> 494 Cases_on `h < k` >- 495 metis_tac[] >> 496 `k < h` by decide_tac >> 497 metis_tac[] 498 ) >> 499 `0 < k - h` by decide_tac >> 500 qabbrev_tac `n = k - h` >> 501 `FUNPOW f n x = FUNPOW f (k - h) x` by rw[Abbr`n`] >> 502 `_ = FUNPOW (LINV f s) h (FUNPOW f k x)` by rw[FUNPOW_SUB_LINV2] >> 503 `_ = FUNPOW (LINV f s) h (FUNPOW f h x)` by fs[] >> 504 `_ = x` by rw[FUNPOW_EQ_LINV] >> 505 qabbrev_tac `t = {n | 0 < n /\ FUNPOW f n x = x}` >> 506 qabbrev_tac `m = MIN_SET t` >> 507 `n IN t` by rw[Abbr`t`] >> 508 `m IN t` by metis_tac[MIN_SET_IN_SET, MEMBER_NOT_EMPTY] >> 509 `0 < m /\ (FUNPOW f m x = x)` by fs[Abbr`t`] >> 510 `!j. 0 < j /\ j < m ==> (FUNPOW f j x <> x)` by 511 (spose_not_then strip_assume_tac >> 512 `j IN t` by rw[Abbr`t`] >> 513 `m <= j` by metis_tac[MIN_SET_PROPERTY, MEMBER_NOT_EMPTY] >> 514 decide_tac) >> 515 metis_tac[iterate_period_thm] 516QED 517 518(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 0 < iterate_period f x *) 519(* Proof: by iterate_period_exists *) 520Theorem iterate_period_pos: 521 !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 0 < iterate_period f x 522Proof 523 metis_tac[iterate_period_exists] 524QED 525 526(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 527 FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x *) 528(* Proof: 529 Let p = iterate_period f x. 530 Then 0 < p by iterate_period_pos 531 and FUNPOW f p x = x by iterate_period_property 532 FUNPOW f n x 533 = FUNPOW f (n MOD p) x by FUNPOW_MOD, FUNPOW f p x = x 534*) 535Theorem iterate_mod_period: 536 !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==> 537 FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x 538Proof 539 rpt strip_tac >> 540 qabbrev_tac `p = iterate_period f x` >> 541 `0 < p` by metis_tac[iterate_period_pos] >> 542 `FUNPOW f p x = x` by rw[iterate_period_property, Abbr`p`] >> 543 simp[FUNPOW_MOD] 544QED 545 546(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 547 ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x *) 548(* Proof: 549 Let p = iterate_period f x. 550 Then 0 < p by iterate_period_pos 551 Let m = n MOD p, then m < p by MOD_LESS 552 and FUNPOW f n x = FUNPOW f m x by iterate_mod_period 553*) 554Theorem iterate_reduce: 555 !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==> 556 ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x 557Proof 558 metis_tac[iterate_period_pos, iterate_mod_period, MOD_LESS] 559QED 560 561(* Theorem: iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x *) 562(* Proof: by iterate_period_def *) 563Theorem iterate_period_eq_0: 564 !f x. iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x 565Proof 566 rw[iterate_period_def] >> 567 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 568 simp[] >> 569 metis_tac[NOT_ZERO] 570QED 571 572(* Theorem: iterate_period f x = 1 <=> f x = x *) 573(* Proof: 574 Since 0 < 1, 575 iterate_period f x = 1 576 <=> (FUNPOW f 1 x = x) /\ by iterate_period_thm 577 !m. 0 < m /\ m < 1 ==> FUNPOW f m x <> x) 578 <=> f x = x /\ T by FUNPOW_1 579 <=> f x = x by simplification 580*) 581Theorem iterate_period_eq_1: 582 !f x. iterate_period f x = 1 <=> f x = x 583Proof 584 rw[iterate_period_thm] 585QED 586 587(* Theorem: iterate_period f x = 2 <=> (f x <> x /\ f (f x) = x) *) 588(* Proof: 589 Since 0 < 2, 590 iterate_period f x = 2 591 <=> (FUNPOW f 2 x = x) /\ by iterate_period_thm 592 !m. 0 < m /\ m < 2 ==> FUNPOW f m x <> x) 593 <=> f (f x) = x /\ f x <> x by FUNPOW_1, FUNPOW_2 594*) 595Theorem iterate_period_eq_2: 596 !f x. iterate_period f x = 2 <=> (f x <> x /\ f (f x) = x) 597Proof 598 rw[iterate_period_thm, FUNPOW_2, EQ_IMP_THM] >- 599 metis_tac[FUNPOW_1, DECIDE``0 < 1 /\ 1 < 2``] >> 600 `m = 1` by decide_tac >> 601 simp[] 602QED 603 604(* Theorem: FUNPOW f n x = x <=> ?k. n = k * (iterate_period f x) *) 605(* Proof: 606 Let p = iterate_period f x. 607 When p = 0, 608 If part: FUNPOW f n x = x ==> ?k. n = k * 0, that is: n = 0. 609 By contradiction, suppose n <> 0. 610 Then 0 < n, giving FUNPOW f n x <> x by iterate_period_eq_0 611 This contradicts FUNPOW f n x = x. 612 Only-if part: n = 0 ==> FUNPOW f n x = x 613 That is FUNPOW f 0 x = x, true by FUNPOW_0 614 When p <> 0, then 0 < p. 615 Note FUNPOW f p x = x by iterate_period_property 616 If part: FUNPOW f n x = x ==> ?k. n = k * p 617 Let k = n DIV p, r = n MOD p. 618 Then (n = k * p + r) /\ (r < p) by DIVISION, 0 < p 619 so n = FUNPOW f n x by given 620 = FUNPOW f (r + k * p) x by above 621 = FUNPOW f r (FUNPOW f (k * p) x) by FUNPOW_ADD 622 = FUNPOW f r x by FUNPOW_MULTIPLE 623 Thus r = 0 by iterate_period_minimal 624 so take k = n DIV p. 625 Only-if part: n = k * p ==> FUNPOW f n x = x 626 This is true by FUNPOW_MULTIPLE 627*) 628Theorem iterate_period_multiple: 629 !f x n. FUNPOW f n x = x <=> ?k. n = k * (iterate_period f x) 630Proof 631 rpt strip_tac >> 632 qabbrev_tac `p = iterate_period f x` >> 633 Cases_on `p = 0` >| [ 634 rw[EQ_IMP_THM] >> 635 metis_tac[iterate_period_eq_0, NOT_ZERO], 636 `0 < p` by decide_tac >> 637 `FUNPOW f p x = x` by rw[iterate_period_property, Abbr`p`] >> 638 REVERSE (rw[EQ_IMP_THM]) >- 639 rw[FUNPOW_MULTIPLE] >> 640 qabbrev_tac `k = n DIV p` >> 641 qabbrev_tac `r = n MOD p` >> 642 `(n = k * p + r) /\ (r < p)` by rw[DIVISION, Abbr`k`, Abbr`r`] >> 643 `FUNPOW f n x = FUNPOW f (r + k * p) x` by fs[] >> 644 `_ = FUNPOW f r (FUNPOW f (k * p) x)` by rw[FUNPOW_ADD] >> 645 `_ = FUNPOW f r x` by rw[FUNPOW_MULTIPLE] >> 646 `~(0 < r)` by metis_tac[iterate_period_minimal] >> 647 `r = 0` by decide_tac >> 648 metis_tac[ADD_0] 649 ] 650QED 651 652(* Theorem: 0 < p /\ p = iterate_period f x ==> 653 (FUNPOW f n x = x <=> n MOD p = 0) *) 654(* Proof: 655 FUNPOW f n x = x 656 <=> ?k. n = k * p by iterate_period_multiple 657 <=> n MOD p = 0 by MOD_EQ_0_DIVISOR, 0 < p 658*) 659Theorem iterate_period_mod: 660 !f x n p. 0 < p /\ p = iterate_period f x ==> 661 (FUNPOW f n x = x <=> n MOD p = 0) 662Proof 663 simp[iterate_period_multiple, MOD_EQ_0_DIVISOR] 664QED 665 666(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==> 667 (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) *) 668(* Proof: 669 Note 0 < p by iterate_period_pos 670 and FUNPOW f i x IN s by FUNPOW_closure 671 and FUNPOW f j x IN s by FUNPOW_closure 672 If i = j, the equivalence is trivial. Otherwise, 673 674 FUNPOW f i x = FUNPOW f j x 675 <=> x = FUNPOW (LINV f s) i (FUNPOW f j x) 676 or FUNPOW (LINV f s) j (FUNPOW f i x) = x by FUNPOW_LINV_INV 677 <=> x = FUNPOW f (j - i) x if i <= j 678 or x = FUNPOW f (i - j) x if j <= i by FUNPOW_SUB_LINV2 679 <=> (j - i) MOD p = 0 or (i - j) MOD p = 0 by iterate_period_mod 680 <=> i MOD p = j MOD p by MOD_EQ, 0 < p 681*) 682Theorem iterate_period_mod_eq: 683 !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\ 684 p = iterate_period f x ==> 685 (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) 686Proof 687 rpt strip_tac >> 688 `0 < p` by metis_tac[iterate_period_pos] >> 689 `(i = j) \/ (i < j) \/ (j < i)` by decide_tac >- 690 fs[] >- 691 (`i <= j` by decide_tac >> 692 `FUNPOW f j x IN s` by rw[FUNPOW_closure] >> 693 `FUNPOW f i x = FUNPOW f j x <=> (x = FUNPOW (LINV f s) i (FUNPOW f j x))` by metis_tac[FUNPOW_LINV_INV] >> 694 `_ = (x = FUNPOW f (j - i) x)` by fs[GSYM FUNPOW_SUB_LINV2] >> 695 `_ = ((j - i) MOD p = 0)` by metis_tac[iterate_period_mod] >> 696 fs[MOD_EQ]) >> 697 `j <= i` by decide_tac >> 698 `FUNPOW f i x IN s` by rw[FUNPOW_closure] >> 699 `FUNPOW f i x = FUNPOW f j x <=> (x = FUNPOW (LINV f s) j (FUNPOW f i x))` by metis_tac[FUNPOW_LINV_INV] >> 700 `_ = (x = FUNPOW f (i - j) x)` by fs[GSYM FUNPOW_SUB_LINV2] >> 701 `_ = ((i - j) MOD p = 0)` by metis_tac[iterate_period_mod] >> 702 fs[MOD_EQ] 703QED 704 705(* Another proof of the same theorem. *) 706(* This is 'elementary' in the sense that LINV is not used, but same concept. *) 707 708(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==> 709 (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) *) 710(* Proof: 711 Let h = i MOD p, k = j MOD p. 712 Note 0 < p by iterate_period_pos 713 and FUNPOW f i x = FUNPOW f h x by iterate_mod_period 714 and FUNPOW f j x = FUNPOW f k x by iterate_mod_period 715 and h < p, k < p by MOD_LESS, 0 < p 716 Thus the goal is: FUNPOW f h x = FUNPOW f k x <=> h = k. 717 The only-if part is trivial, so just do the if part. 718 719 Let d = p - h, the difference by h < p 720 Then p = h + d = d + h by arithmetic 721 x = FUNPOW f p x by iterate_period_property 722 = FUNPOW f d (FUNPOW f h x) by FUNPOW_ADD 723 = FUNPOW f d (FUNPOW f k x) by given 724 = FUNPOW f (d + k) x by FUNPOW_ADD 725 Thus (d + k) MOD p = 0 by iterate_period_mod 726 or p divides (d + k) by DIVIDES_MOD_0, 0 < p 727 But d + k < p + p = 2 * p by arithmetic 728 and 0 < d + k by arithmetic 729 Also p divides p by DIVIDES_REFL 730 ==> d + k = p by MULTIPLE_INTERVAL 731 so k = p - d = h by arithmetic 732*) 733Theorem iterate_period_mod_eq: 734 !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\ 735 p = iterate_period f x ==> 736 (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) 737Proof 738 rpt strip_tac >> 739 `0 < p` by metis_tac[iterate_period_pos] >> 740 qabbrev_tac `h = i MOD p` >> 741 qabbrev_tac `k = j MOD p` >> 742 `FUNPOW f h x = FUNPOW f k x <=> (h = k)` suffices_by metis_tac[iterate_mod_period] >> 743 simp[EQ_IMP_THM] >> 744 strip_tac >> 745 `h < p /\ k < p` by rw[Abbr`h`, Abbr`k`] >> 746 `p = p - h + h` by decide_tac >> 747 qabbrev_tac `d = p - h` >> 748 `x = FUNPOW f p x` by metis_tac[iterate_period_property] >> 749 `_ = FUNPOW f (d + k) x` by rfs[FUNPOW_ADD] >> 750 `p divides (d + k)` by metis_tac[iterate_period_multiple, divides_def] >> 751 `d + k < p + p` by decide_tac >> 752 `p - p < d + k` by decide_tac >> 753 `p divides p` by fs[] >> 754 `d + k = p` by metis_tac[MULTIPLE_INTERVAL] >> 755 decide_tac 756QED 757 758(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==> 759 INJ (\j. FUNPOW f j x) (count p) s *) 760(* Proof: 761 By INJ_DEF, this is to show: 762 (1) j < p ==> FUNPOW f j x IN s, true by FUNPOW_closure 763 (2) j < p /\ j' < p /\ FUNPOW f j x = FUNPOW f j' x ==> j = j' 764 FUNPOW f j x = FUNPOW f j' x 765 ==> j MOD p = j' MOD p by iterate_period_mod_eq 766 ==> j = j' by LESS_MOD, j < p, j' < p 767*) 768Theorem iterate_period_funpow_inj: 769 !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ 770 p = iterate_period f x ==> 771 INJ (\j. FUNPOW f j x) (count p) s 772Proof 773 rw[INJ_DEF] >- 774 fs[FUNPOW_closure] >> 775 metis_tac[iterate_period_mod_eq, LESS_MOD] 776QED 777 778(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ 779 p = iterate_period f x ==> p <= CARD s *) 780(* Proof: 781 Note INJ (\j. FUNPOW f j x) (count p) s by iterate_period_funpow_inj 782 and FINITE (count p) by FINITE_COUNT 783 and CARD (count p) = p by CARD_COUNT 784 ==> p <= CARD s by INJ_CARD 785*) 786Theorem iterate_period_upper: 787 !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ 788 p = iterate_period f x ==> p <= CARD s 789Proof 790 metis_tac[iterate_period_funpow_inj, INJ_CARD, FINITE_COUNT, CARD_COUNT] 791QED 792 793(* Idea: period is unchanged for a permutation. *) 794 795(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 796 iterate_period (LINV f s) x = iterate_period f x *) 797(* Proof: 798 Note LINV f s PERMUTES s by LINV_permutes 799 Let q = iterate_period (LINV f s) x 800 Then 0 < q by iterate_period_pos 801 By iterate_period_thm, this is to show: 802 (1) FUNPOW f q x = x. 803 Let y = FUNPOW f q x 804 Then y IN s by FUNPOW_closure 805 so x = FUNPOW (LINV f s) q y by FUNPOW_LINV_INV 806 = y by iterate_period_property 807 (2) !m. 0 < m /\ m < q ==> FUNPOW f m x <> x 808 Let y = FUNPOW f m x. 809 Then y IN s by FUNPOW_closure 810 so x = FUNPOW (LINV f s) m y by FUNPOW_LINV_INV 811 ==> FUNPOW f m x <> x by iterate_period_minimal 812*) 813Theorem iterate_period_inv: 814 !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 815 iterate_period (LINV f s) x = iterate_period f x 816Proof 817 rpt strip_tac >> 818 `LINV f s PERMUTES s` by rw[LINV_permutes] >> 819 qabbrev_tac `q = iterate_period (LINV f s) x` >> 820 `0 < q` by metis_tac[iterate_period_pos] >> 821 simp[iterate_period_thm] >> 822 rpt strip_tac >| [ 823 qabbrev_tac `y = FUNPOW f q x` >> 824 `y IN s` by rw[FUNPOW_closure, Abbr`y`] >> 825 metis_tac[FUNPOW_LINV_INV, iterate_period_property], 826 qabbrev_tac `y = FUNPOW f m x` >> 827 `y IN s` by rw[FUNPOW_closure, Abbr`y`] >> 828 metis_tac[FUNPOW_LINV_INV, iterate_period_minimal] 829 ] 830QED 831 832(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==> 833 iterate_period (LINV f s) x = p *) 834(* Proof: by iterate_period_inv. *) 835Theorem iterate_period_inv_alt: 836 !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==> 837 iterate_period (LINV f s) x = p 838Proof 839 simp[iterate_period_inv] 840QED 841 842(* Idea: all elements in the orbit have the same period. *) 843 844(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==> 845 iterate_period f y = iterate_period f x *) 846(* Proof: 847 Let p = iterate_period f x, 848 q = iterate_period f y, 849 k = j MOD p. 850 Then y = FUNPOW f k x by iterate_mod_period 851 Note y IN s /\ FUNPOW f q x IN s by FUNPOW_closure 852 and 0 < p /\ 0 < q by iterate_period_pos, y IN s 853 and k < p by MOD_LESS, 0 < p 854 855 Step 1: show FUNPOW f p y = y 856 Note p = k + p - k = p - k + k by k < p 857 FUNPOW f p y 858 = FUNPOW f (k + p - k) y 859 = FUNPOW f k (FUNPOW f (p - k) y) by FUNPOW_ADD 860 = FUNPOW f k (FUNPOW f (p - k) (FUNPOW f k x)) 861 = FUNPOW f k (FUNPOW f p x) by FUNPOW_ADD 862 = FUNPOW f k x by iterate_period_property 863 = y 864 Thus p MOD q = 0 by iterate_period_mod 865 or q divides p by DIVIDES_MOD_0, 0 < q 866 867 Step 2: show FUNPOW f q x = x 868 FUNPOW f k x 869 = y by given 870 = FUNPOW f q y by iterate_period_property 871 = FUNPOW f q (FUNPOW f k x) 872 = FUNPOW f k (FUNPOW f q x) by FUNPOW_COMM 873 Note (FUNPOW f k) PERMUTES s by FUNPOW_permutes 874 ==> FUNPOW f q x = x by BIJ_DEF, INJ_DEF 875 Thus q MOD p = 0 by iterate_period_mod 876 or p divides q by DIVIDES_MOD_0, 0 < q 877 878 Thus p = q by DIVIDES_ANTISYM, [1][2] 879*) 880Theorem iterate_period_iterate: 881 !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==> 882 iterate_period f y = iterate_period f x 883Proof 884 rpt strip_tac >> 885 qabbrev_tac `p = iterate_period f x` >> 886 qabbrev_tac `q = iterate_period f y` >> 887 qabbrev_tac `k = j MOD p` >> 888 `y = FUNPOW f k x` by metis_tac[iterate_mod_period] >> 889 `y IN s` by rw[FUNPOW_closure] >> 890 `0 < p /\ 0 < q` by metis_tac[iterate_period_pos] >> 891 `k < p` by rw[Abbr`k`] >> 892 `p = p - k + k` by decide_tac >> 893 `FUNPOW f p y = FUNPOW f (k + p - k) y` by simp[] >> 894 `_ = FUNPOW f k (FUNPOW f (p - k) y)` by rw[GSYM FUNPOW_ADD] >> 895 `_ = FUNPOW f k (FUNPOW f p x)` by metis_tac[FUNPOW_ADD] >> 896 `_ = y` by fs[iterate_period_property, Abbr`p`] >> 897 `p MOD q = 0` by metis_tac[iterate_period_mod] >> 898 `q divides p` by fs[DIVIDES_MOD_0] >> 899 `FUNPOW f k x = y` by simp[] >> 900 `_ = FUNPOW f q y` by rw[iterate_period_property, Abbr`q`] >> 901 `_ = FUNPOW f q (FUNPOW f k x)` by rfs[] >> 902 `_ = FUNPOW f k (FUNPOW f q x)` by rw[FUNPOW_COMM] >> 903 `(FUNPOW f k) PERMUTES s` by rw[FUNPOW_permutes] >> 904 `FUNPOW f q x IN s` by rw[FUNPOW_closure] >> 905 `FUNPOW f q x = x` by metis_tac[BIJ_DEF, INJ_DEF] >> 906 `q MOD p = 0` by metis_tac[iterate_period_mod] >> 907 `p divides q` by fs[DIVIDES_MOD_0] >> 908 simp[DIVIDES_ANTISYM] 909QED 910 911(* ------------------------------------------------------------------------- *) 912 913(* export theory at end *) 914val _ = export_theory(); 915 916(*===========================================================================*) 917