5250
|
1 |
(* Title: HOL/ex/LocaleGroup.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
4 |
|
|
5 |
Group theory via records and locales.
|
|
6 |
*)
|
|
7 |
|
|
8 |
LocaleGroup = PiSets + Record +
|
|
9 |
|
|
10 |
record 'a grouptype =
|
|
11 |
carrier :: "'a set"
|
|
12 |
bin_op :: "['a, 'a] => 'a"
|
|
13 |
inverse :: "'a => 'a"
|
|
14 |
unit :: "'a"
|
|
15 |
|
|
16 |
constdefs
|
|
17 |
Group :: "('a, 'more) grouptype_scheme set"
|
5846
|
18 |
"Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
|
|
19 |
inverse G : carrier G -> carrier G
|
5250
|
20 |
& unit G : carrier G &
|
|
21 |
(! x: carrier G. ! y: carrier G. !z: carrier G.
|
|
22 |
(bin_op G (inverse G x) x = unit G)
|
|
23 |
& (bin_op G (unit G) x = x)
|
5846
|
24 |
& (bin_op G (bin_op G x y) z =
|
|
25 |
bin_op G (x) (bin_op G y z)))}"
|
5250
|
26 |
|
|
27 |
locale groups =
|
|
28 |
fixes
|
|
29 |
G ::"('a, 'more :: more) grouptype_scheme"
|
|
30 |
e :: "'a"
|
|
31 |
binop :: "'a => 'a => 'a" (infixr "#" 80)
|
5846
|
32 |
(*INV renamed from inv temporarily to avoid clash with Fun.inv*)
|
5848
|
33 |
INV :: "'a => 'a" ("i'(_')")
|
5250
|
34 |
assumes
|
|
35 |
Group_G "G: Group"
|
|
36 |
defines
|
5846
|
37 |
e_def "e == unit G"
|
|
38 |
binop_def "x # y == bin_op G x y"
|
|
39 |
inv_def "INV == inverse G"
|
5250
|
40 |
|
|
41 |
end
|