1(* ------------------------------------------------------------------------- *) 2(* Submonoid *) 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 "submonoid"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories local *) 23(* val _ = load "monoidMapTheory"; *) 24open monoidTheory monoidMapTheory; 25 26open pred_setTheory; 27open helperSetTheory; 28 29 30(* ------------------------------------------------------------------------- *) 31(* Submonoid Documentation *) 32(* ------------------------------------------------------------------------- *) 33(* Overloading (# are temporary): 34# K = k.carrier 35# x o y = h.op x y 36# #i = h.id 37 h << g = Submonoid h g 38 h mINTER k = monoid_intersect h k 39 smbINTER g = submonoid_big_intersect g 40*) 41(* Definitions and Theorems (# are exported): 42 43 Helper Theorems: 44 45 Submonoid of a Monoid: 46 Submonoid_def |- !h g. h << g <=> 47 Monoid h /\ Monoid g /\ H SUBSET G /\ ($o = $* ) /\ (#i = #e) 48 submonoid_property |- !g h. h << g ==> 49 Monoid h /\ Monoid g /\ H SUBSET G /\ 50 (!x y. x IN H /\ y IN H ==> (x o y = x * y)) /\ (#i = #e) 51 submonoid_carrier_subset |- !g h. h << g ==> H SUBSET G 52# submonoid_element |- !g h. h << g ==> !x. x IN H ==> x IN G 53# submonoid_id |- !g h. h << g ==> (#i = #e) 54 submonoid_exp |- !g h. h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n 55 submonoid_homomorphism |- !g h. h << g ==> Monoid h /\ Monoid g /\ submonoid h g 56 submonoid_order |- !g h. h << g ==> !x. x IN H ==> (order h x = ord x) 57 submonoid_alt |- !g. Monoid g ==> !h. h << g <=> H SUBSET G /\ 58 (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\ 59 h.id IN H /\ (h.op = $* ) /\ (h.id = #e) 60 61 Submonoid Theorems: 62 submonoid_reflexive |- !g. Monoid g ==> g << g 63 submonoid_antisymmetric |- !g h. h << g /\ g << h ==> (h = g) 64 submonoid_transitive |- !g h k. k << h /\ h << g ==> k << g 65 submonoid_monoid |- !g h. h << g ==> Monoid h 66 67 Submonoid Intersection: 68 monoid_intersect_def |- !g h. g mINTER h = <|carrier := G INTER H; op := $*; id := #e|> 69 monoid_intersect_property |- !g h. ((g mINTER h).carrier = G INTER H) /\ 70 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e) 71 monoid_intersect_element |- !g h x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H 72 monoid_intersect_id |- !g h. (g mINTER h).id = #e 73 74 submonoid_intersect_property |- !g h k. h << g /\ k << g ==> 75 ((h mINTER k).carrier = H INTER K) /\ 76 (!x y. x IN H INTER K /\ y IN H INTER K ==> 77 ((h mINTER k).op x y = x * y)) /\ ((h mINTER k).id = #e) 78 submonoid_intersect_monoid |- !g h k. h << g /\ k << g ==> Monoid (h mINTER k) 79 submonoid_intersect_submonoid |- !g h k. h << g /\ k << g ==> (h mINTER k) << g 80 81 Submonoid Big Intersection: 82 submonoid_big_intersect_def |- !g. smbINTER g = 83 <|carrier := BIGINTER (IMAGE (\h. H) {h | h << g}); op := $*; id := #e|> 84 submonoid_big_intersect_property |- !g. 85 ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\ 86 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\ 87 ((smbINTER g).id = #e) 88 submonoid_big_intersect_element |- !g x. x IN (smbINTER g).carrier <=> !h. h << g ==> x IN H 89 submonoid_big_intersect_op_element |- !g x y. x IN (smbINTER g).carrier /\ 90 y IN (smbINTER g).carrier ==> 91 (smbINTER g).op x y IN (smbINTER g).carrier 92 submonoid_big_intersect_has_id |- !g. (smbINTER g).id IN (smbINTER g).carrier 93 submonoid_big_intersect_subset |- !g. Monoid g ==> (smbINTER g).carrier SUBSET G 94 submonoid_big_intersect_monoid |- !g. Monoid g ==> Monoid (smbINTER g) 95 submonoid_big_intersect_submonoid |- !g. Monoid g ==> smbINTER g << g 96*) 97 98(* ------------------------------------------------------------------------- *) 99(* Helper Theorems *) 100(* ------------------------------------------------------------------------- *) 101 102(* ------------------------------------------------------------------------- *) 103(* Submonoid of a Monoid *) 104(* ------------------------------------------------------------------------- *) 105 106(* Use K to denote k.carrier *) 107val _ = temp_overload_on ("K", ``(k:'a monoid).carrier``); 108 109(* Use o to denote h.op *) 110val _ = temp_overload_on ("o", ``(h:'a monoid).op``); 111 112(* Use #i to denote h.id *) 113val _ = temp_overload_on ("#i", ``(h:'a monoid).id``); 114 115(* A Submonoid is a subset of a monoid that's a monoid itself, keeping op, id. *) 116val Submonoid_def = Define` 117 Submonoid (h:'a monoid) (g:'a monoid) <=> 118 Monoid h /\ Monoid g /\ 119 H SUBSET G /\ ($o = $* ) /\ (#i = #e) 120`; 121 122(* Overload Submonoid *) 123val _ = overload_on ("<<", ``Submonoid``); 124val _ = set_fixity "<<" (Infix(NONASSOC, 450)); (* same as relation *) 125 126(* Note: The requirement $o = $* is stronger than the following: 127val _ = overload_on ("<<", ``\(h g):'a monoid. Monoid g /\ Monoid h /\ submonoid h g``); 128Since submonoid h g is based on MonoidHomo I g h, which only gives 129!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) 130 131This is not enough to satisfy monoid_component_equality, 132hence cannot prove: h << g /\ g << h ==> h = g 133*) 134 135(* 136val submonoid_property = save_thm( 137 "submonoid_property", 138 Submonoid_def 139 |> SPEC_ALL 140 |> REWRITE_RULE [ASSUME ``h:'a monoid << g``] 141 |> CONJUNCTS 142 |> (fn thl => List.take(thl, 2) @ List.drop(thl, 3)) 143 |> LIST_CONJ 144 |> DISCH_ALL 145 |> Q.GEN `h` |> Q.GEN `g`); 146val submonoid_property = |- !g h. h << g ==> Monoid h /\ Monoid g /\ ($o = $* ) /\ (#i = #e) 147*) 148 149(* Theorem: properties of submonoid *) 150(* Proof: Assume h << g, then derive all consequences of definition. *) 151val submonoid_property = store_thm( 152 "submonoid_property", 153 ``!(g:'a monoid) h. h << g ==> Monoid h /\ Monoid g /\ H SUBSET G /\ 154 (!x y. x IN H /\ y IN H ==> (x o y = x * y)) /\ (#i = #e)``, 155 rw_tac std_ss[Submonoid_def]); 156 157(* Theorem: h << g ==> H SUBSET G *) 158(* Proof: by Submonoid_def *) 159val submonoid_carrier_subset = store_thm( 160 "submonoid_carrier_subset", 161 ``!(g:'a monoid) h. Submonoid h g ==> H SUBSET G``, 162 rw[Submonoid_def]); 163 164(* Theorem: elements in submonoid are also in monoid. *) 165(* Proof: Since h << g ==> H SUBSET G by Submonoid_def. *) 166val submonoid_element = store_thm( 167 "submonoid_element", 168 ``!(g:'a monoid) h. h << g ==> !x. x IN H ==> x IN G``, 169 rw_tac std_ss[Submonoid_def, SUBSET_DEF]); 170 171(* export simple result *) 172val _ = export_rewrites ["submonoid_element"]; 173 174(* Theorem: h << g ==> (h.op = $* ) *) 175(* Proof: by Subgroup_def *) 176val submonoid_op = store_thm( 177 "submonoid_op", 178 ``!(g:'a monoid) h. h << g ==> (h.op = g.op)``, 179 rw[Submonoid_def]); 180 181(* Theorem: h << g ==> #i = #e *) 182(* Proof: by Submonoid_def. *) 183val submonoid_id = store_thm( 184 "submonoid_id", 185 ``!(g:'a monoid) h. h << g ==> (#i = #e)``, 186 rw_tac std_ss[Submonoid_def]); 187 188(* export simple results *) 189val _ = export_rewrites["submonoid_id"]; 190 191(* Theorem: h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n *) 192(* Proof: by induction on n. 193 Base: h.exp x 0 = x ** 0 194 LHS = h.exp x 0 195 = h.id by monoid_exp_0 196 = #e by submonoid_id 197 = x ** 0 by monoid_exp_0 198 = RHS 199 Step: h.exp x n = x ** n ==> h.exp x (SUC n) = x ** SUC n 200 LHS = h.exp x (SUC n) 201 = h.op x (h.exp x n) by monoid_exp_SUC 202 = x * (h.exp x n) by submonoid_property 203 = x * x ** n by induction hypothesis 204 = x ** SUC n by monoid_exp_SUC 205 = RHS 206*) 207val submonoid_exp = store_thm( 208 "submonoid_exp", 209 ``!(g:'a monoid) h. h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n``, 210 rpt strip_tac >> 211 Induct_on `n` >- 212 rw[] >> 213 `h.exp x (SUC n) = h.op x (h.exp x n)` by rw_tac std_ss[monoid_exp_SUC] >> 214 `_ = x * (h.exp x n)` by metis_tac[submonoid_property, monoid_exp_element] >> 215 `_ = x * (x ** n)` by rw[] >> 216 `_ = x ** (SUC n)` by rw_tac std_ss[monoid_exp_SUC] >> 217 rw[]); 218 219(* Theorem: A submonoid h of g implies identity is a homomorphism from h to g. 220 or h << g ==> Monoid h /\ Monoid g /\ submonoid h g *) 221(* Proof: 222 h << g ==> Monoid h /\ Monoid g by Submonoid_def 223 together with 224 H SUBSET G /\ ($o = $* ) /\ (#i = #e) by Submonoid_def 225 ==> !x. x IN H ==> x IN G /\ 226 !x y. x IN H /\ y IN H ==> (x o y = x * y) /\ 227 #i = #e by SUBSET_DEF 228 ==> MonoidHomo I h g by MonoidHomo_def, f = I. 229 ==> submonoid h g by submonoid_def 230*) 231val submonoid_homomorphism = store_thm( 232 "submonoid_homomorphism", 233 ``!(g:'a monoid) h. h << g ==> Monoid h /\ Monoid g /\ submonoid h g``, 234 rw_tac std_ss[Submonoid_def, submonoid_def, MonoidHomo_def, SUBSET_DEF]); 235 236(* original: 237g `!(g:'a monoid) h. h << g = Monoid h /\ Monoid g /\ submonoid h g`; 238e (rw_tac std_ss[Submonoid_def, submonoid_def, MonoidHomo_def, SUBSET_DEF, EQ_IMP_THM]); 239 240The only-if part (<==) cannot be proved: 241Note Submonoid_def uses h.op = g.op, 242but submonoid_def uses homomorphism I, and so cannot show this for any x y. 243*) 244 245(* Theorem: h << g ==> !x. x IN H ==> (order h x = ord x) *) 246(* Proof: 247 Note Monoid g /\ Monoid h /\ submonoid h g by submonoid_homomorphism, h << g 248 Thus !x. x IN H ==> (order h x = ord x) by submonoid_order_eqn 249*) 250val submonoid_order = store_thm( 251 "submonoid_order", 252 ``!(g:'a monoid) h. h << g ==> !x. x IN H ==> (order h x = ord x)``, 253 metis_tac[submonoid_homomorphism, submonoid_order_eqn]); 254 255(* Theorem: Monoid g ==> !h. Submonoid h g <=> 256 H SUBSET G /\ (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\ (h.id IN H) /\ (h.op = $* ) /\ (h.id = #e) *) 257(* Proof: 258 By Submonoid_def, EQ_IMP_THM, this is to show: 259 (1) x IN H /\ y IN H ==> x * y IN H, true by monoid_op_element 260 (2) #e IN H, true by monoid_id_element 261 (3) Monoid h 262 By Monoid_def, this is to show: 263 (1) x IN H /\ y IN H /\ z IN H 264 ==> x * y * z = x * (y * z), true by monoid_assoc, SUBSET_DEF 265 (2) x IN H ==> #e * x = x, true by monoid_lid, SUBSET_DEF 266 (3) x IN H ==> x * #e = x, true by monoid_rid, SUBSET_DEF 267*) 268val submonoid_alt = store_thm( 269 "submonoid_alt", 270 ``!g:'a monoid. Monoid g ==> !h. Submonoid h g <=> 271 H SUBSET G /\ (* subset *) 272 (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\ (* closure *) 273 (h.id IN H) /\ (* has identity *) 274 (h.op = g.op ) /\ (h.id = #e)``, 275 rw_tac std_ss[Submonoid_def, EQ_IMP_THM] >- 276 metis_tac[monoid_op_element] >- 277 metis_tac[monoid_id_element] >> 278 rw_tac std_ss[Monoid_def] >- 279 fs[monoid_assoc, SUBSET_DEF] >- 280 fs[monoid_lid, SUBSET_DEF] >> 281 fs[monoid_rid, SUBSET_DEF]); 282 283(* ------------------------------------------------------------------------- *) 284(* Submonoid Theorems *) 285(* ------------------------------------------------------------------------- *) 286 287(* Theorem: Monoid g ==> g << g *) 288(* Proof: by Submonoid_def, SUBSET_REFL *) 289val submonoid_reflexive = store_thm( 290 "submonoid_reflexive", 291 ``!g:'a monoid. Monoid g ==> g << g``, 292 rw_tac std_ss[Submonoid_def, SUBSET_REFL]); 293 294(* Theorem: h << g /\ g << h ==> (h = g) *) 295(* Proof: 296 Since h << g ==> Monoid h /\ Monoid g /\ H SUBSET G /\ ($o = $* ) /\ (#i = #e) by Submonoid_def 297 and g << h ==> Monoid g /\ Monoid h /\ G SUBSET H /\ ($* = $o) /\ (#e = #i) by Submonoid_def 298 Now, H SUBSET G /\ G SUBSET H ==> H = G by SUBSET_ANTISYM 299 Hence h = g by monoid_component_equality 300*) 301val submonoid_antisymmetric = store_thm( 302 "submonoid_antisymmetric", 303 ``!g h:'a monoid. h << g /\ g << h ==> (h = g)``, 304 rw_tac std_ss[Submonoid_def] >> 305 full_simp_tac bool_ss[monoid_component_equality, SUBSET_ANTISYM]); 306 307(* Theorem: k << h /\ h << g ==> k << g *) 308(* Proof: by Submonoid_def and SUBSET_TRANS *) 309val submonoid_transitive = store_thm( 310 "submonoid_transitive", 311 ``!g h k:'a monoid. k << h /\ h << g ==> k << g``, 312 rw_tac std_ss[Submonoid_def] >> 313 metis_tac[SUBSET_TRANS]); 314 315(* Theorem: h << g ==> Monoid h *) 316(* Proof: by Submonoid_def. *) 317val submonoid_monoid = store_thm( 318 "submonoid_monoid", 319 ``!g h:'a monoid. h << g ==> Monoid h``, 320 rw[Submonoid_def]); 321 322(* ------------------------------------------------------------------------- *) 323(* Submonoid Intersection *) 324(* ------------------------------------------------------------------------- *) 325 326(* Define intersection of monoids *) 327val monoid_intersect_def = Define` 328 monoid_intersect (g:'a monoid) (h:'a monoid) = 329 <| carrier := G INTER H; 330 op := $*; (* g.op *) 331 id := #e (* g.id *) 332 |> 333`; 334 335val _ = overload_on ("mINTER", ``monoid_intersect``); 336val _ = set_fixity "mINTER" (Infix(NONASSOC, 450)); (* same as relation *) 337(* 338> monoid_intersect_def; 339val it = |- !g h. g mINTER h = <|carrier := G INTER H; op := $*; id := #e|>: thm 340*) 341 342(* Theorem: ((g mINTER h).carrier = G INTER H) /\ 343 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e) *) 344(* Proof: by monoid_intersect_def *) 345val monoid_intersect_property = store_thm( 346 "monoid_intersect_property", 347 ``!g h:'a monoid. ((g mINTER h).carrier = G INTER H) /\ 348 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e)``, 349 rw[monoid_intersect_def]); 350 351(* Theorem: !x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H *) 352(* Proof: 353 x IN (g mINTER h).carrier 354 ==> x IN G INTER H by monoid_intersect_def 355 ==> x IN G and x IN H by IN_INTER 356*) 357val monoid_intersect_element = store_thm( 358 "monoid_intersect_element", 359 ``!g h:'a monoid. !x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H``, 360 rw[monoid_intersect_def, IN_INTER]); 361 362(* Theorem: (g mINTER h).id = #e *) 363(* Proof: by monoid_intersect_def. *) 364val monoid_intersect_id = store_thm( 365 "monoid_intersect_id", 366 ``!g h:'a monoid. (g mINTER h).id = #e``, 367 rw[monoid_intersect_def]); 368 369(* Theorem: h << g /\ k << g ==> 370 ((h mINTER k).carrier = H INTER K) /\ 371 (!x y. x IN H INTER K /\ y IN H INTER K ==> ((h mINTER k).op x y = x * y)) /\ 372 ((h mINTER k).id = #e) *) 373(* Proof: 374 (h mINTER k).carrier = H INTER K by monoid_intersect_def 375 Hence x IN (h mINTER k).carrier ==> x IN H /\ x IN K by IN_INTER 376 and y IN (h mINTER k).carrier ==> y IN H /\ y IN K by IN_INTER 377 so (h mINTER k).op x y = x o y by monoid_intersect_def 378 = x * y by submonoid_property 379 and (h mINTER k).id = #i by monoid_intersect_def 380 = #e by submonoid_property 381*) 382val submonoid_intersect_property = store_thm( 383 "submonoid_intersect_property", 384 ``!g h k:'a monoid. h << g /\ k << g ==> 385 ((h mINTER k).carrier = H INTER K) /\ 386 (!x y. x IN H INTER K /\ y IN H INTER K ==> ((h mINTER k).op x y = x * y)) /\ 387 ((h mINTER k).id = #e)``, 388 rw[monoid_intersect_def, submonoid_property]); 389 390(* Theorem: h << g /\ k << g ==> Monoid (h mINTER k) *) 391(* Proof: 392 By definitions, this is to show: 393 (1) x IN H INTER K /\ y IN H INTER K ==> x o y IN H INTER K 394 x IN H INTER K ==> x IN H /\ x IN K by IN_INTER 395 y IN H INTER K ==> y IN H /\ y IN K by IN_INTER 396 x IN H /\ y IN H ==> x o y IN H by monoid_op_element 397 x IN K /\ y IN K ==> k.op x y IN K by monoid_op_element 398 x o y = x * y by submonoid_property 399 k.op x y = x * y by submonoid_property 400 Hence x o y IN H INTER K by IN_INTER 401 (2) x IN H INTER K /\ y IN H INTER K /\ z IN H INTER K ==> (x o y) o z = x o y o z 402 x IN H INTER K ==> x IN H by IN_INTER 403 y IN H INTER K ==> y IN H by IN_INTER 404 z IN H INTER K ==> z IN H by IN_INTER 405 x IN H /\ y IN H ==> x o y IN H by monoid_op_element 406 y IN H /\ z IN H ==> y o z IN H by monoid_op_element 407 x, y, z IN H ==> x, y, z IN G by submonoid_element 408 LHS = (x o y) o z 409 = (x o y) * z by submonoid_property 410 = (x * y) * z by submonoid_property 411 = x * (y * z) by monoid_assoc 412 = x * (y o z) by submonoid_property 413 = x o (y o z) = RHS by submonoid_property 414 (3) #i IN H INTER K 415 #i IN H and #i = #e by monoid_id_element, submonoid_id 416 k.id IN K and k.id = #e by monoid_id_element, submonoid_id 417 Hence #e = #i IN H INTER K by IN_INTER 418 (4) x IN H INTER K ==> #i o x = x 419 x IN H INTER K ==> x IN H by IN_INTER 420 ==> x IN G by submonoid_element 421 #i IN H and #i = #e by monoid_id_element, submonoid_id 422 #i o x 423 = #i * x by submonoid_property 424 = #e * x by submonoid_id 425 = x by monoid_id 426 (5) x IN H INTER K ==> x o #i = x 427 x IN H INTER K ==> x IN H by IN_INTER 428 ==> x IN G by submonoid_element 429 #i IN H and #i = #e by monoid_id_element, submonoid_id 430 x o #i 431 = x * #i by submonoid_property 432 = x * #e by submonoid_id 433 = x by monoid_id 434*) 435val submonoid_intersect_monoid = store_thm( 436 "submonoid_intersect_monoid", 437 ``!g h k:'a monoid. h << g /\ k << g ==> Monoid (h mINTER k)``, 438 rpt strip_tac >> 439 `Monoid h /\ Monoid k /\ Monoid g` by metis_tac[submonoid_property] >> 440 rw_tac std_ss[Monoid_def, monoid_intersect_def] >| [ 441 `x IN H /\ x IN K /\ y IN H /\ y IN K` by metis_tac[IN_INTER] >> 442 `x o y IN H /\ (x o y = x * y)` by metis_tac[submonoid_property, monoid_op_element] >> 443 `k.op x y IN K /\ (k.op x y = x * y)` by metis_tac[submonoid_property, monoid_op_element] >> 444 metis_tac[IN_INTER], 445 `x IN H /\ y IN H /\ z IN H` by metis_tac[IN_INTER] >> 446 `x IN G /\ y IN G /\ z IN G` by metis_tac[submonoid_element] >> 447 `x o y IN H /\ y o z IN H` by metis_tac[monoid_op_element] >> 448 `(x o y) o z = (x * y) * z` by metis_tac[submonoid_property] >> 449 `x o (y o z) = x * (y * z)` by metis_tac[submonoid_property] >> 450 rw[monoid_assoc], 451 metis_tac[IN_INTER, submonoid_id, monoid_id_element], 452 metis_tac[submonoid_property, monoid_id, submonoid_element, IN_INTER, monoid_id_element], 453 metis_tac[submonoid_property, monoid_id, submonoid_element, IN_INTER, monoid_id_element] 454 ]); 455 456(* Theorem: h << g /\ k << g ==> (h mINTER k) << g *) 457(* Proof: 458 By Submonoid_def, this is to show: 459 (1) Monoid (h mINTER k), true by submonoid_intersect_monoid 460 (2) (h mINTER k).carrier SUBSET G 461 Since (h mINTER k).carrier = H INTER K by submonoid_intersect_property 462 and (H INTER K) SUBSET H by INTER_SUBSET 463 and h << g ==> H SUBSET G by submonoid_property 464 Hence (h mINTER k).carrier SUBSET G by SUBSET_TRANS 465 (3) (h mINTER k).op = $* 466 (h mINTER k).op = $o by monoid_intersect_def 467 = $* by Submonoid_def 468 (4) (h mINTER k).id = #e 469 (h mINTER k).id = #i by monoid_intersect_def 470 = #e by Submonoid_def 471*) 472val submonoid_intersect_submonoid = store_thm( 473 "submonoid_intersect_submonoid", 474 ``!g h k:'a monoid. h << g /\ k << g ==> (h mINTER k) << g``, 475 rpt strip_tac >> 476 `Monoid h /\ Monoid k /\ Monoid g` by metis_tac[submonoid_property] >> 477 rw[Submonoid_def] >| [ 478 metis_tac[submonoid_intersect_monoid], 479 `(h mINTER k).carrier = H INTER K` by metis_tac[submonoid_intersect_property] >> 480 `H SUBSET G` by rw[submonoid_property] >> 481 metis_tac[INTER_SUBSET, SUBSET_TRANS], 482 `(h mINTER k).op = $o` by rw[monoid_intersect_def] >> 483 metis_tac[Submonoid_def], 484 `(h mINTER k).id = #i` by rw[monoid_intersect_def] >> 485 metis_tac[Submonoid_def] 486 ]); 487 488(* ------------------------------------------------------------------------- *) 489(* Submonoid Big Intersection *) 490(* ------------------------------------------------------------------------- *) 491 492(* Define intersection of submonoids of a monoid *) 493val submonoid_big_intersect_def = Define` 494 submonoid_big_intersect (g:'a monoid) = 495 <| carrier := BIGINTER (IMAGE (\h. H) {h | h << g}); 496 op := $*; (* g.op *) 497 id := #e (* g.id *) 498 |> 499`; 500 501val _ = overload_on ("smbINTER", ``submonoid_big_intersect``); 502(* 503> submonoid_big_intersect_def; 504val it = |- !g. smbINTER g = 505 <|carrier := BIGINTER (IMAGE (\h. H) {h | h << g}); op := $*; id := #e|>: thm 506*) 507 508(* Theorem: ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\ 509 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\ 510 ((smbINTER g).id = #e) *) 511(* Proof: by submonoid_big_intersect_def. *) 512val submonoid_big_intersect_property = store_thm( 513 "submonoid_big_intersect_property", 514 ``!g:'a monoid. ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\ 515 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\ 516 ((smbINTER g).id = #e)``, 517 rw[submonoid_big_intersect_def]); 518 519(* Theorem: x IN (smbINTER g).carrier <=> (!h. h << g ==> x IN H) *) 520(* Proof: 521 x IN (smbINTER g).carrier 522 <=> x IN BIGINTER (IMAGE (\h. H) {h | h << g}) by submonoid_big_intersect_def 523 <=> !P. P IN (IMAGE (\h. H) {h | h << g}) ==> x IN P by IN_BIGINTER 524 <=> !P. ?h. (P = H) /\ h IN {h | h << g}) ==> x IN P by IN_IMAGE 525 <=> !P. ?h. (P = H) /\ h << g) ==> x IN P by GSPECIFICATION 526 <=> !h. h << g ==> x IN H 527*) 528val submonoid_big_intersect_element = store_thm( 529 "submonoid_big_intersect_element", 530 ``!g:'a monoid. !x. x IN (smbINTER g).carrier <=> (!h. h << g ==> x IN H)``, 531 rw[submonoid_big_intersect_def] >> 532 metis_tac[]); 533 534(* Theorem: x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> (smbINTER g).op x y IN (smbINTER g).carrier *) 535(* Proof: 536 Since x IN (smbINTER g).carrier, !h. h << g ==> x IN H by submonoid_big_intersect_element 537 also y IN (smbINTER g).carrier, !h. h << g ==> y IN H by submonoid_big_intersect_element 538 Now !h. h << g ==> x o y IN H by Submonoid_def, monoid_op_element 539 ==> x * y IN H by submonoid_property 540 Now, (smbINTER g).op x y = x * y by submonoid_big_intersect_property 541 Hence (smbINTER g).op x y IN (smbINTER g).carrier by submonoid_big_intersect_element 542*) 543val submonoid_big_intersect_op_element = store_thm( 544 "submonoid_big_intersect_op_element", 545 ``!g:'a monoid. !x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> 546 (smbINTER g).op x y IN (smbINTER g).carrier``, 547 rpt strip_tac >> 548 `!h. h << g ==> x IN H /\ y IN H` by metis_tac[submonoid_big_intersect_element] >> 549 `!h. h << g ==> x * y IN H` by metis_tac[Submonoid_def, monoid_op_element, submonoid_property] >> 550 `(smbINTER g).op x y = x * y` by rw[submonoid_big_intersect_property] >> 551 metis_tac[submonoid_big_intersect_element]); 552 553(* Theorem: (smbINTER g).id IN (smbINTER g).carrier *) 554(* Proof: 555 !h. h << g ==> #i = #e by submonoid_id 556 !h. h << g ==> #i IN H by Submonoid_def, monoid_id_element 557 Now (smbINTER g).id = #e by submonoid_big_intersect_property 558 Hence !h. h << g ==> (smbINTER g).id IN H by above 559 or (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_element 560*) 561val submonoid_big_intersect_has_id = store_thm( 562 "submonoid_big_intersect_has_id", 563 ``!g:'a monoid. (smbINTER g).id IN (smbINTER g).carrier``, 564 rpt strip_tac >> 565 `!h. h << g ==> (#i = #e)` by rw[submonoid_id] >> 566 `!h. h << g ==> #i IN H` by rw[Submonoid_def] >> 567 `(smbINTER g).id = #e` by metis_tac[submonoid_big_intersect_property] >> 568 metis_tac[submonoid_big_intersect_element]); 569 570(* Theorem: Monoid g ==> (smbINTER g).carrier SUBSET G *) 571(* Proof: 572 By submonoid_big_intersect_def, this is to show: 573 Monoid g ==> BIGINTER (IMAGE (\h. H) {h | h << g}) SUBSET G 574 Let P = IMAGE (\h. H) {h | h << g}. 575 Since g << g by submonoid_reflexive 576 so G IN P by IN_IMAGE, definition of P. 577 Thus P <> {} by MEMBER_NOT_EMPTY. 578 Now h << g ==> H SUBSET G by submonoid_property 579 Hence P SUBSET G by BIGINTER_SUBSET 580*) 581val submonoid_big_intersect_subset = store_thm( 582 "submonoid_big_intersect_subset", 583 ``!g:'a monoid. Monoid g ==> (smbINTER g).carrier SUBSET G``, 584 rw[submonoid_big_intersect_def] >> 585 qabbrev_tac `P = IMAGE (\h. H) {h | h << g}` >> 586 (`!x. x IN P <=> ?h. (H = x) /\ h << g` by (rw[Abbr`P`] >> metis_tac[])) >> 587 `g << g` by rw[submonoid_reflexive] >> 588 `P <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 589 `!h:'a monoid. h << g ==> H SUBSET G` by rw[submonoid_property] >> 590 metis_tac[BIGINTER_SUBSET]); 591 592(* Theorem: Monoid g ==> Monoid (smbINTER g) *) 593(* Proof: 594 Monoid g ==> (smbINTER g).carrier SUBSET G by submonoid_big_intersect_subset 595 By Monoid_def, this is to show: 596 (1) x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> (smbINTER g).op x y IN (smbINTER g).carrier 597 True by submonoid_big_intersect_op_element. 598 (2) (smbINTER g).op ((smbINTER g).op x y) z = (smbINTER g).op x ((smbINTER g).op y z) 599 Since (smbINTER g).op x y IN (smbINTER g).carrier by submonoid_big_intersect_op_element 600 and (smbINTER g).op y z IN (smbINTER g).carrier by submonoid_big_intersect_op_element 601 So this is to show: (x * y) * z = x * (y * z) by submonoid_big_intersect_property 602 Since x IN G, y IN G and z IN G by IN_SUBSET 603 This follows by monoid_assoc. 604 (3) (smbINTER g).id IN (smbINTER g).carrier 605 This is true by submonoid_big_intersect_has_id. 606 (4) x IN (smbINTER g).carrier ==> (smbINTER g).op (smbINTER g).id x = x 607 Since (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_op_element 608 and (smbINTER g).id = #e by submonoid_big_intersect_property 609 also x IN G by IN_SUBSET 610 (smbINTER g).op (smbINTER g).id x 611 = #e * x by submonoid_big_intersect_property 612 = x by monoid_id 613 (5) x IN (smbINTER g).carrier ==> (smbINTER g).op x (smbINTER g).id = x 614 Since (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_op_element 615 and (smbINTER g).id = #e by submonoid_big_intersect_property 616 also x IN G by IN_SUBSET 617 (smbINTER g).op x (smbINTER g).id 618 = x * #e by submonoid_big_intersect_property 619 = x by monoid_id 620*) 621val submonoid_big_intersect_monoid = store_thm( 622 "submonoid_big_intersect_monoid", 623 ``!g:'a monoid. Monoid g ==> Monoid (smbINTER g)``, 624 rpt strip_tac >> 625 `(smbINTER g).carrier SUBSET G` by rw[submonoid_big_intersect_subset] >> 626 rw_tac std_ss[Monoid_def] >| [ 627 metis_tac[submonoid_big_intersect_op_element], 628 `(smbINTER g).op x y IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_op_element] >> 629 `(smbINTER g).op y z IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_op_element] >> 630 `(x * y) * z = x * (y * z)` suffices_by rw[submonoid_big_intersect_property] >> 631 `x IN G /\ y IN G /\ z IN G` by metis_tac[IN_SUBSET] >> 632 rw[monoid_assoc], 633 metis_tac[submonoid_big_intersect_has_id], 634 `(smbINTER g).id = #e` by rw[submonoid_big_intersect_property] >> 635 `(smbINTER g).id IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_has_id] >> 636 `#e * x = x` suffices_by rw[submonoid_big_intersect_property] >> 637 `x IN G` by metis_tac[IN_SUBSET] >> 638 rw[], 639 `(smbINTER g).id = #e` by rw[submonoid_big_intersect_property] >> 640 `(smbINTER g).id IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_has_id] >> 641 `x * #e = x` suffices_by rw[submonoid_big_intersect_property] >> 642 `x IN G` by metis_tac[IN_SUBSET] >> 643 rw[] 644 ]); 645 646(* Theorem: Monoid g ==> (smbINTER g) << g *) 647(* Proof: 648 By Submonoid_def, this is to show: 649 (1) Monoid (smbINTER g) 650 True by submonoid_big_intersect_monoid. 651 (2) (smbINTER g).carrier SUBSET G 652 True by submonoid_big_intersect_subset. 653 (3) (smbINTER g).op = $* 654 True by submonoid_big_intersect_def 655 (4) (smbINTER g).id = #e 656 True by submonoid_big_intersect_def 657*) 658val submonoid_big_intersect_submonoid = store_thm( 659 "submonoid_big_intersect_submonoid", 660 ``!g:'a monoid. Monoid g ==> (smbINTER g) << g``, 661 rw_tac std_ss[Submonoid_def] >| [ 662 rw[submonoid_big_intersect_monoid], 663 rw[submonoid_big_intersect_subset], 664 rw[submonoid_big_intersect_def], 665 rw[submonoid_big_intersect_def] 666 ]); 667 668(* ------------------------------------------------------------------------- *) 669 670(* export theory at end *) 671val _ = export_theory(); 672 673(*===========================================================================*) 674