|
11448
|
1 |
(* Title: HOL/GroupTheory/FactGroup
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Florian Kammueller, with new proofs by L C Paulson
|
|
|
4 |
Copyright 1998-2001 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Factorization of a group
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
FactGroup = Coset +
|
|
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
|
|
|
13 |
|
|
|
14 |
"FactGroup ==
|
|
|
15 |
lam G: Group. lam H: {H. H <| G}.
|
|
|
16 |
(| carrier = set_r_cos G H,
|
|
|
17 |
bin_op = (lam X: set_r_cos G H. lam Y: set_r_cos G H. set_prod G X Y),
|
|
|
18 |
inverse = (lam X: set_r_cos G H. set_inv G X),
|
|
|
19 |
unit = H |)"
|
|
|
20 |
|
|
|
21 |
syntax
|
|
|
22 |
"@Fact" :: "['a grouptype, 'a set] => ('a set) grouptype"
|
|
|
23 |
("_ Mod _" [60,61]60)
|
|
|
24 |
|
|
|
25 |
translations
|
|
|
26 |
"G Mod H" == "FactGroup G H"
|
|
|
27 |
|
|
|
28 |
locale factgroup = coset +
|
|
|
29 |
fixes
|
|
|
30 |
F :: "('a set) grouptype"
|
|
|
31 |
H :: "('a set)"
|
|
|
32 |
assumes
|
|
|
33 |
H_normal "H <| G"
|
|
|
34 |
defines
|
|
|
35 |
F_def "F == FactGroup G H"
|
|
|
36 |
|
|
|
37 |
end
|
|
|
38 |
|