src/HOL/Algebra/Ring.thy

   Copyright: Clemens Ballarin
 *)
 
 theory Ring
 imports FiniteProduct
-uses ("ringsimp.ML") begin
+uses ("ringsimp.ML")
+begin
 
 
 section {* The Algebraic Hierarchy of Rings *}
 
 subsection {* Abelian Groups *}

   zero :: 'a ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
 
 text {* Derived operations. *}
 
-constdefs (structure R)
+definition
   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
-  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
-
+  where "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+
+definition
   a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
+  where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y == x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 locale abelian_monoid =
   fixes G (structure)
   assumes a_comm_monoid:
      "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"

 qed
 
 
 subsection {* Morphisms *}
 
-constdefs (structure R S)
+definition
   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
-  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
+  where "ring_hom R S ==
+    {h. h \<in> carrier R -> carrier S &
       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
-        h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
-      h \<one> = \<one>\<^bsub>S\<^esub>}"
+        h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
+      h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
 
 lemma ring_hom_memI:
   fixes R (structure) and S (structure)
   assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
     and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>