src/HOL/GroupTheory/DirProd.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/DirProd.thy	Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,47 @@
+(*  Title:      HOL/GroupTheory/DirProd
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Copyright   1998-2001  University of Cambridge
+
+Direct product of two groups
+*)
+
+DirProd = Coset +
+
+consts
+  ProdGroup :: "(['a grouptype, 'b grouptype] => ('a * 'b) grouptype)"
+
+defs 
+  ProdGroup_def "ProdGroup == lam G: Group. lam G': Group.
+    (| carrier = ((G.<cr>) \\<times> (G'.<cr>)),
+       bin_op = (lam (x, x'): ((G.<cr>) \\<times> (G'.<cr>)). 
+                 lam (y, y'): ((G.<cr>) \\<times> (G'.<cr>)).
+                  ((G.<f>) x y,(G'.<f>) x' y')),
+       inverse = (lam (x, y): ((G.<cr>) \\<times> (G'.<cr>)). ((G.<inv>) x, (G'.<inv>) y)),
+       unit = ((G.<e>),(G'.<e>)) |)"
+
+syntax
+  "@Pro" :: "['a grouptype, 'b grouptype] => ('a * 'b) grouptype" ("<|_,_|>" [60,61]60)
+
+translations
+  "<| G , G' |>" == "ProdGroup G G'"
+
+locale r_group = group +
+  fixes
+    G'        :: "'b grouptype"
+    e'        :: "'b"
+    binop'    :: "'b => 'b => 'b" 	("(_ ##' _)" [80,81]80 )
+    INV'      :: "'b => 'b"              ("i' (_)"      [90]91)
+  assumes 
+    Group_G' "G' : Group"
+  defines
+    e'_def  "e' == unit G'"
+    binop'_def "x ##' y == bin_op G' x y"
+    inv'_def "i'(x) == inverse G' x"
+
+locale prodgroup = r_group +
+  fixes 
+    P :: "('a * 'b) grouptype"
+  defines 
+    P_def "P == <| G, G' |>"
+end