|
1 (* Title: HOL/GroupTheory/RingConstr |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 1998-2001 University of Cambridge |
|
5 |
|
6 Construction of a ring from a semigroup and an Abelian group |
|
7 *) |
|
8 |
|
9 RingConstr = Homomorphism + |
|
10 |
|
11 constdefs |
|
12 ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype" |
|
13 "ring_of == |
|
14 lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}. |
|
15 (| carrier = (G.<cr>), bin_op = (G.<f>), |
|
16 inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)" |
|
17 |
|
18 ring_constr :: "('a grouptype * 'a semigrouptype *'a ringtype) set" |
|
19 "ring_constr == |
|
20 \\<Sigma>G \\<in> AbelianGroup. \\<Sigma>S \\<in> {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}. |
|
21 {R. R = (| carrier = (G.<cr>), bin_op = (G.<f>), |
|
22 inverse = (G.<inv>), unit = (G.<e>), |
|
23 Rmult = (S.<f>) |) & |
|
24 (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). |
|
25 ((R.<m>) x ((R.<f>) y z) = (R.<f>) ((R.<m>) x y) ((R.<m>) x z))) & |
|
26 (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). |
|
27 ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}" |
|
28 |
|
29 ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype" |
|
30 "ring_from == lam G: AbelianGroup. |
|
31 lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) & |
|
32 distr_l (G.<cr>) (M.<f>) (G.<f>) & |
|
33 distr_r (G.<cr>) (M.<f>) (G.<f>)}. |
|
34 (| carrier = (G.<cr>), bin_op = (G.<f>), |
|
35 inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)" |
|
36 |
|
37 end |
|
38 |