src/HOL/GroupTheory/RingConstr.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/RingConstr.thy	Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,38 @@
+(*  Title:      HOL/GroupTheory/RingConstr
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Copyright   1998-2001  University of Cambridge
+
+Construction of a ring from a semigroup and an Abelian group 
+*)
+
+RingConstr = Homomorphism +
+
+constdefs
+  ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
+  "ring_of ==
+     lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
+                   (| carrier = (G.<cr>), bin_op = (G.<f>), 
+                      inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
+
+  ring_constr :: "('a grouptype * 'a semigrouptype *'a ringtype) set"
+  "ring_constr ==
+    \\<Sigma>G \\<in> AbelianGroup. \\<Sigma>S \\<in> {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
+	 {R. R = (| carrier = (G.<cr>), bin_op = (G.<f>), 
+		     inverse = (G.<inv>), unit = (G.<e>),
+		     Rmult = (S.<f>) |) &
+	     (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). 
+	     ((R.<m>) x ((R.<f>) y z) = (R.<f>) ((R.<m>) x y) ((R.<m>) x z))) &
+(\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). 
+	     ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
+
+  ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
+  "ring_from == lam G: AbelianGroup. 
+     lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
+                distr_l (G.<cr>) (M.<f>) (G.<f>) &
+	        distr_r (G.<cr>) (M.<f>) (G.<f>)}.
+            (| carrier = (G.<cr>), bin_op = (G.<f>), 
+               inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
+
+end
+