src/HOL/Finite_Set.thy
changeset 16632 ad2895beef79
parent 16550 e14b89d6ef13
child 16733 236dfafbeb63
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jul 01 04:32:33 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jul 01 13:51:11 2005 +0200
     1.3 @@ -891,6 +891,10 @@
     1.4    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
     1.5  by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
     1.6  
     1.7 +lemma strong_setsum_cong:
     1.8 +  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B"
     1.9 +by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
    1.10 +
    1.11  lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
    1.12    by (rule setsum_cong[OF refl], auto);
    1.13  
    1.14 @@ -1272,6 +1276,10 @@
    1.15    "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
    1.16  by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
    1.17  
    1.18 +lemma strong_setprod_cong:
    1.19 +  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
    1.20 +by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
    1.21 +
    1.22  lemma setprod_reindex_cong: "inj_on f A ==>
    1.23      B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
    1.24    by (frule setprod_reindex, simp)