# HG changeset patch
# User ballarin
# Date 1064927426 -7200
# Node ID 7bf882b0a51e69ce330b50f08d9e900352e25b27
# Parent  cd05b503ca2da263bdd816324870fc418e8a7dd7
Changed order of prems in finprod_cong.  Slight speedup.

diff -r cd05b503ca2d -r 7bf882b0a51e src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Tue Sep 30 15:09:35 2003 +0200
+++ b/src/HOL/Algebra/CRing.thy	Tue Sep 30 15:10:26 2003 +0200
@@ -276,8 +276,8 @@
     simplified monoid_record_simps])
 
 lemma (in abelian_monoid) finsum_cong:
-  "[| A = B; !!i. i : B ==> f i = g i;
-      g : B -> carrier G = True |] ==> finsum G f A = finsum G g B"
+  "[| A = B;
+      f : B -> carrier G = True; !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps]) auto
 
diff -r cd05b503ca2d -r 7bf882b0a51e src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Tue Sep 30 15:09:35 2003 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Sep 30 15:10:26 2003 +0200
@@ -441,9 +441,10 @@
 qed
 
 lemma (in comm_monoid) finprod_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+
+  "[| A = B; f : B -> carrier G = True;
+      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+  (* This order of prems is slightly faster (3%) than the last two swapped. *)
+  by (rule finprod_cong') force+
 
 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.