New theorems on summation.

--- a/src/HOL/Algebra/FiniteProduct.thy	Tue Jul 29 16:17:13 2008 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Jul 29 16:17:45 2008 +0200
@@ -486,5 +486,27 @@
      finprod G f {..n} \<otimes> finprod G g {..n}"
   by (induct n) (simp_all add: m_ac Pi_def)
 
+(* The following two were contributed by Jeremy Avigad. *)
+
+lemma (in comm_monoid) finprod_reindex:
+  assumes fin: "finite A"
+    shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
+        inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
+  using fin apply induct
+  apply (auto simp add: finprod_insert Pi_def)
+done
+
+lemma (in comm_monoid) finprod_const:
+  assumes fin [simp]: "finite A"
+      and a [simp]: "a : carrier G"
+    shows "finprod G (%x. a) A = a (^) card A"
+  using fin apply induct
+  apply force
+  apply (subst finprod_insert)
+  apply auto
+  apply (force simp add: Pi_def)
+  apply (subst m_comm)
+  apply auto
+done
+
 end
-

--- a/src/HOL/Algebra/Ring.thy	Tue Jul 29 16:17:13 2008 +0200
+++ b/src/HOL/Algebra/Ring.thy	Tue Jul 29 16:17:45 2008 +0200
@@ -315,10 +315,34 @@
    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 +
@@ -354,7 +378,7 @@
 
 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"
@@ -394,9 +418,11 @@
 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)