canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)
(* 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