1(* ------------------------------------------------------------------------- *) 2(* Cyclic 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 "groupCyclic"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* Get dependent theories local *) 20(* (* val _ = load "monoidTheory"; *) *) 21(* (* val _ = load "groupTheory"; *) *) 22(* (* val _ = load "subgroupTheory"; *) *) 23(* val _ = load "groupOrderTheory"; *) 24open monoidTheory monoidOrderTheory; 25open groupTheory subgroupTheory groupOrderTheory; 26open groupMapTheory; 27 28(* val _ = load "groupInstancesTheory"; *) 29open groupInstancesTheory; 30 31(* Get dependent theories in lib *) 32(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 33(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 34open helperNumTheory helperSetTheory; 35 36(* val _ = load "helperFunctionTheory"; *) 37open helperFunctionTheory; 38 39(* val _ = load "GaussTheory"; *) 40open GaussTheory; 41open EulerTheory; 42 43(* open dependent theories *) 44open pred_setTheory listTheory arithmeticTheory; 45(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 46(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 47open dividesTheory gcdTheory; 48 49 50(* ------------------------------------------------------------------------- *) 51(* Cyclic Group Documentation *) 52(* ------------------------------------------------------------------------- *) 53(* Overloads: 54*) 55(* Definitions and Theorems (# are exported): 56 57 Helper Theroems: 58 59 Cyclic Group has a generator: 60 cyclic_def |- !g. cyclic g <=> Group g /\ ?z. z IN G /\ !x. x IN G ==> ?n. x = z ** n 61 cyclic_gen_def |- !g. cyclic g ==> cyclic_gen g IN G /\ 62 !x. x IN G ==> ?n. x = cyclic_gen g ** n 63# cyclic_group |- !g. cyclic g ==> Group g 64 cyclic_element |- !g. cyclic g ==> !x. x IN G ==> ?n. x = cyclic_gen g ** n 65 cyclic_gen_element |- !g. cyclic g ==> cyclic_gen g IN G 66 cyclic_generated_group |- !g. FiniteGroup g ==> !x. x IN G ==> cyclic (gen x) 67 cyclic_gen_order |- !g. cyclic g /\ FINITE G ==> (ord (cyclic_gen g) = CARD G) 68 cyclic_gen_power_order |- !g. cyclic g /\ FINITE G ==> !n. 0 < n /\ (CARD G MOD n = 0) ==> 69 (ord (cyclic_gen g ** (CARD G DIV n)) = n) 70 71 cyclic_generated_by_gen |- !g. cyclic g /\ FINITE G ==> (g = gen (cyclic_gen g)) 72 cyclic_element_by_gen |- !g. cyclic g /\ FINITE G ==> 73 !x. x IN G ==> ?n. n < CARD G /\ (x = cyclic_gen g ** n) 74 cyclic_element_in_generated |- !g. cyclic g /\ FINITE G ==> 75 !x. x IN G ==> x IN (Gen (cyclic_gen g ** (CARD G DIV ord x))) 76 cyclic_finite_has_order_divisor |- !g. cyclic g /\ FINITE G ==> 77 !n. n divides CARD G ==> ?x. x IN G /\ (ord x = n) 78 79 Cyclic Group Properties: 80 cyclic_finite_alt |- !g. FiniteGroup g ==> (cyclic g <=> ?z. z IN G /\ (ord z = CARD G)) 81 cyclic_group_comm |- !g. cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x) 82 cyclic_group_abelian |- !g. cyclic g ==> AbelianGroup g 83 84 Cyclic Subgroups: 85 cyclic_subgroup_cyclic |- !g h. cyclic g /\ h <= g ==> cyclic h 86 cyclic_subgroup_condition |- !g. cyclic g /\ FINITE G ==> 87 !n. (?h. h <= g /\ (CARD H = n)) <=> n divides CARD G 88 89 Cyclic Group Examples: 90 cyclic_uroots_has_primitive |- !g. FINITE G /\ cyclic g ==> 91 !n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier) 92 cyclic_uroots_cyclic |- !g. cyclic g ==> !n. cyclic (uroots n) 93 add_mod_order_1 |- !n. 1 < n ==> (order (add_mod n) 1 = n) 94 add_mod_cylic |- !n. 0 < n ==> cyclic (add_mod n) 95 96 Cyclic Generators: 97 cyclic_generators_def |- !g. cyclic_generators g = {z | z IN G /\ (ord z = CARD G)} 98 cyclic_generators_element |- !g z. z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G) 99 cyclic_generators_subset |- !g. cyclic_generators g SUBSET G 100 cyclic_generators_finite |- !g. FINITE G ==> FINITE (cyclic_generators g) 101 cyclic_generators_nonempty |- !g. cyclic g /\ FINITE G ==> cyclic_generators g <> {} 102 cyclic_generators_coprimes_bij |- !g. cyclic g /\ FINITE G ==> 103 BIJ (\j. cyclic_gen g ** j) (coprimes (CARD G)) (cyclic_generators g) 104 cyclic_generators_card |- !g. cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G)) 105 cyclic_generators_gen_cofactor_eq_orders |- !g. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> 106 (cyclic_generators (Generated g (cyclic_gen g ** (CARD G DIV n))) = orders g n) 107 cyclic_orders_card |- !g. cyclic g /\ FINITE G ==> 108 !n. CARD (orders g n) = if n divides CARD G then phi n else 0 109 110 Partition by order equality: 111 eq_order_def |- !g x y. eq_order g x y <=> (ord x = ord y) 112 eq_order_equiv |- !g. eq_order g equiv_on G 113 cyclic_orders_nonempty |- !g. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {} 114 cyclic_eq_order_partition |- !g. cyclic g /\ FINITE G ==> 115 (partition (eq_order g) G = {orders g n | n | n divides CARD G}) 116 cyclic_eq_order_partition_alt |- !g. cyclic g /\ FINITE G ==> 117 (partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)}) 118 cyclic_eq_order_partition_by_card |- !g. cyclic g /\ FINITE G ==> 119 (IMAGE CARD (partition (eq_order g) G) = IMAGE phi (divisors (CARD G))) 120 121 eq_order_is_feq_order |- !g. eq_order g = feq ord 122 orders_is_feq_class_order |- !g. orders g = feq_class ord G 123 cyclic_image_ord_is_divisors |- !g. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G)) 124 cyclic_orders_partition |- !g. cyclic g /\ FINITE G ==> 125 (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))) 126 127 Finite Cyclic Group Existence: 128 finite_cyclic_group_existence |- !n. 0 < n ==> ?g. cyclic g /\ (CARD g.carrier = n) 129 130 Cyclic Group index relative to a generator: 131 cyclic_index_exists |- !g x. cyclic g /\ x IN G ==> 132 ?n. (x = cyclic_gen g ** n) /\ (FINITE G ==> n < CARD G) 133 cyclic_index_def |- !g x. cyclic g /\ x IN G ==> 134 (x = cyclic_gen g ** cyclic_index g x) /\ 135 (FINITE G ==> cyclic_index g x < CARD G) 136 finite_cyclic_index_property |- !g. cyclic g /\ FINITE G ==> 137 !n. n < CARD G ==> (cyclic_index g (cyclic_gen g ** n) = n) 138 finite_cyclic_index_unique |- !g x. cyclic g /\ FINITE G /\ x IN G ==> 139 !n. n < CARD G ==> ((x = cyclic_gen g ** n) <=> (n = cyclic_index g x)) 140 finite_cyclic_index_add |- !g x y. cyclic g /\ FINITE G /\ x IN G /\ y IN G ==> 141 (cyclic_index g (x * y) = 142 (cyclic_index g x + cyclic_index g y) MOD CARD G) 143 144 Finite Cyclic Group Uniqueness: 145 finite_cyclic_group_homo |- !g1 g2. cyclic g1 /\ cyclic g2 /\ 146 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 147 GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 148 finite_cyclic_group_bij |- !g1 g2. cyclic g1 /\ cyclic g2 /\ 149 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 150 BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier 151 finite_cyclic_group_iso |- !g1 g2. cyclic g1 /\ cyclic g2 /\ 152 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 153 GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 154 finite_cyclic_group_uniqueness |- !g1 g2. cyclic g1 /\ cyclic g2 /\ 155 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 156 ?f. GroupIso f g1 g2 157 finite_cyclic_group_add_mod_homo |- !g. cyclic g /\ FINITE G ==> 158 GroupHomo (\n. cyclic_gen g ** n) (add_mod (CARD G)) g 159 finite_cyclic_group_add_mod_bij |- !g. cyclic g /\ FINITE G ==> 160 BIJ (\n. cyclic_gen g ** n) (add_mod (CARD G)).carrier G 161 finite_cyclic_group_add_mod_iso |- !g. cyclic g /\ FINITE G ==> 162 GroupIso (\n. cyclic_gen g ** n) (add_mod (CARD G)) g 163 164 Isomorphism between Cyclic Groups: 165 cyclic_iso_gen |- !g h f. cyclic g /\ cyclic h /\ FINITE G /\ GroupIso f g h ==> 166 f (cyclic_gen g) IN cyclic_generators h 167*) 168 169(* ------------------------------------------------------------------------- *) 170(* Cyclic Group has a generator. *) 171(* ------------------------------------------------------------------------- *) 172 173(* Define Cyclic Group *) 174val cyclic_def = Define` 175 cyclic (g:'a group) <=> Group g /\ ?z. z IN G /\ (!x. x IN G ==> ?n. x = z ** n) 176`; 177 178(* Apply Skolemization *) 179val lemma = prove( 180 ``!(g:'a group). ?z. cyclic g ==> z IN G /\ !x. x IN G ==> ?n. x = z ** n``, 181 metis_tac[cyclic_def]); 182(* 183- SKOLEM_THM; 184> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm 185*) 186(* Define cyclic generator *) 187(* 188- SIMP_RULE bool_ss [SKOLEM_THM] lemma; 189> val it = |- ?f. !g. cyclic g ==> f g IN G /\ !x. x IN G ==> ?n. x = f g ** n: thm 190*) 191val cyclic_gen_def = new_specification( 192 "cyclic_gen_def", 193 ["cyclic_gen"], 194 SIMP_RULE bool_ss [SKOLEM_THM] lemma); 195(* 196> val cyclic_gen_def = |- 197 !g. cyclic g ==> cyclic_gen g IN G /\ !x. x IN G ==> ?n. x = cyclic_gen g ** n: thm 198*) 199 200(* Theorem: cyclic g ==> Group g *) 201(* Proof: by cyclic_def *) 202val cyclic_group = store_thm( 203 "cyclic_group", 204 ``!g:'a group. cyclic g ==> Group g``, 205 rw[cyclic_def]); 206 207(* export simple result *) 208val _ = export_rewrites ["cyclic_group"]; 209 210(* Theorem: cyclic g ==> !x. x IN G ==> ?n. x = (cyclic_gen g) ** n *) 211(* Proof: by cyclic_gen_def. *) 212val cyclic_element = store_thm( 213 "cyclic_element", 214 ``!g:'a group. cyclic g ==> (!x. x IN G ==> ?n. x = (cyclic_gen g) ** n)``, 215 rw[cyclic_gen_def]); 216 217(* Theorem cyclic g ==> (cyclic_gen g) IN G *) 218(* Proof: by cyclic_gen_def. *) 219val cyclic_gen_element = store_thm( 220 "cyclic_gen_element", 221 ``!g:'a group. cyclic g ==> (cyclic_gen g) IN G``, 222 rw[cyclic_gen_def]); 223 224(* Theorem: FiniteGroup g ==> !x. x IN G ==> cyclic (gen x) *) 225(* Proof: 226 By cyclic_def, this is to show: 227 (1) x IN G ==> Group (gen x) 228 True by generated_group. 229 (2) ?z. z IN (Gen x) /\ !x'. x' IN (Gen x) ==> ?n. x' = (gen x).exp z n 230 x IN (Gen x) by generated_gen_element 231 Let z = x, the assertion is true by generated_element 232*) 233val cyclic_generated_group = store_thm( 234 "cyclic_generated_group", 235 ``!g:'a group. FiniteGroup g ==> !x. x IN G ==> cyclic (gen x)``, 236 rpt strip_tac >> 237 `Group g /\ FINITE G` by metis_tac[FiniteGroup_def] >> 238 rw[cyclic_def] >- 239 rw[generated_group] >> 240 `x IN (Gen x)` by rw[generated_gen_element] >> 241 metis_tac[generated_subgroup, generated_element, subgroup_exp, subgroup_element]); 242 243(* Theorem: cyclic g /\ FINITE G ==> ord (cyclic_gen g) = CARD G *) 244(* Proof: 245 Let z = cyclic_gen g. 246 !x. x IN G ==> ?n. x = z ** n by cyclic_element 247 ==> x IN (Gen z) by generated_element 248 Hence G SUBSET (Gen z) by SUBSET_DEF 249 But (gen z) <= g by generated_subgroup 250 So (Gen z) SUBSET G by Subgroup_def 251 Hence (Gen z) = G by SUBSET_ANTISYM 252 or ord z = CARD (Gen z) by generated_group_card, group_order_pos 253 = CARD G by above 254*) 255val cyclic_gen_order = store_thm( 256 "cyclic_gen_order", 257 ``!g:'a group. cyclic g /\ FINITE G ==> (ord (cyclic_gen g) = CARD G)``, 258 rpt strip_tac >> 259 `Group g /\ cyclic_gen g IN G /\ !x. x IN G ==> ?n. x = cyclic_gen g ** n` by rw[cyclic_gen_def] >> 260 `FiniteGroup g` by rw[FiniteGroup_def] >> 261 `G SUBSET (Gen (cyclic_gen g))` by rw[generated_element, SUBSET_DEF] >> 262 `(Gen (cyclic_gen g)) SUBSET G` by metis_tac[generated_subgroup, Subgroup_def] >> 263 metis_tac[generated_group_card, group_order_pos, SUBSET_ANTISYM]); 264 265(* Theorem: cyclic g /\ FINITE G ==> 266 !n. 0 < n /\ ((CARD G) MOD n = 0) ==> (ord (cyclic_gen g ** (CARD G DIV n)) = n) *) 267(* Proof: 268 First, Group g by cyclic_group 269 Therefore FiniteGroup g by FiniteGroup_def 270 Let t = (cyclic_gen g) ** m, where m = (CARD G) DIV n. 271 Since (cyclic_gen g) IN G by cyclic_gen_element 272 so t IN G by group_exp_element 273 Since ord (cyclic_gen g) = CARD G by cyclic_gen_order 274 so ord t * gcd (CARD G) m = CARD G by group_order_power 275 276 But CARD G 277 = m * n + ((CARD G) MOD n) by DIVISION 278 = m * n since (CARD G) MOD n = 0 279 = n * m by MULT_COMM 280 so gcd (CARD G) m = m by GCD_MULTIPLE_ALT 281 282 But CARD G <> 0 by group_carrier_nonempty, CARD_EQ_0 283 so m = (CARD G) DIV n <> 0 by GCD_EQ_0 284 Therefore ord t * m = n * m 285 or ord t = n by MULT_RIGHT_CANCEL 286*) 287val cyclic_gen_power_order = store_thm( 288 "cyclic_gen_power_order", 289 ``!g:'a group. cyclic g /\ FINITE G ==> 290 !n. 0 < n /\ ((CARD G) MOD n = 0) ==> (ord (cyclic_gen g ** (CARD G DIV n)) = n)``, 291 rpt strip_tac >> 292 `Group g` by rw[] >> 293 `FiniteGroup g` by rw[FiniteGroup_def] >> 294 qabbrev_tac `m = (CARD G) DIV n` >> 295 qabbrev_tac `t = (cyclic_gen g) ** m` >> 296 `(cyclic_gen g) IN G` by rw[cyclic_gen_element] >> 297 `t IN G` by rw[Abbr`t`] >> 298 `ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >> 299 `ord t * gcd (CARD G) m = CARD G` by metis_tac[group_order_power] >> 300 `CARD G = m * n + ((CARD G) MOD n)` by rw[DIVISION, Abbr`m`] >> 301 `_ = n * m` by rw[MULT_COMM] >> 302 `gcd (CARD G) m = m` by metis_tac[GCD_MULTIPLE_ALT] >> 303 `m <> 0` by metis_tac[group_carrier_nonempty, CARD_EQ_0, GCD_EQ_0] >> 304 metis_tac[MULT_RIGHT_CANCEL]); 305 306(* Theorem: cyclic g ==> (g = (gen (cyclic_gen g))) *) 307(* Proof: 308 Since cyclic g ==> Group g by cyclic_group 309 Let z = cyclic_gen g. 310 Then z IN G by cyclic_gen_element 311 and (Gen z) SUBSET G by generated_subset 312 Now, show: G SUBSET (Gen z) 313 or show: x IN G ==> x IN (Gen z) by SUBSET_DEF 314 Since cyclic g and x IN G, 315 ?j. x = z ** j by cyclic_gen_def 316 hence x IN x IN (Gen z) by generated_element 317 318 Thus (Gen z) SUBSET G 319 and G SUBSET (Gen z) 320 ==> G = Gen z by SUBSET_ANTISYM 321 also (gen z).op = $* 322 and (gen z).id = #e by generated_property 323 Therefore g = (gen z) by monoid_component_equality 324*) 325val xcyclic_generated_by_gen = store_thm( 326 "xcyclic_generated_by_gen", 327 ``!g:'a group. cyclic g ==> (g = (gen (cyclic_gen g)))``, 328 rpt strip_tac >> 329 `Group g` by rw[] >> 330 qabbrev_tac `z = cyclic_gen g` >> 331 `z IN G` by rw[cyclic_gen_element, Abbr`z`] >> 332 `(Gen z) SUBSET G` by rw[generated_subset] >> 333 `G SUBSET (Gen z)` by metis_tac[SUBSET_DEF, cyclic_gen_def, generated_element] >> 334 `G = Gen z` by rw[SUBSET_ANTISYM] >> 335 metis_tac[monoid_component_equality, generated_property]); 336 337(* Theorem: cyclic g /\ FINITE G ==> !x. x IN G ==> 338 ?n. n < CARD G /\ (x = (cyclic_gen g) ** n) *) 339(* Proof: 340 Since cyclic g ==> Group g by cyclic_group 341 so FiniteGroup g by FiniteGroup_def 342 Let z = cyclic_gen g, m = CARD G. 343 Then z IN G by cyclic_gen_element 344 and 0 < m by finite_group_card_pos 345 also ord z = m by cyclic_gen_order 346 Now ?k. x = z ** k by cyclic_element 347 Since k MOD m < m by MOD_LESS 348 and z ** k = z (k MOD m) by group_exp_mod, 0 < m 349 Just take n = k MOD m. 350*) 351val cyclic_element_by_gen = store_thm( 352 "cyclic_element_by_gen", 353 ``!g:'a group. cyclic g /\ FINITE G ==> !x. x IN G ==> 354 ?n. n < CARD G /\ (x = (cyclic_gen g) ** n)``, 355 rpt strip_tac >> 356 `Group g` by rw[] >> 357 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 358 qabbrev_tac `z = cyclic_gen g` >> 359 qabbrev_tac `m = CARD G` >> 360 `z IN G` by rw[cyclic_gen_element, Abbr`z`] >> 361 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 362 `ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >> 363 `?k. x = z ** k` by rw[cyclic_element, Abbr`z`] >> 364 qexists_tac `k MOD m` >> 365 metis_tac[group_exp_mod, MOD_LESS]); 366 367(* Theorem: cyclic g /\ FINITE G ==> !x. x IN G ==> 368 x IN (Gen ((cyclic_gen g) ** ((CARD G) DIV (ord x)))) *) 369(* Proof: 370 Since cyclic g ==> Group g by cyclic_group 371 so FiniteGroup g by FiniteGroup_def, FINITE G 372 Let z = cyclic_gen g, m = CARD G. 373 Then z IN G by cyclic_gen_element 374 and ord z = m by cyclic_gen_order 375 and 0 < m by finite_group_card_pos 376 Let n = ord x, k = m DIV n, y = z ** k. 377 To show: x IN (Gen y) 378 Note n divides m by group_order_divides 379 Since x IN G, 380 ?t. x = z ** t by cyclic_element 381 But x ** n = #e by order_property 382 or (z ** t) ** n = #e by x = z ** t 383 or z ** (t * n) = #e by group_exp_mult 384 Thus m divides (t * n) by group_order_divides_exp, m = ord z 385 so k divides t by dividend_divides_divisor_multiple, n divides m 386 Hence ?s. t = s * k by divides_def 387 and x = z ** t 388 = z ** (s * k) by t = s * k 389 = z ** (k * s) by MULT_COMM 390 = (z ** k) ** s by group_exp_mult 391 = y ** s by y = z ** k 392 Therefore x IN (Gen y) by generated_element 393*) 394val cyclic_element_in_generated = store_thm( 395 "cyclic_element_in_generated", 396 ``!g:'a group. cyclic g /\ FINITE G ==> !x. x IN G ==> 397 x IN (Gen ((cyclic_gen g) ** ((CARD G) DIV (ord x))))``, 398 rpt strip_tac >> 399 `Group g ` by rw[] >> 400 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 401 qabbrev_tac `m = CARD G` >> 402 qabbrev_tac `z = cyclic_gen g` >> 403 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 404 `z IN G /\ (ord z = m)` by rw[GSYM cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 405 qabbrev_tac `n = ord x` >> 406 qabbrev_tac `k = m DIV n` >> 407 qabbrev_tac `y = z ** k` >> 408 `n divides m` by rw[group_order_divides, Abbr`n`, Abbr`m`] >> 409 `?t. x = z ** t` by rw[cyclic_element, Abbr`z`] >> 410 `x ** n = #e` by rw[order_property, Abbr`n`] >> 411 `z ** (t * n) = #e` by rw[group_exp_mult] >> 412 `m divides (t * n)` by rw[GSYM group_order_divides_exp] >> 413 `k divides t` by rw[GSYM dividend_divides_divisor_multiple, Abbr`k`] >> 414 `?s. t = s * k` by rw[GSYM divides_def] >> 415 `x = y ** s` by metis_tac[group_exp_mult, MULT_COMM] >> 416 metis_tac[generated_element]); 417 418(* Theorem: cyclic g /\ FINITE G ==> !n. n divides CARD G ==> ?x. x IN G /\ (ord x = n) *) 419(* Proof: 420 Note cyclic g ==> Group g by cyclic_group 421 and Group g /\ FINITE G ==> FiniteGroup g by FiniteGroup_def 422 Let z = cyclic_gen g, m = CARD G. 423 Note 0 < m by finite_group_card_pos 424 Then z IN G by cyclic_gen_element 425 and ord z = m by cyclic_gen_order 426 Let x = z ** (m DIV n), 427 Then x IN G by group_exp_element 428 and ord x = n by group_order_exp_cofactor, 0 < m 429*) 430val cyclic_finite_has_order_divisor = store_thm( 431 "cyclic_finite_has_order_divisor", 432 ``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> ?x. x IN G /\ (ord x = n)``, 433 rpt strip_tac >> 434 `Group g` by rw[] >> 435 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 436 qabbrev_tac `z = cyclic_gen g` >> 437 qabbrev_tac `m = CARD G` >> 438 `z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 439 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 440 qabbrev_tac `x = z ** (m DIV n)` >> 441 metis_tac[group_order_exp_cofactor, group_exp_element]); 442 443(* ------------------------------------------------------------------------- *) 444(* Cyclic Group Properties *) 445(* ------------------------------------------------------------------------- *) 446 447(* Theorem: FiniteGroup g ==> cyclic g <=> ?z. z IN G /\ (ord z = CARD G) *) 448(* Proof: 449 If part: cyclic g ==> ?z. z IN G /\ (ord z = CARD G) 450 Let z = cyclic_gen g. 451 cyclic g ==> z IN G by cyclic_gen_element 452 cyclic g /\ FINITE G ==> (ord z = CARD G) by cyclic_gen_order 453 Only-if part: ?z. z IN G /\ (ord z = CARD G) ==> cyclic g 454 Note 0 < CARD G by finite_group_card_pos 455 (Gen z) SUBSET G by generated_subset 456 CARD (Gen z) = ord z by generated_group_card 457 (Gen z) = G by SUBSET_EQ_CARD 458 Thus !x. x IN G ==> ?n. x = z ** n by generated_element 459*) 460val cyclic_finite_alt = store_thm( 461 "cyclic_finite_alt", 462 ``!g:'a group. FiniteGroup g ==> (cyclic g <=> (?z. z IN G /\ (ord z = CARD G)))``, 463 rpt strip_tac >> 464 `Group g /\ FINITE G` by metis_tac[FiniteGroup_def] >> 465 rw[EQ_IMP_THM] >- 466 metis_tac[cyclic_gen_element, cyclic_gen_order] >> 467 rw[cyclic_def] >> 468 qexists_tac `z` >> 469 rw[] >> 470 `(Gen z) SUBSET G` by metis_tac[generated_subset] >> 471 `CARD (Gen z) = ord z` by rw[generated_group_card, finite_group_card_pos] >> 472 `Gen z = G` by metis_tac[SUBSET_EQ_CARD, SUBSET_FINITE] >> 473 metis_tac[generated_element]); 474 475(* Theorem: cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x) *) 476(* Proof: 477 Let z = cyclic_gen g. 478 x IN G ==> ?n. x = z ** n by cyclic_element 479 y IN G ==> ?m. y = z ** m by cyclic_element 480 x * y 481 = (z ** n) * (z ** m) 482 = z ** (n + m) by group_exp_add 483 = z ** (m + n) by ADD_COMM 484 = (z ** m) * (z ** n) by group_exp_add 485 = y * x 486*) 487val cyclic_group_comm = store_thm( 488 "cyclic_group_comm", 489 ``!g:'a group. cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x)``, 490 metis_tac[cyclic_group, cyclic_gen_def, cyclic_element, group_exp_add, ADD_COMM]);; 491 492(* Theorem: cyclic g ==> AbelianGroup g *) 493(* Proof: by cyclic_group_comm, cyclic_group, AbelianGroup_def *) 494val cyclic_group_abelian = store_thm( 495 "cyclic_group_abelian", 496 ``!g:'a group. cyclic g ==> AbelianGroup g``, 497 rw[cyclic_group_comm, AbelianGroup_def]); 498 499(* ------------------------------------------------------------------------- *) 500(* Cyclic Subgroups *) 501(* ------------------------------------------------------------------------- *) 502 503(* Theorem: cyclic g /\ h <= g ==> cyclic h *) 504(* Proof: 505 Let z = cyclic_gen g. 506 h <= g <=> Group h /\ Group g /\ H SUBSET G by Subgroup_def 507 Hence H <> {} by group_carrier_nonempty 508 and #e IN H by group_id_element, subgroup_id 509 If H = {#e}, 510 !x. x IN H ==> x = #e, #e ** 1 = #e by group_exp_1, IN_SING 511 Hence cyclic h by cyclic_def 512 If H <> {#e}, there is an x IN H and x <> #e by ONE_ELEMENT_SING 513 !x. x IN H ==> x IN G by SUBSET_DEF 514 ==> ?n. x = z ** n by cyclic_element 515 Let m = MIN_SET {n | 0 < n /\ z ** n IN H} 516 Let s = z ** m, s IN H by group_exp_element 517 Then for any x IN H, ?n. x = z ** n by above 518 Now n = q * m + r by DIVISION 519 x = z ** n 520 = z ** (q * m + r) 521 = z ** q * m * z ** r by group_comm_op_exp 522 = (z ** m) ** q * z ** r by group_exp_mult, MULT_COMM 523 = s ** q * z ** r 524 Hence z ** r = |/ (s ** q) * x by group_rsolve 525 or z ** r IN H by group_op_element, group_exp_element 526 But 0 <= r < m, and m is minimum. 527 Hence r = 0, or z ** r = #e by group_exp_0 528 Therefore for any x IN H, ?q. x = s ** q. 529 Result follows by cyclic_def. 530*) 531val cyclic_subgroup_cyclic = store_thm( 532 "cyclic_subgroup_cyclic", 533 ``!g h:'a group. cyclic g /\ h <= g ==> cyclic h``, 534 rpt strip_tac >> 535 `Group g /\ (cyclic_gen g) IN G` by rw[cyclic_gen_def] >> 536 `Group h /\ (h.op = g.op) /\ !x. x IN H ==> x IN G` by metis_tac[Subgroup_def, SUBSET_DEF] >> 537 qabbrev_tac `z = cyclic_gen g` >> 538 `H <> {}` by rw[group_carrier_nonempty] >> 539 `#e IN H` by metis_tac[subgroup_id, group_id_element] >> 540 `!x. x IN H ==> ?n. x = z ** n` by rw[cyclic_element, Abbr`z`] >> 541 `!x. x IN H ==> !n. h.exp x n = x ** n` by rw[subgroup_exp] >> 542 `!x. x IN H ==> (h.inv x = |/ x)` by rw[subgroup_inv] >> 543 rw[cyclic_def] >> 544 Cases_on `H = {#e}` >- 545 rw[] >> 546 `?x. x IN H /\ x <> #e` by metis_tac[ONE_ELEMENT_SING] >> 547 `?n. x = z ** n` by rw[] >> 548 `n <> 0` by metis_tac[group_exp_0] >> 549 `0 < n` by decide_tac >> 550 qabbrev_tac `s = {n | 0 < n /\ z ** n IN H}` >> 551 `n IN s` by rw[Abbr`s`] >> 552 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 553 `MIN_SET s IN s /\ !n. n IN s ==> MIN_SET s <= n` by metis_tac[MIN_SET_LEM] >> 554 qabbrev_tac `m = MIN_SET s` >> 555 `!n. n IN s <=> 0 < n /\ z ** n IN H` by rw[Abbr`s`] >> 556 `0 < m /\ z ** m IN H` by metis_tac[] >> 557 qexists_tac `z ** m` >> 558 rw[] >> 559 `?n'. x' = z ** n'` by rw[] >> 560 `?q r. ?r q. (n' = q * m + r) /\ r < m` by rw[DA] >> 561 `x' = z ** (q * m + r)` by rw[] >> 562 `_ = z ** (q * m) * z ** r` by rw[group_exp_add] >> 563 `_ = z ** (m * q) * z ** r` by metis_tac[MULT_COMM] >> 564 `_ = (z ** m) ** q * z ** r` by metis_tac[group_exp_mult] >> 565 `(z ** m) ** q IN H` by metis_tac[group_exp_element] >> 566 Cases_on `r = 0` >- 567 metis_tac[group_exp_0, group_rid] >> 568 `0 < r` by decide_tac >> 569 `|/ ((z ** m) ** q) IN H` by metis_tac[group_inv_element] >> 570 `z ** r IN H` by metis_tac[group_rsolve, group_exp_element, group_op_element] >> 571 `m <= r` by metis_tac[] >> 572 `~(r < m)` by decide_tac); 573 574(* Theorem: cyclic g /\ FINITE G ==> !n. (?h. h <= g /\ (CARD H = n)) <=> (n divides (CARD G)) *) 575(* Proof: 576 If part: h <= g ==> CARD H divides CARD G 577 True by Lagrange_thm. 578 Only-if part: n divides CARD G ==> ?h. h <= g /\ (CARD H = n) 579 Let z = cyclic_gen g, m = CARD G. 580 Then z IN G by cyclic_gen_element 581 and (ord z = m) by cyclic_gen_order 582 Since n divides m, 583 ?k. m = k * n by divides_def 584 Thus k divides m by divides_def, MULT_COMM 585 and gcd k m = k by divides_iff_gcd_fix 586 Note Group g by cyclic_group 587 and FiniteGroup g by FiniteGroup_def, FINITE G. 588 Let x = z ** k, 589 Then x IN G by group_exp_element 590 and n * k 591 = m by MULT_COMM, m = k * n 592 = ord (z ** k) * gcd m k by group_order_power 593 = ord x * gcd k m by GCD_SYM 594 = ord x * k by above 595 Since 0 < m, m <> 0 by finite_group_card_pos 596 so k <> 0 and n <> 0 by MULT_EQ_0 597 thus ord x = n by EQ_MULT_RCANCEL, k <> 0 598 Take h = gen x, 599 then h <= g by generated_subgroup 600 and CARD (Gen x) 601 = ord x = n by generated_group_card 602*) 603val cyclic_subgroup_condition = store_thm( 604 "cyclic_subgroup_condition", 605 ``!g:'a group. cyclic g /\ FINITE G ==> !n. (?h. h <= g /\ (CARD H = n)) <=> (n divides (CARD G))``, 606 rw[EQ_IMP_THM] >- 607 rw[Lagrange_thm] >> 608 qabbrev_tac `z = cyclic_gen g` >> 609 qabbrev_tac `m = CARD G` >> 610 `z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 611 `?k. m = k * n` by rw[GSYM divides_def] >> 612 `k divides m` by metis_tac[divides_def, MULT_COMM] >> 613 `gcd k m = k` by rw[GSYM divides_iff_gcd_fix] >> 614 qabbrev_tac `x = z ** k` >> 615 `Group g ` by rw[] >> 616 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 617 `ord x * k = n * k` by metis_tac[group_order_power, GCD_SYM, MULT_COMM] >> 618 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 619 `m <> 0` by decide_tac >> 620 `k <> 0 /\ n <> 0` by metis_tac[MULT_EQ_0] >> 621 `ord x = n` by metis_tac[EQ_MULT_RCANCEL] >> 622 `x IN G` by rw[Abbr`x`] >> 623 qexists_tac `gen x` >> 624 metis_tac[generated_subgroup, generated_group_card, NOT_ZERO_LT_ZERO]); 625 626(* ------------------------------------------------------------------------- *) 627(* Cyclic Group Examples *) 628(* ------------------------------------------------------------------------- *) 629 630(* Theorem: FINITE G /\ cyclic g ==> 631 !n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier) *) 632(* Proof: 633 cyclic g 634 ==> AbelianGroup g by cyclic_group_abelian 635 ==> (uroots n) <= g by group_uroots_subgroup 636 ==> cyclic (uroots n) by cyclic_subgroup_cyclic 637 ==> (cyclic_gen (uroots n)) IN (uroots n).carrier 638 by cyclic_gen_element 639 ==> ord (cyclic_gen (uroots n)) = CARD (uroots n) 640 by cyclic_gen_order, subgroup_order 641*) 642val cyclic_uroots_has_primitive = store_thm( 643 "cyclic_uroots_has_primitive", 644 ``!g:'a group. FINITE G /\ cyclic g ==> 645 !n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier)``, 646 rpt strip_tac >> 647 `Group g` by rw[] >> 648 `AbelianGroup g` by rw[cyclic_group_abelian] >> 649 `(uroots n) <= g` by rw[group_uroots_subgroup] >> 650 `cyclic (uroots n)` by metis_tac[cyclic_subgroup_cyclic] >> 651 `(cyclic_gen (uroots n)) IN (uroots n).carrier` by rw[cyclic_gen_element] >> 652 metis_tac[cyclic_gen_order, subgroup_order, Subgroup_def, SUBSET_FINITE]); 653 654(* This cyclic_uroots_has_primitive, originally for the next one, is not used. *) 655 656(* Theorem: cyclic g ==> cyclic (uroots n) *) 657(* Proof: 658 Note AbelianGroup g by cyclic_group_abelian 659 and (uroots n) <= g by group_uroots_subgroup 660 Thus cyclic (uroots n) by cyclic_subgroup_cyclic 661*) 662val cyclic_uroots_cyclic = store_thm( 663 "cyclic_uroots_cyclic", 664 ``!g:'a group. cyclic g ==> !n. cyclic (uroots n)``, 665 rpt strip_tac >> 666 `AbelianGroup g` by rw[cyclic_group_abelian] >> 667 `(uroots n) <= g` by rw[group_uroots_subgroup] >> 668 metis_tac[cyclic_subgroup_cyclic]); 669 670(* Theorem: 1 < n ==> (order (add_mod n) 1 = n) *) 671(* Proof: 672 Since 1 IN (add_mod n).carrier by add_mod_element, 1 < n 673 and !m. (add_mod n).exp 1 m = m MOD n by add_mod_exp, 0 < n 674 Therefore, 675 (add_mod n).exp 1 n = n MOD n = 0 by DIVMOD_ID, 0 < n 676 and !m. 0 < m /\ m < n, 677 (add_mod n).exp 1 m = m <> 0 by NOT_ZERO_LT_ZERO, 0 < n 678 Now (add_mod n).id = 0 by add_mod_property 679 so order (add_mod n) 1 = n by group_order_thm 680*) 681val add_mod_order_1 = store_thm( 682 "add_mod_order_1", 683 ``!n. 1 < n ==> (order (add_mod n) 1 = n)``, 684 rpt strip_tac >> 685 `0 < n` by decide_tac >> 686 `!m. (add_mod n).exp 1 m = m MOD n` by rw[add_mod_exp] >> 687 `1 IN (add_mod n).carrier` by rw[add_mod_element] >> 688 `(add_mod n).exp 1 n = 0` by rw[] >> 689 `!m. 0 < m /\ m < n ==> (add_mod n).exp 1 m <> 0` by rw[NOT_ZERO_LT_ZERO] >> 690 metis_tac[group_order_thm, add_mod_property]); 691 692(* Theorem: 0 < n ==> cyclic (add_mod n) *) 693(* Proof: 694 Note Group (add_mod n) by add_mod_group 695 and FiniteGroup (add_mod n) by add_mod_finite_group 696 and (add_mod n).id = 0 by add_mod_property 697 and CARD (add_mod n).carrier = n by add_mod_property 698 If n = 1, 699 Since order (add_mod 1) 0 = 1 by group_order_id 700 and 0 IN (add_mod 1).carrier by group_id_element 701 and CARD (add_mod 1).carrier = 1 by above 702 Thus cyclic (add_mod 1) by cyclic_finite_alt 703 If n <> 1, 1 < n. 704 Since 1 IN (add_mod n).carrier by add_mod_element, 1 < n 705 and order (add_mod n) 1 = n by add_mod_order_1, 1 < n 706 Thus cyclic (add_mod n) by cyclic_finite_alt 707*) 708val add_mod_cylic = store_thm( 709 "add_mod_cylic", 710 ``!n. 0 < n ==> cyclic (add_mod n)``, 711 rpt strip_tac >> 712 `Group (add_mod n)` by rw[add_mod_group] >> 713 `FiniteGroup (add_mod n)` by rw[add_mod_finite_group] >> 714 `((add_mod n).id = 0) /\ (CARD (add_mod n).carrier = n)` by rw[add_mod_property] >> 715 Cases_on `n = 1` >- 716 metis_tac[cyclic_finite_alt, group_order_id, group_id_element] >> 717 `1 < n` by decide_tac >> 718 metis_tac[cyclic_finite_alt, add_mod_order_1, add_mod_element]); 719 720(* ------------------------------------------------------------------------- *) 721(* Order of elements in a Cyclic Group *) 722(* ------------------------------------------------------------------------- *) 723 724(* 725From FiniteField theory, knowing that F* is cyclic, we can prove stronger results: 726(1) Let G be cyclic with |G| = n, so it has a generator z with (order z = n). 727(2) All elements in G are known: 1, g, g^2, ...., g^(n-1). 728(3) Thus all their orders are known: n/gcd(0,n), n/gcd(1,n), n/gcd(2,n), ..., n/gcd(n-1,n). 729(4) Counting, CARD (order_eq k) = phi k. 730(5) As a result, n = SUM (phi k), over k | n. 731*) 732 733(* ------------------------------------------------------------------------- *) 734(* Cyclic Generators *) 735(* ------------------------------------------------------------------------- *) 736 737(* Define the set of generators for cyclic group *) 738val cyclic_generators_def = Define ` 739 cyclic_generators (g:'a group) = {z | z IN G /\ (ord z = CARD G)} 740`; 741 742(* Theorem: z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G) *) 743(* Proof: by cyclic_generators_def *) 744val cyclic_generators_element = store_thm( 745 "cyclic_generators_element", 746 ``!g:'a group. !z. z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G)``, 747 rw[cyclic_generators_def]); 748 749(* Theorem: (cyclic_generators g) SUBSET G *) 750(* Proof: by cyclic_generators_def, SUBSET_DEF *) 751val cyclic_generators_subset = store_thm( 752 "cyclic_generators_subset", 753 ``!g:'a group. (cyclic_generators g) SUBSET G``, 754 rw[cyclic_generators_def, SUBSET_DEF]); 755 756(* Theorem: FINITE G ==> FINITE (cyclic_generators g) *) 757(* Proof: by cyclic_generators_subset, SUBSET_FINITE *) 758val cyclic_generators_finite = store_thm( 759 "cyclic_generators_finite", 760 ``!g:'a group. FINITE G ==> FINITE (cyclic_generators g)``, 761 metis_tac[cyclic_generators_subset, SUBSET_FINITE]); 762 763(* Theorem: cyclic g /\ FINITE G ==> (cyclic_generators g) <> {} *) 764(* Proof: 765 Let z = cyclic_gen g, m = CARD G. 766 Then z IN G by cyclic_gen_element 767 and ord z = m by cyclic_gen_order, FINITE G 768 Hence z IN cyclic_generators g by cyclic_generators_element 769 or (cyclic_generators g) <> {} by MEMBER_NOT_EMPTY 770*) 771val cyclic_generators_nonempty = store_thm( 772 "cyclic_generators_nonempty", 773 ``!g:'a group. cyclic g /\ FINITE G ==> (cyclic_generators g) <> {}``, 774 metis_tac[cyclic_generators_element, cyclic_gen_element, cyclic_gen_order, MEMBER_NOT_EMPTY]); 775 776(* Theorem: cyclic g /\ FINITE G ==> 777 BIJ (\j. (cyclic_gen g) ** j) (coprimes (CARD G)) (cyclic_generators g) *) 778(* Proof: 779 Since cyclic g ==> Group g by cyclic_group 780 so FiniteGroup g by FiniteGroup_def, FINITE G 781 Let z = cyclic_gen g, m = CARD G. 782 Then z IN G by cyclic_gen_element 783 and ord z = m by cyclic_gen_order 784 and 0 < m by finite_group_card_pos 785 Expanding by BIJ_DEF, INJ_DEF, and SURJ_DEF, this is to show: 786 (1) z IN G /\ (ord z = m) /\ j IN coprimes m ==> z ** j IN cyclic_generators g 787 Since z ** j IN G by group_exp_element 788 and coprime j m by coprimes_element 789 so ord (z ** j) = m by group_order_power_eq_order 790 Hence z ** j IN cyclic_generators g by cyclic_generators_element 791 (2) z IN G /\ (ord z = m) /\ j IN coprimes m /\ j' IN coprimes m /\ z ** j = z ** j' ==> j = j' 792 If m = 1, 793 then coprimes 1 = {1} by coprimes_1 794 hence j = 1 = j' by IN_SING 795 If m <> 1, 1 < m. 796 then j IN coprimes m ==> j < m by coprimes_element_less 797 and j' IN coprimes m ==> j' < m by coprimes_element_less 798 Therefore j = j' by group_exp_equal 799 (3) same as (1) 800 (4) z IN G /\ (ord z = m) /\ x IN cyclic_generators g ==> ?j. j IN coprimes m /\ (z ** j = x) 801 Since x IN cyclic_generators g 802 ==> x IN G /\ (ord x = m) by cyclic_generators_element 803 Also ?k. k < m /\ (x = z ** k) by cyclic_element_by_gen 804 If m = 1, 805 then ord x = 1 ==> x = #e by group_order_eq_1 806 then ord z = 1 ==> z = #e by group_order_eq_1 807 Take j = 1, 808 and 1 IN (coprimes 1) by coprimes_1, IN_SING 809 with z ** 1 = x by group_exp_1 810 If m <> 1, 811 then x <> #e by group_order_eq_1 812 thus k <> 0 by group_exp_0 813 so 0 < k, and k < m ==> k <= m by LESS_IMP_LESS_OR_EQ 814 Also ord (z ** k) = m ==> coprime k m by group_order_power_eq_order 815 Take j = k, and j IN coprimes m by coprimes_element 816*) 817val cyclic_generators_coprimes_bij = store_thm( 818 "cyclic_generators_coprimes_bij", 819 ``!g:'a group. cyclic g /\ FINITE G ==> 820 BIJ (\j. (cyclic_gen g) ** j) (coprimes (CARD G)) (cyclic_generators g)``, 821 rpt strip_tac >> 822 `Group g ` by rw[] >> 823 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 824 qabbrev_tac `z = cyclic_gen g` >> 825 qabbrev_tac `m = CARD G` >> 826 `z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 827 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 828 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >| [ 829 qabbrev_tac `m = ord z` >> 830 `coprime j m` by metis_tac[coprimes_element] >> 831 `z ** j IN G` by rw[] >> 832 `ord (z ** j) = m` by metis_tac[group_order_power_eq_order] >> 833 metis_tac[cyclic_generators_element], 834 qabbrev_tac `m = ord z` >> 835 Cases_on `m = 1` >- 836 metis_tac[coprimes_1, IN_SING] >> 837 `1 < m` by decide_tac >> 838 metis_tac[coprimes_element_less, group_exp_equal], 839 qabbrev_tac `m = ord z` >> 840 `coprime j m` by metis_tac[coprimes_element] >> 841 `z ** j IN G` by rw[] >> 842 `ord (z ** j) = m` by metis_tac[group_order_power_eq_order] >> 843 metis_tac[cyclic_generators_element], 844 qabbrev_tac `m = ord z` >> 845 `x IN G /\ (ord x = m)` by metis_tac[cyclic_generators_element] >> 846 `?k. k < m /\ (x = z ** k)` by metis_tac[cyclic_element_by_gen] >> 847 Cases_on `m = 1` >- 848 metis_tac[group_order_eq_1, coprimes_1, IN_SING, group_exp_1] >> 849 `x <> #e` by metis_tac[group_order_eq_1] >> 850 `k <> 0` by metis_tac[group_exp_0] >> 851 `0 < k /\ k <= m` by decide_tac >> 852 metis_tac[group_order_power_eq_order, coprimes_element] 853 ]); 854 855(* Theorem: cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G)) *) 856(* Proof: 857 Let z = cyclic_gen g, m = CARD G. 858 Then z IN G by cyclic_gen_element 859 and ord z = m by cyclic_gen_order 860 Now BIJ (\j. z ** j) (coprimes m) (cyclic_generators g) by cyclic_generators_coprimes_bij 861 Since FINITE (coprimes m) by coprimes_finite 862 and FINITE (cyclic_generators g) by cyclic_generators_finite 863 Hence CARD (cyclic_generators g) 864 = CARD (coprimes m) by FINITE_BIJ_CARD_EQ 865 = phi m by phi_def 866*) 867val cyclic_generators_card = store_thm( 868 "cyclic_generators_card", 869 ``!g:'a group. cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G))``, 870 rpt strip_tac >> 871 qabbrev_tac `z = cyclic_gen g` >> 872 qabbrev_tac `m = CARD G` >> 873 `z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 874 `BIJ (\j. z ** j) (coprimes m) (cyclic_generators g)` by rw[cyclic_generators_coprimes_bij, Abbr`z`, Abbr`m`] >> 875 `FINITE (coprimes m)` by rw[coprimes_finite] >> 876 `FINITE (cyclic_generators g)` by rw[cyclic_generators_finite] >> 877 metis_tac[phi_def, FINITE_BIJ_CARD_EQ]); 878 879(* 880Goolge: order of elements in a cyclic group. 881 882Pattern of orders of elements in a cyclic group 883http://math.stackexchange.com/questions/158281/pattern-of-orders-of-elements-in-a-cyclic-group 884 885The number of elements of order d, where d is a divisor of n, is ��(d). 886 887Let G be a cyclic group of order n, and let a in G be a generator. Let d be a divisor of n. 888 889Certainly, a^{n/d} is an element of G of order d (in other words, <a^{n/d}> is a subgroup of G of order d). 890If a^{t} in G is an element of order d, then (a^{t})^{d} = e, hence n ��� td, and thus (n/d) ��� t. 891This shows that a^{t} in <a^{n/d}>, and thus <a^{t}> = <a^{n/d}> (since they are both subgroups of order d). 892Thus, there is exactly one subgroup, let's call it H_{d}, of G of order d, for each divisor d of n, 893and all of these subgroups are themselves cyclic. 894 895Any cyclic group of order d has ��(d) generators, i.e. there are ��(d) elements of order d in H_{d}, 896and hence there are ��(d) elements of order d in G. Here, �� is Euler's phi function. 897 898This can be checked to make sense via the identity: n = SUM ��(d), over d | n. 899*) 900 901(* Theorem: cyclic g /\ FINITE G ==> !n. n divides (CARD G) ==> 902 (cyclic_generators (Generated g ((cyclic_gen g) ** ((CARD G) DIV n))) = orders g n) *) 903(* Proof: 904 Since cyclic g ==> Group g by cyclic_group 905 so FiniteGroup g by FiniteGroup_def, FINITE G 906 Let z = cyclic_gen g, m = CARD G. 907 Then z IN G by cyclic_gen_element 908 and ord z = m by cyclic_gen_order 909 and 0 < m by finite_group_card_pos 910 911 Let k = m DIV n, y = z ** k, h = Generated g y. 912 Then y IN G by group_exp_element 913 and h <= g by generated_subgroup, y IN G 914 915 Expanding by cyclic_generators_def, orders_def, this is to show: 916 (1) h <= g /\ x IN H ==> x IN G 917 True by Subgroup_def, SUBSET_DEF. 918 (2) h <= g /\ order h x = CARD H ==> ord x = n 919 Note ord x = CARD H by subgroup_order 920 = ord y by generated_group_card, group_order_pos 921 = n by group_order_exp_cofactor 922 (3) h <= g /\ x IN G /\ (ord x) divides m ==> x IN H 923 True by cyclic_element_in_generated. 924 (4) h <= g /\ x IN G ==> order h x = CARD H 925 Note x IN H by cyclic_element_in_generated 926 and (ord x) divides m by group_order_divides 927 order h x 928 = ord x by subgroup_order, x IN H 929 = ord (z ** k) by group_order_exp_cofactor, (ord x) divides m = ord z 930 = ord y by y = z ** k 931 = CARD H by generated_group_card, group_order_pos 932*) 933val cyclic_generators_gen_cofactor_eq_orders = store_thm( 934 "cyclic_generators_gen_cofactor_eq_orders", 935 ``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides (CARD G) ==> 936 (cyclic_generators (Generated g ((cyclic_gen g) ** ((CARD G) DIV n))) = orders g n)``, 937 rpt strip_tac >> 938 `Group g ` by rw[] >> 939 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 940 qabbrev_tac `m = CARD G` >> 941 qabbrev_tac `z = cyclic_gen g` >> 942 `z IN G` by rw[cyclic_gen_element, Abbr`z`] >> 943 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 944 `ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >> 945 qabbrev_tac `k = m DIV n` >> 946 qabbrev_tac `y = z ** k` >> 947 qabbrev_tac `h = Generated g y` >> 948 `y IN G` by rw[Abbr`y`, Abbr`z`] >> 949 `h <= g` by rw[generated_subgroup, Abbr`h`] >> 950 rw[cyclic_generators_def, orders_def, EXTENSION, EQ_IMP_THM] >- 951 metis_tac[Subgroup_def, SUBSET_DEF] >- 952 metis_tac[subgroup_order, generated_group_card, group_order_exp_cofactor, group_order_pos] >- 953 metis_tac[cyclic_element_in_generated] >> 954 qabbrev_tac `m = ord z` >> 955 qabbrev_tac `n = ord x` >> 956 `x IN H` by metis_tac[cyclic_element_in_generated] >> 957 `order h x = n` by rw[subgroup_order, Abbr`n`] >> 958 `ord y = n` by rw[group_order_exp_cofactor, Abbr`m`, Abbr`y`, Abbr`k`] >> 959 `CARD H = ord y` by rw[generated_group_card, group_order_pos, Abbr`h`] >> 960 decide_tac); 961 962(* Theorem: cyclic g /\ FINITE G ==> 963 !n. CARD (orders g n) = if (n divides CARD G) then phi n else 0 *) 964(* Proof: 965 Let m = CARD G. 966 Note 0 < m by finite_group_card_pos 967 Since cyclic g ==> Group g by cyclic_group 968 so FiniteGroup g by FiniteGroup_def, FINITE G 969 Let z = cyclic_gen g, m = CARD G. 970 Then z IN G by cyclic_gen_element 971 and ord z = m by cyclic_gen_order 972 If n divides m, to show: CARD (orders g n) = phi n 973 Let k = m DIV n, y = z ** k, h = Generated g y. 974 Then y IN G by group_exp_element 975 and ord y = n by group_order_exp_cofactor 976 also h <= g by generated_subgroup 977 and CARD H = n by generated_group_card, group_order_pos 978 Also cyclic h by cyclic_subgroup_cyclic 979 and FINITE H by finite_subgroup_carrier_finite 980 Hence CARD (orders g n) 981 = CARD (cyclic_generators h) by cyclic_generators_gen_cofactor_eq_orders 982 = phi n by cyclic_generators_card, FINITE H 983 984 If ~(n divides m), to show: CARD (orders g n) = 0 985 By contradiction, suppose CARD (orders g n) <> 0. 986 Since FINITE (orders g n) by orders_finite 987 so orders g n <> {} by CARD_EQ_0 988 Thus ?x. x IN orders g n by MEMBER_NOT_EMPTY 989 or x IN G /\ (ord x = n) by orders_element 990 Now (ord x) divides m by group_order_divides 991 which contradicts ~(n divides m). 992*) 993val cyclic_orders_card = store_thm( 994 "cyclic_orders_card", 995 ``!g:'a group. cyclic g /\ FINITE G ==> 996 !n. CARD (orders g n) = if (n divides CARD G) then phi n else 0``, 997 rpt strip_tac >> 998 `Group g ` by rw[] >> 999 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 1000 qabbrev_tac `z = cyclic_gen g` >> 1001 qabbrev_tac `m = CARD G` >> 1002 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 1003 `z IN G` by rw[cyclic_gen_element, Abbr`z`] >> 1004 `ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >> 1005 Cases_on `n divides m` >| [ 1006 simp[] >> 1007 qabbrev_tac `k = m DIV n` >> 1008 qabbrev_tac `y = z ** k` >> 1009 qabbrev_tac `h = Generated g y` >> 1010 `y IN G` by rw[Abbr`y`] >> 1011 `ord y = n` by metis_tac[group_order_exp_cofactor] >> 1012 `h <= g` by rw[generated_subgroup, Abbr`h`] >> 1013 `CARD H = n` by rw[generated_group_card, group_order_pos, Abbr`h`] >> 1014 `cyclic h` by metis_tac[cyclic_subgroup_cyclic] >> 1015 `FINITE H` by metis_tac[finite_subgroup_carrier_finite] >> 1016 metis_tac[cyclic_generators_gen_cofactor_eq_orders, cyclic_generators_card], 1017 simp[] >> 1018 spose_not_then strip_assume_tac >> 1019 `FINITE (orders g n)` by rw[orders_finite] >> 1020 `orders g n <> {}` by rw[GSYM CARD_EQ_0] >> 1021 metis_tac[MEMBER_NOT_EMPTY, orders_element, group_order_divides] 1022 ]); 1023 1024(* ------------------------------------------------------------------------- *) 1025(* Partition by order equality *) 1026(* ------------------------------------------------------------------------- *) 1027 1028(* Define a relation: eq_order *) 1029val eq_order_def = Define ` 1030 eq_order (g:'a group) x y <=> (ord x = ord y) 1031`; 1032 1033(* Theorem: (eq_order g) equiv_on G *) 1034(* Proof: by eq_order_def, equiv_on_def *) 1035val eq_order_equiv = store_thm( 1036 "eq_order_equiv", 1037 ``!g:'a group. (eq_order g) equiv_on G``, 1038 rw[eq_order_def, equiv_on_def]); 1039 1040(* Theorem: cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {} *) 1041(* Proof: 1042 Let z = cyclic_gen g, m = CARD G. 1043 Note 0 < m by finite_group_card_pos 1044 Then z IN G by cyclic_gen_element 1045 and ord z = m by cyclic_gen_order 1046 Let x = z ** (m DIV n) 1047 Then x IN G by group_exp_element 1048 and ord x = n by group_order_exp_cofactor 1049 so x IN (orders g n) by orders_element 1050 Thus orders g n <> {} by MEMBER_NOT_EMPTY 1051*) 1052val cyclic_orders_nonempty = store_thm( 1053 "cyclic_orders_nonempty", 1054 ``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {}``, 1055 rpt strip_tac >> 1056 `Group g ` by rw[] >> 1057 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 1058 qabbrev_tac `z = cyclic_gen g` >> 1059 qabbrev_tac `m = CARD G` >> 1060 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 1061 `z IN G` by rw[cyclic_gen_element, Abbr`z`] >> 1062 `ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >> 1063 qabbrev_tac `x = z ** (m DIV n)` >> 1064 `x IN G` by rw[Abbr`x`] >> 1065 `ord x = n` by metis_tac[group_order_exp_cofactor] >> 1066 metis_tac[orders_element, MEMBER_NOT_EMPTY]); 1067 1068(* Theorem: cyclic g /\ FINITE G ==> 1069 (partition (eq_order g) G = {orders g n | n | n divides (CARD G)}) *) 1070(* Proof: 1071 Expanding by partition_def, eq_order_def, orders_def, this is to show: 1072 (1) x' IN G /\ ... ==> ?n. ... (ord x' = n) ... /\ n divides CARD G 1073 Let n = ord x', 1074 Result is true since n divides CARD G by group_order_divides 1075 (2) n divides CARD G /\ ... (ord x'' = n) ... ==> ?x'. x' IN G /\ ... (ord x' = ord x'') ... 1076 Since n divides CARD G 1077 ==> (orders g n) <> {} by cyclic_orders_nonempty 1078 ==> ?z. z IN G /\ (ord z = n) by orders_element, , MEMBER_NOT_EMPTY 1079 Let x' = z, then the result follows. 1080*) 1081val cyclic_eq_order_partition = store_thm( 1082 "cyclic_eq_order_partition", 1083 ``!g:'a group. cyclic g /\ FINITE G ==> 1084 (partition (eq_order g) G = {orders g n | n | n divides (CARD G)})``, 1085 rpt strip_tac >> 1086 `Group g ` by rw[] >> 1087 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 1088 rw[partition_def, eq_order_def, orders_def, EXTENSION, EQ_IMP_THM] >- 1089 metis_tac[group_order_divides] >> 1090 metis_tac[orders_element, cyclic_orders_nonempty, MEMBER_NOT_EMPTY]); 1091 1092(* Theorem: cyclic g /\ FINITE G ==> 1093 (partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)}) *) 1094(* Proof: 1095 Note Group g by cyclic_group 1096 so FiniteGroup g by FiniteGroup_def 1097 ==> 0 < CARD G by finite_group_card_pos, FiniteGroup g 1098 partition (eq_order g) G 1099 = {orders g n | n | n divides (CARD G)} by cyclic_eq_order_partition 1100 = {orders g n | n | n IN divisors (CARD G)} by rw[divisors_element_alt 1101*) 1102val cyclic_eq_order_partition_alt = store_thm( 1103 "cyclic_eq_order_partition_alt", 1104 ``!g:'a group. cyclic g /\ FINITE G ==> 1105 (partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)})``, 1106 rpt strip_tac >> 1107 `0 < CARD G` by metis_tac[finite_group_card_pos, cyclic_group, FiniteGroup_def] >> 1108 rw[cyclic_eq_order_partition, divisors_element_alt]); 1109 1110(* We have shown: in a finite cyclic group G, 1111 For each divisor d | |G|, there are phi(d) elements of order d. 1112 Since each element must have some order in a finite group, 1113 the sum of phi(d) over all divisors d will count all elements in the group, 1114 that is, n = SUM phi(d), over d | n. 1115*) 1116 1117(* Theorem: cyclic g /\ FINITE G ==> 1118 (IMAGE CARD (partition (eq_order g) g.carrier) = IMAGE phi (divisors (CARD G))) *) 1119(* Proof: 1120 Since cyclic g ==> Group g by cyclic_group 1121 so FiniteGroup g by FiniteGroup_def 1122 Let z = cyclic_gen g, m = CARD G. 1123 Then z IN G by cyclic_gen_element 1124 and ord z = m by cyclic_gen_order 1125 and 0 < m by finite_group_card_pos 1126 1127 Apply partition_def, eq_order_def, to show: 1128 (1) ?x''. (CARD s = phi x'') /\ x'' IN divisors m 1129 Note s = orders g n by orders_def 1130 Let n = ord x'', y = z ** (m DIV n). 1131 Then n divides m by group_order_divides 1132 and y IN G by group_exp_element 1133 and ord y = n by group_order_exp_cofactor 1134 Since 0 < m, n IN divisors m by divisors_element_alt 1135 hence CARD s = phi n by cyclic_orders_card 1136 So take x'' = n. 1137 (2) x' IN divisors m ==> ?x''. (phi x' = CARD x'') /\ ?x. x IN orders g x' 1138 Let n = x', y = z ** (m DIV n). 1139 Since n IN divisors m, 1140 ==> n divides m by divisors_element 1141 Let s = orders g n, 1142 Then CARD s = phi n by cyclic_orders_card 1143 and y IN G by group_exp_element 1144 and ord y = n by group_order_exp_cofactor 1145 so y IN orders g n by orders_element 1146 So take x'' = y. 1147*) 1148val cyclic_eq_order_partition_by_card = store_thm( 1149 "cyclic_eq_order_partition_by_card", 1150 ``!g:'a group. cyclic g /\ FINITE G ==> 1151 (IMAGE CARD (partition (eq_order g) g.carrier) = IMAGE phi (divisors (CARD G)))``, 1152 rpt strip_tac >> 1153 `Group g` by rw[] >> 1154 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 1155 qabbrev_tac `m = CARD G` >> 1156 qabbrev_tac `z = cyclic_gen g` >> 1157 `z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >> 1158 `0 < m` by rw[finite_group_card_pos, Abbr`m`] >> 1159 rw[partition_def, eq_order_def, EXTENSION, EQ_IMP_THM] >| [ 1160 qabbrev_tac `m = ord z` >> 1161 qabbrev_tac `n = ord x''` >> 1162 (`x' = orders g n` by (rw[orders_def, EXTENSION] >> metis_tac[])) >> 1163 qabbrev_tac `y = z ** (m DIV n)` >> 1164 `n divides m` by metis_tac[group_order_divides] >> 1165 `y IN G` by rw[Abbr`y`] >> 1166 `ord y = n` by rw[group_order_exp_cofactor, Abbr`y`, Abbr`m`] >> 1167 metis_tac[cyclic_orders_card, divisors_element_alt], 1168 qabbrev_tac `m = ord z` >> 1169 qabbrev_tac `n = x'` >> 1170 qabbrev_tac `y = z ** (m DIV n)` >> 1171 `n <= m /\ n divides m` by metis_tac[divisors_element] >> 1172 `y IN G` by rw[Abbr`y`] >> 1173 `ord y = n` by rw[group_order_exp_cofactor, Abbr`y`, Abbr`m`] >> 1174 metis_tac[cyclic_orders_card, orders_element] 1175 ]); 1176 1177(* Theorem: eq_order g = feq ord *) 1178(* Proof: 1179 eq_order g x y 1180 <=> ord x = ord y by eq_order_def 1181 <=> feq ord x y by feq_def 1182 Hence true by FUN_EQ_THM. 1183*) 1184val eq_order_is_feq_order = store_thm( 1185 "eq_order_is_feq_order", 1186 ``!g:'a group. eq_order g = feq ord``, 1187 rw[eq_order_def, feq_def, FUN_EQ_THM]); 1188 1189(* Theorem: orders g = feq_class ord G *) 1190(* Proof: 1191 orders g n 1192 = {x | x IN G /\ (ord x = n)} by orders_def 1193 = feq_class ord G n by feq_class_def 1194 Hence true by FUN_EQ_THM. 1195*) 1196val orders_is_feq_class_order = store_thm( 1197 "orders_is_feq_class_order", 1198 ``!g:'a group. orders g = feq_class ord G``, 1199 rw[orders_def, feq_class_def, FUN_EQ_THM]); 1200 1201(* Theorem: cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G)) *) 1202(* Proof: 1203 Note cyclic g ==> Group g by cyclic_group 1204 and Group g /\ FINITE G ==> FiniteGroup g by FiniteGroup_def 1205 If part: x IN G ==> ord x <= CARD G /\ (ord x) divides (CARD G) 1206 Since FiniteGroup g ==> 0 < CARD G by finite_group_card_pos 1207 also ==> (ord x) divides (CARD G) by group_order_divides 1208 Hence ord x <= CARD G by DIVIDES_LE 1209 Only-if part: n <= CARD G /\ n divides CARD G ==> ?x. x IN G /\ (ord x = n) 1210 True by cyclic_finite_has_order_divisor. 1211*) 1212val cyclic_image_ord_is_divisors = store_thm( 1213 "cyclic_image_ord_is_divisors", 1214 ``!g:'a group. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G))``, 1215 rpt strip_tac >> 1216 `Group g` by rw[] >> 1217 `FiniteGroup g` by metis_tac[FiniteGroup_def] >> 1218 rw[EXTENSION, divisors_def, EQ_IMP_THM] >- 1219 rw[group_order_divides, DIVIDES_LE, finite_group_card_pos] >- 1220 rw[group_order_divides] >> 1221 metis_tac[cyclic_finite_has_order_divisor]); 1222 1223(* Theorem: cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))) *) 1224(* Proof: 1225 Since cyclic g /\ FINITE G 1226 ==> FiniteGroup g by FiniteGroup_def, cyclic_group 1227 so 0 < CARD G by finite_group_card_pos 1228 Then partition (eq_order g) G 1229 = {orders g n | n | n divides CARD G} by cyclic_eq_order_partition 1230 = IMAGE (orders g) (divisors (CARD G)) by divisors_def, EXTENSION, DIVIDES_LE 1231*) 1232val cyclic_orders_partition = store_thm( 1233 "cyclic_orders_partition", 1234 ``!g:'a group. cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G)))``, 1235 rpt strip_tac >> 1236 `FiniteGroup g` by metis_tac[FiniteGroup_def, cyclic_group] >> 1237 `0 < CARD G` by rw[finite_group_card_pos] >> 1238 `partition (eq_order g) G = {orders g n | n | n divides CARD G}` by rw[cyclic_eq_order_partition] >> 1239 rw[divisors_def, EXTENSION] >> 1240 metis_tac[DIVIDES_LE]); 1241 1242(* ------------------------------------------------------------------------- *) 1243(* Finite Cyclic Group Existence. *) 1244(* ------------------------------------------------------------------------- *) 1245 1246(* Theorem: 0 < n ==> ?g:num group. cyclic g /\ (CARD g.carrier = n) *) 1247(* Proof: 1248 Let g = add_mod n. 1249 Then cyclic (add_mod n) by add_mod_cylic 1250 and CARD g.carrier = n by add_mod_card 1251*) 1252val finite_cyclic_group_existence = store_thm( 1253 "finite_cyclic_group_existence", 1254 ``!n. 0 < n ==> ?g:num group. cyclic g /\ (CARD g.carrier = n)``, 1255 rpt strip_tac >> 1256 qexists_tac `add_mod n` >> 1257 rpt strip_tac >- 1258 rw[add_mod_cylic] >> 1259 rw[add_mod_card]); 1260 1261(* ------------------------------------------------------------------------- *) 1262(* Cyclic Group index relative to a generator. *) 1263(* ------------------------------------------------------------------------- *) 1264 1265(* Extract cyclic index w.r.t a generator *) 1266 1267(* Theorem: cyclic g /\ x IN G ==> ?n. (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G) *) 1268(* Proof: 1269 Note Group g by cyclic_def 1270 and cyclic_gen g IN G /\ 1271 ?k. x = (cyclic_gen g) ** k by cyclic_gen_def 1272 If FINITE G, 1273 Then FiniteGroup g by FiniteGroup_def 1274 so 0 < CARD G by finite_group_card_pos 1275 and ord (cyclic_gen g) = CARD G by cyclic_gen_order 1276 Take n = k MOD (CARD G). 1277 Then (cyclic_gen g) ** n 1278 = (cyclic_gen g) ** k by group_exp_mod, 0 < CARD G 1279 = x by above 1280 and n < CARD G by MOD_LESS, 0 < CARD G 1281 If INFINITE G, 1282 Take n = k, the result follows. 1283*) 1284val cyclic_index_exists = store_thm( 1285 "cyclic_index_exists", 1286 ``!(g:'a group) x. cyclic g /\ x IN G ==> ?n. (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G)``, 1287 rpt strip_tac >> 1288 `Group g` by rw[] >> 1289 `cyclic_gen g IN G /\ ?n. x = (cyclic_gen g) ** n` by rw[cyclic_gen_def] >> 1290 Cases_on `FINITE G` >| [ 1291 rw[] >> 1292 `FiniteGroup g` by rw[FiniteGroup_def] >> 1293 `0 < CARD G` by rw[finite_group_card_pos] >> 1294 `ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >> 1295 qexists_tac `n MOD (CARD G)` >> 1296 rw[Once group_exp_mod], 1297 metis_tac[] 1298 ]); 1299 1300(* Apply Skolemization *) 1301val lemma = prove( 1302 ``!(g:'a group) x. ?n. cyclic g /\ x IN G ==> (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G)``, 1303 metis_tac[cyclic_index_exists]); 1304(* 1305- SKOLEM_THM; 1306> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm 1307*) 1308(* Define cyclic generator *) 1309(* 1310- SIMP_RULE (bool_ss) [SKOLEM_THM] lemma; 1311> val it = 1312 |- ?f. !g x. cyclic g /\ x IN G ==> x = cyclic_gen g ** f g x /\ (FINITE G ==> f g x < CARD G): thm 1313*) 1314val cyclic_index_def = new_specification( 1315 "cyclic_index_def", 1316 ["cyclic_index"], 1317 SIMP_RULE bool_ss [SKOLEM_THM] lemma); 1318(* 1319val cyclic_index_def = 1320 |- !g x. cyclic g /\ x IN G ==> x = cyclic_gen g ** cyclic_index g x /\ 1321 (FINITE G ==> cyclic_index g x < CARD G): thm 1322*) 1323 1324(* Theorem: cyclic g /\ FINITE G ==> 1325 !n. n < CARD G ==> (cyclic_index g (cyclic_gen g ** n) = n) *) 1326(* Proof: 1327 Note Group g by cyclic_group 1328 ==> FiniteGroup g by FiniteGroup_def 1329 Let x = (cyclic_gen g) ** n. 1330 Note cyclic_gen g IN G by cyclic_gen_def 1331 Then x IN G by group_exp_element 1332 Thus (x = (cyclic_gen g) ** (cyclic_index g x)) /\ 1333 cyclic_index g x < CARD G by cyclic_index_def 1334 Now ord (cyclic_gen g) = CARD G by cyclic_gen_order 1335 and 0 < CARD G by finite_group_card_pos 1336 Thus n = cyclic_index g x by group_exp_equal 1337*) 1338val finite_cyclic_index_property = store_thm( 1339 "finite_cyclic_index_property", 1340 ``!g:'a group. cyclic g /\ FINITE G ==> 1341 !n. n < CARD G ==> (cyclic_index g ((cyclic_gen g) ** n) = n)``, 1342 rpt strip_tac >> 1343 `Group g` by rw[] >> 1344 `FiniteGroup g` by rw[FiniteGroup_def] >> 1345 qabbrev_tac `x = (cyclic_gen g) ** n` >> 1346 `cyclic_gen g IN G` by rw[cyclic_gen_def] >> 1347 `x IN G` by rw[Abbr`x`] >> 1348 `(x = (cyclic_gen g) ** (cyclic_index g x)) /\ cyclic_index g x < CARD G` by fs[cyclic_index_def] >> 1349 `ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >> 1350 metis_tac[group_exp_equal, finite_group_card_pos]); 1351 1352(* Theorem: cyclic g /\ FINITE G /\ x IN G ==> 1353 !n. n < CARD G ==> ((x = (cyclic_gen g) ** n) <=> (n = cyclic_index g x)) *) 1354(* Proof: 1355 If part: (x = (cyclic_gen g) ** n) ==> (n = cyclic_index g x) 1356 This is true by finite_cyclic_index_property. 1357 Only-if part: (n = cyclic_index g x) ==> (x = (cyclic_gen g) ** n) 1358 This is true by cyclic_index_def 1359*) 1360val finite_cyclic_index_unique = store_thm( 1361 "finite_cyclic_index_unique", 1362 ``!g:'a group x. cyclic g /\ FINITE G /\ x IN G ==> 1363 !n. n < CARD G ==> ((x = (cyclic_gen g) ** n) <=> (n = cyclic_index g x))``, 1364 rpt strip_tac >> 1365 `Group g` by rw[] >> 1366 rw[cyclic_index_def, EQ_IMP_THM] >> 1367 rw[finite_cyclic_index_property]); 1368 1369(* Theorem: cyclic g /\ FINITE G /\ x IN G /\ y IN G ==> 1370 (cyclic_index g (x * y) = ((cyclic_index g x) + (cyclic_index g y)) MOD (CARD G)) *) 1371(* Proof: 1372 Note Group g by cyclic_group 1373 so FiniteGroup g by FiniteGroup_def 1374 and x * y IN G by group_op_element 1375 Let z = cyclic_gen g. 1376 Then z IN G by cyclic_gen_def 1377 and ord z = CARD G by cyclic_gen_order 1378 Note 0 < CARD G by finite_group_card_pos 1379 Let h = cyclic_index g x, k = cyclic_index g y. 1380 z ** ((h + k) MOD CARD G) 1381 = z ** (h + k) by group_exp_mod 1382 = (z ** h) * (z ** k) by group_exp_add 1383 = x * y by cyclic_index_def 1384 Note (h + k) MOD (CARD G) < CARD G by MOD_LESS 1385 Thus (h + k) MOD (CARD G) = cyclic_index g (x * y) by finite_cyclic_index_unique 1386*) 1387val finite_cyclic_index_add = store_thm( 1388 "finite_cyclic_index_add", 1389 ``!g:'a group x y. cyclic g /\ FINITE G /\ x IN G /\ y IN G ==> 1390 (cyclic_index g (x * y) = ((cyclic_index g x) + (cyclic_index g y)) MOD (CARD G))``, 1391 rpt strip_tac >> 1392 `Group g` by rw[] >> 1393 `FiniteGroup g` by rw[FiniteGroup_def] >> 1394 `x * y IN G` by rw[] >> 1395 qabbrev_tac `z = cyclic_gen g` >> 1396 `z IN G` by rw[cyclic_gen_def, Abbr`z`] >> 1397 `ord z = CARD G` by rw[cyclic_gen_order, Abbr`z`] >> 1398 `0 < CARD G` by rw[finite_group_card_pos] >> 1399 qabbrev_tac `h = cyclic_index g x` >> 1400 qabbrev_tac `k = cyclic_index g y` >> 1401 `z ** ((h + k) MOD CARD G) = z ** (h + k)` by metis_tac[group_exp_mod] >> 1402 `_ = (z ** h) * (z ** k)` by rw[] >> 1403 `_ = x * y` by metis_tac[cyclic_index_def] >> 1404 `0 < CARD G` by rw[finite_group_card_pos] >> 1405 `(h + k) MOD (CARD G) < CARD G` by rw[] >> 1406 metis_tac[finite_cyclic_index_unique]); 1407 1408(* ------------------------------------------------------------------------- *) 1409(* Finite Cyclic Group Uniqueness. *) 1410(* ------------------------------------------------------------------------- *) 1411 1412(* Theorem: cyclic g1 /\ cyclic g2 /\ 1413 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1414 GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 *) 1415(* Proof: 1416 Note Group g2 by cyclic_group 1417 and FiniteGroup g2 by FiniteGroup_def 1418 Note cyclic_gen g2 IN g2.carrier by cyclic_gen_def 1419 and order g2 (cyclic_gen g2) = CARD g2.carrier by cyclic_gen_order 1420 1421 By GroupHomo_def, this is to show: 1422 (1) x IN g1.carrier ==> g2.exp (cyclic_gen g2) (cyclic_index g1 x) IN g2.carrier 1423 This is true by group_exp_element 1424 (2) x IN g1.carrier /\ x' IN g1.carrier ==> 1425 g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x')) = 1426 g2.op (g2.exp (cyclic_gen g2) (cyclic_index g1 x)) (g2.exp (cyclic_gen g2) (cyclic_index g1 x')) 1427 1428 g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x')) 1429 = g2.exp (cyclic_gen g2) (((cyclic_index g1 x) + 1430 (cyclic_index g1 x')) MOD (CARD g1.carrier)) by finite_cyclic_index_add 1431 = g2.exp (cyclic_gen g2) ((cyclic_index g1 x) + (cyclic_index g1 x')) by group_exp_mod, group_order_pos 1432 = g2.op (g2.exp (cyclic_gen g2) (cyclic_index g1 x)) 1433 (g2.exp (cyclic_gen g2) (cyclic_index g1 x')) by group_exp_add 1434*) 1435val finite_cyclic_group_homo = store_thm( 1436 "finite_cyclic_group_homo", 1437 ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ 1438 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1439 GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2``, 1440 rpt strip_tac >> 1441 `Group g2 /\ FiniteGroup g2` by rw[FiniteGroup_def, cyclic_group] >> 1442 `cyclic_gen g2 IN g2.carrier` by rw[cyclic_gen_def] >> 1443 `order g2 (cyclic_gen g2) = CARD g2.carrier` by rw[cyclic_gen_order] >> 1444 rw[GroupHomo_def] >> 1445 `g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x')) = 1446 g2.exp (cyclic_gen g2) (((cyclic_index g1 x) + (cyclic_index g1 x')) MOD (CARD g1.carrier))` by rw[finite_cyclic_index_add] >> 1447 `_ = g2.exp (cyclic_gen g2) ((cyclic_index g1 x) + (cyclic_index g1 x'))` by metis_tac[group_exp_mod, group_order_pos] >> 1448 rw[group_exp_add]); 1449 1450(* Theorem: cyclic g1 /\ cyclic g2 /\ 1451 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1452 BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier *) 1453(* Proof: 1454 Note Group g2 by cyclic_group 1455 and FiniteGroup g2 by FiniteGroup_def 1456 Note cyclic_gen g2 IN g2.carrier by cyclic_gen_def 1457 and order g2 (cyclic_gen g2) = CARD g2.carrier by cyclic_gen_order 1458 1459 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 1460 (1) x IN g1.carrier ==> g2.exp (cyclic_gen g2) (cyclic_index g1 x) IN g2.carrier 1461 This is true by group_exp_element 1462 (2) x IN g1.carrier /\ x' IN g1.carrier /\ 1463 g2.exp (cyclic_gen g2) (cyclic_index g1 x) = g2.exp (cyclic_gen g2) (cyclic_index g1 x') ==> x = x' 1464 Note cyclic_index g1 x < CARD g2.carrier by cyclic_index_def 1465 and cyclic_index g1 x' < CARD g2.carrier by cyclic_index_def 1466 Thus cyclic_index g1 x = cyclic_index g1 x' by group_exp_equal, group_order_ps 1467 x 1468 = g1.exp (cyclic_gen g1) (cyclic_index g1 x) by finite_cyclic_index_unique 1469 = g1.exp (cyclic_gen g1) (cyclic_index g1 x') by above 1470 = x' by finite_cyclic_index_unique 1471 (3) x IN g2.carrier ==> ?x'. x' IN g1.carrier /\ g2.exp (cyclic_gen g2) (cyclic_index g1 x') = x 1472 Note Group g1 by cyclic_group 1473 and FiniteGroup g1 by FiniteGroup_def 1474 Note cyclic_gen g1 IN g2.carrier by cyclic_gen_def 1475 and order g1 (cyclic_gen g1) = CARD g1.carrier by cyclic_gen_order 1476 and cyclic_index g2 x < CARD g2.carrier by cyclic_index_def 1477 1478 Let x' = g1.exp (cyclic_gen g1) (cyclic_index g2 x). 1479 Then g1.exp (cyclic_gen g1) (cyclic_index g2 x) IN g1.carrier by group_exp_element 1480 and g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.exp (cyclic_gen g1) (cyclic_index g2 x))) 1481 = g2.exp (cyclic_gen g2) (cyclic_index g2 x) by finite_cyclic_index_property 1482 = x by cyclic_index_def 1483*) 1484val finite_cyclic_group_bij = store_thm( 1485 "finite_cyclic_group_bij", 1486 ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ 1487 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1488 BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier``, 1489 rpt strip_tac >> 1490 `Group g2 /\ FiniteGroup g2` by rw[FiniteGroup_def, cyclic_group] >> 1491 `cyclic_gen g2 IN g2.carrier` by rw[cyclic_gen_def] >> 1492 `order g2 (cyclic_gen g2) = CARD g2.carrier` by rw[cyclic_gen_order] >> 1493 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >| [ 1494 `cyclic_index g1 x < CARD g2.carrier /\ cyclic_index g1 x' < CARD g2.carrier` by metis_tac[cyclic_index_def] >> 1495 `cyclic_index g1 x = cyclic_index g1 x'` by metis_tac[group_exp_equal, group_order_pos] >> 1496 metis_tac[finite_cyclic_index_unique], 1497 `Group g1 /\ FiniteGroup g1` by rw[FiniteGroup_def, cyclic_group] >> 1498 `cyclic_gen g1 IN g1.carrier` by rw[cyclic_gen_def] >> 1499 `order g1 (cyclic_gen g1) = CARD g1.carrier` by rw[cyclic_gen_order] >> 1500 qexists_tac `g1.exp (cyclic_gen g1) (cyclic_index g2 x)` >> 1501 rw[] >> 1502 `cyclic_index g2 x < CARD g2.carrier` by rw[cyclic_index_def] >> 1503 `cyclic_index g1 (g1.exp (cyclic_gen g1) (cyclic_index g2 x)) = cyclic_index g2 x` by fs[finite_cyclic_index_property] >> 1504 rw[cyclic_index_def] 1505 ]); 1506 1507(* Theorem: cyclic g1 /\ cyclic g2 /\ 1508 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1509 GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 *) 1510(* Proof: 1511 By GroupIso_def, this is to show: 1512 (1) GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 1513 This is true by finite_cyclic_group_homo 1514 (2) BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier 1515 This is true by finite_cyclic_group_bij 1516*) 1517val finite_cyclic_group_iso = store_thm( 1518 "finite_cyclic_group_iso", 1519 ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ 1520 FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==> 1521 GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2``, 1522 rw[GroupIso_def] >- 1523 rw[finite_cyclic_group_homo] >> 1524 rw[finite_cyclic_group_bij]); 1525 1526(* Theorem: cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\ 1527 (CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2 *) 1528(* Proof: 1529 Let f = \x. g2.exp (cyclic_gen g2) (cyclic_index g1 x). 1530 The result follows by finite_cyclic_group_iso 1531*) 1532val finite_cyclic_group_uniqueness = store_thm( 1533 "finite_cyclic_group_uniqueness", 1534 ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\ 1535 (CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2``, 1536 metis_tac[finite_cyclic_group_iso]); 1537 1538(* This completes the classification of finite cyclic groups. *) 1539 1540(* Another proof of uniqueness *) 1541 1542(* Theorem: cyclic g /\ FINITE G ==> GroupHomo (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g *) 1543(* Proof: 1544 Note Group g by cyclic_group 1545 and FiniteGroup g by FiniteGroup_def 1546 and cyclic_gen g IN G by cyclic_gen_def 1547 and order g (cyclic_gen g) = CARD G by cyclic_gen_order 1548 By GroupHomo_def, this is to show: 1549 (1) (cyclic_gen g) ** n IN G, true by group_exp_element 1550 (2) n < CARD G /\ n' < CARD G ==> 1551 cyclic_gen g ** ((n + n') MOD CARD G) = cyclic_gen g ** n * cyclic_gen g ** n' 1552 Note cyclic_gen g ** ((n + n') MOD CARD G) 1553 = cyclic_gen g ** (n + n') by group_exp_mod, 0 < CARD G 1554 = cyclic_gen g ** n * cyclic_gen g ** n' by group_exp_add 1555*) 1556val finite_cyclic_group_add_mod_homo = store_thm( 1557 "finite_cyclic_group_add_mod_homo", 1558 ``!g:'a group. cyclic g /\ FINITE G ==> GroupHomo (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g``, 1559 rpt strip_tac >> 1560 `Group g /\ FiniteGroup g` by rw[FiniteGroup_def, cyclic_group] >> 1561 `cyclic_gen g IN G` by rw[cyclic_gen_def] >> 1562 `order g (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >> 1563 rw[GroupHomo_def] >> 1564 `0 < CARD G` by decide_tac >> 1565 `cyclic_gen g ** ((n + n') MOD CARD G) = cyclic_gen g ** (n + n')` by metis_tac[group_exp_mod] >> 1566 rw[]); 1567 1568(* Theorem: cyclic g /\ FINITE G ==> BIJ (\n. (cyclic_gen g) ** n) (add_mod (CARD G)).carrier G *) 1569(* Proof: 1570 Note Group g by cyclic_group 1571 and FiniteGroup g by FiniteGroup_def 1572 and cyclic_gen g IN G by cyclic_gen_def 1573 and order g (cyclic_gen g) = CARD G by cyclic_gen_order 1574 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 1575 (1) (cyclic_gen g) ** n IN G, true by group_exp_element 1576 (2) n < CARD G /\ n' < CARD G /\ cyclic_gen g ** n = cyclic_gen g ** n' ==> n = n' 1577 This is true by finite_cyclic_index_property 1578 (3) x IN G ==> ?n. n < CARD G /\ (cyclic_gen g ** n = x) 1579 This is true by cyclic_index_def 1580*) 1581val finite_cyclic_group_add_mod_bij = store_thm( 1582 "finite_cyclic_group_add_mod_bij", 1583 ``!g:'a group. cyclic g /\ FINITE G ==> BIJ (\n. (cyclic_gen g) ** n) (add_mod (CARD G)).carrier G``, 1584 rpt strip_tac >> 1585 `Group g /\ FiniteGroup g` by rw[FiniteGroup_def, cyclic_group] >> 1586 `cyclic_gen g IN G` by rw[cyclic_gen_def] >> 1587 `order g (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >> 1588 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >- 1589 metis_tac[finite_cyclic_index_property] >> 1590 metis_tac[cyclic_index_def]); 1591 1592(* Theorem: cyclic g /\ FINITE G ==> GroupIso (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g *) 1593(* Proof: 1594 By GroupIso_def, this is to show: 1595 (1) GroupHomo (\n. cyclic_gen g ** n) (add_mod (CARD G)) g 1596 This is true by finite_cyclic_group_add_mod_homo 1597 (2) BIJ (\n. cyclic_gen g ** n) (add_mod (CARD G)).carrier G 1598 This is true by finite_cyclic_group_add_mod_bij 1599*) 1600val finite_cyclic_group_add_mod_iso = store_thm( 1601 "finite_cyclic_group_add_mod_iso", 1602 ``!g:'a group. cyclic g /\ FINITE G ==> GroupIso (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g``, 1603 rw_tac std_ss[GroupIso_def] >- 1604 rw[finite_cyclic_group_add_mod_homo] >> 1605 rw[finite_cyclic_group_add_mod_bij]); 1606 1607(* Theorem: cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\ 1608 (CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2 *) 1609(* Proof: 1610 Note Group g1 by cyclic_group 1611 so FiniteGroup g1 by FiniteGroup_def 1612 ==> 0 < CARD g1.carrier by finite_group_card_pos 1613 Thus Group (add_mod (CARD g1.carrier)) by add_mod_group, 0 < CARD g1.carrier 1614 Let f1 = (\n. g1.exp (cyclic_gen g1) n), 1615 f2 = (\n. g2.exp (cyclic_gen g2) n). 1616 Now GroupIso f1 (add_mod (CARD g1.carrier)) g1 by finite_cyclic_group_add_mod_iso 1617 and GroupIso f2 (add_mod (CARD g2.carrier)) g2 by finite_cyclic_group_add_mod_iso 1618 Thus GroupIso (LINV f1 (add_mod (CARD g1.carrier)).carrier) g1 (add_mod (CARD g1.carrier)) 1619 by group_iso_sym 1620 or ?f. GroupIso f g1 g2 by group_iso_trans 1621*) 1622val finite_cyclic_group_uniqueness = store_thm( 1623 "finite_cyclic_group_uniqueness", 1624 ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\ 1625 (CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2``, 1626 rpt strip_tac >> 1627 `Group g1 /\ FiniteGroup g1` by rw[cyclic_group, FiniteGroup_def] >> 1628 `0 < CARD g1.carrier` by rw[finite_group_card_pos] >> 1629 `Group (add_mod (CARD g1.carrier))` by rw[add_mod_group] >> 1630 `GroupIso (\n. g1.exp (cyclic_gen g1) n) (add_mod (CARD g1.carrier)) g1` by rw[finite_cyclic_group_add_mod_iso] >> 1631 `GroupIso (\n. g2.exp (cyclic_gen g2) n) (add_mod (CARD g2.carrier)) g2` by rw[finite_cyclic_group_add_mod_iso] >> 1632 metis_tac[group_iso_sym, group_iso_trans]); 1633 1634(* ------------------------------------------------------------------------- *) 1635(* Isomorphism between Cyclic Groups *) 1636(* ------------------------------------------------------------------------- *) 1637 1638(* Theorem: cyclic g /\ cyclic h /\ FINITE G /\ 1639 GroupIso f g h ==> f (cyclic_gen g) IN (cyclic_generators h) *) 1640(* Proof: 1641 Note Group g /\ Group h by cyclic_group 1642 and cyclic_gen g IN G by cyclic_gen_element 1643 By cyclic_generators_element, this is to show: 1644 (1) f (cyclic_gen g) IN h.carrier, true by group_iso_element 1645 (2) order h (f (cyclic_gen g)) = CARD h.carrier 1646 order h (f (cyclic_gen g)) 1647 = ord (cyclic_gen g) by group_iso_order 1648 = CARD G by cyclic_gen_order, FINITE G 1649 = CARD h.carrier by group_iso_card_eq 1650*) 1651val cyclic_iso_gen = store_thm( 1652 "cyclic_iso_gen", 1653 ``!(g:'a group) (h:'b group) f. cyclic g /\ cyclic h /\ FINITE G /\ 1654 GroupIso f g h ==> f (cyclic_gen g) IN (cyclic_generators h)``, 1655 rpt strip_tac >> 1656 `Group g /\ Group h` by rw[] >> 1657 `cyclic_gen g IN G` by rw[cyclic_gen_element] >> 1658 rw[cyclic_generators_element] >- 1659 metis_tac[group_iso_element] >> 1660 `order h (f (cyclic_gen g)) = ord (cyclic_gen g)` by rw[group_iso_order] >> 1661 `_ = CARD G` by rw[cyclic_gen_order] >> 1662 metis_tac[group_iso_card_eq]); 1663 1664(* ------------------------------------------------------------------------- *) 1665 1666(* export theory at end *) 1667val _ = export_theory(); 1668 1669(*===========================================================================*) 1670