summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | ballarin |

Tue, 30 Sep 2003 15:10:26 +0200 | |

changeset 14213 | 7bf882b0a51e |

parent 14212 | cd05b503ca2d |

child 14214 | 5369d671f100 |

Changed order of prems in finprod_cong. Slight speedup.

src/HOL/Algebra/CRing.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/FiniteProduct.thy | file | annotate | diff | comparison | revisions |

--- 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

--- 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.