diff -r a246a0a52dfb -r 5fcc8bf538ee src/HOL/GroupTheory/Ring.thy
--- a/src/HOL/GroupTheory/Ring.thy	Wed Sep 25 11:23:26 2002 +0200
+++ b/src/HOL/GroupTheory/Ring.thy	Thu Sep 26 10:40:13 2002 +0200
@@ -1,60 +1,204 @@
 (*  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
 *)
 
-Ring = Coset +
+header{*Ring Theory*}
+
+theory Ring = Bij + Coset:
+
+
+subsection{*Definition of a Ring*}
+
+record 'a ring  = "'a group" +
+  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)
+
+record 'a unit_ring  = "'a ring" +
+  one :: 'a    ("\<one>\<index>")
+
+
+text{*Abbrevations for the left and right distributive laws*}
+constdefs
+  distrib_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+    "distrib_l A f g ==
+       (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f x (g y z) = g (f x y) (f x z)))"
 
-record 'a ringtype = 'a grouptype +
-  Rmult    :: "['a, 'a] => 'a"
+  distrib_r       :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
+    "distrib_r A f g == 
+       (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f (g y z) x = g (f y x) (f z x)))"
+
+
+locale ring = abelian_group R +
+  assumes prod_funcset: "prod R \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R"
+      and prod_assoc:   
+            "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|] 
+             ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+      and left:  "distrib_l (carrier R) (prod R) (sum R)"
+      and right: "distrib_r (carrier R) (prod R) (sum R)"
+
+constdefs (*????FIXME needed?*)
+  Ring :: "('a,'b) ring_scheme set"
+   "Ring == Collect ring"
+
+
+lemma ring_is_abelian_group: "ring(R) ==> abelian_group(R)"
+by (simp add: ring_def abelian_group_def)
 
-syntax 
-  "@Rmult"     :: "('a ringtype) => (['a, 'a] => 'a)"  ("_ .<m>"     [10] 10)
+text{*Construction of a ring from a semigroup and an Abelian group*}
+lemma "[|abelian_group R; 
+         semigroup(|carrier = carrier R, sum = prod R|);
+         distrib_l (carrier R) (prod R) (sum R);
+         distrib_r (carrier R) (prod R) (sum R)|] ==> ring R"
+by (simp add: abelian_group_def ring_def ring_axioms_def semigroup_def) 
+
+lemma (in ring) prod_closed [simp]:
+     "[| x \<in> carrier R; y \<in> carrier R |] ==>  x \<cdot> y \<in> carrier R"
+apply (insert prod_funcset) 
+apply (blast dest: funcset_mem) 
+done
+
+declare ring.prod_closed [simp]
+
+lemma (in ring) sum_closed:
+     "[| x \<in> carrier R; y \<in> carrier R |] ==>  x \<oplus> y \<in> carrier R"
+by simp 
+
+declare ring.sum_closed [simp]
 
-translations 
-  "R.<m>"  == "Rmult R"
+lemma (in ring) distrib_left:
+     "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]  
+      ==> x \<cdot> (y \<oplus> z) = (x \<cdot> y) \<oplus> (x \<cdot> z)"
+apply (insert left) 
+apply (simp add: distrib_l_def)
+done
+
+lemma (in ring) distrib_right:
+     "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]  
+      ==> (y \<oplus> z) \<cdot> x = (y \<cdot> x) \<oplus> (z \<cdot> x)"
+apply (insert right) 
+apply (simp add: distrib_r_def)
+done
+
+lemma (in ring) prod_zero_left: "x \<in> carrier R ==> \<zero> \<cdot> x = \<zero>"
+by (simp add: idempotent_imp_zero distrib_right [symmetric])
+
+lemma (in ring) prod_zero_right: "x \<in> carrier R ==> x \<cdot> \<zero> = \<zero>"
+by (simp add: idempotent_imp_zero distrib_left [symmetric])
+
+lemma (in ring) prod_minus_left:
+     "[|x \<in> carrier R; y \<in> carrier R|]  
+      ==> (\<ominus>x) \<cdot> y = \<ominus> (x \<cdot> y)"
+by (simp add: minus_unique prod_zero_left distrib_right [symmetric]) 
+
+lemma (in ring) prod_minus_right:
+     "[|x \<in> carrier R; y \<in> carrier R|]  
+      ==> x \<cdot> (\<ominus>y) = \<ominus> (x \<cdot> y)"
+by (simp add: minus_unique prod_zero_right distrib_left [symmetric]) 
+
+
+subsection {*Ring Homomorphisms*}
 
 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)))"
+ ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set"
+  "ring_hom R R' ==
+   {h. h \<in> carrier R -> carrier R' & 
+       (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(sum R x y) = sum R' (h x) (h y)) &
+       (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(prod R x y) = prod R' (h x) (h y))}"
+
+ ring_auto :: "('a,'b)ring_scheme => ('a => 'a)set"
+  "ring_auto R == ring_hom R R \<inter> Bij(carrier R)"
 
-consts
-  Ring :: "('a ringtype) set"
+  RingAutoGroup :: "[('a,'c) ring_scheme] => ('a=>'a) group"
+  "RingAutoGroup R == BijGroup (carrier R) (|carrier := ring_auto R |)"
+
+
+lemma ring_hom_subset_hom: "ring_hom R R' <= hom R R'"
+by (force simp add: ring_hom_def hom_def)
+
+subsection{*The Ring Automorphisms From a Group*}
+
+lemma id_in_ring_auto: "ring R ==> (%x: carrier R. x) \<in> ring_auto R"
+by (simp add: ring_auto_def ring_hom_def restrictI ring.axioms id_Bij) 
 
-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>) }"
+lemma restrict_Inv_ring_hom:
+      "[|ring R; h \<in> ring_hom R R; h \<in> Bij (carrier R)|]
+       ==> restrict (Inv (carrier R) h) (carrier R) \<in> ring_hom R R"
+by (simp add: ring.axioms group.axioms 
+              ring_hom_def Bij_Inv_mem restrictI ring.sum_closed 
+              semigroup.sum_funcset ring.prod_funcset Bij_Inv_lemma)
+
+text{*Ring automorphisms are a subgroup of the group of bijections over the 
+   ring's carrier, and thus a group*}
+lemma subgroup_ring_auto:
+      "ring R ==> subgroup (ring_auto R) (BijGroup (carrier R))"
+apply (rule group.subgroupI) 
+    apply (rule group_BijGroup) 
+   apply (force simp add: ring_auto_def BijGroup_def) 
+  apply (blast intro: dest: id_in_ring_auto) 
+ apply (simp add: ring_auto_def BijGroup_def restrict_Inv_Bij
+                  restrict_Inv_ring_hom) 
+apply (simp add: ring_auto_def BijGroup_def compose_Bij)
+apply (simp add: ring_hom_def compose_def Pi_def)
+done
+
+lemma ring_auto: "ring R ==> group (RingAutoGroup R)"
+apply (drule subgroup_ring_auto) 
+apply (simp add: subgroup_def RingAutoGroup_def) 
+done
 
 
-constdefs
-  group_of :: "'a ringtype => 'a grouptype"
-   "group_of == %R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
-			        inverse = (R.<inv>), unit = (R.<e>) |)"
+subsection{*A Locale for a Pair of Rings and a Homomorphism*}
+
+locale ring_homomorphism = ring R + ring R' +
+  fixes h
+  assumes homh: "h \<in> ring_hom R R'"
+
+lemma ring_hom_sum:
+     "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] 
+      ==> h(sum R x y) = sum R' (h x) (h y)"
+by (simp add: ring_hom_def) 
+
+lemma ring_hom_prod:
+     "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] 
+      ==> h(prod R x y) = prod R' (h x) (h y)"
+by (simp add: ring_hom_def) 
+
+lemma ring_hom_closed:
+     "[|h \<in> ring_hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
+by (auto simp add: ring_hom_def funcset_mem)
+
+lemma (in ring_homomorphism) ring_hom_sum [simp]:
+     "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
+by (simp add: ring_hom_sum [OF homh])
 
-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"
+lemma (in ring_homomorphism) ring_hom_prod [simp]:
+     "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<cdot>\<^sub>1 y) = (h x) \<cdot>\<^sub>2 (h y)"
+by (simp add: ring_hom_prod [OF homh])
+
+lemma (in ring_homomorphism) group_homomorphism: "group_homomorphism R R' h"
+by (simp add: group_homomorphism_def group_homomorphism_axioms_def
+              prems homh ring_hom_subset_hom [THEN subsetD])
+
+lemma (in ring_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier R'"
+by (simp add: ring_hom_closed [OF homh]) 
+
+lemma (in ring_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
+by (rule group_homomorphism.hom_zero [OF group_homomorphism]) 
+
+lemma (in ring_homomorphism) hom_minus_closed [simp]:
+     "x \<in> carrier R ==> h (\<ominus>x) \<in> carrier R'"
+by (rule group_homomorphism.hom_minus_closed [OF group_homomorphism]) 
+
+lemma (in ring_homomorphism) hom_minus [simp]:
+     "x \<in> carrier R ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
+by (rule group_homomorphism.hom_minus [OF group_homomorphism]) 
+
+
+text{*Needed because the standard theorem @{text "ring_homomorphism.intro"} 
+is unnatural.*}
+lemma ring_homomorphismI:
+    "[|ring R; ring R'; h \<in> ring_hom R R'|] ==> ring_homomorphism R R' h"
+by (simp add: ring_def ring_homomorphism_def ring_homomorphism_axioms_def)
 
 end
-
-