11448
|
1 |
(* Title: HOL/GroupTheory/FactGroup
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, with new proofs by L C Paulson
|
|
4 |
Copyright 1998-2001 University of Cambridge
|
|
5 |
|
|
6 |
Factorization of a group
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
Open_locale "factgroup";
|
|
11 |
|
|
12 |
val H_normal = thm "H_normal";
|
|
13 |
val F_def = thm "F_def";
|
|
14 |
|
|
15 |
Addsimps [H_normal, F_def,setrcos_def];
|
|
16 |
|
|
17 |
Goal "carrier F = {* H *}";
|
|
18 |
by (afs [FactGroup_def] 1);
|
|
19 |
qed "F_carrier";
|
|
20 |
|
|
21 |
Goal "bin_op F = (lam X: {* H *}. lam Y: {* H *}. X <#> Y) ";
|
|
22 |
by (afs [FactGroup_def, setprod_def] 1);
|
|
23 |
qed "F_bin_op";
|
|
24 |
|
|
25 |
Goal "inverse F = (lam X: {* H *}. I(X))";
|
|
26 |
by (afs [FactGroup_def, setinv_def] 1);
|
|
27 |
qed "F_inverse";
|
|
28 |
|
|
29 |
Goal "unit F = H";
|
|
30 |
by (afs [FactGroup_def] 1);
|
|
31 |
qed "F_unit";
|
|
32 |
|
|
33 |
Goal "F = (| carrier = {* H *}, \
|
|
34 |
\ bin_op = (lam X: {* H *}. lam Y: {* H *}. X <#> Y), \
|
|
35 |
\ inverse = (lam X: {* H *}. I(X)), unit = H |)";
|
|
36 |
by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
|
|
37 |
by (auto_tac (claset() addSIs [restrict_ext],
|
|
38 |
simpset() addsimps [set_prod_def, setprod_def, setinv_def]));
|
|
39 |
qed "F_defI";
|
|
40 |
val F_DefI = export F_defI;
|
|
41 |
|
|
42 |
Delsimps [setrcos_def];
|
|
43 |
|
|
44 |
(* MAIN PROOF *)
|
|
45 |
Goal "F \\<in> Group";
|
|
46 |
val l1 = H_normal RS normal_imp_subgroup ;
|
|
47 |
val l2 = l1 RS subgroup_imp_subset;
|
|
48 |
by (stac F_defI 1);
|
|
49 |
by (rtac GroupI 1);
|
|
50 |
(* 1. *)
|
|
51 |
by (afs [restrictI, setprod_closed] 1);
|
|
52 |
(* 2. *)
|
|
53 |
by (afs [restrictI, setinv_closed] 1);
|
|
54 |
(* 3. H\\<in>{* H *} *)
|
|
55 |
by (rtac (l1 RS setrcos_unit_closed) 1);
|
|
56 |
(* 4. inverse property *)
|
|
57 |
by (simp_tac (simpset() addsimps [setinv_closed, setrcos_inv_prod_eq]) 1);
|
|
58 |
(* 5. unit property *)
|
|
59 |
by (simp_tac (simpset() addsimps [normal_imp_subgroup,
|
|
60 |
setrcos_unit_closed, setrcos_prod_eq]) 1);
|
|
61 |
(* 6. associativity *)
|
|
62 |
by (asm_simp_tac
|
|
63 |
(simpset() addsimps [setprod_closed, H_normal RS setrcos_prod_assoc]) 1);
|
|
64 |
qed "factorgroup_is_group";
|
|
65 |
val FactorGroup_is_Group = export factorgroup_is_group;
|
|
66 |
|
|
67 |
|
|
68 |
Delsimps [H_normal, F_def];
|
|
69 |
Close_locale "factgroup";
|
|
70 |
|
|
71 |
|
|
72 |
Goalw [FactGroup_def] "FactGroup \\<in> (PI G: Group. {H. H <| G} \\<rightarrow> Group)";
|
|
73 |
by (rtac restrictI 1);
|
|
74 |
by (rtac restrictI 1);
|
|
75 |
by (asm_full_simp_tac
|
|
76 |
(simpset() addsimps [F_DefI RS sym, FactorGroup_is_Group]) 1);
|
|
77 |
qed "FactGroup_arity";
|
|
78 |
|
|
79 |
Close_locale "coset";
|
|
80 |
Close_locale "group";
|