author | nipkow |
Tue, 26 Nov 1996 14:28:17 +0100 | |
changeset 2223 | 4b43a8d046e5 |
permissions | -rw-r--r-- |
2223
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Group.thy |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1996 TU Muenchen |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
5 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
6 |
A little bit of group theory leading up to rings. Hence groups are additive. |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
7 |
*) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
8 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
9 |
Group = Set + |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
10 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
11 |
(* 0 already used in Nat *) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
12 |
axclass zero < term |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
13 |
consts zero :: "'a::zero" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
14 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
15 |
(* additive semigroups *) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
16 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
17 |
axclass add_semigroup < plus |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
18 |
plus_assoc "(x + y) + z = x + (y + z)" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
19 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
20 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
21 |
(* additive monoids *) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
22 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
23 |
axclass add_monoid < add_semigroup, zero |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
24 |
zeroL "zero + x = x" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
25 |
zeroR "x + zero = x" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
26 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
27 |
(* additive groups *) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
28 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
29 |
axclass add_group < add_monoid, minus |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
30 |
left_inv "(zero-x)+x = zero" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
31 |
minus_inv "x-y = x + (zero-y)" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
32 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
33 |
(* additive abelian groups *) |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
34 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
35 |
axclass add_agroup < add_group |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
36 |
plus_commute "x + y = y + x" |
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
37 |
|
4b43a8d046e5
A bit of commutative ing theory, with a simplification tacxtic and an example.
nipkow
parents:
diff
changeset
|
38 |
end |