1(* ------------------------------------------------------------------------- *) 2(* Involution Fix *) 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 "involuteFix"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17val _ = load("involuteTheory"); 18open helperFunctionTheory; (* for FUNPOW_2 *) 19open helperSetTheory; (* for BIJ_ELEMENT *) 20open helperNumTheory; (* for MOD_EQ *) 21open helperTheory; (* for doublet_finite, doublet_card *) 22open involuteTheory; 23 24(* arithmeticTheory -- load by default *) 25open arithmeticTheory pred_setTheory; 26 27 28(* ------------------------------------------------------------------------- *) 29(* Involution Fix Documentation *) 30(* ------------------------------------------------------------------------- *) 31(* Overloading: 32 pair_by f = \x y. (x fpair y) f 33*) 34(* 35 36 Helper Theorems: 37 38 Singles and Doubles of Involution: 39 fpair_def |- !x y f. pair_by f x y <=> y = x \/ y = f x 40 fpair_refl |- !f x. pair_by f x x 41 fpair_sym |- !f s x y. f involute s /\ x IN s /\ 42 pair_by f x y ==> pair_by f y x 43 fpair_trans |- !f s x y z. f involute s /\ x IN s /\ 44 pair_by f x y /\ pair_by f y z ==> pair_by f x z 45 fpair_equiv |- !f s. f involute s ==> (\x y. pair_by f x y) equiv_on s 46 47 fixes_def |- !f s. fixes f s = {x | x IN s /\ f x = x} 48 pairs_def |- !f s. pairs f s = {x | x IN s /\ f x <> x} 49 fixes_element |- !f s x. x IN fixes f s <=> x IN s /\ f x = x 50 pairs_element |- !f s x. x IN pairs f s <=> x IN s /\ f x <> x 51 fixes_subset |- !f s. fixes f s SUBSET s 52 pairs_subset |- !f s. pairs f s SUBSET s 53 fixes_finite |- !f s. FINITE s ==> FINITE (fixes f s) 54 pairs_finite |- !f s. FINITE s ==> FINITE (pairs f s) 55 56 Equivalence classes of pair_by: 57 equiv_class_fixes_iff |- !f s x. f endo s ==> 58 (x IN fixes f s <=> 59 equiv_class (\x y. pair_by f x y) s x = {x}) 60 equiv_class_fixes |- !f s x. x IN fixes f s ==> 61 equiv_class (\x y. pair_by f x y) s x = {x} 62 equiv_class_pairs_iff |- !f s x. f endo s ==> 63 (x IN pairs f s <=> 64 equiv_class (\x y. pair_by f x y) s x = {x; f x} /\ f x <> x) 65 equiv_class_pairs |- !f s x. x IN pairs f s /\ f x IN s ==> 66 equiv_class (\x y. pair_by f x y) s x = {x; f x} 67 involute_pairs_element_pair 68 |- !f s x. f involute s /\ x IN pairs f s ==> f x IN pairs f s 69 equiv_class_pairs_pairs |- !f s x. f involute s /\ x IN pairs f s ==> 70 equiv_class (\x y. pair_by f x y) s (f x) = 71 equiv_class (\x y. pair_by f x y) s x 72 73 Show partitions: 74 fixes_pairs_split |- !f s. s =|= fixes f s # pairs f s 75 fixes_pairs_union |- !f s. s = fixes f s UNION pairs f s 76 fixes_pairs_disjoint |- !f s. DISJOINT (fixes f s) (pairs f s) 77 78 equiv_fixes_def |- !f s. equiv_fixes f s = 79 IMAGE (\x. equiv_class (\x y. pair_by f x y) s x) (fixes f s) 80 equiv_pairs_def |- !f s. equiv_pairs f s = 81 IMAGE (\x. equiv_class (\x y. pair_by f x y) s x) (pairs f s) 82 equiv_fixes_element |- !f s x. x IN equiv_fixes f s <=> 83 ?y. y IN fixes f s /\ (x = equiv_class (\x y. pair_by f x y) s y) 84 equiv_pairs_element |- !f s x. x IN equiv_pairs f s <=> 85 ?y. y IN pairs f s /\ (x = equiv_class (\x y. pair_by f x y) s y) 86 equiv_fixes_pairs_disjoint 87 |- !f s. DISJOINT (equiv_fixes f s) (equiv_pairs f s) 88 89 equiv_fixes_pairs_union |- !f s. partition (\x y. pair_by f x y) s = 90 equiv_fixes f s UNION equiv_pairs f s 91 equiv_fixes_pairs_split |- !f s. partition (\x y. pair_by f x y) s =|= 92 equiv_fixes f s # equiv_pairs f s 93 equiv_fixes_subset |- !f s. equiv_fixes f s SUBSET partition (\x y. pair_by f x y) s 94 equiv_pairs_subset |- !f s. equiv_pairs f s SUBSET partition (\x y. pair_by f x y) s 95 equiv_fixes_element_sing_iff 96 |- !f s t. f endo s ==> 97 (t IN equiv_fixes f s <=> ?x. x IN fixes f s /\ t = {x}) 98 equiv_fixes_element_sing |- !f s t. t IN equiv_fixes f s ==> ?x. x IN fixes f s /\ t = {x} 99 equiv_fixes_element_card |- !f s t. t IN equiv_fixes f s ==> CARD t = 1 100 equiv_pairs_element_doublet_iff 101 |- !f s t. f endo s ==> 102 (t IN equiv_pairs f s <=> ?x. x IN pairs f s /\ t = {x; f x}) 103 equiv_pairs_element_doublet 104 |- !f s t. f endo s /\ t IN equiv_pairs f s ==> 105 ?x. x IN pairs f s /\ t = {x; f x} 106 equiv_pairs_element_card |- !f s t. f endo s /\ t IN equiv_pairs f s ==> CARD t = 2 107 equiv_fixes_fixes_bij |- !f s. f endo s ==> BIJ CHOICE (equiv_fixes f s) (fixes f s) 108 equiv_fixes_card |- !f s. FINITE s /\ f endo s ==> 109 CARD (equiv_fixes f s) = CARD (fixes f s) 110 equiv_fixes_finite |- !f s. FINITE s ==> FINITE (equiv_fixes f s) 111 equiv_pairs_finite |- !f s. FINITE s ==> FINITE (equiv_pairs f s) 112 113 equiv_fixes_pair_disjoint |- !f s. f involute s ==> PAIR_DISJOINT (equiv_fixes f s) 114 equiv_pairs_pair_disjoint |- !f s. f involute s ==> PAIR_DISJOINT (equiv_pairs f s) 115 equiv_pairs_bigunion_card_even 116 |- !f s. FINITE s /\ f involute s ==> 117 EVEN (CARD (BIGUNION (equiv_pairs f s))) 118 equiv_fixes_by_image |- !f s. f endo s ==> equiv_fixes f s = IMAGE (\x. {x}) (fixes f s) 119 equiv_pairs_by_image |- !f s. f endo s ==> equiv_pairs f s = IMAGE (\x. {x; f x}) (pairs f s) 120 equiv_fixes_bigunion |- !f s. f endo s ==> BIGUNION (equiv_fixes f s) = fixes f s 121 equiv_fixes_pairs_bigunion_disjoint 122 |- !f s. f involute s ==> 123 DISJOINT (BIGUNION (equiv_fixes f s)) (BIGUNION (equiv_pairs f s)) 124 equiv_fixes_pairs_bigunion_union 125 |- !f s. f involute s ==> 126 s = BIGUNION (equiv_fixes f s) UNION BIGUNION (equiv_pairs f s) 127 equiv_fixes_pairs_bigunion_split 128 |- !f s. f involute s ==> 129 s =|= BIGUNION (equiv_fixes f s) # BIGUNION (equiv_pairs f s) 130 equiv_pairs_bigunion |- !f s. f involute s ==> (BIGUNION (equiv_pairs f s) = pairs f s) 131 pairs_card_even |- !f s. FINITE s /\ f involute s ==> EVEN (CARD (pairs f s)) 132 involute_set_fixes_both_even 133 |- !f s. FINITE s /\ f involute s ==> 134 (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) 135 involute_set_fixes_both_odd 136 |- !f s. FINITE s /\ f involute s ==> 137 (ODD (CARD s) <=> ODD (CARD (fixes f s))) 138 139 Reformulate using mates: 140 mates_def |- !f s. mates f s = s DIFF fixes f s 141 mates_element |- !f s x. x IN mates f s <=> x IN s /\ f x <> x 142 mates_subset |- !f s. mates f s SUBSET s 143 mates_finite |- !f s. FINITE s ==> FINITE (mates f s) 144 mates_fixes_union |- !f s. s = mates f s UNION fixes f s 145 mates_fixes_disjoint |- !f s. DISJOINT (mates f s) (fixes f s) 146 mates_fixes_card |- !f s. FINITE s ==> CARD s = CARD (mates f s) + CARD (fixes f s) 147 involute_mates |- !f s. f involute s ==> f involute mates f s 148 involute_mates_partner|- !f s x. f involute s /\ x IN mates f s ==> f x IN mates f s 149 fpair_equiv_on_mates |- !f s. f involute s ==> (\x y. pair_by f x y) equiv_on mates f s 150 mates_partition_element_doublet 151 |- !f s t. f involute s ==> 152 t IN partition (\x y. pair_by f x y) (mates f s) <=> 153 ?x. x IN mates f s /\ t = {x; f x} 154 mates_partition_element_card 155 |- !f s t. FINITE s /\ f involute s /\ 156 t IN partition (\x y. pair_by f x y) (mates f s) ==> 157 CARD t = 2 158 mates_card_even |- !f s. FINITE s /\ f involute s ==> EVEN (CARD (mates f s)) 159 involute_set_fixes_both_even 160 |- !f s. FINITE s /\ f involute s ==> 161 (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) 162 163 Two Involutions: 164 involute_two_fixes_both_even 165 |- !f g s. FINITE s /\ f involute s /\ g involute s ==> 166 (EVEN (CARD (fixes f s)) <=> EVEN (CARD (fixes g s))) 167 involute_two_fixes_both_odd 168 |- !f g s. FINITE s /\ f involute s /\ g involute s ==> 169 (ODD (CARD (fixes f s)) <=> ODD (CARD (fixes g s))) 170*) 171 172(* ------------------------------------------------------------------------- *) 173(* Helper Theorems *) 174(* ------------------------------------------------------------------------- *) 175 176(* ------------------------------------------------------------------------- *) 177(* Singles and Doubles of Involution *) 178(* ------------------------------------------------------------------------- *) 179 180(* Use this approach: 181 182A finite set and the set of its fixed points under any involution have cardinalities of the same parity 183https://math.stackexchange.com/questions/1373671/ 184answer by Brian M. Scott, July 2015. 185 186*) 187 188(* 189if fpair x y f <=> y = f x 190this is too general: 191* it cannot be shown to be reflexive 192* it cannot be symmetric in general: y = f x /\ x = f y ==> x = f (f x) only. 193* it is almost transitive: y = f x /\ z = f y ==> z = f (f x) 194* Thus to make this an equivalence relation, need to extend y = f x to y = f^n x 195for whatever n. That's the repeat of f, and the relation is: reachable. 196 197Adding the possibility of equality in (fpair x y f) changes things: 198* it is reflexive by default of equality. 199* it is symmetric when f (f x) = x, that is, an involution. 200* it is transitive when f (f x) = x, due to equality, that is, an involution. 201*) 202 203(* Define an equivalence relation *) 204Definition fpair_def: 205 fpair x y f <=> y = x \/ y = f x 206End 207 208(* make this infix *) 209val _ = set_fixity "fpair" (Infix(NONASSOC, 450)); 210 211(* Theorem: (x fpair x) f *) 212(* Proof: by fpair_def, x = x. *) 213Theorem fpair_refl: 214 !f x. (x fpair x) f 215Proof 216 rw[fpair_def] 217QED 218 219(* Theorem: f involute s /\ x IN s /\ (x fpair y) f ==> (y fpair x) f *) 220(* Proof: 221 If x = y, this is trivial. 222 Assume x <> y, 223 Then y = f x by fpair_def 224 and f y = f (f x) = x by f involute s, x IN s 225 Thus (y fpair x) f by fpair_def 226*) 227Theorem fpair_sym: 228 !f s x y. f involute s /\ x IN s /\ (x fpair y) f ==> (y fpair x) f 229Proof 230 metis_tac[fpair_def] 231QED 232 233(* Theorem: f involute s /\ x IN s /\ (x fpair y) f /\ (y fpair z) f ==> (x fpair z) f *) 234(* Proof: 235 If x = y or y = z, this is trivial. 236 Assume x <> y and y <> z. 237 Then y = f x by fpair_def 238 and z = f y by fpair_def 239 = f (f x) by above 240 = x by f involute s, x IN s 241 Thus (x fpair z) f by fpair_def 242*) 243Theorem fpair_trans: 244 !f s x y z. f involute s /\ x IN s /\ 245 (x fpair y) f /\ (y fpair z) f ==> (x fpair z) f 246Proof 247 (rw[fpair_def] >> metis_tac[]) 248QED 249 250(* Overload the equivalence relation *) 251val _ = overload_on("pair_by", ``\f x y. (x fpair y) f``); 252 253(* Theorem: f involute s ==> (pair_by f) equiv_on s *) 254(* Proof: by equiv_on_def, fpair_refl, fpair_sym, fpair_trans *) 255Theorem fpair_equiv: 256 !f s. f involute s ==> (pair_by f) equiv_on s 257Proof 258 rw[equiv_on_def] >- 259 simp[fpair_refl] >- 260 metis_tac[fpair_sym] >> 261 metis_tac[fpair_trans] 262QED 263 264(* Define the fixed points and pairs of involution. *) 265Definition fixes_def: 266 fixes f s = {x | x IN s /\ f x = x} 267End 268 269(* Define the pairs of involution. *) 270Definition pairs_def: 271 pairs f s = {x | x IN s /\ f x <> x} 272End 273 274(* Theorem: x IN fixes f s <=> x IN s /\ f x = x *) 275(* Proof: by fixes_def *) 276Theorem fixes_element: 277 !f s x. x IN fixes f s <=> x IN s /\ f x = x 278Proof 279 rw[fixes_def] 280QED 281 282(* Theorem: x IN pairs f s <=> x IN s /\ f x <> x *) 283(* Proof: by pairs_def *) 284Theorem pairs_element: 285 !f s x. x IN pairs f s <=> x IN s /\ f x <> x 286Proof 287 rw[pairs_def] 288QED 289 290(* Theorem: fixes f s SUBSET s *) 291(* Proof: by fixes_def *) 292Theorem fixes_subset: 293 !f s. fixes f s SUBSET s 294Proof 295 rw[fixes_def, SUBSET_DEF] 296QED 297 298(* Theorem: pairs f s SUBSET s *) 299(* Proof: by pairs_def *) 300Theorem pairs_subset: 301 !f s. pairs f s SUBSET s 302Proof 303 rw[pairs_def, SUBSET_DEF] 304QED 305 306(* Theorem: FINITE s ==> FINITE (fixes f s) *) 307(* Proof: 308 Note (fixes f s) SUBSET s by fixes_subset 309 Thus FINITE (fixes f s) by SUBSET_FINITE 310*) 311Theorem fixes_finite: 312 !f s. FINITE s ==> FINITE (fixes f s) 313Proof 314 metis_tac[fixes_subset, SUBSET_FINITE] 315QED 316 317(* Theorem: FINITE s ==> FINITE (pairs f s) *) 318(* Proof: 319 Note (pairs f s) SUBSET s by pairs_subset 320 Thus FINITE (pairs f s) by SUBSET_FINITE 321*) 322Theorem pairs_finite: 323 !f s. FINITE s ==> FINITE (pairs f s) 324Proof 325 metis_tac[pairs_subset, SUBSET_FINITE] 326QED 327 328(* Equivalence classes of pair_by *) 329 330(* Theorem: f endo s ==> (x IN fixes f s <=> equiv_class (pair_by f) s x = {x}) *) 331(* Proof: 332 y IN equiv_class (pair_by f) s x 333 <=> y IN s /\ (pair_by f) x y by equiv_class_element 334 <=> y IN s /\ (x fpair y) f by notation 335 <=> y IN s /\ ((x = y) \/ (y = f x)) by fpair_def 336 <=> y IN s /\ ((x = y) \/ (y = x)) by fixes_def 337 <=> y IN s /\ (x = y) 338 <=> y IN {x} /\ x IN s by fixes_def 339 Thus equiv_class (pair_by f) s x = {x} by EXTENSION 340*) 341Theorem equiv_class_fixes_iff: 342 !f s x. f endo s ==> 343 (x IN fixes f s <=> equiv_class (pair_by f) s x = {x}) 344Proof 345 rw[fixes_def, fpair_def, EXTENSION, EQ_IMP_THM] 346QED 347 348(* Theorem: x IN fixes f s ==> equiv_class (pair_by f) s x = {x} *) 349(* Proof: simplifed form of equiv_class_fixes_iff. *) 350Theorem equiv_class_fixes: 351 !f s x. x IN fixes f s ==> equiv_class (pair_by f) s x = {x} 352Proof 353 rw[fixes_def, fpair_def, EXTENSION] >> 354 metis_tac[] 355QED 356 357(* Theorem: f endo s ==> 358 (x IN pairs f s <=> equiv_class (pair_by f) s x = {x; f x} /\ f x <> x) *) 359(* Proof: 360 y IN equiv_class (pair_by f) s x 361 <=> y IN s /\ (pair_by f) x y by equiv_class_element 362 <=> y IN s /\ (x fpair y) f by notation 363 <=> y IN s /\ ((x = y) \/ (y = f x)) by fpair_def 364 <=> y IN s /\ y IN {x; f x} /\ f x <> x by pairs_def 365 <=> y IN {x; f x} /\ x IN s /\ f x IN s by pairs_def, f x IN s 366 Thus equiv_class (pair_by f) s x = {x; f x} by EXTENSION 367*) 368Theorem equiv_class_pairs_iff: 369 !f s x. f endo s ==> 370 (x IN pairs f s <=> equiv_class (pair_by f) s x = {x; f x} /\ f x <> x) 371Proof 372 rw[pairs_def, fpair_def, EXTENSION] >> 373 metis_tac[] 374QED 375 376(* Theorem: x IN pairs f s /\ f x IN s ==> 377 equiv_class (pair_by f) s x = {x; f x} *) 378(* Proof: simplifed form of equiv_class_pairs_iff. *) 379Theorem equiv_class_pairs: 380 !f s x. x IN pairs f s /\ f x IN s ==> 381 equiv_class (pair_by f) s x = {x; f x} 382Proof 383 rw[pairs_def, fpair_def, EXTENSION] >> 384 metis_tac[] 385QED 386 387(* Theorem: x IN pairs f s /\ f x IN s ==> f x IN pairs f s *) 388(* Proof: 389 Note x IN pairs f s 390 <=> x IN s /\ f x <> x by pairs_def 391 f x IN pairs f s 392 <=> f x IN s /\ f (f x) <> f x by pairs_def 393 <=> T by f involute s 394*) 395Theorem involute_pairs_element_pair: 396 !f s x. f involute s /\ x IN pairs f s ==> f x IN pairs f s 397Proof 398 rw[pairs_def] 399QED 400 401(* Theorem: f involute s /\ x IN pairs f s ==> 402 equiv_class (pair_by f) s (f x) = equiv_class (pair_by f) s x *) 403(* Proof: 404 Note f involute s /\ x IN s ==> 405 f x IN s /\ f (f x) = x by notation 406 equiv_class (pair_by f) s (f x) 407 = {f x; f (f x)} by equiv_class_pairs 408 = {f x; x} by f involute s 409 = equiv_class (pair_by f) s x by equiv_class_pairs 410*) 411Theorem equiv_class_pairs_pairs: 412 !f s x. f involute s /\ x IN pairs f s ==> 413 equiv_class (pair_by f) s (f x) = equiv_class (pair_by f) s x 414Proof 415 rw[pairs_def, fpair_def, EXTENSION] >> 416 metis_tac[] 417QED 418 419(* Show partitions! *) 420 421(* Theorem: s =|= (fixes f s) # (pairs f s) *) 422(* Proof: by fixes_def, pairs_def *) 423Theorem fixes_pairs_split: 424 !f s. s =|= (fixes f s) # (pairs f s) 425Proof 426 (rw[fixes_def, pairs_def, DISJOINT_DEF, EXTENSION] >> metis_tac[]) 427QED 428 429(* Extract theorems *) 430val fixes_pairs_union = save_thm("fixes_pairs_union", 431 fixes_pairs_split |> SPEC_ALL |> CONJUNCT1 |> GEN ``s:'a -> bool`` |> GEN_ALL); 432(* val fixes_pairs_union = |- !f s. s = fixes f s UNION pairs f s: thm *) 433 434val fixes_pairs_disjoint = save_thm("fixes_pairs_disjoint", 435 fixes_pairs_split |> SPEC_ALL |> CONJUNCT2 |> GEN ``s:'a -> bool`` |> GEN_ALL); 436(* val fixes_pairs_disjoint = |- !f s. DISJOINT (fixes f s) (pairs f s): thm *) 437 438 439(* Those equivalent classes of fixes *) 440Definition equiv_fixes_def: 441 equiv_fixes f s = IMAGE (equiv_class (pair_by f) s) (fixes f s) 442End 443 444(* Those equivalent classes of pairs *) 445Definition equiv_pairs_def: 446 equiv_pairs f s = IMAGE (equiv_class (pair_by f) s) (pairs f s) 447End 448 449(* Theorem: x IN equiv_fixes f s <=> 450 ?y. y IN (fixes f s) /\ x = equiv_class (pair_by f) s y *) 451(* Proof: by equiv_fixes_def *) 452Theorem equiv_fixes_element: 453 !f s x. x IN equiv_fixes f s <=> 454 ?y. y IN (fixes f s) /\ x = equiv_class (pair_by f) s y 455Proof 456 rw[equiv_fixes_def] >> 457 metis_tac[] 458QED 459 460(* Theorem: x IN equiv_pairs f s <=> 461 ?y. y IN (pairs f s) /\ x = equiv_class (pair_by f) s y *) 462(* Proof: by equiv_fixes_def *) 463Theorem equiv_pairs_element: 464 !f s x. x IN equiv_pairs f s <=> 465 ?y. y IN (pairs f s) /\ x = equiv_class (pair_by f) s y 466Proof 467 rw[equiv_pairs_def] >> 468 metis_tac[] 469QED 470 471(* Theorem: DISJOINT (equiv_fixes f s) (equiv_pairs f s) *) 472(* Proof: 473 Let R = (pair_by f). 474 By contradiction, suppose there is an x such that: 475 x IN (equiv_fixes f s) INTER (equiv_pairs f s) 476 ==> x IN IMAGE (equiv_class R s) (fixes f s) /\ 477 x IN IMAGE (equiv_class R s) (pairs f s) by equiv_fixes_def, equiv_pairs_def 478 ==> ?y. (y = equiv_class R s x) /\ y IN fixes f s /\ by IN_IMAGE 479 ?z. (z = equiv_class R s x) /\ z IN pairs f s by IN_IMAGE 480 ==> ?y. y IN fixes f s /\ y IN pairs f s 481 This contradicts DISJOINT (fixes f s) (pairs f s) by fixes_pairs_disjoint 482*) 483Theorem equiv_fixes_pairs_disjoint: 484 !f s. DISJOINT (equiv_fixes f s) (equiv_pairs f s) 485Proof 486 rw[DISJOINT_DEF, equiv_fixes_def, equiv_pairs_def, EXTENSION] >> 487 spose_not_then strip_assume_tac >> 488 `x' IN x /\ x'' IN x /\ pair_by f x' x''` by metis_tac[fixes_element, pairs_element, fpair_refl] >> 489 `x' = x''` by fs[fpair_def, fixes_def] >> 490 metis_tac[fixes_pairs_disjoint, IN_DISJOINT] 491QED 492 493(* Theorem: partition (pair_by f) s = (equiv_fixes f s) UNION (equiv_pairs f s) *) 494(* Proof: 495 Let R = (pair_by f). 496 x IN partition R s 497 <=> ?t. t IN s /\ (x = equiv_class R s t) by partition_def 498 <=> ?t. (t IN (fixes f s) \/ t IN (pairs f s)) /\ 499 (x = equiv_class R s t) by fixes_pairs_union 500 <=> (x IN equiv_fixes R s) \/ by equiv_fixes_def 501 (x IN equiv_pairs R s) by equiv_pairs_def 502 <=> x IN (equiv_fixes f s) UNION (equiv_pairs f s) by IN_UNION 503*) 504Theorem equiv_fixes_pairs_union: 505 !f s. partition (pair_by f) s = (equiv_fixes f s) UNION (equiv_pairs f s) 506Proof 507 rpt strip_tac >> 508 `!x. x IN equiv_fixes f s <=> ?t. (x = equiv_class (\x y. pair_by f x y) s t) /\t IN (fixes f s)` by rw[equiv_fixes_def] >> 509 `!x. x IN equiv_pairs f s <=> ?t. (x = equiv_class (\x y. pair_by f x y) s t) /\t IN (pairs f s)` by rw[equiv_pairs_def] >> 510 qabbrev_tac `R = \x y. pair_by f x y` >> 511 rw_tac std_ss[EXTENSION] >> 512 `x IN partition R s <=> ?t. t IN s /\ (x = equiv_class R s t)` by rw[partition_def] >> 513 `_ = ?t. (t IN (fixes f s) \/ t IN (pairs f s)) /\ (x = equiv_class R s t)` by metis_tac[fixes_pairs_union, IN_UNION] >> 514 metis_tac[IN_UNION] 515QED 516 517(* Theorem: partition (pair_by f) s =|= (equiv_fixes f s) # (equiv_pairs f s) *) 518(* Proof: by equiv_fixes_pairs_union, equiv_fixes_pairs_disjoint *) 519Theorem equiv_fixes_pairs_split: 520 !f s. partition (pair_by f) s =|= (equiv_fixes f s) # (equiv_pairs f s) 521Proof 522 rw[equiv_fixes_pairs_union, equiv_fixes_pairs_disjoint] 523QED 524 525(* Theorem: equiv_fixes f s SUBSET partition (pair_by f) s *) 526(* Proof: by equiv_fixes_pairs_union, SUBSET_UNION *) 527Theorem equiv_fixes_subset: 528 !f s. equiv_fixes f s SUBSET partition (pair_by f) s 529Proof 530 rw[equiv_fixes_pairs_union, SUBSET_UNION] 531QED 532 533(* Theorem: equiv_pairs f s SUBSET partition (pair_by f) s *) 534(* Proof: by equiv_fixes_pairs_union, SUBSET_UNION *) 535Theorem equiv_pairs_subset: 536 !f s. equiv_pairs f s SUBSET partition (pair_by f) s 537Proof 538 rw[equiv_fixes_pairs_union, SUBSET_UNION] 539QED 540 541(* Theorem: f endo s ==> 542 (t IN equiv_fixes f s <=> ?x. x IN fixes f s /\ t = {x}) *) 543(* Proof: 544 t IN equiv_fixes f s 545 <=> ?x. x IN fixes f s /\ (t = equiv_class (pair_by f) s x) 546 by equiv_fixes_element 547 <=> ?x. x IN fixes f s /\ t = {x} by equiv_class_fixes_iff 548*) 549Theorem equiv_fixes_element_sing_iff: 550 !f s t. f endo s ==> 551 (t IN equiv_fixes f s <=> ?x. x IN fixes f s /\ t = {x}) 552Proof 553 metis_tac[equiv_fixes_element, equiv_class_fixes_iff] 554QED 555 556(* Theorem: t IN equiv_fixes f s ==> ?x. x IN fixes f s /\ t = {x} *) 557(* Proof: simplified form of equiv_fixes_element_sing_iff. *) 558Theorem equiv_fixes_element_sing: 559 !f s t. t IN equiv_fixes f s ==> ?x. x IN fixes f s /\ t = {x} 560Proof 561 rpt strip_tac >> 562 imp_res_tac equiv_fixes_element >> 563 rw[equiv_class_fixes] 564QED 565 566(* Theorem: t IN equiv_fixes f s ==> CARD t = 1 *) 567(* Proof: by equiv_fixes_element_sing, CARD_SING. *) 568Theorem equiv_fixes_element_card: 569 !f s t. t IN equiv_fixes f s ==> CARD t = 1 570Proof 571 metis_tac[equiv_fixes_element_sing, CARD_SING] 572QED 573 574(* Theorem: f endo s ==> 575 (t IN equiv_pairs f s <=> ?x. x IN pairs f s /\ t = {x; f x}) *) 576(* Proof: 577 t IN equiv_pairs f s 578 <=> ?x. x IN pairs f s /\ t = equiv_class (pair_by f) s x 579 by equiv_pairs_element 580 <=> ?x. x IN pairs f s /\ t = {x; f x} 581 by equiv_class_pairs_iff 582*) 583Theorem equiv_pairs_element_doublet_iff: 584 !f s t. f endo s ==> 585 (t IN equiv_pairs f s <=> ?x. x IN pairs f s /\ t = {x; f x}) 586Proof 587 metis_tac[equiv_pairs_element, pairs_element, equiv_class_pairs_iff] 588QED 589 590(* Theorem: f endo s /\ t IN equiv_pairs f s ==> 591 ?x. x IN pairs f s /\ t = {x; f x} *) 592(* Proof: simplified form of equiv_pairs_element_doublet_iff. *) 593Theorem equiv_pairs_element_doublet: 594 !f s t. f endo s /\ t IN equiv_pairs f s ==> ?x. x IN pairs f s /\ t = {x; f x} 595Proof 596 rpt strip_tac >> 597 imp_res_tac equiv_pairs_element >> 598 metis_tac[equiv_class_pairs, pairs_element] 599QED 600 601(* Theorem: f endo s /\ t IN equiv_pairs f s ==> CARD t = 2 *) 602(* Proof: 603 Note ?x. x IN pairs f s /\ (t = {x; f x}) by equiv_pairs_element_doublet 604 now f x <> x by pairs_element 605 thus CARD t = 2 by CARD_DEF 606*) 607Theorem equiv_pairs_element_card: 608 !f s t. f endo s /\ t IN equiv_pairs f s ==> CARD t = 2 609Proof 610 rpt strip_tac >> 611 `?x. x IN pairs f s /\ t = {x; f x}` by rw[equiv_pairs_element_doublet] >> 612 `f x <> x` by metis_tac[pairs_element] >> 613 rw[] 614QED 615 616(* Theorem: f endo s ==> BIJ CHOICE (equiv_fixes f s) (fixes f s) *) 617(* Proof: 618 By BIJ_DEF, this is to show: 619 (1) x IN equiv_fixes f s ==> CHOICE x IN fixes f s 620 Note ?y. (x = {y}) /\ y IN fixes f s by equiv_fixes_element_sing_iff 621 so CHOICE x = y by CHOICE_SING 622 thus true. 623 (2) x IN equiv_fixes f s /\ y IN equiv_fixes f s /\ CHOICE x = CHOICE y ==> x = y 624 Note ?u. x = {u} by equiv_fixes_element_sing_iff 625 and ?v. y = {v} by equiv_fixes_element_sing_iff 626 so CHOICE x = u by CHOICE_SING 627 and CHOICE y = v by CHOICE_SING 628 Thus u = v, and x = y by EXTENSION 629 (3) same as (1). 630 (4) x IN fixes f s ==> ?y. y IN equiv_fixes f s /\ (CHOICE y = x) 631 Let y = {x}, then CHOICE y = x by CHOICE_SING 632 and y IN equiv_fixes f s by equiv_fixes_element_sing_iff 633*) 634Theorem equiv_fixes_fixes_bij: 635 !f s. f endo s ==> BIJ CHOICE (equiv_fixes f s) (fixes f s) 636Proof 637 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >> 638 metis_tac[equiv_fixes_element_sing_iff, CHOICE_SING] 639QED 640 641(* Theorem: FINITE s /\ f endo s ==> CARD (equiv_fixes f s) = CARD (fixes f s) *) 642(* Proof: 643 Note (fixes f s) SUBSET s by fixes_subset 644 so FINITE (fixes f s) by SUBSET_FINITE 645 Now BIJ CHOICE (equiv_fixes f s) (fixes f s) by equiv_fixes_fixes_bij 646 so ?g. BIJ g (fixes f s) (equiv_fixes f s) by BIJ_INV 647 ==> CARD (equiv_fixes f s) = CARD (fixes f s) by FINITE_BIJ_CARD 648*) 649Theorem equiv_fixes_card: 650 !f s. FINITE s /\ f endo s ==> CARD (equiv_fixes f s) = CARD (fixes f s) 651Proof 652 rpt strip_tac >> 653 `FINITE (fixes f s)` by metis_tac[fixes_subset, SUBSET_FINITE] >> 654 `BIJ CHOICE (equiv_fixes f s) (fixes f s)` by rw[equiv_fixes_fixes_bij] >> 655 metis_tac[FINITE_BIJ_CARD, BIJ_INV] 656QED 657 658(* Theorem: FINITE s ==> FINITE (equiv_fixes f s)` *) 659(* Proof: 660 Let g = equiv_class (pair_by f) s. 661 Note equiv_fixes f s = IMAGE g (fixes f s) by equiv_fixes_def 662 now FINITE (fixes f s) by fixes_finite 663 so FINITE (equiv_fixes f s) by IMAGE_FINITE 664*) 665Theorem equiv_fixes_finite: 666 !f s. FINITE s ==> FINITE (equiv_fixes f s) 667Proof 668 rw[equiv_fixes_def, fixes_finite, IMAGE_FINITE] 669QED 670 671(* Theorem: FINITE s ==> FINITE (equiv_pairs f s)` *) 672(* Proof: 673 Let g = equiv_class (pair_by f) s. 674 Note equiv_pairs f s = IMAGE g (pairs f s) by equiv_pairs_def 675 now FINITE (pairs f s) by pairs_finite 676 so FINITE (equiv_pairs f s) by IMAGE_FINITE 677*) 678Theorem equiv_pairs_finite: 679 !f s. FINITE s ==> FINITE (equiv_pairs f s) 680Proof 681 rw[equiv_pairs_def, pairs_finite, IMAGE_FINITE] 682QED 683 684(* Theorem: f involute s ==> PAIR_DISJOINT (equiv_fixes f s) *) 685(* Proof: 686 Let R = pair_by f. 687 Note R equiv_on s by fpair_equiv 688 so PAIR_DISJOINT (partition R s) by partition_elements_disjoint 689 But (equiv_fixes f s) SUBSET (partition R s) by equiv_fixes_subset 690 so PAIR_DISJOINT (equiv_fixes f s) by pair_disjoint_subset 691*) 692Theorem equiv_fixes_pair_disjoint: 693 !f s. f involute s ==> PAIR_DISJOINT (equiv_fixes f s) 694Proof 695 ntac 3 strip_tac >> 696 qabbrev_tac `R = pair_by f` >> 697 `R equiv_on s` by rw[fpair_equiv, Abbr`R`] >> 698 `PAIR_DISJOINT (partition R s)` by metis_tac[partition_elements_disjoint] >> 699 `(equiv_fixes f s) SUBSET (partition R s)` by rw[equiv_fixes_subset, Abbr`R`] >> 700 prove_tac[pair_disjoint_subset] 701QED 702 703(* Theorem: f involute s ==> PAIR_DISJOINT (equiv_pairs f s) *) 704(* Proof: 705 Let R = pair_by f. 706 Note R equiv_on s by fpair_equiv 707 so PAIR_DISJOINT (partition R s) by partition_elements_disjoint 708 But (equiv_pairs f s) SUBSET (partition R s) by equiv_pairs_subset 709 so PAIR_DISJOINT (equiv_pairs f s) by pair_disjoint_subset 710*) 711Theorem equiv_pairs_pair_disjoint: 712 !f s. f involute s ==> PAIR_DISJOINT (equiv_pairs f s) 713Proof 714 ntac 3 strip_tac >> 715 qabbrev_tac `R = pair_by f` >> 716 `R equiv_on s` by rw[fpair_equiv, Abbr`R`] >> 717 `PAIR_DISJOINT (partition R s)` by metis_tac[partition_elements_disjoint] >> 718 `(equiv_pairs f s) SUBSET (partition R s)` by rw[equiv_pairs_subset, Abbr`R`] >> 719 prove_tac[pair_disjoint_subset] 720QED 721 722(* Theorem: FINITE s /\ f involute s ==> EVEN (CARD (BIGUNION (equiv_pairs f s))) *) 723(* Proof: 724 Let c = equiv_pairs f s. 725 Then FINITE c by equiv_pairs_finite 726 Note !t. t IN c ==> ?x. x IN pairs f s /\ (t = {x; f x}) 727 by equiv_pairs_element_doublet 728 also f x <> x by pairs_element 729 Thus !t. t IN c ==> FINITE t /\ (CARD t = 2) 730 by doublet_finite, doublet_card 731 also PAIR_DISJOINT c by equiv_pairs_pair_disjoint 732 CARD (BIGUNION c) 733 = 2 * CARD c by CARD_BIGUNION_SAME_SIZED_SETS 734 Thus EVEN (CARD (BIGUNION c)) by EVEN_DOUBLE 735*) 736Theorem equiv_pairs_bigunion_card_even: 737 !f s. FINITE s /\ f involute s ==> EVEN (CARD (BIGUNION (equiv_pairs f s))) 738Proof 739 rpt strip_tac >> 740 qabbrev_tac `c = equiv_pairs f s` >> 741 `FINITE c` by rw[equiv_pairs_finite, Abbr`c`] >> 742 `!t. t IN c ==> ?x. (t = {x; f x}) /\ (f x <> x)` by metis_tac[equiv_pairs_element_doublet, pairs_element] >> 743 `!t. t IN c ==> FINITE t /\ (CARD t = 2)` by metis_tac[doublet_finite, doublet_card] >> 744 `PAIR_DISJOINT c` by metis_tac[equiv_pairs_pair_disjoint] >> 745 `CARD (BIGUNION c) = CARD c * 2` by rw[CARD_BIGUNION_SAME_SIZED_SETS] >> 746 `_ = 2 * CARD c` by simp[] >> 747 rw[EVEN_DOUBLE] 748QED 749 750(* Theorem: f endo s ==> equiv_fixes f s = IMAGE (\x. {x}) (fixes f s) *) 751(* Proof: 752 Let g = \x. {x}. 753 t IN equiv_fixes f s 754 <=> ?x. x IN fixes f s /\ (t = {x}) by equiv_fixes_element_sing_iff 755 <=> ?x. x IN fixes f x /\ (t = g x) by notation 756 <=> t IN IMAGE g (fixes f s) by IN_IMAGE 757*) 758Theorem equiv_fixes_by_image: 759 !f s. f endo s ==> equiv_fixes f s = IMAGE (\x. {x}) (fixes f s) 760Proof 761 rpt strip_tac >> 762 qabbrev_tac `g = \x. {x}` >> 763 `!x. g x = {x}` by rw[Abbr`g`] >> 764 rw_tac bool_ss[EXTENSION] >> 765 metis_tac[equiv_fixes_element_sing_iff, IN_IMAGE] 766QED 767 768(* Theorem: f endo s ==> equiv_pairs f s = IMAGE (\x. {x; f x}) (pairs f s) *) 769(* Proof: 770 Let g = \x. {x; f x}. 771 t IN equiv_pairs f s 772 <=> ?x. x IN pairs f s /\ (t = {x; f x}) by equiv_pairs_element_doublet_iff 773 <=> ?x. x IN pairs f s /\ (t = g x) by notation 774 <=> t IN IMAGE g (pairs f s) by IN_IMAGE 775*) 776Theorem equiv_pairs_by_image: 777 !f s. f endo s ==> equiv_pairs f s = IMAGE (\x. {x; f x}) (pairs f s) 778Proof 779 rpt strip_tac >> 780 qabbrev_tac `g = \x. {x; f x}` >> 781 `!x. g x = {x; f x}` by rw[Abbr`g`] >> 782 rw_tac bool_ss[EXTENSION] >> 783 metis_tac[equiv_pairs_element_doublet_iff, IN_IMAGE] 784QED 785 786(* Theorem: f endo s ==> BIGUNION (equiv_fixes f s) = fixes f s *) 787(* Proof: 788 BIGUNION (equiv_fixes f s) 789 = BIGUNION (IMAGE (\x. {x}) (fixes f s)) by equiv_fixes_by_image 790 = fixes f s by BIGUNION_ELEMENTS_SING 791*) 792Theorem equiv_fixes_bigunion: 793 !f s. f endo s ==> BIGUNION (equiv_fixes f s) = fixes f s 794Proof 795 rw[equiv_fixes_by_image, BIGUNION_ELEMENTS_SING] 796QED 797 798(* Theorem: f involute s ==> 799 DISJOINT (BIGUNION (equiv_fixes f s)) (BIGUNION (equiv_pairs f s)) *) 800(* Proof: 801 By contradiction, this is to show that the following is impossible: 802 x IN a /\ x IN b /\ a IN equiv_fixes f s /\ b IN equiv_pairs f s 803 Note ?y. y IN fixes f s /\ (a = {y}) by equiv_fixes_element_sing 804 and ?z. z IN pairs f s /\ (b = {z; f z}) by equiv_pairs_element_doublet 805 also y IN s /\ f y = y by fixes_element 806 and z IN s /\ f z <> z by pairs_element 807 Now x IN a = {y} ==> x = y by IN_SING 808 and x IN b = {z; f z} ==> x = z \/ x = f z by EXTENSION 809 If x = z, 810 then z = y, and f y <> y is a contradiction. 811 If x = f z, 812 then f z = y = f y = f x = f (f z) = z by f involute s 813 and f z = z is a contradiction. 814*) 815Theorem equiv_fixes_pairs_bigunion_disjoint: 816 !f s. f involute s ==> 817 DISJOINT (BIGUNION (equiv_fixes f s)) (BIGUNION (equiv_pairs f s)) 818Proof 819 rw[DISJOINT_DEF, BIGUNION, EXTENSION] >> 820 spose_not_then strip_assume_tac >> 821 `?y. y IN fixes f s /\ (s' = {y})` by rw[equiv_fixes_element_sing] >> 822 `?z. z IN pairs f s /\ (s'' = {z; f z})` by rw[equiv_pairs_element_doublet] >> 823 `y IN s /\ (f y = y)` by metis_tac[fixes_element] >> 824 `z IN s /\ (f z <> z)` by metis_tac[pairs_element] >> 825 `x = y` by fs[] >> 826 `(x = z) \/ (x = f z)` by fs[] >> 827 metis_tac[] 828QED 829 830(* Note: 831equiv_fixes_pairs_disjoint 832|- !f s. DISJOINT (equiv_fixes f s) (equiv_pairs f s) 833 834In general, DISJOINT s t cannot imply DISJOINT (BIGUNION s) (BIGUNION t): 835s = { {a,b,x}, {d,e,f}} BIGUNION s = {a,b,x,d,e,f} 836t = { {A,B,C}, {x,E,F}} BIGUNION t = {A,B,C,x,E,F} 837*) 838 839(* Theorem: f involute s ==> 840 s = BIGUNION (equiv_fixes f s) UNION BIGUNION (equiv_pairs f s) *) 841(* Proof: 842 Let R = pair_by f, 843 a = fixes f s, ea = equiv_fixes f s, 844 b = pairs f s, eb = equiv_pairs f s. 845 then BIGUNION (partition R s) 846 = BIGUNION (ea UNION eb) by equiv_fixes_pairs_union 847 = (BIGUNION ea) UNION (BIGUNION eb) by BIGUNION_UNION 848 and DISJOINT (BIGUNION ea) (BIGUNION eb) by equiv_fixes_pairs_bigunion_disjoint 849 Now R equiv_on s by fpair_equiv 850 so s = BIGUNION (partition R s) by BIGUNION_partition 851 Hence s == BIGUNION ea UNION BIGUNION eb. 852*) 853Theorem equiv_fixes_pairs_bigunion_union: 854 !f s. f involute s ==> 855 s = BIGUNION (equiv_fixes f s) UNION BIGUNION (equiv_pairs f s) 856Proof 857 rpt strip_tac >> 858 qabbrev_tac `R = pair_by f` >> 859 `R equiv_on s` by rw[fpair_equiv, Abbr`R`] >> 860 `s = BIGUNION (partition R s)` by rw[BIGUNION_partition] >> 861 `_ = BIGUNION ((equiv_fixes f s) UNION (equiv_pairs f s))` by rw[equiv_fixes_pairs_union, Abbr`R`] >> 862 fs[BIGUNION_UNION] 863QED 864 865(* Theorem: f involute s ==> 866 s =|= (BIGUNION (equiv_fixes f s)) # (BIGUNION (equiv_pairs f s)) *) 867(* Proof: by equiv_fixes_pairs_bigunion_union, equiv_fixes_pairs_bigunion_disjoint *) 868Theorem equiv_fixes_pairs_bigunion_split: 869 !f s. f involute s ==> 870 s =|= (BIGUNION (equiv_fixes f s)) # (BIGUNION (equiv_pairs f s)) 871Proof 872 metis_tac[equiv_fixes_pairs_bigunion_union, equiv_fixes_pairs_bigunion_disjoint] 873QED 874 875(* Theorem: f involute s ==> BIGUNION (equiv_pairs f s) = pairs f s *) 876(* Proof: 877 Let a = fixes f s, u = BIGUNION (equiv_fixes f s), 878 b = pairs f s, v = BIGUNION (equiv_pairs f s). 879 Note s =|= u # v by equiv_fixes_pairs_bigunion_split 880 and s =|= a # b by fixes_pairs_split 881 v 882 = s DIFF u by SPLIT_EQ_DIFF 883 = s DIFF a by equiv_fixes_bigunion 884 = b by SPLIT_EQ_DIFF 885*) 886Theorem equiv_pairs_bigunion: 887 !f s. f involute s ==> BIGUNION (equiv_pairs f s) = pairs f s 888Proof 889 rpt strip_tac >> 890 qabbrev_tac `a = fixes f s` >> 891 qabbrev_tac `b = pairs f s` >> 892 qabbrev_tac `u = BIGUNION (equiv_fixes f s)` >> 893 qabbrev_tac `v = BIGUNION (equiv_pairs f s)` >> 894 `s =|= u # v` by rw[equiv_fixes_pairs_bigunion_split, Abbr`u`, Abbr`v`] >> 895 `s =|= a # b` by rw[fixes_pairs_split, Abbr`a`, Abbr`b`] >> 896 metis_tac[SPLIT_EQ_DIFF, equiv_fixes_bigunion] 897QED 898 899(* This is an indirect proof. A direct proof is desirable. *) 900 901(* Theorem: f involute s ==> BIGUNION (equiv_pairs f s) = pairs f s *) 902(* Proof: 903 Let b = pairs f s, eb = equiv_pairs f s. 904 This is to show: BIGUNION eb = b. 905 First, show BIGUNION eb SUBSET b. 906 By SUBSET_DEF, this is to show: 907 x IN t /\ t IN eb ==> x IN b. 908 Note ?z. z IN b /\ t = {z; f z} by equiv_pairs_element_doublet 909 Thus x = z or z = f z. 910 If x = z, then x IN b. 911 If x = f z, then x IN b by involute_pairs_element_pair 912 Hence BIGUNION eb SUBSET b by SUBSET_DEF 913 Next, show b SUBSET BIGUNION eb. 914 By SUBSET_DEF, this is to show: 915 x IN b ==> ?s. x IN s /\ s IN eb 916 Let s = {x; f x}. 917 Note s IN eb by equiv_pairs_element_doublet_iff 918 and x IN s by EXTENSION 919 Hence b SUBSET (BIGUNION eb) by SUBSET_DEF 920 921 Therefore, BIGUNION eb = b by SUBSET_ANTISYM 922*) 923Theorem equiv_pairs_bigunion: 924 !f s. f involute s ==> BIGUNION (equiv_pairs f s) = pairs f s 925Proof 926 rpt strip_tac >> 927 qabbrev_tac `b = pairs f s` >> 928 qabbrev_tac `eb = equiv_pairs f s` >> 929 irule SUBSET_ANTISYM >> 930 rw[SUBSET_DEF] >| [ 931 `?z. z IN b /\ s' = {z; f z}` by rw[equiv_pairs_element_doublet, Abbr`b`, Abbr`eb`] >> 932 `x = z \/ x = f z` by fs[] >- 933 simp[] >> 934 metis_tac[involute_pairs_element_pair], 935 qexists_tac `{x; f x}` >> 936 simp[] >> 937 metis_tac[equiv_pairs_element_doublet_iff] 938 ] 939QED 940 941(* Theorem: FINITE s /\ f involute s ==> EVEN (CARD (pairs f s)) *) 942(* Proof: 943 Note BIGUNION (equiv_pairs f s) = pairs f s by equiv_pairs_bigunion 944 and EVEN (CARD (BIGUNION (equiv_pairs f s))) by equiv_pairs_bigunion_card_even 945 Thus EVEN (CARD (pairs f s)). 946*) 947Theorem pairs_card_even: 948 !f s. FINITE s /\ f involute s ==> EVEN (CARD (pairs f s)) 949Proof 950 rw[GSYM equiv_pairs_bigunion, equiv_pairs_bigunion_card_even] 951QED 952 953(* Theorem: FINITE s /\ f involute s ==> (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) *) 954(* Proof: 955 Note s =|= (fixes f s) # (pairs f s) by fixes_pairs_split 956 so CARD s = CARD (fixes f s) + CARD (pairs f s) by SPLIT_CARD 957 But EVEN (CARD (pairs f s)) by pairs_card_even 958 Thus EVEN (CARD s) <=> EVEN (CARD (fixes f s)) by EVEN_ADD 959*) 960Theorem involute_set_fixes_both_even: 961 !f s. FINITE s /\ f involute s ==> (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) 962Proof 963 rpt strip_tac >> 964 `CARD s = CARD (fixes f s) + CARD (pairs f s)` by rw[fixes_pairs_split, SPLIT_CARD] >> 965 `EVEN (CARD (pairs f s))` by rw[pairs_card_even] >> 966 metis_tac[EVEN_ADD] 967QED 968 969(* Theorem: FINITE s /\ f involute s ==> (ODD (CARD s) <=> ODD (CARD (fixes f s))) *) 970(* Proof: by involute_set_fixes_both_even, ODD_EVEN. *) 971Theorem involute_set_fixes_both_odd: 972 !f s. FINITE s /\ f involute s ==> (ODD (CARD s) <=> ODD (CARD (fixes f s))) 973Proof 974 rw[involute_set_fixes_both_even, ODD_EVEN] 975QED 976 977(* ------------------------------------------------------------------------- *) 978(* Reformulate using mates *) 979(* ------------------------------------------------------------------------- *) 980 981(* Define mates of involution *) 982Definition mates_def: 983 mates f s = s DIFF (fixes f s) 984End 985 986(* Theorem: x IN mates f s <=> x IN s /\ f x <> x *) 987(* Proof: by mates_def, fixes_def, IN_DIFF *) 988Theorem mates_element: 989 !f s x. x IN mates f s <=> x IN s /\ f x <> x 990Proof 991 rw[mates_def, fixes_def] >> 992 metis_tac[] 993QED 994 995(* Theorem: mates f s SUBSET s *) 996(* Proof: by mates_element, SUBSET_DEF *) 997Theorem mates_subset: 998 !f s. mates f s SUBSET s 999Proof 1000 simp[mates_element, SUBSET_DEF] 1001QED 1002 1003(* Theorem: FINITE s ==> FINITE (mates f s) *) 1004(* Proof: by mates_subset, SUBSET_FINITE *) 1005Theorem mates_finite: 1006 !f s. FINITE s ==> FINITE (mates f s) 1007Proof 1008 metis_tac[mates_subset, SUBSET_FINITE] 1009QED 1010 1011(* Theorem: s = (fixes f s) UNION (mates f s) *) 1012(* Proof: 1013 Note (mates f s) = s DIFF (fixes f s) by mates_def 1014 and (fixes f s) SUBSET s by fixes_subset 1015 Thus s = (fixes f s) UNION (mates f s) by UNION_DIFF 1016*) 1017Theorem mates_fixes_union: 1018 !f s. s = (mates f s) UNION (fixes f s) 1019Proof 1020 simp[mates_def, fixes_subset, UNION_DIFF] 1021QED 1022 1023(* Theorem: DISJOINT (mates f s) (fixes f s) *) 1024(* Proof: by mates_def, DISJOINT_DIFF *) 1025Theorem mates_fixes_disjoint: 1026 !f s. DISJOINT (mates f s) (fixes f s) 1027Proof 1028 simp[mates_def, DISJOINT_DIFF] 1029QED 1030 1031(* Theorem: FINITE s ==> CARD s = CARD (mates f s) + CARD (fixes f s) *) 1032(* Proof: 1033 Let a = mates f s, b = fixes f s. 1034 Then s = a UNION b by mates_fixes_union 1035 and DISJOINT a b by mates_fixes_disjoint 1036 and FINITE a by fixes_finite 1037 and FINITE b by mates_finite 1038 Thus CARD s = CARD a + CARD b by CARD_UNION_DISJOINT 1039*) 1040Theorem mates_fixes_card: 1041 !f s. FINITE s ==> CARD s = CARD (mates f s) + CARD (fixes f s) 1042Proof 1043 metis_tac[fixes_finite, mates_finite, 1044 mates_fixes_union, mates_fixes_disjoint, CARD_UNION_DISJOINT] 1045QED 1046 1047(* Theorem: f involute s ==> f involute (mates f s) *) 1048(* Proof: by mates_element *) 1049Theorem involute_mates: 1050 !f s. f involute s ==> f involute (mates f s) 1051Proof 1052 simp[mates_element] 1053QED 1054 1055(* Theorem: f involute s /\ x IN mates f s ==> f x IN mates f s *) 1056(* Proof: by mates_element *) 1057Theorem involute_mates_partner: 1058 !f s x. f involute s /\ x IN mates f s ==> f x IN mates f s 1059Proof 1060 simp[mates_element] 1061QED 1062 1063(* Theorem: f involute s ==> (pair_by f) equiv_on (mates f s) *) 1064(* Proof: 1065 By equiv_on_def, this is to show: 1066 (1) x IN mates f s ==> pair_by f x x 1067 True by fpair_refl 1068 (2) x IN mates f s /\ y IN mates f s ==> pair_by f y x <=> pair_by f x y 1069 True by mates_element, fpair_sym 1070 (3) x IN mates f s /\ x' IN mates f s /\ y IN mates f s /\ 1071 pair_by f x x' /\ pair_by f x' y ==> pair_by f x y 1072 True by mates_element, fpair_trans 1073*) 1074Theorem fpair_equiv_on_mates: 1075 !f s. f involute s ==> (pair_by f) equiv_on (mates f s) 1076Proof 1077 rw[equiv_on_def] >- 1078 simp[fpair_refl] >- 1079 metis_tac[mates_element, fpair_sym] >> 1080 metis_tac[mates_element, fpair_trans] 1081QED 1082 1083(* Theorem: f involute s ==> 1084 (t IN partition (pair_by f) (mates f s) <=> 1085 ?x. x IN (mates f s) /\ t = {x; f x}) *) 1086(* Proof: 1087 By partition_def, this is to show: 1088 ?x. x IN mates f s /\ (t = {y | y IN mates f s /\ pair_by f x y}) 1089 <=> ?x. x IN mates f s /\ (t = {x; f x}) 1090 {y | y IN mates f s /\ pair_by f x y} 1091 = {y | y IN mates f s /\ (y = x \/ y = f x)} by fpair_def 1092 = {x; f x} by mates_element, f x <> x 1093*) 1094Theorem mates_partition_element_doublet: 1095 !f s t. f involute s ==> 1096 (t IN partition (pair_by f) (mates f s) <=> 1097 ?x. x IN (mates f s) /\ t = {x; f x}) 1098Proof 1099 rw[partition_def, fpair_def, EXTENSION] >> 1100 metis_tac[mates_element] 1101QED 1102 1103(* Theorem: FINITE s /\ f involute s /\ 1104 t IN partition (pair_by f) (mates f s) ==> CARD t = 2 *) 1105(* Proof: 1106 Note ?x. x IN (mates f s) /\ (t = {x; f x}) by mates_partition_element_doublet 1107 and f x <> x by mates_element 1108 thus CARD t = 2 by CARD_DEF 1109*) 1110Theorem mates_partition_element_card: 1111 !f s t. FINITE s /\ f involute s /\ 1112 t IN partition (pair_by f) (mates f s) ==> CARD t = 2 1113Proof 1114 rpt strip_tac >> 1115 `?x. x IN (mates f s) /\ (t = {x; f x})` by rw[GSYM mates_partition_element_doublet] >> 1116 fs[mates_element] 1117QED 1118 1119(* Theorem: FINITE s /\ f involute s ==> EVEN (CARD (mates f s)) *) 1120(* Proof: 1121 Let R = pair_by f, t = mates f s. 1122 Note FINITE t by mates_finite 1123 and R equiv_on t by fpair_equiv_on_mates 1124 and !e. e IN (partition R t) ==> (CARD e = 2) 1125 by mates_partition_element_card 1126 Thus CARD t = 2 * CARD (partition R t) 1127 by equal_partition_card 1128 so EVEN (CARD t) by EVEN_DOUBLE 1129*) 1130Theorem mates_card_even: 1131 !f s. FINITE s /\ f involute s ==> EVEN (CARD (mates f s)) 1132Proof 1133 rpt strip_tac >> 1134 qabbrev_tac `t = mates f s` >> 1135 `!e. e IN partition (\x y. pair_by f x y) t ==> (CARD e = 2)` by metis_tac[mates_partition_element_card] >> 1136 qabbrev_tac `R = pair_by f` >> 1137 `FINITE t` by rw[mates_finite, Abbr`t`] >> 1138 `R equiv_on t` by rw[fpair_equiv_on_mates, Abbr`R`, Abbr`t`] >> 1139 `CARD t = 2 * CARD (partition R t)` by rw[equal_partition_card] >> 1140 fs[EVEN_DOUBLE] 1141QED 1142 1143(* Theorem: FINITE s /\ f involute s ==> (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) *) 1144(* Proof: 1145 Let a = CARD s, b = CARD (mates f s), c = CARD (fixes f s). 1146 Then a = b + c by mates_fixes_card 1147 and EVEN b by mates_card_even 1148 Thus EVEN a <=> EVEN c by EVEN_ADD 1149*) 1150Theorem involute_set_fixes_both_even: 1151 !f s. FINITE s /\ f involute s ==> (EVEN (CARD s) <=> EVEN (CARD (fixes f s))) 1152Proof 1153 rpt strip_tac >> 1154 qabbrev_tac `a = CARD s` >> 1155 qabbrev_tac `b = CARD (mates f s)` >> 1156 qabbrev_tac `c = CARD (fixes f s)` >> 1157 `a = b + c` by rw[mates_fixes_card, Abbr`a`, Abbr`b`, Abbr`c`] >> 1158 `EVEN b` by rw[mates_card_even, Abbr`b`] >> 1159 metis_tac[EVEN_ADD] 1160QED 1161 1162(* This proof is much better! *) 1163 1164(* ------------------------------------------------------------------------- *) 1165(* Two Involutions *) 1166(* ------------------------------------------------------------------------- *) 1167 1168(* Theorem: FINITE s /\ f involute s /\ g involute s ==> 1169 (EVEN (CARD (fixes f s)) <=> EVEN (CARD (fixes g s))) *) 1170(* Proof: 1171 EVEN (CARD (fixes f s) 1172 <=> EVEN (CARD s) by involute_set_fixes_both_even 1173 <=> EVEN (CARD (fixes g s)) by involute_set_fixes_both_even 1174*) 1175Theorem involute_two_fixes_both_even: 1176 !f g s. FINITE s /\ f involute s /\ g involute s ==> 1177 (EVEN (CARD (fixes f s)) <=> EVEN (CARD (fixes g s))) 1178Proof 1179 metis_tac[involute_set_fixes_both_even] 1180QED 1181 1182(* Theorem: FINITE s /\ f involute s /\ g involute s ==> 1183 (ODD (CARD (fixes f s)) <=> ODD (CARD (fixes g s))) *) 1184(* Proof: by involute_two_fixes_both_even, ODD_EVEN. *) 1185Theorem involute_two_fixes_both_odd: 1186 !f g s. FINITE s /\ f involute s /\ g involute s ==> 1187 (ODD (CARD (fixes f s)) <=> ODD (CARD (fixes g s))) 1188Proof 1189 rw[involute_two_fixes_both_even, ODD_EVEN] 1190QED 1191 1192 1193(* ------------------------------------------------------------------------- *) 1194 1195(* export theory at end *) 1196val _ = export_theory(); 1197 1198(*===========================================================================*) 1199