1(* ------------------------------------------------------------------------- *) 2(* Involution and Action *) 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 "involuteAction"; 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 "involuteTheory"; *) 28open involuteTheory; 29 30(* val _ = load "groupInstancesTheory"; *) 31open groupInstancesTheory; (* for Zadd_def *) 32 33(* val _ = load "groupActionTheory"; *) 34open groupActionTheory; (* for fixed_points_def *) 35 36 37(* ------------------------------------------------------------------------- *) 38(* Involution and Action Documentation *) 39(* ------------------------------------------------------------------------- *) 40(* 41 42 FUNPOW Action: 43 funpow_action |- !f X. f involute X ==> (Z2 act X) (FUNPOW f) 44 funpow_reach |- !f x y. reach (FUNPOW f) Z2 x y <=> ?a. a < 2 /\ FUNPOW f a x = y 45 funpow_equiv |- !f X. f involute X ==> reach (FUNPOW f) Z2 equiv_on X 46 47 FUNPOW Orbits: 48 funpow_orbits |- !f X. orbits (FUNPOW f) Z2 X = IMAGE (orbit (FUNPOW f) Z2) X 49 funpow_orbit |- !f x. orbit (FUNPOW f) Z2 x = {FUNPOW f a x | a < 2} 50 funpow_orbit_alt|- !f x. orbit (FUNPOW f) Z2 x = IMAGE (\a. FUNPOW f a x) (count 2) 51 funpow_orbit_element 52 |- !f x y. y IN orbit (FUNPOW f) Z2 x <=> ?a. a < 2 /\ FUNPOW f a x = y 53 funpow_orbit_in_orbits 54 |- !f X x. x IN X ==> orbit (FUNPOW f) Z2 x IN orbits (FUNPOW f) Z2 X 55 funpow_orbit_finite 56 |- !f x. FINITE (orbit (FUNPOW f) Z2 x) 57 funpow_orbits_finite 58 |- !f X. FINITE X ==> FINITE (orbits (FUNPOW f) Z2 X) 59 funpow_multi_orbits_finite 60 |- !f X. FINITE X ==> FINITE (multi_orbits (FUNPOW f) Z2 X) 61 62 Involution Orbits: 63 involute_orbit_element 64 |- !f X x y. f involute X /\ x IN X /\ y IN orbit (FUNPOW f) Z2 x ==> 65 y = x \/ y = f x 66 involute_orbit_has_self 67 |- !f X x. f involute X /\ x IN X ==> x IN orbit (FUNPOW f) Z2 x 68 involute_orbit_has_funpow 69 |- !f X x n. f involute X /\ x IN X ==> 70 FUNPOW f n x IN orbit (FUNPOW f) Z2 x 71 involute_orbit_has_image 72 |- !f X x. f involute X /\ x IN X ==> f x IN orbit (FUNPOW f) Z2 x 73 involute_orbit_nonempty 74 |- !f X e. f involute X /\ e IN orbits (FUNPOW f) Z2 X ==> e <> {} 75 involute_orbits_element_is_orbit 76 |- !f X e x. f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ 77 x IN e ==> e = orbit (FUNPOW f) Z2 x 78 involute_orbits_element_element 79 |- !f X e x. f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ 80 x IN e ==> x IN X 81 82 Involution fixed points: 83 involute_fixed_points 84 |- !f X x. f involute X /\ 85 x IN fixed_points (FUNPOW f) Z2 X ==> f x = x 86 involute_fixed_points_iff 87 |- !f X x. f involute X /\ x IN X ==> 88 (x IN fixed_points (FUNPOW f) Z2 X <=> f x = x) 89 involute_fixed_points_element_element 90 |- !f X x. x IN fixed_points (FUNPOW f) Z2 X ==> x IN X 91 92 Involution Target Cardinality: 93 involute_target_card_by_types 94 |- !f X. FINITE X /\ f involute X ==> 95 CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + 96 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) 97 involute_target_card_eqn 98 |- !f X. FINITE X /\ f involute X ==> 99 (CARD A = CARD (fixed_points (FUNPOW f) Z2 X) + 100 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X)) 101 involute_orbit_fixed 102 |- !f X x. f involute X /\ x IN X /\ f x = x ==> 103 orbit (FUNPOW f) Z2 x = {x} 104 involute_orbit_not_fixed 105 |- !f X x. f involute X /\ x IN X /\ f x <> x ==> 106 orbit (FUNPOW f) Z2 x = {x; f x} 107 involute_multi_orbits_element_card 108 |- !f X e. f involute X /\ e IN multi_orbits (FUNPOW f) Z2 X ==> 109 CARD e = 2 110 involute_target_card_thm 111 |- !f X. FINITE X /\ f involute X ==> 112 CARD X = 2 * CARD (multi_orbits (FUNPOW f) Z2 X) + 113 CARD (fixed_points (FUNPOW f) Z2 X) 114 involute_fixed_points_both_even 115 |- !f X. FINITE X /\ f involute X ==> 116 (EVEN (CARD X) <=> EVEN (CARD (fixed_points (FUNPOW f) Z2 X))) 117 involute_fixed_points_both_odd 118 |- !f X. FINITE X /\ f involute X ==> 119 (ODD (CARD X) <=> ODD (CARD (fixed_points (FUNPOW f) Z2 X))) 120 involute_two_fixed_points_both_even 121 |- !f g X. FINITE X /\ f involute X /\ g involute X ==> 122 (EVEN (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 123 EVEN (CARD (fixed_points (FUNPOW g) Z2 X))) 124 involute_two_fixed_points_both_odd 125 |- !f g X. FINITE X /\ f involute X /\ g involute X ==> 126 (ODD (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 127 ODD (CARD (fixed_points (FUNPOW g) Z2 X))) 128*) 129 130(* ------------------------------------------------------------------------- *) 131(* Helper Theorems *) 132(* ------------------------------------------------------------------------- *) 133 134(* ------------------------------------------------------------------------- *) 135(* FUNPOW Action *) 136(* ------------------------------------------------------------------------- *) 137 138(* The group for involution action. *) 139val _ = overload_on("Z2", ``Zadd 2``); 140 141(* 142Zadd_property; 143|- !n. (!x. x IN (Zadd n).carrier <=> x < n) /\ (Zadd n).id = 0 /\ 144 (!x y. (Zadd n).op x y = (x + y) MOD n) /\ 145 FINITE (Zadd n).carrier /\ CARD (Zadd n).carrier = n 146*) 147 148(* Theorem: f involute X ==> (Z2 act X) (FUNPOW f) *) 149(* Proof: 150 By action_def, Zadd_property, this is to show: 151 (1) x IN X /\ a < 2 ==> FUNPOW f a x IN X 152 Note f PERMUTES X by involute_permutes 153 so FUNPOW f a x IN X by FUNPOW_closure 154 (2) x IN X /\ a < 2 /\ b < 2 ==> 155 FUNPOW f a (FUNPOW f b x) = FUNPOW f ((a + b) MOD 2) x 156 Note FUNPOW f a (FUNPOW f b x) 157 = FUNPOW f (a + b) x by FUNPOW_ADD 158 If a = 0, b = 0, a + b = 0 = 0 MOD 2. 159 If a = 0, b = 1, a + b = 1 = 1 MOD 2. 160 If a = 1, b = 0, a + b = 1 = 1 MOD 2. 161 If a = 1, b = 1, a + b = 2. 2 MOD 2 = 0. 162 The goal becomes: FUNPOW f 2 x = x 163 But FUNPOW f 2 x 164 = f (f x) by FUNPOW_2 165 = x by f involute X 166 = FUNPOW f 0 x by FUNPOW_0 167*) 168Theorem funpow_action: 169 !f X. f involute X ==> (Z2 act X) (FUNPOW f) 170Proof 171 rw[action_def, Zadd_property] >- 172 rw[involute_permutes, FUNPOW_closure] >> 173 `FUNPOW f a (FUNPOW f b x) = FUNPOW f (a + b) x` by rw[FUNPOW_ADD] >> 174 (`(a = 0 \/ a = 1) /\ (b = 0 \/ b = 1)` by decide_tac >> simp[]) >> 175 simp[FUNPOW_2] 176QED 177 178(* Adapt the general theory of group action to (FUNPOW f). *) 179(* Note: Eventually, X = mills n, a set of triples (x,y,z), f = zagier or f = flip. *) 180 181(* Extract theorems *) 182 183val funpow_reach = save_thm("funpow_reach", 184 reach_def |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` 185 |> REWRITE_RULE[Zadd_property] |> GEN_ALL 186); 187(* val funpow_reach = 188|- !f x y. reach (FUNPOW f) Z2 x y <=> ?a. a < 2 /\ FUNPOW f a x = y: thm *) 189 190val funpow_equiv = save_thm("funpow_equiv", 191 reach_equiv |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 192); 193(* val funpow_equiv = 194|- !f X. Group Z2 /\ (Z2 act X) (FUNPOW f) ==> reach (FUNPOW f) Z2 equiv_on X: thm *) 195 196(* A better version *) 197 198(* Theorem: f involute X ==> reach (FUNPOW f) Z2 equiv_on X *) 199(* Proof: 200 Note Group Z2 by Zadd_group, 0 < 2 201 and (Z2 act X) (FUNPOW f) by funpow_action 202 Thus reach (FUNPOW f) Z2 equiv_on X by reach_equiv 203*) 204Theorem funpow_equiv: 205 !f X. f involute X ==> reach (FUNPOW f) Z2 equiv_on X 206Proof 207 rw[Zadd_group, funpow_action, reach_equiv] 208QED 209 210(* ------------------------------------------------------------------------- *) 211(* FUNPOW Orbits *) 212(* ------------------------------------------------------------------------- *) 213 214val funpow_orbits = save_thm("funpow_orbits", 215 orbits_def |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 216); 217(* val funpow_orbits = 218|- !f X. orbits (FUNPOW f) Z2 X = IMAGE (orbit (FUNPOW f) Z2) X: thm *) 219 220val funpow_orbit = save_thm("funpow_orbit", 221 orbit_def |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` 222 |> REWRITE_RULE[Zadd_carrier] |> GEN_ALL 223); 224(* val funpow_orbit = 225|- !f x. orbit (FUNPOW f) Z2 x = IMAGE (\a. FUNPOW f a x) (count 2): thm *) 226 227val funpow_orbit_element = save_thm("funpow_orbit_element", 228 orbit_element |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` 229 |> SIMP_RULE (srw_ss()) [reach_def, Zadd_carrier] |> GEN_ALL 230); 231(* val funpow_orbit_element = 232|- !f x y. y IN orbit (FUNPOW f) Z2 x <=> ?a. a < 2 /\ FUNPOW f a x = y: thm *) 233 234val funpow_orbit_in_orbits = save_thm("funpow_orbit_in_orbits", 235 orbit_is_orbits_element |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 236); 237(* val funpow_orbit_in_orbits = 238|- !f X x. x IN X ==> orbit (FUNPOW f) Z2 x IN orbits (FUNPOW f) Z2 X: thm *) 239 240(* Theorem: FINITE (orbit (FUNPOW f) Z2 x) *) 241(* Proof: 242 Let b = orbit (FUNPOW f) Z2 x. 243 Note Z2.carrier = count 2 by Zadd_carrier 244 and FINITE (count 2) by FINITE_COUNT 245 so FINITE b by orbit_finite 246*) 247Theorem funpow_orbit_finite: 248 !f x. FINITE (orbit (FUNPOW f) Z2 x) 249Proof 250 simp[Zadd_carrier, orbit_finite] 251QED 252 253val funpow_orbits_finite = save_thm("funpow_orbits_finite", 254 orbits_finite |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 255); 256(* val funpow_orbits_finite = 257|- !f X. FINITE X ==> FINITE (orbits (FUNPOW f) Z2 X): thm *) 258 259val funpow_multi_orbits_finite = save_thm("funpow_multi_orbits_finite", 260 multi_orbits_finite |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 261); 262(* val funpow_multi_orbits_finite = 263|- !f X. FINITE X ==> FINITE (multi_orbits (FUNPOW f) Z2 X): thm *) 264 265(* ------------------------------------------------------------------------- *) 266(* Involution Orbits *) 267(* ------------------------------------------------------------------------- *) 268 269(* Theorem: f involute X /\ x IN X /\ 270 y IN (orbit (FUNPOW f) Z2 x) ==> y = x \/ y = f x *) 271(* Proof: 272 Note ?a. a < 2 /\ FUNPOW f a x = y by funpow_orbit_element 273 When n = 0, y = FUNPOW f 0 x = x by FUNPOW_0 274 When n = 1, y = FUNPOW f 1 x = f x by FUNPOW_1 275*) 276Theorem involute_orbit_element: 277 !f X x y. f involute X /\ x IN X /\ 278 y IN (orbit (FUNPOW f) Z2 x) ==> y = x \/ y = f x 279Proof 280 rpt strip_tac >> 281 imp_res_tac funpow_orbit_element >> 282 (`a = 0 \/ a = 1` by decide_tac >> fs[]) 283QED 284 285(* Theorem: f involute X /\ x IN X ==> x IN orbit (FUNPOW f) Z2 x *) 286(* Proof: 287 Note Group Z2 by Zadd_group, 0 < 2 288 and (Z2 act X) (FUNPOW f) by funpow_action 289 Thus x IN orbit (FUNPOW f) Z2 x by orbit_has_self 290*) 291Theorem involute_orbit_has_self: 292 !f X x. f involute X /\ x IN X ==> x IN orbit (FUNPOW f) Z2 x 293Proof 294 metis_tac[Zadd_group, funpow_action, orbit_has_self, DECIDE``0 < 2``] 295QED 296 297(* Theorem: f involute X /\ x IN X ==> 298 FUNPOW f n a IN orbit (FUNPOW f) Z2 x *) 299(* Proof: 300 Let b = orbit (FUNPOW f) Z2 x, k = n MOD 2. 301 Then k < 2 by MOD_LESS, 0 < 2 302 and FUNPOW f 2 x = x by involute_alt 303 so FUNPOW f n x = FUNPOW f k x by FUNPOW_MOD, 0 < 2, [1] 304 Note Group Z2 by Zadd_group, 0 < 2 305 and (Z2 act X) (FUNPOW f) by funpow_action 306 and k IN Z2.carrier by Zadd_element, n < 2 307 Thus (FUNPOW f k a) IN b by orbit_has_action_element 308 or (FUNPOW f n a) IN b by above [1] 309*) 310Theorem involute_orbit_has_funpow: 311 !f X x n. f involute X /\ x IN X ==> 312 FUNPOW f n x IN orbit (FUNPOW f) Z2 x 313Proof 314 rpt strip_tac >> 315 qabbrev_tac `k = n MOD 2` >> 316 `k < 2` by rw[Abbr`k`] >> 317 `FUNPOW f n x = FUNPOW f k x` by fs[involute_alt, FUNPOW_MOD, Abbr`k`] >> 318 rw[Zadd_group, funpow_action, orbit_has_action_element, Zadd_element] 319QED 320 321(* Theorem: f involute X /\ x IN X ==> f x IN orbit (FUNPOW f) Z2 x *) 322(* Proof: 323 Let b = orbit (FUNPOW f) Z2 x. 324 Note (FUNPOW f 1 x) IN b by involute_orbit_has_funpow 325 and FUNPOW f 1 x = f x by FUNPOW_1 326*) 327Theorem involute_orbit_has_image: 328 !f X x. f involute X /\ x IN X ==> f x IN orbit (FUNPOW f) Z2 x 329Proof 330 metis_tac[involute_orbit_has_funpow, FUNPOW_1, DECIDE``1 < 2``] 331QED 332 333(* Theorem: f involute X /\ e IN orbits (FUNPOW f) Z2 X ==> e <> EMPTY *) 334(* Proof: 335 Let B = orbits (FUNPOW f) Z2 X. 336 Note Group Z2 by Zadd_group, 0 < 2 337 and (Z2 act X) (FUNPOW f) by funpow_action 338 Thus e IN B ==> e <> EMPTY by orbits_element_nonempty 339*) 340Theorem involute_orbit_nonempty: 341 !f X e. f involute X /\ e IN orbits (FUNPOW f) Z2 X ==> e <> EMPTY 342Proof 343 metis_tac[Zadd_group, funpow_action, orbits_element_nonempty, DECIDE``0 < 2``] 344QED 345 346(* Theorem: f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ x IN e ==> 347 e = orbit (FUNPOW f) Z2 x *) 348(* Proof: 349 Let B = orbits (FUNPOW f) Z2 X. 350 Note Group Z2 by Zadd_group, 0 < 2 351 and (Z2 act X) (FUNPOW f) by funpow_action 352 Thus e = orbit (FUNPOW f) Z2 x by orbits_element_is_orbit 353*) 354Theorem involute_orbits_element_is_orbit: 355 !f X e x. f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ x IN e ==> 356 e = orbit (FUNPOW f) Z2 x 357Proof 358 metis_tac[Zadd_group, funpow_action, orbits_element_is_orbit, DECIDE``0 < 2``] 359QED 360 361(* Theorem: f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ x IN e ==> x IN X *) 362(* Proof: 363 Let B = orbits (FUNPOW f) Z2 X. 364 Note (Z2 act X) (FUNPOW f) by funpow_action 365 Thus x IN X by orbits_element_element 366*) 367Theorem involute_orbits_element_element: 368 !f X e x. f involute X /\ e IN orbits (FUNPOW f) Z2 X /\ x IN e ==> x IN X 369Proof 370 metis_tac[funpow_action, orbits_element_element] 371QED 372 373(* ------------------------------------------------------------------------- *) 374(* Involution fixed points *) 375(* ------------------------------------------------------------------------- *) 376 377(* Theorem: f involute X /\ x IN fixed_points (FUNPOW f) Z2 X ==> f x = x *) 378(* Proof: 379 Note 1 IN Z2.carrier by Zadd_element, 1 < 2 380 f x 381 = FUNPOW f 1 x by FUNPOW_1 382 = x by fixed_points_element 383*) 384Theorem involute_fixed_points: 385 !f X x. f involute X /\ x IN fixed_points (FUNPOW f) Z2 X ==> f x = x 386Proof 387 rw[fixed_points_element, Zadd_element] >> 388 metis_tac[FUNPOW_1, DECIDE``1 < 2``] 389QED 390 391(* Theorem: f involute X /\ x IN X ==> 392 (x IN fixed_points (FUNPOW f) Z2 X <=> f x = x) *) 393(* Proof: 394 By fixed_points_element, this is to show: 395 If part: x IN X /\ !a. a < 2 /\ FUNPOW f a x = x ==> f x = x 396 Since f x = FUNPOW 1 x by FUNPOW_1 397 so f x = x by implication 398 Only-if part: x IN X /\ f x = x ==> !a. a < 2 ==> FUNPOW f a x = x 399 When a = 0, FUNPOW f 0 x = x by FUNPOW_0 400 When a = 1, FUNPOW f 1 x = f x = x by FUNPOW_1, f involute X 401*) 402Theorem involute_fixed_points_iff: 403 !f X x. f involute X /\ x IN X ==> 404 (x IN fixed_points (FUNPOW f) Z2 X <=> f x = x) 405Proof 406 rw[fixed_points_element, Zadd_element, EQ_IMP_THM] >- 407 metis_tac[FUNPOW_1, DECIDE``1 < 2``] >> 408 (`a = 0 \/ a = 1` by decide_tac >> simp[]) 409QED 410 411val involute_fixed_points_element_element = 412 save_thm("involute_fixed_points_element_element", 413 fixed_points_element_element |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 414); 415(* val involute_fixed_points_element_element = 416|- !f X x. x IN fixed_points (FUNPOW f) Z2 X ==> x IN X: thm *) 417 418(* ------------------------------------------------------------------------- *) 419(* Involution Target Cardinality *) 420(* ------------------------------------------------------------------------- *) 421 422val involute_target_card_by_types = save_thm("involute_target_card_by_types", 423 target_card_by_orbit_types |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL 424); 425(* val involute_target_card_by_types = 426|- !f X. Group Z2 /\ (Z2 act X) (FUNPOW f) /\ FINITE X ==> 427 CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + 428 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X): thm *) 429 430(* A better version *) 431 432(* Theorem: FINITE X /\ f involute X ==> 433 CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + 434 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) *) 435(* Proof: 436 Note Group Z2 by Zadd_group, 0 < 2 437 and (Z2 act X) (FUNPOW f) by funpow_action 438 Thus CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + 439 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) 440 by target_card_by_orbit_types 441*) 442Theorem involute_target_card_by_types: 443 !f X. FINITE X /\ f involute X ==> 444 CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + 445 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) 446Proof 447 simp[Zadd_group, funpow_action, target_card_by_orbit_types] 448QED 449 450(* Theorem: FINITE X /\ f involute X ==> 451 CARD X = CARD (fixed_points (FUNPOW f) Z2 X) + 452 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) *) 453(* Proof: 454 Note Group Z2 by Zadd_group 455 and (Z2 act X) (FUNPOW f) by funpow_action 456 Thus CARD X = CARD (fixed_points (FUNPOW f) Z2 X) + 457 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) 458 by target_card_by_fixed_points 459*) 460Theorem involute_target_card_eqn: 461 !f X. FINITE X /\ f involute X ==> 462 CARD X = CARD (fixed_points (FUNPOW f) Z2 X) + 463 SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) 464Proof 465 simp[Zadd_group, funpow_action, target_card_by_fixed_points] 466QED 467 468(* This will be very useful! *) 469 470(* Theorem: f involute X /\ x IN X /\ f x = x ==> 471 orbit (FUNPOW f) Z2 x = {x} *) 472(* Proof: 473 Let b = orbit (FUNPOW f) Z2 x. 474 Note x IN b by involute_orbit_has_self 475 and !b. b IN X ==> (b = x) by involute_orbit_element, f x = x. 476 Thus b = {x} by EXTENSION 477*) 478Theorem involute_orbit_fixed: 479 !f X x. f involute X /\ x IN X /\ f x = x ==> 480 orbit (FUNPOW f) Z2 x = {x} 481Proof 482 rw[EXTENSION] >> 483 metis_tac[involute_orbit_has_self, involute_orbit_element] 484QED 485 486(* Theorem: f involute X /\ x IN X /\ f x <> x ==> 487 orbit (FUNPOW f) Z2 x = {x; f x} *) 488(* Proof: 489 Let b = orbit (FUNPOW f) Z2 x. 490 Note x IN b by involute_orbit_has_self 491 and f x IN b by involute_orbit_has_image 492 and !c. c IN X ==> (c = x) \/ (c = f x) 493 by involute_orbit_element, f x <> x 494 Thus b = {x; f x} by EXTENSION 495*) 496Theorem involute_orbit_not_fixed: 497 !f X x. f involute X /\ x IN X /\ f x <> x ==> 498 orbit (FUNPOW f) Z2 x = {x; f x} 499Proof 500 rw[EXTENSION] >> 501 imp_res_tac involute_orbit_has_self >> 502 metis_tac[involute_orbit_has_image, involute_orbit_element] 503QED 504 505(* Theorem: f involute X /\ 506 e IN (multi_orbits (FUNPOW f) Z2 X) ==> CARD e = 2 *) 507(* Proof: 508 By multi_orbits_def, this is to show: 509 !e. e IN orbits (FUNPOW f) Z2 X /\ ~SING e ==> CARD e = 2. 510 Note e <> EMPTY by involute_orbit_nonempty 511 so ?x. x IN e by MEMBER_NOT_EMPTY 512 and e = orbit (FUNPOW f) Z2 x by involute_orbits_element_is_orbit 513 now x IN X by involute_orbits_element_element 514 If f x = x, 515 then e = {x} by involute_orbit_fixed 516 thus SING e by SING_DEF 517 This contradicts ~SING e 518 Otherwise, f x <> x. 519 then e = {x; f x} by involute_orbit_not_fixed 520 so CARD e = 2 by CARD_DEF 521*) 522Theorem involute_multi_orbits_element_card: 523 !f X e. f involute X /\ 524 e IN (multi_orbits (FUNPOW f) Z2 X) ==> CARD e = 2 525Proof 526 rw[multi_orbits_def] >> 527 `?x. x IN e` by metis_tac[involute_orbit_nonempty, MEMBER_NOT_EMPTY] >> 528 `e = orbit (FUNPOW f) Z2 x` by metis_tac[involute_orbits_element_is_orbit] >> 529 `x IN X` by metis_tac[involute_orbits_element_element] >> 530 Cases_on `f x = x` >- 531 metis_tac[involute_orbit_fixed, SING_DEF] >> 532 `e = {x; f x}` by metis_tac[involute_orbit_not_fixed] >> 533 rw[] 534QED 535 536(* Theorem: FINITE X /\ f involute X ==> 537 CARD X = 2 * CARD (multi_orbits (FUNPOW f) Z2 X) + 538 CARD (fixed_points (FUNPOW f) Z2 X) *) 539(* Proof: 540 Let a = multi_orbits (FUNPOW f) Z2 X, 541 b = fixed_points (FUNPOW f) Z2 X. 542 Then FINITE a by funpow_multi_orbits_finite 543 CARD X 544 = CARD b + SIGMA CARD a by involute_target_card_eqn 545 = CARD b + 2 * CARD a by SIGMA_CONSTANT, involute_multi_orbits_element_card 546 = 2 * CARD a + CARD b by ADD_COMM 547*) 548Theorem involute_target_card_thm: 549 !f X. FINITE X /\ f involute X ==> 550 CARD X = 2 * CARD (multi_orbits (FUNPOW f) Z2 X) + 551 CARD (fixed_points (FUNPOW f) Z2 X) 552Proof 553 rpt strip_tac >> 554 qabbrev_tac `a = multi_orbits (FUNPOW f) Z2 X` >> 555 qabbrev_tac `b = fixed_points (FUNPOW f) Z2 X` >> 556 `FINITE a` by rw[funpow_multi_orbits_finite, Abbr`a`] >> 557 `CARD X = CARD b + SIGMA CARD a` by rw[involute_target_card_eqn, Abbr`a`, Abbr`b`] >> 558 `_ = CARD b + 2 * CARD a` by metis_tac[SIGMA_CONSTANT, involute_multi_orbits_element_card] >> 559 simp[] 560QED 561 562(* Theorem: FINITE X /\ f involute X ==> 563 (EVEN (CARD X) <=> EVEN (CARD (fixed_points (FUNPOW f) Z2 X))) *) 564(* Proof: 565 Let a = multi_orbits (FUNPOW f) Z2 X, 566 b = fixed_points (FUNPOW f) Z2 X. 567 Note CARD X = 2 * a + CARD b by involute_target_card_thm 568 so EVEN (CARD X) <=> EVEN (CARD b) by EQ_PARITY 569*) 570Theorem involute_fixed_points_both_even: 571 !f X. FINITE X /\ f involute X ==> 572 (EVEN (CARD X) <=> EVEN (CARD (fixed_points (FUNPOW f) Z2 X))) 573Proof 574 metis_tac[involute_target_card_thm, EQ_PARITY] 575QED 576 577(* Theorem: FINITE X /\ f involute X ==> 578 (ODD (CARD X) <=> ODD (CARD (fixed_points (FUNPOW f) Z2 X))) *) 579(* Proof: by involute_fixed_points_both_even, ODD_EVEN. *) 580Theorem involute_fixed_points_both_odd: 581 !f X. FINITE X /\ f involute X ==> 582 (ODD (CARD X) <=> ODD (CARD (fixed_points (FUNPOW f) Z2 X))) 583Proof 584 rw[involute_fixed_points_both_even, ODD_EVEN] 585QED 586 587(* A useful corollary. *) 588 589(* Theorem: FINITE X /\ f involute X /\ g involute X ==> 590 (EVEN (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 591 EVEN (CARD (fixed_points (FUNPOW g) Z2 X))) *) 592(* Proof: 593 Let a = multi_orbits (FUNPOW f) Z2 X, 594 b = fixed_points (FUNPOW f) Z2 X, 595 c = multi_orbits (FUNPOW g) Z2 X, 596 d = fixed_points (FUNPOW g) Z2 X. 597 Note EVEN (CARD X) <=> EVEN (CARD b) by involute_fixed_points_both_even 598 and EVEN (CARD X) <=> EVEN (CARD d) by involute_fixed_points_both_even 599 Thus EVEN (CARD b) <=> EVEN (CARD d) 600*) 601Theorem involute_two_fixed_points_both_even: 602 !f g X. FINITE X /\ f involute X /\ g involute X ==> 603 (EVEN (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 604 EVEN (CARD (fixed_points (FUNPOW g) Z2 X))) 605Proof 606 metis_tac[involute_fixed_points_both_even] 607QED 608 609(* Theorem: FINITE X /\ f involute X /\ g involute X ==> 610 (ODD (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 611 ODD (CARD (fixed_points (FUNPOW g) Z2 X))) *) 612(* Proof: by involute_two_fixed_points_both_even, ODD_EVEN. *) 613Theorem involute_two_fixed_points_both_odd: 614 !f g X. FINITE X /\ f involute X /\ g involute X ==> 615 (ODD (CARD (fixed_points (FUNPOW f) Z2 X)) <=> 616 ODD (CARD (fixed_points (FUNPOW g) Z2 X))) 617Proof 618 rw[involute_two_fixed_points_both_even, ODD_EVEN] 619QED 620 621(* ------------------------------------------------------------------------- *) 622 623(* export theory at end *) 624val _ = export_theory(); 625 626(*===========================================================================*) 627