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



Nice!
I'll soon try it out, it should make some of my proofs definitely more
elegant.

Peter

Brian Huffman wrote:
> 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.