|
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"; |