| author | paulson |
| Tue, 13 Aug 2002 17:42:34 +0200 | |
| changeset 13496 | 6f0c57def6d5 |
| parent 12459 | 6978ab7cac64 |
| permissions | -rw-r--r-- |
| 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 == |
|
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
15 |
%G: Group. %H: {H. H <| G}.
|
| 11448 | 16 |
(| carrier = set_r_cos G H, |
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
17 |
bin_op = (%X: set_r_cos G H. %Y: set_r_cos G H. set_prod G X Y), |
|
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
18 |
inverse = (%X: set_r_cos G H. set_inv G X), |
| 11448 | 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 |