1(* ------------------------------------------------------------------------- *) 2(* Symmetry Group. *) 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 "symmetryGroup"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* open dependent theories *) 21open pred_setTheory arithmeticTheory; 22 23(* Get dependent theories local *) 24(* val _ = load "groupTheory"; *) 25open groupTheory monoidTheory; 26open monoidOrderTheory; 27 28(* val _ = load "subgroupTheory"; *) 29open submonoidTheory; 30open subgroupTheory; 31open monoidMapTheory groupMapTheory; 32 33(* Get dependent theories in lib *) 34(* (* val _ = load "helperSetTheory"; loaded by monoidTheory *) *) 35open helperSetTheory; 36 37(* Load dependent theories *) 38(* val _ = load "Satisfysimps"; *) 39(* used in coset_id_eq_subgroup: srw_tac[SatisfySimps.SATISFY_ss] *) 40 41(* val _ = load "groupCyclicTheory"; *) 42open groupCyclicTheory groupInstancesTheory; 43 44 45(* ------------------------------------------------------------------------- *) 46(* Symmetry Group Documentation *) 47(* ------------------------------------------------------------------------- *) 48(* Overloading (# is temporary): 49*) 50(* Definitions and Theorems (# are exported): 51 52 Helper Theorems: 53 54 Function on a Set 55 on_def |- !f s. (f on s) = (\x. if x IN s then f x else ARB) 56 fun_on_eq |- !f1 f2 s. (f1 on s) = (f2 on s) <=> !x. x IN s ==> f1 x = f2 x 57 fun_on_element |- !f s t x. x IN s /\ f x IN t ==> (f on s) x IN t 58 fun_on_on |- !f s. ((f on s) on s) = (f on s) 59 fun_on_compose |- !f1 f2 s. (!x. x IN s ==> f2 x IN s) ==> 60 ((f1 on s) o (f2 on s) on s) = (f1 o f2 on s) 61 fun_on_compose_assoc |- !f1 f2 f3 s. (!x. x IN s ==> f3 x IN s) ==> 62 ((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s) 63 64 bij_on_bij |- !f s t. BIJ f s t ==> BIJ (f on s) s t 65 bij_on_compose_bij |- !f g s t u. BIJ f s t /\ BIJ g t u ==> BIJ (g o f on s) s u 66 bij_on_compose |- !f1 f2 s. f2 PERMUTES s ==> ((f1 on s) o (f2 on s) on s) = (f1 o f2 on s) 67 bij_on_compose_assoc |- !f1 f2 f3 s. f3 PERMUTES s ==> ((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s) 68 bij_on_id |- !s. (I on s) PERMUTES s 69 bij_on_inv |- !f s. f PERMUTES s ==> (LINV f s o f on s) = (I on s) 70 71 Symmetric Group: 72 symmetric_group_def |- !s. symmetric_group s = 73 <|carrier := {f on s | f | f PERMUTES s}; 74 op := (\f1 f2. f1 o f2 on s); 75 id := (I on s) 76 |> 77 symmetric_group_group |- !s. Group (symmetric_group s) 78 79 Maps restricted on a Set: 80 monoid_homo_on_homo |- !g h f. Monoid g /\ MonoidHomo f g h ==> MonoidHomo (f on G) g h 81 monoid_iso_on_iso |- !g h f. Monoid g /\ MonoidIso f g h ==> MonoidIso (f on G) g h 82 monoid_auto_on_auto |- !g f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (f on G) g 83 monoid_auto_on_id |- !g. Monoid g ==> MonoidAuto (I on G) g 84 group_homo_on_homo |- !g h f. Group g /\ GroupHomo f g h ==> GroupHomo (f on G) g h 85 group_iso_on_iso |- !g h f. Group g /\ GroupIso f g h ==> GroupIso (f on G) g h 86 group_auto_on_auto |- !g f. Group g /\ GroupAuto f g ==> GroupAuto (f on G) g 87 group_auto_on_id |- !g. Group g ==> GroupAuto (I on G) g 88 89 Automorphism Group: 90 automorphism_group_def |- !g. automorphism_group g = 91 <|carrier := {f on G | f | GroupAuto f g}; 92 op := (\f1 f2. f1 o f2 on G); 93 id := (I on G)|> 94 automorphism_group_group |- !g. Group g ==> Group (automorphism_group g) 95 96*) 97 98(* ------------------------------------------------------------------------- *) 99(* Helper Theorems *) 100(* ------------------------------------------------------------------------- *) 101 102(* ------------------------------------------------------------------------- *) 103(* Function on a Set *) 104(* ------------------------------------------------------------------------- *) 105 106(* Function with domain on a set *) 107(* val _ = overload_on("on", ``\(f:'a -> 'b) (s:'a -> bool) x. if x IN s then f x else ARB``); *) 108val on_def = Define` 109 on (f:'a -> 'b) (s:'a -> bool) = (\x. if x IN s then f x else ARB) 110`; 111(* make this an infix operator *) 112val _ = set_fixity "on" (Infix(NONASSOC, 450)); (* same as relation *) 113 114(* Theorem: ((f1 on s) = (f2 on s)) <=> (!x. x IN s ==> (f1 x <=> f2 x)) *) 115(* Proof: by on_def *) 116val fun_on_eq = store_thm( 117 "fun_on_eq", 118 ``!(f1 f2):'a -> 'b. !s. ((f1 on s) = (f2 on s)) <=> (!x. x IN s ==> (f1 x = f2 x))``, 119 rw[on_def, EQ_IMP_THM] >> 120 metis_tac[]); 121 122(* Theorem: x IN s /\ f x IN t ==> (f on s) x IN t *) 123(* Proof: by on_def *) 124val fun_on_element = store_thm( 125 "fun_on_element", 126 ``!f:'a -> 'b. !s t x. x IN s /\ f x IN t ==> (f on s) x IN t``, 127 rw_tac std_ss[on_def]); 128 129(* Theorem: ((f on s) on s) = (f on s) *) 130(* Proof: by on_def *) 131val fun_on_on = store_thm( 132 "fun_on_on", 133 ``!(f:'a -> 'b) s. ((f on s) on s) = (f on s)``, 134 rw_tac std_ss[on_def]); 135 136(* Theorem: (!x. x IN s ==> f2 x IN s) ==> ((((f1 on s) o (f2 on s)) on s) = ((f1 o f2) on s)) *) 137(* Proof: by on_def *) 138val fun_on_compose = store_thm( 139 "fun_on_compose", 140 ``!(f1 f2):'a -> 'a. !s. (!x. x IN s ==> f2 x IN s) ==> 141 ((((f1 on s) o (f2 on s)) on s) = ((f1 o f2) on s))``, 142 rw[on_def, FUN_EQ_THM]); 143 144(* Theorem: (!x. x IN s ==> f3 x IN s) ==> 145 (((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s)) *) 146(* Proof: by on_def, FUN_EQ_THM *) 147val fun_on_compose_assoc = store_thm( 148 "fun_on_compose_assoc", 149 ``!(f1 f2 f3):'a -> 'a. !(s:'a -> bool). (!x. x IN s ==> f3 x IN s) ==> 150 (((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s))``, 151 rw[on_def, FUN_EQ_THM]); 152 153(* Theorem: BIJ f s t ==> BIJ (f on s) s t *) 154(* Proof: by [BIJ_DEF, INJ_DEF, SURJ_DEF, on_def *) 155val bij_on_bij = store_thm( 156 "bij_on_bij", 157 ``!f:'a -> 'b. !s t. BIJ f s t ==> BIJ (f on s) s t``, 158 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF, on_def] >> 159 metis_tac[]); 160 161(* Theorem: BIJ f s t /\ BIJ g t u ==> BIJ (g o f on s) s u *) 162(* Proof: by BIJ_DEF, INJ_DEF, SURJ_DEF, on_def *) 163val bij_on_compose_bij = store_thm( 164 "bij_on_compose_bij", 165 ``!f g (s:'a -> bool) t u. BIJ f s t /\ BIJ g t u ==> BIJ ((g o f) on s) s u``, 166 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF, on_def] >> 167 metis_tac[]); 168 169(* Theorem: f2 PERMUTES s ==> ((f1 on s) o (f2 on s) on s) = (f1 o f2 on s) *) 170(* Proof: by fun_on_compose, BIJ_ELEMENT *) 171val bij_on_compose = store_thm( 172 "bij_on_compose", 173 ``!(f1 f2):'a -> 'a. !s. f2 PERMUTES s ==> ((f1 on s) o (f2 on s) on s) = (f1 o f2 on s)``, 174 metis_tac[fun_on_compose, BIJ_ELEMENT]); 175 176(* Theorem: f3 PERMUTES s ==> ((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s) *) 177(* Proof: by fun_on_compose_assoc, BIJ_ELEMENT *) 178val bij_on_compose_assoc = store_thm( 179 "bij_on_compose_assoc", 180 ``!(f1 f2 f3):'a -> 'a. !s. f3 PERMUTES s ==> ((f1 o f2 on s) o f3 on s) = (f1 o (f2 o f3 on s) on s)``, 181 metis_tac[fun_on_compose_assoc, BIJ_ELEMENT]); 182 183(* Theorem: (I on s) PERMUTES s *) 184(* Proof: by BIJ_DEF, INJ_DEF, SURJ_DEF, on_def *) 185val bij_on_id = store_thm( 186 "bij_on_id", 187 ``!s. (I on s) PERMUTES s``, 188 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF, on_def] >> 189 metis_tac[]); 190 191(* Theorem: f PERMUTES s ==> (LINV f s o f on s) = (I on s) *) 192(* Proof: by on_def, FUN_EQ_THM, BIJ_DEF, LINV_DEF *) 193val bij_on_inv = store_thm( 194 "bij_on_inv", 195 ``!f (s:'a -> bool). f PERMUTES s ==> (LINV f s o f on s) = (I on s)``, 196 rw[on_def, FUN_EQ_THM] >> 197 rw[] >> 198 metis_tac[BIJ_DEF, LINV_DEF]); 199 200(* ------------------------------------------------------------------------- *) 201(* Symmetric Group *) 202(* ------------------------------------------------------------------------- *) 203 204(* 205Given a finite set s of cardinality n, 206the set of bijections (permutations) form a group under composition, 207called the symmetric group Sym(n), or simply S_n. 208*) 209 210(* Define symmetric group *) 211val symmetric_group_def = Define` 212 symmetric_group (s:'a -> bool) = 213 <| carrier := {f on s | f | f PERMUTES s}; 214 op := (\(f1 f2):'a -> 'a. (f1 o f2) on s); 215 id := (I on s) 216 |> 217`; 218 219(* Theorem: Group (symmetric_group s) *) 220(* Proof: 221 By group_def_alt, sym_group_def, this is to show: 222 (1) f PERMUTES s /\ f' PERMUTES s ==> ?f''. ((f on s) o (f' on s) on s = f'' on s) /\ f'' PERMUTES s 223 Let f'' = (f o f') on s. 224 Then (f on s) o (f' on s) on s = f'' on s by fun_on_compose, fun_on_on, BIJ_ELEMENT 225 and f'' PERMUTES s by bij_on_compose_bij 226 and the other, by FUN_EQ_THM, 227 says: x IN s /\ f' x NOTIN s ==> ARB = f (f' x) 228 The premise is F by BIJ_ELEMENT. 229 (2) f PERMUTES s /\ f' PERMUTES s /\ f'' PERMUTES s ==> 230 ((f on s) o (f' on s) on s) o (f'' on s) on s = (f on s) o ((f' on s) o (f'' on s) on s) on s 231 Note (f on s) PERMUTES s by bij_on_bij 232 and (f' on s) PERMUTES s by bij_on_bij 233 and (f'' on s) PERMUTES s by bij_on_bij 234 The result follows by bij_on_compose_assoc 235 (3) ?f. (I on s = f on s) /\ f PERMUTES s 236 Let f = I. 237 Then I PERMUTES s by BIJ_I_SAME 238 (4) f PERMUTES s ==> (I on s) o (f on s) on s = f on s 239 Note !x. x IN s ==> f x IN s by BIJ_ELEMENT 240 (I on s) o (f on s) on s 241 = (I o f) on s by fun_on_compose 242 = f on s by I_o_ID 243 (5) f PERMUTES s ==> ?y. (?f. (y = f on s) /\ f PERMUTES s) /\ (y o (f on s) on s = I on s) 244 Let y = (LINV f s) on s. Then this is to show: 245 (1) ?f'. (LINV f s on s = f' on s) /\ f' PERMUTES s 246 Let f' = LINV f s. 247 Then f' PERMUTES s by BIJ_LINV_BIJ 248 (2) (LINV f s on s) o (f on s) on s = I on s 249 Note !x. x IN s ==> f x IN s by BIJ_ELEMENT 250 (LINV f s on s) o (f on s) on s 251 = (LINV f s o f) on s by fun_on_compose 252 = I on s by bij_on_inv 253*) 254Theorem symmetric_group_group: 255 !(s:'a -> bool). Group (symmetric_group s) 256Proof 257 rw_tac std_ss[group_def_alt, symmetric_group_def, GSPECIFICATION] >| [ 258 rename [���(f on s) o (f' on s) on s���] >> 259 qexists_tac `(f o f') on s` >> 260 rpt strip_tac 261 >- metis_tac[fun_on_compose, fun_on_on, BIJ_ELEMENT] >> 262 metis_tac[bij_on_compose_bij], 263 metis_tac[bij_on_compose_assoc, bij_on_bij], 264 metis_tac[BIJ_I_SAME], 265 rename [���f PERMUTES s���] >> 266 `!x. x IN s ==> f x IN s` by metis_tac[BIJ_ELEMENT] >> 267 rw[fun_on_compose], 268 rename [���f PERMUTES s���] >> 269 qexists_tac `(LINV f s) on s` >> 270 rpt strip_tac >- metis_tac[BIJ_LINV_BIJ] >> 271 metis_tac[fun_on_compose, bij_on_inv, BIJ_ELEMENT] 272 ] 273QED 274 275(* This is a very good result! *) 276 277(* ------------------------------------------------------------------------- *) 278(* Maps restricted on a Set *) 279(* ------------------------------------------------------------------------- *) 280 281(* Theorem: Monoid g /\ MonoidHomo f g h ==> MonoidHomo (f on G) g h *) 282(* Proof: by MonoidHomo_def, on_def, monoid_op_element, monoid_id_element *) 283val monoid_homo_on_homo = store_thm( 284 "monoid_homo_on_homo", 285 ``!(g:'a monoid) (h:'b monoid). !f. Monoid g /\ MonoidHomo f g h ==> MonoidHomo (f on G) g h``, 286 rw_tac std_ss[MonoidHomo_def, on_def, monoid_op_element, monoid_id_element]); 287 288(* Theorem: Monoid g /\ MonoidIso f g h ==> MonoidIso (f on G) g h *) 289(* Proof: 290 MonoidIso f g h 291 = MonoidHomo f g h /\ BIJ f G h.carrier by MonoidIso_def 292 ==> MonoidHomo f g h /\ BIJ (f on G) G h.carrier by bij_on_bij 293 ==> MonoidHomo (f on G) g h /\ BIJ (f o G) G h.carrier by monoid_homo_on_homo 294 = MonoidIso (f on G) g h by MonoidIso_def 295*) 296val monoid_iso_on_iso = store_thm( 297 "monoid_iso_on_iso", 298 ``!(g:'a monoid) (h:'b monoid). !f. Monoid g /\ MonoidIso f g h ==> MonoidIso (f on G) g h``, 299 rw_tac std_ss[MonoidIso_def, bij_on_bij, monoid_homo_on_homo]); 300 301(* Theorem: Monoid g /\ MonoidAuto f g ==> MonoidAuto (f on G) g *) 302(* Proof: by MonoidAuto_def, monoid_iso_on_iso *) 303val monoid_auto_on_auto = store_thm( 304 "monoid_auto_on_auto", 305 ``!g:'a monoid. !f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (f on G) g``, 306 rw_tac std_ss[MonoidAuto_def, monoid_iso_on_iso]); 307 308(* Theorem: Monoid g ==> MonoidAuto (I on G) g *) 309(* Proof: by monoid_auto_I, monoid_auto_on_auto. *) 310val monoid_auto_on_id = store_thm( 311 "monoid_auto_on_id", 312 ``!(g:'a monoid). Monoid g ==> MonoidAuto (I on G) g``, 313 rw_tac std_ss[monoid_auto_I, monoid_auto_on_auto]); 314 315(* Theorem: Group g /\ GroupHomo f g h ==> GroupHomo (f on G) g h *) 316(* Proof: by GroupHomo_def, on_def, group_op_element *) 317val group_homo_on_homo = store_thm( 318 "group_homo_on_homo", 319 ``!(g:'a group) (h:'b group). !f. Group g /\ GroupHomo f g h ==> GroupHomo (f on G) g h``, 320 rw_tac std_ss[GroupHomo_def, on_def, group_op_element]); 321 322(* Theorem: Group g /\ GroupIso f g h ==> GroupIso (f on G) g h *) 323(* Proof: 324 GroupIso f g h 325 = GroupHomo f g h /\ BIJ f G h.carrier by GroupIso_def 326 ==> GroupHomo f g h /\ BIJ (f on G) G h.carrier by bij_on_bij 327 ==> GroupHomo (f on G) g h /\ BIJ (f o G) G h.carrier by group_homo_on_homo 328 = GroupIso (f on G) g h by GroupIso_def 329*) 330val group_iso_on_iso = store_thm( 331 "group_iso_on_iso", 332 ``!(g:'a group) (h:'b group). !f. Group g /\ GroupIso f g h ==> GroupIso (f on G) g h``, 333 rw_tac std_ss[GroupIso_def, bij_on_bij, group_homo_on_homo]); 334 335(* Theorem: Group g /\ GroupAuto f g ==> GroupAuto (f on G) g *) 336(* Proof: by GroupAuto_def, group_iso_on_iso *) 337val group_auto_on_auto = store_thm( 338 "group_auto_on_auto", 339 ``!g:'a group. !f. Group g /\ GroupAuto f g ==> GroupAuto (f on G) g``, 340 rw_tac std_ss[GroupAuto_def, group_iso_on_iso]); 341 342(* Theorem: Group g ==> GroupAuto (I on G) g *) 343(* Proof: by group_auto_I, group_auto_on_auto *) 344val group_auto_on_id = store_thm( 345 "group_auto_on_id", 346 ``!(g:'a group). Group g ==> GroupAuto (I on G) g``, 347 rw_tac std_ss[group_auto_I, group_auto_on_auto]); 348 349(* ------------------------------------------------------------------------- *) 350(* Automorphism Group *) 351(* ------------------------------------------------------------------------- *) 352 353(* All automorphisms of a Group form a Group. *) 354val automorphism_group_def = Define` 355 automorphism_group (g:'a group) = 356 <| carrier := {f on G | f | GroupAuto f g}; 357 op := \f1 f2. (f1 o f2) on G; 358 id := (I on G) 359 |> 360`; 361 362(* Theorem: Group g ==> Group (automorphism_group g) *) 363(* Proof: 364 By group_def_alt, automorphism_group_def, this is to show: 365 (1) GroupAuto f g /\ GroupAuto f' g ==> ?f''. ((f on G) o (f' on G) on G = f'' on G) /\ GroupAuto f'' g 366 Let f'' = f o f' on G. 367 Note f PERMUTES G /\ f' PERMUTES G by group_auto_bij 368 Then (f on G) o (f' on G) on G = (f o f' on G) on G by bij_on_compose, fun_on_on 369 and GroupAuto (f o f' on G) g by group_auto_compose, group_auto_on_auto 370 (2) GroupAuto f g /\ GroupAuto f' g /\ GroupAuto f'' g ==> 371 ((f on G) o (f' on G) on G) o (f'' on G) on G = (f on G) o ((f' on G) o (f'' on G) on G) on G 372 Note f PERMUTES G /\ f' PERMUTES G /\ f'' PERMUTES G by group_auto_bij 373 The result follows by bij_on_compose_assoc, bij_on_bij 374 (3) ?f. (I on G = f on G) /\ GroupAuto f g 375 Let f = I, then GroupAuto I g by group_auto_I 376 (4) (I on G) o (f on G) on G = f on G 377 Note !x. x IN G ==> f x IN G by group_auto_bij, BIJ_ELEMENT 378 (I on G) o (f on G) on G 379 = (I o f) on G by fun_on_compose 380 = f on G by I_o_ID 381 (5) GroupAuto f g ==> ?y. (?f. (y = f on G) /\ GroupAuto f g) /\ (y o (f on G) on G = I on G) 382 Let y = (LINV f G) on G, Then 383 (1) Let f = LINV f G, then GroupAuto f g by group_auto_linv_auto 384 (2) GroupAuto f g ==> (LINV f G on G) o (f on G) on G = I on G 385 Note f PERMUTES G by group_auto_bij 386 (LINV f G on G) o (f on G) on s 387 = (LINV f G o f) on G by bij_on_compose 388 = I on G by bij_on_inv 389*) 390Theorem automorphism_group_group: 391 !g:'a group. Group g ==> Group (automorphism_group g) 392Proof 393 rpt strip_tac >> 394 rw_tac std_ss[group_def_alt, automorphism_group_def, GSPECIFICATION] >| [ 395 rename [���(f on G) o (f' on G) on G���] >> 396 qexists_tac `f o f' on G` >> 397 rpt strip_tac >- metis_tac[bij_on_compose, fun_on_on, group_auto_bij] >> 398 metis_tac[group_auto_compose, group_auto_on_auto], 399 metis_tac[group_auto_bij, bij_on_bij, bij_on_compose_assoc], 400 metis_tac[group_auto_I], 401 rename [���(I on G) o (f on G) on G���] >> 402 `!x. x IN G ==> f x IN G` by metis_tac[group_auto_bij, BIJ_ELEMENT] >> 403 rw[fun_on_compose], 404 rename [���_ o (f on G) on G���] >> 405 qexists_tac `(LINV f G) on G` >> 406 rpt strip_tac >- metis_tac[group_auto_linv_auto] >> 407 metis_tac[bij_on_compose, bij_on_inv, group_auto_bij] 408 ] 409QED 410 411(* Another major result. *) 412 413(* ------------------------------------------------------------------------- *) 414 415(* export theory at end *) 416val _ = export_theory(); 417 418(*===========================================================================*) 419