diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/GroupTheory/Coset.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Coset.ML	Tue Jul 03 15:28:24 2001 +0200
@@ -0,0 +1,394 @@
+(*  Title:      HOL/GroupTheory/Coset
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Copyright   1998-2001  University of Cambridge
+
+Theory of cosets, using locales
+*)
+
+(** these versions are useful for Sylow's Theorem **)
+
+Goal "[|finite A; finite B; \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A|] ==> card(A) <= card(B)";
+by (Clarify_tac 1); 
+by (rtac card_inj_on_le 1);
+by (auto_tac (claset(), simpset() addsimps [Pi_def])); 
+qed "card_inj";
+
+Goal "[| finite A;  finite B;  \\<exists>f \\<in> A\\<rightarrow>B. inj_on f A;  \
+\        \\<exists>g \\<in> B\\<rightarrow>A. inj_on g B |] ==> card(A) = card(B)";
+by (Clarify_tac 1); 
+by (rtac card_bij_eq 1);
+by (auto_tac (claset(), simpset() addsimps [Pi_def])); 
+qed "card_bij";
+
+
+
+Open_locale "coset";
+
+val rcos_def = thm "rcos_def";
+val lcos_def = thm "lcos_def";
+val setprod_def = thm "setprod_def";
+val setinv_def = thm "setinv_def";
+val setrcos_def = thm "setrcos_def";
+
+val group_defs = [thm "binop_def", thm "inv_def", thm "e_def"];
+val coset_defs = [thm "rcos_def", thm "lcos_def", thm "setprod_def"];
+
+(** Alternative definitions, reducing to locale constants **)
+
+Goal "H #> a = {b . \\<exists>h\\<in>H. h ## a = b}";
+by (auto_tac (claset(),
+              simpset() addsimps [rcos_def, r_coset_def, binop_def])); 
+qed "r_coset_eq";
+
+Goal "a <# H = {b . \\<exists>h\\<in>H. a ## h = b}";
+by (auto_tac (claset(),
+              simpset() addsimps [lcos_def, l_coset_def, binop_def])); 
+qed "l_coset_eq";
+
+Goal "{*H*} = {C . \\<exists>a\\<in>carrier G. C = H #> a}";
+by (auto_tac (claset(),
+     simpset() addsimps [set_r_cos_def, setrcos_def, rcos_def, binop_def])); 
+qed "setrcos_eq";
+
+Goal "H <#> K = {c . \\<exists>h\\<in>H. \\<exists>k\\<in>K. c = h ## k}";
+by (simp_tac
+    (simpset() addsimps [setprod_def, set_prod_def, binop_def, image_def]) 1); 
+qed "set_prod_eq";
+
+Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
+\     ==> (M #> g) #> h = M #> (g ## h)";
+by (force_tac (claset(), simpset() addsimps [r_coset_eq, binop_assoc]) 1); 
+qed "coset_mul_assoc";
+
+Goal "[| M <= carrier G |] ==> M #> e = M";
+by (force_tac (claset(), simpset() addsimps [r_coset_eq]) 1); 
+qed "coset_mul_e";
+
+Goal "[| M #> (x ## (i y)) = M;  x \\<in> carrier G ; y \\<in> carrier G;\
+\        M <= carrier G |] ==> M #> x = M #> y";
+by (eres_inst_tac [("P","%z. M #> x = z #> y")] subst 1);
+by (asm_simp_tac (simpset() addsimps [coset_mul_assoc, binop_assoc]) 1); 
+qed "coset_mul_inv1";
+
+Goal "[| M #> x = M #> y;  x \\<in> carrier G;  y \\<in> carrier G;  M <= carrier G |] \
+\     ==> M #> (x ## (i y)) = M ";
+by (afs [coset_mul_assoc RS sym] 1);
+by (afs [coset_mul_assoc, coset_mul_e] 1);
+qed "coset_mul_invers2";
+
+Goal "[| H #> x = H;  x \\<in> carrier G;  H <<= G |] ==> x\\<in>H";
+by (etac subst 1);
+by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
+by (blast_tac (claset() addIs [e_ax1, subgroup_e_closed]) 1); 
+qed "coset_join1";
+
+Goal "[| x\\<in>carrier G;  H <<= G;  x\\<in>H |] ==> H #> x = H";
+by (auto_tac (claset(), simpset() addsimps [r_coset_eq])); 
+by (res_inst_tac [("x","xa ## (i x)")] bexI 2);
+by (auto_tac (claset(), 
+     simpset() addsimps [subgroup_f_closed, subgroup_inv_closed,
+                         binop_assoc, subgroup_imp_subset RS subsetD]));
+qed "coset_join2";
+
+Goal "[| H <= carrier G; x\\<in>carrier G |] ==> H #> x <= carrier G";
+by (auto_tac (claset(), simpset() addsimps [r_coset_eq])); 
+qed "r_coset_subset_G";
+
+Goal "[| h \\<in> H; H <= carrier G; x \\<in> carrier G|] ==> h ## x \\<in> H #> x";
+by (auto_tac (claset(), simpset() addsimps [r_coset_eq])); 
+qed "rcosI";
+
+Goal "[| H <= carrier G; x \\<in> carrier G |] ==> H #> x \\<in> {*H*}";
+by (auto_tac (claset(), simpset() addsimps [setrcos_eq])); 
+qed "setrcosI";
+
+
+Goal "[| x ## y = z;  x \\<in> carrier G;  y \\<in> carrier G;  z\\<in>carrier G |] \
+\     ==> (i x) ## z = y";
+by (Clarify_tac 1); 
+by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1); 
+qed "transpose_inv";
+
+
+Goal "[| y \\<in> H #> x;  x \\<in> carrier G; H <<= G |] ==> H #> x = H #> y";
+by (auto_tac (claset(), 
+	    simpset() addsimps [r_coset_eq, binop_assoc RS sym,
+				right_cancellation_iff, subgroup_imp_subset RS subsetD,
+				subgroup_f_closed])); 
+by (res_inst_tac [("x","ha ## i h")] bexI 1);  
+by (auto_tac (claset(), 
+         simpset() addsimps [binop_assoc, subgroup_imp_subset RS subsetD, 
+                             subgroup_inv_closed, subgroup_f_closed])); 
+qed "repr_independence";
+
+Goal "[| x \\<in> carrier G; H <<= G |] ==> x \\<in> H #> x";
+by (simp_tac (simpset() addsimps [r_coset_eq]) 1);
+by (blast_tac (claset() addIs [e_ax1, subgroup_imp_subset RS subsetD, 
+                               subgroup_e_closed]) 1);  
+qed "rcos_self";
+
+Goal "setinv H = INV`H";
+by (simp_tac
+    (simpset() addsimps [image_def, setinv_def, set_inv_def, inv_def]) 1); 
+qed "setinv_eq_image_inv";
+
+
+(*** normal subgroups ***)
+
+Goal "(H <| G) = (H <<= G & (\\<forall>x \\<in> carrier G. H #> x = x <# H))";
+by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
+qed "normal_iff";
+
+Goal "H <| G ==> H <<= G";
+by (afs [normal_def] 1);
+qed "normal_imp_subgroup";
+
+Goal "[| H <| G; x \\<in> carrier G |] ==> H #> x = x <# H";
+by (afs [thm "lcos_def", thm "rcos_def", normal_def] 1);
+qed "normal_imp_rcos_eq_lcos";
+
+Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> i x ## h ## x \\<in> H";
+by (auto_tac (claset(), 
+              simpset() addsimps [l_coset_eq, r_coset_eq, normal_iff]));
+by (ball_tac 1);
+by (dtac (equalityD1 RS subsetD) 1); 
+by (Blast_tac 1); 
+by (Clarify_tac 1); 
+by (etac subst 1); 
+by (asm_simp_tac
+    (simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD]) 1); 
+qed "normal_inv_op_closed1";
+
+Goal "\\<lbrakk>H \\<lhd> G; x \\<in> (G .<cr>); h \\<in> H\\<rbrakk> \\<Longrightarrow> x ## h ## i x \\<in> H";
+by (dres_inst_tac [("x","i x")] normal_inv_op_closed1 1); 
+by Auto_tac; 
+qed "normal_inv_op_closed2";
+
+Goal "[| M <= carrier G; g\\<in>carrier G; h\\<in>carrier G |] \
+\                 ==> g <# (h <# M) = (g ## h) <# M";
+by (force_tac (claset(), simpset() addsimps [l_coset_eq, binop_assoc]) 1); 
+qed "lcos_mul_assoc";
+
+Goal "M <= carrier G ==> e <# M = M";
+by (force_tac (claset(), simpset() addsimps [l_coset_eq]) 1); 
+qed "lcos_mul_e";
+
+Goal "[| H <= carrier G; x\\<in>carrier G |]\
+\           ==> x <# H <= carrier G";
+by (auto_tac (claset(), simpset() addsimps [l_coset_eq, subsetD])); 
+qed "lcosetGaH_subset_G";
+
+Goal "[| y \\<in> x <# H;  x \\<in> carrier G;  H <<= G |] ==> x <# H = y <# H";
+by (auto_tac (claset(), 
+              simpset() addsimps [l_coset_eq, binop_assoc,
+                                  left_cancellation_iff, subgroup_imp_subset RS subsetD,
+                                  subgroup_f_closed])); 
+by (res_inst_tac [("x","i h ## ha")] bexI 1);  
+by (auto_tac (claset(), 
+         simpset() addsimps [binop_assoc RS sym, subgroup_imp_subset RS subsetD, 
+                             subgroup_inv_closed, subgroup_f_closed])); 
+qed "l_repr_independence";
+
+Goal "[| H1 <= carrier G; H2 <= carrier G |] ==> H1 <#> H2 <= carrier G";
+by (auto_tac (claset(), simpset() addsimps [set_prod_eq, subsetD])); 
+qed "setprod_subset_G";
+val set_prod_subset_G = export setprod_subset_G;
+
+Goal "H <<= G ==> H <#> H = H";
+by (auto_tac (claset(), 
+       simpset() addsimps [set_prod_eq, Sigma_def,image_def])); 
+by (res_inst_tac [("x","x")] bexI 2);
+by (res_inst_tac [("x","e")] bexI 2);
+by (auto_tac (claset(), 
+              simpset() addsimps [subgroup_f_closed, subgroup_e_closed, e_ax2,
+                                  subgroup_imp_subset RS subsetD])); 
+qed "subgroup_prod_id";
+val Subgroup_prod_id = export subgroup_prod_id;
+
+
+(* set of inverses of an r_coset *)
+Goal "[| H <| G; x \\<in> carrier G |] ==> I(H #> x) = H #>(i x)";
+by (ftac normal_imp_subgroup 1); 
+by (auto_tac (claset(), 
+       simpset() addsimps [r_coset_eq, setinv_eq_image_inv, image_def]));
+by (res_inst_tac [("x","i x ## i h ## x")] bexI 1);  
+by (asm_simp_tac (simpset() addsimps [binop_assoc, inv_prod, 
+                                      subgroup_imp_subset RS subsetD]) 1); 
+by (res_inst_tac [("x","i(h ## i x)")] exI 2);
+by (asm_simp_tac (simpset() addsimps [inv_inv, inv_prod, 
+                           subgroup_imp_subset RS subsetD]) 2); 
+by (res_inst_tac [("x","x ## i h ## i x")] bexI 2);  
+by (auto_tac (claset(), 
+         simpset() addsimps [normal_inv_op_closed1, normal_inv_op_closed2, 
+                             binop_assoc, subgroup_imp_subset RS subsetD, 
+                             subgroup_inv_closed])); 
+qed "rcos_inv";
+val r_coset_inv = export rcos_inv;
+
+Goal "[| H <| G; H1\\<in>{*H*}; x \\<in> H1 |] ==> I(H1) = H #> (i x)";
+by (afs [setrcos_eq] 1);
+by (Clarify_tac 1); 
+by (subgoal_tac "x : carrier G" 1);
+ by (rtac subsetD 2);
+ by (assume_tac 3);
+ by (asm_full_simp_tac (simpset() addsimps [r_coset_subset_G,
+                                    subgroup_imp_subset,normal_imp_subgroup]) 2);
+by (dtac repr_independence 1);
+  by (assume_tac 1);
+ by (etac normal_imp_subgroup 1);
+by (asm_simp_tac (simpset() addsimps [rcos_inv]) 1);  
+qed "rcos_inv2";
+val r_coset_inv2 = export rcos_inv2;
+
+
+
+(* some rules for <#> with #> or <# *)
+Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
+\ ==> H1 <#> (H2 #> x) = (H1 <#> H2) #> x";
+by (auto_tac (claset(), 
+       simpset() addsimps [rcos_def, r_coset_def, 
+                         setprod_def, set_prod_def, Sigma_def,image_def])); 
+by (auto_tac (claset() addSIs [bexI,exI], 
+               simpset() addsimps [binop_assoc, subsetD]));  
+qed "setprod_rcos_assoc";
+val set_prod_r_coset_assoc = export setprod_rcos_assoc;
+
+Goal "[| H1 <= carrier G; H2 <= carrier G; x \\<in> carrier G |]\
+\ ==> (H1 #> x) <#> H2 = H1 <#> (x <# H2)";
+by (asm_simp_tac
+    (simpset() addsimps [rcos_def, r_coset_def, lcos_def, l_coset_def, 
+                         setprod_def, set_prod_def, Sigma_def,image_def]) 1); 
+by (force_tac (claset() addSIs [bexI,exI], 
+               simpset() addsimps [binop_assoc, subsetD]) 1);  
+qed "rcos_prod_assoc_lcos";
+val rcoset_prod_assoc_lcoset = export rcos_prod_assoc_lcos;
+
+
+(* product of rcosets *)
+(* To show H x H y = H x y. which is done by
+   H x H y =1= H (x H) y =2= H (H x) y =3= H H x y =4= H x y *)
+
+Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
+\ ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y";
+by (afs [setprod_rcos_assoc, normal_imp_subgroup RS subgroup_imp_subset, r_coset_subset_G, 
+         lcosetGaH_subset_G, rcos_prod_assoc_lcos] 1); 
+qed "rcos_prod_step1";
+
+Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
+\ ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y";
+by (afs [normal_imp_rcos_eq_lcos] 1);
+qed "rcos_prod_step2";
+
+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);
+qed "rcos_prod_step3";
+
+Goal "[| H <| G; x \\<in> carrier G; y \\<in> carrier G |]\
+\     ==> (H #> x) <#> (H #> y) = H #> (x ## y)";
+by (afs [rcos_prod_step1,rcos_prod_step2,rcos_prod_step3] 1);
+qed "rcos_prod";
+val rcoset_prod = export rcos_prod;
+
+(* operations on cosets *)
+Goal "[| H <| G; H1 \\<in> {*H*}; H2 \\<in> {*H*} |] ==> H1 <#> H2 \\<in> {*H*}";
+by (auto_tac (claset(), 
+              simpset() addsimps [normal_imp_subgroup RS subgroup_imp_subset, 
+                                  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, 
+                                  rcos_inv, setrcos_eq]));
+qed "setinv_closed";
+
+Goal "H <<= G ==> H \\<in> {*H*}";
+by (simp_tac (simpset() addsimps [setrcos_eq]) 1); 
+by (blast_tac (claset() delrules [equalityI]
+          addSIs [subgroup_e_closed, e_closed, coset_join2 RS sym]) 1);
+qed "setrcos_unit_closed";
+
+
+(**** back to Sylow again, i.e. direction Lagrange ****)
+
+(* Theorems necessary for Lagrange *)
+
+Goal "H <<= G ==> \\<Union> {*H*} = carrier G";
+by (rtac equalityI 1);
+by (force_tac (claset(), 
+    simpset() addsimps [subgroup_imp_subset RS subsetD, setrcos_eq, r_coset_eq]) 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [setrcos_eq, subgroup_imp_subset, rcos_self])); 
+qed "setrcos_part_G";
+
+Goal "[| c \\<in> {*H*};  H <= carrier G;  finite (carrier G) |] ==> finite c";
+by (auto_tac (claset(), simpset() addsimps [setrcos_eq])); 
+by (asm_simp_tac (simpset() addsimps [r_coset_subset_G RS finite_subset]) 1);
+qed "cosets_finite";
+
+Goal "[| c \\<in> {*H*};  H <= carrier G; finite(carrier G) |] ==> card c = card H";
+by (auto_tac (claset(), simpset() addsimps [setrcos_eq])); 
+by (res_inst_tac [("f", "%y. y ## i a"), ("g","%y. y ## a")] card_bij_eq 1);
+by (afs [r_coset_subset_G RS finite_subset] 1);
+by (blast_tac (claset() addIs [finite_subset]) 1); 
+(* injective maps *)
+   by (blast_tac (claset() addIs [restrictI, rcosI]) 3);
+  by (force_tac (claset(), 
+      simpset() addsimps [inj_on_def, right_cancellation_iff, subsetD]) 3);
+(*now for f*)
+ by (force_tac (claset(),
+                simpset() addsimps [binop_assoc, subsetD, r_coset_eq]) 1); 
+(* injective *)
+by (rtac inj_onI 1); 
+by (subgoal_tac "x \\<in> carrier G & y \\<in> carrier G" 1);
+ by (blast_tac (claset() addIs [r_coset_subset_G RS subsetD]) 2);
+by (rotate_tac ~1 1); 
+by (asm_full_simp_tac
+    (simpset() addsimps [right_cancellation_iff, subsetD]) 1); 
+qed "card_cosets_equal";
+
+
+(** Two distinct right cosets are disjoint **)
+
+Goal "[|H <<= G;  a \\<in> (G .<cr>);  b \\<in> (G .<cr>);  ha ## a = h ## b;  \
+\       h \\<in> H;  ha \\<in> H;  hb \\<in> H|] \
+\     ==> \\<exists>h\\<in>H. h ## b = hb ## a";
+by (res_inst_tac [("x","hb ## ((i ha) ## h)")] bexI 1);
+by (afs [subgroup_f_closed, subgroup_inv_closed] 2);
+by (asm_simp_tac (simpset() addsimps [binop_assoc, left_cancellation_iff, 
+            transpose_inv, subgroup_imp_subset RS subsetD]) 1);
+qed "rcos_equation";
+
+Goal "[|H <<= G; c1 \\<in> {*H*}; c2 \\<in> {*H*}; c1 \\<noteq> c2|] ==> c1 \\<inter> c2 = {}";
+by (asm_full_simp_tac (simpset() addsimps [setrcos_eq, r_coset_eq]) 1); 
+by (blast_tac (claset() addIs [rcos_equation, sym]) 1); 
+qed "rcos_disjoint";
+
+Goal "H <<= G  ==> {*H*} <= Pow(carrier G)";
+by (simp_tac (simpset() addsimps [setrcos_eq]) 1); 
+by (blast_tac (claset() addDs [r_coset_subset_G,subgroup_imp_subset]) 1); 
+qed "setrcos_subset_PowG";
+
+Goal "[| finite(carrier G); H <<= G |]\
+\     ==> card({*H*}) * card(H) = order(G)";
+by (asm_simp_tac (simpset() addsimps [order_def, setrcos_part_G RS sym]) 1); 
+by (stac mult_commute 1);
+by (rtac card_partition 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [setrcos_subset_PowG RS finite_subset]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [setrcos_part_G]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [card_cosets_equal, subgroup_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [rcos_disjoint, subgroup_def]) 1); 
+qed "lagrange";
+val Lagrange = export lagrange;
+
+Close_locale "coset";
+Close_locale "group";
+
+
+