481 apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1") |
481 apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1") |
482 apply (erule ssubst) |
482 apply (erule ssubst) |
483 apply (rule int_of_diff, auto) |
483 apply (rule int_of_diff, auto) |
484 done |
484 done |
485 |
485 |
486 (*FIXME: we should not have to rename x to x' below! There's a bug in the |
|
487 interaction between simproc inteq_cancel_numerals and the simplifier.*) |
|
488 lemma setsum_decr2: |
486 lemma setsum_decr2: |
489 "Finite(A) |
487 "Finite(A) |
490 ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M). |
488 ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M). |
491 setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) = |
489 setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) = |
492 (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a |
490 (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a |
493 else setsum(%x'. $# mcount(M, x'), A)))" |
491 else setsum(%x. $# mcount(M, x), A)))" |
494 apply (simp add: multiset_def) |
492 apply (simp add: multiset_def) |
495 apply (erule Finite_induct) |
493 apply (erule Finite_induct) |
496 apply (auto simp add: multiset_fun_iff mcount_def mset_of_def) |
494 apply (auto simp add: multiset_fun_iff mcount_def mset_of_def) |
497 done |
495 done |
498 |
496 |