1(* ------------------------------------------------------------------------- *) 2(* Monoid Maps *) 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 "monoidMap"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* Get dependent theories local *) 20(* val _ = load "monoidOrderTheory"; *) 21open monoidTheory monoidOrderTheory; 22 23(* open dependent theories *) 24open pred_setTheory arithmeticTheory; 25 26(* Get dependent theories in lib *) 27(* (* val _ = load "helperNumTheory"; -- from monoidTheory *) *) 28(* (* val _ = load "helperSetTheory"; -- from monoidTheory *) *) 29open helperNumTheory helperSetTheory; 30 31 32(* ------------------------------------------------------------------------- *) 33(* Monoid Maps Documentation *) 34(* ------------------------------------------------------------------------- *) 35(* Overloading: 36 H = h.carrier 37 o = binary operation of homo_monoid: (homo_monoid g f).op 38 #i = identity of homo_monoid: (homo_monoid g f).id 39 fG = carrier of homo_monoid: (homo_monoid g f).carrier 40*) 41(* Definitions and Theorems (# are exported): 42 43 Homomorphism, isomorphism, endomorphism, automorphism and submonoid: 44 MonoidHomo_def |- !f g h. MonoidHomo f g h <=> 45 (!x. x IN G ==> f x IN h.carrier) /\ (f #e = h.id) /\ 46 !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y)) 47 MonoidIso_def |- !f g h. MonoidIso f g h <=> MonoidHomo f g h /\ BIJ f G h.carrier 48 MonoidEndo_def |- !f g. MonoidEndo f g <=> MonoidHomo f g g 49 MonoidAuto_def |- !f g. MonoidAuto f g <=> MonoidIso f g g 50 submonoid_def |- !h g. submonoid h g <=> MonoidHomo I h g 51 52 Monoid Homomorphisms: 53 monoid_homo_id |- !f g h. MonoidHomo f g h ==> (f #e = h.id) 54 monoid_homo_element |- !f g h. MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier 55 monoid_homo_cong |- !g h f1 f2. Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==> 56 (MonoidHomo f1 g h <=> MonoidHomo f2 g h) 57 monoid_homo_I_refl |- !g. MonoidHomo I g g 58 monoid_homo_trans |- !g h k f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k 59 monoid_homo_sym |- !g h f. Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g 60 monoid_homo_compose |- !g h k f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k 61 monoid_homo_exp |- !g h f. Monoid g /\ MonoidHomo f g h ==> 62 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n 63 64 Monoid Isomorphisms: 65 monoid_iso_property |- !f g h. MonoidIso f g h <=> 66 MonoidHomo f g h /\ !y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y) 67 monoid_iso_id |- !f g h. MonoidIso f g h ==> (f #e = h.id) 68 monoid_iso_element |- !f g h. MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier 69 monoid_iso_monoid |- !g h f. Monoid g /\ MonoidIso f g h ==> Monoid h 70 monoid_iso_I_refl |- !g. MonoidIso I g g 71 monoid_iso_trans |- !g h k f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k 72 monoid_iso_sym |- !g h f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g 73 monoid_iso_compose |- !g h k f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k 74 monoid_iso_exp |- !g h f. Monoid g /\ MonoidIso f g h ==> 75 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n 76 monoid_iso_linv_iso |- !g h f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g 77 monoid_iso_bij |- !g h f. MonoidIso f g h ==> BIJ f G h.carrier 78 monoid_iso_eq_id |- !g h f. Monoid g /\ Monoid h /\ MonoidIso f g h ==> 79 !x. x IN G ==> ((f x = h.id) <=> (x = #e)) 80 monoid_iso_order |- !g h f. Monoid g /\ Monoid h /\ MonoidIso f g h ==> 81 !x. x IN G ==> (order h (f x) = ord x) 82 monoid_iso_card_eq |- !g h f. MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier) 83 84 Monoid Automorphisms: 85 monoid_auto_id |- !f g. MonoidAuto f g ==> (f #e = #e) 86 monoid_auto_element |- !f g. MonoidAuto f g ==> !x. x IN G ==> f x IN G 87 monoid_auto_compose |- !g f1 f2. MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g 88 monoid_auto_exp |- !g f. Monoid g /\ MonoidAuto f g ==> 89 !x. x IN G ==> !n. f (x ** n) = f x ** n 90 monoid_auto_I |- !g. MonoidAuto I g 91 monoid_auto_linv_auto|- !g f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g 92 monoid_auto_bij |- !g f. MonoidAuto f g ==> f PERMUTES G 93 monoid_auto_order |- !g f. Monoid g /\ MonoidAuto f g ==> 94 !x. x IN G ==> (ord (f x) = ord x) 95 96 Submonoids: 97 submonoid_eqn |- !g h. submonoid h g <=> H SUBSET G /\ 98 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e) 99 submonoid_subset |- !g h. submonoid h g ==> H SUBSET G 100 submonoid_homo_homo |- !g h k f. submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k 101 submonoid_refl |- !g. submonoid g g 102 submonoid_trans |- !g h k. submonoid g h /\ submonoid h k ==> submonoid g k 103 submonoid_I_antisym |- !g h. submonoid h g /\ submonoid g h ==> MonoidIso I h g 104 submonoid_carrier_antisym |- !g h. submonoid h g /\ G SUBSET H ==> MonoidIso I h g 105 submonoid_order_eqn |- !g h. Monoid g /\ Monoid h /\ submonoid h g ==> 106 !x. x IN H ==> (order h x = ord x) 107 108 Homomorphic Image of Monoid: 109 image_op_def |- !g f x y. image_op g f x y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)) 110 image_op_inj |- !g f. INJ f G univ(:'b) ==> 111 !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (x * y)) 112 homo_monoid_def |- !g f. homo_monoid g f = <|carrier := IMAGE f G; op := image_op g f; id := f #e|> 113 homo_monoid_property |- !g f. (fG = IMAGE f G) /\ 114 (!x y. x IN fG /\ y IN fG ==> 115 (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))) /\ 116 (#i = f #e) 117 homo_monoid_element |- !g f x. x IN G ==> f x IN fG 118 homo_monoid_id |- !g f. f #e = #i 119 homo_monoid_op_inj |- !g f. INJ f G univ(:'b) ==> !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y) 120 homo_monoid_I |- !g. MonoidIso I (homo_group g I) g 121 122 homo_monoid_closure |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 123 !x y. x IN fG /\ y IN fG ==> x o y IN fG 124 homo_monoid_assoc |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 125 !x y z. x IN fG /\ y IN fG /\ z IN fG ==> ((x o y) o z = x o y o z) 126 homo_monoid_id_property |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> #i IN fG /\ 127 !x. x IN fG ==> (#i o x = x) /\ (x o #i = x) 128 homo_monoid_comm |- !g f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> 129 !x y. x IN fG /\ y IN fG ==> (x o y = y o x) 130 homo_monoid_monoid |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f) 131 homo_monoid_abelian_monoid |- !g f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> 132 AbelianMonoid (homo_monoid g f) 133 homo_monoid_by_inj |- !g f. Monoid g /\ INJ f G univ(:'b) ==> MonoidHomo f g (homo_monoid g f) 134 135 Weaker form of Homomorphic of Monoid and image of identity: 136 WeakHomo_def |- !f g h. WeakHomo f g h <=> 137 (!x. x IN G ==> f x IN h.carrier) /\ 138 !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y)) 139 WeakIso_def |- !f g h. WeakIso f g h <=> WeakHomo f g h /\ BIJ f G h.carrier 140 monoid_weak_iso_id |- !f g h. Monoid g /\ Monoid h /\ WeakIso f g h ==> (f #e = h.id) 141*) 142 143(* ------------------------------------------------------------------------- *) 144(* Homomorphism, isomorphism, endomorphism, automorphism and submonoid. *) 145(* ------------------------------------------------------------------------- *) 146 147(* val _ = overload_on ("H", ``h.carrier``); 148 149- type_of ``H``; 150> val it = ``:'a -> bool`` : hol_type 151 152then MonoidIso f g h = MonoidHomo f g h /\ BIJ f G H 153will make MonoidIso apply only for f: 'a -> 'a. 154 155will need val _ = overload_on ("H", ``(h:'b monoid).carrier``); 156*) 157 158(* A function f from g to h is a homomorphism if monoid properties are preserved. *) 159(* For monoids, need to ensure that identity is preserved, too. See: monoid_weak_iso_id. *) 160val MonoidHomo_def = Define` 161 MonoidHomo (f:'a -> 'b) (g:'a monoid) (h:'b monoid) <=> 162 (!x. x IN G ==> f x IN h.carrier) /\ 163 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))) /\ 164 (f #e = h.id) 165`; 166(* 167If MonoidHomo_def uses the condition: !x y. f (x * y) = h.op (f x) (f y) 168this will mean a corresponding change in GroupHomo_def, but then 169in quotientGroup <<normal_subgroup_coset_homo>> will give a goal: 170h <= g ==> x * y * H = (x * H) o (y * H) with no qualification on x, y! 171*) 172 173(* A function f from g to h is an isomorphism if f is a bijective homomorphism. *) 174val MonoidIso_def = Define` 175 MonoidIso f g h <=> MonoidHomo f g h /\ BIJ f G h.carrier 176`; 177 178(* A monoid homomorphism from g to g is an endomorphism. *) 179val MonoidEndo_def = Define `MonoidEndo f g <=> MonoidHomo f g g`; 180 181(* A monoid isomorphism from g to g is an automorphism. *) 182val MonoidAuto_def = Define `MonoidAuto f g <=> MonoidIso f g g`; 183 184(* A submonoid h of g if identity is a homomorphism from h to g *) 185val submonoid_def = Define `submonoid h g <=> MonoidHomo I h g`; 186 187(* ------------------------------------------------------------------------- *) 188(* Monoid Homomorphisms *) 189(* ------------------------------------------------------------------------- *) 190 191(* Theorem: MonoidHomo f g h ==> (f #e = h.id) *) 192(* Proof: by MonoidHomo_def. *) 193val monoid_homo_id = store_thm( 194 "monoid_homo_id", 195 ``!f g h. MonoidHomo f g h ==> (f #e = h.id)``, 196 rw[MonoidHomo_def]); 197 198(* Theorem: MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier *) 199(* Proof: by MonoidHomo_def *) 200val monoid_homo_element = store_thm( 201 "monoid_homo_element", 202 ``!f g h. MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier``, 203 rw_tac std_ss[MonoidHomo_def]); 204 205(* Theorem: Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==> (MonoidHomo f1 g h = MonoidHomo f2 g h) *) 206(* Proof: by MonoidHomo_def, monoid_op_element, monoid_id_element *) 207val monoid_homo_cong = store_thm( 208 "monoid_homo_cong", 209 ``!g h f1 f2. Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==> 210 (MonoidHomo f1 g h = MonoidHomo f2 g h)``, 211 rw_tac std_ss[MonoidHomo_def, EQ_IMP_THM] >- 212 metis_tac[monoid_op_element] >- 213 metis_tac[monoid_id_element] >- 214 metis_tac[monoid_op_element] >> 215 metis_tac[monoid_id_element]); 216 217(* Theorem: MonoidHomo I g g *) 218(* Proof: by MonoidHomo_def. *) 219val monoid_homo_I_refl = store_thm( 220 "monoid_homo_I_refl", 221 ``!g:'a monoid. MonoidHomo I g g``, 222 rw[MonoidHomo_def]); 223 224(* Theorem: MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo f2 o f1 g k *) 225(* Proof: true by MonoidHomo_def. *) 226val monoid_homo_trans = store_thm( 227 "monoid_homo_trans", 228 ``!(g:'a monoid) (h:'b monoid) (k:'c monoid). 229 !f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k``, 230 rw[MonoidHomo_def]); 231 232(* Theorem: Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g *) 233(* Proof: 234 Note BIJ f G h.carrier 235 ==> BIJ (LINV f G) h.carrier G by BIJ_LINV_BIJ 236 By MonoidHomo_def, this is to show: 237 (1) x IN h.carrier ==> LINV f G x IN G 238 With BIJ (LINV f G) h.carrier G 239 ==> INJ (LINV f G) h.carrier G by BIJ_DEF 240 ==> x IN h.carrier ==> LINV f G x IN G by INJ_DEF 241 (2) x IN h.carrier /\ y IN h.carrier ==> LINV f G (h.op x y) = LINV f G x * LINV f G y 242 With x IN h.carrier 243 ==> ?x1. (x = f x1) /\ x1 IN G by BIJ_DEF, SURJ_DEF 244 With y IN h.carrier 245 ==> ?y1. (y = f y1) /\ y1 IN G by BIJ_DEF, SURJ_DEF 246 and x1 * y1 IN G by monoid_op_element 247 LINV f G (h.op x y) 248 = LINV f G (f (x1 * y1)) by MonoidHomo_def 249 = x1 * y1 by BIJ_LINV_THM, x1 * y1 IN G 250 = (LINV f G (f x1)) * (LINV f G (f y1)) by BIJ_LINV_THM, x1 IN G, y1 IN G 251 = (LINV f G x) * (LINV f G y) by x = f x1, y = f y1. 252 (3) LINV f G h.id = #e 253 Since #e IN G by monoid_id_element 254 LINV f G h.id 255 = LINV f G (f #e) by MonoidHomo_def 256 = #e by BIJ_LINV_THM 257*) 258val monoid_homo_sym = store_thm( 259 "monoid_homo_sym", 260 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==> 261 MonoidHomo (LINV f G) h g``, 262 rpt strip_tac >> 263 `BIJ (LINV f G) h.carrier G` by rw[BIJ_LINV_BIJ] >> 264 fs[MonoidHomo_def] >> 265 rpt strip_tac >- 266 metis_tac[BIJ_DEF, INJ_DEF] >- 267 (`?x1. (x = f x1) /\ x1 IN G` by metis_tac[BIJ_DEF, SURJ_DEF] >> 268 `?y1. (y = f y1) /\ y1 IN G` by metis_tac[BIJ_DEF, SURJ_DEF] >> 269 `g.op x1 y1 IN G` by rw[] >> 270 metis_tac[BIJ_LINV_THM]) >> 271 `#e IN G` by rw[] >> 272 metis_tac[BIJ_LINV_THM]); 273 274(* Theorem: MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k *) 275(* Proof: by MonoidHomo_def *) 276val monoid_homo_compose = store_thm( 277 "monoid_homo_compose", 278 ``!(g:'a monoid) (h:'b monoid) (k:'c monoid). 279 !f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k``, 280 rw_tac std_ss[MonoidHomo_def]); 281(* This is the same as monoid_homo_trans *) 282 283(* Theorem: Monoid g /\ MonoidHomo f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *) 284(* Proof: 285 By induction on n. 286 Base: f (x ** 0) = h.exp (f x) 0 287 f (x ** 0) 288 = f #e by monoid_exp_0 289 = h.id by monoid_homo_id 290 = h.exp (f x) 0 by monoid_exp_0 291 Step: f (x ** SUC n) = h.exp (f x) (SUC n) 292 Note x ** n IN G by monoid_exp_element 293 f (x ** SUC n) 294 = f (x * x ** n) by monoid_exp_SUC 295 = h.op (f x) (f (x ** n)) by MonoidHomo_def 296 = h.op (f x) (h.exp (f x) n) by induction hypothesis 297 = h.exp (f x) (SUC n) by monoid_exp_SUC 298*) 299val monoid_homo_exp = store_thm( 300 "monoid_homo_exp", 301 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidHomo f g h ==> 302 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n``, 303 rpt strip_tac >> 304 Induct_on `n` >- 305 rw[monoid_exp_0, monoid_homo_id] >> 306 fs[monoid_exp_SUC, MonoidHomo_def]); 307 308(* ------------------------------------------------------------------------- *) 309(* Monoid Isomorphisms *) 310(* ------------------------------------------------------------------------- *) 311 312(* Theorem: MonoidIso f g h <=> MonoidHomo f g h /\ (!y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y)) *) 313(* Proof: 314 This is to prove: 315 (1) BIJ f G H /\ y IN H ==> ?!x. x IN G /\ (f x = y) 316 true by INJ_DEF and SURJ_DEF. 317 (2) !y. y IN H /\ MonoidHomo f g h ==> ?!x. x IN G /\ (f x = y) ==> BIJ f G H 318 true by INJ_DEF and SURJ_DEF, and 319 x IN G /\ GroupHomo f g h ==> f x IN H by MonoidHomo_def 320*) 321val monoid_iso_property = store_thm( 322 "monoid_iso_property", 323 ``!f g h. MonoidIso f g h <=> MonoidHomo f g h /\ (!y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y))``, 324 rw_tac std_ss[MonoidIso_def, EQ_IMP_THM] >- 325 metis_tac[BIJ_ALT] >> 326 rw[BIJ_ALT] >> 327 metis_tac[MonoidHomo_def]); 328 329(* Note: all these proofs so far do not require the condition: f #e = h.id in MonoidHomo_def, 330 but evetually it should, as this is included in definitions of all resources. *) 331 332(* Theorem: MonoidIso f g h ==> (f #e = h.id) *) 333(* Proof: by MonoidIso_def, monoid_homo_id. *) 334val monoid_iso_id = store_thm( 335 "monoid_iso_id", 336 ``!f g h. MonoidIso f g h ==> (f #e = h.id)``, 337 rw_tac std_ss[MonoidIso_def, monoid_homo_id]); 338 339(* Theorem: MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier *) 340(* Proof: by MonoidIso_def, monoid_homo_element *) 341val monoid_iso_element = store_thm( 342 "monoid_iso_element", 343 ``!f g h. MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier``, 344 metis_tac[MonoidIso_def, monoid_homo_element]); 345 346(* Theorem: Monoid g /\ MonoidIso f g h ==> Monoid h *) 347(* Proof: 348 This is to show: 349 (1) x IN h.carrier /\ y IN h.carrier ==> h.op x y IN h.carrier 350 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property 351 ?y'. y' IN G /\ (f y' = y) by monoid_iso_property 352 h.op x y = f (x' * y') by MonoidHomo_def 353 As x' * y' IN G by monoid_op_element 354 hence f (x' * y') IN h.carrier by MonoidHomo_def 355 (2) x IN h.carrier /\ y IN h.carrier /\ z IN h.carrier ==> h.op (h.op x y) z = h.op x (h.op y z) 356 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property 357 ?y'. y' IN G /\ (f y' = y) by monoid_iso_property 358 ?z'. z' IN G /\ (f z' = z) by monoid_iso_property 359 as x' * y' IN G by monoid_op_element 360 and f (x' * y') IN h.carrier by MonoidHomo_def 361 ?!t. t IN G /\ f t = f (x' * y') by monoid_iso_property 362 i.e. t = x' * y' by uniqueness 363 hence h.op (h.op x y) z = f (x' * y' * z') by MonoidHomo_def 364 Similary, 365 as y' * z' IN G by monoid_op_element 366 and f (y' * z') IN h.carrier by MonoidHomo_def 367 ?!s. s IN G /\ f s = f (y' * z') by monoid_iso_property 368 i.e. s = y' * z' by uniqueness 369 and h.op x (h.op y z) = f (x' * (y' * z')) by MonoidHomo_def 370 hence true by monoid_assoc. 371 (3) h.id IN h.carrier 372 Since #e IN G by monoid_id_element 373 (f #e) = h.id IN h.carrier by MonoidHomo_def 374 (4) x IN h.carrier ==> h.op h.id x = x 375 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property 376 h.id IN h.carrier by monoid_id_element 377 ?!e. e IN G /\ f e = h.id = f #e by monoid_iso_property 378 i.e. e = #e by uniqueness 379 hence h.op h.id x = f (e * x') by MonoidHomo_def 380 = f (#e * x') 381 = f x' by monoid_lid 382 = x 383 (5) x IN h.carrier ==> h.op x h.id = x 384 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property 385 h.id IN h.carrier by monoid_id_element 386 ?!e. e IN G /\ f e = h.id = f #e by monoid_iso_property 387 i.e. e = #e by uniqueness 388 hence h.op x h.id = f (x' * e) by MonoidHomo_def 389 = f (x' * #e) 390 = f x' by monoid_rid 391 = x 392*) 393val monoid_iso_monoid = store_thm( 394 "monoid_iso_monoid", 395 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> Monoid h``, 396 rw[monoid_iso_property] >> 397 `(!x. x IN G ==> f x IN h.carrier) /\ 398 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))) /\ 399 (f #e = h.id)` by metis_tac[MonoidHomo_def] >> 400 rw_tac std_ss[Monoid_def] >- 401 metis_tac[monoid_op_element] >- 402 (`?x'. x' IN G /\ (f x' = x)` by metis_tac[] >> 403 `?y'. y' IN G /\ (f y' = y)` by metis_tac[] >> 404 `?z'. z' IN G /\ (f z' = z)` by metis_tac[] >> 405 `?t. t IN G /\ (t = x' * y')` by metis_tac[monoid_op_element] >> 406 `h.op (h.op x y) z = f (x' * y' * z')` by metis_tac[] >> 407 `?s. s IN G /\ (s = y' * z')` by metis_tac[monoid_op_element] >> 408 `h.op x (h.op y z) = f (x' * (y' * z'))` by metis_tac[] >> 409 `x' * y' * z' = x' * (y' * z')` by rw[monoid_assoc] >> 410 metis_tac[]) >- 411 metis_tac[monoid_id_element, MonoidHomo_def] >- 412 metis_tac[monoid_lid, monoid_id_element] >> 413 metis_tac[monoid_rid, monoid_id_element]); 414 415(* Theorem: MonoidIso I g g *) 416(* Proof: 417 By MonoidIso_def, this is to show: 418 (1) MonoidHomo I g g, true by monoid_homo_I_refl 419 (2) BIJ I R R, true by BIJ_I_SAME 420*) 421val monoid_iso_I_refl = store_thm( 422 "monoid_iso_I_refl", 423 ``!g:'a monoid. MonoidIso I g g``, 424 rw[MonoidIso_def, monoid_homo_I_refl, BIJ_I_SAME]); 425 426(* Theorem: MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k *) 427(* Proof: 428 By MonoidIso_def, this is to show: 429 (1) MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k 430 True by monoid_homo_trans. 431 (2) BIJ f1 G h.carrier /\ BIJ f2 h.carrier k.carrier ==> BIJ (f2 o f1) G k.carrier 432 True by BIJ_COMPOSE. 433*) 434val monoid_iso_trans = store_thm( 435 "monoid_iso_trans", 436 ``!(g:'a monoid) (h:'b monoid) (k:'c monoid). 437 !f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k``, 438 rw[MonoidIso_def] >- 439 metis_tac[monoid_homo_trans] >> 440 metis_tac[BIJ_COMPOSE]); 441 442(* Theorem: Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g *) 443(* Proof: 444 By MonoidIso_def, this is to show: 445 (1) MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g 446 True by monoid_homo_sym. 447 (2) BIJ f G h.carrier ==> BIJ (LINV f G) h.carrier G 448 True by BIJ_LINV_BIJ 449*) 450val monoid_iso_sym = store_thm( 451 "monoid_iso_sym", 452 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g``, 453 rw[MonoidIso_def, monoid_homo_sym, BIJ_LINV_BIJ]); 454 455(* Theorem: MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k *) 456(* Proof: 457 By MonoidIso_def, this is to show: 458 (1) MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k 459 True by monoid_homo_compose. 460 (2) BIJ f1 G h.carrier /\ BIJ f2 h.carrier k.carrier ==> BIJ (f2 o f1) G k.carrier 461 True by BIJ_COMPOSE 462*) 463val monoid_iso_compose = store_thm( 464 "monoid_iso_compose", 465 ``!(g:'a monoid) (h:'b monoid) (k:'c monoid). 466 !f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k``, 467 rw_tac std_ss[MonoidIso_def] >- 468 metis_tac[monoid_homo_compose] >> 469 metis_tac[BIJ_COMPOSE]); 470(* This is the same as monoid_iso_trans. *) 471 472(* Theorem: Monoid g /\ MonoidIso f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *) 473(* Proof: by MonoidIso_def, monoid_homo_exp *) 474val monoid_iso_exp = store_thm( 475 "monoid_iso_exp", 476 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> 477 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n``, 478 rw[MonoidIso_def, monoid_homo_exp]); 479 480(* Theorem: Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g *) 481(* Proof: 482 By MonoidIso_def, MonoidHomo_def, this is to show: 483 (1) BIJ f G h.carrier /\ x IN h.carrier ==> LINV f G x IN G 484 True by BIJ_LINV_ELEMENT 485 (2) BIJ f G h.carrier /\ x IN h.carrier /\ y IN h.carrier ==> LINV f G (h.op x y) = LINV f G x * LINV f G y 486 Let x' = LINV f G x, y' = LINV f G y. 487 Then x' IN G /\ y' IN G by BIJ_LINV_ELEMENT 488 so x' * y' IN G by monoid_op_element 489 ==> f (x' * y') = h.op (f x') (f y') by MonoidHomo_def 490 = h.op x y by BIJ_LINV_THM 491 Thus LINV f G (h.op x y) 492 = LINV f G (f (x' * y')) by above 493 = x' * y' by BIJ_LINV_THM 494 (3) BIJ f G h.carrier ==> LINV f G h.id = #e 495 Note #e IN G by monoid_id_element 496 and f #e = h.id by MonoidHomo_def 497 ==> LINV f G h.id = #e by BIJ_LINV_THM 498 (4) BIJ f G h.carrier ==> BIJ (LINV f G) h.carrier G 499 True by BIJ_LINV_BIJ 500*) 501val monoid_iso_linv_iso = store_thm( 502 "monoid_iso_linv_iso", 503 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g``, 504 rw_tac std_ss[MonoidIso_def, MonoidHomo_def] >- 505 metis_tac[BIJ_LINV_ELEMENT] >- 506 (qabbrev_tac `x' = LINV f G x` >> 507 qabbrev_tac `y' = LINV f G y` >> 508 metis_tac[BIJ_LINV_THM, BIJ_LINV_ELEMENT, monoid_op_element]) >- 509 metis_tac[BIJ_LINV_THM, monoid_id_element] >> 510 rw_tac std_ss[BIJ_LINV_BIJ]); 511(* This is the same as monoid_iso_sym, just a direct proof. *) 512 513(* Theorem: MonoidIso f g h ==> BIJ f G h.carrier *) 514(* Proof: by MonoidIso_def *) 515val monoid_iso_bij = store_thm( 516 "monoid_iso_bij", 517 ``!(g:'a monoid) (h:'b monoid) f. MonoidIso f g h ==> BIJ f G h.carrier``, 518 rw_tac std_ss[MonoidIso_def]); 519 520(* Theorem: Monoid g /\ Monoid h /\ MonoidIso f g h ==> 521 !x. x IN G ==> ((f x = h.id) <=> (x = #e)) *) 522(* Proof: 523 Note MonoidHomo f g h /\ BIJ f G h.carrier by MonoidIso_def 524 If part: x IN G /\ f x = h.id ==> x = #e 525 By monoid_id_unique, this is to show: 526 (1) !y. y IN G ==> y * x = y 527 Let z = y * x. 528 Then z IN G by monoid_op_element 529 f z = h.op (f y) (f x) by MonoidHomo_def 530 = h.op (f y) h.id by f x = h.id 531 = f y by monoid_homo_element, monoid_id 532 Thus z = y by BIJ_DEF, INJ_DEF 533 (2) !y. y IN G ==> x * y = y 534 Let z = x * y. 535 Then z IN G by monoid_op_element 536 f z = h.op (f x) (f y) by MonoidHomo_def 537 = h.op h.id (f y) by f x = h.id 538 = f y by monoid_homo_element, monoid_id 539 Thus z = y by BIJ_DEF, INJ_DEF 540 541 Only-if part: f #e = h.id, true by monoid_homo_id 542*) 543val monoid_iso_eq_id = store_thm( 544 "monoid_iso_eq_id", 545 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ Monoid h /\ MonoidIso f g h ==> 546 !x. x IN G ==> ((f x = h.id) <=> (x = #e))``, 547 rw[MonoidIso_def] >> 548 rw[EQ_IMP_THM] >| [ 549 rw[GSYM monoid_id_unique] >| [ 550 qabbrev_tac `z = x' * x` >> 551 `z IN G` by rw[Abbr`z`] >> 552 `f z = h.op (f x') (f x)` by fs[MonoidHomo_def, Abbr`z`] >> 553 `_ = f x'` by metis_tac[monoid_homo_element, monoid_id] >> 554 metis_tac[BIJ_DEF, INJ_DEF], 555 qabbrev_tac `z = x * x'` >> 556 `z IN G` by rw[Abbr`z`] >> 557 `f z = h.op (f x) (f x')` by fs[MonoidHomo_def, Abbr`z`] >> 558 `_ = f x'` by metis_tac[monoid_homo_element, monoid_id] >> 559 metis_tac[BIJ_DEF, INJ_DEF] 560 ], 561 rw[monoid_homo_id] 562 ]); 563 564(* Theorem: Monoid g /\ Monoid h /\ MonoidIso f g h ==> !x. x IN G ==> (order h (f x) = ord x)` *) 565(* Proof: 566 Let n = ord x, y = f x. 567 If n = 0, to show: order h y = 0. 568 By contradiction, suppose order h y <> 0. 569 Let m = order h y. 570 Note h.id = h.exp y m by order_property 571 = f (x ** m) by monoid_iso_exp 572 Thus x ** m = #e by monoid_iso_eq_id, monoid_exp_element 573 But x ** m <> #e by order_eq_0, ord x = 0 574 This is a contradiction. 575 576 If n <> 0, to show: order h y = n. 577 Note ord x = n 578 ==> (x ** n = #e) /\ 579 !m. 0 < m /\ m < n ==> x ** m <> #e by order_thm, 0 < n 580 Note h.exp y n = f (x ** n) by monoid_iso_exp 581 = f #e by x ** n = #e 582 = h.id by monoid_iso_id, [1] 583 Claim: !m. 0 < m /\ m < n ==> h.exp y m <> h.id 584 Proof: By contradiction, suppose h.exp y m = h.id. 585 Then f (x ** m) = h.exp y m by monoid_iso_exp 586 = h.id by above 587 or x ** m = #e by monoid_iso_eq_id, monoid_exp_element 588 But !m. 0 < m /\ m < n ==> x ** m <> #e by above 589 This is a contradiction. 590 591 Thus by [1] and claim, order h y = n by order_thm 592*) 593val monoid_iso_order = store_thm( 594 "monoid_iso_order", 595 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ Monoid h /\ MonoidIso f g h ==> 596 !x. x IN G ==> (order h (f x) = ord x)``, 597 rpt strip_tac >> 598 qabbrev_tac `n = ord x` >> 599 qabbrev_tac `y = f x` >> 600 Cases_on `n = 0` >| [ 601 spose_not_then strip_assume_tac >> 602 qabbrev_tac `m = order h y` >> 603 `0 < m` by decide_tac >> 604 `h.exp y m = h.id` by metis_tac[order_property] >> 605 `f (x ** m) = h.id` by metis_tac[monoid_iso_exp] >> 606 `x ** m = #e` by metis_tac[monoid_iso_eq_id, monoid_exp_element] >> 607 metis_tac[order_eq_0], 608 `0 < n` by decide_tac >> 609 `(x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e` by metis_tac[order_thm] >> 610 `h.exp y n = h.id` by metis_tac[monoid_iso_exp, monoid_iso_id] >> 611 `!m. 0 < m /\ m < n ==> h.exp y m <> h.id` by 612 (spose_not_then strip_assume_tac >> 613 `f (x ** m) = h.id` by metis_tac[monoid_iso_exp] >> 614 `x ** m = #e` by metis_tac[monoid_iso_eq_id, monoid_exp_element] >> 615 metis_tac[]) >> 616 metis_tac[order_thm] 617 ]); 618 619(* Theorem: MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier) *) 620(* Proof: by MonoidIso_def, FINITE_BIJ_CARD. *) 621val monoid_iso_card_eq = store_thm( 622 "monoid_iso_card_eq", 623 ``!g:'a monoid h:'b monoid f. MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier)``, 624 metis_tac[MonoidIso_def, FINITE_BIJ_CARD]); 625 626(* ------------------------------------------------------------------------- *) 627(* Monoid Automorphisms *) 628(* ------------------------------------------------------------------------- *) 629 630(* Theorem: MonoidAuto f g ==> (f #e = #e) *) 631(* Proof: by MonoidAuto_def, monoid_iso_id. *) 632val monoid_auto_id = store_thm( 633 "monoid_auto_id", 634 ``!f g. MonoidAuto f g ==> (f #e = #e)``, 635 rw_tac std_ss[MonoidAuto_def, monoid_iso_id]); 636 637(* Theorem: MonoidAuto f g ==> !x. x IN G ==> f x IN G *) 638(* Proof: by MonoidAuto_def, monoid_iso_element *) 639val monoid_auto_element = store_thm( 640 "monoid_auto_element", 641 ``!f g. MonoidAuto f g ==> !x. x IN G ==> f x IN G``, 642 metis_tac[MonoidAuto_def, monoid_iso_element]); 643 644(* Theorem: MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g *) 645(* Proof: by MonoidAuto_def, monoid_iso_compose *) 646val monoid_auto_compose = store_thm( 647 "monoid_auto_compose", 648 ``!(g:'a monoid). !f1 f2. MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g``, 649 metis_tac[MonoidAuto_def, monoid_iso_compose]); 650 651(* Theorem: Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> !n. f (x ** n) = (f x) ** n *) 652(* Proof: by MonoidAuto_def, monoid_iso_exp *) 653val monoid_auto_exp = store_thm( 654 "monoid_auto_exp", 655 ``!f g. Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> !n. f (x ** n) = (f x) ** n``, 656 rw[MonoidAuto_def, monoid_iso_exp]); 657 658(* Theorem: MonoidAuto I g *) 659(* Proof: 660 MonoidAuto I g 661 <=> MonoidIso I g g by MonoidAuto_def 662 <=> MonoidHomo I g g /\ BIJ f G G by MonoidIso_def 663 <=> T /\ BIJ f G G by MonoidHomo_def, I_THM 664 <=> T /\ T by BIJ_I_SAME 665*) 666val monoid_auto_I = store_thm( 667 "monoid_auto_I", 668 ``!(g:'a monoid). MonoidAuto I g``, 669 rw_tac std_ss[MonoidAuto_def, MonoidIso_def, MonoidHomo_def, BIJ_I_SAME]); 670 671(* Theorem: Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g *) 672(* Proof: 673 MonoidAuto I g 674 ==> MonoidIso I g g by MonoidAuto_def 675 ==> MonoidIso (LINV f G) g by monoid_iso_linv_iso 676 ==> MonoidAuto (LINV f G) g by MonoidAuto_def 677*) 678val monoid_auto_linv_auto = store_thm( 679 "monoid_auto_linv_auto", 680 ``!(g:'a monoid) f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g``, 681 rw_tac std_ss[MonoidAuto_def, monoid_iso_linv_iso]); 682 683(* Theorem: MonoidAuto f g ==> f PERMUTES G *) 684(* Proof: by MonoidAuto_def, MonoidIso_def *) 685val monoid_auto_bij = store_thm( 686 "monoid_auto_bij", 687 ``!g:'a monoid. !f. MonoidAuto f g ==> f PERMUTES G``, 688 rw_tac std_ss[MonoidAuto_def, MonoidIso_def]); 689 690(* Theorem: Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> (ord (f x) = ord x) *) 691(* Proof: by MonoidAuto_def, monoid_iso_order. *) 692val monoid_auto_order = store_thm( 693 "monoid_auto_order", 694 ``!(g:'a monoid) f. Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> (ord (f x) = ord x)``, 695 rw[MonoidAuto_def, monoid_iso_order]); 696 697(* ------------------------------------------------------------------------- *) 698(* Submonoids. *) 699(* ------------------------------------------------------------------------- *) 700 701(* Use H to denote h.carrier *) 702val _ = overload_on ("H", ``(h:'a monoid).carrier``); 703 704(* Theorem: submonoid h g ==> H SUBSET G /\ (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e) *) 705(* Proof: 706 submonoid h g 707 <=> MonoidHomo I h g by submonoid_def 708 <=> (!x. x IN H ==> I x IN G) /\ 709 (!x y. x IN H /\ y IN H ==> (I (h.op x y) = (I x) * (I y))) /\ 710 (h.id = I #e) by MonoidHomo_def 711 <=> (!x. x IN H ==> x IN G) /\ 712 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ 713 (h.id = #e) by I_THM 714 <=> H SUBSET G 715 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ 716 (h.id = #e) by SUBSET_DEF 717*) 718val submonoid_eqn = store_thm( 719 "submonoid_eqn", 720 ``!(g:'a monoid) (h:'a monoid). submonoid h g <=> 721 H SUBSET G /\ (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e)``, 722 rw_tac std_ss[submonoid_def, MonoidHomo_def, SUBSET_DEF]); 723 724(* Theorem: submonoid h g ==> H SUBSET G *) 725(* Proof: by submonoid_eqn *) 726val submonoid_subset = store_thm( 727 "submonoid_subset", 728 ``!(g:'a monoid) (h:'a monoid). submonoid h g ==> H SUBSET G``, 729 rw_tac std_ss[submonoid_eqn]); 730 731(* Theorem: submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k *) 732(* Proof: 733 Note H SUBSET G by submonoid_subset 734 or !x. x IN H ==> x IN G by SUBSET_DEF 735 By MonoidHomo_def, this is to show: 736 (1) x IN H ==> f x IN k.carrier 737 True by MonoidHomo_def, MonoidHomo f g k 738 (2) x IN H /\ y IN H /\ f (h.op x y) = k.op (f x) (f y) 739 Note x IN H ==> x IN G by above 740 and y IN H ==> y IN G by above 741 f (h.op x y) 742 = f (x * y) by submonoid_eqn 743 = k.op (f x) (f y) by MonoidHomo_def 744 (3) f h.id = k.id 745 f (h.id) 746 = f #e by submonoid_eqn 747 = k.id by MonoidHomo_def 748*) 749val submonoid_homo_homo = store_thm( 750 "submonoid_homo_homo", 751 ``!(g:'a monoid) (h:'a monoid) (k:'b monoid) f. submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k``, 752 rw_tac std_ss[submonoid_def, MonoidHomo_def]); 753 754(* Theorem: submonoid g g *) 755(* Proof: 756 By submonoid_def, this is to show: 757 MonoidHomo I g g, true by monoid_homo_I_refl. 758*) 759val submonoid_refl = store_thm( 760 "submonoid_refl", 761 ``!g:'a monoid. submonoid g g``, 762 rw[submonoid_def, monoid_homo_I_refl]); 763 764(* Theorem: submonoid g h /\ submonoid h k ==> submonoid g k *) 765(* Proof: 766 By submonoid_def, this is to show: 767 MonoidHomo I g h /\ MonoidHomo I h k ==> MonoidHomo I g k 768 Since I o I = I by combinTheory.I_o_ID 769 This is true by monoid_homo_trans 770*) 771val submonoid_trans = store_thm( 772 "submonoid_trans", 773 ``!(g h k):'a monoid. submonoid g h /\ submonoid h k ==> submonoid g k``, 774 prove_tac[submonoid_def, combinTheory.I_o_ID, monoid_homo_trans]); 775 776(* Theorem: submonoid h g /\ submonoid g h ==> MonoidIso I h g *) 777(* Proof: 778 By submonoid_def, MonoidIso_def, this is to show: 779 MonoidHomo I h g /\ MonoidHomo I g h ==> BIJ I H G 780 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 781 (1) x IN H ==> x IN G, true by submonoid_subset, submonoid h g 782 (2) x IN G ==> x IN H, true by submonoid_subset, submonoid g h 783*) 784val submonoid_I_antisym = store_thm( 785 "submonoid_I_antisym", 786 ``!(g:'a monoid) h. submonoid h g /\ submonoid g h ==> MonoidIso I h g``, 787 rw_tac std_ss[submonoid_def, MonoidIso_def] >> 788 fs[MonoidHomo_def] >> 789 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF]); 790 791(* Theorem: submonoid h g /\ G SUBSET H ==> MonoidIso I h g *) 792(* Proof: 793 By submonoid_def, MonoidIso_def, this is to show: 794 MonoidHomo I h g /\ G SUBSET H ==> BIJ I H G 795 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 796 (1) x IN H ==> x IN G, true by submonoid_subset, submonoid h g 797 (2) x IN G ==> x IN H, true by G SUBSET H, given 798*) 799val submonoid_carrier_antisym = store_thm( 800 "submonoid_carrier_antisym", 801 ``!(g:'a monoid) h. submonoid h g /\ G SUBSET H ==> MonoidIso I h g``, 802 rpt (stripDup[submonoid_def]) >> 803 rw_tac std_ss[MonoidIso_def] >> 804 `H SUBSET G` by rw[submonoid_subset] >> 805 fs[MonoidHomo_def, SUBSET_DEF] >> 806 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF]); 807 808(* Theorem: Monoid g /\ Monoid h /\ submonoid h g ==> !x. x IN H ==> (order h x = ord x) *) 809(* Proof: 810 Note MonoidHomo I h g by submonoid_def 811 If ord x = 0, to show: order h x = 0. 812 By contradiction, suppose order h x <> 0. 813 Let n = order h x. 814 Then 0 < n by n <> 0 815 and h.exp x n = h.id by order_property 816 or x ** n = #e by monoid_homo_exp, monoid_homo_id, I_THM 817 But x ** n <> #e by order_eq_0, ord x = 0 818 This is a contradiction. 819 If ord x <> 0, to show: order h x = ord x. 820 Note 0 < ord x by ord x <> 0 821 By order_thm, this is to show: 822 (1) h.exp x (ord x) = h.id 823 h.exp x (ord x) 824 = I (h.exp x (ord x)) by I_THM 825 = (I x) ** ord x by monoid_homo_exp 826 = x ** ord x by I_THM 827 = #e by order_property 828 = I (h.id) by monoid_homo_id 829 = h.id by I_THM 830 (2) 0 < m /\ m < ord x ==> h.exp x m <> h.id 831 By contradiction, suppose h.exp x m = h.id 832 h.exp x m 833 = I (h.exp x m) by I_THM 834 = (I x) ** m by monoid_homo_exp 835 = x ** m by I_THM 836 h.id = I (h.id) by I_THM 837 = #e by monoid_homo_id 838 Thus x ** m = #e by h.exp x m = h.id 839 But x ** m <> #e by order_thm 840 This is a contradiction. 841*) 842val submonoid_order_eqn = store_thm( 843 "submonoid_order_eqn", 844 ``!(g:'a monoid) h. Monoid g /\ Monoid h /\ submonoid h g ==> 845 !x. x IN H ==> (order h x = ord x)``, 846 rw[submonoid_def] >> 847 `!x. I x = x` by rw[] >> 848 Cases_on `ord x = 0` >| [ 849 spose_not_then strip_assume_tac >> 850 qabbrev_tac `n = order h x` >> 851 `0 < n` by decide_tac >> 852 `h.exp x n = h.id` by rw[order_property, Abbr`n`] >> 853 `x ** n = #e` by metis_tac[monoid_homo_exp, monoid_homo_id] >> 854 metis_tac[order_eq_0], 855 `0 < ord x` by decide_tac >> 856 rw[order_thm] >- 857 metis_tac[monoid_homo_exp, order_property, monoid_homo_id] >> 858 spose_not_then strip_assume_tac >> 859 `x ** m = #e` by metis_tac[monoid_homo_exp, monoid_homo_id] >> 860 metis_tac[order_thm] 861 ]); 862 863(* ------------------------------------------------------------------------- *) 864(* Homomorphic Image of Monoid. *) 865(* ------------------------------------------------------------------------- *) 866 867(* Define an operation on images *) 868val image_op_def = Define` 869 image_op (g:'a monoid) (f:'a -> 'b) x y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)) 870`; 871 872(* Theorem: INJ f G univ(:'b) ==> !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (x * y)) *) 873(* Proof: 874 Note x = CHOICE (preimage f G (f x)) by preimage_inj_choice 875 and y = CHOICE (preimage f G (f y)) by preimage_inj_choice 876 image_op g f (f x) (f y) 877 = f (CHOICE (preimage f G (f x)) * CHOICE (preimage f G (f y)) by image_op_def 878 = f (x * y) by above 879*) 880val image_op_inj = store_thm( 881 "image_op_inj", 882 ``!g:'a monoid f. INJ f G univ(:'b) ==> 883 !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (g.op x y))``, 884 rw[image_op_def, preimage_inj_choice]); 885 886(* Define the homomorphic image of a monoid. *) 887val homo_monoid_def = Define` 888 homo_monoid (g:'a monoid) (f:'a -> 'b) = 889 <| carrier := IMAGE f G; 890 op := image_op g f; 891 id := f #e 892 |> 893`; 894 895(* set overloading *) 896val _ = overload_on ("o", ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).op``); 897val _ = overload_on ("#i", ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).id``); 898val _ = overload_on ("fG", ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).carrier``); 899 900(* Theorem: Properties of homo_monoid. *) 901(* Proof: by homo_monoid_def and image_op_def. *) 902val homo_monoid_property = store_thm( 903 "homo_monoid_property", 904 ``!(g:'a monoid) (f:'a -> 'b). (fG = IMAGE f G) /\ 905 (!x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))) /\ 906 (#i = f #e)``, 907 rw[homo_monoid_def, image_op_def]); 908 909(* Theorem: !x. x IN G ==> f x IN fG *) 910(* Proof: by homo_monoid_def, IN_IMAGE *) 911val homo_monoid_element = store_thm( 912 "homo_monoid_element", 913 ``!(g:'a monoid) (f:'a -> 'b). !x. x IN G ==> f x IN fG``, 914 rw[homo_monoid_def]); 915 916(* Theorem: f #e = #i *) 917(* Proof: by homo_monoid_def *) 918val homo_monoid_id = store_thm( 919 "homo_monoid_id", 920 ``!(g:'a monoid) (f:'a -> 'b). f #e = #i``, 921 rw[homo_monoid_def]); 922 923(* Theorem: INJ f G univ(:'b) ==> 924 !x y. x IN G /\ y IN G ==> (f (x * y) = (f x) o (f y)) *) 925(* Proof: 926 Note x = CHOICE (preimage f G (f x)) by preimage_inj_choice 927 and y = CHOICE (preimage f G (f y)) by preimage_inj_choice 928 f (x * y) 929 = f (CHOICE (preimage f G (f x)) * CHOICE (preimage f G (f y)) by above 930 = (f x) o (f y) by homo_monoid_property 931*) 932val homo_monoid_op_inj = store_thm( 933 "homo_monoid_op_inj", 934 ``!(g:'a monoid) (f:'a -> 'b). INJ f G univ(:'b) ==> 935 !x y. x IN G /\ y IN G ==> (f (x * y) = (f x) o (f y))``, 936 rw[homo_monoid_property, preimage_inj_choice]); 937 938(* Theorem: MonoidIso I (homo_monoid g I) g *) 939(* Proof: 940 Note IMAGE I G = G by IMAGE_I 941 and INJ I G univ(:'a) by INJ_I 942 and !x. I x = x by I_THM 943 By MonoidIso_def, this is to show: 944 (1) MonoidHomo I (homo_monoid g I) g 945 By MonoidHomo_def, homo_monoid_def, this is to show: 946 x IN G /\ y IN G ==> image_op g I x y = x * y 947 This is true by image_op_inj 948 (2) BIJ I (homo_group g I).carrier G 949 (homo_group g I).carrier 950 = IMAGE I G by homo_monoid_property 951 = G by above, IMAGE_I 952 This is true by BIJ_I_SAME 953*) 954val homo_monoid_I = store_thm( 955 "homo_monoid_I", 956 ``!g:'a monoid. MonoidIso I (homo_monoid g I) g``, 957 rpt strip_tac >> 958 `IMAGE I G = G` by rw[] >> 959 `INJ I G univ(:'a)` by rw[INJ_I] >> 960 `!x. I x = x` by rw[] >> 961 rw_tac std_ss[MonoidIso_def] >| [ 962 rw_tac std_ss[MonoidHomo_def, homo_monoid_def] >> 963 metis_tac[image_op_inj], 964 rw[homo_monoid_property, BIJ_I_SAME] 965 ]); 966 967(* Theorem: [Closure] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> x IN fG /\ y IN fG ==> x o y IN fG *) 968(* Proof: 969 Let a = CHOICE (preimage f G x), 970 b = CHOICE (preimage f G y). 971 Then a IN G /\ x = f a by preimage_choice_property 972 b IN G /\ y = f b by preimage_choice_property 973 x o y 974 = (f a) o (f b) 975 = f (a * b) by homo_monoid_property 976 Note a * b IN G by monoid_op_element 977 so f (a * b) IN fG by homo_monoid_element 978*) 979val homo_monoid_closure = store_thm( 980 "homo_monoid_closure", 981 ``!(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 982 !x y. x IN fG /\ y IN fG ==> x o y IN fG``, 983 rw_tac std_ss[homo_monoid_property] >> 984 rw[preimage_choice_property]); 985 986(* Theorem: [Associative] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 987 x IN fG /\ y IN fG /\ z IN fG ==> (x o y) o z = x o (y o z) *) 988(* Proof: 989 By MonoidHomo_def, 990 !x. x IN G ==> f x IN fG 991 !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y) 992 Let a = CHOICE (preimage f G x), 993 b = CHOICE (preimage f G y), 994 c = CHOICE (preimage f G z). 995 Then a IN G /\ x = f a by preimage_choice_property 996 b IN G /\ y = f b by preimage_choice_property 997 c IN G /\ z = f c by preimage_choice_property 998 (x o y) o z 999 = ((f a) o (f b)) o (f c) by expanding x, y, z 1000 = f (a * b) o (f c) by homo_monoid_property 1001 = f (a * b * c) by homo_monoid_property 1002 = f (a * (b * c)) by monoid_assoc 1003 = (f a) o f (b * c) by homo_monoid_property 1004 = (f a) o ((f b) o (f c)) by homo_monoid_property 1005 = x o (y o z) by contracting x, y, z 1006*) 1007val homo_monoid_assoc = store_thm( 1008 "homo_monoid_assoc", 1009 ``!(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 1010 !x y z. x IN fG /\ y IN fG /\ z IN fG ==> ((x o y) o z = x o (y o z))``, 1011 rw_tac std_ss[MonoidHomo_def] >> 1012 `(fG = IMAGE f G) /\ !x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))` by rw[homo_monoid_property] >> 1013 qabbrev_tac `a = CHOICE (preimage f G x)` >> 1014 qabbrev_tac `b = CHOICE (preimage f G y)` >> 1015 qabbrev_tac `c = CHOICE (preimage f G z)` >> 1016 `a IN G /\ (f a = x)` by metis_tac[preimage_choice_property] >> 1017 `b IN G /\ (f b = y)` by metis_tac[preimage_choice_property] >> 1018 `c IN G /\ (f c = z)` by metis_tac[preimage_choice_property] >> 1019 `a * b IN G /\ b * c IN G ` by rw[] >> 1020 `a * b * c = a * (b * c)` by rw[monoid_assoc] >> 1021 metis_tac[]); 1022 1023(* Theorem: [Identity] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> #i IN fG /\ #i o x = x /\ x o #i = x. *) 1024(* Proof: 1025 By homo_monoid_property, #i = f #e, and #i IN fG. 1026 Since CHOICE (preimage f G x) IN G /\ x = f (CHOICE (preimage f G x)) by preimage_choice_property 1027 hence #i o x 1028 = (f #e) o f (preimage f G x) 1029 = f (#e * preimage f G x) by homo_monoid_property 1030 = f (preimage f G x) by monoid_lid 1031 = x 1032 similarly for x o #i = x by monoid_rid 1033*) 1034val homo_monoid_id_property = store_thm( 1035 "homo_monoid_id_property", 1036 ``!(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> 1037 #i IN fG /\ (!x. x IN fG ==> (#i o x = x) /\ (x o #i = x))``, 1038 rw[MonoidHomo_def, homo_monoid_property] >- 1039 metis_tac[monoid_lid, monoid_id_element, preimage_choice_property] >> 1040 metis_tac[monoid_rid, monoid_id_element, preimage_choice_property]); 1041 1042(* Theorem: [Commutative] AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> 1043 x IN fG /\ y IN fG ==> (x o y = y o x) *) 1044(* Proof: 1045 Note AbelianMonoid g ==> Monoid g and 1046 !x y. x IN G /\ y IN G ==> (x * y = y * x) by AbelianMonoid_def 1047 By MonoidHomo_def, 1048 !x. x IN G ==> f x IN fG 1049 !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y) 1050 Let a = CHOICE (preimage f G x), 1051 b = CHOICE (preimage f G y). 1052 Then a IN G /\ x = f a by preimage_choice_property 1053 b IN G /\ y = f b by preimage_choice_property 1054 x o y 1055 = (f a) o (f b) by expanding x, y 1056 = f (a * b) by homo_monoid_property 1057 = f (b * a) by AbelianMonoid_def, above 1058 = (f b) o (f a) by homo_monoid_property 1059 = y o x by contracting x, y 1060*) 1061val homo_monoid_comm = store_thm( 1062 "homo_monoid_comm", 1063 ``!(g:'a monoid) (f:'a -> 'b). AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> 1064 !x y. x IN fG /\ y IN fG ==> (x o y = y o x)``, 1065 rw_tac std_ss[AbelianMonoid_def, MonoidHomo_def] >> 1066 `(fG = IMAGE f G) /\ !x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))` by rw[homo_monoid_property] >> 1067 qabbrev_tac `a = CHOICE (preimage f G x)` >> 1068 qabbrev_tac `b = CHOICE (preimage f G y)` >> 1069 `a IN G /\ (f a = x)` by metis_tac[preimage_choice_property] >> 1070 `b IN G /\ (f b = y)` by metis_tac[preimage_choice_property] >> 1071 `a * b = b * a` by rw[] >> 1072 metis_tac[]); 1073 1074(* Theorem: Homomorphic image of a monoid is a monoid. 1075 Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f) *) 1076(* Proof: 1077 This is to show each of these: 1078 (1) x IN fG /\ y IN fG ==> x o y IN fG true by homo_monoid_closure 1079 (2) x IN fG /\ y IN fG /\ z IN fG ==> (x o y) o z = (x o y) o z true by homo_monoid_assoc 1080 (3) #i IN fG, true by homo_monoid_id_property 1081 (4) x IN fG ==> #i o x = x, true by homo_monoid_id_property 1082 (5) x IN fG ==> x o #i = x, true by homo_monoid_id_property 1083*) 1084val homo_monoid_monoid = store_thm( 1085 "homo_monoid_monoid", 1086 ``!(g:'a monoid) f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f)``, 1087 rpt strip_tac >> 1088 rw_tac std_ss[Monoid_def] >| [ 1089 rw[homo_monoid_closure], 1090 rw[homo_monoid_assoc], 1091 rw[homo_monoid_id_property], 1092 rw[homo_monoid_id_property], 1093 rw[homo_monoid_id_property] 1094 ]); 1095 1096(* Theorem: Homomorphic image of an Abelian monoid is an Abelian monoid. 1097 AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> AbelianMonoid (homo_monoid g f) *) 1098(* Proof: 1099 Note AbelianMonoid g ==> Monoid g by AbelianMonoid_def 1100 By AbelianMonoid_def, this is to show: 1101 (1) Monoid (homo_monoid g f), true by homo_monoid_monoid, Monoid g 1102 (2) x IN fG /\ y IN fG ==> x o y = y o x, true by homo_monoid_comm, AbelianMonoid g 1103*) 1104val homo_monoid_abelian_monoid = store_thm( 1105 "homo_monoid_abelian_monoid", 1106 ``!(g:'a monoid) f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> AbelianMonoid (homo_monoid g f)``, 1107 metis_tac[homo_monoid_monoid, AbelianMonoid_def, homo_monoid_comm]); 1108 1109(* Theorem: Monoid g /\ INJ f G UNIV ==> MonoidHomo f g (homo_monoid g f) *) 1110(* Proof: 1111 By MonoidHomo_def, homo_monoid_property, this is to show: 1112 (1) x IN G ==> f x IN IMAGE f G, true by IN_IMAGE 1113 (2) x IN G /\ y IN G ==> f (x * y) = f x o f y, true by homo_monoid_op_inj 1114*) 1115val homo_monoid_by_inj = store_thm( 1116 "homo_monoid_by_inj", 1117 ``!(g:'a monoid) (f:'a -> 'b). Monoid g /\ INJ f G UNIV ==> MonoidHomo f g (homo_monoid g f)``, 1118 rw_tac std_ss[MonoidHomo_def, homo_monoid_property] >- 1119 rw[] >> 1120 rw[homo_monoid_op_inj]); 1121 1122(* ------------------------------------------------------------------------- *) 1123(* Weaker form of Homomorphic of Monoid and image of identity. *) 1124(* ------------------------------------------------------------------------- *) 1125 1126(* Let us take out the image of identity requirement *) 1127val WeakHomo_def = Define` 1128 WeakHomo (f:'a -> 'b) (g:'a monoid) (h:'b monoid) <=> 1129 (!x. x IN G ==> f x IN h.carrier) /\ 1130 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))) 1131 (* no requirement for: f #e = h.id *) 1132`; 1133 1134(* A function f from g to h is an isomorphism if f is a bijective homomorphism. *) 1135val WeakIso_def = Define` 1136 WeakIso f g h <=> WeakHomo f g h /\ BIJ f G h.carrier 1137`; 1138 1139(* Then the best we can prove about monoid identities is the following: 1140 Monoid g /\ Monoid h /\ WeakIso f g h ==> f #e = h.id 1141 which is NOT: 1142 Monoid g /\ Monoid h /\ WeakHomo f g h ==> f #e = h.id 1143*) 1144 1145(* Theorem: Monoid g /\ Monoid h /\ WeakIso f g h ==> f #e = h.id *) 1146(* Proof: 1147 By monoid_id_unique: 1148 |- !g. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (x * e = x) /\ (e * x = x)) <=> (e = #e)) : thm 1149 Hence this is to show: !x. x IN h.carrier ==> (h.op x (f #e) = x) /\ (h.op (f #e) x = x) 1150 Note that WeakIso f g h = WeakHomo f g h /\ BIJ f G h.carrier. 1151 (1) x IN h.carrier /\ f #e IN h.carrier ==> h.op x (f #e) = x 1152 Since x = f y for some y IN G, by BIJ_ALT 1153 h.op x (f #e) = h.op (f y) (f #e) 1154 = f (y * #e) by WeakHomo_def 1155 = f y = x by monoid_rid 1156 (2) x IN h.carrier /\ f #e IN h.carrier ==> h.op (f #e) x = x 1157 Similar to above, 1158 h.op (f #e) x = h.op (f #e) (f y) = f (#e * y) = f y = x by monoid_lid. 1159*) 1160val monoid_weak_iso_id = store_thm( 1161 "monoid_weak_iso_id", 1162 ``!f g h. Monoid g /\ Monoid h /\ WeakIso f g h ==> (f #e = h.id)``, 1163 rw_tac std_ss[WeakIso_def] >> 1164 `#e IN G /\ f #e IN h.carrier` by metis_tac[WeakHomo_def, monoid_id_element] >> 1165 `!x. x IN h.carrier ==> (h.op x (f #e) = x) /\ (h.op (f #e) x = x)` suffices_by rw_tac std_ss[monoid_id_unique] >> 1166 rpt strip_tac>| [ 1167 `?y. y IN G /\ (f y = x)` by metis_tac[BIJ_ALT] >> 1168 metis_tac[WeakHomo_def, monoid_rid], 1169 `?y. y IN G /\ (f y = x)` by metis_tac[BIJ_ALT] >> 1170 metis_tac[WeakHomo_def, monoid_lid] 1171 ]); 1172 1173(* ------------------------------------------------------------------------- *) 1174 1175(* export theory at end *) 1176val _ = export_theory(); 1177 1178(*===========================================================================*) 1179