author | paulson |
Wed, 25 Jul 2001 13:13:01 +0200 | |
changeset 11451 | 8abfb4f7bd02 |
parent 11448 | aa519e0cc050 |
child 12459 | 6978ab7cac64 |
permissions | -rw-r--r-- |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11448
diff
changeset
|
1 |
(* Title: HOL/GroupTheory/Ring |
11448 | 2 |
ID: $Id$ |
3 |
Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 |
Copyright 1998-2001 University of Cambridge |
|
5 |
||
6 |
Ring theory. Sigma version |
|
7 |
*) |
|
8 |
||
9 |
Ring = Coset + |
|
10 |
||
11 |
record 'a ringtype = 'a grouptype + |
|
12 |
Rmult :: "['a, 'a] => 'a" |
|
13 |
||
14 |
syntax |
|
15 |
"@Rmult" :: "('a ringtype) => (['a, 'a] => 'a)" ("_ .<m>" [10] 10) |
|
16 |
||
17 |
translations |
|
18 |
"R.<m>" == "Rmult R" |
|
19 |
||
20 |
constdefs |
|
21 |
distr_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool" |
|
22 |
"distr_l S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S. |
|
23 |
(f1 x (f2 y z) = f2 (f1 x y) (f1 x z)))" |
|
24 |
distr_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool" |
|
25 |
"distr_r S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S. |
|
26 |
(f1 (f2 y z) x = f2 (f1 y x) (f1 z x)))" |
|
27 |
||
28 |
consts |
|
29 |
Ring :: "('a ringtype) set" |
|
30 |
||
31 |
defs |
|
32 |
Ring_def |
|
33 |
"Ring == |
|
34 |
{R. (| carrier = (R.<cr>), bin_op = (R.<f>), |
|
35 |
inverse = (R.<inv>), unit = (R.<e>) |) \\<in> AbelianGroup & |
|
36 |
(R.<m>) \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>) & |
|
37 |
(\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). |
|
38 |
((R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z)) & |
|
39 |
distr_l (R.<cr>)(R.<m>)(R.<f>) & |
|
40 |
distr_r (R.<cr>)(R.<m>)(R.<f>) }" |
|
41 |
||
42 |
||
43 |
constdefs |
|
44 |
group_of :: "'a ringtype => 'a grouptype" |
|
45 |
"group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>), |
|
46 |
inverse = (R.<inv>), unit = (R.<e>) |)" |
|
47 |
||
48 |
locale ring = group + |
|
49 |
fixes |
|
50 |
R :: "'a ringtype" |
|
51 |
rmult :: "['a, 'a] => 'a" (infixr "**" 80) |
|
52 |
assumes |
|
53 |
Ring_R "R \\<in> Ring" |
|
54 |
defines |
|
55 |
rmult_def "op ** == (R.<m>)" |
|
56 |
R_id_G "G == group_of R" |
|
57 |
||
58 |
end |
|
59 |
||
60 |