Final version of Florian Kammueller's examples
authorpaulson
Mon Jul 23 17:47:49 2001 +0200 (2001-07-23)
changeset 11448aa519e0cc050
parent 11447 559c304bc6b2
child 11449 d25be0ad1a6c
Final version of Florian Kammueller's examples
src/HOL/GroupTheory/Bij.ML
src/HOL/GroupTheory/Bij.thy
src/HOL/GroupTheory/FactGroup.ML
src/HOL/GroupTheory/FactGroup.thy
src/HOL/GroupTheory/Homomorphism.ML
src/HOL/GroupTheory/Homomorphism.thy
src/HOL/GroupTheory/Ring.ML
src/HOL/GroupTheory/Ring.thy
src/HOL/GroupTheory/RingConstr.ML
src/HOL/GroupTheory/RingConstr.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/GroupTheory/Bij.ML	Mon Jul 23 17:47:49 2001 +0200
     1.3 @@ -0,0 +1,171 @@
     1.4 +(*  Title:      HOL/GroupTheory/Bij
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     1.7 +    Copyright   1998-2001  University of Cambridge
     1.8 +
     1.9 +Bijections of a set and the group of bijections
    1.10 +	Sigma version with locales
    1.11 +*)
    1.12 +
    1.13 +Addsimps [Id_compose, compose_Id];
    1.14 +
    1.15 +(*Inv_f_f should suffice, only here A=B=S so the equality remains.*)
    1.16 +Goalw [Inv_def]
    1.17 +     "[|  f`A = B;  x : B |] ==> Inv A f x : A";
    1.18 +by (Clarify_tac 1); 
    1.19 +by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
    1.20 +qed "Inv_mem";
    1.21 +
    1.22 +Open_locale "bij";
    1.23 +
    1.24 +val B_def = thm "B_def";
    1.25 +val o'_def = thm "o'_def";
    1.26 +val inv'_def = thm "inv'_def";
    1.27 +val e'_def = thm "e'_def";
    1.28 +
    1.29 +Addsimps [B_def, o'_def, inv'_def];
    1.30 +
    1.31 +Goal "f \\<in> B ==> f \\<in> S \\<rightarrow> S";
    1.32 +by (afs [Bij_def] 1);
    1.33 +qed "BijE1";
    1.34 +
    1.35 +Goal "f \\<in> B ==> f ` S = S";
    1.36 +by (afs [Bij_def] 1);
    1.37 +qed "BijE2";
    1.38 +
    1.39 +Goal "f \\<in> B ==> inj_on f S";
    1.40 +by (afs [Bij_def] 1);
    1.41 +qed "BijE3";
    1.42 +
    1.43 +Goal "[| f \\<in> S \\<rightarrow> S; f ` S = S; inj_on f S |] ==> f \\<in> B";
    1.44 +by (afs [Bij_def] 1);
    1.45 +qed "BijI";
    1.46 +
    1.47 +Delsimps [B_def];
    1.48 +Addsimps [BijE1,BijE2,BijE3];
    1.49 +
    1.50 +
    1.51 +(* restrict (Inv S f) S  *)
    1.52 +Goal "f \\<in> B ==> (lam x: S. (inv' f) x) \\<in> B";
    1.53 +by (rtac BijI 1);
    1.54 +(* 1. (lam x: S. (inv' f) x): S \\<rightarrow> S *)
    1.55 +by (afs [Inv_funcset] 1);
    1.56 +(* 2. (lam x: S. (inv' f) x) ` S = S *)
    1.57 +by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1); 
    1.58 +by (rtac equalityI 1);
    1.59 +(* 2. <= *)
    1.60 +by (Clarify_tac 1); 
    1.61 +by (afs [Inv_mem, BijE2] 1);
    1.62 +(* 2. => *)
    1.63 +by (rtac subsetI 1);
    1.64 +by (res_inst_tac [("x","f x")] image_eqI 1);
    1.65 +by (asm_simp_tac (simpset() addsimps [Inv_f_f, BijE1 RS funcset_mem]) 1); 
    1.66 +by (asm_simp_tac (simpset() addsimps [BijE1 RS funcset_mem]) 1); 
    1.67 +(* 3. *)
    1.68 +by (rtac inj_onI 1);
    1.69 +by (auto_tac (claset() addEs [Inv_injective], simpset())); 
    1.70 +qed "restrict_Inv_Bij";
    1.71 +
    1.72 +Addsimps [e'_def];
    1.73 +
    1.74 +Goal "e'\\<in>B ";
    1.75 +by (rtac BijI 1);
    1.76 +by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def])); 
    1.77 +qed "restrict_id_Bij";
    1.78 +
    1.79 +Goal "f \\<in> B ==> (lam g: B. lam x: S. (inv' g) x) f = (lam x: S. (inv' f) x)";
    1.80 +by (Asm_full_simp_tac 1); 
    1.81 +qed "eval_restrict_Inv";
    1.82 +
    1.83 +Goal "[| x \\<in> B; y \\<in> B|] ==> x o' y \\<in> B";
    1.84 +by (simp_tac (simpset() addsimps [o'_def]) 1);
    1.85 +by (rtac BijI 1);
    1.86 +by (blast_tac (claset() addIs [funcset_compose] addDs [BijE1,BijE2,BijE3]) 1); 
    1.87 +by (blast_tac (claset() delrules [equalityI]
    1.88 +			addIs [surj_compose] addDs [BijE1,BijE2,BijE3]) 1); 
    1.89 +by (blast_tac (claset() addIs [inj_on_compose] addDs [BijE1,BijE2,BijE3]) 1); 
    1.90 +qed "compose_Bij";
    1.91 +
    1.92 +
    1.93 +
    1.94 +(**** Bijections form a group ****)
    1.95 +
    1.96 +
    1.97 +Open_locale "bijgroup";
    1.98 +
    1.99 +val BG_def = thm "BG_def";
   1.100 +
   1.101 +Goal "[| x\\<in>B; y\\<in>B |] ==> (lam g: B. lam f: B. g o' f) x y = x o' y";
   1.102 +by (Asm_full_simp_tac 1); 
   1.103 +qed "eval_restrict_comp2";
   1.104 +
   1.105 +
   1.106 +Addsimps [BG_def, B_def, o'_def, inv'_def,e'_def];
   1.107 +
   1.108 +Goal "carrier BG == B";
   1.109 +by (afs [BijGroup_def] 1);
   1.110 +qed "BG_carrier";
   1.111 +
   1.112 +Goal "bin_op BG == lam g: B. lam f: B. g o' f";
   1.113 +by (afs [BijGroup_def] 1);
   1.114 +qed "BG_bin_op";
   1.115 +               
   1.116 +Goal "inverse BG == lam f: B. lam x: S. (inv' f) x";
   1.117 +by (afs [BijGroup_def] 1);
   1.118 +qed "BG_inverse"; 
   1.119 +
   1.120 +Goal "unit BG   == e'";
   1.121 +by (afs [BijGroup_def] 1);
   1.122 +qed "BG_unit";
   1.123 +
   1.124 +Goal "BG = (| carrier = BG.<cr>, bin_op = BG.<f>,\
   1.125 +\             inverse = BG.<inv>, unit = BG.<e> |)";
   1.126 +by (afs [BijGroup_def,BG_carrier, BG_bin_op, BG_inverse, BG_unit] 1);
   1.127 +qed "BG_defI";
   1.128 +
   1.129 +Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
   1.130 +
   1.131 +
   1.132 +Goal "(lam g: B. lam f: B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
   1.133 +by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1); 
   1.134 +qed "restrict_compose_Bij";
   1.135 +
   1.136 +
   1.137 +Goal "BG \\<in> Group";
   1.138 +by (stac BG_defI 1);
   1.139 +by (rtac GroupI 1);
   1.140 +(* 1. (BG .<f>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) \\<rightarrow> (BG .<cr>) *)
   1.141 +by (afs [BG_bin_op, BG_carrier, restrict_compose_Bij] 1);
   1.142 +(*  2: (BG .<inv>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) *)
   1.143 +by (simp_tac (simpset() addsimps [BG_inverse, BG_carrier, restrict_Inv_Bij, 
   1.144 +                                  funcsetI]) 1); 
   1.145 +by (afs [BG_inverse, BG_carrier,eval_restrict_Inv, restrict_Inv_Bij] 1);
   1.146 +(* 3.  *)
   1.147 +by (afs [BG_carrier, BG_unit, restrict_id_Bij] 1);
   1.148 +(* Now the equalities *)
   1.149 +(* 4. ! x:BG .<cr>. (BG .<f>) ((BG .<inv>) x) x = (BG .<e>) *)
   1.150 +by (simp_tac
   1.151 +    (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
   1.152 +            e'_def, compose_Inv_id, inv'_def, o'_def]) 1); 
   1.153 +by (simp_tac
   1.154 +    (simpset() addsimps [symmetric (inv'_def), restrict_Inv_Bij]) 1); 
   1.155 +(* 5: ! x:BG .<cr>. (BG .<f>) (BG .<e>) x = x *)
   1.156 +by (simp_tac
   1.157 +    (simpset() addsimps [BG_carrier, BG_unit, BG_bin_op,
   1.158 +            e'_def, o'_def]) 1); 
   1.159 +by (simp_tac
   1.160 +    (simpset() addsimps [symmetric (e'_def), restrict_id_Bij]) 1); 
   1.161 +(* 6. ! x:BG .<cr>.
   1.162 +       ! y:BG .<cr>.
   1.163 +          ! z:BG .<cr>.
   1.164 +             (BG .<f>) ((BG .<f>) x y) z = (BG .<f>) x ((BG .<f>) y z) *)
   1.165 +by (simp_tac
   1.166 +    (simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
   1.167 +                         compose_Bij]) 1); 
   1.168 +by (simp_tac (simpset() addsimps [o'_def]) 1);
   1.169 +by (blast_tac (claset() addIs [compose_assoc RS sym, BijE1]) 1); 
   1.170 +qed "Bij_are_Group";
   1.171 +
   1.172 +Close_locale "bijgroup";
   1.173 +Close_locale "bij";
   1.174 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/GroupTheory/Bij.thy	Mon Jul 23 17:47:49 2001 +0200
     2.3 @@ -0,0 +1,42 @@
     2.4 +(*  Title:      HOL/GroupTheory/Coset
     2.5 +    ID:         $Id$
     2.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     2.7 +    Copyright   1998-2001  University of Cambridge
     2.8 +
     2.9 +Bijections of a set and the group of bijections
    2.10 +	Sigma version with locales
    2.11 +*)
    2.12 +
    2.13 +Bij = Group +
    2.14 +
    2.15 +constdefs
    2.16 +  Bij :: "'a set => (('a => 'a)set)" 
    2.17 +    "Bij S == {f. f \\<in> S \\<rightarrow> S & f`S = S & inj_on f S}"
    2.18 +
    2.19 +constdefs 
    2.20 +BijGroup ::  "'a set => (('a => 'a) grouptype)"
    2.21 +"BijGroup S == (| carrier = Bij S, 
    2.22 +                  bin_op  = lam g: Bij S. lam f: Bij S. compose S g f,
    2.23 +                  inverse = lam f: Bij S. lam x: S. (Inv S f) x, 
    2.24 +                  unit    = lam x: S. x |)"
    2.25 +
    2.26 +locale bij = 
    2.27 +  fixes 
    2.28 +    S :: "'a set"
    2.29 +    B :: "('a => 'a)set"
    2.30 +    comp :: "[('a => 'a),('a => 'a)]=>('a => 'a)" (infixr "o''" 80)
    2.31 +    inv'   :: "('a => 'a)=>('a => 'a)"              
    2.32 +    e'   :: "('a => 'a)"
    2.33 +  defines
    2.34 +    B_def    "B == Bij S"
    2.35 +    o'_def   "g o' f == compose S g f"
    2.36 +    inv'_def   "inv' f == Inv S f"
    2.37 +    e'_def   "e'  == (lam x: S. x)"
    2.38 +
    2.39 +locale bijgroup = bij +
    2.40 +  fixes 
    2.41 +    BG :: "('a => 'a) grouptype"
    2.42 +  defines
    2.43 +    BG_def "BG == BijGroup S"
    2.44 +end
    2.45 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/GroupTheory/FactGroup.ML	Mon Jul 23 17:47:49 2001 +0200
     3.3 @@ -0,0 +1,80 @@
     3.4 +(*  Title:      HOL/GroupTheory/FactGroup
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     3.7 +    Copyright   1998-2001  University of Cambridge
     3.8 +
     3.9 +Factorization of a group
    3.10 +*)
    3.11 +
    3.12 +
    3.13 +Open_locale "factgroup";
    3.14 +
    3.15 +val H_normal = thm "H_normal";
    3.16 +val F_def = thm "F_def";
    3.17 +
    3.18 +Addsimps [H_normal, F_def,setrcos_def];
    3.19 +
    3.20 +Goal "carrier F = {* H *}";
    3.21 +by (afs [FactGroup_def] 1);
    3.22 +qed "F_carrier";
    3.23 +
    3.24 +Goal "bin_op F = (lam X: {* H *}. lam Y: {* H *}. X <#> Y) ";
    3.25 +by (afs [FactGroup_def, setprod_def] 1);
    3.26 +qed "F_bin_op";
    3.27 +
    3.28 +Goal "inverse F = (lam X: {* H *}. I(X))";
    3.29 +by (afs [FactGroup_def, setinv_def] 1);
    3.30 +qed "F_inverse";
    3.31 +
    3.32 +Goal "unit F = H";
    3.33 +by (afs [FactGroup_def] 1);
    3.34 +qed "F_unit";
    3.35 +
    3.36 +Goal "F = (| carrier = {* H *}, \
    3.37 +\            bin_op  = (lam X: {* H *}. lam Y: {* H *}. X <#> Y), \
    3.38 +\            inverse = (lam X: {* H *}. I(X)),  unit = H |)";
    3.39 +by (afs [FactGroup_def, F_carrier, F_bin_op, F_inverse, F_unit] 1);
    3.40 +by (auto_tac (claset() addSIs [restrict_ext], 
    3.41 +              simpset() addsimps [set_prod_def, setprod_def, setinv_def])); 
    3.42 +qed "F_defI";
    3.43 +val F_DefI = export F_defI;
    3.44 +
    3.45 +Delsimps [setrcos_def];
    3.46 +
    3.47 +(* MAIN PROOF *)
    3.48 +Goal "F \\<in> Group";
    3.49 +val l1 = H_normal RS normal_imp_subgroup ;
    3.50 +val l2 = l1 RS subgroup_imp_subset;
    3.51 +by (stac F_defI 1);
    3.52 +by (rtac GroupI 1);
    3.53 +(* 1.  *)
    3.54 +by (afs [restrictI, setprod_closed] 1);
    3.55 +(* 2. *)
    3.56 +by (afs [restrictI, setinv_closed] 1);
    3.57 +(* 3. H\\<in>{* H *} *)
    3.58 +by (rtac (l1 RS setrcos_unit_closed) 1);
    3.59 +(* 4. inverse property *)
    3.60 +by (simp_tac (simpset() addsimps [setinv_closed, setrcos_inv_prod_eq]) 1);
    3.61 +(* 5. unit property *)
    3.62 +by (simp_tac (simpset() addsimps [normal_imp_subgroup, 
    3.63 +           setrcos_unit_closed, setrcos_prod_eq]) 1);
    3.64 +(* 6. associativity *)
    3.65 +by (asm_simp_tac
    3.66 +    (simpset() addsimps [setprod_closed, H_normal RS setrcos_prod_assoc]) 1);
    3.67 +qed "factorgroup_is_group";
    3.68 +val FactorGroup_is_Group = export factorgroup_is_group;
    3.69 +
    3.70 +
    3.71 +Delsimps [H_normal, F_def];
    3.72 +Close_locale "factgroup";
    3.73 +
    3.74 +
    3.75 +Goalw [FactGroup_def] "FactGroup \\<in> (PI G: Group. {H. H <| G} \\<rightarrow> Group)";
    3.76 +by (rtac restrictI 1);
    3.77 +by (rtac restrictI 1);
    3.78 +by (asm_full_simp_tac
    3.79 +    (simpset() addsimps [F_DefI RS sym, FactorGroup_is_Group]) 1); 
    3.80 +qed "FactGroup_arity";
    3.81 + 
    3.82 +Close_locale "coset";
    3.83 +Close_locale "group";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/GroupTheory/FactGroup.thy	Mon Jul 23 17:47:49 2001 +0200
     4.3 @@ -0,0 +1,38 @@
     4.4 +(*  Title:      HOL/GroupTheory/FactGroup
     4.5 +    ID:         $Id$
     4.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     4.7 +    Copyright   1998-2001  University of Cambridge
     4.8 +
     4.9 +Factorization of a group
    4.10 +*)
    4.11 +
    4.12 +FactGroup = Coset +
    4.13 +
    4.14 +constdefs
    4.15 +  FactGroup :: "(['a grouptype, 'a set] => ('a set) grouptype)"
    4.16 +
    4.17 +   "FactGroup ==
    4.18 +     lam G: Group. lam H: {H. H <| G}.
    4.19 +      (| carrier = set_r_cos G H,
    4.20 +	 bin_op = (lam X: set_r_cos G H. lam Y: set_r_cos G H. set_prod G X Y),
    4.21 +	 inverse = (lam X: set_r_cos G H. set_inv G X), 
    4.22 +	 unit = H |)"
    4.23 +
    4.24 +syntax
    4.25 +  "@Fact" :: "['a grouptype, 'a set] => ('a set) grouptype"
    4.26 +              ("_ Mod _" [60,61]60)
    4.27 +
    4.28 +translations
    4.29 +  "G Mod H" == "FactGroup G H"
    4.30 +
    4.31 +locale factgroup = coset +
    4.32 +fixes 
    4.33 +  F :: "('a set) grouptype"
    4.34 +  H :: "('a set)"
    4.35 +assumes
    4.36 +  H_normal "H <| G"
    4.37 +defines
    4.38 +  F_def "F == FactGroup G H"
    4.39 +
    4.40 +end
    4.41 +  
    4.42 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/GroupTheory/Homomorphism.ML	Mon Jul 23 17:47:49 2001 +0200
     5.3 @@ -0,0 +1,267 @@
     5.4 +(*  Title:      HOL/GroupTheory/Homomorphism
     5.5 +    ID:         $Id$
     5.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     5.7 +    Copyright   1998-2001  University of Cambridge
     5.8 +
     5.9 +Homomorphisms of groups, rings, and automorphisms.
    5.10 +Sigma version with Locales
    5.11 +*)
    5.12 +
    5.13 +Open_locale "bij";
    5.14 +
    5.15 +Addsimps [B_def, o'_def, inv'_def];
    5.16 +
    5.17 +Goal "[|x \\<in> S; f \\<in> B|] ==> EX x'. x = f x'";
    5.18 +by (dtac BijE2 1); 
    5.19 +by Auto_tac; 
    5.20 +
    5.21 +
    5.22 +Goal "[| f \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S;\
    5.23 +\      \\<forall>x \\<in> S. \\<forall>y \\<in> S. f(g x y) = g (f x) (f y) |] \
    5.24 +\     ==> inv' f (g x y) = g (inv' f x) (inv' f y)";
    5.25 +by (subgoal_tac "EX x':S. EX y':S. x = f x' & y = f y'" 1);
    5.26 +by (blast_tac (claset() addDs [BijE2]) 2);
    5.27 +by (Clarify_tac 1); 
    5.28 +(*the next step could be avoided if we could re-orient the quanitifed 
    5.29 +  assumption, to rewrite g (f x') (f y') ...*)
    5.30 +by (rtac inj_onD 1);
    5.31 +by (etac BijE3 1);
    5.32 +by (asm_full_simp_tac (simpset() addsimps [f_Inv_f, Inv_f_f, BijE2, BijE3, 
    5.33 +                                  funcset_mem RS funcset_mem]) 1); 
    5.34 +by (ALLGOALS
    5.35 +    (asm_full_simp_tac
    5.36 +     (simpset() addsimps [funcset_mem RS funcset_mem, BijE2, Inv_mem])));
    5.37 +qed "Bij_op_lemma";
    5.38 +
    5.39 +Goal "[| a \\<in> B; b \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S; \
    5.40 +\       \\<forall>x \\<in> S. \\<forall>y \\<in> S. a (b (g x y)) = g (a (b x)) (a (b y)) |]  \
    5.41 +\     ==> (a o' b) (g x y) = g ((a o' b) x) ((a o' b) y)";
    5.42 +by (afs [o'_def, compose_eq, B_def, 
    5.43 +         funcset_mem RS funcset_mem] 1);
    5.44 +qed "Bij_comp_lemma";
    5.45 +
    5.46 +
    5.47 +Goal "[| R1 \\<in> Ring; R2 \\<in> Ring |]  \
    5.48 +\  ==> RingHom `` {R1} `` {R2} = \
    5.49 +\      {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) & \
    5.50 +\            (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
    5.51 +\               (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &\
    5.52 +\            (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
    5.53 +\               (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}";
    5.54 +by (afs [Image_def,RingHom_def] 1);
    5.55 +qed "RingHom_apply";
    5.56 +
    5.57 +(* derive the defining properties as single lemmas *)
    5.58 +Goal "(R1,R2,Phi) \\<in> RingHom ==> Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>)";
    5.59 +by (afs [RingHom_def] 1);
    5.60 +qed "RingHom_imp_funcset";
    5.61 +
    5.62 +Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |]  \
    5.63 +\     ==> Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y)";
    5.64 +by (afs [RingHom_def] 1);
    5.65 +qed "RingHom_preserves_rplus";
    5.66 +
    5.67 +Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |]  \
    5.68 +\     ==> Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)";
    5.69 +by (afs [RingHom_def] 1);
    5.70 +qed "RingHom_preserves_rmult";
    5.71 +
    5.72 +Goal "[| R1 \\<in> Ring; R2 \\<in> Ring; Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>); \
    5.73 +\        \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
    5.74 +\          Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y);\
    5.75 +\        \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \
    5.76 +\          Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)|]\
    5.77 +\    ==> (R1,R2,Phi) \\<in> RingHom";
    5.78 +by (afs [RingHom_def] 1);
    5.79 +qed "RingHomI";
    5.80 +
    5.81 +Open_locale "ring";
    5.82 +
    5.83 +val Ring_R = thm "Ring_R";
    5.84 +val rmult_def = thm "rmult_def";
    5.85 +
    5.86 +Addsimps [simp_R, Ring_R];
    5.87 +
    5.88 +
    5.89 +
    5.90 +(* RingAutomorphisms *)
    5.91 +Goal "RingAuto `` {R} = \
    5.92 +\ {Phi. (R,R,Phi)  \\<in> RingHom & inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}";
    5.93 +by (rewtac RingAuto_def);
    5.94 +by (afs [Image_def] 1);
    5.95 +qed "RingAuto_apply";
    5.96 +
    5.97 +Goal "(R,Phi) \\<in> RingAuto  ==> (R, R, Phi)  \\<in> RingHom";
    5.98 +by (afs [RingAuto_def] 1);
    5.99 +qed "RingAuto_imp_RingHom";
   5.100 +
   5.101 +Goal "(R,Phi) \\<in> RingAuto ==> inj_on Phi (R.<cr>)";
   5.102 +by (afs [RingAuto_def] 1);
   5.103 +qed "RingAuto_imp_inj_on";
   5.104 +
   5.105 +Goal "(R,Phi) \\<in> RingAuto ==> Phi ` (R.<cr>) = (R.<cr>)";
   5.106 +by (afs [RingAuto_def] 1);
   5.107 +qed "RingAuto_imp_preserves_R";
   5.108 +
   5.109 +Goal "(R,Phi) \\<in> RingAuto ==> Phi \\<in> (R.<cr>) \\<rightarrow> (R.<cr>)";
   5.110 +by (etac (RingAuto_imp_RingHom RS RingHom_imp_funcset) 1); 
   5.111 +qed "RingAuto_imp_funcset";
   5.112 +
   5.113 +Goal "[| (R,R,Phi) \\<in> RingHom; \
   5.114 +\        inj_on Phi (R.<cr>); \
   5.115 +\        Phi ` (R.<cr>) = (R.<cr>) |]\
   5.116 +\     ==> (R,Phi) \\<in> RingAuto";
   5.117 +by (afs [RingAuto_def] 1);
   5.118 +qed "RingAutoI";
   5.119 +
   5.120 +
   5.121 +(* major result: RingAutomorphism builds a group *)
   5.122 +(* We prove that they are a subgroup of the bijection group.
   5.123 +   Note!!! Here we need "RingAuto `` {R} ~= {}", (as a result from the
   5.124 +   resolution with subgroupI). That is, this is an example where one might say
   5.125 +   the discipline of Pi types pays off, because there we have the proof basically
   5.126 +   already there (compare the Pi-version).
   5.127 +   Here in the Sigma version, we have to redo now the proofs (or slightly
   5.128 +   adapted verisions) of promoteRingHom and promoteRingAuto *)
   5.129 +
   5.130 +Goal "RingAuto `` {R} ~= {}";
   5.131 +by (stac RingAuto_apply 1);
   5.132 +by Auto_tac; 
   5.133 +by (res_inst_tac [("x","lam y: (R.<cr>). y")] exI 1);
   5.134 +by (auto_tac (claset(), simpset() addsimps [inj_on_def])); 
   5.135 +by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI, 
   5.136 +     R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1);
   5.137 +qed "RingAutoEx";
   5.138 +
   5.139 +Goal "(R,f) \\<in> RingAuto ==> f \\<in> Bij (R.<cr>)";
   5.140 +by (afs [RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on, 
   5.141 +                RingAuto_imp_preserves_R, export BijI] 1);
   5.142 +qed "RingAuto_Bij";
   5.143 +Addsimps [RingAuto_Bij];
   5.144 +
   5.145 +Goal "[| (R,a) \\<in> RingAuto; (R,b) \\<in> RingAuto; \
   5.146 +\        g \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>); x \\<in> carrier R; y \\<in> carrier R; \
   5.147 +\        \\<forall>Phi. (R,Phi) \\<in> RingAuto --> \
   5.148 +\          (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). Phi(g x y) = g(Phi x) (Phi y)) |] \
   5.149 +\     ==> compose (R.<cr>) a b (g x y) = \
   5.150 +\           g (compose (R.<cr>) a b x) (compose (R.<cr>) a b y)";
   5.151 +by (asm_simp_tac (simpset() addsimps [export Bij_comp_lemma, 
   5.152 +                                    RingAuto_imp_funcset RS funcset_mem]) 1);
   5.153 +qed "Auto_comp_lemma";
   5.154 +
   5.155 +Goal "[|(R, a) \\<in> RingAuto; x \\<in> carrier R; y \\<in> carrier R|]  \
   5.156 +\     ==> Inv (carrier R) a (x ## y) =  \
   5.157 +\         Inv (carrier R) a x ## Inv (carrier R) a y"; 
   5.158 +by (rtac (export Bij_op_lemma) 1);
   5.159 +by (etac RingAuto_Bij 1);
   5.160 +by (rtac rplus_funcset 1);
   5.161 +by (assume_tac 1);
   5.162 +by (assume_tac 1);
   5.163 +by (asm_simp_tac (simpset() addsimps [R_binop_def RS sym, 
   5.164 +                         RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1);
   5.165 +qed "Inv_rplus_lemma";
   5.166 +
   5.167 +Goal "(R,a) \\<in> RingAuto \
   5.168 +\     ==> (R, grouptype.inverse (BijGroup (carrier R)) a) \\<in> RingAuto";
   5.169 +by (rtac RingAutoI 1);
   5.170 +by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE3)] 2);
   5.171 +by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE2)] 2);
   5.172 +by (rtac RingHomI 1);
   5.173 +by (rtac (Ring_R) 1);
   5.174 +by (rtac (Ring_R) 1);
   5.175 +(* ...  ==> (BijGroup (R .<R>) .<inv>) a \\<in> (R .<R>) \\<rightarrow> (R .<R>) *)
   5.176 +by (asm_simp_tac (simpset() addsimps [BijGroup_def, 
   5.177 +                     export restrict_Inv_Bij RS export BijE1]) 1); 
   5.178 +by (asm_simp_tac (simpset() addsimps [BijGroup_def, R_binop_def, rplus_closed, Inv_rplus_lemma]) 1); 
   5.179 +by (afs [BijGroup_def, symmetric (rmult_def), rmult_closed] 1);
   5.180 +by (afs [export Bij_op_lemma, rmult_funcset, rmult_def, 
   5.181 +         RingAuto_imp_RingHom RS RingHom_preserves_rmult] 1);
   5.182 +qed "inverse_BijGroup_lemma";
   5.183 +
   5.184 +Goal "[|(R, a) \\<in> RingAuto; (R, b) \\<in> RingAuto|]  \
   5.185 +\     ==> (R, bin_op (BijGroup (carrier R)) a b) \\<in> RingAuto";
   5.186 +by (afs [BijGroup_def] 1);
   5.187 +by (rtac RingAutoI 1);
   5.188 +by (rtac RingHomI 1);
   5.189 +by (rtac (Ring_R) 1);
   5.190 +by (rtac (Ring_R) 1);
   5.191 +by (afs [RingAuto_Bij,export compose_Bij,export BijE1] 1);
   5.192 +by (Clarify_tac 1); 
   5.193 +by (rtac Auto_comp_lemma 1);
   5.194 +by (ALLGOALS Asm_full_simp_tac);
   5.195 +by (asm_full_simp_tac (simpset() addsimps [R_binop_def, rplus_funcset]) 1); 
   5.196 +by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1); 
   5.197 +by (Clarify_tac 1); 
   5.198 +by (rtac Auto_comp_lemma 1);
   5.199 +by (assume_tac 1); 
   5.200 +by (assume_tac 1); 
   5.201 +by (asm_full_simp_tac (simpset() addsimps [rmult_funcset]) 1); 
   5.202 +by (assume_tac 1); 
   5.203 +by (assume_tac 1); 
   5.204 +by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rmult]) 1); 
   5.205 +(*       ==> inj_on (compose (R .<R>) a b) (R .<R>) *)
   5.206 +by (blast_tac (claset() delrules [equalityI]
   5.207 +			addIs [inj_on_compose, RingAuto_imp_inj_on, 
   5.208 +                          RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1); 
   5.209 +(*      ==> compose (R .<R>) a b ` (R .<R>) = (R .<R>) *)
   5.210 +by (blast_tac (claset() delrules [equalityI] 
   5.211 +      addIs [surj_compose, RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1);
   5.212 +qed "binop_BijGroup_lemma";
   5.213 +
   5.214 +
   5.215 +(* Ring automorphisms are a subgroup of the group of bijections over the 
   5.216 +   ring's carrier, and thus a group *)
   5.217 +Goal "RingAuto `` {R} <<= BijGroup (R.<cr>)";
   5.218 +by (rtac SubgroupI 1);
   5.219 +by (rtac (export Bij_are_Group) 1);
   5.220 +(* 1. RingAuto `` {R} <= (BijGroup (R .<R>) .<cr>) *)
   5.221 +by (afs [subset_def, BijGroup_def, Bij_def, 
   5.222 +         RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on, 
   5.223 +         RingAuto_imp_preserves_R, Image_def] 1);
   5.224 +(* 1. !!R. R \\<in> Ring ==> RingAuto `` {R} ~= {} *)
   5.225 +by (rtac RingAutoEx 1);
   5.226 +by (auto_tac (claset(),
   5.227 +         simpset() addsimps [inverse_BijGroup_lemma, binop_BijGroup_lemma])); 
   5.228 +qed "RingAuto_SG_BijGroup";
   5.229 +
   5.230 +Delsimps [simp_R, Ring_R];
   5.231 +
   5.232 +Close_locale "ring";
   5.233 +Close_locale "group";
   5.234 +
   5.235 +val RingAuto_are_Group = (export RingAuto_SG_BijGroup) RS (export Bij_are_Group RS SubgroupE2);
   5.236 +(* So far:
   5.237 +"[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |]
   5.238 +   ==> (| carrier = RingAuto `` {?R2},
   5.239 +          bin_op =
   5.240 +            lam x:RingAuto `` {?R2}.
   5.241 +               restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}),
   5.242 +          inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}),
   5.243 +          unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *)
   5.244 +
   5.245 +(* Unfortunately we have to eliminate the extra assumptions 
   5.246 +Now only group_of R \\<in> Group *)
   5.247 +
   5.248 +Goal "R \\<in> Ring ==> group_of R \\<in> Group";
   5.249 +by (asm_full_simp_tac (simpset() addsimps [group_of_def]) 1); 
   5.250 +by (rtac Abel_imp_Group 1);
   5.251 +by (etac (export R_Abel) 1);
   5.252 +qed "R_Group";
   5.253 +
   5.254 +Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\
   5.255 +\          bin_op =  lam x:RingAuto `` {R}. lam y: RingAuto `` {R}.\
   5.256 +\                             (BijGroup (R.<cr>) .<f>) x y ,\
   5.257 +\          inverse = lam x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\
   5.258 +\          unit = BijGroup (R.<cr>) .<e> |) \\<in> Group";
   5.259 +by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1);
   5.260 +by (assume_tac 1);
   5.261 +by (assume_tac 1);
   5.262 +qed "RingAuto_are_Groupf";
   5.263 +
   5.264 +(* "?R \\<in> Ring
   5.265 +   ==> (| carrier = RingAuto `` {?R},
   5.266 +          bin_op =
   5.267 +            lam x:RingAuto `` {?R}.
   5.268 +               restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}),
   5.269 +          inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}),
   5.270 +          unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/GroupTheory/Homomorphism.thy	Mon Jul 23 17:47:49 2001 +0200
     6.3 @@ -0,0 +1,40 @@
     6.4 +(*  Title:      HOL/GroupTheory/Homomorphism
     6.5 +    ID:         $Id$
     6.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     6.7 +    Copyright   1998-2001  University of Cambridge
     6.8 +
     6.9 +Homomorphisms of groups, rings, and automorphisms.
    6.10 +Sigma version with Locales
    6.11 +*)
    6.12 +
    6.13 +Homomorphism = Ring + Bij +
    6.14 +
    6.15 +consts
    6.16 +  Hom :: "('a grouptype * 'b grouptype * ('a => 'b)) set"
    6.17 +
    6.18 +defs
    6.19 +  Hom_def "Hom == \\<Sigma>G \\<in> Group. \\<Sigma>H \\<in> Group. {Phi. Phi \\<in> (G.<cr>) \\<rightarrow> (H.<cr>) & 
    6.20 +                  (\\<forall>x \\<in> (G.<cr>) . \\<forall>y \\<in> (G.<cr>) . (Phi((G.<f>) x y) = (H.<f>) (Phi x)(Phi y)))}"
    6.21 +
    6.22 +consts
    6.23 +  RingHom :: "(('a ringtype) * ('b ringtype) * ('a => 'b))set"
    6.24 +defs
    6.25 +  RingHom_def "RingHom == \\<Sigma>R1 \\<in> Ring. \\<Sigma>R2 \\<in> Ring. {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) &
    6.26 +                   (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &
    6.27 +                   (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}"
    6.28 +
    6.29 +consts
    6.30 +  GroupAuto :: "('a grouptype * ('a => 'a)) set"
    6.31 +
    6.32 +defs
    6.33 +  GroupAuto_def "GroupAuto == \\<Sigma>G \\<in> Group. {Phi. (G,G,Phi)\\<in>Hom  &
    6.34 +                    inj_on Phi (G.<cr>) & Phi ` (G.<cr>) = (G.<cr>)}"
    6.35 +
    6.36 +consts
    6.37 +  RingAuto :: "(('a ringtype) * ('a => 'a))set"
    6.38 +
    6.39 +defs
    6.40 +  RingAuto_def "RingAuto == \\<Sigma>R \\<in> Ring. {Phi. (R,R,Phi)\\<in>RingHom &
    6.41 +                    inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}"
    6.42 +
    6.43 +end
    6.44 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/GroupTheory/Ring.ML	Mon Jul 23 17:47:49 2001 +0200
     7.3 @@ -0,0 +1,138 @@
     7.4 +(*  Title:      HOL/GroupTheory/Ring
     7.5 +    ID:         $Id$
     7.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     7.7 +    Copyright   1998-2001  University of Cambridge
     7.8 +
     7.9 +Ring theory. Sigma version
    7.10 +*)
    7.11 +
    7.12 +Goal
    7.13 +"[| (| carrier = carrier R, bin_op = R .<f>, \
    7.14 +\      inverse = R .<inv>, unit = R .<e> |) \\<in> AbelianGroup;\
    7.15 +\   (R.<m>) \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R); \
    7.16 +\   \\<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;\ 
    7.17 +\   distr_l (carrier R)(R.<m>)(R.<f>); distr_r (carrier R)(R.<m>)(R.<f>) |]\
    7.18 +\ ==> R \\<in> Ring";
    7.19 +by (afs [Ring_def] 1);
    7.20 +qed "RingI";
    7.21 +
    7.22 +Open_locale "ring";
    7.23 +
    7.24 +val simp_R = simplify (simpset() addsimps [Ring_def]) (thm "Ring_R");
    7.25 +
    7.26 +Addsimps [simp_R, thm "Ring_R", thm "rmult_def",thm "R_id_G"];
    7.27 +
    7.28 +Goal "(| carrier = (carrier R), bin_op = (R.<f>), inverse = (R.<inv>), \
    7.29 +\        unit = (R.<e>) |) \\<in> AbelianGroup";
    7.30 +by (Asm_full_simp_tac 1);
    7.31 +qed "R_Abel";
    7.32 +
    7.33 +Goal "group_of R \\<in> AbelianGroup";
    7.34 +by (afs [group_of_def] 1);
    7.35 +qed "R_forget";
    7.36 +
    7.37 +Goal "((group_of R).<cr>) = (carrier R)";
    7.38 +by (afs [group_of_def] 1);
    7.39 +qed "FR_carrier";
    7.40 +
    7.41 +Goal "(G.<cr>) = (carrier R)";
    7.42 +by (simp_tac (simpset() addsimps [FR_carrier RS sym]) 1); 
    7.43 +qed "R_carrier_def";
    7.44 +
    7.45 +Goal "((group_of R).<f>) = op ##";
    7.46 +by (afs [binop_def, thm "R_id_G"] 1);
    7.47 +qed "FR_bin_op";
    7.48 +
    7.49 +Goal "(R.<f>) = op ##";
    7.50 +by (afs [FR_bin_op RS sym, group_of_def] 1);
    7.51 +qed "R_binop_def";
    7.52 +
    7.53 +Goal "((group_of R).<inv>) = INV";
    7.54 +by (afs [thm "inv_def"] 1);
    7.55 +qed "FR_inverse";
    7.56 +
    7.57 +Goal "(R.<inv>) = INV";
    7.58 +by (afs [FR_inverse RS sym, group_of_def] 1);
    7.59 +qed "R_inv_def";
    7.60 +
    7.61 +Goal "((group_of R).<e>) = e";
    7.62 +by (afs [thm "e_def"] 1);
    7.63 +qed "FR_unit";
    7.64 +
    7.65 +Goal "(R.<e>) = e";
    7.66 +by (afs [FR_unit RS sym, group_of_def] 1);
    7.67 +qed "R_unit_def";
    7.68 +
    7.69 +Goal "G \\<in> AbelianGroup";
    7.70 +by (afs [group_of_def] 1);
    7.71 +qed "G_abelian";
    7.72 +
    7.73 +
    7.74 +Delsimps [thm "R_id_G"];  (*needed below?*)
    7.75 +
    7.76 +Goal "[| x \\<in> (G.<cr>); y \\<in> (G.<cr>) |] ==> x ## y = y ## x";
    7.77 +by (afs [thm "binop_def", G_abelian RS Group_commute] 1);
    7.78 +qed "binop_commute";
    7.79 +
    7.80 +Goal "op ** \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R)";
    7.81 +by (simp_tac (simpset() addsimps [thm "rmult_def"]) 1); 
    7.82 +qed "rmult_funcset";
    7.83 +
    7.84 +Goal "[| x \\<in> (carrier R); y \\<in> (carrier R) |] ==>  x ** y \\<in> (carrier R)";
    7.85 +by (blast_tac
    7.86 +    (claset() addIs [rmult_funcset RS funcset_mem RS funcset_mem]) 1); 
    7.87 +qed "rmult_closed";
    7.88 +
    7.89 +Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
    7.90 +\     ==> x **(y ** z) = (x ** y)** z";
    7.91 +by (Asm_full_simp_tac 1);
    7.92 +qed "rmult_assoc";
    7.93 +
    7.94 +Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \
    7.95 +\     ==> x **(y ## z) = (x ** y) ## (x ** z)";
    7.96 +by (cut_facts_tac [thm "Ring_R"] 1);
    7.97 +by (asm_full_simp_tac (simpset() delsimps [thm "Ring_R", simp_R]
    7.98 +                    addsimps [Ring_def, distr_l_def, R_binop_def]) 1); 
    7.99 +qed "R_distrib1";
   7.100 +
   7.101 +
   7.102 +(* The following have been in the earlier version without locales and the
   7.103 +record extension proofs in which we needed to use conversion functions to
   7.104 +establish these facts.  We can transfer all facts that are
   7.105 +derived for groups to rings now. The subsequent proofs are not really hard
   7.106 +proofs, they are just instantiations of the known facts to rings. This is
   7.107 +because the elements of the ring and the group are now identified!! Before, in
   7.108 +the older version we could do something similar, but we always had to go the
   7.109 +longer way, via the implication R \\<in> Ring ==> R \\<in> Abelian group and then
   7.110 +conversion functions for the operators *)
   7.111 +
   7.112 +Goal "e \\<in> carrier R";
   7.113 +by (afs [R_carrier_def RS sym,e_closed] 1);
   7.114 +qed "R_e_closed";
   7.115 +
   7.116 +Goal "\\<forall>x \\<in> carrier R. e ## x = x";
   7.117 +by (afs [R_carrier_def RS sym,e_ax1] 1);
   7.118 +qed "R_e_ax1";
   7.119 +
   7.120 +Goal "op ## \\<in> carrier R \\<rightarrow> carrier R \\<rightarrow> carrier R";
   7.121 +by (afs [R_carrier_def RS sym, binop_funcset] 1);
   7.122 +qed "rplus_funcset";
   7.123 +
   7.124 +Goal "[| x \\<in> carrier R; y \\<in> carrier R |] ==> x ## y \\<in> carrier R";
   7.125 +by (afs  [rplus_funcset RS funcset_mem RS funcset_mem] 1);
   7.126 +qed "rplus_closed";
   7.127 +
   7.128 +Goal "[| a \\<in> carrier R; a ## a = a |] ==> a = e";
   7.129 +by (afs [ R_carrier_def RS sym, idempotent_e] 1);
   7.130 +qed "R_idempotent_e";
   7.131 +
   7.132 +Delsimps [simp_R, thm "Ring_R", thm "rmult_def", thm "R_id_G"];
   7.133 +
   7.134 +Goal "e ** e = e";
   7.135 +by (rtac R_idempotent_e 1);
   7.136 +by (blast_tac (claset() addIs [rmult_closed, R_e_closed]) 1);
   7.137 +by (simp_tac (simpset() addsimps [R_distrib1 RS sym, R_e_closed]) 1);
   7.138 +qed "R_e_mult_base";
   7.139 +
   7.140 +Close_locale "ring";
   7.141 +Close_locale "group";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/GroupTheory/Ring.thy	Mon Jul 23 17:47:49 2001 +0200
     8.3 @@ -0,0 +1,60 @@
     8.4 +(*  Title:      HOL/GroupTheory/Bij
     8.5 +    ID:         $Id$
     8.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     8.7 +    Copyright   1998-2001  University of Cambridge
     8.8 +
     8.9 +Ring theory. Sigma version
    8.10 +*)
    8.11 +
    8.12 +Ring = Coset +
    8.13 +
    8.14 +record 'a ringtype = 'a grouptype +
    8.15 +  Rmult    :: "['a, 'a] => 'a"
    8.16 +
    8.17 +syntax 
    8.18 +  "@Rmult"     :: "('a ringtype) => (['a, 'a] => 'a)"  ("_ .<m>"     [10] 10)
    8.19 +
    8.20 +translations 
    8.21 +  "R.<m>"  == "Rmult R"
    8.22 +
    8.23 +constdefs
    8.24 +  distr_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
    8.25 +    "distr_l S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S. 
    8.26 +                    (f1 x (f2 y z) = f2 (f1 x y) (f1 x z)))"
    8.27 +  distr_r       :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
    8.28 +    "distr_r S f1 f2 == (\\<forall>x \\<in> S. \\<forall>y \\<in> S. \\<forall>z \\<in> S. 
    8.29 +                    (f1 (f2 y z) x = f2 (f1 y x) (f1 z x)))"
    8.30 +
    8.31 +consts
    8.32 +  Ring :: "('a ringtype) set"
    8.33 +
    8.34 +defs 
    8.35 +  Ring_def
    8.36 +    "Ring == 
    8.37 +       {R. (| carrier = (R.<cr>), bin_op = (R.<f>),
    8.38 +	      inverse = (R.<inv>), unit = (R.<e>) |) \\<in> AbelianGroup &
    8.39 +           (R.<m>) \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>) & 
    8.40 +           (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). 
    8.41 +                        ((R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z)) &
    8.42 +           distr_l (R.<cr>)(R.<m>)(R.<f>) &
    8.43 +	   distr_r (R.<cr>)(R.<m>)(R.<f>) }"
    8.44 +
    8.45 +
    8.46 +constdefs
    8.47 +  group_of :: "'a ringtype => 'a grouptype"
    8.48 +   "group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
    8.49 +			        inverse = (R.<inv>), unit = (R.<e>) |)"
    8.50 +
    8.51 +locale ring = group +
    8.52 +  fixes
    8.53 +    R     :: "'a ringtype"
    8.54 +    rmult :: "['a, 'a] => 'a" (infixr "**" 80)
    8.55 +  assumes
    8.56 +    Ring_R "R \\<in> Ring"
    8.57 +  defines
    8.58 +    rmult_def "op ** == (R.<m>)"
    8.59 +    R_id_G    "G == group_of R"
    8.60 +
    8.61 +end
    8.62 +
    8.63 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/GroupTheory/RingConstr.ML	Mon Jul 23 17:47:49 2001 +0200
     9.3 @@ -0,0 +1,67 @@
     9.4 +(*  Title:      HOL/GroupTheory/RingConstr
     9.5 +    ID:         $Id$
     9.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     9.7 +    Copyright   1998-2001  University of Cambridge
     9.8 +
     9.9 +Construction of a ring from a semigroup and an Abelian group 
    9.10 +*)
    9.11 +
    9.12 +Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
    9.13 +\        R \\<in> ring_constr `` {G} `` {S} |] \
    9.14 +\     ==> R \\<in>  Ring";
    9.15 +by (force_tac (claset(), 
    9.16 +         simpset() addsimps [Ring_def, ring_constr_def, Abel_Abel, 
    9.17 +                             Semigroup_def]@[distr_l_def, distr_r_def]) 1); 
    9.18 +qed "RingC_Ring";
    9.19 +
    9.20 +Goal "R = (| carrier = R .<cr>, bin_op = R .<f>, inverse = R .<inv>,\
    9.21 +\                unit = R .<e>, Rmult = R .<m> |)";
    9.22 +by Auto_tac; 
    9.23 +qed "surjective_Ring";
    9.24 +
    9.25 +Goal "R \\<in>  Ring \
    9.26 +\     ==> \\<exists>G \\<in> AbelianGroup. \\<exists>S \\<in> Semigroup. R \\<in> ring_constr `` {G} `` {S}";
    9.27 +by (res_inst_tac [("x","group_of R")] bexI 1);
    9.28 +by (afs [Ring_def, group_of_def] 2);
    9.29 +by (res_inst_tac [("x","(| carrier = (R.<cr>), bin_op = (R.<m>) |)")] bexI 1);
    9.30 +by (afs [Ring_def, AbelianGroup_def, Semigroup_def] 2);
    9.31 +(* Now the main conjecture:
    9.32 + R\\<in>Ring
    9.33 +         ==> R\\<in>ring_constr `` {group_of R} ``
    9.34 +                 {(| carrier = R .<cr>, bin_op = R .<m> |)} *)
    9.35 +by (afs [ring_constr_def, Ring_def, group_of_def, AbelianGroup_def, 
    9.36 +         Semigroup_def,distr_l_def,distr_r_def] 1);
    9.37 +qed "Ring_RingC";
    9.38 +
    9.39 +
    9.40 +Goal "[| G \\<in> AbelianGroup; S \\<in> Semigroup; (S.<cr>) = (G.<cr>); \
    9.41 +\        distr_l (G .<cr>) (S .<f>) (G .<f>); \
    9.42 +\        distr_r (G .<cr>) (S .<f>) (G .<f>) |] \
    9.43 +\     ==> ring_from G S \\<in>  Ring";
    9.44 +by (rtac RingI 1);
    9.45 +by (ALLGOALS
    9.46 +    (asm_full_simp_tac (simpset() addsimps [ring_from_def, Abel_Abel, 
    9.47 +                                            Semigroup_def]))); 
    9.48 +qed "RingFrom_is_Ring";
    9.49 +
    9.50 +
    9.51 +Goal "ring_from \\<in> (PI G : AbelianGroup. {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) \
    9.52 +\         & distr_l (G.<cr>) (M.<f>) (G.<f>) & distr_r (G.<cr>) (M.<f>) (G.<f>)} \\<rightarrow> Ring)";
    9.53 +by (rtac Pi_I 1);
    9.54 +by (afs [ring_from_def] 2);
    9.55 +by (rtac funcsetI 1);
    9.56 +by (asm_full_simp_tac (simpset() addsimps [ring_from_def]) 2);
    9.57 +by (Force_tac 2);
    9.58 +by (afs [RingFrom_is_Ring] 1);
    9.59 +qed "RingFrom_arity";
    9.60 +
    9.61 +(* group_of, i.e. the group in a ring *)
    9.62 +
    9.63 +Goal "R \\<in> Ring ==> group_of R \\<in> AbelianGroup";
    9.64 +by (afs [group_of_def] 1);
    9.65 +by (etac (export R_Abel) 1);
    9.66 +qed "group_of_in_AbelianGroup";
    9.67 +
    9.68 +val R_Group = group_of_in_AbelianGroup RS Abel_imp_Group;
    9.69 +
    9.70 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/GroupTheory/RingConstr.thy	Mon Jul 23 17:47:49 2001 +0200
    10.3 @@ -0,0 +1,38 @@
    10.4 +(*  Title:      HOL/GroupTheory/RingConstr
    10.5 +    ID:         $Id$
    10.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
    10.7 +    Copyright   1998-2001  University of Cambridge
    10.8 +
    10.9 +Construction of a ring from a semigroup and an Abelian group 
   10.10 +*)
   10.11 +
   10.12 +RingConstr = Homomorphism +
   10.13 +
   10.14 +constdefs
   10.15 +  ring_of :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
   10.16 +  "ring_of ==
   10.17 +     lam G: AbelianGroup. lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
   10.18 +                   (| carrier = (G.<cr>), bin_op = (G.<f>), 
   10.19 +                      inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
   10.20 +
   10.21 +  ring_constr :: "('a grouptype * 'a semigrouptype *'a ringtype) set"
   10.22 +  "ring_constr ==
   10.23 +    \\<Sigma>G \\<in> AbelianGroup. \\<Sigma>S \\<in> {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>)}.
   10.24 +	 {R. R = (| carrier = (G.<cr>), bin_op = (G.<f>), 
   10.25 +		     inverse = (G.<inv>), unit = (G.<e>),
   10.26 +		     Rmult = (S.<f>) |) &
   10.27 +	     (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). 
   10.28 +	     ((R.<m>) x ((R.<f>) y z) = (R.<f>) ((R.<m>) x y) ((R.<m>) x z))) &
   10.29 +(\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). \\<forall>z \\<in> (R.<cr>). 
   10.30 +	     ((R.<m>) ((R.<f>) y z) x = (R.<f>) ((R.<m>) y x) ((R.<m>) z x)))}"
   10.31 +
   10.32 +  ring_from :: "['a grouptype, 'a semigrouptype] => 'a ringtype"
   10.33 +  "ring_from == lam G: AbelianGroup. 
   10.34 +     lam S: {M. M \\<in> Semigroup & (M.<cr>) = (G.<cr>) &
   10.35 +                distr_l (G.<cr>) (M.<f>) (G.<f>) &
   10.36 +	        distr_r (G.<cr>) (M.<f>) (G.<f>)}.
   10.37 +            (| carrier = (G.<cr>), bin_op = (G.<f>), 
   10.38 +               inverse = (G.<inv>), unit = (G.<e>), Rmult = (S.<f>) |)"
   10.39 +
   10.40 +end
   10.41 +