src/HOL/GroupTheory/Ring.thy

             "[|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?*)
+constdefs
   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)
 
 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"
+lemma ringI:
+     "[|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) 

      "[|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 {*Example: The Ring of Integers*}
+
+constdefs
+ integers :: "int ring"
+  "integers == (|carrier = UNIV, 
+                 sum = op +,
+                 gminus = (%x. -x),
+                 zero = 0::int,
+                 prod = op *|)"
+
+theorem ring_integers: "ring (integers)"
+by (simp add: integers_def ring_def ring_axioms_def 
+              distrib_l_def distrib_r_def 
+              zadd_zmult_distrib zadd_zmult_distrib2 
+              abelian_group_axioms_def group_axioms_def semigroup_def) 
+
+
 subsection {*Ring Homomorphisms*}
 
 constdefs
  ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set"
   "ring_hom R R' ==

 
 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 
+              ring_hom_def Bij_Inv_mem restrictI 
               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 (blast 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