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

author | berghofe |

Fri, 01 Jul 2005 14:01:13 +0200 | |

changeset 16637 | 62dff56b43d3 |

parent 16636 | 1ed737a98198 |

child 16638 | 3dc904d93767 |

Tuned finsum_cong to allow that premises are simplified more eagerly.

--- a/src/HOL/Algebra/CRing.thy Fri Jul 01 13:57:53 2005 +0200 +++ b/src/HOL/Algebra/CRing.thy Fri Jul 01 14:01:13 2005 +0200 @@ -277,10 +277,10 @@ simplified monoid_record_simps]) lemma (in abelian_monoid) finsum_cong: - "[| A = B; f : B -> carrier G = True; - !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B" + "[| A = B; f : B -> carrier G; + !!i. i : B =simp=> 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 + simplified monoid_record_simps]) (auto simp add: simp_implies_def) 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.