author ballarin Tue, 29 Jul 2008 16:17:45 +0200 changeset 27699 489e3f33af0e parent 27698 197f0517f0bd child 27700 ef4b26efa8b6
New theorems on summation.
 src/HOL/Algebra/FiniteProduct.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Ring.thy file | annotate | diff | comparison | revisions
```--- 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)```