# HG changeset patch
# User ballarin
# Date 1047661216 -3600
# Node ID f44f121dd275c6126c49f92119a864a032b13a25
# Parent  ec901a432ea10c532859b87a9d57296cb13118ec
Bugs fixed and operators finprod and finsum.

diff -r ec901a432ea1 -r f44f121dd275 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Mar 14 12:03:23 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy	Fri Mar 14 18:00:16 2003 +0100
@@ -5,9 +5,7 @@
   Copyright: Clemens Ballarin
 *)
 
-header {* The algebraic hierarchy of rings as axiomatic classes *}
-
-theory CRing = Group
+theory CRing = Summation
 files ("ringsimp.ML"):
 
 section {* The Algebraic Hierarchy of Rings *}
@@ -37,7 +35,13 @@
   divide_def:   "a / b = a * inverse b"
   power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
 *)
-subsection {* Basic Facts *}
+
+locale "domain" = cring +
+  assumes one_not_zero [simp]: "\<one> ~= \<zero>"
+    and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
+                  a = \<zero> | b = \<zero>"
+
+subsection {* Basic Facts of Rings *}
 
 lemma (in cring) a_magma [simp, intro]:
   "magma (| carrier = carrier R,
@@ -73,39 +77,42 @@
      mult = add R, one = zero R, m_inv = a_inv R |)"
   by (simp add: abelian_semigroup_def)
 
-lemma (in cring) a_abelian_group:
-  "abelian_group (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  by (simp add: abelian_group_def)
+lemmas group_record_simps = semigroup.simps monoid.simps group.simps
 
 lemmas (in cring) a_closed [intro, simp] =
-  magma.m_closed [OF a_magma, simplified]
+  magma.m_closed [OF a_magma, simplified group_record_simps]
 
 lemmas (in cring) zero_closed [intro, simp] = 
-  l_one.one_closed [OF a_l_one, simplified]
+  l_one.one_closed [OF a_l_one, simplified group_record_simps]
 
 lemmas (in cring) a_inv_closed [intro, simp] =
-  group.inv_closed [OF a_group, simplified]
+  group.inv_closed [OF a_group, simplified group_record_simps]
 
 lemma (in cring) minus_closed [intro, simp]:
   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
   by (simp add: minus_def)
 
-lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
+lemmas (in cring) a_l_cancel [simp] =
+  group.l_cancel [OF a_group, simplified group_record_simps]
 
-lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
+lemmas (in cring) a_r_cancel [simp] =
+  group.r_cancel [OF a_group, simplified group_record_simps]
 
-lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
+lemmas (in cring) a_assoc =
+  semigroup.m_assoc [OF a_semigroup, simplified group_record_simps]
 
-lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
+lemmas (in cring) l_zero [simp] =
+  l_one.l_one [OF a_l_one, simplified group_record_simps]
 
-lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
+lemmas (in cring) l_neg =
+  group.l_inv [OF a_group, simplified group_record_simps]
 
-lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
-  simplified]
+lemmas (in cring) a_comm =
+  abelian_semigroup.m_comm [OF a_abelian_semigroup,
+  simplified group_record_simps]
 
 lemmas (in cring) a_lcomm =
-  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
+  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps]
 
 lemma (in cring) r_zero [simp]:
   "x \<in> carrier R ==> x \<oplus> \<zero> = x"
@@ -117,11 +124,12 @@
   using group.r_inv [OF a_group]
   by simp
 
-lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
+lemmas (in cring) minus_zero [simp] =
+  group.inv_one [OF a_group, simplified group_record_simps]
 
 lemma (in cring) minus_minus [simp]:
   "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
-  using group.inv_inv [OF a_group, simplified]
+  using group.inv_inv [OF a_group, simplified group_record_simps]
   by simp
 
 lemma (in cring) minus_add:
@@ -217,6 +225,8 @@
   {* Method.ctxt_args cring_normalise *}
   {* computes distributive normal form in commutative rings (locales version) *}
 
+text {* Two examples for use of method algebra *}
+
 lemma
   includes cring R + cring S
   shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
@@ -228,4 +238,225 @@
   shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
   by algebra
 
