# Re: [isabelle] Common sub-expression elimination

I don't think any user-supplied theorem theorem should be necessary. If a
term tm[s] contains multiple occurrences of a subterm s, then (\x. tm[x]) s
= tm is always provable. There may already be a let-like construct that is
syntactic sugar for that lambda abstraction.
On 19 January 2016 at 21:30, Manuel Eberl <eberlm at in.tum.de> wrote:
> I was wondering whether there is any work on common subexpression
> elimination, ideally in a generic fashion, similar to the Reification tool
> by Amine Chaieb.
>
> This would, of course, be interesting in general, but parcitularly for the
> approximation decision procedure. I believe that CSE is complex enough to
> make a generic mechanism for it interesting.
>
>
> If something like this does not exist, it might make a nice student
> project. What I am envisioning is something that
> â takes a HOL term
> â returns one or all subterms that occur more than once
> â ideally, provides some mechanism for "pulling out" all occurrences of a
> common subexpression, e.g. by putting them in a "let"-like construct (e.g.
> by a user-supplied theorem that says that one can "pull out" terms like
> this)
> To make things easier, one can possibly assume that the term does not
> contain any Î-abstractions.
>
>
> Cheers,
>
> Manuel
>
>

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