src/HOL/GroupTheory/DirProd.ML

less_induct, wf_induct_rule;

(*  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
*)

Open_locale "prodgroup";

val e'_def = thm "e'_def";
val binop'_def = thm "binop'_def";
val inv'_def = thm "inv'_def";
val P_def = thm "P_def";
val Group_G' = thm "Group_G'";


Addsimps [P_def, Group_G', Group_G];

Goal "(P.<cr>) = ((G.<cr>) \\<times> (G'.<cr>))";
by (afs [ProdGroup_def] 1);
qed "P_carrier";

Goal "(P.<f>) = \
\     (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>). ( x ## y, x' ##' y'))";
by (afs [ProdGroup_def, binop_def, binop'_def] 1);
qed "P_bin_op";

Goal "(P.<inv>) = (lam (x, y): (P.<cr>). (i x, i' y))";
by (afs [ProdGroup_def, inv_def, inv'_def] 1);
qed "P_inverse";

Goal "(P.<e>) = (G.<e>, G'.<e>)";
by (afs [ProdGroup_def, e_def, e'_def] 1);
qed "P_unit";

Goal "P = (| carrier = P.<cr>, \
\       bin_op = (lam (x, x'): (P.<cr>). lam (y, y'): (P.<cr>).\
\                  (x ## y, x' ##' y')), \
\       inverse = (lam (x, y): (P.<cr>). (i x, i' y)), \
\       unit = P.<e> |)";
by (afs [ProdGroup_def, P_carrier, P_bin_op, P_inverse, P_unit] 1);
by (afs [binop_def, binop'_def, inv_def, inv'_def] 1);
qed "P_defI";
val P_DefI = export P_defI;

Delsimps [P_def];

Goal "(P.<f>) : (P.<cr>) \\<rightarrow> (P.<cr>) \\<rightarrow> (P.<cr>)";
by (auto_tac (claset() addSIs [restrictI], 
              simpset() addsimps  [P_bin_op, P_carrier, binop'_def, 
                                   bin_op_closed])); 
qed "bin_op_prod_closed";

Goal "(P.<inv>) : (P.<cr>) \\<rightarrow> (P.<cr>)";
by (auto_tac (claset() addSIs [restrictI], 
              simpset() addsimps  [P_inverse, P_carrier, inv_closed, 
                    inv'_def, inverse_closed])); 
qed "inverse_prod_closed";

(* MAIN PROOF *)
Goal "P : Group";
by (stac P_defI 1);
by (rtac GroupI 1);
by (auto_tac (claset(), 
       simpset() addsimps ([P_carrier,P_bin_op,P_inverse,P_unit] RL [sym]))); 
(* 1.  *)
by (rtac bin_op_prod_closed 1);
(* 2. *)
by (rtac inverse_prod_closed 1);
(* 3. *)
by (afs [P_carrier, P_unit, export e_closed] 1);
(* 4. *)
by (afs [P_carrier, P_bin_op, P_inverse, P_unit, Group_G' RS inverse_closed,
         inv'_def, e_def, binop'_def, Group_G' RS (export inv_ax2)] 1);
(* 5 *)
by (afs [P_carrier,P_bin_op,P_unit, Group_G' RS unit_closed, export e_ax1,
         binop_def, binop'_def] 1);
(* 6 *)
by (afs [P_carrier,P_bin_op, Group_G' RS bin_op_closed, 
         binop'_def, binop_assoc,export binop_assoc] 1);
qed "prodgroup_is_group";
val ProdGroup_is_Group = export prodgroup_is_group;

Delsimps [P_def, Group_G', Group_G];

Close_locale "prodgroup";
Close_locale "r_group";
Close_locale "group";

Goal "ProdGroup : Group \\<rightarrow> Group \\<rightarrow> Group";
by (REPEAT (ares_tac [funcsetI, ProdGroup_is_Group] 1));
by (auto_tac (claset(), simpset() addsimps [ProdGroup_def])); 
qed "ProdGroup_arity";