+subsection {* Sums over Finite Sets *}
+
+text {*
+  This definition makes it easy to lift lemmas from @{term finprod}.
+*}
+
+constdefs
+  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+  "finsum R f A == finprod (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |) f A"
+
+lemma (in cring) a_abelian_monoid:
+  "abelian_monoid (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  by (simp add: abelian_monoid_def)
+
+(*
+  lemmas (in cring) finsum_empty [simp] =
+    abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified]
+  is dangeous, because attributes (like simplified) are applied upon opening
+  the locale, simplified refers to the simpset at that time!!!
+*)
+
+lemmas (in cring) finsum_empty [simp] =
+  abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_insert [simp] =
+  abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_zero =
+  abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_closed [simp] =
+  abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_Un_Int =
+  abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_Un_disjoint =
+  abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_addf =
+  abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_cong =
+  abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_0 [simp] =
+  abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_Suc [simp] =
+  abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_Suc2 =
+  abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_add [simp] =
+  abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+lemmas (in cring) finsum_cong' [cong] =
+  abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def,
+    simplified group_record_simps]
+
+(*
+lemma (in cring) finsum_empty [simp]:
+  "finsum R f {} = \<zero>"
+  by (simp add: finsum_def
+    abelian_monoid.finprod_empty [OF a_abelian_monoid])
+
+lemma (in cring) finsum_insert [simp]:
+  "[| finite F; a \<notin> F; f : F -> carrier R; f a \<in> carrier R |] ==>
+   finsum R f (insert a F) = f a \<oplus> finsum R f F"
+  by (simp add: finsum_def
+    abelian_monoid.finprod_insert [OF a_abelian_monoid])
+
+lemma (in cring) finsum_zero:
+  "finite A ==> finsum R (%i. \<zero>) A = \<zero>"
+  by (simp add: finsum_def
+    abelian_monoid.finprod_one [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_closed [simp]:
+  "[| finite A; f : A -> carrier R |] ==> finsum R f A \<in> carrier R"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_closed [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_Un_Int:
+  "[| finite A; finite B; g \<in> A -> carrier R; g \<in> B -> carrier R |] ==>
+     finsum R g (A Un B) \<oplus> finsum R g (A Int B) =
+     finsum R g A \<oplus> finsum R g B"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_Un_disjoint:
+  "[| finite A; finite B; A Int B = {};
+      g \<in> A -> carrier R; g \<in> B -> carrier R |]
+   ==> finsum R g (A Un B) = finsum R g A \<oplus> finsum R g B"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_addf:
+  "[| finite A; f \<in> A -> carrier R; g \<in> A -> carrier R |] ==>
+   finsum R (%x. f x \<oplus> g x) A = (finsum R f A \<oplus> finsum R g A)"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_multf [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_cong:
+  "[| A = B; g : B -> carrier R;
+      !!i. i : B ==> f i = g i |] ==> finsum R f A = finsum R g B"
+  apply (simp only: finsum_def)
+  apply (rule abelian_monoid.finprod_cong [OF a_abelian_monoid, simplified])
+  apply simp_all
+  done
+
+lemma (in cring) finsum_0 [simp]:
+  "f \<in> {0::nat} -> carrier R ==> finsum R f {..0} = f 0"
+  by (simp add: finsum_def
+    abelian_monoid.finprod_0 [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_Suc [simp]:
+  "f \<in> {..Suc n} -> carrier R ==>
+   finsum R f {..Suc n} = (f (Suc n) \<oplus> finsum R f {..n})"
+  by (simp add: finsum_def
+    abelian_monoid.finprod_Suc [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_Suc2:
+  "f \<in> {..Suc n} -> carrier R ==>
+   finsum R f {..Suc n} = (finsum R (%i. f (Suc i)) {..n} \<oplus> f 0)"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_add [simp]:
+  "[| f : {..n} -> carrier R; g : {..n} -> carrier R |] ==>
+     finsum R (%i. f i \<oplus> g i) {..n::nat} =
+     finsum R f {..n} \<oplus> finsum R g {..n}"
+  by (simp only: finsum_def
+    abelian_monoid.finprod_mult [OF a_abelian_monoid, simplified])
+
+lemma (in cring) finsum_cong' [cong]:
+  "[| A = B; !!i. i : B ==> f i = g i;
+      g \<in> B -> carrier R = True |] ==> finsum R f A = finsum R g B"
+  apply (simp only: finsum_def)
+  apply (rule abelian_monoid.finprod_cong' [OF a_abelian_monoid, simplified])
+  apply simp_all
+  done
+*)
+
+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 cring) finsum_ldistr:
+  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+   finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
+proof (induct set: Finites)
+  case empty then show ?case by simp
+next
+  case (insert F x) then show ?case by (simp add: Pi_def l_distr)
+qed
+
+lemma (in cring) finsum_rdistr:
+  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+   a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
+proof (induct set: Finites)
+  case empty then show ?case by simp
+next
+  case (insert F x) then show ?case by (simp add: Pi_def r_distr)
+qed
+
+subsection {* Facts of Integral Domains *}
+
+lemma (in "domain") zero_not_one [simp]:
+  "\<zero> ~= \<one>"
+  by (rule not_sym) simp
+
+lemma (in "domain") integral_iff: (* not by default a simp rule! *)
+  "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
+proof
+  assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
+  then show "a = \<zero> | b = \<zero>" by (simp add: integral)
+next
+  assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
+  then show "a \<otimes> b = \<zero>" by auto
+qed
+
+lemma (in "domain") m_lcancel:
+  assumes prem: "a ~= \<zero>"
+    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+  shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
+proof
+  assume eq: "a \<otimes> b = a \<otimes> c"
+  with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
+  with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
+  with prem and R have "b \<ominus> c = \<zero>" by auto 
+  with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
+  also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
+  finally show "b = c" .
+next
+  assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
+qed
+
+lemma (in "domain") m_rcancel:
+  assumes prem: "a ~= \<zero>"
+    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+  shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
+proof -
+  from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
+  with R show ?thesis by algebra
+qed
+
 end
diff -r ec901a432ea1 -r f44f121dd275 src/HOL/Algebra/Summation.thy
--- a/src/HOL/Algebra/Summation.thy	Fri Mar 14 12:03:23 2003 +0100
+++ b/src/HOL/Algebra/Summation.thy	Fri Mar 14 18:00:16 2003 +0100
@@ -5,9 +5,9 @@
 This file is largely based on HOL/Finite_Set.thy.
 *)
 
-theory FoldSet = Group:
+header {* Summation Operator *}
 
-section {* Summation operator *}
+theory Summation = Group:
 
 (* Instantiation of LC from Finite_Set.thy is not possible,
    because here we have explicit typing rules like x : carrier G.
@@ -293,18 +293,20 @@
   by (simp add: foldD_Un_Int
     left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
 
-subsection {* A Product Operator for Finite Sets *}
+subsection {* Products over Finite Sets *}
 
-text {*
-  Definition of product (or summation, if the monoid is written addivitively)
-  operator.
-*}
+constdefs
+  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
+  "finprod G f A == if finite A
+      then foldD (carrier G) (mult G o f) (one G) A
+      else arbitrary"
 
+(*
 locale finite_prod = abelian_monoid + var prod +
   defines "prod == (%f A. if finite A
       then foldD (carrier G) (op \<otimes> o f) \<one> A
       else arbitrary)"
-
+*)
 (* TODO: nice syntax for the summation operator inside the locale
    like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
 
@@ -313,9 +315,9 @@
 Context.>> (fn thy => (simpset_ref_of thy :=
   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
 
-lemma (in finite_prod) prod_empty [simp]: 
-  "prod f {} = \<one>"
-  by (simp add: prod_def)
+lemma (in abelian_monoid) finprod_empty [simp]: 
+  "finprod G f {} = \<one>"
+  by (simp add: finprod_def)
 
 ML_setup {* 
 
@@ -325,11 +327,11 @@
 declare funcsetI [intro]
   funcset_mem [dest]
 
-lemma (in finite_prod) prod_insert [simp]:
+lemma (in abelian_monoid) finprod_insert [simp]:
   "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
-   prod f (insert a F) = f a \<otimes> prod f F"
+   finprod G f (insert a F) = f a \<otimes> finprod G f F"
   apply (rule trans)
-  apply (simp add: prod_def)
+  apply (simp add: finprod_def)
   apply (rule trans)
   apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
     apply simp
@@ -337,11 +339,11 @@
       apply fast apply fast apply assumption
     apply (fastsimp intro: m_closed)
     apply simp+ apply fast
-  apply (auto simp add: prod_def)
+  apply (auto simp add: finprod_def)
   done
 
-lemma (in finite_prod) prod_one:
-  "finite A ==> prod (%i. \<one>) A = \<one>"
+lemma (in abelian_monoid) finprod_one:
+  "finite A ==> finprod G (%i. \<one>) A = \<one>"
 proof (induct set: Finites)
   case empty show ?case by simp
 next
@@ -350,29 +352,10 @@
   with insert show ?case by simp
 qed
 
-(*
-lemma prod_eq_0_iff [simp]:
-    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
-  by (induct set: Finites) auto
-
-lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: prod_def)
-  apply (erule rev_mp)
-  apply (erule finite_induct)
-   apply auto
-  done
-
-lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
-*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
-(*
-  by (induct set: Finites) auto
-*)
-
-lemma (in finite_prod) prod_closed:
+lemma (in abelian_monoid) finprod_closed [simp]:
   fixes A
   assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
-  shows "prod f A \<in> carrier G"
+  shows "finprod G f A \<in> carrier G"
 using fin f
 proof induct
   case empty show ?case by simp
@@ -391,50 +374,33 @@
   "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   by fast
 
-lemma (in finite_prod) prod_Un_Int:
+lemma (in abelian_monoid) finprod_Un_Int:
   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
-   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
+     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
+     finprod G g A \<otimes> finprod G g B"
   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
 proof (induct set: Finites)
-  case empty then show ?case by (simp add: prod_closed)
+  case empty then show ?case by (simp add: finprod_closed)
 next
   case (insert A a)
   then have a: "g a \<in> carrier G" by fast
   from insert have A: "g \<in> A -> carrier G" by fast
   from insert A a show ?case
-    by (simp add: ac Int_insert_left insert_absorb prod_closed
+    by (simp add: ac Int_insert_left insert_absorb finprod_closed
           Int_mono2 Un_subset_iff) 
 qed
 
-lemma (in finite_prod) prod_Un_disjoint:
+lemma (in abelian_monoid) finprod_Un_disjoint:
   "[| finite A; finite B; A Int B = {};
       g \<in> A -> carrier G; g \<in> B -> carrier G |]
-   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
-  apply (subst prod_Un_Int [symmetric])
-    apply (auto simp add: prod_closed)
+   ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
+  apply (subst finprod_Un_Int [symmetric])
+    apply (auto simp add: finprod_closed)
   done
 
-(*
-lemma prod_UN_disjoint:
-  fixes f :: "'a => 'b::plus_ac0"
-  shows
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
-  apply (induct set: Finites)
-   apply simp
-  apply atomize
-  apply (subgoal_tac "ALL i:F. x \<noteq> i")
-   prefer 2 apply blast
-  apply (subgoal_tac "A x Int UNION F A = {}")
-   prefer 2 apply blast
-  apply (simp add: prod_Un_disjoint)
-  done
-*)
-
-lemma (in finite_prod) prod_addf:
+lemma (in abelian_monoid) finprod_multf:
   "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
-   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
+   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
 proof (induct set: Finites)
   case empty show ?case by simp
 next
@@ -447,138 +413,85 @@
   from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
     by (simp add: Pi_def)
   show ?case  (* check if all simps are really necessary *)
-    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
+    by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
 qed
 
-(*
-lemma prod_Un: "finite A ==> finite B ==>
-    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
-  apply (subst prod_Un_Int [symmetric])
-    apply auto
-  done
-
-lemma prod_diff1: "(prod f (A - {a}) :: nat) =
-    (if a:A then prod f A - f a else prod f A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: prod_def)
-  apply (erule finite_induct)
-   apply (auto simp add: insert_Diff_if)
-  apply (drule_tac a = a in mk_disjoint_insert)
-  apply auto
-  done
-*)
-
-text {*
-  Congruence rule.  The simplifier requires the rule to be in this form.
-*}
-(*
-lemma (in finite_prod) prod_cong [cong]:
-  "[| A = B; !!i. i \<in> B ==> f i = g i;
-      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
-*)
-lemma (in finite_prod) prod_cong:
-  "[| A = B; g \<in> B -> carrier G;
-      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
-
+lemma (in abelian_monoid) finprod_cong:
+  "[| A = B; g : B -> carrier G;
+      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
 proof -
-  assume prems: "A = B"
-    "!!i. i \<in> B ==> f i = g i"
-    "g \<in> B -> carrier G"
+  assume prems: "A = B" "g : B -> carrier G"
+    "!!i. i : B ==> f i = g i"
   show ?thesis
   proof (cases "finite B")
     case True
-    then have "!!A. [| A = B; g \<in> B -> carrier G;
-      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
+    then have "!!A. [| A = B; g : B -> carrier G;
+      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
     proof induct
       case empty thus ?case by simp
     next
       case (insert B x)
-      then have "prod f A = prod f (insert x B)" by simp
-      also from insert have "... = f x \<otimes> prod f B"
-      proof (intro prod_insert)
+      then have "finprod G f A = finprod G f (insert x B)" by simp
+      also from insert have "... = f x \<otimes> finprod G f B"
+      proof (intro finprod_insert)
 	show "finite B" .
       next
-	show "x \<notin> B" .
+	show "x ~: B" .
       next
-	assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
 	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f \<in> B -> carrier G" by fastsimp
+	thus "f : B -> carrier G" by fastsimp
       next
 	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
 	  "g \<in> insert x B \<rightarrow> carrier G"
 	thus "f x \<in> carrier G" by fastsimp
       qed
-      also from insert have "... = g x \<otimes> prod g B" by fastsimp
-      also from insert have "... = prod g (insert x B)"
-      by (intro prod_insert [THEN sym]) auto
+      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
+      also from insert have "... = finprod G g (insert x B)"
+      by (intro finprod_insert [THEN sym]) auto
       finally show ?case .
     qed
     with prems show ?thesis by simp
   next
-    case False with prems show ?thesis by (simp add: prod_def)
+    case False with prems show ?thesis by (simp add: finprod_def)
   qed
 qed
 
-lemma (in finite_prod) prod_cong1 [cong]:
-  "[| A = B; !!i. i \<in> B ==> f i = g i;
-      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
-  by (rule prod_cong) fast+
+lemma (in abelian_monoid) finprod_cong' [cong]:
+  "[| A = B; !!i. i : B ==> f i = g i;
+      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
+  by (rule finprod_cong) fast+
 
-text {*
-   Usually, if this rule causes a failed congruence proof error,
-   the reason is that the premise @{text "g \<in> B -> carrier G"} could not
-   be shown. Adding @{thm [source] Pi_def} to the simpset is often useful.
-*}
+text {*Usually, if this rule causes a failed congruence proof error,
+   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
+   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
 
 declare funcsetI [rule del]
   funcset_mem [rule del]
 
-subsection {* Summation over the integer interval @{term "{..n}"} *}
-
-text {*
-  A new locale where the index set is restricted to @{term "nat"} is
-  necessary, because currently locales demand types in theorems to be as
-  general as in the locale's definition.
-*}
-
-locale finite_prod_nat = finite_prod +
-  assumes "False ==> prod f (A::nat set) = prod f A"
-
-lemma (in finite_prod_nat) natSum_0 [simp]:
-  "f \<in> {0::nat} -> carrier G ==> prod f {..0} = f 0"
+lemma (in abelian_monoid) finprod_0 [simp]:
+  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
 by (simp add: Pi_def)
 
-lemma (in finite_prod_nat) natsum_Suc [simp]:
-  "f \<in> {..Suc n} -> carrier G ==>
-   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
+lemma (in abelian_monoid) finprod_Suc [simp]:
+  "f : {..Suc n} -> carrier G ==>
+   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
 by (simp add: Pi_def atMost_Suc)
 
-lemma (in finite_prod_nat) natsum_Suc2:
-  "f \<in> {..Suc n} -> carrier G ==>
-   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
+lemma (in abelian_monoid) finprod_Suc2:
+  "f : {..Suc n} -> carrier G ==>
+   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
 proof (induct n)
   case 0 thus ?case by (simp add: Pi_def)
 next
-  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
+  case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed)
 qed
 
-lemma (in finite_prod_nat) natsum_zero [simp]:
-  "prod (%i. \<one>) {..n::nat} = \<one>"
-by (induct n) (simp_all add: Pi_def)
-
-lemma (in finite_prod_nat) natsum_add [simp]:
-  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
-   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
-by (induct n) (simp_all add: ac Pi_def prod_closed)
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+lemma (in abelian_monoid) finprod_mult [simp]:
+  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+     finprod G (%i. f i \<otimes> g i) {..n::nat} =
+     finprod G f {..n} \<otimes> finprod G g {..n}"
+  by (induct n) (simp_all add: ac Pi_def finprod_closed)
 
 end
+
diff -r ec901a432ea1 -r f44f121dd275 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Mar 14 12:03:23 2003 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Mar 14 18:00:16 2003 +0100
@@ -64,9 +64,9 @@
 val cring_ss = HOL_ss settermless termless_ring;
 
 fun cring_normalise ctxt = let
-    fun filter t = case HOLogic.dest_Trueprop t of
+    fun filter t = (case HOLogic.dest_Trueprop t of
         Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
-      | _ => [] 
+      | _ => [])
       handle TERM _ => [];
     val insts = flat (map (filter o #prop o rep_thm)
       (ProofContext.prems_of ctxt));