[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
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