# HG changeset patch
# User paulson
# Date 995902649 -7200
# Node ID 77ed7e2b56c8c0b661fb27719b22e1a32f1cac2f
# Parent  8682a88c3d6aa5974c278db89c833d6a6cfa47bb
The final version of Florian Kammueller's proofs

diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/Coset.ML
--- 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 ****)
 
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/DirProd.ML
--- 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";
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/Group.ML
--- 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";
+
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/PiSets.ML
--- /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";
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/PiSets.thy
--- /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
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/README.html
--- /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>
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/ROOT.ML
--- 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";
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/Sylow.ML
--- 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";
diff -r 8682a88c3d6a -r 77ed7e2b56c8 src/HOL/GroupTheory/Sylow.thy
--- 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 +