[isabelle] Simplifier problem (Congruence rules?)



Hi all,

I have some problem with the simplifier, probably with congruence rule
setup:

Consider the goal:
  "P (\<Union>x\<in>S.
      case x of
        [] \<Rightarrow> f True |
        (a#as) \<Rightarrow>
          f (case c x of [] \<Rightarrow> True | (b#bs) \<Rightarrow> True)
    )"

is there any way to set up the simplifier such that it will rewrite this
goal to:
 "P (\<Union>x\<in>S. f True)" ?

Regards & thanks for any help in advance,
  Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.