Re: [isabelle] Simplifier question

I don't think this can be done except by a simplification procedure (in ML) which looks at the actual term representation.


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

p.s. My current workaround is to instantiate ?i using [of exp], but I'd
like to have it automatically.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.