1(* ------------------------------------------------------------------------- *) 2(* Iteration of Involution Composition *) 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 "iterateCompose"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17(* arithmeticTheory -- load by default *) 18 19(* val _ = load "helperTheory"; *) 20open helperTheory; 21open helperNumTheory; 22open helperSetTheory; 23open helperFunctionTheory; 24open arithmeticTheory pred_setTheory; 25open dividesTheory; (* for divides_def, prime_def *) 26 27(* val _ = load "involuteFixTheory"; *) 28open involuteTheory; (* for involute_bij *) 29open involuteFixTheory; 30 31(* val _ = load "iterateComputeTheory"; *) 32open iterateTheory; 33open iterateComputeTheory; (* for iterate_while_thm *) 34 35 36(* ------------------------------------------------------------------------- *) 37(* Iteration of Involution Composition Documentation *) 38(* ------------------------------------------------------------------------- *) 39(* Overloading: 40*) 41(* 42 43 Helper Theorems: 44 45 Involution Composition Orbits: 46 involute_involute_permutes 47 |- !f g s. f involute s /\ g involute s ==> f o g PERMUTES s 48 involute_involute_involute 49 |- !f g s. f involute s /\ g involute s /\ f o g = g o f ==> 50 f o g involute s 51 52 Orbit as path: 53 involute_compose_inv 54 |- !f g s x. f involute s /\ g involute s /\ x IN s ==> 55 LINV (f o g) s x = (g o f) x 56 involute_funpow_inv 57 |- !f g s x n. f involute s /\ g involute s /\ x IN s ==> 58 FUNPOW (f o g) n (FUNPOW (g o f) n x) = x 59 60 Iteration of Composed Involutions: 61 iterate_involute_compose_inv 62 |- !f g s x n. f involute s /\ g involute s /\ x IN s ==> 63 LINV (FUNPOW (f o g) n) s x = FUNPOW (g o f) n x 64 iterate_involute_compose_eqn 65 |- !f g s x n. f involute s /\ g involute s /\ x IN s ==> 66 FUNPOW (g o f) n x = (g o FUNPOW (f o g) n o g) x 67 iterate_involute_compose_shift 68 |- !f g s x n. f involute s /\ g involute s /\ x IN s ==> 69 f (FUNPOW (g o f) n x) = FUNPOW (f o g) n (f x) 70 71 Iteration Period and Fixes: 72 iterate_involute_mod_period 73 |- !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN s /\ 74 p = iterate_period (f o g) x ==> 75 (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) 76 involute_involute_period_inv 77 |- !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 78 iterate_period (g o f) x = iterate_period (f o g) x 79 involute_involute_fixes_both 80 |- !f g s p x. f involute s /\ g involute s /\ x IN fixes f s /\ 81 p = iterate_period (f o g) x ==> (p = 1 <=> x IN fixes g s) 82 involute_involute_fix_orbit_1 83 |- !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 84 p = iterate_period (f o g) x ==> 85 (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> (i + j) MOD p = 0) 86 involute_involute_fix_orbit_2 87 |- !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 88 p = iterate_period (f o g) x ==> 89 (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> (i + j + 1) MOD p = 0) 90 involute_involute_fix_orbit_fix_even 91 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 92 p = iterate_period (f o g) x /\ EVEN p ==> 93 FUNPOW (f o g) (HALF p) x IN fixes f s 94 involute_involute_fix_orbit_fix_odd 95 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 96 p = iterate_period (f o g) x /\ ODD p ==> 97 FUNPOW (f o g) (HALF p) x IN fixes g s 98 involute_involute_fix_orbit_fix_even_distinct 99 |- !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 100 p = iterate_period (f o g) x /\ 101 (y = FUNPOW (f o g) (HALF p) x) /\ EVEN p ==> y IN fixes f s /\ y <> x 102 involute_involute_fix_orbit_fix_even_distinct_iff 103 |- !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 104 p = iterate_period (f o g) x /\ 105 (y = FUNPOW (f o g) (HALF p) x) /\ EVEN p ==> 106 y IN fixes f s /\ (y = x <=> p = 0) 107 involute_involute_fix_orbit_fix_odd_distinct 108 |- !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 109 p = iterate_period (f o g) x /\ 110 (y = FUNPOW (f o g) (HALF p) x) /\ ODD p ==> 111 y IN fixes g s /\ (1 < p ==> y <> x) 112 involute_involute_fix_orbit_fix_odd_distinct_iff 113 |- !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 114 p = iterate_period (f o g) x /\ 115 (y = FUNPOW (f o g) (HALF p) x) /\ ODD p ==> 116 y IN fixes g s /\ (y = x <=> p = 1) 117 involute_involute_fix_sing_period_odd 118 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ fixes f s = {x} /\ 119 p = iterate_period (f o g) x ==> ODD p 120 involute_involute_fix_iterates_1 121 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 122 p = iterate_period (f o g) x ==> 123 !j. j <= p ==> f (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - j) x 124 involute_involute_fix_iterates_2 125 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 126 p = iterate_period (f o g) x ==> 127 !j. j < p ==> g (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - 1 - j) x 128 involute_involute_fix_even_period_fix 129 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 130 p = iterate_period (f o g) x /\ EVEN p ==> 131 !j. 0 < j /\ j < p ==> (FUNPOW (f o g) j x IN fixes f s <=> (j = HALF p)) 132 involute_involute_fix_odd_period_fix 133 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 134 p = iterate_period (f o g) x /\ ODD p ==> 135 !j. 0 < j /\ j < p ==> (FUNPOW (f o g) j x IN fixes g s <=> (j = HALF p)) 136 137 Iteration Mate Involution: 138 iterate_mate_def |- !f g x. iterate_mate f g x = 139 (let h = HALF (iterate_period (f o g) x) 140 in if f x = x then FUNPOW (f o g) h x 141 else if g x = x then FUNPOW (g o f) h x 142 else x) 143 iterate_mate_element |- !f g s x. f involute s /\ g involute s /\ x IN s ==> 144 iterate_mate f g x IN s 145 iterate_mate_reverse |- !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 146 iterate_mate g f x = iterate_mate f g x 147 iterate_mate_fixes_mate 148 |- !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s ==> 149 iterate_mate f g (iterate_mate f g x) = x 150 iterate_mate_mate |- !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 151 iterate_mate f g (iterate_mate f g x) = x 152 iterate_mate_fixes_mate_fixes 153 |- !f g s x. FINITE s /\ f involute s /\ g involute s /\ 154 x IN fixes f s UNION fixes g s ==> 155 iterate_mate f g x IN fixes f s UNION fixes g s 156 iterate_mate_involute_fixes 157 |- !f g s. FINITE s /\ f involute s /\ g involute s ==> 158 iterate_mate f g involute fixes f s UNION fixes g s 159 160 Using direct WHILE: 161 involute_involute_fix_odd_period_fix_while 162 |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 163 x IN fixes f s /\ 164 p = iterate_period (f o g) x /\ ODD p ==> 165 WHILE (\y. g y <> y) (f o g) x IN fixes g s 166*) 167 168(* ------------------------------------------------------------------------- *) 169(* Helper Theorems *) 170(* ------------------------------------------------------------------------- *) 171 172(* ------------------------------------------------------------------------- *) 173(* Involution Composition Orbits *) 174(* ------------------------------------------------------------------------- *) 175 176(* Theorem: f involute s /\ g involute s ==> (f o g) PERMUTES s *) 177(* Proof: 178 Note f PERMUTES s /\ g PERMUTES s by involute_bij 179 ==> (f o g) PERMUTES s by BIJ_COMPOSE 180*) 181Theorem involute_involute_permutes: 182 !f g s. f involute s /\ g involute s ==> (f o g) PERMUTES s 183Proof 184 metis_tac[involute_bij, BIJ_COMPOSE] 185QED 186 187(* Idea: (f o g) involute s iff f and g are inverses. *) 188 189(* Theorem: f involute s /\ g involute s /\ f o g = g o f ==> (f o g) involute s *) 190(* Proof: 191 Note !x. x IN s ==> 192 (f x) IN s /\ (g x) IN s by involution 193 Thus (f o g) x = f (g x) IN s by o_THM, (g x) IN s 194 and (f o g) ((f o g) x) 195 = (f o g) ((g o f) x) by given 196 = f (g (g (f x))) by o_THM 197 = f (f x) by g involute s, (f x) IN s 198 = x by f involute s 199*) 200Theorem involute_involute_involute: 201 !f g s. f involute s /\ g involute s /\ f o g = g o f ==> (f o g) involute s 202Proof 203 ntac 4 strip_tac >> 204 `!x. x IN s ==> (f x) IN s /\ (g x) IN s` by rw[] >> 205 simp[] >> 206 rpt strip_tac >> 207 `!x. f (g x) = g (f x)` by fs[FUN_EQ_THM] >> 208 metis_tac[] 209QED 210 211(* ------------------------------------------------------------------------- *) 212(* Orbit as path. *) 213(* ------------------------------------------------------------------------- *) 214 215(* Theorem: f involute s /\ g involute s /\ x IN s ==> 216 (LINV (f o g) s) x = (g o f) x *) 217(* Proof: 218 Note (f o g) PERMUTES s by involute_involute_permutes 219 Let y = LINV (f o g) s x, 220 z = (g o f) x. 221 Then y IN s by BIJ_LINV_ELEMENT 222 and z IN s by o_THM 223 Now (f o g) y = x by BIJ_LINV_THM 224 and (f o g) z 225 = (f o g) ((g o f) x) 226 = f (g (g (f x))) by o_THM 227 = f (f x) by g involute s, f x IN s 228 = x by f involute s, x IN s 229 Thus y = z by BIJ_IS_INJ 230*) 231Theorem involute_compose_inv: 232 !f g s x. f involute s /\ g involute s /\ x IN s ==> 233 (LINV (f o g) s) x = (g o f) x 234Proof 235 rpt strip_tac >> 236 `(f o g) PERMUTES s` by rw[involute_involute_permutes] >> 237 qabbrev_tac `y = LINV (f o g) s x` >> 238 qabbrev_tac `z = (g o f) x` >> 239 `y IN s` by metis_tac[BIJ_LINV_ELEMENT] >> 240 `z IN s` by fs[Abbr`z`] >> 241 `(f o g) y = x` by metis_tac[BIJ_LINV_THM] >> 242 `(f o g) z = x` by fs[Abbr`z`] >> 243 metis_tac[BIJ_IS_INJ] 244QED 245 246(* Theorem: f involute s /\ g involute s /\ x IN s ==> 247 FUNPOW (f o g) n (FUNPOW (g o f) n x) = x *) 248(* Proof: 249 By induction on n. 250 Base: FUNPOW (f o g) 0 (FUNPOW (g o f) 0 x) = x 251 FUNPOW (f o g) 0 (FUNPOW (g o f) 0 x) 252 = FUNPOW (f o g) 0 x by FUNPOW_0 253 = x by FUNPOW_0 254 Step: !x. FUNPOW (f o g) n (FUNPOW (g o f) n x) = x ==> 255 FUNPOW (f o g) (SUC n) (FUNPOW (g o f) (SUC n) x) = x 256 Note (g o f) x IN s by BIJ_ELEMENT 257 FUNPOW (f o g) (SUC n) (FUNPOW (g o f) (SUC n) x) 258 = (f o g) (FUNPOW (f o g) n (FUNPOW (g o f) (SUC n) x)) by FUNPOW_SUC 259 = (f o g) (FUNPOW (f o g) n (FUNPOW (g o f) n ((g o f) x))) by FUNPOW 260 = (f o g) ((g o f) x) by induction hypothesis 261 = x by f involute s, g involute s 262*) 263Theorem involute_funpow_inv: 264 !f g s x n. f involute s /\ g involute s /\ x IN s ==> 265 FUNPOW (f o g) n (FUNPOW (g o f) n x) = x 266Proof 267 ntac 3 strip_tac >> 268 Induct_on `n` >- 269 simp[] >> 270 rpt strip_tac >> 271 `(g o f) x IN s` by rw[BIJ_COMPOSE, BIJ_ELEMENT] >> 272 `FUNPOW (f o g) (SUC n) (FUNPOW (g o f) (SUC n) x) 273 = (f o g) (FUNPOW (f o g) n (FUNPOW (g o f) (SUC n) x))` by rw[FUNPOW_SUC] >> 274 `_ = (f o g) (FUNPOW (f o g) n (FUNPOW (g o f) n ((g o f) x)))` by rw[FUNPOW] >> 275 `_ = (f o g) ((g o f) x)` by rw[] >> 276 `_ = x` by fs[] >> 277 simp[] 278QED 279 280(* ------------------------------------------------------------------------- *) 281(* Iteration of Composed Involutions. *) 282(* ------------------------------------------------------------------------- *) 283 284(* Theorem: f involute s /\ g involute s /\ x IN s ==> 285 FUNPOW (f o g) n (FUNPOW (g o f) n x) = x *) 286(* Proof: by involute_funpow_inv *) 287(* Theorem not stored as this is just an alias of involute_funpow_inv. *) 288val iterate_involute_inv = prove( 289 ``!f g s x n. f involute s /\ g involute s /\ x IN s ==> 290 FUNPOW (f o g) n (FUNPOW (g o f) n x) = x``, 291 rpt strip_tac >> 292 irule involute_funpow_inv >> 293 metis_tac[]); 294(* This is just involute_funpow_inv. 295 Funny that simp[involute_funpow_inv], rw, or metis_tac, or prove_tac ... 296 will not work! 297 Possibly due to difficulty in matching two function compositions. 298 Many proofs below have such problems, which can be resolved by: 299 . invoke imp_res_tac 300 . invoke assume_tac 301 . invoke drule_then 302*) 303 304(* Theorem: f involute s /\ g involute s /\ x IN s ==> 305 (LINV (FUNPOW (f o g) n) s) x = FUNPOW (g o f) n x *) 306(* Proof: 307 Note (f o g) PERMUTES s by involute_involute_permutes 308 and (g o f) PERMUTES s by involute_involute_permutes 309 Let y = LINV (FUNPOW (f o g) n) s x, 310 z = FUNPOW (g o f) n x, 311 h = FUNPOW (f o g) n. 312 Then h PERMUTES s by FUNPOW_permutes 313 so y IN s by BIJ_LINV_ELEMENT 314 and z IN s by FUNPOW_closure 315 Now h y = x by BIJ_LINV_THM, h PERMUTES s 316 and h z = x by involute_funpow_inv 317 Thus y = z by BIJ_IS_INJ 318*) 319Theorem iterate_involute_compose_inv: 320 !f g s x n. f involute s /\ g involute s /\ x IN s ==> 321 (LINV (FUNPOW (f o g) n) s) x = FUNPOW (g o f) n x 322Proof 323 rpt strip_tac >> 324 `(f o g) PERMUTES s /\ (g o f) PERMUTES s` by rw[involute_involute_permutes] >> 325 qabbrev_tac `y = LINV (FUNPOW (f o g) n) s x` >> 326 qabbrev_tac `z = FUNPOW (g o f) n x` >> 327 qabbrev_tac `h = FUNPOW (f o g) n` >> 328 `h PERMUTES s` by rw[FUNPOW_permutes, Abbr`h`] >> 329 `y IN s` by metis_tac[BIJ_LINV_ELEMENT] >> 330 `z IN s` by fs[FUNPOW_closure, Abbr`z`] >> 331 `h y = x` by metis_tac[BIJ_LINV_THM] >> 332 imp_res_tac involute_funpow_inv >> 333 `h z = x` by fs[Abbr`h`, Abbr`z`] >> 334 metis_tac[BIJ_IS_INJ] 335QED 336 337(* Theorem: f involute s /\ g involute s /\ x IN s ==> 338 FUNPOW (g o f) n x = (g o (FUNPOW (f o g) n) o g) x *) 339(* Proof: 340 By induction on n. 341 Base: FUNPOW (g o f) 0 x = g (FUNPOW (f o g) 0 (g x)) 342 LHS = FUNPOW (g o f) 0 x = x by FUNPOW_0 343 RHS = g (FUNPOW (f o g) 0 (g x)) 344 = g (g x) by FUNPOW_0 345 = x by g involute s 346 Step: FUNPOW (g o f) n x = g (FUNPOW (f o g) n (g x)) ==> 347 FUNPOW (g o f) (SUC n) x = g (FUNPOW (f o g) (SUC n) (g x)) 348 FUNPOW (g o f) (SUC n) x 349 = (g o f) (FUNPOW (g o f) n x) by FUNPOW_SUC 350 = (g o f) (g (FUNPOW (f o g) n (g x)) by induction hypothesis 351 = g ((f o g) (FUNPOW (f o g) n (g x))) by o_THM 352 = g (FUNPOW (f o g) (SUC n) (g x)) by FUNPOW_SUC 353*) 354Theorem iterate_involute_compose_eqn: 355 !f g s x n. f involute s /\ g involute s /\ x IN s ==> 356 FUNPOW (g o f) n x = (g o (FUNPOW (f o g) n) o g) x 357Proof 358 rpt strip_tac >> 359 Induct_on `n` >- 360 simp[] >> 361 simp[FUNPOW_SUC] 362QED 363 364(* Note: 365 f o (g o f) o (g o f) o (g o f) 366 = (f o g) o (f o g) o (f o g) o f by associativity 367 368 The following is a formal proof of this situation. 369*) 370 371(* Theorem: f involute s /\ g involute s /\ x IN s ==> 372 f (FUNPOW (g o f) n x) = FUNPOW (f o g) n (f x) *) 373(* Proof: 374 By induction on n. 375 Base: f (FUNPOW (g o f) 0 x) = FUNPOW (f o g) 0 (f x) 376 f (FUNPOW (g o f) 0 x) 377 = f x by FUNPOW_0 378 = FUNPOW (f o g) 0 (f x) by FUNPOW_0 379 Step: f (FUNPOW (g o f) n x) = FUNPOW (f o g) n (f x) ==> 380 f (FUNPOW (g o f) (SUC n) x) = FUNPOW (f o g) (SUC n) (f x) 381 f (FUNPOW (g o f) (SUC n) x) 382 = f ((g o f) (FUNPOW (g o f) n x)) by FUNPOW_SUC 383 = f o g (f (FUNPOW (g o f) n x)) by o_THM 384 = f o g (FUNPOW (f o g) n (f x)) by induction hypothesis 385 = FUNPOW (f o g) (SUC n) (f x) by FUNPOW_SUC 386*) 387Theorem iterate_involute_compose_shift: 388 !f g s x n. f involute s /\ g involute s /\ x IN s ==> 389 f (FUNPOW (g o f) n x) = FUNPOW (f o g) n (f x) 390Proof 391 rpt strip_tac >> 392 Induct_on `n` >- 393 simp[] >> 394 simp[FUNPOW_SUC] 395QED 396 397(* ------------------------------------------------------------------------- *) 398(* Iteration Period and Fixes. *) 399(* ------------------------------------------------------------------------- *) 400 401(* Idea: iterates (f o g)^i = (g o f)^j iff (i + j) MOD p = 0. *) 402 403(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 404 x IN s /\ p = iterate_period (f o g) x ==> 405 (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) *) 406(* Proof: 407 Note f o g PERMUTES s by involute_involute_permutes 408 and 0 < p by iterate_period_pos, FINITE s 409 410 If part: FUNPOW (f o g) i x = FUNPOW (g o f) j x ==> (i + j) MOD p = 0 411 FUNPOW (f o g) (i + j) x 412 = FUNPOW (f o g) (j + i) x by arithmetic 413 = FUNPOW (f o g) j (FUNPOW (f o g) i x) by FUNPOW_ADD 414 = FUNPOW (f o g) j (FUNPOW (g o f) j x) by given 415 = x by involute_funpow_inv, x IN s 416 Thus (i + j) MOD p = 0 by iterate_period_mod 417 418 Only-if part: (i + j) MOD p = 0 ==> FUNPOW (f o g) i x = FUNPOW (g o f) j x 419 Note FUNPOW (f o g) p x = x by iterate_period_property, [1] 420 so ?k. (i + j) = k * p by MOD_EQ_0_DIVISOR, (i + j) MOD p = 0 421 Let y = FUNPOW (f o g) i x. 422 Then y IN s by FUNPOW_closure, f o g PERMUTES s 423 FUNPOW (f o g) i x = y 424 = FUNPOW (g o f) j (FUNPOW (f o g) j y) by involute_funpow_inv, y IN s 425 = FUNPOW (g o f) j (FUNPOW (f o g) (j + i) x) by FUNPOW_ADD 426 = FUNPOW (g o f) j (FUNPOW (f o g) p x) by FUNPOW_MULTIPLE, 0 < p 427 = FUNPOW (g o f) j x by [1] 428*) 429Theorem iterate_involute_mod_period: 430 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 431 x IN s /\ p = iterate_period (f o g) x ==> 432 (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) 433Proof 434 rpt strip_tac >> 435 qabbrev_tac `y = FUNPOW (f o g) i x` >> 436 qabbrev_tac `z = FUNPOW (g o f) j x` >> 437 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 438 `0 < p` by metis_tac[iterate_period_pos] >> 439 (rewrite_tac[EQ_IMP_THM] >> rpt strip_tac) >| [ 440 assume_tac involute_funpow_inv >> 441 last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `j`] strip_assume_tac) >> 442 `FUNPOW (f o g) (i + j) x = FUNPOW (f o g) (j + i) x` by simp[] >> 443 `_ = FUNPOW (f o g) j z` by rw[FUNPOW_ADD] >> 444 `_ = x` by fs[Abbr`z`] >> 445 metis_tac[iterate_period_mod], 446 `?k. (i + j) = k * p` by rfs[MOD_EQ_0_DIVISOR] >> 447 `y IN s` by rw[FUNPOW_closure, Abbr`y`] >> 448 `FUNPOW (f o g) p x = x` by rw[iterate_period_property] >> 449 assume_tac involute_funpow_inv >> 450 last_x_assum (qspecl_then [`g`, `f`, `s`, `y`, `j`] strip_assume_tac) >> 451 `y = FUNPOW (g o f) j (FUNPOW (f o g) j y)` by fs[] >> 452 `_ = FUNPOW (g o f) j (FUNPOW (f o g) (j + i) x)` by metis_tac[FUNPOW_ADD] >> 453 rfs[FUNPOW_MULTIPLE] 454 ] 455QED 456 457(* Better proof of the same theorem. *) 458 459(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 460 x IN s /\ p = iterate_period (f o g) x ==> 461 (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) *) 462(* Proof: 463 Let y = FUNPOW (f o g) i x, 464 z = FUNPOW (g o f) j x, 465 h = FUNPOW (f o g) j. 466 Note f o g PERMUTES s by involute_involute_permutes 467 and g o f PERMUTES s by involute_involute_permutes 468 so y IN s and z IN s by FUNPOW_closure 469 also 0 < p by iterate_period_pos, FINITE s 470 and h PERMUTES s by FUNPOW_permutes 471 Note h y 472 = FUNPOW (f o g) (j + i) x by FUNPOW_ADD 473 = FUNPOW (f o g) (i + j) x by arithmetic 474 and h z = x by involute_funpow_inv, x IN s 475 476 y = z 477 <=> h y = h z by BIJ_DEF, INJ_EQ_11 478 <=> FUNPOW (f o g) (i + j) x = x by above 479 <=> (i + j) MOD p = 0 by iterate_period_mod, 0 < p 480*) 481Theorem iterate_involute_mod_period: 482 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 483 x IN s /\ p = iterate_period (f o g) x ==> 484 (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) 485Proof 486 rpt strip_tac >> 487 qabbrev_tac `y = FUNPOW (f o g) i x` >> 488 qabbrev_tac `z = FUNPOW (g o f) j x` >> 489 qabbrev_tac `h = FUNPOW (f o g) j` >> 490 `f o g PERMUTES s /\ g o f PERMUTES s` by rw[involute_involute_permutes] >> 491 `y IN s /\ z IN s` by rw[FUNPOW_closure, Abbr`y`, Abbr`z`] >> 492 `0 < p` by metis_tac[iterate_period_pos] >> 493 `h PERMUTES s` by rw[FUNPOW_permutes, Abbr`h`] >> 494 `h y = FUNPOW (f o g) (j + i) x` by fs[FUNPOW_ADD, Abbr`h`, Abbr`y`] >> 495 `_ = FUNPOW (f o g) (i + j) x` by simp[] >> 496 assume_tac involute_funpow_inv >> 497 last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `j`] strip_assume_tac) >> 498 `h z = x` by rfs[] >> 499 `(y = z) <=> (h y = h z)` by metis_tac[BIJ_DEF, INJ_EQ_11] >> 500 `_ = (FUNPOW (f o g) (i + j) x = x)` by fs[] >> 501 `_ = ((i + j) MOD p = 0)` by rw[iterate_period_mod] >> 502 simp[] 503QED 504 505(* Idea: period of (g o f) equals period of (f o g). *) 506 507(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 508 iterate_period (g o f) x = iterate_period (f o g) x *) 509(* Proof: 510 Cannot show: LINV (f o g) s = g o f 511 see involute_compose_inv 512 although there is iterate_involute_compose_inv. 513 514 Note f o g PERMUTES s by involute_involute_permutes 515 and g o f PERMUTES s by involute_involute_permutes 516 Let p = iterate_period (f o g) x, 517 q = iterate_period (g o f) x, 518 then goal becomes: q = p. 519 520 Note 0 < p /\ 0 < q by iterate_period_pos 521 By iterate_period_thm, this is to show: 522 (1) FUNPOW (g o f) p x = x 523 Note (0 + p) MOD p = 0 by DIVMOD_ID 524 FUNPOW (g o f) p x 525 = FUNPOW (f o g) 0 x by iterate_involute_mod_period 526 = x by FUNPOW_0 527 (2) !m. 0 < m /\ m < p ==> FUNPOW (g o f) m x <> x 528 Note ((p - m) + m) MOD p = 0 by DIVMOD_ID 529 and p - m < p by arithmetic 530 FUNPOW (g o f) m x 531 = FUNPOW (f o g) (p - m) x by iterate_involute_mod_period 532 <> x by iterate_period_minimal 533*) 534Theorem involute_involute_period_inv: 535 !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 536 iterate_period (g o f) x = iterate_period (f o g) x 537Proof 538 rpt strip_tac >> 539 `f o g PERMUTES s /\ g o f PERMUTES s` by rw[involute_involute_permutes] >> 540 qabbrev_tac `p = iterate_period (f o g) x` >> 541 qabbrev_tac `q = iterate_period (g o f) x` >> 542 `0 < p /\ 0 < q` by metis_tac[iterate_period_pos] >> 543 simp[iterate_period_thm, Abbr`q`] >> 544 qabbrev_tac `q = iterate_period (g o f) x` >> 545 rpt strip_tac >| [ 546 `(0 + p) MOD p = 0` by rw[] >> 547 drule_then strip_assume_tac iterate_involute_mod_period >> 548 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `0`, `p`] strip_assume_tac) >> 549 rfs[], 550 `((p - m) + m) MOD p = 0` by rw[] >> 551 `p - m < p` by decide_tac >> 552 drule_then strip_assume_tac iterate_involute_mod_period >> 553 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `p - m`, `m`] strip_assume_tac) >> 554 rfs[iterate_period_minimal, Abbr`p`] 555 ] 556QED 557 558(* Idea: when f fixes x, then g fixes x iff (f o g) has period 1 for x. *) 559 560(* Theorem: f involute s /\ g involute s /\ x IN fixes f s /\ 561 p = iterate_period (f o g) x ==> (p = 1 <=> x IN fixes g s) *) 562(* Proof: 563 If part: x IN s /\ f x = x ==> g x = x 564 Note (f o g) x = x by iterate_period_eq_1 565 so f (g x) = x by o_THM 566 Thus g x = x by BIJ_IS_INJ, f x = x 567 Only-if part: x IN s /\ g x = x /\ f x = x ==> p = 1 568 Note (f o g) x 569 = f (g x) by o_THM 570 = f x by g x = x 571 = x by f x = x 572 Thus p = 1 by iterate_period_eq_1 573*) 574Theorem involute_involute_fixes_both: 575 !f g s p x. f involute s /\ g involute s /\ 576 x IN fixes f s /\ p = iterate_period (f o g) x ==> 577 (p = 1 <=> x IN fixes g s) 578Proof 579 rw[fixes_def, iterate_period_eq_1, EQ_IMP_THM] >> 580 metis_tac[BIJ_IS_INJ] 581QED 582 583(* Idea: when f fixes x, then (f o g)^i = f ((f o g)^j) iff (i+j) MOD p = 0. *) 584 585(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 586 x IN fixes f s /\ p = iterate_period (f o g) x ==> 587 (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> (i + j) MOD p = 0) *) 588(* Proof: 589 Note x IN s /\ f x = x by fixes_element 590 591 If part: FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) ==> (i + j) MOD p = 0 592 Note f o g PERMUTES s by involute_involute_permutes 593 so 0 < p by iterate_period_pos, FINITE s 594 FUNPOW (f o g) (i + j) x 595 = FUNPOW (f o g) i (FUNPOW (f o g) j x) by FUNPOW_ADD 596 = FUNPOW (f o g) i (f (f (FUNPOW (f o g) j x))) by FUNPOW_closure, f o g involute s 597 = FUNPOW (f o g) i (f (FUNPOW (f o g) i x)) by given 598 = f (FUNPOW (g o f) i (FUNPOW (f o g) i x)) by iterate_involute_compose_shift 599 = f x by involute_funpow_inv 600 = x by involute_fixed_points 601 Thus (i + j) MOD p = 0 by iterate_period_mod, 0 < p 602 603 Only-if part: (i + j) MOD p = 0 ==> FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) 604 f (FUNPOW (f o g) j x) 605 = f (FUNPOW (g o f) i x) by iterate_involute_mod_period 606 = FUNPOW (f o g) i (f x) by iterate_involute_compose_shift 607 = FUNPOW (f o g) i x by involute_fixed_points, f x = x 608*) 609Theorem involute_involute_fix_orbit_1: 610 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 611 x IN fixes f s /\ p = iterate_period (f o g) x ==> 612 (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> 613 (i + j) MOD p = 0) 614Proof 615 rpt strip_tac >> 616 qabbrev_tac `y = FUNPOW (f o g) i x` >> 617 qabbrev_tac `z = FUNPOW (f o g) j x` >> 618 `x IN s /\ f x = x` by fs[fixes_element] >> 619 (simp[EQ_IMP_THM] >> rpt strip_tac) >| [ 620 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 621 `0 < p` by metis_tac[iterate_period_pos] >> 622 `y IN s /\ z IN s` by fs[FUNPOW_closure, Abbr`y`, Abbr`z`] >> 623 imp_res_tac iterate_involute_compose_shift >> 624 `f (FUNPOW (g o f) i y) = FUNPOW (f o g) i (f y)` by fs[] >> 625 assume_tac involute_funpow_inv >> 626 last_x_assum (qspecl_then [`g`, `f`, `s`, `x`, `i`] strip_assume_tac) >> 627 `FUNPOW (g o f) i y = x` by rfs[] >> 628 `FUNPOW (f o g) (i + j) x = FUNPOW (f o g) i z` by rw[FUNPOW_ADD, Abbr`z`] >> 629 `_ = FUNPOW (f o g) i (f (f z))` by rw[] >> 630 `_ = FUNPOW (f o g) i (f y)` by rw[] >> 631 `_ = f (FUNPOW (g o f) i y)` by fs[] >> 632 `_ = f x` by fs[Abbr`y`] >> 633 `_ = x` by rfs[] >> 634 metis_tac[iterate_period_mod], 635 drule_then strip_assume_tac iterate_involute_mod_period >> 636 `z = FUNPOW (g o f) i x` by fs[Abbr`z`] >> 637 imp_res_tac iterate_involute_compose_shift >> 638 `f (FUNPOW (g o f) i x) = FUNPOW (f o g) i (f x)` by fs[] >> 639 `f z = f (FUNPOW (g o f) i x)` by fs[] >> 640 `_ = FUNPOW (f o g) i (f x)` by fs[] >> 641 `_ = y` by fs[Abbr`y`] >> 642 simp[] 643 ] 644QED 645 646(* Better proof of the same theorem. *) 647 648(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 649 x IN fixes f s /\ p = iterate_period (f o g) x ==> 650 (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> (i + j) MOD p = 0) *) 651(* Proof: 652 Note x IN s /\ f x = x by fixes_element 653 and f o g PERMUTES s by involute_involute_permutes 654 and g o f PERMUTES s by involute_involute_permutes 655 so FUNPOW (g o f) i x IN s by FUNPOW_closure 656 and FUNPOW (f o g) j x IN s by FUNPOW_closure 657 also 0 < p by iterate_period_pos 658 659 FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) 660 <=> FUNPOW (f o g) i (f x) = f (FUNPOW (f o g) j x) by f x = x, above 661 <=> f (FUNPOW (g o f) i x) = f (FUNPOW (f o g) j x) by iterate_involute_compose_shift 662 <=> FUNPOW (g o f) i x = FUNPOW (f o g) j x by BIJ_DEF, INJ_EQ_11 663 <=> (i + j) MOD p = 0 by iterate_involute_mod_period, 0 < p 664*) 665Theorem involute_involute_fix_orbit_1: 666 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 667 x IN fixes f s /\ p = iterate_period (f o g) x ==> 668 (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> 669 (i + j) MOD p = 0) 670Proof 671 rpt strip_tac >> 672 qabbrev_tac `y = FUNPOW (f o g) j x` >> 673 qabbrev_tac `z = FUNPOW (f o g) i x` >> 674 `x IN s /\ f x = x` by fs[fixes_element] >> 675 qabbrev_tac `t = FUNPOW (g o f) i x` >> 676 `f o g PERMUTES s /\ g o f PERMUTES s` by rw[involute_involute_permutes] >> 677 `0 < p` by metis_tac[iterate_period_pos] >> 678 `y IN s /\ t IN s` by rw[FUNPOW_closure, Abbr`y`, Abbr`t`] >> 679 assume_tac iterate_involute_compose_shift >> 680 last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `i`] strip_assume_tac) >> 681 `(z = f y) <=> (FUNPOW (f o g) i (f x) = f y)` by metis_tac[] >> 682 `_ = (f t = f y)` by rfs[] >> 683 `_ = (t = y)` by metis_tac[BIJ_DEF, INJ_EQ_11] >> 684 drule_then strip_assume_tac iterate_involute_mod_period >> 685 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `j`, `i`] strip_assume_tac) >> 686 metis_tac[ADD_COMM] 687QED 688 689(* Idea: when f fixes x, then (f o g)^i = g ((f o g)^j) iff (i+j+1) MOD p = 0. *) 690 691(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 692 x IN fixes f s /\ p = iterate_period (f o g) x ==> 693 (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> (i + j + 1) MOD p = 0) *) 694(* Proof: 695 Note x IN s /\ f x = x by fixes_element 696 697 If part: FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) ==> (i + j + 1) MOD p = 0 698 Note f o g PERMUTES s by involute_involute_permutes 699 so 0 < p by iterate_period_pos, FINITE s 700 FUNPOW (f o g) (i + j + 1) x 701 = (f o g) (FUNPOW (f o g) (i + j) x) by FUNPOW_SUC 702 = (f o g) (FUNPOW (f o g) i (FUNPOW (f o g) j x)) by FUNPOW_ADD 703 = f (g (FUNPOW (f o g) i (FUNPOW (f o g) j x))) by o_THM 704 = f (FUNPOW (g o f) i (g (FUNPOW (f o g) j x))) by iterate_involute_compose_shift 705 = f (FUNPOW (g o f) i (FUNPOW (f o g) i x)) by given 706 = f x by involute_funpow_inv 707 = x by involute_fixed_points 708 Thus (i + j + 1) MOD p = 0 by iterate_period_mod, 0 < p 709 710 Only-if part: (i + j + 1) MOD p = 0 ==> FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) 711 FUNPOW (f o g) i x 712 = FUNPOW (g o f) (j + 1) x by iterate_involute_mod_period 713 = FUNPOW (g o f) j ((g o f) x) by FUNPOW 714 = FUNPOW (g o f) j (g (f x)) by o_THM 715 = FUNPOW (g o f) j (g x) by f x = x 716 = g (FUNPOW (f o g) j x) by iterate_involute_compose_shift 717*) 718Theorem involute_involute_fix_orbit_2: 719 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 720 x IN fixes f s /\ p = iterate_period (f o g) x ==> 721 (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> 722 (i + j + 1) MOD p = 0) 723Proof 724 rpt strip_tac >> 725 qabbrev_tac `y = FUNPOW (f o g) j x` >> 726 qabbrev_tac `z = FUNPOW (f o g) i x` >> 727 `x IN s /\ f x = x` by fs[fixes_element] >> 728 (rewrite_tac[EQ_IMP_THM] >> rpt strip_tac) >| [ 729 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 730 `0 < p` by metis_tac[iterate_period_pos] >> 731 `y IN s /\ z IN s` by rw[FUNPOW_closure, Abbr`y`, Abbr`z`] >> 732 imp_res_tac iterate_involute_compose_shift >> 733 `g (FUNPOW (f o g) i y) = FUNPOW (g o f) i (g y)` by fs[] >> 734 imp_res_tac involute_funpow_inv >> 735 `FUNPOW (g o f) i z = x` by fs[Abbr`z`] >> 736 `i + j + 1 = SUC (i + j)` by decide_tac >> 737 `FUNPOW (f o g) (i + j + 1) x = FUNPOW (f o g) (SUC (i + j)) x` by rw[] >> 738 `_ = (f o g) (FUNPOW (f o g) (i + j) x)` by fs[FUNPOW_SUC] >> 739 `_ = (f o g) (FUNPOW (f o g) i y)` by fs[FUNPOW_ADD, Abbr`y`] >> 740 `_ = f (g (FUNPOW (f o g) i y))` by rw[] >> 741 `_ = f (FUNPOW (g o f) i (g y))` by fs[] >> 742 `_ = f (FUNPOW (g o f) i z)` by metis_tac[] >> 743 `_ = f x` by rfs[] >> 744 `_ = x` by fs[] >> 745 metis_tac[iterate_period_mod], 746 drule_then strip_assume_tac iterate_involute_mod_period >> 747 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `i`, `j+1`] strip_assume_tac) >> 748 `FUNPOW (g o f) (j + 1) x = z` by rfs[Abbr`z`] >> 749 drule_then strip_assume_tac iterate_involute_compose_shift >> 750 `g y = FUNPOW (g o f) j (g x)` by fs[Abbr`y`] >> 751 `_ = FUNPOW (g o f) j ((g o f) x)` by fs[] >> 752 `_ = FUNPOW (g o f) (j + 1) x` by rw[GSYM FUNPOW, ADD1] >> 753 `_ = z` by fs[] >> 754 simp[] 755 ] 756QED 757 758(* Better proof of the same theorem. *) 759 760(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 761 x IN fixes f s /\ p = iterate_period (f o g) x ==> 762 (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> (i + j + 1) MOD p = 0) *) 763(* Proof: 764 Note x IN s /\ f x = x by fixes_element 765 and f o g PERMUTES s by involute_involute_permutes 766 also 0 < p by iterate_period_pos 767 768 FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) 769 <=> FUNPOW (f o g) i x = g (FUNPOW (f o g) j (f x)) by f x = x, above 770 <=> FUNPOW (f o g) i x = g (f (FUNPOW (g o f) j x)) by iterate_involute_compose_shift 771 <=> FUNPOW (f o g) i x = (g o f) (FUNPOW (g o f) j x) by o_THM 772 <=> FUNPOW (f o g) i x = FUNPOW (g o f) (j + 1) x by FUNPOW 773 <=> (i + j + 1) MOD p = 0 by iterate_involute_mod_period, 0 < p 774*) 775Theorem involute_involute_fix_orbit_2: 776 !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ 777 x IN fixes f s /\ p = iterate_period (f o g) x ==> 778 (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> 779 (i + j + 1) MOD p = 0) 780Proof 781 rpt strip_tac >> 782 qabbrev_tac `y = FUNPOW (f o g) j x` >> 783 qabbrev_tac `z = FUNPOW (f o g) i x` >> 784 `x IN s /\ f x = x` by fs[fixes_element] >> 785 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 786 `0 < p` by metis_tac[iterate_period_pos] >> 787 qabbrev_tac `t = FUNPOW (g o f) j x` >> 788 assume_tac iterate_involute_compose_shift >> 789 last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `j`] strip_assume_tac) >> 790 `(z = g y) <=> (z = g (FUNPOW (f o g) j (f x)))` by fs[] >> 791 `_ = (z = g (f t))` by rfs[] >> 792 `_ = (z = (g o f) (FUNPOW (g o f) j x))` by rfs[] >> 793 `_ = (z = FUNPOW (g o f) (j + 1) x)` by rfs[FUNPOW_SUC, GSYM ADD1] >> 794 assume_tac iterate_involute_mod_period >> 795 last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `p`, `i`, `j+1`] strip_assume_tac) >> 796 rfs[] 797QED 798 799(* Idea: when f fixes x, and (f o g) has even period p for x, 800 then f also fixes (f o g)^(p/2) x. *) 801 802(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 803 p = iterate_period (f o g) x /\ EVEN p ==> 804 (FUNPOW (f o g) (p DIV 2) x) IN fixes f s *) 805(* Proof: 806 Let h = p DIV 2, 807 y = FUNPOW (f o g) h x. 808 Note p = h * 2 + p MOD 2 by DIVISION 809 = 2 * h + 0 by EVEN_MOD2 810 = h + h by arithmetic 811 Note (f o g) PERMUTES s by involute_involute_permutes 812 and x IN s by fixes_element 813 so 0 < p by iterate_period_pos 814 and p MOD p = 0 by DIVMOD_ID, 0 < p 815 816 Now y IN s by FUNPOW_closure 817 Thus f y = y by involute_involute_fix_orbit_1, x IN fixes f s 818 ==> y IN fixes f s by fixes_element 819*) 820Theorem involute_involute_fix_orbit_fix_even: 821 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 822 p = iterate_period (f o g) x /\ EVEN p ==> 823 (FUNPOW (f o g) (p DIV 2) x) IN fixes f s 824Proof 825 rpt strip_tac >> 826 qabbrev_tac `h = p DIV 2` >> 827 qabbrev_tac `y = FUNPOW (f o g) h x` >> 828 `p = h * 2 + p MOD 2` by rw[DIVISION, Abbr`h`] >> 829 `_ = 2 * h + 0` by fs[EVEN_MOD2] >> 830 `_ = h + h` by decide_tac >> 831 `(f o g) PERMUTES s` by rw[involute_involute_permutes] >> 832 `x IN s` by fs[fixes_element] >> 833 `y IN s` by fs[FUNPOW_closure, Abbr`y`] >> 834 `0 < p` by metis_tac[iterate_period_pos] >> 835 `p MOD p = 0` by rw[] >> 836 drule_then strip_assume_tac involute_involute_fix_orbit_1 >> 837 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `h`, `h`] strip_assume_tac) >> 838 `f y = y` by metis_tac[] >> 839 fs[fixes_element] 840QED 841 842(* When f fixes x, and (f o g) has odd period p for x, 843 then g fixes (f o g)^(p/2) x. *) 844 845(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 846 p = iterate_period (f o g) x /\ ODD p ==> 847 (FUNPOW (f o g) (p DIV 2) x) IN fixes g s *) 848(* Proof: 849 Let h = p DIV 2, 850 y = FUNPOW (f o g) h x. 851 Note p = h * 2 + p MOD 2 by DIVISION 852 = 2 * h + 1 by ODD_MOD2 853 = h + h + 1 by arithmetic 854 so 0 < p by p = 2 * h + 1 855 and p MOD p = 0 by DIVMOD_ID, 0 < p 856 857 Note (f o g) PERMUTES s by involute_involute_permutes 858 so x IN s by fixes_element 859 and y IN s by FUNPOW_closure 860 Thus g y = y by involute_involute_fix_orbit_2, x IN fixes f s 861 ==> y IN fixes g s by fixes_element 862*) 863Theorem involute_involute_fix_orbit_fix_odd: 864 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 865 p = iterate_period (f o g) x /\ ODD p ==> 866 (FUNPOW (f o g) (p DIV 2) x) IN fixes g s 867Proof 868 rpt strip_tac >> 869 qabbrev_tac `h = p DIV 2` >> 870 qabbrev_tac `y = FUNPOW (f o g) h x` >> 871 `p = h * 2 + p MOD 2` by rw[DIVISION, Abbr`h`] >> 872 `_ = 2 * h + 1` by fs[ODD_MOD2] >> 873 `_ = h + h + 1` by decide_tac >> 874 `p MOD p = 0` by rw[] >> 875 `(f o g) PERMUTES s` by rw[involute_involute_permutes] >> 876 `x IN s` by fs[fixes_element] >> 877 `y IN s` by fs[FUNPOW_closure, Abbr`y`] >> 878 drule_then strip_assume_tac involute_involute_fix_orbit_2 >> 879 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `h`, `h`] strip_assume_tac) >> 880 `g y = y` by rfs[Abbr`y`] >> 881 fs[fixes_element] 882QED 883 884(* Idea: when f fixes x, and (f o g) has even period p for x, 885 then f also fixes (f o g)^(p/2) x, which is not x itself. *) 886 887(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 888 p = iterate_period (f o g) x /\ 889 (y = FUNPOW (f o g) (p DIV 2) x) /\ 890 EVEN p ==> (y IN fixes f s /\ y <> x) *) 891(* Proof: 892 Note y IN fixes f s by involute_involute_fix_orbit_fix_even 893 Remains to show: y <> x. 894 By contradiction, suppose y = x. 895 Note x IN s by fixes_element 896 and f o g PERMUTES s by involute_involute_permutes 897 so 0 < p by iterate_period_pos 898 ==> p DIV 2 < p by DIV_LESS, 0 < p 899 Thus ~(0 < HALF p) by iterate_period_minimal, y = x. 900 or HALF p = 0 by ~(0 < HALF p) 901 so p = 1 by HALF_EQ_0 902 This contradicts EVEN p by ODD_1, ODD_EVEN 903*) 904Theorem involute_involute_fix_orbit_fix_even_distinct: 905 !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 906 p = iterate_period (f o g) x /\ 907 (y = FUNPOW (f o g) (p DIV 2) x) /\ 908 EVEN p ==> (y IN fixes f s /\ y <> x) 909Proof 910 ntac 7 strip_tac >> 911 drule_then strip_assume_tac involute_involute_fix_orbit_fix_even >> 912 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`] strip_assume_tac) >> 913 `y IN fixes f s` by fs[] >> 914 (rpt strip_tac >> simp[]) >> 915 `x IN s` by fs[fixes_element] >> 916 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 917 `0 < p` by metis_tac[iterate_period_pos] >> 918 `p DIV 2 < p` by rw[DIV_LESS] >> 919 `~(0 < HALF p)` by metis_tac[iterate_period_minimal] >> 920 `HALF p = 0` by decide_tac >> 921 `p = 1` by fs[HALF_EQ_0] >> 922 metis_tac[ODD_1, ODD_EVEN] 923QED 924 925(* Another version of involute_involute_fix_orbit_fix_even_distinct *) 926 927(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 928 p = iterate_period (f o g) x /\ 929 (y = FUNPOW (f o g) (p DIV 2) x) /\ 930 EVEN p ==> y IN fixes f s /\ (y = x <=> p = 0) *) 931(* Proof: 932 When p = 0, 933 y = FUNPOW (f o g) 0 x = x by FUNPOW_0 934 When p <> 0, 935 This is true by involute_involute_fix_orbit_fix_even_distinct 936*) 937Theorem involute_involute_fix_orbit_fix_even_distinct_iff: 938 !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 939 p = iterate_period (f o g) x /\ 940 (y = FUNPOW (f o g) (p DIV 2) x) /\ 941 EVEN p ==> y IN fixes f s /\ (y = x <=> p = 0) 942Proof 943 ntac 7 strip_tac >> 944 (Cases_on `p = 0` >> simp[]) >> 945 irule involute_involute_fix_orbit_fix_even_distinct >> 946 metis_tac[] 947QED 948 949(* Idea: when f fixes x, and (f o g) has odd period p for x, 950 then g fixes (f o g)^(p/2) x, which, if p <> 1, is not x itself. *) 951 952(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 953 p = iterate_period (f o g) x /\ 954 (y = FUNPOW (f o g) (p DIV 2) x) /\ 955 ODD p ==> y IN fixes g s /\ (1 < p ==> y <> x) *) 956(* Proof: 957 Note y IN fixes g s by involute_involute_fix_orbit_fix_odd 958 Remains to show: y <> x. 959 By contradiction, suppose y = x. 960 Then p = 1 by involute_involute_fix_point 961 This contradicts 1 < p by given 962*) 963Theorem involute_involute_fix_orbit_fix_odd_distinct: 964 !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 965 p = iterate_period (f o g) x /\ 966 (y = FUNPOW (f o g) (p DIV 2) x) /\ 967 ODD p ==> y IN fixes g s /\ (1 < p ==> y <> x) 968Proof 969 ntac 7 strip_tac >> 970 drule_then strip_assume_tac involute_involute_fix_orbit_fix_odd >> 971 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`] strip_assume_tac) >> 972 `y IN fixes g s` by fs[] >> 973 (rpt strip_tac >> simp[]) >> 974 assume_tac involute_involute_fixes_both >> 975 last_x_assum (qspecl_then [`f`, `g`, `s`, `p`, `x`] strip_assume_tac) >> 976 `p = 1` by fs[] >> 977 decide_tac 978QED 979 980(* Another version of involute_involute_fix_orbit_fix_odd_distinct *) 981 982(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 983 p = iterate_period (f o g) x /\ 984 (y = FUNPOW (f o g) (p DIV 2) x) /\ 985 ODD p ==> y IN fixes g s /\ (y = x <=> p = 1) *) 986(* Proof: 987 Note y IN fixes g s by involute_involute_fix_orbit_fix_odd 988 When p = 1, 989 y = FUNPOW (f o g) 0 x = x by FUNPOW_0 990 When p <> 1, 1 < p, 991 Hence true by involute_involute_fix_orbit_fix_odd_distinct 992*) 993Theorem involute_involute_fix_orbit_fix_odd_distinct_iff: 994 !f g s p x y. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 995 p = iterate_period (f o g) x /\ 996 (y = FUNPOW (f o g) (p DIV 2) x) /\ 997 ODD p ==> y IN fixes g s /\ (y = x <=> p = 1) 998Proof 999 ntac 7 strip_tac >> 1000 assume_tac involute_involute_fix_orbit_fix_odd_distinct >> 1001 last_x_assum (qspecl_then [`f`, `g`, `s`, `p`, `x`, `y`] strip_assume_tac) >> 1002 (Cases_on `p = 1` >> simp[]) >> 1003 `x IN s` by fs[fixes_element] >> 1004 `(f o g) PERMUTES s` by rw[involute_involute_permutes] >> 1005 `0 < p` by metis_tac[iterate_period_pos] >> 1006 rfs[] 1007QED 1008 1009(* Idea: if f fixes just a single x, then period of (f o g) for x must be odd. *) 1010 1011(* Theorem: FINITE s /\ f involute s /\ g involute s /\ fixes f s = {x} /\ 1012 p = iterate_period (f o g) x ==> ODD p *) 1013(* Proof: 1014 Let y = FUNPOW (f o g) (p DIV 2) x, 1015 and a = fixes f s. 1016 By contradiction, suppose ~ODD p. 1017 Then EVEN p by ODD_EVEN 1018 Note x IN a by IN_SING 1019 Thus y IN a /\ y <> x by involute_involute_fix_orbit_fix_even_distinct 1020 But y = x by IN_SING 1021 Hence this is a contradiction. 1022*) 1023Theorem involute_involute_fix_sing_period_odd: 1024 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1025 fixes f s = {x} /\ p = iterate_period (f o g) x ==> ODD p 1026Proof 1027 spose_not_then strip_assume_tac >> 1028 qabbrev_tac `p = iterate_period (f o g) x` >> 1029 qabbrev_tac `y = FUNPOW (f o g) (p DIV 2) x` >> 1030 drule_then strip_assume_tac involute_involute_fix_orbit_fix_even_distinct >> 1031 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`, `y`] strip_assume_tac) >> 1032 qabbrev_tac `a = fixes f s` >> 1033 `x IN a` by fs[] >> 1034 `y IN a /\ y <> x` by rfs[ODD_EVEN] >> 1035 metis_tac[IN_SING] 1036QED 1037 1038(* Idea: for j <= p, apply f to the j-th iterate equals to the (p-j)-th iterate. *) 1039 1040(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1041 p = iterate_period (f o g) x ==> 1042 !j. j <= p ==> f (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - j) x *) 1043(* Proof: 1044 Note (f o g) PERMUTES s by involute_involute_permutes 1045 and x IN s by fixes_element 1046 so 0 < p by iterate_period_pos 1047 Let i = p - j. 1048 then i + j = p, 1049 or (i + j) MOD p = 0 by DIVMOD_ID, 0 < p 1050 so f (FUNPOW (f o g) j x) 1051 = FUNPOW (f o g) i x by involute_involute_fix_orbit_1 1052*) 1053Theorem involute_involute_fix_iterates_1: 1054 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1055 x IN fixes f s /\ p = iterate_period (f o g) x ==> 1056 !j. j <= p ==> f (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - j) x 1057Proof 1058 rpt strip_tac >> 1059 `p = p - j + j` by decide_tac >> 1060 qabbrev_tac `i = p - j` >> 1061 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 1062 `0 < p` by metis_tac[fixes_element, iterate_period_pos] >> 1063 `(i + j) MOD p = 0` by rw[] >> 1064 drule_then strip_assume_tac involute_involute_fix_orbit_1 >> 1065 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `i`, `j`] strip_assume_tac) >> 1066 rfs[] 1067QED 1068 1069(* Idea: for j < p, apply g to the j-th iterate equals to the (p-1-j)-th iterate. *) 1070 1071(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1072 p = iterate_period (f o g) x ==> 1073 !j. j < p ==> g (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - 1 - j) x *) 1074(* Proof: 1075 Note (f o g) PERMUTES s by involute_involute_permutes 1076 and x IN s by fixes_element 1077 so 0 < p by iterate_period_pos 1078 Let i = p - (j + 1). 1079 then i + j + 1 = p, 1080 or (i + j + 1) MOD p = 0 by DIVMOD_ID, 0 < p 1081 so g (FUNPOW (f o g) j x) 1082 = FUNPOW (f o g) i x by involute_involute_fix_orbit_2 1083*) 1084Theorem involute_involute_fix_iterates_2: 1085 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1086 x IN fixes f s /\ p = iterate_period (f o g) x ==> 1087 !j. j < p ==> g (FUNPOW (f o g) j x) = FUNPOW (f o g) (p - 1 - j) x 1088Proof 1089 rpt strip_tac >> 1090 `p = p - (j + 1) + j + 1` by decide_tac >> 1091 qabbrev_tac `i = p - (j + 1)` >> 1092 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 1093 `0 < p` by metis_tac[fixes_element, iterate_period_pos] >> 1094 `(i + j + 1) MOD p = 0` by rw[] >> 1095 drule_then strip_assume_tac involute_involute_fix_orbit_2 >> 1096 last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `i`, `j`] strip_assume_tac) >> 1097 rfs[] 1098QED 1099 1100(* Idea: for even period, the only f fixed point is at the midpoint. *) 1101 1102(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1103 p = iterate_period (f o g) x /\ EVEN p ==> 1104 !j. 0 < j /\ j < p ==> (FUNPOW (f o g) j x IN fixes f s <=> j = p DIV 2) *) 1105(* Proof: 1106 Note (f o g) PERMUTES s by involute_involute_permutes 1107 and x IN s by fixes_element 1108 so 0 < p by iterate_period_pos, or just by 0 < j < p 1109 Let y = FUNPOW (f o g) j x. 1110 then y IN s by FUNPOW_closure, x IN s 1111 Note j < p, so 0 < p - j < p. 1112 y IN fixes f s 1113 <=> f y = y by fixes_element 1114 <=> FUNPOW (f o g) (p - j) x = FUNPOW (f o g) j x 1115 by involute_involute_fix_iterates_1, j < p 1116 <=> p - j MOD p = j MOD p by iterate_period_mod_eq 1117 <=> p - j = j by LESS_MOD, p - j < p, j < p 1118 <=> 2 * j = p by arithmetic 1119 <=> 2 * j = 2 * p DIV 2 by EVEN_HALF, EVEN p 1120 <=> j = p DIV 2 by EQ_MULT_LCANCEL 1121*) 1122Theorem involute_involute_fix_even_period_fix: 1123 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1124 x IN fixes f s /\ p = iterate_period (f o g) x /\ EVEN p ==> 1125 !j. 0 < j /\ j < p ==> 1126 (FUNPOW (f o g) j x IN fixes f s <=> j = p DIV 2) 1127Proof 1128 rpt strip_tac >> 1129 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 1130 qabbrev_tac `y = FUNPOW (f o g) j x` >> 1131 `x IN s` by fs[fixes_element] >> 1132 `y IN s` by fs[FUNPOW_closure, Abbr`y`] >> 1133 drule_then strip_assume_tac involute_involute_fix_iterates_1 >> 1134 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`, `j`] strip_assume_tac) >> 1135 drule_then strip_assume_tac (iterate_period_mod_eq |> ISPEC ``(f:'a -> 'a) o (g:'a -> 'a)``) >> 1136 last_x_assum (qspecl_then [`g`, `f`, `p`, `x`, `p-j`, `j`] strip_assume_tac) >> 1137 rfs[] >> 1138 `p - j < p` by decide_tac >> 1139 `y IN fixes f s <=> f y = y` by metis_tac[fixes_element] >> 1140 `_ = ((p - j) MOD p = j MOD p)` by rfs[] >> 1141 `_ = (p - j = j)` by rw[LESS_MOD] >> 1142 `_ = (p = 2 * j)` by decide_tac >> 1143 metis_tac[EVEN_HALF, EQ_MULT_LCANCEL, DECIDE``2 <> 0``] 1144QED 1145 1146(* Idea: for odd period, the only g fixed point is at the midpoint. *) 1147 1148(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1149 p = iterate_period (f o g) x /\ ODD p ==> 1150 !j. 0 < j /\ j < p ==> (FUNPOW (f o g) j x IN fixes g s <=> j = p DIV 2) *) 1151(* Proof: 1152 Note (f o g) PERMUTES s by involute_involute_permutes 1153 and x IN s by fixes_element 1154 so 0 < p by iterate_period_pos, or just by 0 < j < p 1155 Let y = FUNPOW (f o g) j x. 1156 then y IN s by FUNPOW_closure, x IN s 1157 Note j < p, so 0 < p - 1 - j < p. 1158 y IN fixes g s 1159 <=> g y = y by fixes_element 1160 <=> FUNPOW (f o g) (p - 1 - j) x = FUNPOW (f o g) j x 1161 by involute_involute_fix_iterates_2, j < p 1162 <=> p - 1 - j MOD p = j MOD p by iterate_period_mod_eq 1163 <=> p - 1 - j = j by LESS_MOD, p - 1 - j < p, j < p 1164 <=> 2 * j + 1 = p by arithmetic 1165 <=> 2 * j + 1 = 2 * p DIV 2 + 1 by ODD_HALF 1166 <=> j = p DIV 2 by EQ_MULT_LCANCEL 1167*) 1168Theorem involute_involute_fix_odd_period_fix: 1169 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1170 x IN fixes f s /\ p = iterate_period (f o g) x /\ ODD p ==> 1171 !j. 0 < j /\ j < p ==> 1172 (FUNPOW (f o g) j x IN fixes g s <=> j = p DIV 2) 1173Proof 1174 rpt strip_tac >> 1175 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 1176 qabbrev_tac `y = FUNPOW (f o g) j x` >> 1177 `x IN s` by fs[fixes_element] >> 1178 `y IN s` by fs[FUNPOW_closure, Abbr`y`] >> 1179 drule_then strip_assume_tac involute_involute_fix_iterates_2 >> 1180 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`, `j`] strip_assume_tac) >> 1181 drule_then strip_assume_tac (iterate_period_mod_eq |> ISPEC ``(f:'a -> 'a) o (g:'a -> 'a)``) >> 1182 last_x_assum (qspecl_then [`g`, `f`, `p`, `x`, `p - 1 -j`, `j`] strip_assume_tac) >> 1183 rfs[] >> 1184 `p - 1 - j < p` by decide_tac >> 1185 `y IN fixes g s <=> g y = y` by metis_tac[fixes_element] >> 1186 `_ = ((p - 1 - j) MOD p = j MOD p)` by rfs[] >> 1187 `_ = (p - 1 - j = j)` by rw[LESS_MOD] >> 1188 `_ = (p = 2 * j + 1)` by decide_tac >> 1189 metis_tac[ODD_HALF, EQ_MONO_ADD_EQ, EQ_MULT_LCANCEL, DECIDE``2 <> 0``] 1190QED 1191 1192(* ------------------------------------------------------------------------- *) 1193(* Iteration Mate Involution. *) 1194(* ------------------------------------------------------------------------- *) 1195 1196(* Idea: an involution for the mapping of fixed points. *) 1197 1198(* For EVEN period, say 6, orbit: [x, f x, f^2 x, f^3 x, f^4 x, f^5 x] 1199 The middle one is slightly right: f^3 x, HALF 6 = 3, which is f^(p-3) x. 1200 For ODD period, say 7, orbit: [x, f x, f^2 x, f^3 x, f^4 x, f^5 x, f^6 x] 1201 The middle one is exactly at center: f^3 x, HALF 7 = 3, which is f^(p-1-3) x. 1202 1203 This means, for p = iterate_period (f o g) x, 1204 if start from (fixes f s), 1205 then even period ==> iterate_mate (f o g) x IN fixes f s, 1206 and odd period ==> iterate_mate (f o g) x IN fixes g s. 1207 if start from (fixes g s), 1208 then even period ==> iterate_mate (g o f) x IN fixes g s, 1209 and iterate_mate (g o f) x = iterate_mate (f o g) x when even 1210 and odd period ==> iterate_mate (g o f) x IN fixes f s. 1211 but iterate_mate (g o f) x <> iterate_mate (f o g) x 1212 because iterate_mate (g o f) x = FUNPOW (f o g) (1 + HALF p) x 1213 All these mean: 1214 if even period, iterate_mate (f o g) (iterate_mate (f o g) x) = x, by 3 + 3 = 6. 1215 if odd period, to have the same equality, iterate_mate is tricky to define! 1216*) 1217 1218(* Define the iterate mate, pairing up with middle iterate, for composite. *) 1219Definition iterate_mate_def: 1220 iterate_mate f g x = 1221 let h = (iterate_period (f o g) x) DIV 2 (* half period *) 1222 in if f x = x then FUNPOW (f o g) h x (* walk by (f o g) *) 1223 else if g x = x then FUNPOW (g o f) h x (* walk by (g o f) *) 1224 else x (* don't care, better just be yourself. *) 1225End 1226 1227(* Idea: the mate is an element of the set. *) 1228 1229(* Theorem: f involute s /\ g involute s /\ x IN s ==> iterate_mate f g x IN s *) 1230(* Proof: 1231 Note f o g PERMUTES s by involute_involute_permutes 1232 and g o f PERMUTES s by involute_involute_permutes 1233 Thus iterate_mate f g x IN s by iterate_mate_def, FUNPOW_closure 1234*) 1235Theorem iterate_mate_element: 1236 !f g s x. f involute s /\ g involute s /\ x IN s ==> 1237 iterate_mate f g x IN s 1238Proof 1239 rpt strip_tac >> 1240 `f o g PERMUTES s /\ g o f PERMUTES s` by rw[involute_involute_permutes] >> 1241 rw[iterate_mate_def, FUNPOW_closure] 1242QED 1243 1244(* Idea: the reverse of a mate is the mate itself. *) 1245 1246(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 1247 iterate_mate g f x = iterate_mate f g x *) 1248(* Proof: 1249 Let p = iterate_period (f o g) x, 1250 q = iterate_period (g o f) x. 1251 Then p = q by involute_involute_period_inv 1252 1253 If f x = x /\ g x = x, 1254 Then x IN fixes f s by fixes_element 1255 and x IN fixes g s by fixes_element 1256 so p = 1 by involute_involute_fixes_both 1257 iterate_mate g f x 1258 = FUNPOW (f o g) (HALF q) x by iterate_mate_def 1259 = FUNPOW (f o g) 0 x by q = 1 1260 = FUNPOW (g o f) 0 x by FUNPOW_0 1261 = FUNPOW (g o f) (HALF p) x by p = 1 1262 = iterate_mate f g x by iterate_mate_def 1263 If f x = x, g x <> x 1264 iterate_mate g f x 1265 = FUNPOW (f o g) (HALF q) x by iterate_mate_def 1266 = FUNPOW (f o g) (HALF p) x by q = p 1267 = iterate_mate f g x by iterate_mate_def 1268 If g x = x, f x <> x 1269 iterate_mate g f x 1270 = FUNPOW (g o f) (HALF q) x by iterate_mate_def 1271 = FUNPOW (g o f) (HALF p) x by q = p 1272 = iterate_mate f g x by iterate_mate_def 1273*) 1274Theorem iterate_mate_reverse: 1275 !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 1276 iterate_mate g f x = iterate_mate f g x 1277Proof 1278 simp[iterate_mate_def] >> 1279 rpt strip_tac >> 1280 qabbrev_tac `p = iterate_period (f o g) x` >> 1281 qabbrev_tac `q = iterate_period (g o f) x` >> 1282 drule_then strip_assume_tac involute_involute_period_inv >> 1283 last_x_assum (qspecl_then [`f`, `g`, `x`] strip_assume_tac) >> 1284 `p = q` by rfs[] >> 1285 rw[] >> 1286 qabbrev_tac `h = HALF p` >> 1287 `x IN fixes f s /\ x IN fixes g s` by fs[fixes_element] >> 1288 drule_then strip_assume_tac involute_involute_fixes_both >> 1289 last_x_assum (qspecl_then [`f`, `p`, `x`] strip_assume_tac) >> 1290 `p = 1` by rw[] >> 1291 simp[Abbr`h`] 1292QED 1293 1294(* Idea: the mate of a mate is itself. *) 1295 1296(* First, when x IN fixes f s, then prove this situation. *) 1297 1298(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s ==> 1299 iterate_mate f g (iterate_mate f g x) = x *) 1300(* Proof: 1301 Let p = iterate_period (f o g) x, h = HALF p. 1302 Given x IN fixes f s, 1303 so x IN s /\ f x = x by fixes_element 1304 Let y = FUNPOW (f o g) h x. 1305 Note (f o g) PERMUTES s by involute_involute_permutes 1306 so p = iterate_period (f o g) y by iterate_period_iterate 1307 1308 If EVEN p, 1309 Then y IN fixes f s by involute_involute_fix_orbit_fix_even 1310 so y IN s /\ f y = y by fixes_element 1311 iterate_mate f g (iterate_mate f g x) 1312 = iterate_mate f g y by iterate_mate_def, f x = x 1313 = FUNPOW (f o g) h y by iterate_mate_def, f y = y 1314 = FUNPOW (f o g) h (FUNPOW (f o g) h x) 1315 = FUNPOW (f o g) (h + h) x by FUNPOW_ADD 1316 = FUNPOW (f o g) p x by EVEN_HALF 1317 = x by iterate_period_property 1318 1319 If ~EVEN p, then ODD p by ODD_EVEN 1320 Then y IN fixes g s by involute_involute_fix_orbit_fix_odd 1321 so y IN s /\ g y = y by fixes_element 1322 Note p = iterate_period (g o f) y by involute_involute_period_inv 1323 If f y = y, 1324 Then y IN fixes f s by fixes_element 1325 so p = 1 by involute_involute_fixes_both 1326 iterate_mate f g (iterate_mate f g x) 1327 = iterate_mate f g y by iterate_mate_def, f x = x 1328 = FUNPOW (f o g) h y by iterate_mate_def, f y = y 1329 = FUNPOW (f o g) 0 y by h = HALF 1 = 0 1330 = y by FUNPOW_0 1331 = FUNPOW (f o g) 0 x by y = FUNPOW (f o g) h x 1332 = x 1333 If f y <> y, 1334 Note h + h + 1 = p by ODD_HALF 1335 so (h + h + 1) MOD p = 0 by DIVMOD_ID, 0 < p 1336 iterate_mate f g (iterate_mate f g x) 1337 = iterate_mate f g y by iterate_mate_def, f x = x 1338 = FUNPOW (g o f) h y by iterate_mate_def, f y <> y 1339 = FUNPOW (f o g) (h + 1) y by iterate_involute_mod_period 1340 = FUNPOW (f o g) (h + 1) (FUNPOW (f o g) h x) 1341 = FUNPOW (f o g) (h + 1 + h) x by FUNPOW_ADD 1342 = FUNPOW (f o g) p x by above 1343 = x by iterate_period_property 1344*) 1345Theorem iterate_mate_fixes_mate: 1346 !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s ==> 1347 iterate_mate f g (iterate_mate f g x) = x 1348Proof 1349 simp[iterate_mate_def] >> 1350 rpt strip_tac >> 1351 qabbrev_tac `p = iterate_period (f o g) x` >> 1352 `x IN s /\ f x = x` by fs[fixes_element] >> 1353 simp[] >> 1354 qabbrev_tac `y = FUNPOW (f o g) (HALF p) x` >> 1355 `(f o g) PERMUTES s` by rw[involute_involute_permutes] >> 1356 `iterate_period (f o g) y = p` by metis_tac[iterate_period_iterate] >> 1357 Cases_on `EVEN p` >| [ 1358 `y IN fixes f s` by fs[involute_involute_fix_orbit_fix_even, Abbr`p`, Abbr`y`] >> 1359 `y IN s /\ f y = y` by fs[fixes_element] >> 1360 simp[] >> 1361 qabbrev_tac `h = p DIV 2` >> 1362 `h + h = p` by rw[EVEN_HALF, Abbr`h`] >> 1363 `FUNPOW (f o g) h y = FUNPOW (f o g) (h + h) x` by rw[FUNPOW_ADD, Abbr`y`] >> 1364 `_ = x` by rw[iterate_period_property, Abbr`p`] >> 1365 simp[], 1366 `ODD p` by rw[ODD_EVEN] >> 1367 `y IN fixes g s` by fs[involute_involute_fix_orbit_fix_odd, Abbr`p`, Abbr`y`] >> 1368 `y IN s /\ g y = y` by fs[fixes_element] >> 1369 simp[] >> 1370 drule_then strip_assume_tac involute_involute_period_inv >> 1371 last_x_assum (qspecl_then [`f`, `g`, `y`] strip_assume_tac) >> 1372 `p = iterate_period (g o f) y` by rw[Abbr`p`] >> 1373 (Cases_on `f y = y` >> rfs[]) >| [ 1374 `y IN fixes f s` by rw[fixes_element] >> 1375 drule_then strip_assume_tac involute_involute_fixes_both >> 1376 last_x_assum (qspecl_then [`f`, `p`, `y`] strip_assume_tac) >> 1377 `p = 1` by rw[] >> 1378 simp[Abbr`y`], 1379 qabbrev_tac `h = p DIV 2` >> 1380 `h + h + 1 = p` by rw[ODD_HALF, Abbr`h`] >> 1381 `(h + h + 1) MOD p = 0` by fs[DIVMOD_ID] >> 1382 drule_then strip_assume_tac iterate_involute_mod_period >> 1383 last_x_assum (qspecl_then [`g`, `f`, `y`, `p`, `h`, `h+1`] strip_assume_tac) >> 1384 `FUNPOW (g o f) h y = FUNPOW (f o g) (h + 1) y` by rfs[] >> 1385 `_ = FUNPOW (f o g) (h + 1 + h) x` by fs[FUNPOW_ADD, Abbr`y`] >> 1386 `_ = x` by rfs[iterate_period_property, Abbr`p`] >> 1387 simp[] 1388 ] 1389 ] 1390QED 1391 1392(* Idea: the mate of a mate is itself. *) 1393 1394(* Now, remove x IN fixes f s condition. *) 1395 1396(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 1397 iterate_mate f g (iterate_mate f g x) = x *) 1398(* Proof: 1399 If x IN fixes f s, 1400 Then iterate_mate f g (iterate_mate f g x) = x 1401 by iterate_mate_fixes_mate 1402 else if x IN fixes g s, 1403 Note iterate_mate g f x IN s by iterate_mate_element 1404 iterate_mate f g (iterate_mate f g x) 1405 = iterate_mate f g (iterate_mate g f x) by iterate_mate_reverse 1406 = iterate_mate g f (iterate_mate g f x) by iterate_mate_reverse 1407 = x by iterate_mate_fixes_mate 1408 Otherwise, f x <> x and g x <> x by fixes_element 1409 iterate_mate f g (iterate_mate f g x) 1410 = iterate_mate f g x by iterate_mate_def 1411 = x by iterate_mate_def 1412*) 1413Theorem iterate_mate_mate: 1414 !f g s x. FINITE s /\ f involute s /\ g involute s /\ x IN s ==> 1415 iterate_mate f g (iterate_mate f g x) = x 1416Proof 1417 rpt strip_tac >> 1418 drule_then strip_assume_tac iterate_mate_fixes_mate >> 1419 Cases_on `x IN fixes f s` >| [ 1420 last_x_assum (qspecl_then [`f`, `g`, `x`] strip_assume_tac) >> 1421 fs[], 1422 Cases_on `x IN fixes g s` >| [ 1423 last_x_assum (qspecl_then [`g`, `f`, `x`] strip_assume_tac) >> 1424 qabbrev_tac `y = iterate_mate g f x` >> 1425 `y IN s` by rw[iterate_mate_element, Abbr`y`] >> 1426 drule_then strip_assume_tac iterate_mate_reverse >> 1427 last_x_assum (qspecl_then [`f`, `g`] strip_assume_tac) >> 1428 `iterate_mate f g (iterate_mate f g x) = iterate_mate f g y` by rfs[Abbr`y`] >> 1429 first_x_assum (qspecl_then [`y`] strip_assume_tac) >> 1430 rfs[], 1431 `f x <> x /\ g x <> x` by rfs[fixes_element] >> 1432 simp[iterate_mate_def] 1433 ] 1434 ] 1435QED 1436 1437(* Idea: if x is a fixed point, its mate is also a fixed point. *) 1438 1439(* Theorem: FINITE s /\ f involute s /\ g involute s /\ 1440 x IN (fixes f s UNION fixes g s) ==> 1441 iterate_mate f g x IN (fixes f s UNION fixes g s) *) 1442(* Proof: 1443 Let p = iterate_period (f o g) x, h = HALF p. 1444 If x IN fixes f s, 1445 Then x IN s /\ f x = x by fixes_element 1446 Let y = FUNPOW (f o g) h x. 1447 so iterate_mate f g x = y by iterate_mate_def 1448 If EVEN p, 1449 then y IN fixes f s by involute_involute_fix_orbit_fix_even 1450 If ~EVEN p, then ODD p by ODD_EVEN 1451 and y IN fixes g s by involute_involute_fix_orbit_fix_odd 1452 1453 If x IN fixes g s, 1454 Then x IN s /\ g x = x by fixes_element 1455 and p = iterate_period (g o f) x by involute_involute_period_inv 1456 1457 If f x = x, 1458 Let y = FUNPOW (f o g) h x. 1459 so iterate_mate f g x = y by iterate_mate_def 1460 But x IN fixes f s by fixes_element 1461 so p = 1 by involute_involute_fixes_both 1462 ==> h = 0 by h = HALF p 1463 Thus y = x by FUNPOW_0 1464 and x IN fixes g s by given case 1465 1466 If f x <> x, 1467 Let y = FUNPOW (g o h) h x. 1468 so iterate_mate f g x = y by iterate_mate_def 1469 If EVEN p, 1470 then y IN fixes g s by involute_involute_fix_orbit_fix_even 1471 If ~EVEN p, then ODD p by ODD_EVEN 1472 and y IN fixes f s by involute_involute_fix_orbit_fix_odd 1473*) 1474Theorem iterate_mate_fixes_mate_fixes: 1475 !f g s x. FINITE s /\ f involute s /\ g involute s /\ 1476 x IN (fixes f s UNION fixes g s) ==> 1477 iterate_mate f g x IN (fixes f s UNION fixes g s) 1478Proof 1479 simp[iterate_mate_def] >> 1480 ntac 4 strip_tac >> 1481 qabbrev_tac `p = iterate_period (f o g) x` >> 1482 strip_tac >| [ 1483 `x IN s /\ f x = x` by fs[fixes_element] >> 1484 simp[] >> 1485 Cases_on `EVEN p` >- 1486 fs[involute_involute_fix_orbit_fix_even, Abbr`p`] >> 1487 fs[involute_involute_fix_orbit_fix_odd, ODD_EVEN, Abbr`p`], 1488 `x IN s /\ (g x = x)` by fs[fixes_element] >> 1489 simp[] >> 1490 drule_then strip_assume_tac involute_involute_period_inv >> 1491 last_x_assum (qspecl_then [`f`, `g`, `x`] strip_assume_tac) >> 1492 `p = iterate_period (g o f) x` by rw[Abbr`p`] >> 1493 (Cases_on `f x = x` >> rfs[]) >| [ 1494 `x IN fixes f s` by rw[fixes_element] >> 1495 drule_then strip_assume_tac involute_involute_fixes_both >> 1496 last_x_assum (qspecl_then [`f`, `p`, `x`] strip_assume_tac) >> 1497 `p = 1` by rw[] >> 1498 simp[], 1499 Cases_on `EVEN p` >- 1500 fs[involute_involute_fix_orbit_fix_even, Abbr`p`] >> 1501 fs[involute_involute_fix_orbit_fix_odd, ODD_EVEN, Abbr`p`] 1502 ] 1503 ] 1504QED 1505 1506(* Idea: mate is an involution on all the fixes. *) 1507 1508(* Theorem: FINITE s /\ f involute s /\ g involute s ==> 1509 (iterate_mate f g) involute ((fixes f s) UNION (fixes g s)) *) 1510(* Proof: 1511 This is to show: 1512 (1) x IN fixes f s UNION fixes g s ==> 1513 iterate_mate f g x IN fixes f s UNION fixes g s 1514 This is true by iterate_mate_fixes_mate_fixes 1515 (2) x IN fixes f s UNION fixes g s ==> 1516 iterate_mate f g (iterate_mate f g x) = x 1517 Note x IN s by fixes_element 1518 Hence true by iterate_mate_mate 1519*) 1520Theorem iterate_mate_involute_fixes: 1521 !f g s. FINITE s /\ f involute s /\ g involute s ==> 1522 (iterate_mate f g) involute ((fixes f s) UNION (fixes g s)) 1523Proof 1524 rpt strip_tac >- 1525 rw[iterate_mate_fixes_mate_fixes] >> 1526 `x IN s` by fs[fixes_element] >> 1527 drule_then strip_assume_tac iterate_mate_mate >> 1528 last_x_assum (qspecl_then [`f`, `g`, `x`] strip_assume_tac) >> 1529 simp[] 1530QED 1531 1532(* ------------------------------------------------------------------------- *) 1533(* Using direct WHILE. *) 1534(* ------------------------------------------------------------------------- *) 1535 1536(* Idea: a WHILE loop with involutions goes from fixed point to fixed point. *) 1537 1538(* Note: 1539 1540involute_involute_fix_odd_period_fix 1541|- !f g s p x. 1542 FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1543 p = iterate_period (f o g) x /\ ODD p ==> 1544 !j. 1545 0 < j /\ j < p ==> 1546 (FUNPOW (f o g) j x IN fixes g s <=> (j = HALF p)) 1547 1548iterate_while_thm 1549|- !g b x k. 1550 (!j. j < k ==> g (FUNPOW b j x)) /\ ~g (FUNPOW b k x) ==> 1551 (WHILE g b x = FUNPOW b k x) 1552*) 1553 1554(* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ 1555 p = iterate_period (f o g) x /\ ODD p ==> 1556 WHILE (\y. g y <> y) (f o g) x IN fixes g s *) 1557(* Proof: 1558 Let b = \y. g y <> y, 1559 The goal is: WHILE b (f o g) x IN fixes g s 1560 1561 If p = 1, 1562 Then x IN fixes g s by involute_involute_fixes_both 1563 so ~b x by fixes_element 1564 WHILE b (f o g) x 1565 = x by iterate_while_thm_0, ~b x 1566 and x IN fixes g s by above 1567 1568 If p <> 1, 1569 Let h = HALF p, 1570 z = FUNPOW (f o g) h x. 1571 Then h <> 0 by HALF_EQ_0, p <> 0, p <> 1 1572 and h < p by HALF_LESS, p <> 0 1573 Note (f o g) PERMUTES s by involute_involute_permutes 1574 and p <> 0 by given ODD p 1575 and z IN fixes g s by involute_involute_fix_orbit_fix_odd [1] 1576 Thus ~b z by fixes_element [2] 1577 1578 Claim: !j. j < h ==> b (FUNPOW (f o g) j x) [3] 1579 Proof: Let y = FUNPOW (f o g) j x, to show: b y. 1580 Note x IN s by fixes_element 1581 so y IN s by FUNPOW_closure 1582 If j = 0, 1583 then y = x by FUNPOW_0 1584 and y NOTIN fixes g s by involute_involute_fixes_both, p <> 1 1585 or b y by fixes_element 1586 If j <> 0, 1587 then 0 < j /\ j < p by j < h, h < p 1588 so y NOTIN fixes g s by involute_involute_fix_odd_period_fix, j <> h 1589 or b y by fixes_element 1590 1591 Thus WHILE b (f o g) x = z by iterate_while_thm, [3], [2] 1592 and z IN fixes g s by [1] 1593*) 1594Theorem involute_involute_fix_odd_period_fix_while: 1595 !f g s p x. FINITE s /\ f involute s /\ g involute s /\ 1596 x IN fixes f s /\ p = iterate_period (f o g) x /\ ODD p ==> 1597 WHILE (\y. g y <> y) (f o g) x IN fixes g s 1598Proof 1599 rpt strip_tac >> 1600 qabbrev_tac `b = \y. g y <> y` >> 1601 Cases_on `p = 1` >| [ 1602 assume_tac involute_involute_fixes_both >> 1603 last_x_assum (qspecl_then [`f`, `g`, `s`, `p`, `x`] strip_assume_tac) >> 1604 `x IN fixes g s` by rfs[] >> 1605 `~b x` by rfs[fixes_element, Abbr`b`] >> 1606 simp[iterate_while_thm_0], 1607 `f o g PERMUTES s` by rw[involute_involute_permutes] >> 1608 drule_then strip_assume_tac involute_involute_fix_orbit_fix_odd >> 1609 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`] strip_assume_tac) >> 1610 qabbrev_tac `h = HALF p` >> 1611 qabbrev_tac `z = FUNPOW (f o g) h x` >> 1612 `z IN fixes g s` by rfs[] >> 1613 `~b z` by rfs[fixes_element, Abbr`b`] >> 1614 `!j. j < h ==> b (FUNPOW (f o g) j x)` by 1615 (rpt strip_tac >> 1616 (Cases_on `j = 0` >> simp[]) >| [ 1617 spose_not_then strip_assume_tac >> 1618 `x IN fixes g s` by rfs[fixes_element, Abbr`b`] >> 1619 assume_tac involute_involute_fixes_both >> 1620 last_x_assum (qspecl_then [`f`, `g`, `s`, `p`, `x`] strip_assume_tac) >> 1621 rfs[], 1622 `p <> 0` by metis_tac[EVEN, ODD_EVEN] >> 1623 `h < p` by rw[HALF_LESS, Abbr`h`] >> 1624 spose_not_then strip_assume_tac >> 1625 qabbrev_tac `y = FUNPOW (f o g) j x` >> 1626 `y IN s` by rfs[fixes_element, FUNPOW_closure, Abbr`y`] >> 1627 `y IN fixes g s` by rfs[fixes_element, Abbr`b`] >> 1628 drule_then strip_assume_tac involute_involute_fix_odd_period_fix >> 1629 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`] strip_assume_tac) >> 1630 `0 < j /\ j < p` by decide_tac >> 1631 `j = h` by metis_tac[] >> 1632 decide_tac 1633 ]) >> 1634 drule_then strip_assume_tac involute_involute_fix_orbit_fix_odd >> 1635 last_x_assum (qspecl_then [`f`, `g`, `p`, `x`] strip_assume_tac) >> 1636 assume_tac iterate_while_thm >> 1637 last_x_assum (qspecl_then [`b`, `f o g`, `x`, `h`] strip_assume_tac) >> 1638 rfs[] 1639 ] 1640QED 1641 1642 1643(* ------------------------------------------------------------------------- *) 1644 1645(* export theory at end *) 1646val _ = export_theory(); 1647 1648(*===========================================================================*) 1649