--- a/src/HOL/GroupTheory/Coset.ML Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/Coset.ML Mon Jul 23 17:37:29 2001 +0200
@@ -24,6 +24,7 @@
Open_locale "coset";
+Addsimps [Group_G, simp_G];
val rcos_def = thm "rcos_def";
val lcos_def = thm "lcos_def";
@@ -282,8 +283,10 @@
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
\ ==> (H <#> (H #> x)) #> y = H #> (x ## y)";
-by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,r_coset_subset_G,
- coset_mul_assoc, setprod_subset_G,normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,normal_imp_subgroup] 1);
+by (afs [setprod_rcos_assoc,normal_imp_subgroup RS subgroup_imp_subset,
+ r_coset_subset_G, coset_mul_assoc, setprod_subset_G,
+ normal_imp_subgroup RS subgroup_imp_subset,subgroup_prod_id,
+ normal_imp_subgroup] 1);
qed "rcos_prod_step3";
Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
@@ -299,7 +302,6 @@
rcos_prod, setrcos_eq]));
qed "setprod_closed";
-
Goal "[| H <| G; H1 \\<in> {*H*} |] ==> I(H1) \\<in> {*H*}";
by (auto_tac (claset(),
simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset,
@@ -312,6 +314,32 @@
addSIs [subgroup_e_closed, e_closed, coset_join2 RS sym]) 1);
qed "setrcos_unit_closed";
+Goal "[|H <| G; M \\<in> {*H*}|] ==> I M <#> M = H";
+by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
+by (Clarify_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps [rcos_inv, rcos_prod, normal_imp_subgroup,
+ subgroup_imp_subset, coset_mul_e]) 1);
+qed "setrcos_inv_prod_eq";
+
+(*generalizes subgroup_prod_id*)
+Goal "[|H <| G; M \\<in> {*H*}|] ==> H <#> M = M";
+by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
+by (Clarify_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps [normal_imp_subgroup, subgroup_imp_subset,
+ setprod_rcos_assoc, subgroup_prod_id]) 1);
+qed "setrcos_prod_eq";
+
+Goal "[|H <| G; M1 \\<in> {*H*}; M2 \\<in> {*H*}; M3 \\<in> {*H*}|] \
+\ ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)";
+by (asm_full_simp_tac (simpset() addsimps [setrcos_eq]) 1);
+by (Clarify_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps [rcos_prod, normal_imp_subgroup,
+ subgroup_imp_subset, binop_assoc]) 1);
+qed "setrcos_prod_assoc";
+
(**** back to Sylow again, i.e. direction Lagrange ****)
--- a/src/HOL/GroupTheory/DirProd.ML Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/DirProd.ML Mon Jul 23 17:37:29 2001 +0200
@@ -82,7 +82,7 @@
qed "prodgroup_is_group";
val ProdGroup_is_Group = export prodgroup_is_group;
-Delsimps [Group_G', Group_G];
+Delsimps [P_def, Group_G', Group_G];
Close_locale "prodgroup";
Close_locale "r_group";
--- a/src/HOL/GroupTheory/Group.ML Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/Group.ML Mon Jul 23 17:37:29 2001 +0200
@@ -204,4 +204,20 @@
val Abel_imp_Group = Abel_subset_Group RS subsetD;
+Delsimps [simp_G, Group_G];
Close_locale "group";
+
+Goal "G \\<in> Group ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
+\ unit = G .<e> |) \\<in> Group";
+by (blast_tac
+ (claset() addIs [GroupI, export binop_funcset, export inv_funcset, export e_closed, export inv_ax2, export e_ax1, export binop_assoc]) 1);
+qed "Group_Group";
+
+Goal "G \\<in> AbelianGroup \
+\ ==> (| carrier = G .<cr>, bin_op = G .<f>, inverse = G .<inv>,\
+\ unit = G .<e> |) \\<in> AbelianGroup";
+by (asm_full_simp_tac (simpset() addsimps [AbelianGroup_def]) 1);
+by (rtac Group_Group 1);
+by Auto_tac;
+qed "Abel_Abel";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/PiSets.ML Mon Jul 23 17:37:29 2001 +0200
@@ -0,0 +1,66 @@
+(* Title: HOL/ex/PiSets.ML
+ ID: $Id$
+ Author: Florian Kammueller, University of Cambridge
+
+Pi sets and their application.
+*)
+
+(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
+Goal "f \\<in> Pi A B ==> PiBij A B f <= Sigma A B";
+by (auto_tac (claset(), simpset() addsimps [PiBij_def,Pi_def]));
+qed "PiBij_subset_Sigma";
+
+Goal "f \\<in> Pi A B ==> \\<forall>x \\<in> A. \\<exists>!y. (x, y) \\<in> (PiBij A B f)";
+by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
+qed "PiBij_unique";
+
+Goal "f \\<in> Pi A B ==> PiBij A B f \\<in> Graph A B";
+by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
+ PiBij_subset_Sigma]) 1);
+qed "PiBij_in_Graph";
+
+Goalw [PiBij_def, Graph_def] "PiBij A B \\<in> Pi A B \\<rightarrow> Graph A B";
+by (rtac restrictI 1);
+by (auto_tac (claset(), simpset() addsimps [Pi_def]));
+qed "PiBij_func";
+
+Goal "inj_on (PiBij A B) (Pi A B)";
+by (rtac inj_onI 1);
+by (rtac Pi_extensionality 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
+by (Blast_tac 1);
+qed "inj_PiBij";
+
+
+Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
+by (rtac restrictI 1);
+by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1);
+ by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
+by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
+by (stac some_equality 1);
+ by (assume_tac 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
+qed "in_Graph_imp_in_Pi";
+
+Goal "PiBij A B ` (Pi A B) = Graph A B";
+by (rtac equalityI 1);
+by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
+by (rtac subsetI 1);
+by (rtac image_eqI 1);
+by (etac in_Graph_imp_in_Pi 2);
+(* x = PiBij A B (lam a:A. @ y. (a, y)\\<in>x) *)
+by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
+by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def]));
+by (fast_tac (claset() addIs [someI2]) 1);
+qed "surj_PiBij";
+
+Goal "f \\<in> Pi A B ==> Inv (Pi A B) (PiBij A B) (PiBij A B f) = f";
+by (asm_simp_tac (simpset() addsimps [Inv_f_f, inj_PiBij]) 1);
+qed "PiBij_bij1";
+
+Goal "f \\<in> Graph A B ==> PiBij A B (Inv (Pi A B) (PiBij A B) f) = f";
+by (asm_simp_tac (simpset() addsimps [f_Inv_f, surj_PiBij]) 1);
+qed "PiBij_bij2";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/PiSets.thy Mon Jul 23 17:37:29 2001 +0200
@@ -0,0 +1,18 @@
+(* Title: HOL/ex/PiSets.thy
+ ID: $Id$
+ Author: Florian Kammueller, University of Cambridge
+
+The bijection between elements of the Pi set and functional graphs
+*)
+
+PiSets = Group +
+
+constdefs
+(* bijection between Pi_sig and Pi_=> *)
+ PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
+ "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
+
+ Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
+ "Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/README.html Mon Jul 23 17:37:29 2001 +0200
@@ -0,0 +1,48 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
+
+<P>This directory presents proofs about group theory, by
+Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.)
+These theories use locales and were indeed the original motivation for
+locales. However, this treatment of groups must still be regarded as
+experimental. We can expect to see refinements in the future.
+
+Here is an outline of the directory's contents:
+
+<UL>
+<LI>Theory <A HREF="Bij.thy"><CODE>Bij</CODE></A>
+defines bijections over sets and operations on them and shows that they
+are a group.
+
+<LI>Theory <A HREF="DirProd.thy"><CODE>DirProd</CODE></A>
+defines the product of two groups and proves that it is a group again.
+
+<LI>Theory <A HREF="FactGroup.thy"><CODE>FactGroup</CODE></A>
+defines the factorization of a group and shows that the factorization a
+normal subgroup is a group.
+
+<LI>Theory <A HREF="Homomorphism.thy"><CODE>Homomorphism</CODE></A>
+defines homomorphims and automorphisms for groups and rings and shows that
+ring automorphisms are a group by using the previous result for
+bijections.
+
+<LI>Theory <A HREF="Ring.thy"><CODE>Ring</CODE></A>
+and <A HREF="RingConstr.thy"><CODE>RingConstr</CODE></A>
+defines rings, proves a few basic theorems and constructs a lambda
+function to extract the group that is part of the ring showing that it is
+an abelian group.
+
+<LI>Theory <A HREF="Sylow.thy"><CODE>Sylow</CODE></A>
+contains a proof of the first Sylow theorem.
+
+</UL>
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
--- a/src/HOL/GroupTheory/ROOT.ML Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/ROOT.ML Mon Jul 23 17:37:29 2001 +0200
@@ -3,3 +3,5 @@
use_thy "DirProd";
use_thy "Sylow";
+use_thy "RingConstr";
+use_thy "PiSets";
--- a/src/HOL/GroupTheory/Sylow.ML Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML Mon Jul 23 17:37:29 2001 +0200
@@ -4,6 +4,11 @@
Copyright 1998-2001 University of Cambridge
Sylow's theorem using locales (combinatorial argument in Exponent.thy)
+
+See Florian Kamm\"uller and L. C. Paulson,
+ A Formal Proof of Sylow's theorem:
+ An Experiment in Abstract Algebra with Isabelle HOL
+ J. Automated Reasoning 23 (1999), 235-264
*)
Open_locale "sylow";
--- a/src/HOL/GroupTheory/Sylow.thy Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Mon Jul 23 17:37:29 2001 +0200
@@ -4,6 +4,11 @@
Copyright 1998-2001 University of Cambridge
Sylow's theorem using locales (combinatorial argument in Exponent.thy)
+
+See Florian Kamm\"uller and L. C. Paulson,
+ A Formal Proof of Sylow's theorem:
+ An Experiment in Abstract Algebra with Isabelle HOL
+ J. Automated Reasoning 23 (1999), 235-264
*)
Sylow = Coset +