Changed order of prems in finprod_cong. Slight speedup.
authorballarin
Tue Sep 30 15:10:26 2003 +0200 (2003-09-30)
changeset 142137bf882b0a51e
parent 14212 cd05b503ca2d
child 14214 5369d671f100
Changed order of prems in finprod_cong. Slight speedup.
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/FiniteProduct.thy
     1.1 --- a/src/HOL/Algebra/CRing.thy	Tue Sep 30 15:09:35 2003 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Tue Sep 30 15:10:26 2003 +0200
     1.3 @@ -276,8 +276,8 @@
     1.4      simplified monoid_record_simps])
     1.5  
     1.6  lemma (in abelian_monoid) finsum_cong:
     1.7 -  "[| A = B; !!i. i : B ==> f i = g i;
     1.8 -      g : B -> carrier G = True |] ==> finsum G f A = finsum G g B"
     1.9 +  "[| A = B;
    1.10 +      f : B -> carrier G = True; !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
    1.11    by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
    1.12      simplified monoid_record_simps]) auto
    1.13  
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Sep 30 15:09:35 2003 +0200
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Sep 30 15:10:26 2003 +0200
     2.3 @@ -441,9 +441,10 @@
     2.4  qed
     2.5  
     2.6  lemma (in comm_monoid) finprod_cong:
     2.7 -  "[| A = B; !!i. i : B ==> f i = g i;
     2.8 -      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
     2.9 -  by (rule finprod_cong') fast+
    2.10 +  "[| A = B; f : B -> carrier G = True;
    2.11 +      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
    2.12 +  (* This order of prems is slightly faster (3%) than the last two swapped. *)
    2.13 +  by (rule finprod_cong') force+
    2.14  
    2.15  text {*Usually, if this rule causes a failed congruence proof error,
    2.16    the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.