*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Simplifier question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 19 Oct 2007 16:15:48 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <47188D99.7030704@uni-muenster.de>*References*: <47188D99.7030704@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias Peter Lammich wrote:

I have the following lemma about foldl: "foldl op @ ?i ?ww = ?i @ foldl op @ [] ?ww" (or with any other suitable operator like \<union>) Using this as a simplification lemma loops (I think because repeatedly rewriting the RHS with "?i=[]"). But reformulating the lemma as "?i~=[] ==> foldl op @ ?i ?ww = ?i @ foldl op @ [] ?ww" does not help, because I want it for all expressions ?i (except literal "[]"). Is there any way to set the simplifier up to make the intended simplification, i.e. simplify with the above lemma only if ?i is not a literal "[]" ? Many thanks in advance, yours Peter p.s. My current workaround is to instantiate ?i using [of exp], but I'd like to have it automatically.

**References**:**[isabelle] Simplifier question***From:*Peter Lammich

- Previous by Date: [isabelle] Isabelle and Computer Algebra
- Next by Date: [isabelle] induction: list
- Previous by Thread: [isabelle] Simplifier question
- Next by Thread: [isabelle] Isabelle and Computer Algebra
- Cl-isabelle-users October 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list