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> 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.