src/HOL/Algebra/Ring.thy

 
 text {*Usually, if this rule causes a failed congruence proof error,
    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
    Adding @{thm [source] Pi_def} to the simpset is often useful. *}
 
+lemma (in abelian_monoid) finsum_reindex:
+  assumes fin: "finite A"
+    shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
+        inj_on h A ==> finsum G f (h ` A) = finsum G (%x. f (h x)) A"
+  using fin apply induct
+  apply (auto simp add: finsum_insert Pi_def)
+done
+
+(* The following is wrong.  Needed is the equivalent of (^) for addition,
+  or indeed the canonical embedding from Nat into the monoid.
+
+lemma (in abelian_monoid) finsum_const:
+  assumes fin [simp]: "finite A"
+      and a [simp]: "a : carrier G"
+    shows "finsum G (%x. a) A = a (^) card A"
+  using fin apply induct
+  apply force
+  apply (subst finsum_insert)
+  apply auto
+  apply (force simp add: Pi_def)
+  apply (subst m_comm)
+  apply auto
+done
+*)
+
 
 section {* The Algebraic Hierarchy of Rings *}
-
 
 subsection {* Basic Definitions *}
 
 locale ring = abelian_group R + monoid R +
   assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]

   by (auto intro: ring.intro
     abelian_group.axioms ring_axioms.intro prems)
 
 lemma (in ring) is_abelian_group:
   "abelian_group R"
-  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
+  by unfold_locales
 
 lemma (in ring) is_monoid:
   "monoid R"
   by (auto intro!: monoidI m_assoc)
 

     finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
   qed (rule l_distr)
 qed (auto intro: cring.intro
   abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
 
+(*
 lemma (in cring) is_comm_monoid:
   "comm_monoid R"
   by (auto intro!: comm_monoidI m_assoc m_comm)
+*)
 
 lemma (in cring) is_cring:
   "cring R" by (rule cring_axioms)