equal
deleted
inserted
replaced
|
1 (* Title: HOL/GroupTheory/Group |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 2001 University of Cambridge |
|
5 *) |
|
6 |
|
7 (* Theory file for the proof of Sylow's theorem. F. Kammueller 11.10.96 |
|
8 Step 1: Use two separate .thy files for groups and Sylow's thm, respectively: |
|
9 |
|
10 I.e. here are the definitions which are specific for Sylow's theorem. |
|
11 *) |
|
12 |
|
13 Sylow = Group + |
|
14 |
|
15 types i |
|
16 arities i::term |
|
17 |
|
18 consts |
|
19 G :: "i set * ([i, i] => i) * (i => i) * i" |
|
20 (* overloading for the carrier of G does not work because "duplicate declaration" : G :: "i set" *) |
|
21 p, a, m :: "nat" |
|
22 r_cos :: "[i set, i] => i set" ("_ #> _" [60,61]60) |
|
23 "##" :: "[i, i] => i" (infixl 60) |
|
24 |
|
25 (* coset and bin_op short forms *) |
|
26 defs |
|
27 r_coset_abbr "H #> x == r_coset G H x" |
|
28 bin_op_abbr "x ## y == bin_op G x y" |
|
29 |
|
30 constdefs |
|
31 e :: "i" "e == unity G" |
|
32 inv :: "i => i" "inv == invers G" |
|
33 calM :: "i set set" |
|
34 "calM == {s. s <= carrier(G) & card(s) = (p ^ a)}" |
|
35 RelM :: "(i set * i set)set" |
|
36 "RelM == {(N1,N2).(N1,N2): calM <*> calM & (? g: carrier(G). N1 = (N2 #> g) )}" |
|
37 |
|
38 rules |
|
39 (* specific rules modeling the section mechanism *) |
|
40 p1 "p : prime" |
|
41 p2 "G : Group" |
|
42 p3 "order(G) = (p ^ a) * m" |
|
43 p4 "finite (carrier G)" |
|
44 |
|
45 end |