1open HolKernel Parse boolLib; 2val _ = new_theory "group"; 3 4open bossLib listTheory HurdUseful subtypeTools res_quanTools 5 res_quanTheory pred_setTheory extra_pred_setTheory arithContext 6 relationTheory ho_proverTools extra_listTheory 7 listContext arithmeticTheory subtypeTheory extra_numTheory 8 pred_setContext; 9 10val EXISTS_DEF = boolTheory.EXISTS_DEF; 11 12infixr 0 ++ << || THENC ORELSEC ORELSER ##; 13infix 1 >>; 14 15val op!! = op REPEAT; 16val op++ = op THEN; 17val op<< = op THENL; 18val op|| = op ORELSE; 19val op>> = op THEN1; 20 21(* ------------------------------------------------------------------------- *) 22(* Tools. *) 23(* ------------------------------------------------------------------------- *) 24 25val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC; 26 27val std_pc = precontext_mergel [arith_pc, list_pc, pred_set_pc]; 28val std_c = precontext_compile std_pc; 29 30val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS std_c; 31 32val Strip = S_TAC; 33val Simplify = R_TAC; 34 35(* ------------------------------------------------------------------------- *) 36(* Definitions. *) 37(* ------------------------------------------------------------------------- *) 38 39val group_def = Define 40 `group (gp : 'a -> bool, star) = 41 star IN (gp -> gp -> gp) /\ 42 (!x y z :: gp. star (star x y) z = star x (star y z)) /\ 43 ?e :: gp. !x :: gp. ?ix :: gp. (star e x = x) /\ (star ix x = e)`; 44 45val gset_def = Define `gset (gp : 'a -> bool, star : 'a -> 'a -> 'a) = gp`; 46 47val gop_def = Define `gop (gp : 'a -> bool, star : 'a -> 'a -> 'a) = star`; 48 49val gid_def = Define 50 `gid (G : ('a -> bool) # ('a -> 'a -> 'a)) = 51 @e :: gset G. !x :: gset G. ?ix :: gset G. 52 (gop G e x = x) /\ (gop G ix x = e)`; 53 54val ginv_def = Define 55 `ginv (G : ('a -> bool) # ('a -> 'a -> 'a)) x = 56 @ix :: gset G. gop G ix x = gid G`; 57 58val prod_group_def = Define 59 `prod_group G H = 60 (gset G CROSS gset H, \ (x1, y1) (x2, y2). (gop G x1 x2, gop H y1 y2))`; 61 62val subgroup_def = Define 63 `subgroup G H = 64 H IN group /\ gset H SUBSET gset G /\ !g h :: gset H. gop H g h = gop G g h`; 65 66val psubgroup_def = Define 67 `psubgroup G H = H IN subgroup G /\ gset H PSUBSET gset G`; 68 69val gpow_def = Define 70 `(gpow G g 0 = gid G) /\ (gpow G g (SUC n) = gop G g (gpow G g n))`; 71 72val group_homo_def = Define 73 `group_homo G H f 74 = f IN (gset G -> gset H) /\ 75 (!x y :: gset G. gop H (f x) (f y) = f (gop G x y))`; 76 77val group_iso_def = Define 78 `group_iso G H f = f IN group_homo G H /\ BIJ f (gset G) (gset H)`; 79 80val lcoset_def = Define 81 `lcoset G g H = IMAGE (gop G g) (gset H)`; 82 83(* ------------------------------------------------------------------------- *) 84(* Theorems. *) 85(* ------------------------------------------------------------------------- *) 86 87val IN_GROUP = store_thm 88 ("IN_GROUP", 89 ``!G. 90 G IN group = 91 gop G IN (gset G -> gset G -> gset G) /\ 92 (!x y z :: gset G. gop G (gop G x y) z = gop G x (gop G y z)) /\ 93 ?e :: gset G. !x :: gset G. ?ix :: gset G. 94 (gop G e x = x) /\ (gop G ix x = e)``, 95 Cases 96 ++ R_TAC [group_def, SPECIFICATION, gop_def, gset_def]); 97 98val GROUP = store_thm 99 ("GROUP", 100 ``!G. 101 G IN group = 102 gop G IN (gset G -> gset G -> gset G) /\ 103 (!x y z :: gset G. gop G (gop G x y) z = gop G x (gop G y z)) /\ 104 gid G IN gset G /\ 105 ginv G IN (gset G -> gset G) /\ 106 !x :: gset G. (gop G (gid G) x = x) /\ (gop G (ginv G x) x = gid G)``, 107 R_TAC [IN_GROUP] 108 ++ ONCE_REWRITE_TAC [RES_EXISTS_ALT] 109 ++ BETA_TAC 110 ++ R_TAC [GSYM gid_def] 111 ++ STRIP_TAC 112 ++ Suff 113 `(!x :: gset G. ?ix :: gset G. 114 (gop G (gid G) x = x) /\ (gop G ix x = gid G)) = 115 (ginv G IN (gset G -> gset G) /\ 116 !x :: gset G. (gop G (gid G) x = x) /\ (gop G (ginv G x) x = gid G))` 117 >> PROVE_TAC [] 118 ++ R_TAC [IN_FUNSET] 119 ++ Suff 120 `!x :: gset G. 121 (?ix :: gset G. (gop G (gid G) x = x) /\ (gop G ix x = gid G)) = 122 (ginv G x IN gset G /\ (gop G (gid G) x = x) /\ 123 (gop G (ginv G x) x = gid G))` 124 >> (RESQ_TAC ++ PROVE_TAC []) 125 ++ R_TAC [RES_EXISTS_ALT, ginv_def]); 126 127val GSET_SUBTYPE = store_thm 128 ("GSET_SUBTYPE", 129 ``gset IN (group -> nonempty)``, 130 R_TAC [IN_FUNSET, IN_NONEMPTY] 131 ++ SET_EQ_TAC 132 ++ R_TAC [GROUP] 133 ++ PROVE_TAC []); 134 135val GOP_SUBTYPE = store_thm 136 ("GOP_SUBTYPE", 137 ``gop IN (group --> \G. gset G -> gset G -> gset G)``, 138 R_TAC [IN_DFUNSET] 139 ++ R_TAC [GROUP]); 140 141val GROUP_ASSOC = store_thm 142 ("GROUP_ASSOC", 143 ``!G :: group. !x y z :: gset G. gop G (gop G x y) z = gop G x (gop G y z)``, 144 S_TAC 145 ++ AR_TAC [GROUP]); 146 147val GROUP_LASSOC = store_thm 148 ("GROUP_LASSOC", 149 ``!G :: group. !x y z :: gset G. gop G x (gop G y z) = gop G (gop G x y) z``, 150 S_TAC 151 ++ AR_TAC [GROUP]); 152 153val GID_SUBTYPE = store_thm 154 ("GID_SUBTYPE", 155 ``gid IN (group --> gset)``, 156 R_TAC [IN_DFUNSET, GROUP]); 157 158val GROUP_LID = store_thm 159 ("GROUP_LID", 160 ``!G :: group. !x :: gset G. gop G (gid G) x = x``, 161 S_TAC 162 ++ AR_TAC [GROUP]); 163 164val GINV_SUBTYPE = store_thm 165 ("GINV_SUBTYPE", 166 ``ginv IN (group --> \G. gset G -> gset G)``, 167 R_TAC [IN_DFUNSET, GROUP]); 168 169val GROUP_LINV = store_thm 170 ("GROUP_LINV", 171 ``!G :: group. !x :: gset G. gop G (ginv G x) x = gid G``, 172 S_TAC 173 ++ AR_TAC [GROUP]); 174 175val GROUP_RINV = store_thm 176 ("GROUP_RINV", 177 ``!G :: group. !x :: gset G. gop G x (ginv G x) = gid G``, 178 S_TAC 179 ++ Suff `gop G (gid G) (gop G x (ginv G x)) = gid G` 180 >> R_TAC [GROUP_LID, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 181 ++ Suff 182 `gop G (gop G (ginv G (ginv G x)) (ginv G x)) (gop G x (ginv G x)) = 183 gid G` 184 >> R_TAC [GROUP_LINV, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 185 ++ Suff 186 `gop G (ginv G (ginv G x)) (gop G (ginv G x) (gop G x (ginv G x))) = 187 gid G` 188 >> R_TAC [GROUP_ASSOC, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 189 ++ Suff 190 `gop G (ginv G (ginv G x)) (gop G (gop G (ginv G x) x) (ginv G x)) = 191 gid G` 192 >> R_TAC [GROUP_ASSOC, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 193 ++ Suff `gop G (ginv G (ginv G x)) (gop G (gid G) (ginv G x)) = gid G` 194 >> R_TAC [GROUP_LINV, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 195 ++ Suff `gop G (ginv G (ginv G x)) (ginv G x) = gid G` 196 >> R_TAC [GROUP_LID, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE] 197 >> R_TAC [GROUP_LINV, GOP_SUBTYPE, GID_SUBTYPE, GINV_SUBTYPE]); 198 199val GROUP_RID = store_thm 200 ("GROUP_RID", 201 ``!G :: group. !x :: gset G. gop G x (gid G) = x``, 202 S_TAC 203 ++ Suff `gop G x (gop G (ginv G x) x) = x` 204 >> R_TAC [GROUP_LINV] 205 ++ Suff `gop G (gop G x (ginv G x)) x = x` 206 >> R_TAC [GROUP_ASSOC, GINV_SUBTYPE] 207 ++ R_TAC [GROUP_RINV, GROUP_LID, GINV_SUBTYPE]); 208 209val GROUP_LCANCEL = store_thm 210 ("GROUP_LCANCEL", 211 ``!G :: group. !g h h' :: gset G. (gop G g h = gop G g h') = (h = h')``, 212 S_TAC 213 ++ REVERSE EQ_TAC >> R_TAC [] 214 ++ S_TAC 215 ++ Suff `gop G (gid G) h = gop G (gid G) h'` 216 >> R_TAC [GROUP_LID] 217 ++ Suff `gop G (gop G (ginv G g) g) h = gop G (gop G (ginv G g) g) h'` 218 >> R_TAC [GROUP_LINV] 219 ++ R_TAC [GROUP_ASSOC, GINV_SUBTYPE]); 220 221val GROUP_RCANCEL = store_thm 222 ("GROUP_RCANCEL", 223 ``!G :: group. !g g' h :: gset G. (gop G g h = gop G g' h) = (g = g')``, 224 S_TAC 225 ++ REVERSE EQ_TAC >> R_TAC [] 226 ++ S_TAC 227 ++ Suff `gop G g (gid G) = gop G g' (gid G)` 228 >> R_TAC [GROUP_RID] 229 ++ Suff `gop G g (gop G h (ginv G h)) = gop G g' (gop G h (ginv G h))` 230 >> R_TAC [GROUP_RINV] 231 ++ R_TAC [GROUP_LASSOC, GINV_SUBTYPE]); 232 233val GROUP_LCANCEL_ID = store_thm 234 ("GROUP_LCANCEL_ID", 235 ``!G :: group. !g h :: gset G. (gop G g h = g) = (h = gid G)``, 236 S_TAC 237 ++ REVERSE EQ_TAC >> R_TAC [GROUP_RID] 238 ++ S_TAC 239 ++ Suff `gop G g h = gop G g (gid G)` 240 >> R_TAC [GROUP_LCANCEL, GID_SUBTYPE] 241 ++ R_TAC [GROUP_RID]); 242 243val GROUP_RCANCEL_ID = store_thm 244 ("GROUP_RCANCEL_ID", 245 ``!G :: group. !g h :: gset G. (gop G g h = h) = (g = gid G)``, 246 S_TAC 247 ++ REVERSE EQ_TAC >> R_TAC [GROUP_LID] 248 ++ S_TAC 249 ++ Suff `gop G g h = gop G (gid G) h` 250 >> R_TAC [GROUP_RCANCEL, GID_SUBTYPE] 251 ++ R_TAC [GROUP_LID]); 252 253val PROD_GROUP_SET = store_thm 254 ("PROD_GROUP_SET", 255 ``!G H. gset (prod_group G H) = gset G CROSS gset H``, 256 R_TAC [prod_group_def, gset_def]); 257 258val PROD_GROUP_OP = store_thm 259 ("PROD_GROUP_OP", 260 ``!G H g1 g2 h1 h2. 261 gop (prod_group G H) (g1, h1) (g2, h2) = (gop G g1 g2, gop H h1 h2)``, 262 R_TAC [prod_group_def, gop_def]); 263 264val IN_ABELIAN = store_thm 265 ("IN_ABELIAN", 266 ``!G. G IN abelian = abelian G``, 267 R_TAC [SPECIFICATION]); 268 269(* Consolidate theorems so far in a simplification context *) 270 271val group1_sc = 272 map SC_SIMPLIFICATION 273 [] @ 274 map SC_JUDGEMENT 275 [] @ 276 map SC_SUBTYPE 277 [GSET_SUBTYPE, 278 GOP_SUBTYPE, 279 GID_SUBTYPE, 280 GINV_SUBTYPE] 281 282val group1_pc = precontext_add 283 ("group1", 284 map C_SUBTYPE group1_sc @ 285 map C_THM 286 [GROUP_LCANCEL, 287 GROUP_RCANCEL, 288 GROUP_LCANCEL_ID, 289 GROUP_RCANCEL_ID, 290 GROUP_LID, 291 GROUP_RID, 292 GROUP_LINV, 293 GROUP_RINV, 294 PROD_GROUP_SET, 295 PROD_GROUP_OP]) 296 std_pc; 297 298val group1_c = precontext_compile group1_pc; 299 300val (G_TAC, AG_TAC, G_TAC', AG_TAC') = SIMPLIFY_TACS group1_c; 301 302(* back to proving theorems *) 303 304val GID_UNIQUE = store_thm 305 ("GID_UNIQUE", 306 ``!G :: group. !x :: gset G. (gop G x x = x) = (x = gid G)``, 307 S_TAC 308 ++ G_TAC []); 309 310val IN_SUBGROUP = store_thm 311 ("IN_SUBGROUP", 312 ``!G H. 313 H IN subgroup G = 314 H IN group /\ gset H SUBSET gset G /\ 315 !g h :: gset H. gop H g h = gop G g h``, 316 R_TAC [SPECIFICATION, subgroup_def]); 317 318val SUBGROUP_GROUP = store_thm 319 ("SUBGROUP_GROUP", 320 ``!G H. H IN subgroup G ==> H IN group``, 321 R_TAC [IN_SUBGROUP]); 322 323val SUBGROUP_SET = store_thm 324 ("SUBGROUP_SET", 325 ``!G H. H IN subgroup G ==> gset H SUBSET gset G``, 326 R_TAC [IN_SUBGROUP]); 327 328val SUBGROUP_OP = store_thm 329 ("SUBGROUP_OP", 330 ``!G H. H IN subgroup G ==> !g h :: gset H. gop H g h = gop G g h``, 331 R_TAC [IN_SUBGROUP]); 332 333val SUBGROUP_ID = store_thm 334 ("SUBGROUP_ID", 335 ``!G H. G IN group /\ H IN subgroup G ==> (gid H = gid G)``, 336 S_TAC 337 ++ ASM_MATCH_MP_TAC [SUBGROUP_GROUP, SUBGROUP_SET, SUBGROUP_OP] 338 ++ Know `gid H IN gset G` >> R_TAC [GID_SUBTYPE] 339 ++ STRIP_TAC 340 ++ Suff `gop G (gid H) (gid H) = gid H` 341 >> R_TAC [GID_UNIQUE] 342 ++ Suff `gop H (gid H) (gid H) = gid H` 343 >> R_TAC [GID_SUBTYPE] 344 ++ G_TAC []); 345 346val SUBGROUP_INV = store_thm 347 ("SUBGROUP_INV", 348 ``!G H. 349 G IN group /\ H IN subgroup G ==> !h :: gset H. ginv H h = ginv G h``, 350 S_TAC 351 ++ ASM_MATCH_MP_TAC [SUBGROUP_GROUP, SUBGROUP_SET, SUBGROUP_OP, SUBGROUP_ID] 352 ++ Suff `gop G h (ginv H h) = gop G h (ginv G h)` 353 >> G_TAC [] 354 ++ R_TAC [GROUP_RINV] 355 ++ Suff `gop H h (ginv H h) = gid H` >> G_TAC [] 356 ++ R_TAC [GROUP_RINV]); 357 358val IN_PSUBGROUP = store_thm 359 ("IN_PSUBGROUP", 360 ``!G H. 361 H IN psubgroup G = H IN subgroup G /\ gset H PSUBSET gset G``, 362 R_TAC [SPECIFICATION, psubgroup_def]); 363 364val PSUBGROUP_SUBGROUP = store_thm 365 ("PSUBGROUP_SUBGROUP", 366 ``!G H. H IN psubgroup G ==> H IN subgroup G``, 367 R_TAC [IN_PSUBGROUP]); 368 369val PSUBGROUP_PSUBSET = store_thm 370 ("PSUBGROUP_PSUBSET", 371 ``!G H. H IN psubgroup G ==> gset H PSUBSET gset G``, 372 R_TAC [IN_PSUBGROUP]); 373 374(* Consolidate theorems so far in a simplification context *) 375 376val group2_pc = precontext_add 377 ("group2", 378 map C_FORWARDS 379 [SUBGROUP_SET, 380 SUBGROUP_GROUP, 381 SUBGROUP_OP, 382 SUBGROUP_ID, 383 SUBGROUP_INV, 384 PSUBGROUP_SUBGROUP, 385 PSUBGROUP_PSUBSET]) 386 group1_pc; 387 388val group2_c = precontext_compile group2_pc; 389 390val (G_TAC, AG_TAC, G_TAC', AG_TAC') = SIMPLIFY_TACS group2_c; 391 392(* back to proving theorems *) 393 394val GPOW = store_thm 395 ("GPOW", 396 ``!G. !g :: gset G. 397 (gpow G g 0 = gid G) /\ 398 (!n. gpow G g (SUC n) = gop G g (gpow G g n))``, 399 R_TAC [gpow_def]); 400 401val GPOW_SUBTYPE = store_thm 402 ("GPOW_SUBTYPE", 403 ``gpow IN (group --> \G. gset G -> UNIV -> gset G)``, 404 R_TAC [IN_DFUNSET, IN_FUNSET] 405 ++ S_TAC 406 ++ Induct_on `x` 407 ++ G_TAC [GPOW]); 408 409val GPOW_ID = store_thm 410 ("GPOW_ID", 411 ``!G :: group. !n. gpow G (gid G) n = gid G``, 412 S_TAC 413 ++ Induct_on `n` 414 ++ G_TAC [GPOW]); 415 416val GPOW_ADD = store_thm 417 ("GPOW_ADD", 418 ``!(G :: group) (g :: gset G) m n. 419 gpow G g (m + n) = gop G (gpow G g m) (gpow G g n)``, 420 S_TAC 421 ++ Induct_on `m` 422 ++ G_TAC [GPOW, GPOW_SUBTYPE, ADD_CLAUSES, GROUP_ASSOC]); 423 424val GPOW_MULT = store_thm 425 ("GPOW_MULT", 426 ``!(G :: group) (g :: gset G) m n. 427 gpow G g (m * n) = gpow G (gpow G g m) n``, 428 S_TAC 429 ++ Induct_on `n` >> G_TAC [GPOW, GPOW_SUBTYPE] 430 ++ G_TAC [GPOW, MULT_CLAUSES, GPOW_ADD, GPOW_SUBTYPE]); 431 432val IN_GROUP_HOMO = store_thm 433 ("IN_GROUP_HOMO", 434 ``!G H f. 435 f IN group_homo G H = 436 f IN (gset G -> gset H) /\ 437 !x y :: gset G. gop H (f x) (f y) = f (gop G x y)``, 438 R_TAC [SPECIFICATION, group_homo_def]); 439 440val IN_GROUP_ISO = store_thm 441 ("IN_GROUP_ISO", 442 ``!G H f. 443 f IN group_iso G H = f IN group_homo G H /\ BIJ f (gset G) (gset H)``, 444 R_TAC [SPECIFICATION, group_iso_def]); 445 446val GROUP_SURJ_HOMO_GROUP = store_thm 447 ("GROUP_SURJ_HOMO_GROUP", 448 ``!(G :: group) H (f :: group_homo G H). 449 SURJ f (gset G) (gset H) ==> H IN group``, 450 S_TAC 451 ++ Cases_on `H` 452 ++ R_TAC [IN_GROUP] 453 ++ AR_TAC [GROUP, IN_GROUP_HOMO, SURJ_ALT, gset_def, gop_def] 454 ++ S_TAC << 455 [R_TAC [IN_FUNSET] 456 ++ S_TAC 457 ++ Q.PAT_X_ASSUM `!y :: q. P y` 458 (fn th => 459 (MP_TAC o RESQ_SPEC ``x':'b``) th ++ (MP_TAC o RESQ_SPEC ``x:'b``) th) 460 ++ S_TAC 461 ++ R_TAC [], 462 Q.PAT_X_ASSUM `!y :: q. P y` 463 (fn th => 464 (MP_TAC o RESQ_SPEC ``x:'b``) th 465 ++ (MP_TAC o RESQ_SPEC ``y:'b``) th 466 ++ (MP_TAC o RESQ_SPEC ``z:'b``) th) 467 ++ S_TAC 468 ++ R_TAC [], 469 RESQ_EXISTS_TAC ``f (gid G)`` 470 ++ S_TAC >> R_TAC [] 471 ++ RESQ_EXISTS_TAC 472 ``(f :'a -> 'b) (ginv G (@y. y IN gset G /\ (x = f y)))`` 473 ++ R_TAC [] 474 ++ S_TAC << 475 [RW_TAC std_ss [IN_FUNSET] 476 ++ Suff `(@y. y IN gset G /\ (x = f y)) IN gset G` 477 >> (S_TAC ++ G_TAC []) 478 ++ Q.PAT_X_ASSUM `!y::q. P y` (MP_TAC o RESQ_SPEC ``x : 'b``) 479 ++ G_TAC [RES_EXISTS, EXISTS_DEF], 480 Q.PAT_X_ASSUM `!y::q. P y` (MP_TAC o RESQ_SPEC ``x:'b``) 481 ++ S_TAC 482 ++ R_TAC [], 483 Q.PAT_X_ASSUM `!y::q. P y` (MP_TAC o RESQ_SPEC ``x:'b``) 484 ++ R_TAC [RES_EXISTS] 485 ++ DISCH_THEN (fn th => MP_TAC th ++ MP_TAC th) 486 ++ RESQ_STRIP_TAC 487 ++ simpLib.ASM_SIMP_TAC std_ss [EXISTS_DEF] 488 ++ Q.SPEC_TAC (`@y. y IN gset G /\ (f x' = f y)`, `y`) 489 ++ simpLib.SIMP_TAC std_ss [] 490 ++ S_TAC 491 ++ R_TAC []]]); 492 493val GROUP_ISO_GROUP = store_thm 494 ("GROUP_ISO_GROUP", 495 ``!(G :: group) H (f :: group_iso G H). H IN group``, 496 S_TAC 497 ++ AR_TAC [IN_GROUP_ISO, BIJ_DEF] 498 ++ MP_TAC GROUP_SURJ_HOMO_GROUP 499 ++ RESQ_TAC 500 ++ ho_PROVE_TAC []); 501 502val LCOSETS_EQUAL_OR_DISJOINT = store_thm 503 ("LCOSETS_EQUAL_OR_DISJOINT", 504 ``!G :: group. !H :: subgroup G. !g1 g2 :: gset G. 505 (lcoset G g1 H = lcoset G g2 H) 506 \/ DISJOINT (lcoset G g1 H) (lcoset G g2 H)``, 507 S_TAC 508 ++ REVERSE 509 (Cases_on `?g. g IN lcoset G g1 H 510 /\ g IN lcoset G g2 H`) 511 >> (R_TAC [DISJOINT_DEF] 512 ++ !! (POP_ASSUM MP_TAC) 513 ++ RW_TAC std_ss [EXTENSION, IN_INTER, NOT_IN_EMPTY] 514 ++ PROVE_TAC []) 515 ++ POP_ASSUM MP_TAC 516 ++ RW_TAC std_ss [DISJOINT_DEF] 517 ++ Suff `!v. v IN lcoset G g1 H = v IN lcoset G g2 H` 518 >> (!! (POP_ASSUM MP_TAC) 519 ++ RW_TAC std_ss [EXTENSION, IN_INTER, NOT_IN_EMPTY] 520 ++ PROVE_TAC []) 521 ++ NTAC 4 (POP_ASSUM MP_TAC) 522 ++ Q.SPEC_TAC (`g2`, `g2`) 523 ++ Q.SPEC_TAC (`g1`, `g1`) 524 ++ Suff `!g1 g2 :: gset G. 525 g IN lcoset G g1 H /\ 526 g IN lcoset G g2 H ==> 527 !v. 528 v IN lcoset G g1 H ==> 529 v IN lcoset G g2 H` 530 >> (RESQ_TAC ++ ho_PROVE_TAC []) 531 ++ G_TAC [lcoset_def] 532 ++ AR_TAC [IN_IMAGE] 533 ++ S_TAC 534 ++ RW_TAC std_ss [] 535 ++ Q.EXISTS_TAC `gop H x' (gop H (ginv H x) x'')` 536 ++ REVERSE CONJ_TAC >> R_TAC [SUBGROUP_GROUP, GOP_SUBTYPE, GINV_SUBTYPE] 537 ++ G_TAC [] 538 ++ Suff `gop G g1 x'' = gop G (gop G (gop G g2 x') (ginv G x)) x''` 539 >> G_TAC [GROUP_ASSOC] 540 ++ G_TAC [] 541 ++ G_TAC [GROUP_ASSOC]); 542 543(* Consolidate all theorems in a theory simplification context *) 544 545val group3_sc = 546 map SC_SIMPLIFICATION 547 [] @ 548 map SC_JUDGEMENT 549 [] @ 550 map SC_SUBTYPE 551 [GPOW_SUBTYPE]; 552 553val group3_pc = precontext_add 554 ("group3", 555 map C_SUBTYPE group3_sc @ 556 map C_THM 557 [GPOW, 558 GPOW_ID, 559 GPOW_ADD, 560 GPOW_MULT]) 561 group2_pc; 562 563val group3_c = precontext_compile group3_pc; 564 565val (G_TAC, AG_TAC, G_TAC', AG_TAC') = SIMPLIFY_TACS group3_c; 566 567(* back to proving theorems *) 568 569val GROUP_SET_EMPTY = store_thm 570 ("GROUP_SET_EMPTY", 571 ``!G :: group. ~(gset G = {})``, 572 S_TAC 573 ++ AR_TAC [IN_GROUP]); 574 575val GINV_UNIQUE = store_thm 576 ("GINV_UNIQUE", 577 ``!G :: group. !g h :: gset G. 578 (gop G g h = gid G) \/ (gop G h g = gid G) ==> (ginv G g = h)``, 579 S_TAC << 580 [Suff `gop G g (ginv G g) = gop G g h` >> G_TAC [] 581 ++ ASM_REWRITE_TAC [] 582 ++ G_TAC [], 583 Suff `gop G (ginv G g) g = gop G h g` >> G_TAC [] 584 ++ ASM_REWRITE_TAC [] 585 ++ G_TAC []]); 586 587val IS_GINV = store_thm 588 ("IS_GINV", 589 ``!G :: group. !g h :: gset G. 590 (ginv G g = h) = (gop G g h = gid G) \/ (gop G h g = gid G)``, 591 S_TAC 592 ++ EQ_TAC >> DISCH_THEN (fn th => G_TAC [SYM th]) 593 ++ S_TAC << 594 [MATCH_MP_TAC (Q_RESQ_SPECL [`G`, `g`, `h`] GINV_UNIQUE) 595 ++ R_TAC [], 596 MATCH_MP_TAC (Q_RESQ_SPECL [`G`, `g`, `h`] GINV_UNIQUE) 597 ++ R_TAC []]); 598 599val GINV_GID = store_thm 600 ("GINV_GID", 601 ``!G :: group. ginv G (gid G) = gid G``, 602 S_TAC 603 ++ R_TAC [IS_GINV, GID_SUBTYPE] 604 ++ G_TAC []); 605 606val GPOW_1 = store_thm 607 ("GPOW_1", 608 ``!G :: group. !g :: gset G. gpow G g 1 = g``, 609 S_TAC 610 ++ REWRITE_TAC [GSYM SUC_0, gpow_def] 611 ++ G_TAC []); 612 613val GINV_GOP = store_thm 614 ("GINV_GOP", 615 ``!G :: group. !g h :: gset G. 616 ginv G (gop G g h) = gop G (ginv G h) (ginv G g)``, 617 S_TAC 618 ++ G_TAC [IS_GINV] 619 ++ DISJ1_TAC 620 ++ Suff `gop G g (gop G (gop G h (ginv G h)) (ginv G g)) = gid G` 621 >> G_TAC [GROUP_ASSOC] 622 ++ G_TAC []); 623 624val GPOW_COMM = store_thm 625 ("GPOW_COMM", 626 ``!G :: group. !g :: gset G. !n. 627 gop G g (gpow G g n) = gop G (gpow G g n) g``, 628 NTAC 2 RESQ_STRIP_TAC 629 ++ Induct >> G_TAC [] 630 ++ G_TAC [] 631 ++ Suff `gop G (gop G g (gpow G g n)) g = gop G (gpow G g n) (gop G g g)` 632 >> G_TAC [GROUP_ASSOC] 633 ++ ASM_REWRITE_TAC [] 634 ++ G_TAC [GROUP_ASSOC]); 635 636val GINV_GPOW = store_thm 637 ("GINV_GPOW", 638 ``!G :: group. !g :: gset G. !n. ginv G (gpow G g n) = gpow G (ginv G g) n``, 639 NTAC 2 RESQ_STRIP_TAC 640 ++ Induct >> G_TAC [GINV_GID] 641 ++ G_TAC [] 642 ++ G_TAC [GINV_GOP] 643 ++ ONCE_REWRITE_TAC [EQ_SYM_EQ] 644 ++ G_TAC [GPOW_COMM]); 645 646val GINV_EQ_GID = store_thm 647 ("GINV_EQ_GID", 648 ``!G :: group. !g :: gset G. (ginv G g = gid G) = (g = gid G)``, 649 S_TAC 650 ++ REVERSE EQ_TAC >> G_TAC [GINV_GID] 651 ++ S_TAC 652 ++ Suff `gop G (ginv G g) g = gop G (ginv G g) (gid G)` 653 >> G_TAC [] 654 ++ POP_ASSUM 655 (fn th => 656 R_TAC [GROUP_RID, GINV_SUBTYPE, GROUP_LINV] 657 ++ ASSUME_TAC th) 658 ++ G_TAC []); 659 660val SET_SUBGROUP = store_thm 661 ("SET_SUBGROUP", 662 ``!s G. 663 G IN group /\ s SUBSET gset G /\ ~(s = {}) /\ 664 ginv G IN (s -> s) /\ gop G IN (s -> s -> s) ==> 665 (s, gop G) IN subgroup G``, 666 Strip 667 ++ Simplify [IN_SUBGROUP, gset_def, gop_def, IN_GROUP] 668 ++ Strip >> G_TAC [GROUP_ASSOC] 669 ++ Q_RESQ_EXISTS_TAC `gid G` 670 ++ STRONG_CONJ_TAC 671 >> (Know `?x. x IN s` 672 >> (Q.PAT_X_ASSUM `~(s = {})` MP_TAC 673 ++ SET_EQ_TAC 674 ++ Simplify [NOT_IN_EMPTY]) 675 ++ Strip 676 ++ Know `ginv G x IN s` >> R_TAC' [] 677 ++ Strip 678 ++ Know `gop G (ginv G x) x IN s` >> R_TAC' [] 679 ++ G_TAC []) 680 ++ Strip 681 ++ Q_RESQ_EXISTS_TAC `ginv G x` 682 ++ G_TAC' []); 683 684val GROUP_HOMO_GID = store_thm 685 ("GROUP_HOMO_GID", 686 ``!f G H. 687 f IN group_homo G H /\ G IN group /\ H IN group ==> 688 (f (gid G) = gid H)``, 689 Simplify [IN_GROUP_HOMO] 690 ++ Strip 691 ++ Q.PAT_X_ASSUM `!x :: P. M x` 692 (MP_TAC o Q_RESQ_HALF_SPECL [`gid G`, `gid G`]) 693 ++ G_TAC' []); 694 695val GROUP_HOMO_GPOW = store_thm 696 ("GROUP_HOMO_GPOW", 697 ``!f G H g n. 698 f IN group_homo G H /\ G IN group /\ H IN group /\ g IN gset G ==> 699 (f (gpow G g n) = gpow H (f g) n)``, 700 Strip 701 ++ Q.PAT_X_ASSUM `f IN x` 702 (fn th => MP_TAC th ++ Simplify [IN_GROUP_HOMO] ++ ASSUME_TAC th) 703 ++ Strip 704 ++ Induct_on `n` >> G_TAC [GROUP_HOMO_GID] 705 ++ POP_ASSUM (ASSUME_TAC o SYM) 706 ++ G_TAC []); 707 708val PROD_GROUP_SUBTYPE = store_thm 709 ("PROD_GROUP_SUBTYPE", 710 ``prod_group IN (group -> group -> group)``, 711 Simplify [IN_FUNSET] 712 ++ Strip 713 ++ Simplify [IN_GROUP, PROD_GROUP_OP, PROD_GROUP_SET, IN_FUNSET, IN_CROSS] 714 ++ Strip << 715 [Cases_on `x'''` 716 ++ Cases_on `x''` 717 ++ AG_TAC' [], 718 Cases_on `x'''` 719 ++ Cases_on `x''` 720 ++ AG_TAC' [], 721 Cases_on `x''` 722 ++ Cases_on `y` 723 ++ Cases_on `z` 724 ++ AG_TAC' [IN_CROSS, GROUP_ASSOC], 725 Q_RESQ_EXISTS_TAC `(gid x', gid x)` 726 ++ G_TAC' [IN_CROSS] 727 ++ Strip 728 ++ Cases_on `x''` 729 ++ Q_RESQ_EXISTS_TAC `(ginv x' q, ginv x r)` 730 ++ AG_TAC' [IN_CROSS]]); 731 732val PROD_GROUP_GID = store_thm 733 ("PROD_GROUP_GID", 734 ``!G H :: group. gid (prod_group G H) = (gid G, gid H)``, 735 Strip 736 ++ MATCH_MP_TAC EQ_SYM 737 ++ Know `(gid G, gid H) IN gset (prod_group G H)` >> G_TAC' [IN_CROSS] 738 ++ Know `prod_group G H IN group` >> G_TAC' [PROD_GROUP_SUBTYPE] 739 ++ Strip 740 ++ Simplify [GSYM GID_UNIQUE] 741 ++ MATCH_MP_TAC EQ_SYM 742 ++ G_TAC []); 743 744val PROD_GROUP_GPOW = store_thm 745 ("PROD_GROUP_GPOW", 746 ``!G H :: group. !g :: gset G. !h :: gset H. !n. 747 gpow (prod_group G H) (g, h) n = (gpow G g n, gpow H h n)``, 748 Strip 749 ++ Know `(g,h) IN gset (prod_group G H)` 750 >> G_TAC' [PROD_GROUP_SET, IN_CROSS] 751 ++ Strip 752 ++ Induct_on `n` >> G_TAC [PROD_GROUP_GID] 753 ++ G_TAC [PROD_GROUP_OP]); 754 755(* non-interactive mode 756*) 757val _ = export_theory (); 758