--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Bij.ML Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,171 @@
+(* Title: HOL/GroupTheory/Bij
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Bijections of a set and the group of bijections
+ Sigma version with locales
+*)
+
+Addsimps [Id_compose, compose_Id];
+
+(*Inv_f_f should suffice, only here A=B=S so the equality remains.*)
+Goalw [Inv_def]
+ "[| f`A = B; x : B |] ==> Inv A f x : A";
+by (Clarify_tac 1);
+by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
+qed "Inv_mem";
+
+Open_locale "bij";
+
+val B_def = thm "B_def";
+val o'_def = thm "o'_def";
+val inv'_def = thm "inv'_def";
+val e'_def = thm "e'_def";
+
+Addsimps [B_def, o'_def, inv'_def];
+
+Goal "f \\<in> B ==> f \\<in> S \\<rightarrow> S";
+by (afs [Bij_def] 1);
+qed "BijE1";
+
+Goal "f \\<in> B ==> f ` S = S";
+by (afs [Bij_def] 1);
+qed "BijE2";
+
+Goal "f \\<in> B ==> inj_on f S";
+by (afs [Bij_def] 1);
+qed "BijE3";
+
+Goal "[| f \\<in> S \\<rightarrow> S; f ` S = S; inj_on f S |] ==> f \\<in> B";
+by (afs [Bij_def] 1);
+qed "BijI";
+
+Delsimps [B_def];
+Addsimps [BijE1,BijE2,BijE3];
+
+
+(* restrict (Inv S f) S *)
+Goal "f \\<in> B ==> (lam x: S. (inv' f) x) \\<in> B";
+by (rtac BijI 1);
+(* 1. (lam x: S. (inv' f) x): S \\<rightarrow> S *)
+by (afs [Inv_funcset] 1);
+(* 2. (lam x: S. (inv' f) x) ` S = S *)
+by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1);
+by (rtac equalityI 1);
+(* 2. <= *)
+by (Clarify_tac 1);
+by (afs [Inv_mem, BijE2] 1);
+(* 2. => *)
+by (rtac subsetI 1);
+by (res_inst_tac [("x","f x")] image_eqI 1);
+by (asm_simp_tac (simpset() addsimps [Inv_f_f, BijE1 RS funcset_mem]) 1);
+by (asm_simp_tac (simpset() addsimps [BijE1 RS funcset_mem]) 1);
+(* 3. *)
+by (rtac inj_onI 1);
+by (auto_tac (claset() addEs [Inv_injective], simpset()));
+qed "restrict_Inv_Bij";
+
+Addsimps [e'_def];
+
+Goal "e'\\<in>B ";
+by (rtac BijI 1);
+by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def]));
+qed "restrict_id_Bij";
+
+Goal "f \\<in> B ==> (lam g: B. lam x: S. (inv' g) x) f = (lam x: S. (inv' f) x)";
+by (Asm_full_simp_tac 1);
+qed "eval_restrict_Inv";
+
+Goal "[| x \\<in> B; y \\<in> B|] ==> x o' y \\<in> B";
+by (simp_tac (simpset() addsimps [o'_def]) 1);
+by (rtac BijI 1);
+by (blast_tac (claset() addIs [funcset_compose] addDs [BijE1,BijE2,BijE3]) 1);
+by (blast_tac (claset() delrules [equalityI]
+ addIs [surj_compose] addDs [BijE1,BijE2,BijE3]) 1);
+by (blast_tac (claset() addIs [inj_on_compose] addDs [BijE1,BijE2,BijE3]) 1);
+qed "compose_Bij";
+
+
+
+(**** Bijections form a group ****)
+
+
+Open_locale "bijgroup";
+
+val BG_def = thm "BG_def";
+
+Goal "[| x\\<in>B; y\\<in>B |] ==> (lam g: B. lam f: B. g o' f) x y = x o' y";
+by (Asm_full_simp_tac 1);
+qed "eval_restrict_comp2";
+
+
+Addsimps [BG_def, B_def, o'_def, inv'_def,e'_def];
+
+Goal "carrier BG == B";
+by (afs [BijGroup_def] 1);
+qed "BG_carrier";
+
+Goal "bin_op BG == lam g: B. lam f: B. g o' f";
+by (afs [BijGroup_def] 1);
+qed "BG_bin_op";
+
+Goal "inverse BG == lam f: B. lam x: S. (inv' f) x";
+by (afs [BijGroup_def] 1);
+qed "BG_inverse";
+
+Goal "unit BG == e'";
+by (afs [BijGroup_def] 1);
+qed "BG_unit";
+
+Goal "BG = (| carrier = BG.<cr>, bin_op = BG.<f>,\
+\ inverse = BG.<inv>, unit = BG.<e> |)";
+by (afs [BijGroup_def,BG_carrier, BG_bin_op, BG_inverse, BG_unit] 1);
+qed "BG_defI";
+
+Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
+
+
+Goal "(lam g: B. lam f: B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
+by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1);
+qed "restrict_compose_Bij";
+
+
+Goal "BG \\<in> Group";
+by (stac BG_defI 1);
+by (rtac GroupI 1);
+(* 1. (BG .<f>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) \\<rightarrow> (BG .<cr>) *)
+by (afs [BG_bin_op, BG_carrier, restrict_compose_Bij] 1);
+(* 2: (BG .<inv>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) *)
+by (simp_tac (simpset() addsimps [BG_inverse, BG_carrier, restrict_Inv_Bij,
+ funcsetI]) 1);
+by (afs [BG_inverse, BG_carrier,eval_restrict_Inv, restrict_Inv_Bij] 1);
+(* 3. *)
+by (afs [BG_carrier, BG_unit, restrict_id_Bij] 1);
+(* Now the equalities *)
+(* 4. ! x:BG .<cr>. (BG .<f>) ((BG .<inv>) x) x = (BG .<e>) *)
+by (simp_tac
+ (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
+ e'_def, compose_Inv_id, inv'_def, o'_def]) 1);
+by (simp_tac
+ (simpset() addsimps [symmetric (inv'_def), restrict_Inv_Bij]) 1);
+(* 5: ! x:BG .<cr>. (BG .<f>) (BG .<e>) x = x *)
+by (simp_tac
+ (simpset() addsimps [BG_carrier, BG_unit, BG_bin_op,
+ e'_def, o'_def]) 1);
+by (simp_tac
+ (simpset() addsimps [symmetric (e'_def), restrict_id_Bij]) 1);
+(* 6. ! x:BG .<cr>.
+ ! y:BG .<cr>.
+ ! z:BG .<cr>.
+ (BG .<f>) ((BG .<f>) x y) z = (BG .<f>) x ((BG .<f>) y z) *)
+by (simp_tac
+ (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
+ compose_Bij]) 1);
+by (simp_tac (simpset() addsimps [o'_def]) 1);
+by (blast_tac (claset() addIs [compose_assoc RS sym, BijE1]) 1);
+qed "Bij_are_Group";
+
+Close_locale "bijgroup";
+Close_locale "bij";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Bij.thy Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,42 @@
+(* Title: HOL/GroupTheory/Coset
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Bijections of a set and the group of bijections
+ Sigma version with locales
+*)
+
+Bij = Group +
+
+constdefs
+ Bij :: "'a set => (('a => 'a)set)"
+ "Bij S == {f. f \\<in> S \\<rightarrow> S & f`S = S & inj_on f S}"
+
+constdefs
+BijGroup :: "'a set => (('a => 'a) grouptype)"
+"BijGroup S == (| carrier = Bij S,
+ bin_op = lam g: Bij S. lam f: Bij S. compose S g f,
+ inverse = lam f: Bij S. lam x: S. (Inv S f) x,
+ unit = lam x: S. x |)"
+
+locale bij =
+ fixes
+ S :: "'a set"
+ B :: "('a => 'a)set"
+ comp :: "[('a => 'a),('a => 'a)]=>('a => 'a)" (infixr "o''" 80)
+ inv' :: "('a => 'a)=>('a => 'a)"
+ e' :: "('a => 'a)"
+ defines
+ B_def "B == Bij S"
+ o'_def "g o' f == compose S g f"
+ inv'_def "inv' f == Inv S f"
+ e'_def "e' == (lam x: S. x)"
+
+locale bijgroup = bij +
+ fixes
+ BG :: "('a => 'a) grouptype"
+ defines
+ BG_def "BG == BijGroup S"
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/FactGroup.ML Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,80 @@
+(* Title: HOL/GroupTheory/FactGroup
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Factorization of a group
+*)
+
+
+Open_locale "factgroup";
+
+val H_normal = thm "H_normal";
+val F_def = thm "F_def";
+
+Addsimps [H_normal, F_def,setrcos_def];
+
+Goal "carrier F = {* H *}";
+by (afs [FactGroup_def] 1);
+qed "F_carrier";
+
+Goal "bin_op F = (lam X: {* H *}. lam Y: {* H *}. X <#> Y) ";
+by (afs [FactGroup_def, setprod_def] 1);
+qed "F_bin_op";
+
+Goal "inverse F = (lam X: {* H *}. I(X))";
+by (afs [FactGroup_def, setinv_def] 1);
+qed "F_inverse";
+
+Goal "unit F = H";
+by (afs [FactGroup_def] 1);
+qed "F_unit";
+
+Goal "F = (| carrier = {* H *}, \
+\ bin_op = (lam X: {* H *}. lam Y: {* H *}. X <#> Y), \
+\ inverse = (lam X: {* H *}. I(X)), unit = H |)";
+by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
+by (auto_tac (claset() addSIs [restrict_ext],
+ simpset() addsimps [set_prod_def, setprod_def, setinv_def]));
+qed "F_defI";
+val F_DefI = export F_defI;
+
+Delsimps [setrcos_def];
+
+(* MAIN PROOF *)
+Goal "F \\<in> Group";
+val l1 = H_normal RS normal_imp_subgroup ;
+val l2 = l1 RS subgroup_imp_subset;
+by (stac F_defI 1);
+by (rtac GroupI 1);
+(* 1. *)
+by (afs [restrictI, setprod_closed] 1);
+(* 2. *)
+by (afs [restrictI, setinv_closed] 1);
+(* 3. H\\<in>{* H *} *)
+by (rtac (l1 RS setrcos_unit_closed) 1);
+(* 4. inverse property *)
+by (simp_tac (simpset() addsimps [setinv_closed, setrcos_inv_prod_eq]) 1);
+(* 5. unit property *)
+by (simp_tac (simpset() addsimps [normal_imp_subgroup,
+ setrcos_unit_closed, setrcos_prod_eq]) 1);
+(* 6. associativity *)
+by (asm_simp_tac
+ (simpset() addsimps [setprod_closed, H_normal RS setrcos_prod_assoc]) 1);
+qed "factorgroup_is_group";
+val FactorGroup_is_Group = export factorgroup_is_group;
+
+
+Delsimps [H_normal, F_def];
+Close_locale "factgroup";
+
+
+Goalw [FactGroup_def] "FactGroup \\<in> (PI G: Group. {H. H <| G} \\<rightarrow> Group)";
+by (rtac restrictI 1);
+by (rtac restrictI 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [F_DefI RS sym, FactorGroup_is_Group]) 1);
+qed "FactGroup_arity";
+
+Close_locale "coset";
+Close_locale "group";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/FactGroup.thy Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,38 @@
+(* Title: HOL/GroupTheory/FactGroup
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Factorization of a group
+*)
+
+FactGroup = Coset +
+
+constdefs
+ FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
+
+ "FactGroup ==
+ lam G: Group. lam H: {H. H <| G}.
+ (| carrier = set_r_cos G H,
+ bin_op = (lam X: set_r_cos G H. lam Y: set_r_cos G H. set_prod G X Y),
+ inverse = (lam X: set_r_cos G H. set_inv G X),
+ unit = H |)"
+
+syntax
+ "@Fact" :: "['a grouptype, 'a set] => ('a set) grouptype"
+ ("_ Mod _" [60,61]60)
+
+translations
+ "G Mod H" == "FactGroup G H"
+
+locale factgroup = coset +
+fixes
+ F :: "('a set) grouptype"
+ H :: "('a set)"
+assumes
+ H_normal "H <| G"
+defines
+ F_def "F == FactGroup G H"
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Homomorphism.ML Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,267 @@
+(* Title: HOL/GroupTheory/Homomorphism
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Homomorphisms of groups, rings, and automorphisms.
+Sigma version with Locales
+*)
+
+Open_locale "bij";
+
+Addsimps [B_def, o'_def, inv'_def];
+
+Goal "[|x \\<in> S; f \\<in> B|] ==> EX x'. x = f x'";
+by (dtac BijE2 1);
+by Auto_tac;
+
+
+Goal "[| f \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S;\
+\ \\<forall>x \\<in> S. \\<forall>y \\<in> S. f(g x y) = g (f x) (f y) |] \
+\ ==> inv' f (g x y) = g (inv' f x) (inv' f y)";
+by (subgoal_tac "EX x':S. EX y':S. x = f x' & y = f y'" 1);
+by (blast_tac (claset() addDs [BijE2]) 2);
+by (Clarify_tac 1);
+(*the next step could be avoided if we could re-orient the quanitifed
+ assumption, to rewrite g (f x') (f y') ...*)
+by (rtac inj_onD 1);
+by (etac BijE3 1);
+by (asm_full_simp_tac (simpset() addsimps [f_Inv_f, Inv_f_f, BijE2, BijE3,
+ funcset_mem RS funcset_mem]) 1);
+by (ALLGOALS
+ (asm_full_simp_tac
+ (simpset() addsimps [funcset_mem RS funcset_mem, BijE2, Inv_mem])));
+qed "Bij_op_lemma";
+
+Goal "[| a \\<in> B; b \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S; \
+\ \\<forall>x \\<in> S. \\<forall>y \\<in> S. a (b (g x y)) = g (a (b x)) (a (b y)) |] \
+\ ==> (a o' b) (g x y) = g ((a o' b) x) ((a o' b) y)";
+by (afs [o'_def, compose_eq, B_def,
+ funcset_mem RS funcset_mem] 1);
+qed "Bij_comp_lemma";
+
+
+Goal "[| R1 \\<in> Ring; R2 \\<in> Ring |] \
+\ ==> RingHom `` {R1} `` {R2} = \
+\ {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) & \
+\ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
+\ (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &\
+\ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
+\ (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}";
+by (afs [Image_def,RingHom_def] 1);
+qed "RingHom_apply";
+
+(* derive the defining properties as single lemmas *)
+Goal "(R1,R2,Phi) \\<in> RingHom ==> Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>)";
+by (afs [RingHom_def] 1);
+qed "RingHom_imp_funcset";
+
+Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \
+\ ==> Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y)";
+by (afs [RingHom_def] 1);
+qed "RingHom_preserves_rplus";
+
+Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \
+\ ==> Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)";
+by (afs [RingHom_def] 1);
+qed "RingHom_preserves_rmult";
+
+Goal "[| R1 \\<in> Ring; R2 \\<in> Ring; Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>); \
+\ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
+\ Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y);\
+\ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
+\ Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)|]\
+\ ==> (R1,R2,Phi) \\<in> RingHom";
+by (afs [RingHom_def] 1);
+qed "RingHomI";
+
+Open_locale "ring";
+
+val Ring_R = thm "Ring_R";
+val rmult_def = thm "rmult_def";
+
+Addsimps [simp_R, Ring_R];
+
+
+
+(* RingAutomorphisms *)
+Goal "RingAuto `` {R} = \
+\ {Phi. (R,R,Phi) \\<in> RingHom & inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}";
+by (rewtac RingAuto_def);
+by (afs [Image_def] 1);
+qed "RingAuto_apply";
+
+Goal "(R,Phi) \\<in> RingAuto ==> (R, R, Phi) \\<in> RingHom";
+by (afs [RingAuto_def] 1);
+qed "RingAuto_imp_RingHom";
+
+Goal "(R,Phi) \\<in> RingAuto ==> inj_on Phi (R.<cr>)";
+by (afs [RingAuto_def] 1);
+qed "RingAuto_imp_inj_on";
+
+Goal "(R,Phi) \\<in> RingAuto ==> Phi ` (R.<cr>) = (R.<cr>)";
+by (afs [RingAuto_def] 1);
+qed "RingAuto_imp_preserves_R";
+
+Goal "(R,Phi) \\<in> RingAuto ==> Phi \\<in> (R.<cr>) \\<rightarrow> (R.<cr>)";
+by (etac (RingAuto_imp_RingHom RS RingHom_imp_funcset) 1);
+qed "RingAuto_imp_funcset";
+
+Goal "[| (R,R,Phi) \\<in> RingHom; \
+\ inj_on Phi (R.<cr>); \
+\ Phi ` (R.<cr>) = (R.<cr>) |]\
+\ ==> (R,Phi) \\<in> RingAuto";
+by (afs [RingAuto_def] 1);
+qed "RingAutoI";
+
+
+(* major result: RingAutomorphism builds a group *)
+(* We prove that they are a subgroup of the bijection group.
+ Note!!! Here we need "RingAuto `` {R} ~= {}", (as a result from the
+ resolution with subgroupI). That is, this is an example where one might say
+ the discipline of Pi types pays off, because there we have the proof basically
+ already there (compare the Pi-version).
+ Here in the Sigma version, we have to redo now the proofs (or slightly
+ adapted verisions) of promoteRingHom and promoteRingAuto *)
+
+Goal "RingAuto `` {R} ~= {}";
+by (stac RingAuto_apply 1);
+by Auto_tac;
+by (res_inst_tac [("x","lam y: (R.<cr>). y")] exI 1);
+by (auto_tac (claset(), simpset() addsimps [inj_on_def]));
+by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI,
+ R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1);
+qed "RingAutoEx";
+
+Goal "(R,f) \\<in> RingAuto ==> f \\<in> Bij (R.<cr>)";
+by (afs [RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on,
+ RingAuto_imp_preserves_R, export BijI] 1);
+qed "RingAuto_Bij";
+Addsimps [RingAuto_Bij];
+
+Goal "[| (R,a) \\<in> RingAuto; (R,b) \\<in> RingAuto; \
+\ g \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>); x \\<in> carrier R; y \\<in> carrier R; \
+\ \\<forall>Phi. (R,Phi) \\<in> RingAuto --> \
+\ (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). Phi(g x y) = g(Phi x) (Phi y)) |] \
+\ ==> compose (R.<cr>) a b (g x y) = \
+\ g (compose (R.<cr>) a b x) (compose (R.<cr>) a b y)";
+by (asm_simp_tac (simpset() addsimps [export Bij_comp_lemma,
+ RingAuto_imp_funcset RS funcset_mem]) 1);
+qed "Auto_comp_lemma";
+
+Goal "[|(R, a) \\<in> RingAuto; x \\<in> carrier R; y \\<in> carrier R|] \
+\ ==> Inv (carrier R) a (x ## y) = \
+\ Inv (carrier R) a x ## Inv (carrier R) a y";
+by (rtac (export Bij_op_lemma) 1);
+by (etac RingAuto_Bij 1);
+by (rtac rplus_funcset 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [R_binop_def RS sym,
+ RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1);
+qed "Inv_rplus_lemma";
+
+Goal "(R,a) \\<in> RingAuto \
+\ ==> (R, grouptype.inverse (BijGroup (carrier R)) a) \\<in> RingAuto";
+by (rtac RingAutoI 1);
+by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE3)] 2);
+by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE2)] 2);
+by (rtac RingHomI 1);
+by (rtac (Ring_R) 1);
+by (rtac (Ring_R) 1);
+(* ... ==> (BijGroup (R .<R>) .<inv>) a \\<in> (R .<R>) \\<rightarrow> (R .<R>) *)
+by (asm_simp_tac (simpset() addsimps [BijGroup_def,
+ export restrict_Inv_Bij RS export BijE1]) 1);
+by (asm_simp_tac (simpset() addsimps [BijGroup_def, R_binop_def, rplus_closed, Inv_rplus_lemma]) 1);
+by (afs [BijGroup_def, symmetric (rmult_def), rmult_closed] 1);
+by (afs [export Bij_op_lemma, rmult_funcset, rmult_def,
+ RingAuto_imp_RingHom RS RingHom_preserves_rmult] 1);
+qed "inverse_BijGroup_lemma";
+
+Goal "[|(R, a) \\<in> RingAuto; (R, b) \\<in> RingAuto|] \
+\ ==> (R, bin_op (BijGroup (carrier R)) a b) \\<in> RingAuto";
+by (afs [BijGroup_def] 1);
+by (rtac RingAutoI 1);
+by (rtac RingHomI 1);
+by (rtac (Ring_R) 1);
+by (rtac (Ring_R) 1);
+by (afs [RingAuto_Bij,export compose_Bij,export BijE1] 1);
+by (Clarify_tac 1);
+by (rtac Auto_comp_lemma 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (asm_full_simp_tac (simpset() addsimps [R_binop_def, rplus_funcset]) 1);
+by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1);
+by (Clarify_tac 1);
+by (rtac Auto_comp_lemma 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [rmult_funcset]) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rmult]) 1);
+(* ==> inj_on (compose (R .<R>) a b) (R .<R>) *)
+by (blast_tac (claset() delrules [equalityI]
+ addIs [inj_on_compose, RingAuto_imp_inj_on,
+ RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1);
+(* ==> compose (R .<R>) a b ` (R .<R>) = (R .<R>) *)
+by (blast_tac (claset() delrules [equalityI]
+ addIs [surj_compose, RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1);
+qed "binop_BijGroup_lemma";
+
+
+(* Ring automorphisms are a subgroup of the group of bijections over the
+ ring's carrier, and thus a group *)
+Goal "RingAuto `` {R} <<= BijGroup (R.<cr>)";
+by (rtac SubgroupI 1);
+by (rtac (export Bij_are_Group) 1);
+(* 1. RingAuto `` {R} <= (BijGroup (R .<R>) .<cr>) *)
+by (afs [subset_def, BijGroup_def, Bij_def,
+ RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on,
+ RingAuto_imp_preserves_R, Image_def] 1);
+(* 1. !!R. R \\<in> Ring ==> RingAuto `` {R} ~= {} *)
+by (rtac RingAutoEx 1);
+by (auto_tac (claset(),
+ simpset() addsimps [inverse_BijGroup_lemma, binop_BijGroup_lemma]));
+qed "RingAuto_SG_BijGroup";
+
+Delsimps [simp_R, Ring_R];
+
+Close_locale "ring";
+Close_locale "group";
+
+val RingAuto_are_Group = (export RingAuto_SG_BijGroup) RS (export Bij_are_Group RS SubgroupE2);
+(* So far:
+"[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |]
+ ==> (| carrier = RingAuto `` {?R2},
+ bin_op =
+ lam x:RingAuto `` {?R2}.
+ restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}),
+ inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}),
+ unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *)
+
+(* Unfortunately we have to eliminate the extra assumptions
+Now only group_of R \\<in> Group *)
+
+Goal "R \\<in> Ring ==> group_of R \\<in> Group";
+by (asm_full_simp_tac (simpset() addsimps [group_of_def]) 1);
+by (rtac Abel_imp_Group 1);
+by (etac (export R_Abel) 1);
+qed "R_Group";
+
+Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\
+\ bin_op = lam x:RingAuto `` {R}. lam y: RingAuto `` {R}.\
+\ (BijGroup (R.<cr>) .<f>) x y ,\
+\ inverse = lam x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
+\ unit = BijGroup (R.<cr>) .<e> |) \\<in> Group";
+by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "RingAuto_are_Groupf";
+
+(* "?R \\<in> Ring
+ ==> (| carrier = RingAuto `` {?R},
+ bin_op =
+ lam x:RingAuto `` {?R}.
+ restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}),
+ inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}),
+ unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Homomorphism.thy Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,40 @@
+(* Title: HOL/GroupTheory/Homomorphism
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Homomorphisms of groups, rings, and automorphisms.
+Sigma version with Locales
+*)
+
+Homomorphism = Ring + Bij +
+
+consts
+ Hom :: "('a grouptype * 'b grouptype * ('a => 'b)) set"
+
+defs
+ Hom_def "Hom == \\<Sigma>G \\<in> Group. \\<Sigma>H \\<in> Group. {Phi. Phi \\<in> (G.<cr>) \\<rightarrow> (H.<cr>) &
+ (\\<forall>x \\<in> (G.<cr>) . \\<forall>y \\<in> (G.<cr>) . (Phi((G.<f>) x y) = (H.<f>) (Phi x)(Phi y)))}"
+
+consts
+ RingHom :: "(('a ringtype) * ('b ringtype) * ('a => 'b))set"
+defs
+ RingHom_def "RingHom == \\<Sigma>R1 \\<in> Ring. \\<Sigma>R2 \\<in> Ring. {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) &
+ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &
+ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}"
+
+consts
+ GroupAuto :: "('a grouptype * ('a => 'a)) set"
+
+defs
+ GroupAuto_def "GroupAuto == \\<Sigma>G \\<in> Group. {Phi. (G,G,Phi)\\<in>Hom &
+ inj_on Phi (G.<cr>) & Phi ` (G.<cr>) = (G.<cr>)}"
+
+consts
+ RingAuto :: "(('a ringtype) * ('a => 'a))set"
+
+defs
+ RingAuto_def "RingAuto == \\<Sigma>R \\<in> Ring. {Phi. (R,R,Phi)\\<in>RingHom &
+ inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Ring.ML Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,138 @@
+(* Title: HOL/GroupTheory/Ring
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Ring theory. Sigma version
+*)
+
+Goal
+"[| (| carrier = carrier R, bin_op = R .<f>, \
+\ inverse = R .<inv>, unit = R .<e> |) \\<in> AbelianGroup;\
+\ (R.<m>) \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R); \
+\ \\<forall>x \\<in> carrier R. \\<forall>y \\<in> carrier R. \\<forall>z \\<in> carrier R. (R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z;\
+\ distr_l (carrier R)(R.<m>)(R.<f>); distr_r (carrier R)(R.<m>)(R.<f>) |]\
+\ ==> R \\<in> Ring";
+by (afs [Ring_def] 1);
+qed "RingI";
+
+Open_locale "ring";
+
+val simp_R = simplify (simpset() addsimps [Ring_def]) (thm "Ring_R");
+
+Addsimps [simp_R, thm "Ring_R", thm "rmult_def",thm "R_id_G"];
+
+Goal "(| carrier = (carrier R), bin_op = (R.<f>), inverse = (R.<inv>), \
+\ unit = (R.<e>) |) \\<in> AbelianGroup";
+by (Asm_full_simp_tac 1);
+qed "R_Abel";
+
+Goal "group_of R \\<in> AbelianGroup";
+by (afs [group_of_def] 1);
+qed "R_forget";
+
+Goal "((group_of R).<cr>) = (carrier R)";
+by (afs [group_of_def] 1);
+qed "FR_carrier";
+
+Goal "(G.<cr>) = (carrier R)";
+by (simp_tac (simpset() addsimps [FR_carrier RS sym]) 1);
+qed "R_carrier_def";
+
+Goal "((group_of R).<f>) = op ##";
+by (afs [binop_def, thm "R_id_G"] 1);
+qed "FR_bin_op";
+
+Goal "(R.<f>) = op ##";
+by (afs [FR_bin_op RS sym, group_of_def] 1);
+qed "R_binop_def";
+
+Goal "((group_of R).<inv>) = INV";
+by (afs [thm "inv_def"] 1);
+qed "FR_inverse";
+
+Goal "(R.<inv>) = INV";
+by (afs [FR_inverse RS sym, group_of_def] 1);
+qed "R_inv_def";
+
+Goal "((group_of R).<e>) = e";
+by (afs [thm "e_def"] 1);
+qed "FR_unit";
+
+Goal "(R.<e>) = e";
+by (afs [FR_unit RS sym, group_of_def] 1);
+qed "R_unit_def";
+
+Goal "G \\<in> AbelianGroup";
+by (afs [group_of_def] 1);
+qed "G_abelian";
+
+
+Delsimps [thm "R_id_G"]; (*needed below?*)
+
+Goal "[| x \\<in> (G.<cr>); y \\<in> (G.<cr>) |] ==> x ## y = y ## x";
+by (afs [thm "binop_def", G_abelian RS Group_commute] 1);
+qed "binop_commute";
+
+Goal "op ** \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R)";
+by (simp_tac (simpset() addsimps [thm "rmult_def"]) 1);
+qed "rmult_funcset";
+
+Goal "[| x \\<in> (carrier R); y \\<in> (carrier R) |] ==> x ** y \\<in> (carrier R)";
+by (blast_tac
+ (claset() addIs [rmult_funcset RS funcset_mem RS funcset_mem]) 1);
+qed "rmult_closed";
+
+Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
+\ ==> x **(y ** z) = (x ** y)** z";
+by (Asm_full_simp_tac 1);
+qed "rmult_assoc";
+
+Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
+\ ==> x **(y ## z) = (x ** y) ## (x ** z)";
+by (cut_facts_tac [thm "Ring_R"] 1);
+by (asm_full_simp_tac (simpset() delsimps [thm "Ring_R", simp_R]
+ addsimps [Ring_def, distr_l_def, R_binop_def]) 1);
+qed "R_distrib1";
+
+
+(* The following have been in the earlier version without locales and the
+record extension proofs in which we needed to use conversion functions to
+establish these facts. We can transfer all facts that are
+derived for groups to rings now. The subsequent proofs are not really hard
+proofs, they are just instantiations of the known facts to rings. This is
+because the elements of the ring and the group are now identified!! Before, in
+the older version we could do something similar, but we always had to go the
+longer way, via the implication R \\<in> Ring ==> R \\<in> Abelian group and then
+conversion functions for the operators *)
+
+Goal "e \\<in> carrier R";
+by (afs [R_carrier_def RS sym,e_closed] 1);
+qed "R_e_closed";
+
+Goal "\\<forall>x \\<in> carrier R. e ## x = x";
+by (afs [R_carrier_def RS sym,e_ax1] 1);
+qed "R_e_ax1";
+
+Goal "op ## \\<in> carrier R \\<rightarrow> carrier R \\<rightarrow> carrier R";
+by (afs [R_carrier_def RS sym, binop_funcset] 1);
+qed "rplus_funcset";
+
+Goal "[| x \\<in> carrier R; y \\<in> carrier R |] ==> x ## y \\<in> carrier R";
+by (afs [rplus_funcset RS funcset_mem RS funcset_mem] 1);
+qed "rplus_closed";
+
+Goal "[| a \\<in> carrier R; a ## a = a |] ==> a = e";
+by (afs [ R_carrier_def RS sym, idempotent_e] 1);
+qed "R_idempotent_e";
+
+Delsimps [simp_R, thm "Ring_R", thm "rmult_def", thm "R_id_G"];
+
+Goal "e ** e = e";
+by (rtac R_idempotent_e 1);
+by (blast_tac (claset() addIs [rmult_closed, R_e_closed]) 1);
+by (simp_tac (simpset() addsimps [R_distrib1 RS sym, R_e_closed]) 1);
+qed "R_e_mult_base";
+
+Close_locale "ring";
+Close_locale "group";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Ring.thy Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,60 @@
+(* Title: HOL/GroupTheory/Bij
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Ring theory. Sigma version
+*)
+
+Ring = Coset +
+
+record 'a ringtype = 'a grouptype +
+ Rmult :: "['a, 'a] => 'a"
+
+syntax
+ "@Rmult" :: "('a ringtype) => (['a, 'a] => 'a)" ("_ .<m>" [10] 10)
+
+translations
+ "R.<m>" == "Rmult R"
+
+constdefs
+ distr_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+ "distr_l S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S.
+ (f1 x (f2 y z) = f2 (f1 x y) (f1 x z)))"
+ distr_r :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+ "distr_r S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S.
+ (f1 (f2 y z) x = f2 (f1 y x) (f1 z x)))"
+
+consts
+ Ring :: "('a ringtype) set"
+
+defs
+ Ring_def
+ "Ring ==
+ {R. (| carrier = (R.<cr>), bin_op = (R.<f>),
+ inverse = (R.<inv>), unit = (R.<e>) |) \\<in> AbelianGroup &
+ (R.<m>) \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>) &
+ (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
+ ((R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z)) &
+ distr_l (R.<cr>)(R.<m>)(R.<f>) &
+ distr_r (R.<cr>)(R.<m>)(R.<f>) }"
+
+
+constdefs
+ group_of :: "'a ringtype => 'a grouptype"
+ "group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
+ inverse = (R.<inv>), unit = (R.<e>) |)"
+
+locale ring = group +
+ fixes
+ R :: "'a ringtype"
+ rmult :: "['a, 'a] => 'a" (infixr "**" 80)
+ assumes
+ Ring_R "R \\<in> Ring"
+ defines
+ rmult_def "op ** == (R.<m>)"
+ R_id_G "G == group_of R"
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/RingConstr.ML Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,67 @@
+(* Title: HOL/GroupTheory/RingConstr
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Construction of a ring from a semigroup and an Abelian group
+*)
+
+Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
+\ R \\<in> ring_constr `` {G} `` {S} |] \
+\ ==> R \\<in> Ring";
+by (force_tac (claset(),
+ simpset() addsimps [Ring_def, ring_constr_def, Abel_Abel,
+ Semigroup_def]@[distr_l_def, distr_r_def]) 1);
+qed "RingC_Ring";
+
+Goal "R = (| carrier = R .<cr>, bin_op = R .<f>, inverse = R .<inv>,\
+\ unit = R .<e>, Rmult = R .<m> |)";
+by Auto_tac;
+qed "surjective_Ring";
+
+Goal "R \\<in> Ring \
+\ ==> \\<exists>G \\<in> AbelianGroup. \\<exists>S \\<in> Semigroup. R \\<in> ring_constr `` {G} `` {S}";
+by (res_inst_tac [("x","group_of R")] bexI 1);
+by (afs [Ring_def, group_of_def] 2);
+by (res_inst_tac [("x","(| carrier = (R.<cr>), bin_op = (R.<m>) |)")] bexI 1);
+by (afs [Ring_def, AbelianGroup_def, Semigroup_def] 2);
+(* Now the main conjecture:
+ R\\<in>Ring
+ ==> R\\<in>ring_constr `` {group_of R} ``
+ {(| carrier = R .<cr>, bin_op = R .<m> |)} *)
+by (afs [ring_constr_def, Ring_def, group_of_def, AbelianGroup_def,
+ Semigroup_def,distr_l_def,distr_r_def] 1);
+qed "Ring_RingC";
+
+
+Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
+\ distr_l (G .<cr>) (S .<f>) (G .<f>); \
+\ distr_r (G .<cr>) (S .<f>) (G .<f>) |] \
+\ ==> ring_from G S \\<in> Ring";
+by (rtac RingI 1);
+by (ALLGOALS
+ (asm_full_simp_tac (simpset() addsimps [ring_from_def, Abel_Abel,
+ Semigroup_def])));
+qed "RingFrom_is_Ring";
+
+
+Goal "ring_from \\<in> (PI G : AbelianGroup. {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) \
+\ & distr_l (G.<cr>) (M.<f>) (G.<f>) & distr_r (G.<cr>) (M.<f>) (G.<f>)} \\<rightarrow> Ring)";
+by (rtac Pi_I 1);
+by (afs [ring_from_def] 2);
+by (rtac funcsetI 1);
+by (asm_full_simp_tac (simpset() addsimps [ring_from_def]) 2);
+by (Force_tac 2);
+by (afs [RingFrom_is_Ring] 1);
+qed "RingFrom_arity";
+
+(* group_of, i.e. the group in a ring *)
+
+Goal "R \\<in> Ring ==> group_of R \\<in> AbelianGroup";
+by (afs [group_of_def] 1);
+by (etac (export R_Abel) 1);
+qed "group_of_in_AbelianGroup";
+
+val R_Group = group_of_in_AbelianGroup RS Abel_imp_Group;
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/RingConstr.thy Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,38 @@
+(* Title: HOL/GroupTheory/RingConstr
+ ID: $Id$
+ Author: Florian Kammueller, with new proofs by L C Paulson
+ Copyright 1998-2001 University of Cambridge
+
+Construction of a ring from a semigroup and an Abelian group
+*)
+
+RingConstr = Homomorphism +
+
+constdefs
+ ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
+ "ring_of ==
+ lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
+ (| carrier = (G.<cr>), bin_op = (G.<f>),
+ inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
+
+ ring_constr :: "('a grouptype * 'a semigrouptype *'a ringtype) set"
+ "ring_constr ==
+ \\<Sigma>G \\<in> AbelianGroup. \\<Sigma>S \\<in> {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
+ {R. R = (| carrier = (G.<cr>), bin_op = (G.<f>),
+ inverse = (G.<inv>), unit = (G.<e>),
+ Rmult = (S.<f>) |) &
+ (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
+ ((R.<m>) x ((R.<f>) y z) = (R.<f>) ((R.<m>) x y) ((R.<m>) x z))) &
+(\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>).
+ ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
+
+ ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
+ "ring_from == lam G: AbelianGroup.
+ lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
+ distr_l (G.<cr>) (M.<f>) (G.<f>) &
+ distr_r (G.<cr>) (M.<f>) (G.<f>)}.
+ (| carrier = (G.<cr>), bin_op = (G.<f>),
+ inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
+
+end
+