author paulson Mon Jul 23 17:37:29 2001 +0200 (2001-07-23) changeset 11443 77ed7e2b56c8 parent 11442 8682a88c3d6a child 11444 b24017251fc1
The final version of Florian Kammueller's proofs
 src/HOL/GroupTheory/Coset.ML file | annotate | diff | revisions src/HOL/GroupTheory/DirProd.ML file | annotate | diff | revisions src/HOL/GroupTheory/Group.ML file | annotate | diff | revisions src/HOL/GroupTheory/PiSets.ML file | annotate | diff | revisions src/HOL/GroupTheory/PiSets.thy file | annotate | diff | revisions src/HOL/GroupTheory/README.html file | annotate | diff | revisions src/HOL/GroupTheory/ROOT.ML file | annotate | diff | revisions src/HOL/GroupTheory/Sylow.ML file | annotate | diff | revisions src/HOL/GroupTheory/Sylow.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/GroupTheory/Coset.ML	Mon Jul 23 13:50:23 2001 +0200
1.2 +++ b/src/HOL/GroupTheory/Coset.ML	Mon Jul 23 17:37:29 2001 +0200
1.3 @@ -24,6 +24,7 @@
1.4
1.5
1.6  Open_locale "coset";
1.8
1.9  val rcos_def = thm "rcos_def";
1.10  val lcos_def = thm "lcos_def";
1.11 @@ -282,8 +283,10 @@
1.12
1.13  Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
1.14  \ ==> (H <#> (H #> x)) #> y = H #> (x ## y)";
1.15 -by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,r_coset_subset_G,
1.16 -         coset_mul_assoc, setprod_subset_G,normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,normal_imp_subgroup] 1);
1.17 +by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,
1.18 +         r_coset_subset_G, coset_mul_assoc, setprod_subset_G,
1.19 +         normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,
1.20 +         normal_imp_subgroup] 1);
1.21  qed "rcos_prod_step3";
1.22
1.23  Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
1.24 @@ -299,7 +302,6 @@
1.25                                    rcos_prod, setrcos_eq]));
1.26  qed "setprod_closed";
1.27
1.28 -
1.29  Goal "[| H <| G; H1 \\<in> {*H*} |] ==> I(H1) \\<in> {*H*}";
1.30  by (auto_tac (claset(),
1.31                simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
1.32 @@ -312,6 +314,32 @@
1.33            addSIs [subgroup_e_closed, e_closed, coset_join2 RS sym]) 1);
1.34  qed "setrcos_unit_closed";
1.35
1.36 +Goal "[|H <| G; M \\<in> {*H*}|] ==> I M <#> M = H";
1.37 +by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
1.38 +by (Clarify_tac 1);
1.39 +by (asm_simp_tac
1.40 +    (simpset() addsimps [rcos_inv, rcos_prod, normal_imp_subgroup,
1.41 +                         subgroup_imp_subset, coset_mul_e]) 1);
1.42 +qed "setrcos_inv_prod_eq";
1.43 +
1.44 +(*generalizes subgroup_prod_id*)
1.45 +Goal "[|H <| G; M \\<in> {*H*}|] ==> H <#> M = M";
1.46 +by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
1.47 +by (Clarify_tac 1);
1.48 +by (asm_simp_tac
1.49 +    (simpset() addsimps [normal_imp_subgroup, subgroup_imp_subset,
1.50 +                         setprod_rcos_assoc, subgroup_prod_id]) 1);
1.51 +qed "setrcos_prod_eq";
1.52 +
1.53 +Goal "[|H <| G; M1 \\<in> {*H*}; M2 \\<in> {*H*}; M3 \\<in> {*H*}|]  \
1.54 +\     ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)";
1.55 +by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
1.56 +by (Clarify_tac 1);
1.57 +by (asm_simp_tac
1.58 +    (simpset() addsimps [rcos_prod, normal_imp_subgroup,
1.59 +                         subgroup_imp_subset, binop_assoc]) 1);
1.60 +qed "setrcos_prod_assoc";
1.61 +
1.62
1.63  (**** back to Sylow again, i.e. direction Lagrange ****)
1.64
```
```     2.1 --- a/src/HOL/GroupTheory/DirProd.ML	Mon Jul 23 13:50:23 2001 +0200
2.2 +++ b/src/HOL/GroupTheory/DirProd.ML	Mon Jul 23 17:37:29 2001 +0200
2.3 @@ -82,7 +82,7 @@
2.4  qed "prodgroup_is_group";
2.5  val ProdGroup_is_Group = export prodgroup_is_group;
2.6
2.7 -Delsimps [Group_G', Group_G];
2.8 +Delsimps [P_def, Group_G', Group_G];
2.9
2.10  Close_locale "prodgroup";
2.11  Close_locale "r_group";
```
```     3.1 --- a/src/HOL/GroupTheory/Group.ML	Mon Jul 23 13:50:23 2001 +0200
3.2 +++ b/src/HOL/GroupTheory/Group.ML	Mon Jul 23 17:37:29 2001 +0200
3.3 @@ -204,4 +204,20 @@
3.4
3.5  val Abel_imp_Group = Abel_subset_Group RS subsetD;
3.6
3.7 +Delsimps [simp_G, Group_G];
3.8  Close_locale "group";
3.9 +
3.10 +Goal "G \\<in> Group ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
3.11 +\                unit = G .<e> |) \\<in> Group";
3.12 +by (blast_tac
3.13 +    (claset() addIs [GroupI, export binop_funcset, export inv_funcset, export e_closed, export inv_ax2, export e_ax1, export binop_assoc]) 1);
3.14 +qed "Group_Group";
3.15 +
3.16 +Goal "G \\<in> AbelianGroup \
3.17 +\     ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
3.18 +\            unit = G .<e> |) \\<in> AbelianGroup";
3.19 +by (asm_full_simp_tac (simpset() addsimps [AbelianGroup_def]) 1);
3.20 +by (rtac Group_Group 1);
3.21 +by Auto_tac;
3.22 +qed "Abel_Abel";
3.23 +
```
```     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/GroupTheory/PiSets.ML	Mon Jul 23 17:37:29 2001 +0200
4.3 @@ -0,0 +1,66 @@
4.4 +(*  Title:      HOL/ex/PiSets.ML
4.5 +    ID:         \$Id\$
4.6 +    Author:     Florian Kammueller, University of Cambridge
4.7 +
4.8 +Pi sets and their application.
4.9 +*)
4.10 +
4.11 +(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
4.12 +Goal "f \\<in> Pi A B ==> PiBij A B f <= Sigma A B";
4.13 +by (auto_tac (claset(), simpset() addsimps [PiBij_def,Pi_def]));
4.14 +qed "PiBij_subset_Sigma";
4.15 +
4.16 +Goal "f \\<in> Pi A B ==> \\<forall>x \\<in> A. \\<exists>!y. (x, y) \\<in> (PiBij A B f)";
4.17 +by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
4.18 +qed "PiBij_unique";
4.19 +
4.20 +Goal "f \\<in> Pi A B ==> PiBij A B f \\<in> Graph A B";
4.21 +by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
4.22 +				      PiBij_subset_Sigma]) 1);
4.23 +qed "PiBij_in_Graph";
4.24 +
4.25 +Goalw [PiBij_def, Graph_def] "PiBij A B \\<in> Pi A B \\<rightarrow> Graph A B";
4.26 +by (rtac restrictI 1);
4.27 +by (auto_tac (claset(), simpset() addsimps [Pi_def]));
4.28 +qed "PiBij_func";
4.29 +
4.30 +Goal "inj_on (PiBij A B) (Pi A B)";
4.31 +by (rtac inj_onI 1);
4.32 +by (rtac Pi_extensionality 1);
4.33 +by (assume_tac 1);
4.34 +by (assume_tac 1);
4.35 +by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
4.36 +by (Blast_tac 1);
4.37 +qed "inj_PiBij";
4.38 +
4.39 +
4.40 +Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
4.41 +by (rtac restrictI 1);
4.42 +by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1);
4.43 + by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
4.44 +by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
4.45 +by (stac some_equality 1);
4.46 +  by (assume_tac 1);
4.47 + by (Blast_tac 1);
4.48 +by (Blast_tac 1);
4.49 +qed "in_Graph_imp_in_Pi";
4.50 +
4.51 +Goal "PiBij A B ` (Pi A B) = Graph A B";
4.52 +by (rtac equalityI 1);
4.53 +by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
4.54 +by (rtac subsetI 1);
4.55 +by (rtac image_eqI 1);
4.56 +by (etac in_Graph_imp_in_Pi 2);
4.57 +(* x = PiBij A B (lam a:A. @ y. (a, y)\\<in>x) *)
4.58 +by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
4.59 +by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def]));
4.60 +by (fast_tac (claset() addIs [someI2]) 1);
4.61 +qed "surj_PiBij";
4.62 +
4.63 +Goal "f \\<in> Pi A B ==> Inv (Pi A B) (PiBij A B) (PiBij A B f) = f";
4.64 +by (asm_simp_tac (simpset() addsimps [Inv_f_f, inj_PiBij]) 1);
4.65 +qed "PiBij_bij1";
4.66 +
4.67 +Goal "f \\<in> Graph A B ==> PiBij A B (Inv (Pi A B) (PiBij A B) f) = f";
4.68 +by (asm_simp_tac (simpset() addsimps [f_Inv_f, surj_PiBij]) 1);
4.69 +qed "PiBij_bij2";
```
```     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/GroupTheory/PiSets.thy	Mon Jul 23 17:37:29 2001 +0200
5.3 @@ -0,0 +1,18 @@
5.4 +(*  Title:      HOL/ex/PiSets.thy
5.5 +    ID:         \$Id\$
5.6 +    Author:     Florian Kammueller, University of Cambridge
5.7 +
5.8 +The bijection between elements of the Pi set and functional graphs
5.9 +*)
5.10 +
5.11 +PiSets = Group +
5.12 +
5.13 +constdefs
5.14 +(* bijection between Pi_sig and Pi_=> *)
5.15 +  PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
5.16 +    "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
5.17 +
5.18 +  Graph ::  "['a set, 'a => 'b set] => ('a * 'b) set set"
5.19 +   "Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}"
5.20 +
5.21 +end
```
```     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/GroupTheory/README.html	Mon Jul 23 17:37:29 2001 +0200
6.3 @@ -0,0 +1,48 @@
6.4 +<!-- \$Id\$ -->
6.6 +
6.7 +<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
6.8 +
6.9 +<P>This directory presents proofs about group theory, by
6.10 +Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
6.11 +These theories use locales and were indeed the original motivation for
6.12 +locales.  However, this treatment of groups must still be regarded as
6.13 +experimental.  We can expect to see refinements in the future.
6.14 +
6.15 +Here is an outline of the directory's contents:
6.16 +
6.17 +<UL>
6.18 +<LI>Theory <A HREF="Bij.thy"><CODE>Bij</CODE></A>
6.19 +defines bijections over sets and operations on them and shows that they
6.20 +are a group.
6.21 +
6.22 +<LI>Theory <A HREF="DirProd.thy"><CODE>DirProd</CODE></A>
6.23 +defines the product of two groups and proves that it is a group again.
6.24 +
6.25 +<LI>Theory <A HREF="FactGroup.thy"><CODE>FactGroup</CODE></A>
6.26 +defines the factorization of a group and shows that the factorization a
6.27 +normal subgroup is a group.
6.28 +
6.29 +<LI>Theory <A HREF="Homomorphism.thy"><CODE>Homomorphism</CODE></A>
6.30 +defines homomorphims and automorphisms for groups and rings and shows that
6.31 +ring automorphisms are a group by using the previous result for
6.32 +bijections.
6.33 +
6.34 +<LI>Theory <A HREF="Ring.thy"><CODE>Ring</CODE></A>
6.35 +and <A HREF="RingConstr.thy"><CODE>RingConstr</CODE></A>
6.36 +defines rings, proves a few basic theorems and constructs a lambda
6.37 +function to extract the group that is part of the ring showing that it is
6.38 +an abelian group.
6.39 +
6.40 +<LI>Theory <A HREF="Sylow.thy"><CODE>Sylow</CODE></A>
6.41 +contains a proof of the first Sylow theorem.
6.42 +
6.43 +</UL>
6.44 +
6.45 +<HR>
6.47 +
6.49 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
6.51 +</BODY></HTML>
```
```     7.1 --- a/src/HOL/GroupTheory/ROOT.ML	Mon Jul 23 13:50:23 2001 +0200
7.2 +++ b/src/HOL/GroupTheory/ROOT.ML	Mon Jul 23 17:37:29 2001 +0200
7.3 @@ -3,3 +3,5 @@
7.4
7.5  use_thy "DirProd";
7.6  use_thy "Sylow";
7.7 +use_thy "RingConstr";
7.8 +use_thy "PiSets";
```
```     8.1 --- a/src/HOL/GroupTheory/Sylow.ML	Mon Jul 23 13:50:23 2001 +0200
8.2 +++ b/src/HOL/GroupTheory/Sylow.ML	Mon Jul 23 17:37:29 2001 +0200
8.3 @@ -4,6 +4,11 @@
8.4      Copyright   1998-2001  University of Cambridge
8.5
8.6  Sylow's theorem using locales (combinatorial argument in Exponent.thy)
8.7 +
8.8 +See Florian Kamm\"uller and L. C. Paulson,
8.9 +    A Formal Proof of Sylow's theorem:
8.10 +	An Experiment in Abstract Algebra with Isabelle HOL
8.11 +    J. Automated Reasoning 23 (1999), 235-264
8.12  *)
8.13
8.14  Open_locale "sylow";
```
```     9.1 --- a/src/HOL/GroupTheory/Sylow.thy	Mon Jul 23 13:50:23 2001 +0200
9.2 +++ b/src/HOL/GroupTheory/Sylow.thy	Mon Jul 23 17:37:29 2001 +0200
9.3 @@ -4,6 +4,11 @@
9.4      Copyright   1998-2001  University of Cambridge
9.5
9.6  Sylow's theorem using locales (combinatorial argument in Exponent.thy)
9.7 +
9.8 +See Florian Kamm\"uller and L. C. Paulson,
9.9 +    A Formal Proof of Sylow's theorem:
9.10 +	An Experiment in Abstract Algebra with Isabelle HOL
9.11 +    J. Automated Reasoning 23 (1999), 235-264
9.12  *)
9.13
9.14  Sylow =  Coset +
```