# Re: [isabelle] Simplifier problem (Congruence rules?)

Hi Peter,
I managed to get the simplifier to do what you want. First, you will
need to prove a simp rule for rewriting list_case when both branches
are the same:
lemma list_case_const: "(case xs of [] => k | b # bs => k) = k"
by (induct xs) simp_all
You are also correct in thinking that the congruence rules are causing
problems. You will need to disable the default cong rule for
list_case, which you can do with "cong del". The following command
does what you want:
apply (simp add: list_case_const cong del: list.case_cong)
- Brian
On Tue, Oct 27, 2009 at 12:59 PM, Peter Lammich
<peter.lammich at uni-muenster.de> wrote:
> 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.*