author | paulson |
Tue, 13 Aug 2002 17:42:34 +0200 | |
changeset 13496 | 6f0c57def6d5 |
parent 12459 | 6978ab7cac64 |
permissions | -rw-r--r-- |
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 == |
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
14 |
%G: AbelianGroup. %S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}. |
11448 | 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" |
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
30 |
"ring_from == %G: AbelianGroup. |
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11448
diff
changeset
|
31 |
%S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) & |
11448 | 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 |