11448
|
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 |
|