The final version of Florian Kammueller's proofs
authorpaulson
Mon Jul 23 17:37:29 2001 +0200 (2001-07-23)
changeset 1144377ed7e2b56c8
parent 11442 8682a88c3d6a
child 11444 b24017251fc1
The final version of Florian Kammueller's proofs
src/HOL/GroupTheory/Coset.ML
src/HOL/GroupTheory/DirProd.ML
src/HOL/GroupTheory/Group.ML
src/HOL/GroupTheory/PiSets.ML
src/HOL/GroupTheory/PiSets.thy
src/HOL/GroupTheory/README.html
src/HOL/GroupTheory/ROOT.ML
src/HOL/GroupTheory/Sylow.ML
src/HOL/GroupTheory/Sylow.thy
     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.7 +Addsimps [Group_G, simp_G];
     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.5 +<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
     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.46 +<P>Last modified on $Date$
    6.47 +
    6.48 +<ADDRESS>
    6.49 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    6.50 +</ADDRESS>
    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 +