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.