|
1 (* Title: HOL/GroupTheory/Coset |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 1998-2001 University of Cambridge |
|
5 |
|
6 Theory of cosets, using locales |
|
7 *) |
|
8 |
|
9 Coset = Group + Exponent + |
|
10 |
|
11 constdefs |
|
12 r_coset :: "['a grouptype,'a set, 'a] => 'a set" |
|
13 "r_coset G H a == (% x. (bin_op G) x a) ` H" |
|
14 |
|
15 l_coset :: "['a grouptype, 'a, 'a set] => 'a set" |
|
16 "l_coset G a H == (% x. (bin_op G) a x) ` H" |
|
17 |
|
18 set_r_cos :: "['a grouptype,'a set] => ('a set)set" |
|
19 "set_r_cos G H == r_coset G H ` (carrier G)" |
|
20 |
|
21 set_prod :: "['a grouptype,'a set,'a set] => 'a set" |
|
22 "set_prod G H1 H2 == (%x. (bin_op G) (fst x)(snd x)) ` (H1 \\<times> H2)" |
|
23 set_inv :: "['a grouptype,'a set] => 'a set" |
|
24 "set_inv G H == (%x. (inverse G) x) ` H" |
|
25 |
|
26 normal :: "('a grouptype * 'a set)set" |
|
27 "normal == \\<Sigma>G \\<in> Group. {H. H <<= G & |
|
28 (\\<forall>x \\<in> carrier G. r_coset G H x = l_coset G x H)}" |
|
29 |
|
30 |
|
31 syntax |
|
32 "@NS" :: "['a set, 'a grouptype] => bool" ("_ <| _" [60,61]60) |
|
33 |
|
34 syntax (xsymbols) |
|
35 "@NS" :: "['a set, 'a grouptype] => bool" ("_ \\<lhd> _" [60,61]60) |
|
36 |
|
37 translations |
|
38 "N <| G" == "(G,N) \\<in> normal" |
|
39 |
|
40 locale coset = group + |
|
41 fixes |
|
42 rcos :: "['a set, 'a] => 'a set" ("_ #> _" [60,61]60) |
|
43 lcos :: "['a, 'a set] => 'a set" ("_ <# _" [60,61]60) |
|
44 setprod :: "['a set, 'a set] => 'a set" ("_ <#> _" [60,61]60) |
|
45 setinv :: "'a set => 'a set" ("I (_)" [90]91) |
|
46 setrcos :: "'a set => 'a set set" ("{*_*}" [90]91) |
|
47 assumes |
|
48 |
|
49 defines |
|
50 rcos_def "H #> x == r_coset G H x" |
|
51 lcos_def "x <# H == l_coset G x H" |
|
52 setprod_def "H1 <#> H2 == set_prod G H1 H2" |
|
53 setinv_def "I(H) == set_inv G H" |
|
54 setrcos_def "{*H*} == set_r_cos G H" |
|
55 |
|
56 end |
|
57 |
|
58 |