# [isabelle] Simplifier question

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.

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