# HG changeset patch
# User paulson
# Date 995903269 -7200
# Node ID aa519e0cc050d2270933eea60aec6b5c5922678f
# Parent  559c304bc6b2e0388c939b0b87654b6f5cbdee9d
Final version of Florian Kammueller's examples

diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Bij.ML
--- /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";
+
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Bij.thy
--- /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
+
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/FactGroup.ML
--- /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";
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/FactGroup.thy
--- /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
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Homomorphism.ML
--- /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" *)
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Homomorphism.thy
--- /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
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Ring.ML
--- /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";
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/Ring.thy
--- /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
+
+
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/RingConstr.ML
--- /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;
+
+
diff -r 559c304bc6b2 -r aa519e0cc050 src/HOL/GroupTheory/RingConstr.thy
--- /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
+